wai: state what each determinism tier guarantees, and make replicate mean it #103
Loading…
Reference in a new issue
No description provided.
Delete branch "wai/land-02-determinism-tiers"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
What this adds
SPEC §7 required an integer decode for
replicatein one paragraph and accepted entropy-consistency in another. Resolved: over a neural capabilityreplicatepromises decode-equivalence; over a standard codec it promises that standard's decoder conformance, stated per registry class (newStandardTolerance,StandardUnclassified).wai.image.jpegaimoves to the newNeuralEntropyExactclass and no longer backsreplicate— recorded as a conservative choice pending a reading of ISO/IEC 6048-4. The JPEG AI decoders refuse codestreams outside the configuration they implement instead of decoding them wrongly;wai wrapwritesreplicateonly where a sink accepts it unpinned; extensions/determinism-tiers.md gains an evidence table saying what ran where, including what has not. A neural-gates workflow runs the model-free refusal tests in an Ubuntu 24.04 image.Verification
Gate run locally on macOS arm64 (rustc 1.98.0) against this link's own tree: wai-rs build and lib tests with the wai-conformance feature list, the carriage test, all 12 conformance corpora (worlds, audio, haptics, feeds, avatars, volumetric, score, int-synth, film, quantum, quantum-ops, OER), byte-exact-conformance (release) and a wasm32-unknown-unknown check of wai-web;
cargo kaniin wai-verify: 12/12 harnesses verified; the neural gates (--features neural, the two named tests): 2 passed..Merge order. This is one link of a linear chain: each branch contains the one before it, so merging the PRs in order into main never conflicts. Merge after: #82 (feat/wai-video-workflow).
Not covered. Windows (its runner has been offline since late August) and Linux x86_64 hardware were not run locally; the forge's CI on this PR is the check for those legs.
🤖 Generated with Claude Code
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]>Fixes the defects reported in the previous commit, and proves both halves: the verifier now discharges the bypass harness, and the conformance vectors still decode byte-identically. The defects shared one root cause: in the bypass escape, the run length and the shift distance are read FROM THE STREAM, so a malformed bitstream drove them out of range. Each fix is a no-op on a well-formed stream, because a conforming encoder never emits the values that trigger them: - shift overflow (rans.rs:77). raw_val is 32 bits and each group carries 4, so at most 8 groups can contribute. n_bypass is now clamped to that. A shift of 32+ on a u32 panics in debug and masks in release — the same bytes decoding two ways depending on how the sink was compiled, which is precisely the byte-exactness claim failing. - add overflow on `value += max_value` and on `value + offset` — now saturating. - slice OOB in renorm(): reads past the buffer on an exhausted stream. Now guarded, setting an `exhausted` flag (exposed as is_exhausted()) instead of panicking a sink that was handed untrusted bytes. - unbounded `while val == MAX_BYPASS_VAL`: stream-controlled, so it need not terminate. Now bounded by the same 8-group limit and by `exhausted`. Also made decode() total for a malformed CDF argument (cdf_len < 2 would underflow `cdf_len - 1`; cdf_len > cdf.len() would index out of bounds) — a caller-contract violation a conforming codec never produces. VERIFIED BOTH WAYS: - Kani: 4 harnesses, 601 checks, 0 failures — including kani_decode_bypass_escape_is_total, which failed before this commit. - Behaviour preserved: byte-exact-conformance + wai-rs neural_int (the rANS round-trip) = 139 tests, 0 failures. The fix changes nothing a conforming encoder can produce. Scope, stated honestly: these are bounded proofs (3-symbol CDF with symbolic interior, 16- and 64-byte streams, unwind 8/20), not unbounded ones, and they cover the stream-controlled paths. decode_categorical's CDF argument is still assumed well-formed — it comes from internal tables, not the wire. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>Extends the machine-checked half to the primitive SPEC §7 names as the replicate-soundness hinge: a bucket that flips selects a different CDF and desyncs the rest of the stream. Proved for det_build_index: - the returned index always addresses a real scale-table entry; - the bucketing is MONOTONE in sigma — a larger sigma never selects a smaller bucket. The doc comment claimed this ("index rises with sigma"); it is now a theorem. It is proved for an ARBITRARY edge table rather than only an ascending one, because the property follows from counting rather than from sortedness — so it does not rest on a precondition a caller might not maintain. A non-monotone bucketing would mis-order the table without ever panicking, which round-trip tests on well-formed vectors would not reliably surface. - the singleton table degenerates correctly to one bucket. Suite now 7 harnesses / 895 checks, 0 failures. CI watches int_entropy.rs so a change there cannot regress the property and merge green. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>Extends the machine-checked half to the integer transformer kernels on the JPEG-AI path — the largest remaining arithmetic surface. PROVED for softmax: - total over the whole fixed-point path: the ln2 reduction, the i128 polynomial multiplies, the shift by q, and the division; - the output sums to EXACTLY 2^PROB_FRAC, with no negative probability. The function asserted this in a comment ("give the whole remainder to the largest element so the distribution sums to EXACTLY 2^PROB_FRAC"); it is now a theorem. It is load-bearing: these probabilities become a CDF, and a denormalised CDF makes the entropy decode select the wrong interval and desync the stream. EXPOSED — the `sum == 0` uniform fallback would BREAK that invariant if it ever fired: n * ((1<<PROB_FRAC)/n) equals 1<<PROB_FRAC only when n divides it (n = 3 gives 65_535, not 65_536). The checker marks the branch UNREACHABLE (the argmax element always has neg = 0, so exps[argmax] = c0 > 0 and sum > 0), so the invariant holds today — but by unreachability, not by construction. Recorded at the site: any change to the exp reduction that lets it fire must distribute the remainder the way the tail of the function does. No behaviour change here; this is the class of defect that panics nothing and fails no well-formed test. Honest scope: the normalisation proof is the two-logit case over ±2^20. Three symbolic logits over ±2^40 did not close in twenty minutes of propositional reduction — each element costs an i128 polynomial and an i128 division. The arity and bound are written into the harness doc rather than quietly tuned until something passed, and the solver (kissat) is pinned on the harness so CI reproduces the result without a flag. Suite now 9 harnesses / 2285 checks, 0 failures, across rans + int_entropy + int_transform. CI watches all three sources. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>Extends the machine-checked half across the remaining reachable kernels, and — more usefully — writes down the coverage boundary instead of listing only wins. PROVED (conditional results, stated as such): - matmul: the accumulation is total for fixed-point operands within ±2^31 at Q16. This is NOT "matmul is safe": the product is formed in i128, truncated to i64, then accumulated with a plain `+=`, which genuinely does overflow for large enough operands. Nothing in the signature constrains magnitude, so every caller inherited that safe-operating range silently. The harness turns an unstated contract into a written, checked precondition — it is not filed as a defect, because it is not one. - layernorm: total at ±2^10 — BELOW realistic Q16 activation magnitude. At ±2^20 the instance did not close in 25 minutes. The guarded divide (`.max(1)` on both radicand and root) and the surrounding arithmetic hold for small operands; this does not establish the kernel over its working range and the harness doc says so. The obstacle is `isqrt` over a symbolic u128 — a limit of bounded model checking, not a property of the code. SPEC §7 now records the boundary: layernorm's bound is below working range, and attention, linear, igdn and the composed TransformerBlock are NOT COVERED AT ALL. A verification section that enumerates only successes invites the wrong inference — that the integer core is proved, full stop. What is true is narrower: four kernels carry machine-checked properties, one only at toy magnitudes, and the largest composed pieces are untouched. Suite: 11 harnesses / 3447 checks / 0 failures, whole run comfortably inside the per-harness cap, so it is viable as a merge gate. CI already watches all three verified sources. Co-Authored-By: Claude Opus 5 <[email protected]>Splits the pure decision policy out of the signing layer (new wai_video_policy.rs: AdCandidate, Impression, decide, billable_spend), leaving wai_video_ssai to own the blake3/Ed25519 receipt and re-export the types so the public surface is unchanged. Behaviour-preserving: all 25 OTT tests pass, including the three that cross the new boundary. WHY THE REFACTOR, rather than the cheaper route. The OTT modules import ed25519_dalek, GrantRef and merkle_root, whose chain runs down into world::{op, replay}. Kani could stub that away — decide() never touches it, so a proof would arguably still be sound. But that is the "stand-in closing a goal nothing decided" pattern this codebase has already been bitten by three times, and getting it wrong is silent. Separating pure policy from the signing layer costs a refactor and buys a proof with no stand-ins near it. It is also the same shape that makes byte-exact-conformance possible. PROVED: a fresh decision bills nothing until its beacons arrive (1602 checks), so a fill can never be mistaken for delivery. NOT PROVED, and recorded in the source rather than quietly dropped: that decide never proposes a fill exceeding the funds, the avail duration or the slot count. Three configurations, none closed — 3 candidates, all symbolic ................ timed out 600s 2 candidates, all symbolic ................ timed out 900s 2 candidates, durations concrete .......... timed out 600s The cost is not the budget arithmetic, which is trivial: decide sorts by `ad_id: String`, so the model carries memcmp plus the Vec/raw_vec/Layout machinery. The plumbing explodes, not the logic. The harness was REMOVED rather than shrunk to a one-candidate pod, which would pass while establishing nothing — no tie-break, no slot contention, a degenerate case dressed as a theorem. So SPEC §7 now states the ssai decision policy is TEST-BACKED, NOT PROOF-BACKED (wai_video_ssai::tests::overspend_cannot_be_signed covers it concretely), and names the real paths forward: a decision that does not sort on a heap-allocated key, or a deductive verifier (Creusot/Verus) rather than a bounded model checker. Suite: 12 harnesses / 5049 checks / 0 failures. CI watches wai_video_policy.rs. Co-Authored-By: Claude Opus 5 <[email protected]>worlddependency video_manifest always had