wai: the deterministic module profile's two checkers, a Rust one and a dependency-free one, held to each other #647

Closed
dcharlot wants to merge 12 commits from wai/det-module-checkers into main
Owner

Merge order. Stacked on #640 (the profile's text, wai/det-module-profile), merge after it. Until #640 merges, this pull request's diff includes its commits.

The two checkers of the deterministic module profile (wai/extensions/deterministic-modules.md, working name): one in Rust, and one with no dependencies that a page can import. Each is held to the profile's planted modules and to the other.

The Rust checker

wai/wai-module-check/, on wasmparser =0.262.0.

  • Validity (R2): WebAssembly 3.0's features without threads. wasmparser's 3.0 set includes threads, and 3.0 does not.
  • Length (R1), then R3 to R12 over each item's offset in binary order, with instructions classified by wasmparser's own operator list. The absence rules, R6 and R10, are checked at the module's length.
  • A CLI with --level, --caps and --cases.
  • tests/module_rules.rs checks that:
    • every planted module gets its stated verdict and breaks exactly its row's rule;
    • every rule from R1 to R12 has a planted module;
    • the two levels differ only in R3.

The planted set

planted/build.py, standard library only, builds §9.1's modules byte by byte. Each verdict's offset is where the generator marked the item while building it, never what a checker says. build.py --limits DIR generates the limits corpus: each validation limit at its value and one past it, 44 modules. It is built in CI, not committed.

The dependency-free checker

check-module.mjs, written from the specification. It decodes and validates all of WebAssembly 3.0 itself: GC subtyping, exception handling, typed references and the limits. Its opcode tables match wasmparser's decoder entry for entry. check-mvp.mjs is unchanged: it still does wai-vector's 1.0-only check.

Held to each other

examples/differential.rs writes 10,000 generated modules from the committed seed 0x6465742d6d6f6431, plus two mutated copies of each, and differential.mjs compares the verdicts. Every rule occurs.

Text corrections to the profile, in their own commits

  • R2 is decidable. WebAssembly 3.0 lets a validator choose its own limits, so two checkers could give one module different verdicts. §4.2 now states a table of validation limits, each confirmed at its boundary by both checkers.
  • R3 is stated for block types and typed selects: refused through the value type after the opcode. Two §9.1 rows hold it, float-block-type and float-select-type.
  • Items: these include instructions in constant expressions and declarations of zero locals. R7's funcref covers both of its encodings.

Verified

On a Linux build host, on Rust 1.99.1:

  • build.py --check: the 53 modules and cases.txt reproduce byte for byte.
  • module_rules: 6 of 6 tests pass, and the unit tests 2 of 2.
  • The planted set: 112 of 112 verdicts in each checker. The limits corpus: 88 of 88 in each.
  • The differential: all 60,000 verdicts agree.
  • clippy, with warnings as errors: clean. The lockfile is current, and the advisory scan finds none.
  • On WebAssembly's own spec tests (examples/spectest.rs), the Rust checker refuses every invalid and malformed module and no valid one, and the two checkers agree on all 11,424 verdicts. This is not in CI, because CI fetches only from the forge.

Of 25 single-line breakages of the checkers, 24 were caught by the planted set, the limits corpus, the differential or the spec tests. The one survivor is cancelled by the next check, so it changes nothing.

CI runs it as one step file, .github/wai-conformance/verifiers/module-check.sh, with the trigger path wai/wai-module-check/**. The changelog entry is wai/changes/2026-11-05-deterministic-module-checkers.md.

🤖 Generated with Claude Code


Closed: Landed as direct commits on main, with the checkers (#647) and the final name WA²ISM™ (WAISM in running text), under the working model of 2026-11-06. Before landing, on the rebased tree: the module-check step passed on a build host, the two checkers agreeing on all 11424 verdicts of 5712 modules, with the repository's public-text, changelog, spec-reference and conformance-list checks.

**Merge order.** Stacked on #640 (the profile's text, `wai/det-module-profile`), merge after it. Until #640 merges, this pull request's diff includes its commits. The two checkers of the deterministic module profile (`wai/extensions/deterministic-modules.md`, working name): one in Rust, and one with no dependencies that a page can import. Each is held to the profile's planted modules and to the other. ## The Rust checker `wai/wai-module-check/`, on `wasmparser` `=0.262.0`. - **Validity (R2):** WebAssembly 3.0's features without threads. `wasmparser`'s 3.0 set includes threads, and 3.0 does not. - **Length (R1)**, then **R3 to R12** over each item's offset in binary order, with instructions classified by `wasmparser`'s own operator list. The absence rules, R6 and R10, are checked at the module's length. - **A CLI** with `--level`, `--caps` and `--cases`. - **`tests/module_rules.rs`** checks that: - every planted module gets its stated verdict and breaks exactly its row's rule; - every rule from R1 to R12 has a planted module; - the two levels differ only in R3. ## The planted set `planted/build.py`, standard library only, builds §9.1's modules byte by byte. Each verdict's offset is where the generator marked the item while building it, never what a checker says. `build.py --limits DIR` generates the limits corpus: each validation limit at its value and one past it, 44 modules. It is built in CI, not committed. ## The dependency-free checker `check-module.mjs`, written from the specification. It decodes and validates all of WebAssembly 3.0 itself: GC subtyping, exception handling, typed references and the limits. Its opcode tables match `wasmparser`'s decoder entry for entry. `check-mvp.mjs` is unchanged: it still does wai-vector's 1.0-only check. ## Held to each other `examples/differential.rs` writes 10,000 generated modules from the committed seed `0x6465742d6d6f6431`, plus two mutated copies of each, and `differential.mjs` compares the verdicts. Every rule occurs. ## Text corrections to the profile, in their own commits - **R2 is decidable.** WebAssembly 3.0 lets a validator choose its own limits, so two checkers could give one module different verdicts. §4.2 now states a table of validation limits, each confirmed at its boundary by both checkers. - **R3** is stated for block types and typed `select`s: refused through the value type after the opcode. Two §9.1 rows hold it, `float-block-type` and `float-select-type`. - **Items:** these include instructions in constant expressions and declarations of zero locals. R7's `funcref` covers both of its encodings. ## Verified On a Linux build host, on Rust 1.99.1: - `build.py --check`: the 53 modules and `cases.txt` reproduce byte for byte. - `module_rules`: 6 of 6 tests pass, and the unit tests 2 of 2. - The planted set: 112 of 112 verdicts in each checker. The limits corpus: 88 of 88 in each. - The differential: all 60,000 verdicts agree. - clippy, with warnings as errors: clean. The lockfile is current, and the advisory scan finds none. - On WebAssembly's own spec tests (`examples/spectest.rs`), the Rust checker refuses every invalid and malformed module and no valid one, and the two checkers agree on all 11,424 verdicts. This is not in CI, because CI fetches only from the forge. Of 25 single-line breakages of the checkers, 24 were caught by the planted set, the limits corpus, the differential or the spec tests. The one survivor is cancelled by the next check, so it changes nothing. CI runs it as one step file, `.github/wai-conformance/verifiers/module-check.sh`, with the trigger path `wai/wai-module-check/**`. The changelog entry is `wai/changes/2026-11-05-deterministic-module-checkers.md`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --- **Closed:** Landed as direct commits on main, with the checkers (#647) and the final name WA²ISM™ (WAISM in running text), under the working model of 2026-11-06. Before landing, on the rebased tree: the module-check step passed on a build host, the two checkers agreeing on all 11424 verdicts of 5712 modules, with the repository's public-text, changelog, spec-reference and conformance-list checks.
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
13285059b4
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]>
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]>
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]>
`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]>
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]>
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]>
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]>
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]>
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]>
§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]>
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]>
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
1dd0d2211b
Co-Authored-By: Claude Opus 5.5 <[email protected]>
dcharlot closed this pull request 2026-11-06 18:28:32 -05:00
Some checks failed
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 7s
WAI breaking changes and the conformance runner / WAI breaking · does this change touch WAI (pull_request) Successful in 5s
WAI conformance / does this change touch it (pull_request) Successful in 5s
WAI energy receipts / does this change touch it (pull_request) Successful in 5s
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

Pull request closed

Sign in to join this conversation.
No reviewers
No labels
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
Transaction-Science/open-standards!647
No description provided.