b3056eb4c6
WAI's contract is that an integer decode is byte-identical on every machine.
byte-exact-conformance establishes that by SAMPLING: fixed vectors on four real
targets. This adds the complementary half — REASONING over all inputs in a
bounded window — using Kani (CBMC) against the same sources.
New crate `wai-verify`: a minimal host that #[path]-includes wai-rs/src/rans.rs
(single source of truth, no copy), mirroring byte-exact-conformance. It carries
no `rust-version` on purpose — the verifier ships its own pinned nightly and an
MSRV above it makes cargo refuse to build the harnesses. Harnesses live beside
the code they verify, behind #[cfg(kani)].
PROVED (3 harnesses, 353 checks, 0 failures):
- RansDecoder::new is total for every input slice.
- decode_categorical is total and returns an in-alphabet symbol, for ALL
16-byte streams and ALL well-formed 3-symbol CDFs — with and without the
rANS state invariant.
A hypothesis was REFUTED in the process: I expected `freq * (state >> 16)` to
overflow on an arbitrary stream. It cannot. freq <= 2^16 (the CDF is normalised
to 2^PRECISION) and state>>16 <= 2^48-1, so the product is at most 2^64 - 2^16.
The safety comes from CDF normalisation, not from the state invariant — a
stronger result than the one I set out to prove.
Non-vacuity is mechanical, not argued: each decode harness carries a
kani::cover obligation, discharged only if the decode is actually reachable, so
an over-strong assumption cannot masquerade as a proof. (A deliberately-false
sentinel was run once and failed as required, confirming the checks discriminate
before the cover mechanism replaced it.)
FOUND — the bypass escape in decode() is NOT total. Harness
kani_decode_bypass_escape_is_total fails, and the failures are the finding:
- rans.rs:77 shift left with overflow: n_bypass is stream-controlled, so
j*BYPASS_PRECISION reaches 32 on a u32. Panics in debug, masks in release —
the same bitstream decoding two ways depending on build profile.
- rans.rs:81 add with overflow on `value += max_value`.
- renorm slice OOB panic reading words[off..off+4] past the buffer.
- rans.rs:70 unwinding assertion: the `while val == MAX_BYPASS_VAL` loop is
stream-controlled and unbounded.
All four are reachable from a malformed or adversarial bitstream and none are
visible to a conformance matrix that only decodes well-formed vectors. Left
unfixed in this commit so the proof and the defect land together; the fix must
be a no-op on well-formed streams and is verified against the conformance
vectors separately.
Also: wai-rs/Cargo.toml had two multi-line inline tables, which are invalid per
TOML 1.0 (inline tables must be single-line). Cargo tolerates them; the
verifier's stricter parser refuses. Joined onto single lines — semantically
identical, `cargo metadata` unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
7 lines
154 B
TOML
7 lines
154 B
TOML
# This file is automatically @generated by Cargo.
|
|
# It is not intended for manual editing.
|
|
version = 4
|
|
|
|
[[package]]
|
|
name = "wai-verify"
|
|
version = "0.1.0"
|