wai: the record made true #201

Merged

dcharlot merged 17 commits from wai/d1-record-true into main 2026-10-11 16:58:41 -04:00

Conversation 0 Commits 17 Files changed 37 +941 -88

2026-10-11

Transaction Science

Merge origin/main (#215, #216, #217) into wai/d1-record-true ...

CHANGELOG: both v0.4.0 entries kept; this branch's entry stays on top, as it
lands after main's vector-graphics entry. README merged without conflict.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

8885e66688

• View at this point in history

2026-10-11 08:35:27 -04:00

Transaction Science

wai-conformance: build wai as one codegen unit for the wasip2 quantum leg ...

The wasip2 leg's `cargo build --bin wai_quantum_vectors` also links wai's
cdylib, and rust-lld 22 (Rust 1.98) segfaults linking it on #201's tree. The
crash is LLD 22's ElemSection::writeBody dereferencing a null indirect function
table: the linker keeps the flags of the first object that names
__indirect_function_table, and on this tree that object (a codegen unit holding
io::Error::is_interrupted, which the new capped manifest writer instantiates)
names it without NO_STRIP. The table is then no GC root, nothing the cdylib keeps
(only cabi_realloc is exported) calls through it, yet live function addresses
still fill the element segment. LLD 23 ORs NO_STRIP across references and links
the same inputs.

Which object comes first follows the codegen units' hashed names, which depend on
the code and the checkout path, so the crash comes and goes with unrelated
changes. With one unit, wai's object comes first and takes function addresses, so
it names the table with NO_STRIP. Measured on 603c6bbb at the CI path in an x86_64
Ubuntu 22.04 container: the step crashes as is and links with this setting.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

1f48766531

• View at this point in history

2026-10-11 08:34:57 -04:00

Transaction Science

wai-web reach: the record leg runs the record's own demo scripts ...

The record leg holds the package of record (reach/record/, built from the
commit reach/manifest.json names) to the demo verify scripts. It ran this
tree's scripts, so a check added after the record's commit was run against
code that predates it: #201's verify_pack test of the writers' manifest
limit failed on every rung of the record leg (jobs 21114, 21188), because
the recorded wai_web_bg.wasm was built before the writers refused a
manifest past 2^27.

run-modern.mjs takes --demo-commit <commit>: step 3 then runs that commit's
demo scripts over that commit's corpora (its wai/, exported with git
archive). A script this tree runs that the commit lacks is reported as
SKIP, not as a pass; a commit with none of them fails the run, as does an
empty or unknown commit. The record leg fetches input.commit (the checkout
is shallow) and passes it. The tree leg is unchanged: this tree's scripts
against this tree's build, where the new verify_pack check runs and passes.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

603c6bbb8c

• View at this point in history

2026-10-11 03:44:06 -04:00

2026-10-10

Transaction Science

Merge wai/reach-builds (with #197 and main) into wai/d1-record-true ...

Brings in #205 and #197 and, through them, main as of #200 and #206.

- wai/extensions/quantum-sim.md: both sides rewrote the status line's
  reference implementation. Kept main's two capabilities (circuit2 WQC2,
  circuit WQC1 frozen) and this branch's wording of where the reference
  lives (the `quantum` feature of wai-quantum, forwarded by wai-rs).
- wai/http-conformance/falsify/run.sh: #200 rewrote the single-run script
  into shards; took the sharded runner unchanged and ported this branch's
  additions into it: manifest-limit-dropped.patch sits with the other
  patches with its must-fail cases on its first line (it applies to the
  merged head.rs unchanged), and the Python mutation manifest-limit-dropped
  is declared in falsify/mutations.txt, after reload-walked where the old
  list had it, with the cases it must fail:
  head_malformed_manifest_too_large_O5 and _OD. The 3/3 shards cover
  134 patches and 78 mutations, each once.
- wai/http-conformance/cases.json: regenerated with wai_http_vectors gen;
  the generator's output equals the merged text (1049 cases), and both
  wai_http_vectors verify and http_verify.py give every outcome.
- wai/CHANGELOG.md: no textual conflict, but git left this branch's entry
  below "Staged measurement"; moved "The record made true" to the top of
  v0.4.0, newest first, above #205's and #197's entries.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

4e7155b955

• View at this point in history

2026-10-10 17:35:03 -04:00

2026-10-09

Transaction Science

wai: SECURITY.md, SPEC §2 and §6.5 say what holds ...

SECURITY.md:
- "Allocation follows the input" was false for the manifest. The reference
  readers parse it into serde_json::Value; measured on the release build,
  a 94 MB prev of 2^20 runs peaks at about 7 times its length and a
  134,217,000-byte array of zeros at about 38 times (5.1 GB RSS, 7.6 s in
  from_bytes, which returned Ok). The text now says so, and the argument
  that a sink short of that memory could not decode such layers either is
  gone.
- CI does link ONNX Runtime and libzstd: wai-neural-gates.yml and
  wai-neural-e2e.yml build `neural`. No workflow builds `codecs`.
- No Kani harness is in int_kernels.rs; the harnesses are in rans.rs,
  int_entropy.rs, int_transform.rs, wai_video_policy.rs, staged/predict.rs
  and staged/wir1_arith.rs. Its SIMD kernels, the only unsafe outside the
  C ABI, are held to the scalar kernels by equality tests, not by a model
  checker.
- The bare "(§5.1)" names http-delivery; the writer test is described as
  it now runs; the Python verifiers' checks are described as they now run.

SPEC §2: the 2^20-unit cap is staged-delivery Appendix A.3's (section 3
bounds a count only by 32 bits); the limit bounds what a reader reads, not
the memory its parse takes; the paragraph is reflowed.

SPEC §6.5: Lane A's records are "among them", and include wai.video.ssai
and wai.video.channel. Lane B no longer says every record applies:
staged-measurement counts no encrypted object, and a verifier without the
key checks no payload-dependent rule of a reconstruct-session claim
(jwp-receipts §2.4.12 rule 3); nothing in the reference states a Lane B
tier. The confidentiality header and the CHANGELOG say the same.

SPEC §5 and determinism-tiers §5: only `photo` comes from a trained model;
gradient, bloom, facade and the cross-architecture golden use seeded
integer weights, as the CHANGELOG said both texts did.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

59ab0d9489

• View at this point in history

2026-10-09 17:16:04 -04:00

Transaction Science

check-wai-section-refs: read wai/SECURITY.md too ...

SECURITY.md cites sections of SPEC, http-delivery, integer-payloads and
jwp-receipts, and nothing checked them: the checker read only SPEC.md and
extensions/*.md, and the workflow's paths left SECURITY.md out. It reads
SECURITY.md now, and the workflow runs when it changes. Every reference in
it resolves; a reference to http-delivery §66 put in by hand fails the
check. CHANGELOG.md stays out: it is a dated record whose older references
are kept as written.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

ddd49ee03d

• View at this point in history

2026-10-09 17:15:06 -04:00

Transaction Science

wai-web: pack and packMulti refuse a payload past its u32 field ...

SECURITY.md and the CHANGELOG named wai-web's writers among those that
refuse a payload whose length does not fit its u32 field, but they still
wrote `payload.len() as u32` and `p.len() as u32`; packMulti's checked_add
caught only a total that overflows, and the claim held only because usize
is 32 bits on wasm32. Both now convert with u32::try_from, as wai-rs's
writers do, and name the payload that does not fit.

verify_pack.mjs: the refused manifest is 2^27 + 1 bytes, one past the
limit; the comment read as if it were 2^27.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

2e398cde86

• View at this point in history

2026-10-09 17:14:52 -04:00

Transaction Science

wai: the Python verifiers check their manifest reader limit in memory ...

In staged_verify, claim_verify and pack_verify the man_len check is
outcome-neutral for any input under 128 MiB: the bounds check after it
refuses the same bytes. No corpus file is that large, so nothing exercised
it. Each verifier now builds, in memory, a WAI1 and a WAI2 (claim_verify:
the WAI2 its wai2_read reads) whose manifest is padded to 2^27 + 1 bytes
by a member no revision defines, and requires it refused, and requires the
same envelope with a 300-byte manifest read, so only the limit tells the
two apart. pack_verify builds its own envelopes, as it shares no code.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

55df2cdc2c

• View at this point in history

2026-10-09 17:03:13 -04:00

Transaction Science

wai: the HTTP corpus holds the manifest reader limit at its edge ...

No case reached the new limit: with the check deleted from
http_verify.parse_head, every case still gave its outcome, and no committed
envelope declares a man_len past 2^27. Four parse_head cases now do, on a
WAI1 (O5) and a WAI2 (OD): eight bytes declaring 2^27 + 1 are refused
(head_malformed), and eight declaring 2^27 ask for the head they declare
(need 134217740 and 134217738). Both implementations give all four.

falsify/manifest-limit-dropped.patch drops the check from head::parse_head,
and http_verify.py --mutate manifest-limit-dropped drops it on the Python
side; run.sh runs both.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

010ee79b28

• View at this point in history

2026-10-09 16:56:04 -04:00

Transaction Science

wai-rs: test the writers' limits through the writers ...

The test named for the writers called manifest_json_within and u32_field
directly and never called Wai::to_bytes or WaiMulti::to_bytes, so putting
serde_json::to_vec and `as u32` back in both writers left every test green.
Both writers now run to_bytes_within(WriteLimits), and to_bytes passes
SPEC's limits. The test writes each envelope at limits equal to its
manifest's and payloads' lengths, and requires manifest_too_large one byte
below the manifest, the field error one byte below a payload, and the sum
error when two payloads each fit and their total does not.

MANIFEST_MAX_LEN's doc cites staged-delivery Appendix A.3 for the 2^20-unit
cap (section 3 bounds a count only by 32 bits), and says the limit bounds
the bytes read, not the memory a parse takes. wai.h regenerated.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

4961fccf1e

• View at this point in history

2026-10-09 16:46:13 -04:00

Transaction Science

wai: the manifest reader limit is 2^27, the largest manifest a staged layer has ...

The gate falsified the 1 MiB limit: `tests/staged_resources.rs` offers layers over
up to 65 536 units whose `refines.prev` names a different producer for each unit,
and the writer refused its 1.47 MB manifest. staged-delivery §3 permits that: a
`WIR1` layer covers up to 2^20 units, and a `prev` with one run per unit is about
90 bytes a run, some 94 MB in all. A reader floor below that would let a sink
refuse layers the extension allows.

`MANIFEST_MAX_LEN` is now 2^27 (134 217 728 bytes), which holds that layer, and SPEC
§2 states why. The Python verifiers use the same bound.

The writers now serialise through a capped writer that stops as soon as the
manifest passes the limit, so a refused manifest is never built in full. Serialising
128 MiB takes a debug build about 17 s, so the tests check the writers' cap at a
small limit, and the readers' boundary from the length field: at the limit a reader
refuses eight bytes only as truncated, one past it as too large. A 2 MiB manifest,
past the old bound, round-trips byte for byte. `verify_pack.mjs` checks a 3 MiB
manifest written and one byte past 2^27 refused by the browser writers.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

07e923c724

• View at this point in history

2026-10-09 13:52:19 -04:00

Transaction Science

wai: CHANGELOG for the record made true ...

Co-Authored-By: Claude Opus 5.5 <[email protected]>

b0bdea2949

• View at this point in history

2026-10-09 13:05:39 -04:00

Transaction Science

wai: SECURITY.md, and SPEC §2's reader limits stated as rules ...

`wai/SECURITY.md` is engineering notes, not normative text:

- how to report a vulnerability: [email protected], the address the
  repository's sandbox standard already gives, and what to send;
- manifest parsing: every bound the readers apply, with where it is specified and
  which tests check it, including the Python verifiers' share of them;
- the native codec libraries behind the `codecs` and `neural` features, that they run
  in-process with no sandbox, what does not touch them, and two gaps stated as gaps:
  `wai.text.zstd` and `wai.text.xz` decompress without an output bound, and the
  random-input smoke test is in no CI workflow;
- module authorisation (SPEC §4, jwp-receipts §7.9) and what it does not yet cover:
  the environment a module runs in;
- the fingerprinting risk of `held_sets`, pointing at the privacy rules still to be
  written for http-delivery.

SPEC §2 gains *Reader limits*: no reader refuses a manifest for its size or nesting
within 1 MiB and 127 levels, any reader may refuse one past them, and a refusal for
length comes from `man_len` alone (`manifest_too_large`). The container layout does
not change. http-delivery §7 step 3 and the WAI2 packer rule point at it.

`verify_pack.mjs`, which the wasm job runs, now checks that `pack` and `packMulti`
write a manifest of exactly 1 MiB and refuse one byte more; it passes against a
release wasm32 build of this source. That build also validates with WebAssembly's
SIMD and relaxed-SIMD features disabled (a control with bulk memory disabled fails),
which determinism-tiers §5 now records in place of a claim about build flags.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

6c3abb1530

• View at this point in history

2026-10-09 13:01:30 -04:00

Transaction Science

wai: the Python verifiers apply the same manifest reader limit as wai-rs ...

The stdlib verifiers already copy the reference reader's nesting limit, so that two
readers agree on an envelope. They now copy its length limit too:
`staged_verify.MANIFEST_MAX` (1 MiB) is refused by `read_wai1` and `read_wai2`, by
`claim_verify.wai2_read`, by `pack_verify.read_envelope`, and by
`http_verify.parse_head` as `head_malformed` before it asks for the head.

Checked: every changed verifier passes its corpus as CI runs it (pack, staged,
http, staged-measure, claim). A manifest of exactly 1 MiB is read by each reader
and one byte more refused, as wai-rs does. On main, `read_wai1` read the longer one
and `parse_head` answered eight bytes declaring u32::MAX by asking for 4 GiB.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

027dca6dc5

• View at this point in history

2026-10-09 12:41:10 -04:00

Transaction Science

wai: a reader need hold no manifest past 1 MiB, and the writers never write one ...

`man_len` is a u32, and nothing bounded it: a reader trusted it up to the bytes in
hand, and the HTTP head parser answered a `man_len` of 4 GiB by asking for
4 GiB + 12 bytes. The reference now sets a reader limit:

- `container::MANIFEST_MAX_LEN` is 1 MiB (1 048 576 bytes), far above any manifest in
  the committed corpora. `check_manifest_len` refuses a longer one with
  `manifest_too_large`, from the length field alone, before anything is sliced.
- Both readers (`Wai::from_bytes`, `WaiMulti::from_bytes`), `manifest_bytes` and
  `http_binding::head::parse_head` (as `head_malformed`) apply it.
- Both writers, and the browser crate's `pack` and `packMulti`, refuse to write a
  manifest past it, so the reference never emits what its reader refuses.
- The writers also refuse a payload whose length does not fit its u32 field;
  `Wai::to_bytes` and `WaiMulti::to_bytes` wrote such a length modulo 2^32.
- `include/wai.h` gains the constant, as cbindgen writes it.

Tests: at the limit both containers read and write back byte for byte; one byte
past it, or a declared u32::MAX, is refused by every reader from the first eight
bytes, and neither writer writes it; the head parser refuses it instead of asking
for it. The manifest's nesting limit, which the JSON reader already applied, is
now pinned: 127 levels read, 128 refused, in WAI1 and WAI2 manifests.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

30a15bad94

• View at this point in history

2026-10-09 12:23:05 -04:00

Transaction Science

wai: SPEC §6.5, protected content in two lanes, and where the exact tier holds ...

A new normative section names the two lanes protected content travels in, and
what a WAI record covers in each.

- Lane A, hardware-protected content: a standard codec decrypted and decoded inside
  the platform's protected media path. This revision registers no
  `security.encryption` value for it, so no WAI envelope carries Lane A media. WAI's
  records about such a title (the served manifest, the package's segment map, the
  key-release decisions, the content hashes of WAI objects) are all it attests; none
  covers a decoded frame. Parametric synthesis applies only inside a decoder the
  protection system certifies, with no tier and no output digest.
- Lane B, end-to-end encryption at the application layer (`mls-sframe`): the
  application decrypts and any decoder runs, so every record and tier applies as to
  plaintext. It is stated not to be a protected-path robustness level: a publisher
  must not offer it for a licence term that requires one.
- The exact tier covers only output a sink can hash. determinism-tiers §5 gains a
  subsection listing the fabrics `decode-equivalence` is shown on in this revision
  (native CPU; wasm32, whose CI job passed on main at 412a08c5), none on GPU or NPU,
  forbids relaxed-SIMD instructions and NaN-bit dependence in a Wasm decoder at the
  tier, and rules out any tier, digest or binding for protected-path output.

The `wai.video.keys` row and the confidentiality extension now say which lane they
belong to.

Two more stale references: README and SPEC Appendix A sent macOS builders to a
committed `.cargo/config.toml` that no longer exists; `wai-rs/build.rs` finds libFLAC
through pkg-config, then the Homebrew prefix.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

ce4646278f

• View at this point in history

2026-10-09 12:05:30 -04:00

Transaction Science

wai: int_synth's weights are quantised after float training, and two engine paths moved ...

SPEC §5 and determinism-tiers §5 said `wai.neural.int_synth` decodes "QAT
weights". No committed model was trained that way. The trained corpus vector was
made by `tools/wai_int_synth_real.py`: float training, then post-training
quantisation with each layer's shift derived from its measured activation range,
the recipe `tools/wai_int_synth_train.py` documents. The synthetic vectors' weights
are generated from a seed. Both texts, the capability constant's comment, the
module doc and a test comment now say that.

`tools/wai_int_synth_qat.py` said it "closes the one open gap" and tunes "the
weights AND the shifts"; it trains the weights against one fixed shift and made no
committed model, and it now says so. `tools/wai_int_synth_export.py` told users to
train with QAT upstream; it now names the working path.

Stale paths: the int_synth decoder is `int_synth.rs` at the crate root, not
`neural/int_synth.rs` (SPEC §5, the export tool, the capability comment); the
quantum-ops engine is `wai-quantum/src/quantum_ops.rs`, and the quantum-sim
receipt's feature is `quantum_receipt` of `wai-quantum`, which `wai-rs` forwards,
not `["quantum", "world"]`.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

08b1568291

• View at this point in history

2026-10-09 11:55:53 -04:00