wai-rs: fast integer decode kernels that give the same integer for every output #108
Loading…
Reference in a new issue
No description provided.
Delete branch "wai/land-07-int-decode-kernels"
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
The integer decoders ran scalar single-threaded loops with no throughput figure. src/int_kernels.rs adds fast convolution, transposed-convolution, matmul and elementwise kernels that give the same integer as the reference for every output element (threads via std:🧵:scope; none on wasm32); operands outside the no-overflow bound go to the reference. research/decode-throughput.md records measured figures, machine and method. Added in this chain: int_kernels is on the JPEG AI decode path, so it now also denies the math-library clippy guard.
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 kani: 12/12; the fast-kernel equivalence suites in dev and release profiles (every committed integer vector under every policy, plus edge geometry): all passed; the JPEG AI pinned-output test still matches bit for bit with the parallel kernels (1/1, decode 5.4 s → 0.8 s in that test); symbol guard and clippy clean; the neural gates: 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: wai/land-06-ci-headline-tests.
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 hadSPEC §5 registers the elementary video and audio bitstreams that distribution chains carry, as sink-supplied capabilities: wai.video.{av2,vvc,hevc,avc,vp9,evc,evc.baseline,avs3,lcevc} and wai.audio.{aac,mpegh,avs3}. Each carries a licence class (royalty-free, or flagged SEP-pool/proprietary), and no flagged codec can become a default. - Every capability now has an explicit replicate class, and an "exact" class is given only where a recorded basis supports it: a standard that requires bit-exact decoder output, or a measured comparison. Elsewhere the class is conservative, and the registry says what evidence would raise it. wai.mesh.glb is not cross-decoder-exact, because a GLB can embed coded textures and compressed geometry. wai.audio.scene answers "not known" until its sources are known (is_cross_decoder_exact_with_sources). - wai.video.lcevc is an enhancement layer, pinned to the ISO/IEC 23094-2 Annex B byte stream and carried as a companion bound to a base payload (SPEC §7.1). Its list of base codecs is WAI's registration, not a limit imposed by that standard. - The companion rules are enforced: a WAI2 companion must be companion-only and must bind to a base it applies to (an HDR descriptor to a video payload, LCEVC to its registered bases), with negative tests. SPEC §7.1 lists the envelopes this makes non-conforming. - A companion-only fallback closes dispatch at step 5, not step 3, so decode and inspect agree (SPEC §4). - SPEC §8 states what a new registration does to earlier uses of its string, and what a MINOR revision may enforce. - research/media-codec-registry.md records the licence and replicate basis for each entry. Co-Authored-By: Claude Opus 5.5 <[email protected]>