f2513980d8
The arithmetic guards of the direct decodes (their own predictors, and the
saturating step of wir1_arith) no longer run outside the test-only decode;
the stage operators carry them now.
- int_video::predict is E10 on an RGB8 frame (the encoder predicts with it,
as the decode does); the direct predictor, verbatim, is
int_video::legacy::predict, test-only.
- staged::wir1: the direct decode's pred_at and step are legacy's. The
encoder predicts with the decode's E11, E12 or the element below
(ops::prediction) and steps with E9; it refuses a stage below of the wrong
shape or element type up front. ops::{up2_prediction, rate_prediction} are
E11 and E12 on the interleaved layouts, which the staged-measurement and
staged-corpus tools now call.
- staged::predict's up2_at, rate_at, rate_index and rdiv, and the
wir1_arith module, are test-only (legacy_int; and cfg(kani), for the
harnesses that still prove them); rate_len, the rate predictor's geometry,
stays. wai-verify declares legacy_int.
- The predictors' proofs move to the operators a decode runs: wai-ops'
e11_up2_between_its_neighbours, e12_rdiv_matches_its_definition and
e12_rate_at_reads_only_source_samples, in the stage shard.
Gate 6's results, for the record (the switch at 9a377f9b): gate.sh GREEN;
the release fast-kernel step; staged_verify.py and int_payload_verify.py;
wai-web native 32 and wasm32, verify_int_payload_wasm and verify_staged_wasm
(69 of 69 cases, 146 unit stage hashes equal the native ones); include/wai.h
unchanged. Falsified with the switch live: E10's half-pel rounding without
its +1 and E12's rdiv halves toward zero turn the file-based goldens red
(byte-exact wiv1_keyframe_0_payloads_are_byte_identical, video_real frame 2;
int_video_real_footage_exercises_the_half_pel_predictor;
staged_audio_rate_ladder_is_byte_exact; wai-rs int_video_halfpel), and the
corpora (wai_int_payload_vectors verify, FAIL video_real; wai_staged_vectors
verify, the encoder's reconstruction differs from the decode); the Python
verifiers stay green. The decode cloning the previous frame for E10 turns
int_payload_cost red: int_video held 42524 bytes against 35612 declared.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
44 lines
1.8 KiB
TOML
44 lines
1.8 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"]
|
|
# 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"]
|