wai: the deterministic module profile's two checkers, a Rust one and a dependency-free one, held to each other #647
2026-11-05
changelog: name §9.1's two new planted modules
Some checks failed
wai-ops integer operators / does this change touch it (pull_request) Successful in 8s
WAI conformance / fast integer kernels, every x86_64 kernel set (AVX-512 silicon) (pull_request) Failing after 0s
WAI breaking changes and the conformance runner / WAI breaking · wire, record and API against main · linux (pull_request) Successful in 40s
WAI conformance / faces from keypoints under wasm32-wasip2 (wasmtime) (pull_request) Successful in 2m1s
WAI breaking changes and the conformance runner / WAI breaking and conform · their tests, and the independent verifiers through wai conform · linux (pull_request) Successful in 2m45s
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 38s
wai-ops integer operators / wasm32 under Node (pull_request) Successful in 24s
wai-ops integer operators / wasm32-wasip2 (wasmtime) (pull_request) Successful in 1m3s
wai-ops integer operators / linux-x86_64 (pull_request) Successful in 1m7s
wai-ops integer operators / independent checker (Python) (pull_request) Successful in 15s
WAI conformance / quantum core and corpus under wasm32-wasip2 (wasmtime) (pull_request) Successful in 4m0s
WAI energy receipts / energy receipts · linux (pull_request) Successful in 12m57s
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 19m26s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 1m29s
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 23s
WAI conformance / codec wrappers · fuzz smoke, text decode limits, C entry points, provenance, the semantic path (pull_request) Successful in 1m4s
wai-ops integer operators / macos-arm64 (pull_request) Successful in 1m0s
standards workspaces build + test / macOS energy backends (pull_request) Successful in 9m41s
WAI energy receipts / energy receipts · macos (pull_request) Successful in 10m12s
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 14m32s
WAI conformance / v2 vocabulary · manifests validate as stated (pull_request) Successful in 22s
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Successful in 6m14s
WAI conformance / delivery telemetry · CMCD and CMSD against an independent library (pull_request) Successful in 15s
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 31s
WAI conformance / C2PA manifest emission · signed, read back, validated (pull_request) Successful in 1m56s
WAI conformance / each feature of the independent verifiers' steps compiles alone (pull_request) Successful in 12m22s
wai-ops integer operators / linux-aarch64 (pull_request) Successful in 1m16s
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 24m41s
WAI energy receipts / energy receipts · linux-arm64 (pull_request) Successful in 12m44s
WAI conformance / independent verifiers · claims, JWP, key discovery and integer payloads (Python) (pull_request) Successful in 1h11m23s
Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-module-check: plant float-block-type and float-select-type
The two rows §9.1 now holds for R3's block types and typed selects, built as their rows say, each verdict's offset the value type marked while building. Co-Authored-By: Claude Opus 5.5 <[email protected]>
deterministic-modules: two planted modules for R3's block types and typed selects
§4.1 says an instruction whose types a block type or a typed select fixes breaks R3 only through that value type, which follows its opcode. No module of §9.1 held a checker to it: with the block type's item left out of a checker, every planted verdict stayed the same. float-block-type (a block of result f32 that holds only unreachable) and float-select-type (a typed select of f32 where the stack is polymorphic) are refused at that value type, at the integer level. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-conformance: run the deterministic module profile's checkers, and its changelog entry
A verifier step of its own (.github/wai-conformance/verifiers/module-check.sh) rebuilds the planted corpus and checks it is what build.py writes, runs the Rust checker's tests and both checkers on the corpus and on the validation limits' corpus, which it generates, then runs the differential on the committed seed. The step's paths name the crate's directory, which is under none of the workflow's trigger paths, so the trigger gains that one line. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-module-check: mutated copies in the differential, and the specification's tests
wasm-smith writes valid modules, or ones invalid only as it is told to be, so the differential tested how the two validators accept far more than how they refuse: with check-module.mjs changed to accept an untyped select of references, or to read an uninitialised local, the 10,000 modules still all agreed. The differential now also writes two mutated copies of each module, one or two bytes changed (a byte replaced, inserted or removed anywhere after the preamble, or a code-section byte replaced by a one-byte opcode), most of them outside R2. On the committed seed the checkers agree on all 60,000 verdicts of its 30,000 modules, and it catches a changed section order, an unchecked if without else or an unchecked alignment. examples/spectest.rs writes every module the specification's test scripts define, assert invalid or assert malformed, with the Rust checker's verdicts, for differential.mjs. On the scripts of the specification build of 2026-11-04 (commit 859d3232a55c, test/core, 259 scripts, one of which the text parser of this release does not read) it writes 5,712 modules: the Rust checker refuses every invalid and malformed one by R2 and no valid one, and the two checkers agree on all 11,424 verdicts. With check-module.mjs changed in any of ten ways a validator can go wrong (a select of references, an uninitialised local, a u32's unused bits, br_if's pushed types, duplicate exports, a custom section's name, a final supertype, a field's mutability in subtyping, catch labels, undeclared function references), they disagree. Its scripts are not in this repository, so it is run by hand on a copy of them. Co-Authored-By: Claude Opus 5.5 <[email protected]>
deterministic-modules: drop the import and export counts from the validation limits
Every import and every export adds at least 1 to the interface limit's sum, so that limit already holds a module to 999,998 imports and exports together, and a separate count of 1,000,000 for each could never decide a verdict. The interface row now says so. Both checkers were held to every limit of the table, at its value and one past it, by the validation limits' corpus. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-module-check: check-module.mjs, the second checker, and the differential
check-module.mjs generalises wai-vector's check-mvp.mjs, which reads a module of WebAssembly 1.0, to WebAssembly 3.0 and to the profile's rules, with no dependency: an ES module a page imports (check, levelOf) and a command line like the Rust checker's. It decodes every section and instruction and validates the module as WebAssembly 3.0 does, written from that text: recursion groups canonicalised so that equivalent types are one, subtyping over the abstract and the defined heap types, typed and untyped stacks, local initialisation, the constant expressions, and the validation limits of §4.2. While it validates it records each item that breaks R3 to R12, with the level and the cap the item depends on, so one reading serves both levels. differential.mjs is the differential's second half: it runs check-module.mjs on every module examples/differential.rs writes, at both levels under the same caps, and names each verdict that differs. On the committed seed the two checkers agree on all 20,000 verdicts of 10,000 modules. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-module-check: the Rust checker of the deterministic module profile
A module's verdict at the integer or the float level under caps (deterministic-modules §4.3): R1 on the length; R2 by the validator of wasmparser 0.262.0, pinned exactly, with the features of WebAssembly 3.0 and no others (its WASM3 set less threads, which 3.0 does not define), whose limits are the profile's validation limits; then R3 to R12 over the module's items in binary order, read from the same parser with each item's offset, an instruction classed by its name and proposal as the parser lists them; then the absences R6 and R10 at the module's length. `findings` lists every rule every item breaks, the first being the verdict. The binary prints a verdict, the level a sink holds a module at (§6 check 9b), or checks a cases.txt. tests/module_rules.rs holds it to planted/cases.txt: every module gets its stated verdict at each level and under each caps; every planted module breaks exactly its row's rule (the two rows §9.1 says break a second, and the relaxed instruction that takes float lanes, named); every rule R1 to R12 has a planted module; the levels differ only in R3. A unit test holds R12's list to every instruction of the proposals it names. examples/differential.rs is the differential's first half: modules from wasm-smith 0.262.0 and this checker's verdicts, from a committed seed. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-module-check: the validation limits' corpus, built from source
`build.py --limits DIR` writes, for each validation limit of deterministic-modules §4.2, minimal-int with the part it bounds at the limit and one past it, and the verdicts by construction: at the limit, the rule the part breaks, if any; one past it, refused R2. The modules reach 10 MB, so the corpus is generated where it is checked and not committed. The planted set's bytes are unchanged (`build.py --check`): the joining of bytes is now linear, which the limits' million-entry sections need. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai-module-check: the checker corpus of the deterministic module profile, built from source
deterministic-modules §9.1 gives each module by its construction: minimal-int, and minimal-int with one change for every case but component. planted/build.py is that construction, byte by byte, standard library only. It writes each module and cases.txt, the verdicts §9.1 states, at each level the row names and under its caps. Every offset in cases.txt is the place where the item its row names lands in the bytes, marked while they are put together, so no verdict is taken from a checker; the two checkers come after this commit. Lines §4.3 decides but §9.1 does not state (a row's other level where it breaks only R3, the profile's caps for the rows with lower ones) are marked as derived. grow-swallowed, §9.2's module, is held: R13 is no checker's rule. `build.py --check` fails unless the committed files are what it writes. Co-Authored-By: Claude Opus 5.5 <[email protected]>
deterministic-modules: fix R2's validation limits, and say how R3 reads a block type
R2 asks for a valid module, but WebAssembly 3.0 lets an implementation limit the number and the size of a module's parts, and a validator a checker is built on does: without fixed limits, two conforming checkers could give one module within the caps different verdicts, so the verdict was not a function of the bytes. §4.2 now fixes the limits, and a module beyond one is refused R2. R3 now says how an instruction whose types an immediate or another item fixes (a block, a typed select, a call) is refused: through that value type, which follows the opcode for a block type or a typed select. The item term covers instructions in constant expressions and a declaration of no locals, and R7's funcref covers both of its encodings. These are the readings both checkers take. Co-Authored-By: Claude Opus 5.5 <[email protected]>
wai/det-module-profile, converted to the layout of the fix: no shared append point
Some checks failed
wai-ops integer operators / does this change touch it (pull_request) Successful in 6s
WAI conformance / fast integer kernels, every x86_64 kernel set (AVX-512 silicon) (pull_request) Successful in 3m34s
WAI breaking changes and the conformance runner / WAI breaking · wire, record and API against main · linux (pull_request) Successful in 57s
WAI breaking changes and the conformance runner / WAI breaking and conform · their tests, and the independent verifiers through wai conform · linux (pull_request) Successful in 2m39s
WAI conformance / quantum core and corpus under wasm32-wasip2 (wasmtime) (pull_request) Successful in 3m10s
WAI conformance / faces from keypoints under wasm32-wasip2 (wasmtime) (pull_request) Successful in 1m32s
wai-ops integer operators / wasm32-wasip2 (wasmtime) (pull_request) Successful in 38s
wai-ops integer operators / independent checker (Python) (pull_request) Successful in 22s
wai-ops integer operators / wasm32 under Node (pull_request) Successful in 25s
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 1m40s
WAI energy receipts / energy receipts · linux (pull_request) Successful in 14m30s
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 18m17s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Has been cancelled
standards workspaces build + test / macOS energy backends (pull_request) Has been cancelled
standards workspaces build + test / joule-code-rs (joule-code/joule-code-rs, joule-code-rs, linux-arm64, true) (pull_request) Has been cancelled
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Has been cancelled
WAI conformance / cargo-class corpora · macos (pull_request) Has been cancelled
WAI conformance / v2 vocabulary · manifests validate as stated (pull_request) Has been cancelled
WAI conformance / independent verifiers · claims, JWP, key discovery and integer payloads (Python) (pull_request) Has been cancelled
WAI conformance / each feature of the independent verifiers' steps compiles alone (pull_request) Has been cancelled
WAI conformance / delivery telemetry · CMCD and CMSD against an independent library (pull_request) Has been cancelled
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Has been cancelled
WAI conformance / cross-arch byte-equality · macos (pull_request) Has been cancelled
WAI conformance / codec wrappers · fuzz smoke, text decode limits, C entry points, provenance, the semantic path (pull_request) Has been cancelled
WAI conformance / C2PA manifest emission · signed, read back, validated (pull_request) Has been cancelled
WAI energy receipts / energy receipts · linux-arm64 (pull_request) Has been cancelled
WAI energy receipts / energy receipts · macos (pull_request) Has been cancelled
wai-ops integer operators / linux-aarch64 (pull_request) Has been cancelled
wai-ops integer operators / linux-x86_64 (pull_request) Successful in 50s
wai-ops integer operators / macos-arm64 (pull_request) Has been cancelled
The change of wai/det-module-profile (4e8e4fb09..45a7b4eb7, 2 commits), on the fix branch: its changelog entries as files of wai/changes/, its wai-conformance.yml edits as step files, corpus files and test tags, and every other file as the branch has it. - 9061cb07f wai: the deterministic module profile, a checked subset of WebAssembly for the decoder modules a sink runs - 45a7b4eb7 wai: the deterministic module profile: a record's key read from the grant's head; the scope of check 9; what the verifiers and corpora cover Co-Authored-By: Claude Opus 5.5 <[email protected]>