9006e7aea4
Harnesses whose windows the checker did not finish within their cap (ten or twenty minutes on an idle 32-core host) are gated by cfg(kani_open): kept in the source with their statements, compiled and run only on request (RUSTFLAGS="--cfg kani_open" cargo kani --lib --exact --harness <name>), so that every harness CI compiles verifies. check_shards.py counts them apart. wai-verify declares the cfg. The shards, from the measured times: the wai-rs harnesses; arith and limb; the two 512-bit isqrt harnesses; the stage harnesses; the two longest stage harnesses (K26, and K29 over every range, renamed so a filter names it alone); sound; plan. Co-Authored-By: Claude Opus 5.5 <[email protected]>
36 lines
1.3 KiB
TOML
36 lines
1.3 KiB
TOML
# Formal verification host for WAI's integer core.
|
|
#
|
|
# Deliberately a SEPARATE tiny crate, mirroring `byte-exact-conformance`: it
|
|
# `#[path]`-includes the pure-integer sources from wai-rs (single source of
|
|
# truth, no copy) so the model checker sees a minimal dependency closure —
|
|
# which is what makes the proofs tractable.
|
|
#
|
|
# NOTE: no `rust-version` on purpose. The verifier ships its own pinned nightly
|
|
# toolchain; an MSRV above it makes cargo refuse to build the proof harnesses.
|
|
[package]
|
|
name = "wai-verify"
|
|
version = "0.1.0"
|
|
edition = "2024"
|
|
license = "Apache-2.0"
|
|
publish = false
|
|
|
|
# `cfg(kani)` is set by the model checker on the included sources. Declared so an
|
|
# ordinary build or clippy run of this crate does not warn on it.
|
|
[lints.rust]
|
|
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)", "cfg(kani_open)"] }
|
|
|
|
[dependencies]
|
|
# None for the library: the integer core this crate verifies is pure std. The
|
|
# `wai-verify` tool (the bounds certifier, the lowerings and the conformance corpus
|
|
# of `wai-ops/1`) drives the `wai-ops` crate, behind the `cli` feature, so that the
|
|
# model checker's compilation environment stays the included sources and nothing
|
|
# else.
|
|
wai-ops = { path = "../wai-ops", optional = true }
|
|
|
|
[features]
|
|
cli = ["dep:wai-ops"]
|
|
|
|
[[bin]]
|
|
name = "wai-verify"
|
|
path = "src/bin/wai-verify/main.rs"
|
|
required-features = ["cli"]
|