# 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"]
# wai-ops' feature of the same name, declared so that the sources the model checker
# includes from wai-ops (`stage/mod.rs`) name a known feature. Their 32-bit forms are
# compiled under `cfg(kani)` whatever it says.
i32_forms = []
# wai-rs's test-only feature (its direct decodes), declared for the same reason: the
# staged-delivery predictors this crate includes are compiled under it, `test` or
# `cfg(kani)`.
legacy_int = []

[[bin]]
name = "wai-verify"
path = "src/bin/wai-verify/main.rs"
required-features = ["cli"]