Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 15 Packages Wiki Activity Actions 6

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
pull from: wai/det-module-checkers
merge into: Transaction-Science:main
Conversation 0 Commits 12 Files changed 75 +4601 -21
75 changed files with 4601 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

34
.github/wai-conformance/verifiers/module-check.sh vendored Normal file
View file

@ -0,0 +1,34 @@
# step: deterministic module profile · the Rust checker, check-module.mjs and their differential
# order: 780
# paths: wai/extensions/deterministic-modules.md wai/wai-module-check/**
# working-directory: wai/wai-module-check
#
# The deterministic module profile (extensions/deterministic-modules.md): its two checkers,
# held to the same corpora and to each other. planted/build.py rebuilds the checker corpus
# of §9.1 from each module's construction, byte for byte, with the verdicts their rows state.
# The Rust checker (wasmparser, pinned) runs tests/module_rules.rs (every module its verdict,
# every planted module exactly its rule, every rule a planted module, the levels differing
# only in R3) and then the corpus itself; check-module.mjs, the second implementation,
# written from the text with no dependency and sharing no code with it, runs the same
# corpus. Both then run the validation limits' corpus (§4.2: each limit at its value and one
# past it), which build.py generates here, being too large to commit. Last, the differential:
# examples/differential.rs writes 10,000 modules from wasm-smith, from its committed seed,
# and two mutated copies of each, with the Rust checker's verdicts, and differential.mjs
# requires check-module.mjs to give every one the same verdict at both levels.
#
# The paths this step brings to the workflow's trigger, and why:
# wai/extensions/deterministic-modules.md: the rules, the limits and the corpus the checkers
# implement.
# wai/wai-module-check/**: the checkers, the corpus and its generator, and the differential.
set -euo pipefail
python3 -I planted/build.py --check
cargo test --locked --release
cargo run --locked --release -q -- --cases planted
node check-module.mjs --cases planted
python3 -I planted/build.py --limits "$RUNNER_TEMP/module-limits"
cargo run --locked --release -q -- --cases "$RUNNER_TEMP/module-limits"
node check-module.mjs --cases "$RUNNER_TEMP/module-limits"
rm -rf "$RUNNER_TEMP/module-limits"
cargo run --locked --release -q --example differential -- --out "$RUNNER_TEMP/module-differential"
node differential.mjs "$RUNNER_TEMP/module-differential"
rm -rf "$RUNNER_TEMP/module-differential"

2
.github/workflows/wai-conformance.yml vendored
View file

@ -112,6 +112,8 @@ on:
- 'wai/research/catalogue-prior/**'
- 'wai/tools/wai_catalogue_prior_verify.py'
- 'wai/wai-web/**'
# The deterministic module profile's two checkers, its corpus and their differential.
- 'wai/wai-module-check/**'
# The audio provenance check below reads the corpora above with this tool.
- 'wai/tools/wai_audio_provenance_check.py'
- '.github/workflows/wai-conformance.yml'

4
wai/SPEC.md
View file

@ -2601,7 +2601,9 @@ WebAssembly, or a neural decoder.
**What the exact tier covers.** `decode-equivalence` covers the medium a sink emits and
can hash ([determinism-tiers](extensions/determinism-tiers.md) §2), on the fabrics
determinism-tiers §5 lists: native CPU and WebAssembly in this revision, and, for a
determinism-tiers §5 lists: native CPU and WebAssembly in this revision (on WebAssembly, a
module a sink holds at the integer level of the deterministic module profile,
[deterministic-modules](extensions/deterministic-modules.md) §6), and, for a
decoder's `wai-ops/1-i32` graphs, the GPUs and backends listed there, with no NPU
decoder: on a neural processor only the operator vectors of `wai-ops/1-npu` have run
(integer-operators §9.5). It never covers output the application cannot read. A sink MUST NOT state

37
wai/changes/2026-11-04-deterministic-module-profile-checked-subset-webassembly.md Normal file
View file

@ -0,0 +1,37 @@
### The deterministic module profile: a checked subset of WebAssembly for the decoder modules a sink runs
- **A new extension, [extensions/deterministic-modules.md](extensions/deterministic-modules.md).** A sink checks a
WebAssembly decoder module before it instantiates it, against numbered rules (§4), each naming the clause of
WebAssembly 3.0 or of WAI it rests on. The profile has two levels (§2). The integer level refuses floating point,
relaxed vector instructions, imports, a start function and a table that can change, and requires one memory with a
declared maximum; its output is the same on every engine that implements WebAssembly 3.0, with no engine setting.
The float level admits floating point; its output holds a tier only on an engine set to the NaN rule of the
deterministic profile (DET) of WebAssembly 3.0, shown by a probe in the sink's process, and never above
`entropy-consistency`. A module exports a fixed interface of `i32` functions (§5). Checks 9 to 13 follow
jwp-receipts §7.9's checks 1 to 8 (§6): the rules; a `conform-result/1` record over the module's digest that
attests its capability's vectors and its refusal of every failed `memory.grow`, signed by a key that the head the
grant was confirmed under lists with `module/decoder`; the engine; an instantiation with
an empty import object; a run under a guard, where a trap or a limit is a refusal and nothing is output; and the
output's hash. The refusal codes are in §8, and the corpora a checker, a module and an engine are held to in §9,
with a planted module for every rule, each given by its construction from one minimal module.
- **jwp-receipts.** §7.9 gains checks 9 and 10 for every decoder module a sink would run on a WebAssembly engine,
whatever its bytes, and their four codes; `key_log::module_check` implements checks 1 to 8, and the key-log corpus
(§5.8) is of checks 1 to 8. §7.5's *Modules* lets a key that holds `module/decoder` sign the record of check 9c,
which a sink finds in the head the grant was confirmed under, since the record carries no `signer_id`. §2.4.12's
decoder entry gains five module members (`module_profile`, `engine`, `engine_settings`, `module_probe`,
`conform_result`), which a `module:` entry that ran under the profile carries and every other entry, and every
entry sealed under an earlier text, does not; and rules 15 to 17, with the codes `session_module_profile_missing`
and `session_module_engine_not_deterministic`. A verifier that implements the profile reads the members and applies
the three rules; one that does not refuses the members as `unknown_member`, as `wai-rs` and `claim_verify.py` do,
and §5.11's claim corpus covers rules 1 to 14. A `module:` entry at `decode-equivalence` sealed under an earlier
text was valid, and a verifier that implements the profile now refuses it (rule 16): that text let a sink state the
tier for a module's output with nothing of the module checked.
- **browser-sink §4.3 step 6.** A wasm decoder's output holds the registered tier only where the decoder is a module
the page holds at the integer level; §7.2 binds the frames of any other wasm decoder at `none`. The routing, the
route's tier and §11's reasons are unchanged. `frame_tier`, the second implementation and the corpus take a `wasm`
frame's decoder to be such a module (§12), and the page the text names loads no wasm decoder for a room's tracks.
- **determinism-tiers §5, integer-operators §6 and SPEC §7.** WebAssembly as a fabric of `decode-equivalence` is a
module a sink holds at the integer level. determinism-tiers §5 states that CI checks wai-web's packages for relaxed
SIMD and threads only, and that the package of record holds floating-point instructions and imports, which the
integer level refuses.
- This change is text. It changes no code, vector or workflow.

29
wai/changes/2026-11-05-deterministic-module-checkers.md Normal file
View file

@ -0,0 +1,29 @@
### The deterministic module profile's two checkers, and fixed validation limits for R2
- **Two checkers of [extensions/deterministic-modules.md](extensions/deterministic-modules.md).**
`wai/wai-module-check` gives a module's verdict (§4.3) at the integer or the float level under caps: R1 on its
length, R2 by a WebAssembly 3.0 validator, then R3 to R12 over its items in binary order and the absences R6 and
R10. The Rust checker is built on wasmparser, pinned at 0.262.0, with the features of WebAssembly 3.0 and no
others; a command prints a verdict, the level a sink holds a module at (§6, check 9b), or checks a corpus.
`check-module.mjs` is the second: written from the text with no dependency and sharing no code with the first,
it decodes and validates every construct of WebAssembly 3.0 itself, garbage collection, exception handling and
typed function references included, and is the ES module a page imports before it instantiates a decoder
module. It generalises wai-vector's `check-mvp.mjs`, which stays as it is for that crate's own package check.
- **The corpora.** `planted/build.py` builds the checker corpus of §9.1 from each module's construction, byte for
byte, and takes each verdict's offset from the item it marks while building, never from a checker. Both checkers
give every module its stated verdict; `tests/module_rules.rs` also requires every planted module to break exactly
its row's rule, every rule R1 to R12 to have one, and the levels to differ only in R3. `build.py --limits`
generates the validation limits' corpus, each limit at its value and one past it. The differential writes
10,000 modules from wasm-smith from a committed seed, with two mutated copies of each, and requires the two
checkers to give every one the same verdict at both levels; `examples/spectest.rs` does the same with the
modules of the specification's test scripts, run by hand on a copy of them.
- **deterministic-modules §4.1 and §4.2.** R2's module is valid within a table of validation limits that §4.2 now
fixes (the counts of a module's parts, the sizes of a name, a body, a function type and a struct, the catches of
a `try_table`, the depth of a subtype chain, and the sum its imports and exports weigh): WebAssembly 3.0 lets an
implementation limit these, so without them two conforming checkers could differ on a module within the caps. A
module beyond one is refused R2. R3 states that an instruction whose types a block type or a typed `select`
fixes is refused through that value type, which follows its opcode, and §9.1 gains a planted module for each
(`float-block-type`, `float-select-type`); an item is also an instruction of a constant expression and the
value type of a declaration of no locals; and R7's `funcref` is either of its encodings.
- **CI.** `wai-conformance.yml` runs both checkers on the corpus, the limits and the differential, from
`.github/wai-conformance/verifiers/module-check.sh`.

24
wai/extensions/browser-sink.md
View file

@ -25,7 +25,8 @@
> `browser_sink`), which `wai/wai-live-web` builds for the page; the page's own code is
> `joule-code/joule-code-rs/crates/joule-moq-web/web/room/binding.js`; the corpus is
> [`live-conformance/browser/`](../live-conformance/browser/), and its second implementation is
> `live-conformance/browser_sink_verify.py`.
> `live-conformance/browser_sink_verify.py`. Each takes a `wasm` frame's decoder to be a module
> the page holds at the integer level of the deterministic module profile (§4.3 step 6, §12).
> Keywords **MUST**, **MUST NOT**, **SHOULD**, **MAY** are RFC 2119/8174.
>
> Texts read for this revision, each pinned to the version named: WebCodecs, W3C Working Draft
@ -235,9 +236,13 @@ For each object `o` of a report, in order, the page computes its route:
for `not_run`, `ua_probe_mismatch` for `mismatch`).
5. **The host leg.** It is taken when `o.capability` is in `host` (`no_host`) with a tier at
least the need (`host_inexact`).
6. **The wasm leg.** It is taken when `o.capability` is in `wasm` (`no_wasm`). A wasm decoder
is WAI's own, so its output holds the registered tier, which step 2 has already held to be at
least the need.
6. **The wasm leg.** It is taken when `o.capability` is in `wasm` (`no_wasm`). The route's tier
is the registered tier, which step 2 has already held to be at least the need. A wasm
decoder's output holds that tier only where the decoder is a module the page holds at the
integer level of the deterministic module profile
([deterministic-modules](deterministic-modules.md) §6), authorised under
[jwp-receipts](jwp-receipts.md) §7.9 and checked before the page instantiated it; the frames
of any other wasm decoder are bound at `none` (§7.2).
7. **Route.** The route is the first leg taken, in the order UA, host, wasm. Where none is taken
the route is `none` (`no_decoder`), and each leg's reason is reported.
@ -459,6 +464,8 @@ lowered to `none` where:
- the route is `ua` and the frame's `format` is `null`: its samples cannot be read without a
conversion, so nothing can check them;
- the route is `wasm` and its decoder is not a module the page holds at the integer level of the
deterministic module profile (§4.3 step 6);
- the page altered the samples after the decode (determinism-tiers §2, *What a tier covers*).
Where the frame's tier is below the object's need, the page **MUST NOT** present the frame as
@ -613,7 +620,8 @@ written by `wai_browser_sink_vectors gen`. It has:
class, the unmetered case, a figure under another route's key, and each refusal of §6.
- **Bindings**: values with their reading: canonical forms, each refusal of §7.1, an unknown tier
read as `none`, and a member the text does not define; the tier §7.2 gives a frame for each
route, format and alteration; and objects bound under a signed group
route, format and alteration, a `wasm` frame's decoder being a module the page holds at the
integer level of the deterministic module profile (§4.3 step 6); and objects bound under a signed group
receipt, each binding's `digest` the object's content hash and its `receipt` the receipt's link
hash, the receipt's signature and the object's inclusion verifiable from the corpus.
- **Frames**: inputs to §10 with their state, covering every row.
@ -622,7 +630,11 @@ written by `wai_browser_sink_vectors gen`. It has:
`wai_browser_sink_vectors verify` and the test `tests/browser_sink.rs` check that `vectors.json`
regenerates byte for byte, that `wai-rs` gives every case its stated outcome, that every reason of
§11 appears, and that §11 lists exactly the reference's codes.
§11 appears, and that §11 lists exactly the reference's codes. `frame_tier` in `wai-rs`, which
the page calls as `frameTier`, is given no module status: it gives a `wasm` frame the tier §7.2
gives the frame of a decoder held at the integer level, and every `wasm` frame of the corpus, the
chain's among them, is of such a decoder. The page whose code the header names loads no wasm
decoder for a room's tracks, so it binds no frame on the `wasm` route.
`live-conformance/browser_sink_verify.py` is the second implementation, written from this text:
it shares no code with `wai-rs`, reads each capability's kind, status and replicate class from the
registry export ([`registry/capabilities.json`](../registry/capabilities.json)), checks

14
wai/extensions/determinism-tiers.md
View file

@ -628,9 +628,17 @@ shows, by fabric:
(`wasm-tools validate`). CI (`wai-web-wasm.yml`) validates both of the crate's
bundles and the package of record, `reach/record/wai_web_bg.wasm`, with relaxed SIMD
and threads disabled, and fails on a module that uses either. CI does not check that
they contain no other SIMD instruction. A WebAssembly decoder at this
tier MUST NOT use relaxed-SIMD instructions, whose results the WebAssembly
specification lets engines choose among, and MUST NOT depend on the bits of a NaN.
they contain no other SIMD instruction, or check them against the deterministic module
profile ([deterministic-modules](deterministic-modules.md)): on the source of the change
that added this sentence, the package of record holds floating-point instructions and
imports, which that profile's integer level refuses. A WebAssembly decoder holds this tier
at a sink only as a module the sink holds at that integer level (deterministic-modules §6).
That level refuses relaxed-SIMD instructions, whose results the WebAssembly specification
lets engines choose among, and every floating-point instruction, so no output of such a
module depends on the bits of a NaN, and it needs no engine setting. A floating-point decode
on WebAssembly fixes its NaNs only under the deterministic profile (DET) of WebAssembly 3.0,
and the deterministic module profile's float level, which runs under it, holds no tier above
`entropy-consistency` (deterministic-modules §2).
- **GPU.** A decoder's `wai-ops/1-i32` graphs ([integer-operators](integer-operators.md)
§9.1) run on a GPU through `wai/wai-ops-gpu`: WGSL compute kernels in 32-bit words, at
the `acc32` widths for a graph whose certificate meets that profile, and otherwise in

510
wai/extensions/deterministic-modules.md Normal file
View file

@ -0,0 +1,510 @@
# WAI Extension: Deterministic Module Profile
> Status: Draft. The deterministic module profile is a checked subset of standard WebAssembly,
> run by unmodified engines. It is not a fork of WebAssembly and not a new bytecode: it adds no
> instruction, type, section or semantics, and any engine that implements WebAssembly 3.0 runs a
> module that meets it. What the profile decides is what a sink may state about such a module's
> output. It has two levels (§2): an **integer level**, with no floating point, whose output is the
> same on every engine with no engine setting; and a **float level**, which admits floating point
> and holds a tier only on an engine set to the NaN rule of the deterministic profile of
> WebAssembly 3.0.
> A sink checks a decoder module against numbered rules (§4) before it instantiates it, holds a
> signed conformance result over the module's digest (§6, check 9c), runs it through a fixed
> interface (§5) under the settings of §7, refuses with the codes of §8, and names what it checked
> in its receipt (§10). Checks 9 to 13 follow [jwp-receipts](jwp-receipts.md) §7.9's checks 1 to 8,
> which authorise the module and which this text leaves as they are. The corpora a checker, a
> module and an engine are held to are in §9. This text defines the profile; it names no
> implementation.
> Keywords **MUST**, **MUST NOT**, **SHOULD**, **MAY** are RFC 2119/8174.
>
> Texts read for this revision: WebAssembly 3.0, the specification build dated 2026-11-04: the
> appendix *Profiles* (*Defined Profiles*: the full profile, FUL, and the deterministic profile,
> DET); the appendix *Implementation Limitations* (*Execution*); *Execution*, *Numerics*
> (*Floating-Point Operations*: *Rounding*, *NaN Propagation*; *Relaxed Operations*) and
> *Instructions* (`memory.grow`); *Binary Format*, *Types* (limits) and *Modules* (the preamble,
> the section ids, custom sections, the start section). A section number in this text is this
> extension's unless it names another document.
## 1. Scope
In scope: the two levels (§2); the rules a module meets, the caps and a checker's verdict (§4);
the interface a module exports (§5); the steps a sink takes to check and run a module (§6); the
engine settings it uses (§7); the refusal codes (§8); the corpora (§9); what a receipt states
(§10); and conformance (§11).
Out of scope: how a sink obtains a module and who may grant it ([jwp-receipts](jwp-receipts.md)
§7.9, [http-delivery](http-delivery.md) §8.4); reconstruct modules, and decoder modules a sink
runs on no WebAssembly engine, which this text does not cover; the arithmetic a decoder
computes, which its capability's text fixes ([integer-operators](integer-operators.md) for the
integer graphs); and a pinned parameter set, which is data and is held by jwp-receipts §7.9's
checks 1 to 8 alone.
Relationship to WebAssembly and to the other texts:
- **WebAssembly 3.0.** Core WebAssembly leaves open the sign and payload of a NaN, the results of
the relaxed vector instructions, whether `memory.grow` and `table.grow` succeed, what an engine
does past its resource limits, and every value a host supplies through an import. Every other
result is fixed: integer instructions are exact, and floating-point ones are rounded to nearest,
ties to even (*Numerics*, *Rounding*). The **deterministic profile** (DET) of WebAssembly 3.0
(appendix *Profiles*, *Defined Profiles*) fixes the first two: every NaN a floating-point
instruction generates is canonical and positive, and every relaxed vector instruction has one
behaviour. Under it, `memory.grow` and `table.grow` remain non-deterministic. The integer level
refuses floating point and relaxed vector instructions, so nothing the deterministic profile
changes is reachable from it, and it needs no engine setting. The float level needs the
deterministic profile's NaN rule, and nothing else of it is reachable, since both levels refuse
relaxed vector instructions (R4). Both levels refuse imports, fix the memory and the table, and
turn a failed `memory.grow` into a refusal.
- **[jwp-receipts](jwp-receipts.md) §7.9.** A module's identity is its digest, the SHA-256 of
its bytes as instantiated, and its grant, key log, revocation and fallback are §7.9's. Its
checks 9 and 10 are this text's (§6).
- **[jwp-receipts](jwp-receipts.md) §2.4.12.** The decoder entry of a `reconstruct-session`
claim names the level, the engine, its settings, the probe and the conformance result (§10).
- **[conformance-results](conformance-results.md).** The record a sink holds for check 9c.
- **[browser-sink](browser-sink.md) §4.3 step 6.** The tier a page's wasm decoder holds.
- **[determinism-tiers](determinism-tiers.md) §5 and SPEC §7.** WebAssembly as a fabric of
`decode-equivalence` is a module held at the integer level.
- **[integer-operators](integer-operators.md) §6.** On WebAssembly, two of that section's
"MUST NOT"s are properties of the module a sink checks.
## 2. Levels
The profile's identifiers are defined here, and only here. Every other text, this one included,
names a level as the **integer level** or the **float level**.
| level | identifier | floating point | engine | what its output holds |
|---|---|---|---|---|
| integer level | `det-module/1-int` | refused (R3) | any engine that implements WebAssembly 3.0, a browser's included, with no setting | the class tier of its capability ([SPEC](../SPEC.md) §3.1, *Tier*) and, for a `GenerativeDeterministic` capability, its generation-equivalence (SPEC §7) |
| float level | `det-module/1-det` | admitted | only an engine set to the deterministic profile's NaN rule, shown by the probe (§6, check 10); no page (§7) | `entropy-consistency` where that is the class tier of its capability, on such an engine; otherwise none. Never `decode-equivalence` or generation-equivalence: SPEC §7, *Replicate-soundness*, admits a neural decode at `decode-equivalence` only where no floating-point operation is on its path, and this revision gives the float level neither |
The levels differ only in R3. Each identifier names this text's version 1; a module meets a
level when a checker gives it `held` at that level (§4.3), and R13.
## 3. Terms
- **Module**: a decoder module (jwp-receipts §7.9) that a sink would run on a WebAssembly
engine, whatever its bytes. Bytes that are not a WebAssembly 3.0 module, such as a component
or bytes that do not decode, are such a module where a sink would run them on one, and R2
refuses them (§4.3). A decoder module a sink runs on no WebAssembly engine is not one.
- **Item**: a part of a module's bytes a rule is about: an instruction, in a function body or a
constant expression; a value type, in a function type, a local declaration (one that declares
no locals among them), a global type, a block type or a typed `select`; an entry of the
import, table, memory, global or export section; a type entry of the type section; or a section.
- **Caps**: the three limits of §4.2's first table. Its validation limits are part of R2, and are
no caps.
- **Verdict**: a checker's answer for a module at a level under caps (§4.3).
- **Need**: the tier a sink holds an object's decoded output to, as [browser-sink](browser-sink.md)
§2 defines it, for any sink: the object's pin `tier`, else its track's declared determinism,
else `none`.
- **Held at a level**: a sink holds a module at a level, for an object, when checks 1 to 10 of §6
pass for it at that level.
## 4. Rules
### 4.1 The rules
Each rule names what it rests on: a clause of WebAssembly 3.0, or a clause of WAI. §9.1 names,
for each rule, at least one planted module that breaks it and no other.
| rule | level | the module | rests on |
|---|---|---|---|
| R1 | both | is at most `module_bytes` long (§4.2). | WebAssembly 3.0, *Implementation Limitations* (an implementation may limit the size of a module); §4.2 |
| R2 | both | is a WebAssembly 3.0 module: its bytes decode under the binary format, from the preamble `\0asm` and version 1, and it is valid, within the validation limits of §4.2. Shared memory, atomic instructions, a component, and every other construct WebAssembly 3.0 does not define, are outside it. | WebAssembly 3.0, *Binary Format* (*Modules*: the preamble and the section ids; *Types*: limits, whose four forms have no shared one), *Validation* and *Implementation Limitations* (an implementation may limit the number and size of a module's parts); §4.2 |
| R3 | integer | contains no floating point: no `f32` or `f64` value type, and no instruction that takes or gives a floating-point value, an `f32` or an `f64` or a `v128` read or written as `f32x4` or `f64x2` lanes. That covers constants, arithmetic, comparisons, conversions to and from integers (the saturating truncations among them), reinterpretations, lane splats and extractions, and loads and stores of floating-point values. | WebAssembly 3.0, *Numerics*, *NaN Propagation* (the sign of a NaN result is non-deterministic, and its payload is chosen among arithmetic NaNs); SPEC §7, *Replicate-soundness* (no float operation anywhere on a decode path that backs `replicate`); integer-operators §6 |
| R4 | both | contains no relaxed vector instruction: the integer ones (`i8x16.relaxed_swizzle`, the four `relaxed_laneselect`s, `i16x8.relaxed_q15mulr_s`, the two relaxed dot products) as well as the floating-point ones. | WebAssembly 3.0, *Numerics*, *Relaxed Operations* (each result is one of a set, and the implementation chooses which); integer-operators §6 (no instruction whose result the instruction set leaves to the implementation) |
| R5 | both | imports nothing: no function, table, memory, global or tag. | WebAssembly 3.0, *Binary Format*, *Modules* (the import section, whose values the host supplies at instantiation); §5 (the output is a function of the capability, the payload and the set alone) |
| R6 | both | defines exactly one memory, with address type `i32` and a declared maximum of at most `memory_pages` (§4.2). | WebAssembly 3.0, *Execution*, `memory.grow` (growth is non-deterministic, and fails past a declared maximum); *Binary Format*, *Types* (limits); §4.2 |
| R7 | both | defines at most one table, whose element type is `funcref` (`ref null func`, in either of its encodings), whose address type is `i32` and whose minimum equals its maximum, and contains no `table.grow`, `table.fill` or `table.set`. | WebAssembly 3.0, *Profiles*, *Defined Profiles* (`table.grow` remains non-deterministic under the deterministic profile); §5 |
| R8 | both | has no start section. | WebAssembly 3.0, *Binary Format*, *Modules* (the start section names a function that runs at instantiation); §6 check 12 (the guard covers `wai_run`, not instantiation) |
| R9 | both | gives no function type, local or global a reference type. | §5 (every value across the interface is an `i32`) |
| R10 | both | exports exactly the six exports of §5, each of the kind and type given there, and nothing else. | §5 |
| R11 | both | defines at most `functions` functions (§4.2). | WebAssembly 3.0, *Implementation Limitations*; §4.2 |
| R12 | both | contains none of these constructs of WebAssembly 3.0: exception handling (a tag section, `throw`, `throw_ref`, `try_table`); tail calls (`return_call`, `return_call_indirect`); typed function references (`call_ref`, `return_call_ref`, `ref.as_non_null`, `br_on_null`, `br_on_non_null`); and garbage-collected types and instructions (a type entry that is not a function type, among them a recursive or subtype declaration; `struct.*`, `array.*`, `ref.i31`, `i31.get_s`, `i31.get_u`, `ref.test`, `ref.cast`, `br_on_cast`, `br_on_cast_fail`, `any.convert_extern`, `extern.convert_any`, `ref.eq`). | §1 (the profile admits what a decoder module uses, so that a checker is small enough for two independent ones to agree on every module, §11) |
| R13 | both | after a `memory.grow` that fails, gives no output: within `wai_run` the call traps, and within `wai_alloc` it traps or returns 0. A module whose memory's minimum equals its maximum and which contains no `memory.grow` meets this rule. | WebAssembly 3.0, *Execution*, `memory.grow` (it may fail, pushing −1) and *Profiles* (growth remains non-deterministic under the deterministic profile); integer-operators §6 ("A refused decode outputs nothing") |
An instruction breaks R3 by what its opcode alone takes or gives. One whose operand or result
types are fixed elsewhere (a block, a typed `select`, a call, `local.get`, `drop`) breaks R3 only
through the value type that fixes them: an earlier item, or, for a block type or a typed
`select`, the value type that follows its opcode.
Rules R1 to R12 are about the module's bytes, and a checker decides them (§4.3). R13 is about
what the module does, and a conformance result attests it (§6, check 9c; §9.2). Custom sections
are part of the bytes, so the digest covers them; WebAssembly's semantics ignore them, and no
rule, check or sink of this text reads them.
### 4.2 Caps and validation limits
| cap | the profile's value | what it bounds |
|---|---|---|
| `module_bytes` | 16,777,216 | the module's length, in bytes |
| `functions` | 50,000 | the functions the module defines |
| `memory_pages` | 65,536 | the memory's declared maximum, in 64 KiB pages |
A sink **MAY** apply lower caps of its own. A module over a sink's caps is not held at that sink:
the caps change where a module is held, never what it outputs.
The **validation limits** are part of R2, and no sink changes them. WebAssembly 3.0 lets an
implementation limit the number and the size of a module's parts, so without fixed limits two
validators could differ on a module within the caps; a module beyond one of these is not valid
under this profile, and is `refused R2 -`.
| limit | value | what it bounds |
|---|---|---|
| types | 1,000,000 | the entries of the type section, and the types they define |
| functions, globals, tags | 1,000,000 each | those the module imports and defines, together |
| tables | 100,000 | the tables the module imports and defines, together |
| memories | 100 | the memories the module imports and defines, together |
| element segments, data segments | 100,000 each | the entries of the element section, and of the data section; and the data count section's count |
| segment items | 10,000,000 | the items of one element segment |
| name | 100,000 | the bytes of one name: an import's module or field, an export's, a custom section's |
| body | 7,654,321 | the bytes of one function body, after its size |
| locals | 50,000 | a function's parameters and the locals its body declares, together |
| parameters, results | 1,000 each | those of one function type |
| struct fields | 10,000 | those of one struct type |
| catches | 10,000 | the catch clauses of one `try_table` |
| subtype depth | 63 | a type's declared supertypes, followed to a type that declares none |
| interface | 999,998 | the sum, over every import and export, of 2 and the parameters and results of its type for a function or a tag, and of 1 for a table, a memory or a global; so a module has at most 999,998 imports and exports |
### 4.3 The verdict
A checker's verdict for a module at a level under caps is one line of ASCII: `held`, or
`refused R<n> <offset>`, with `<n>` the rule and `<offset>` a decimal byte offset into the
module, or `-`. It is a function of the module's bytes, the level and the caps, and it is
decided in this order:
1. R1: a module longer than `module_bytes` is `refused R1 0`, and is not read further.
2. R2: a module that does not decode, or is not valid, is `refused R2 -`. Decoders and
validators report such a failure at different offsets, so this verdict carries none.
3. R3 to R12, over the items of the module in binary order: the first item that breaks one of
them is refused at its offset, by the lowest-numbered rule it breaks. The offset of an
instruction is that of its first byte (for a prefixed opcode, the prefix); of a value type,
its first byte; of an entry or a type entry, its first byte; of a section, its id byte. R11
is broken by the function section; a table instruction that R7 refuses, by that instruction.
4. Then the rules an absence breaks, in rule order, at the offset equal to the module's length:
R6 where the module defines no memory, and R10 where an export of §5 is missing.
5. Otherwise `held`.
A module that breaks rules at several items is refused at the first; a sink reports that rule.
Since the levels differ only in R3, a module refused R3 at the integer level is checked at the
float level, and every other verdict is the same at both.
## 5. The module ABI
A module exports exactly these:
| export | kind and type | what it does |
|---|---|---|
| `memory` | the module's one memory | holds every buffer the sink passes in and reads out |
| `wai_abi` | function `() → i32` | returns `1`, the version of this interface |
| `wai_alloc` | function `(len: i32) → i32` | returns the offset of a region of `len` bytes the module will not otherwise use, or `0` where it cannot |
| `wai_run` | function `(cap_ptr: i32, cap_len: i32, in_ptr: i32, in_len: i32, set_ptr: i32, set_len: i32) → i32` | decodes one object; returns `0` when the output is the decoded medium, or `1` when it is a refusal code |
| `wai_out_ptr` | function `() → i32` | the offset of the output |
| `wai_out_len` | function `() → i32` | the output's length, in bytes |
A sink decodes an object through a module on an instance of its own: it instantiates the module
for that object, makes these calls once each, in this order, and discards the instance.
1. `wai_abi()`. A result other than `1` is `module_result_invalid`.
2. For each of three inputs, in this order: the capability, as the UTF-8 bytes of its term; the
payload, the bytes the envelope carries for that capability; and the set, the pinned parameter
set in its pin's form, which SPEC §3.1's checks 6–8 have held to its digest. The sink calls
`wai_alloc(len)` with the input's length and writes the input at the offset returned. A result
of `0` is `module_resources`. A capability that decodes against no set passes `0, 0` for it,
with no call.
3. `wai_run` with the three offsets and lengths, under the guard of §6 check 12.
4. `wai_out_ptr()` and `wai_out_len()`. A region that does not lie within the memory is
`module_result_invalid`.
5. Where `wai_run` returned `0`, the region is the decoded medium in its capability's canonical
buffer ([determinism-tiers](determinism-tiers.md) §2: canonical RGB8 for an image, int16 PCM,
the attribute tensor, a per-frame hash for video). Where it returned `1`, the region is a
refusal code in ASCII, one of the codes the text that defines the capability's payload lists
for its decode, and the decode is refused with that code, as that text routes it. Any other
result of `wai_run`, or a refusal text that is not such a code, is `module_result_invalid`.
Nothing else reaches the module: it imports nothing (R5), runs nothing at instantiation (R8), and
starts from its own bytes on every instance. So the output is a function of the capability, the
payload and the set. A decode that reads anything else, such as the decoded state of another
object, is not one this interface carries.
## 6. How a sink checks and runs a module
A sink that decodes an object through a module takes these steps in order and reports the first
that fails. A failure at steps 1 to 10 means the module is not held for the object: the capability
is unsupported for that envelope at that sink, and dispatch continues to the declared fallback or
a sibling rendition (jwp-receipts §7.9, *Fail closed*, *Fallback, never inert*). A failure at
steps 11 to 13 refuses the object's decode through the module, and dispatch continues the same
way; nothing is output.
**0. Identity.** The SHA-256 of the exact bytes the sink will instantiate (jwp-receipts §7.9,
*Identity*).
**1–8. Authorisation.** jwp-receipts §7.9's checks 1 to 8, unchanged.
**9. Profile.**
- **9a. The module:** rules R1 and R2.
- **9b. Its contents:** rules R3 to R12. The sink checks the module at the integer level, and,
where its verdict there is `refused R3`, at the float level. The module's level is the first
whose verdict is `held`. Otherwise the sink reports `module_profile_violation` with the
verdict of the last level it checked, its rule and its offset. A sink **MAY** keep the verdict
of 9a and 9b by the module's digest, its level and its caps, since nothing else decides it.
- **9c. Attestation.** The sink holds a `conform-result/1` record
([conformance-results](conformance-results.md) §2) that attests this module for the capability
being decoded: the record is admitted under conformance-results §4.1 against the module corpus
of §9.2 for that capability, as the sink holds it; its `kind` is `decoder` and its `suite` is
`module/` followed by the capability's term; an entry of its `implementation.files` has the
module's digest as its `sha256`; its `key` is `supplied`; and its `signer_pubkey` is a key the
grant's origin lists with `module/decoder`: the head jwp-receipts §7.4 step 3 reached for the
grant at jwp-receipts §7.9's check 3 lists an entry whose `key` is that `signer_pubkey`, which
is not `revoked`, carries no `pq_key` ([pq-signatures](pq-signatures.md) §6.1: a hybrid entry
signs nothing with Ed25519 alone, and a record has no other signature), holds `module/decoder` in its
`may_sign`, and, where it is `retired`, has an `until` no earlier than the record's
`started_at`, the two compared as jwp-receipts §7.4 compares times. Otherwise
`module_unattested`. The record carries no `signer_id`, so it is no item jwp-receipts §7.4
confirms: this check reads the head the grant was confirmed under, and nothing else of the
key log.
**10. Engine.**
- At the float level, where the object's need is above `none`: the sink's engine is set to the
deterministic profile's NaN rule (§7, `nan-canonical`), and the probe of §9.3, run in this
process on that engine and setting before the module's first run, gave the probe's bytes.
Otherwise `module_engine_not_deterministic` where the engine cannot be so set, and
`module_probe_mismatch` where the probe gave other bytes. Where the need is `none` this check
passes, and the output holds no tier.
- At the integer level: a sink **SHOULD** decode one vector of the capability's module corpus
(§9.2) once per engine and setting in each process, before the module's first run there, and
compare the output with the vector's digest. A difference is `module_probe_mismatch`. This
catches an engine that does not implement WebAssembly 3.0 as written; the level's semantics do
not need it.
**11. Instantiate** with an empty import object. A sink **SHOULD** reserve the memory's declared
maximum where its engine allows it. A failure to instantiate or to reserve is `module_resources`.
Then the calls of §5, steps 1 and 2.
**12. Run** `wai_run` under a guard: an instruction budget the engine counts, or a wall-clock
limit the sink enforces (§7). A trap, a stack exhausted among them, is `module_trap`; an
exhausted budget or limit is `module_timeout`. A sink whose engine reports that a `memory.grow`
failed refuses the run (`module_resources`) whatever the module then returns. Every sink also
relies on R13, which check 9c attests: a page cannot observe a failed grow. Availability can
differ between sinks; the output never does.
**13. Output.** §5's steps 4 and 5. The sink hashes the decoded medium (SHA-256), and its
receipt names the module as §10 states.
A module held at the integer level and run through steps 11 to 13 holds, for its output, what §2
gives that level; one held at the float level holds what §2 gives the float level, only after
check 10 passed with the object's need above `none`.
## 7. Engine settings
| term | the setting |
|---|---|
| `threads-off` | the engine refuses shared memory and atomic instructions |
| `relaxed-off` | the engine refuses relaxed vector instructions |
| `nan-canonical` | the engine gives every NaN a floating-point instruction generates as the positive canonical NaN, the deterministic profile's rule |
| `fuel` | the run is bounded by a budget of instructions the engine counts |
| `wall-clock` | the run is bounded by a wall-clock limit the sink enforces |
A sink, at either level:
- instantiates with an empty import object, and links no host interface;
- limits the memory's growth to the module's declared maximum, and its stack to a fixed size, the
same for every run;
- bounds every run of `wai_run` with `fuel` or `wall-clock`;
- **SHOULD** set `threads-off` and `relaxed-off` where its engine can be so set, as a second guard
behind R2 and R4.
At the float level a sink also sets `nan-canonical`, and check 10's probe shows it. A sink
**MUST NOT** take an engine setting that fixes the behaviour of relaxed vector instructions for
the deterministic profile: both levels refuse those instructions (R4), and only the probe shows
an engine's NaN behaviour. A page takes check 10 as failed: the output of a float-level module
in a page holds no tier, and a page decodes through one only an object whose need is `none`.
The **engine** a receipt names (§10) is written `<engine>@<version>`, optionally followed by
`/<compiler>`: `<engine>` and `<compiler>` are 1 to 64 of `a`–`z`, `0`–`9`, `_` and `-`, and
`<version>` is 1 to 64 of ASCII letters, digits, `.`, `+` and `-`, beginning with a digit. A
budget's instruction count is not energy, and no receipt states it.
## 8. Refusal codes
| code | raised at | then |
|---|---|---|
| `module_profile_violation` | §6 check 9a, 9b: with the rule and the offset of the verdict (§4.3) | the module is not held for the object |
| `module_unattested` | §6 check 9c | the module is not held for the object |
| `module_engine_not_deterministic` | §6 check 10 | the module is not held for an object whose need is above `none` |
| `module_probe_mismatch` | §6 check 10 | the module is not held for the object |
| `module_resources` | §6 check 11 (instantiation, reservation, `wai_alloc` returning `0`) and check 12 (a failed `memory.grow` the engine reports) | the object's decode through the module is refused |
| `module_trap` | §6 check 12 | the object's decode through the module is refused |
| `module_timeout` | §6 check 12 | the object's decode through the module is refused |
| `module_result_invalid` | §5 steps 1, 4 and 5 (§6 checks 11 and 13) | the object's decode through the module is refused |
In each case nothing is output, and dispatch continues as §6 states. A refusal the module returns
through `wai_run` is its capability's own, and routes as that capability's text routes it.
## 9. Corpora
### 9.1 The checker corpus
A conforming checker gives each module below the verdict stated, at the level and under the caps
stated. Each module is given by its construction: any bytes built as its row describes are that
module, and the offset in its verdict is that of the item the row names, in those bytes (§4.3).
Caps not stated are the profile's (§4.2).
**Planted modules.**
| case | level, caps | the module | verdict |
|---|---|---|---|
| `oversize` | both; `module_bytes` one below the module's length | `minimal-int`, unchanged | `refused R1 0` |
| `invalid` | both | a function whose body leaves an `i64` where its type returns `i32` | `refused R2 -` |
| `shared-memory` | both | a shared memory and an `i32.atomic.load` | `refused R2 -` |
| `component` | both | a component's preamble | `refused R2 -` |
| `scalar-float` | integer | `f32.add` of two `f32.const`s in `wai_run` | `refused R3`, at the first `f32.const` |
| `float-unreachable` | integer | `f32.add` and `drop` in `wai_run` after a `return`, where the operand stack is polymorphic and no earlier item gives a floating-point value | `refused R3`, at the `f32.add` |
| `float-block-type` | integer | a block in `wai_run` whose type is the result `f32`, holding only `unreachable`, its result dropped | `refused R3`, at the block type's value type |
| `float-select-type` | integer | a typed `select` whose type is `f32` in `wai_run` after a `return`, where the operand stack is polymorphic, its result dropped | `refused R3`, at its value type |
| `float-constant` | integer | a global initialised by `f64.const` | `refused R3`, at the global's value type |
| `float-signature` | integer | a function type with an `f64` parameter | `refused R3`, at that value type |
| `float-vector` | integer | `f32x4.add` | `refused R3`, at the instruction |
| `float-conversion` | integer | `f32x4.convert_i32x4_s` | `refused R3`, at the instruction |
| `float-truncation` | integer | `i32.trunc_sat_f32_s` on an `f32` built by `f32.reinterpret_i32` | `refused R3`, at `f32.reinterpret_i32` |
| `float-load` | integer | `f32.load` | `refused R3`, at the instruction |
| `relaxed-swizzle` | both | `i8x16.relaxed_swizzle` | `refused R4`, at the instruction |
| `relaxed-laneselect` | both | `i16x8.relaxed_laneselect` | `refused R4`, at the instruction |
| `relaxed-dot` | both | `i16x8.relaxed_dot_i8x16_i7x16_s` | `refused R4`, at the instruction |
| `relaxed-madd` | float | `f32x4.relaxed_madd` | `refused R4`, at the instruction |
| `import-function` | both | an imported function returning an `i32` (a clock) | `refused R5`, at the import |
| `import-memory` | both | its memory imported, not defined | `refused R5`, at the import; it breaks R6 too, which §4.3 reports only after every item |
| `import-global` | both | an imported immutable `i32` global | `refused R5`, at the import |
| `no-memory` | both | no memory: its memory, its export `memory` and the store in `wai_run` removed | `refused R6`, at the module's length; it breaks R10 too, which §4.3 reports after R6 |
| `two-memories` | both | a second memory | `refused R6`, at the second memory's entry |
| `memory64` | both | its memory of address type `i64`, and the store in `wai_run` addressed by an `i64` | `refused R6`, at the memory's entry |
| `no-maximum` | both | its memory with no maximum | `refused R6`, at the memory's entry |
| `over-pages` | both; `memory_pages` 16 | its memory's maximum 17 | `refused R6`, at the memory's entry |
| `two-tables` | both | two `funcref` tables, each with its minimum its maximum | `refused R7`, at the second table's entry |
| `externref-table` | both | a table of `externref`, its minimum its maximum | `refused R7`, at the table's entry |
| `table-unfixed` | both | a `funcref` table whose minimum is below its maximum | `refused R7`, at the table's entry |
| `table-grow` | both | a `funcref` table, its minimum its maximum, and `table.grow` | `refused R7`, at the instruction |
| `table-set` | both | the same table, and `table.set` | `refused R7`, at the instruction |
| `table-fill` | both | the same table, and `table.fill` | `refused R7`, at the instruction |
| `start` | both | a start section | `refused R8`, at the section's id byte |
| `funcref-parameter` | both | a function of the module, not exported, with a `funcref` parameter | `refused R9`, at that value type |
| `externref-global` | both | a global of type `externref` | `refused R9`, at its value type |
| `funcref-local` | both | a local of type `funcref` | `refused R9`, at its value type |
| `i64-export` | both | `wai_run` with its last parameter an `i64` | `refused R10`, at the export's entry |
| `extra-export` | both | a seventh export, a function | `refused R10`, at that export's entry |
| `exported-global` | both | an exported global | `refused R10`, at that export's entry |
| `missing-run` | both | no export `wai_run` | `refused R10`, at the module's length |
| `over-functions` | both; `functions` 8 | nine functions | `refused R11`, at the function section's id byte |
| `tail-call` | both | `return_call` | `refused R12`, at the instruction |
| `exception` | both | a tag section and `throw` | `refused R12`, at the tag section's id byte |
| `struct-type` | both | a struct type in the type section | `refused R12`, at that type entry |
| `call-ref` | both | `call_ref` of a `ref.func` naming `wai_abi`, which a declarative element segment declares | `refused R12`, at the instruction |
Every planted module but `component` is the module `minimal-int` (below) with the change
named, which breaks the rule named. Two of them, `import-memory` and `no-memory`, cannot break
it alone, and their rows say which other rule they break and why the verdict is the one stated.
Where a row adds an instruction, unless it says otherwise, the instruction is added to `wai_run`
before its store, its operands are `i32.const`s, `v128.const`s or `ref.null func`, as its type
takes, and a result it leaves is dropped. None of those is a floating-point item, so the
instruction is the first item of the module that breaks a rule. An instruction that takes a
floating-point operand has an earlier item that gives one, which §4.3 refuses first, except in
code the operand stack reaches as polymorphic, as `float-unreachable` places it.
**Conforming modules.**
| case | the module | verdict |
|---|---|---|
| `minimal-int` | the interface of §5 and nothing else: one memory of minimum 1 page and maximum 2; no table, global, data segment, element segment or custom section; `wai_abi` returns 1, `wai_alloc` returns 0, `wai_run` stores one fixed byte at offset 0 with `i32.store8` and returns 0, `wai_out_ptr` returns 0 and `wai_out_len` returns 1; no function reads a parameter | `held` at both levels |
| `vector-int` | `minimal-int` with `i32x4.dot_i16x8_s`, `i8x16.swizzle`, `i8x16.shuffle` and `i16x8.q15mulr_sat_s` | `held` at both levels |
| `bulk-and-sign` | `minimal-int` with `memory.copy`, `memory.fill`, `i32.extend8_s` and a block of two results | `held` at both levels |
| `fixed-table` | `minimal-int` with one `funcref` table, its minimum its maximum, an element segment and `call_indirect` | `held` at both levels |
| `fixed-memory` | `minimal-int` whose memory's minimum is its maximum, with no `memory.grow` | `held` at both levels |
| `custom-section` | `minimal-int` with a custom section whose bytes are the float level's identifier | `held` at both levels |
| `minimal-float` | `minimal-int` with `f64.add` of two `f64.const`s in `wai_run` | `held` at the float level; `refused R3` at the integer level, at the first `f64.const` |
R13 is not a checker's rule; §9.2's planted module breaks it.
### 9.2 The module corpus
The module corpus of a capability holds the cases a module that decodes it is attested on (§6,
check 9c):
- each committed vector and refusal fixture of the capability's conformance corpus, as the text
that defines its payload names that corpus: the module is given the vector's capability, payload
and set (§5), and the case expects the vector's output digest or its refusal code;
- for a module that contains `memory.grow`, the **grow-refusal cases**: for each vector `v`, and
each `k` from 1 to the number of `memory.grow` instructions the module executes decoding `v`,
the case `(v, k)`, in which the `k`-th of them fails and returns −1 and every other succeeds.
The case expects a refusal and no output: a trap, or `module_resources` where the failure was in
`wai_alloc`. A module whose memory's minimum equals its maximum and which contains no
`memory.grow` has none of these cases.
The planted module **`grow-swallowed`** meets R1 to R12 at the integer level, and, when a
`memory.grow` within `wai_run` fails, continues and returns `0` with an output. Its record fails
the grow-refusal case `(v, 1)` of any vector whose decode grows, so check 9c refuses it.
### 9.3 The probe
The probe is a module that meets R1 to R12 at the float level, and whose `wai_run`, for any
input, outputs the results of the cases below, in order: each result's bits in little-endian
order, four bytes for an `f32`, eight for an `f64`, and sixteen for a `v128`, lane 0 first. Each
input is written as its bits. A case's expected result is the one the deterministic profile
prescribes: the positive canonical NaN, `0x7fc00000` for `f32` and `0x7ff8000000000000` for
`f64`, in every lane.
| case | operation | operands |
|---|---|---|
| 1 | `f32.add` | `0xffa00001`, `0x3f800000` |
| 2 | `f32.mul` | `0xffa00001`, `0x40000000` |
| 3 | `f32.div` | `0x00000000`, `0x00000000` |
| 4 | `f32.sub` | `0x7f800000`, `0x7f800000` |
| 5 | `f32.sqrt` | `0xbf800000` |
| 6 | `f32.min` | `0xffa00001`, `0x3f800000` |
| 7 | `f32.nearest` | `0xffa00001` |
| 8 | `f32.demote_f64` | `0xfff4000000000001` |
| 9 | `f64.add` | `0xfff4000000000001`, `0x3ff0000000000000` |
| 10 | `f64.promote_f32` | `0xffa00001` |
| 11 | `f32x4.add` | lanes `0xffa00001`, `0x7fa00001`, `0xffc00000`, `0x7f800000`; lanes `0x3f800000`, `0x3f800000`, `0x3f800000`, `0xff800000` |
| 12 | `f64x2.mul` | lanes `0xfff4000000000001`, `0x7ff8000000000001`; lanes `0x4000000000000000`, `0x4000000000000000` |
The probe is about NaNs only. The deterministic profile's other rule, on relaxed vector
instructions, is unreachable from a module of either level (R4).
## 10. Receipts
A sink that records a `reconstruct-session` claim (jwp-receipts §2.4.12) of a decode through a
module writes, in that decoder entry, the module members of that section:
- `module_profile`: the identifier of the level the module was held at (§2);
- `engine`: the engine that ran it, written as §7 states;
- `engine_settings`: the terms of §7 the run was under, in ascending byte order, none twice;
- `module_probe`: `match` where check 10's probe, or at the integer level its vector, ran and
matched in this process, and `none` where none ran;
- `conform_result`: the SHA-256 of the RFC 8785 form, `sig` included, of the record check 9c
admitted.
A claim verifier that implements this profile checks them under jwp-receipts §2.4.12's rules 15
to 17. One that does not refuses an entry that carries them (`unknown_member`), as that section
states.
## 11. Conformance
- **This text.** Every rule of §4.1 names the clause of WebAssembly 3.0 or of WAI it rests on, and
§9.1, or for R13 §9.2, names at least one planted module that breaks that rule and no other,
with the verdict or the refusal it gets.
- **A conforming checker** gives every module of §9.1 the verdict stated there, and every module
the verdict §4.3 decides. A verdict is a function of the module's bytes, the level and the caps,
so two conforming checkers give every module the same verdict, byte for byte; a module on which
two checkers differ shows that one of them does not conform.
- **A conforming module** at a level gets `held` at that level from a conforming checker, and
meets R13.
- **A conforming sink** takes the steps of §6 in order for every object it decodes through a
module, with the settings of §7; reports the codes of §8; and names the module in its receipt as
§10 states. It states a tier for a module's output only as §2 and §6 give it.
## 12. What holding a module shows
That a sink holds a module at the integer level shows that the module's output is the same on
every engine that implements WebAssembly 3.0, or that there is none: a run that meets a limit is
refused, never output differently. At the float level it shows the same on every engine that
executes the deterministic profile's NaN rule. The record of check 9c shows that the module, on
its capability's corpus and its grow-refusal cases, gave what the corpus states. That the module
decodes every other input as its capability's text fixes is not something the profile shows: the
tier a sink states rests on the capability's registration, the grant and the record together.

2
wai/extensions/integer-operators.md
View file

@ -645,6 +645,8 @@ An implementation MUST NOT:
On a fabric whose shift instruction takes its amount modulo the register width, an implementation handles every shift of §5 that reaches or passes that width explicitly. A shift of a 32-bit value by 32 or more is an example.
On WebAssembly, a sink checks the first two of these "MUST NOT"s on the module it runs: a module held at the integer level of the deterministic module profile ([deterministic-modules](deterministic-modules.md) §6) contains no floating-point instruction and no relaxed vector instruction, and a run of it that traps or meets a limit outputs nothing.
## 7. Profiles
### 7.1 Width classes

88
wai/extensions/jwp-receipts.md
View file

@ -1046,6 +1046,28 @@ named only a pin the sink verified, may carry `pin` and `tier` `null` for an unp
decode that read a parameter set. A verifier cannot tell such an entry from one whose decode
read no set.
**Module members.** A decoder entry whose `decoder` is a `module:` decoder that ran under the
deterministic module profile ([deterministic-modules](deterministic-modules.md) §10) carries the
five members below, and every other entry carries none of them. A verifier that implements that
profile reads them: §3.1 step 2 does not report their absence (`missing_required_field`); where
they are present it reads them after `leaves`, and checks their types; and rules 15 to 17 check
their values. A verifier that does not implement it refuses an entry that carries any of them as
`unknown_member`, as one that does not implement pq-signatures refuses the hybrid members
(§2.4.3), and applies none of rules 15 to 17. An entry sealed by a sink of an earlier text of
this extension has none of them. Where such an entry is a `module:` entry whose `tier` is
`decode-equivalence`, it was valid under that text, and a verifier that implements the profile
refuses it under rule 16 (`session_module_profile_missing`): an earlier text let a sink state
that tier for a module's output with nothing of the module checked, and this one does not. Every
other entry sealed under an earlier text has the outcome it had.
| member | type | meaning |
|---|---|---|
| `module_profile` | term | The identifier of the level the module was held at ([deterministic-modules](deterministic-modules.md) §2). |
| `engine` | string | The engine that ran it, written as deterministic-modules §7 states. |
| `engine_settings` | array of terms | The settings of deterministic-modules §7 the run was under. |
| `module_probe` | string | `match` where deterministic-modules §6's check 10 ran its probe, or its vector, in the sink's process and the output matched; `none` where none ran. |
| `conform_result` | 32 B hex | The SHA-256 of the RFC 8785 form, `sig` included, of the `conform-result/1` record that attested the module ([conformance-results](conformance-results.md) §2; deterministic-modules §6, check 9c). |
`energy` is the decode energy of one completion of the presentations the claim commits
to — the decodes behind its `leaf_count` leaves, the work unit
[staged-measurement](staged-measurement.md) §8 names (its §8.1) — on the host's
@ -1104,6 +1126,20 @@ Rules, checked at §3.1 step 4 in this order:
(determinism-tiers §3, rule 2). Rules 6 and 13 already refuse such an entry for every
capability the registry classifies; this rule reaches the others, such as a capability
a module decodes.
15. A decoder entry's module members **MUST** be all five or none, and none on a
`builtin:` entry; `module_profile` **MUST** be one of the identifiers of
deterministic-modules §2, `engine` of the grammar of deterministic-modules §7,
`engine_settings` terms of that section's table in ascending byte order with none
twice, and `module_probe` `match` or `none` (`session_decoder_malformed`).
16. A `module:` decoder entry whose `tier` is `decode-equivalence` **MUST** carry the
module members, with `module_profile` the integer level's identifier
(`session_module_profile_missing`): a module's output holds that tier only at the
integer level (deterministic-modules §2).
17. A decoder entry whose `module_profile` is the float level's identifier, and whose
`tier` is neither `null` nor `none`, **MUST** have `nan-canonical` among its
`engine_settings` and `module_probe` `match`
(`session_module_engine_not_deterministic`): a float-level module's output holds a
tier only on an engine that passed the probe (deterministic-modules §6, check 10).
**Against the outputs** (§3.1 step 6). The context is the list of presentations, each
`{ "unit", "layers", "decoder", "out_digest" }`: a unit, the layers it was presented
@ -2305,7 +2341,7 @@ and never folds it in: confirmation changes the outcome of no step here.
| 4 | `session_leaf_sum` | the decoder entries' `leaves` do not sum to `leaf_count`, `leaf_count` is below `units`, or one of `units` and `leaf_count` is 0 and the other is not |
| 4 | `session_root_presence` | `output_root` is `null` with presentations, or a hash with none |
| 4 | `session_host_malformed` | the host's `threads` is not a power of two |
| 4 | `session_decoder_malformed` | a decoder entry's `decoder` is not of its grammar, its `rendition` is above 65535, its `tier` is present without `pin` or absent with it or is not a tier, its `module_status` does not fit its decoder, or its `leaves` is 0; or two entries differ only in `leaves` |
| 4 | `session_decoder_malformed` | a decoder entry's `decoder` is not of its grammar, its `rendition` is above 65535, its `tier` is present without `pin` or absent with it or is not a tier, its `module_status` does not fit its decoder, or its `leaves` is 0; or two entries differ only in `leaves`; or an entry's module members are not all five or none, are on a `builtin:` entry, or do not take the values rule 15 gives them |
| 4 | `session_tier_exceeds_class` | a decoder entry's `tier` exceeds its capability's class tier |
| 4 | `session_switch_invalid` | a switch between equal paths or for a reason delivery-telemetry §5 does not list, switches out of order, or other than `switches_total` written, 1024 where it is more |
| 4 | `session_missed_invalid` | `missed` above `leaf_count`, or not 0 with no deadline; `missed_units` holding other than `missed` entries, 256 where it is more, out of order, or an entry with `layers` 0 or above 65535 or `late_us` 0 |
@ -2314,6 +2350,8 @@ and never folds it in: confirmation changes the outcome of no step here.
| 4 | `session_classical_invalid` | `classical_source` present without `classical_declared` or absent with it, or not `wai2-table` |
| 4 | `session_variant_not_exact` | a decoder entry names a capability of the replicate class `neural-int-exact` and does not state an exact path: a `variant` other than `null`, `exact` or the lowering its registration names |
| 4 | `session_tier_exceeds_variant` | a decoder entry does not state an exact path, and its `tier` is `decode-equivalence` |
| 4 | `session_module_profile_missing` | a `module:` decoder entry whose `tier` is `decode-equivalence` does not name the integer level of the deterministic module profile |
| 4 | `session_module_engine_not_deterministic` | a decoder entry at the float level of the deterministic module profile, with a `tier` that is neither `null` nor `none`, lacks `nan-canonical` or a matching probe |
| 4 | `consumption_objects_unordered` | a `consumption` claim's `objects` are not in strictly ascending order ([ai-usage](ai-usage.md) §6.2) |
| 4 | `consumption_subject_mismatch` | its `subject` is not the first of its `objects` |
| 4 | `consumption_usage_unordered` | its `usage` entries are not in strictly ascending order of `vocabulary` |
@ -2821,10 +2859,14 @@ claim that fails §3.1 is declared rejected at its own step with its own
reason, and is never confirmed. `module` gives a module's bytes, a
grant, the sink's module origins, the revisions, anchors and statuses a
sink holds, the time, the capability being decoded and whether the
envelope leaves a fallback, and declares `run` with the kill latency,
or `fallback` or `inert` at a check of §7.9 with its reason; for a
envelope leaves a fallback, and declares `run` with the kill latency
where §7.9's checks 1 to 8 pass, or `fallback` or `inert` at one of
those checks with its reason; for a
pinned parameter set it may give no grant, and it adds the refusal SPEC
§3.1's check 5 reports. The corpus
§3.1's check 5 reports. The bytes its `module` vectors give are not
WebAssembly modules, and `module` runs neither of checks 9 and 10, which
are the deterministic module profile's: deterministic-modules §9 defines
their cases. The corpus
covers each rule of §7.2, the head walk with revisions that are not
held, unattached, injected, forked and superseded, each move of an
anchor, each step of §7.4 including the pinned-only authorities, the
@ -2832,7 +2874,7 @@ authorities a `measurement`, `operating-point`, `stage` or `delivery-gap`
claim needs, a family
receipt whose figures carry two classes,
instants compared across offsets, fractions and a leap second, and each
check of §7.9, with grants from an origin that is not one of the sink's
of §7.9's checks 1 to 8, with grants from an origin that is not one of the sink's
module origins, a grant whose `origin` is not the one its `signer_id`
names, a digest one module origin revokes and another grants, a status
signed under an injected revision, and a pinned parameter set whose
@ -2985,10 +3027,13 @@ arrived layers the session never received, and sessions presenting stages its ap
layers cannot have given — through layers it lists as late or refused among them — and
fewer than it counts; a base forgotten and decoded again (`staged-conformance/`'s
`record_budget`), accepted naming each epoch's claim and refused naming only the last;
every reason of §2.4.12's rules and
every reason of §2.4.12's rules 1 to 14 and of its
checks, the caps of the switches and missed presentations written at and past them; a
metered session's figure of zero (`energy_zero_figure`) and every acquisition-class
reason; and step 2's enumerations and order. The decode path an entry states has a
reason; and step 2's enumerations and order. No session in it carries the module members
of §2.4.12, and its two verifiers do not implement the deterministic module profile: each
refuses those members as `unknown_member` and applies none of rules 15 to 17, as §2.4.12
states for a verifier that does not implement that profile. The decode path an entry states has a
refusal for each of rules 13 and 14 and for a stage hash over a base or layer decoded at
a weaker tier or by a path that is not exact, beside accepted entries for each of
`wai.image.jpegai`'s two paths and for an integer path named by its registered lowering. `claim_verify.py` gives every outcome.
@ -3726,6 +3771,10 @@ its keys is that party is the origin's decision, and its log records it:
names; `module/reconstruct` lets it grant a reconstruct module (§7.9).
Neither is pinned-only; §7.8 says what a module authorised under a
fetched anchor is.
A key that holds `module/decoder` also signs the `conform-result/1` record that attests a
decoder module to the deterministic module profile ([deterministic-modules](deterministic-modules.md)
§6, check 9c). Such a record carries no `signer_id`, so it is no item §7.4 confirms: a sink
finds its key in the head that the module's grant was confirmed under (§7.9, check 3).
- **Rooms.** `live/room` lets a key act as a room authority: sign room descriptors and
the grants under them ([live-rooms](live-rooms.md) §5). It is not pinned-only, and it
is not `delivery`.
@ -4005,8 +4054,25 @@ fails:
(`module_grant_too_long`).
8. The capability being decoded is one of the grant's `capabilities`
(`module_capability_not_granted`).
9. Where the module is a decoder module the sink would run on a WebAssembly engine, it passes
the deterministic module profile's check 9 at one of its levels: its rules R1 to R12, and a
record that attests it, signed by a key that the head this grant was confirmed under lists
with `module/decoder`
([deterministic-modules](deterministic-modules.md) §6)
(`module_profile_violation`, `module_unattested`).
10. It passes that profile's check 10: where it passed check 9 at the float level and the
object's need (deterministic-modules §3) is above `none`, the sink's engine is set to the
deterministic profile's NaN rule and its probe matched; and, at either level, a probe the
sink ran for it matched (`module_engine_not_deterministic`, `module_probe_mismatch`).
`now` is the sink's trusted clock, as a log date-time. The checks are a
Checks 9 and 10 pass for a pinned parameter set, a reconstruct module and a decoder module the
sink runs on no WebAssembly engine, which are none of the modules they name. A decoder module the
sink would run on a WebAssembly engine is in their scope whatever its bytes: a component, or bytes
that do not decode as a WebAssembly module, fail check 9 (deterministic-modules §4.1, R2). A module
that passes every check is instantiated and run as deterministic-modules §6's checks 11 to 13
state.
`now` is the sink's trusted clock, as a log date-time. Checks 1 to 8 are a
function of the module's bytes, the grant, the sink's module origins,
the revisions, anchors and statuses the sink holds, and `now`, and read
no clock and no network of their own. A sink runs them before it instantiates a module, and again
@ -4074,7 +4140,7 @@ reported with the check and the reason — for a digest another origin
revokes, that origin — and with what dispatch did instead: fell back, or
left the file inert because no fallback was declared.
`key_log::module_check` in `wai-rs` implements these checks. The
`key_log::module_check` in `wai-rs` implements checks 1 to 8. The
reference dispatcher runs SPEC §3.1's check 5 when the sink is
configured with a key log (`key_log::SinkKeyLog`, given to
`pin::verify_with`, to `int_payload::resolve`, which runs it for a pinned
@ -4103,3 +4169,7 @@ module is revoked by its digest or through the key that granted it.
| 6 | `module_grant_expired` | `now` is later than `not_after` |
| 7 | `module_grant_too_long` | the grant's window exceeds the head's `grant_max_s` |
| 8 | `module_capability_not_granted` | the capability is not one the grant names |
| 9 | `module_profile_violation` | the module breaks a rule of the deterministic module profile at every level ([deterministic-modules](deterministic-modules.md) §4) |
| 9 | `module_unattested` | the sink holds no record that attests the module for the capability, signed by a key the grant's head lists with `module/decoder` (deterministic-modules §6, check 9c) |
| 10 | `module_engine_not_deterministic` | the module is at the float level, the object needs a tier, and the engine is not set to the deterministic profile's NaN rule |
| 10 | `module_probe_mismatch` | a probe the sink ran gave other bytes than deterministic-modules §6, check 10, expects |

2
wai/signer-conformance/README.md
View file

@ -51,7 +51,7 @@ sink's `module_origins` (each an `origin` and `source`), the `revisions`, `ancho
`statuses` the sink holds, its trusted clock (`now`, or `null` for none) and whether
the envelope leaves a `fallback`. It reports `run` with the granting key's origin,
key-id, head, anchor path, where its module origin came from (`expected=`) and
`kill_latency_s`, or `fallback` or `inert` at a §7.9 check with its reason; a digest
`kill_latency_s`, or `fallback` or `inert` at one of §7.9's checks 1 to 8 with its reason; a digest
another anchored origin revokes adds `revoked_by=<origin>`. A parameter set that is not
held adds the refusal SPEC §3.1's check 5 reports: `refusal=prior_revoked` where its
digest is revoked, `refusal=prior_not_authorised` for any other check. A parameter set

178
wai/wai-module-check/Cargo.lock generated Normal file
View file

@ -0,0 +1,178 @@
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
version = 4
[[package]]
name = "anyhow"
version = "1.0.104"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"
[[package]]
name = "arbitrary"
version = "1.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3bc62ac97cc33321f50863d514c3bc38a453947a8f9e781137e47c7401020aed"
dependencies = [
"derive_arbitrary",
]
[[package]]
name = "bitflags"
version = "2.13.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ded4057c258ba199e2d26386d3af3780957ecaee6c4ef4041c6b4b8b97c0b06"
[[package]]
name = "bumpalo"
version = "3.20.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649"
[[package]]
name = "derive_arbitrary"
version = "1.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1b034bd7d5f032402a2479444dcc6f74e36a03f31854d41680fb240ef682a1ac"
dependencies = [
"proc-macro2",
"quote",
"syn",
]
[[package]]
name = "equivalent"
version = "1.0.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "00d174d5400e5e8fd687ad1049e2f578285fa914201b1af7e8b112a4546bd826"
[[package]]
name = "flagset"
version = "0.4.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b7ac824320a75a52197e8f2d787f6a38b6718bb6897a35142d749af3c0e8f4fe"
[[package]]
name = "hashbrown"
version = "0.17.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a"
[[package]]
name = "indexmap"
version = "2.14.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cc4e190f5d26ca7051642629da2c52fc03bde85a03197c99408dcd291734c855"
dependencies = [
"equivalent",
"hashbrown",
]
[[package]]
name = "leb128fmt"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
[[package]]
name = "memchr"
version = "2.8.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98"
[[package]]
name = "proc-macro2"
version = "1.0.107"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
dependencies = [
"unicode-ident",
]
[[package]]
name = "quote"
version = "1.0.47"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
dependencies = [
"proc-macro2",
]
[[package]]
name = "syn"
version = "3.0.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d78c8dee4c7bf0e14673097256fed6142ce9d3b85a408189d07482442145823b"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "unicode-ident"
version = "1.0.27"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a2c754d6c33795a1c324727428e5a7dedb5b06195f9890bdbcba760d3e246563"
[[package]]
name = "unicode-width"
version = "0.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ca718471876992059f251e33aafc334346ada08042b7661dd1fe313a9bced557"
[[package]]
name = "wai-module-check"
version = "0.1.0"
dependencies = [
"arbitrary",
"wasm-smith",
"wasmparser",
"wast",
]
[[package]]
name = "wasm-encoder"
version = "0.262.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4495a6f85dd94c411c749303efcbc5defade0b0cbdbc0541495241ab917a9b5a"
dependencies = [
"leb128fmt",
"wasmparser",
]
[[package]]
name = "wasm-smith"
version = "0.262.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d59ba1915172128cdc0ef870cae157e539882a9605e591ef36d0d2e9cbb73505"
dependencies = [
"anyhow",
"arbitrary",
"flagset",
"wasm-encoder",
"wasmparser",
]
[[package]]
name = "wasmparser"
version = "0.262.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "974d643b125b272607e2fff8012ea14a8328acd7621e4bafa7afb32500052b1b"
dependencies = [
"bitflags",
"indexmap",
]
[[package]]
name = "wast"
version = "262.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "30612a0c29249b5f185888a107e8a519d920226b7d07f9d351fd094e9f75eb23"
dependencies = [
"bumpalo",
"leb128fmt",
"memchr",
"unicode-width",
"wasm-encoder",
]

29
wai/wai-module-check/Cargo.toml Normal file
View file

@ -0,0 +1,29 @@
[package]
name = "wai-module-check"
version = "0.1.0"
edition = "2021"
license = "Apache-2.0"
publish = false
description = "The checker of WAI's deterministic module profile (extensions/deterministic-modules.md): a module's verdict at the integer or the float level, from rules R1 to R12, on the WebAssembly validator of a pinned wasmparser."
[dependencies]
# Pinned exactly: R2's verdict is this validator's, and the profile's validation limits
# (deterministic-modules §4.2) are the ones it enforces. A new version is a reviewed change.
wasmparser = { version = "=0.262.0", default-features = false, features = ["std", "validate", "features", "simd"] }
[dev-dependencies]
# The differential (examples/differential.rs) generates its modules with wasm-smith, of the
# same release as the parser.
wasm-smith = { version = "=0.262.0", default-features = false, features = ["wasmparser"] }
arbitrary = "1"
# The specification's test scripts (examples/spectest.rs) are read by the text parser of
# the same release.
wast = { version = "=262.0.0", default-features = false, features = ["wasm-module"] }
[[example]]
name = "differential"
path = "examples/differential.rs"
[[example]]
name = "spectest"
path = "examples/spectest.rs"

1374
wai/wai-module-check/check-module.mjs Normal file
View file

File diff suppressed because it is too large Load diff

58
wai/wai-module-check/differential.mjs Normal file
View file

@ -0,0 +1,58 @@
// differential.mjs: the differential's second half. examples/differential.rs writes
// modules from wasm-smith and the Rust checker's verdicts; this runs check-module.mjs on
// every one at both levels, under the caps the Rust side used, and names each verdict
// that differs.
//
// node differential.mjs DIR
//
// DIR/verdicts.txt holds one line a module, `<name> <caps> <integer verdict> | <float
// verdict>`, the module being DIR/<name>.wasm: `<i>` for wasm-smith's i-th, `<i>-<k>` for a
// mutated copy of it, `<script>.<n>` for a module of the specification's tests
// (examples/spectest.rs). Prints each disagreement, then how the verdicts spread over held and
// the rules. Exit status 0 when every verdict agrees, 1 otherwise, 2 for an input error.
// No dependency.
import { readFileSync } from 'node:fs';
import { join } from 'node:path';
import { analyse, verdictOf, parseCaps } from './check-module.mjs';
const dir = process.argv[2];
if (!dir || process.argv.length !== 3) {
console.error('usage: node differential.mjs DIR');
process.exit(2);
}
let lines;
try {
lines = readFileSync(join(dir, 'verdicts.txt'), 'utf8').split('\n').filter(Boolean);
} catch (e) {
console.error(`differential: ${e.message}`);
process.exit(2);
}
const spread = new Map();
const count = (k) => spread.set(k, (spread.get(k) || 0) + 1);
let differ = 0, modules = 0;
for (const line of lines) {
const m = /^(\S+) (\S+) (.+) \| (.+)$/.exec(line);
const caps = m && parseCaps(m[2]);
if (!m || !caps) {
console.error(`differential: not a verdict line: ${line}`);
process.exit(2);
}
const bytes = new Uint8Array(readFileSync(join(dir, `${m[1]}.wasm`)));
const analysis = bytes.length > caps.module_bytes ? null : analyse(bytes);
modules++;
for (const [level, want] of [['integer', m[3]], ['float', m[4]]]) {
const got = verdictOf(analysis, bytes.length, level, caps);
const kind = m[1].includes('.') ? 'spec' : m[1].includes('-') ? 'mutated' : 'wasm-smith';
count(`${kind} ${level} ${want === 'held' ? 'held' : want.split(' ').slice(0, 2).join(' ')}`);
if (got !== want) {
differ++;
if (differ <= 50) console.log(`${m[1]}.wasm ${level} ${m[2]}: the Rust checker ${want}, check-module.mjs ${got}`);
}
}
}
for (const k of [...spread.keys()].sort()) console.log(` ${k}: ${spread.get(k)}`);
console.log(differ
? `differential: ${differ} verdicts of ${modules * 2} differ, over ${modules} modules`
: `differential: the two checkers agree on all ${modules * 2} verdicts of ${modules} modules`);
process.exit(differ ? 1 : 0);

312
wai/wai-module-check/examples/differential.rs Normal file
View file

@ -0,0 +1,312 @@
//! The differential's first half: modules from wasm-smith, and this checker's verdicts.
//!
//! cargo run --release --example differential -- --out DIR [--count N] [--mutants K] [--seed HEX]
//!
//! Writes `DIR/<i>.wasm` for i in 0..N (10,000 by default), K mutated copies of each
//! (`DIR/<i>-<k>.wasm`, 2 by default), and `DIR/verdicts.txt`, one line a module:
//! `<name> <caps> <integer verdict> | <float verdict>`. `differential.mjs DIR` then runs
//! check-module.mjs, the second checker, on every module at both levels under the same
//! caps, and names every verdict that differs.
//!
//! wasm-smith writes valid modules, or modules invalid in the ways it is told to be, so its
//! modules alone test how the two validators accept far more than how they refuse. Each
//! mutated copy changes one or two bytes of its module: a byte anywhere after the preamble
//! replaced, inserted or removed, or a byte of the code section replaced by a one-byte
//! opcode (`select`, `drop`, `end`, `ref.is_null`, ...). Most no longer decode or validate
//! (R2); the rest are other modules, which both checkers must give the same verdict.
//!
//! Each module is a function of the seed and its index alone. Its bytes come from a
//! splitmix64 stream seeded by both, read through wasm-smith's own `Config` and `Module`:
//!
//! - a quarter take wasm-smith's configuration as it comes, threads, the compact import
//! section and its other proposals included, so many are outside WebAssembly 3.0 (R2);
//! - a quarter are shaped toward the profile, each knob with its own chance: the exports
//! of minimal-int (§9.1) in name and type, no imports, one memory with a maximum, at most
//! one table, no start export;
//! - half are shaped to it, their exports minimal-int's or, for some, a planted module's
//! that differ in one export, and at most one knob turned the other way (imports, a
//! second memory, a start function, two tables, tags), so that most reach
//! the code section, where floats, relaxed vector instructions, exceptions, GC, tail calls
//! and reference types are each on or off; their verdicts spread over held and every rule;
//! - one in eight may hold an invalid function body, one in four over-long LEB128s, and one
//! in ten is checked under lower caps (one below its length, few functions, few pages).
//!
//! The seed is committed below; a run with another (`--seed`) is a new corpus.
use std::fmt::Write as _;
use std::path::PathBuf;
use arbitrary::{Arbitrary, Unstructured};
use wai_module_check::{check, Caps, Level};
use wasm_smith::{Config, Module};
/// The committed seed of the differential.
const SEED: u64 = 0x6465_742d_6d6f_6431;
/// The exports a profile-shaped module is given: minimal-int's, in name and type.
const INTERFACE: &[u8] = include_bytes!("../planted/minimal-int.wasm");
/// Other exports a module shaped to the profile may be given, each a planted module whose
/// exports are minimal-int's but for one: a fixed memory (held), and a 64-bit memory, a
/// memory with no maximum, an i64 parameter, a seventh export and an exported global.
const INTERFACES: [&[u8]; 6] = [
include_bytes!("../planted/fixed-memory.wasm"),
include_bytes!("../planted/memory64.wasm"),
include_bytes!("../planted/no-maximum.wasm"),
include_bytes!("../planted/i64-export.wasm"),
include_bytes!("../planted/extra-export.wasm"),
include_bytes!("../planted/exported-global.wasm"),
];
struct SplitMix(u64);
impl SplitMix {
fn next(&mut self) -> u64 {
self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15);
let mut z = self.0;
z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB);
z ^ (z >> 31)
}
fn bytes(&mut self, n: usize) -> Vec<u8> {
let mut out = Vec::with_capacity(n + 8);
while out.len() < n {
out.extend_from_slice(&self.next().to_le_bytes());
}
out.truncate(n);
out
}
/// True with chance `num` in `den`.
fn chance(&mut self, num: u64, den: u64) -> bool {
self.next() % den < num
}
}
fn shaped(cfg: &mut Config, r: &mut SplitMix) {
if r.chance(3, 4) {
cfg.exports = Some(INTERFACE.to_vec());
}
if r.chance(3, 4) {
cfg.max_imports = 0;
}
if r.chance(3, 4) {
cfg.min_memories = 1;
cfg.max_memories = 1;
cfg.memory_max_size_required = true;
cfg.max_memory32_bytes = 1 << (16 + r.next() % 8);
}
if r.chance(1, 2) {
cfg.memory64_enabled = false;
}
if r.chance(3, 4) {
cfg.max_tables = cfg.max_tables.min(1);
cfg.table_max_size_required = true;
}
if r.chance(3, 4) {
cfg.allow_start_export = false;
}
cfg.threads_enabled = r.chance(1, 10);
cfg.compact_imports_enabled = r.chance(1, 10);
cfg.allow_floats = r.chance(1, 2);
cfg.relaxed_simd_enabled = cfg.simd_enabled && r.chance(1, 4);
cfg.exceptions_enabled = r.chance(1, 4);
cfg.tail_call_enabled = r.chance(1, 4);
cfg.gc_enabled = cfg.reference_types_enabled && r.chance(1, 4);
}
fn strict(cfg: &mut Config, r: &mut SplitMix) {
// The exports bring the module's one memory; wasm-smith adds none of its own.
cfg.exports = Some(match r.next() % 16 {
k @ 0..=5 => INTERFACES[k as usize].to_vec(),
_ => INTERFACE.to_vec(),
});
cfg.max_imports = 0;
cfg.min_memories = 0;
cfg.max_memories = 0;
cfg.memory64_enabled = false;
cfg.max_tables = if r.chance(1, 2) { 0 } else { cfg.max_tables.min(1) };
cfg.table_max_size_required = true;
cfg.allow_start_export = false;
cfg.max_tags = 0;
cfg.threads_enabled = false;
cfg.compact_imports_enabled = false;
match r.next() % 10 {
0 => cfg.max_imports = 2,
1 => {
cfg.min_memories = 1;
cfg.max_memories = 1;
}
2 => cfg.allow_start_export = true,
3 => cfg.max_tables = 2,
4 => cfg.max_tags = 2,
_ => {}
}
if r.chance(1, 2) {
cfg.reference_types_enabled = false;
cfg.max_tables = cfg.max_tables.min(1);
}
cfg.allow_floats = r.chance(1, 2);
cfg.relaxed_simd_enabled = cfg.simd_enabled && r.chance(1, 3);
cfg.exceptions_enabled = r.chance(1, 4);
cfg.tail_call_enabled = r.chance(1, 4);
cfg.gc_enabled = cfg.reference_types_enabled && r.chance(1, 4);
}
fn generate(seed: u64, index: u64) -> (Vec<u8>, Caps) {
for attempt in 0u64.. {
let mut r = SplitMix(seed ^ index.wrapping_mul(0xA24B_AED4_963E_E407) ^ attempt.wrapping_mul(0x9FB2_1C65_1E98_DF25));
let shape = r.next() % 4;
let len = 1024 + (r.next() % 32_768) as usize;
let data = r.bytes(len);
let mut u = Unstructured::new(&data);
let Ok(mut cfg) = Config::arbitrary(&mut u) else { continue };
match shape {
0 => {
// Two more proposals outside WebAssembly 3.0, which wasm-smith's own choice
// leaves off.
cfg.custom_page_sizes_enabled = r.chance(1, 8);
cfg.wide_arithmetic_enabled = r.chance(1, 8);
}
1 => shaped(&mut cfg, &mut r),
_ => strict(&mut cfg, &mut r),
}
cfg.allow_invalid_funcs = r.chance(1, 8);
cfg.min_uleb_size = if r.chance(1, 4) { (1 + r.next() % 5) as u8 } else { 1 };
cfg.generate_custom_sections = r.chance(1, 4);
let Ok(module) = Module::new(cfg, &mut u) else { continue };
let bytes = module.to_bytes();
let mut caps = Caps::PROFILE;
if r.chance(1, 10) {
match r.next() % 3 {
0 => caps.module_bytes = (bytes.len() as u64).saturating_sub(r.next() % 2),
1 => caps.functions = r.next() % 8,
_ => caps.memory_pages = r.next() % 4,
}
}
return (bytes, caps);
}
unreachable!()
}
/// One-byte opcodes a mutation writes into a function body.
const OPCODES: [u8; 16] = [
0x00, 0x01, 0x0b, 0x0f, 0x1a, 0x1b, 0x45, 0x50, 0x6a, 0x71, 0xa7, 0xac, 0xd1, 0xd3, 0xd4, 0x0d,
];
/// The content of the code section, if the module has one: its start and end.
fn code_section(bytes: &[u8]) -> Option<(usize, usize)> {
let leb = |at: &mut usize| -> Option<usize> {
let (mut v, mut shift) = (0usize, 0);
loop {
let c = *bytes.get(*at)?;
*at += 1;
v |= usize::from(c & 0x7f) << shift;
if c & 0x80 == 0 {
return Some(v);
}
shift += 7;
if shift > 28 {
return None;
}
}
};
let mut at = 8;
while at < bytes.len() {
let id = bytes[at];
at += 1;
let size = leb(&mut at)?;
if id == 10 {
return Some((at, (at + size).min(bytes.len())));
}
at += size;
}
None
}
/// A copy of `bytes` with one or two edits.
fn mutate(bytes: &[u8], r: &mut SplitMix) -> Vec<u8> {
let mut out = bytes.to_vec();
for _ in 0..1 + r.next() % 2 {
if out.len() <= 8 {
break;
}
let anywhere = 8 + (r.next() as usize) % (out.len() - 8);
match r.next() % 8 {
0..=3 => out[anywhere] = r.next() as u8,
4 | 5 => match code_section(&out) {
Some((start, end)) if end > start => {
let at = start + (r.next() as usize) % (end - start);
out[at] = OPCODES[(r.next() % OPCODES.len() as u64) as usize];
}
_ => out[anywhere] = r.next() as u8,
},
6 => out.insert(anywhere, r.next() as u8),
_ => {
out.remove(anywhere);
}
}
}
out
}
fn caps_text(c: &Caps) -> String {
let mut parts = Vec::new();
if c.module_bytes != Caps::PROFILE.module_bytes {
parts.push(format!("module_bytes={}", c.module_bytes));
}
if c.functions != Caps::PROFILE.functions {
parts.push(format!("functions={}", c.functions));
}
if c.memory_pages != Caps::PROFILE.memory_pages {
parts.push(format!("memory_pages={}", c.memory_pages));
}
if parts.is_empty() {
"-".into()
} else {
parts.join(",")
}
}
fn main() {
let (mut out, mut count, mut mutants, mut seed) = (None, 10_000u64, 2u64, SEED);
let mut args = std::env::args().skip(1);
while let Some(a) = args.next() {
match a.as_str() {
"--out" => out = args.next().map(PathBuf::from),
"--count" => count = args.next().and_then(|n| n.parse().ok()).expect("--count N"),
"--mutants" => mutants = args.next().and_then(|n| n.parse().ok()).expect("--mutants K"),
"--seed" => {
seed = args
.next()
.and_then(|s| u64::from_str_radix(s.trim_start_matches("0x"), 16).ok())
.expect("--seed HEX")
}
_ => panic!("usage: differential --out DIR [--count N] [--mutants K] [--seed HEX]"),
}
}
let out = out.expect("--out DIR");
std::fs::create_dir_all(&out).expect("the output directory");
let mut lines = String::new();
let mut write = |name: String, bytes: &[u8], caps: &Caps| {
std::fs::write(out.join(format!("{name}.wasm")), bytes).expect("a module");
let int = check(bytes, Level::Integer, caps);
let float = check(bytes, Level::Float, caps);
writeln!(lines, "{name} {} {int} | {float}", caps_text(caps)).unwrap();
};
for i in 0..count {
let (bytes, caps) = generate(seed, i);
write(i.to_string(), &bytes, &caps);
let mut r = SplitMix(seed ^ i.wrapping_mul(0xD6E8_FEB8_6659_FD93) ^ 0x6d75_7461_6e74);
for k in 0..mutants {
write(format!("{i}-{k}"), &mutate(&bytes, &mut r), &caps);
}
}
std::fs::write(out.join("verdicts.txt"), lines).expect("verdicts.txt");
println!(
"differential: {count} modules and {} mutated copies from seed {seed:#018x} in {}",
count * mutants,
out.display()
);
}

112
wai/wai-module-check/examples/spectest.rs Normal file
View file

@ -0,0 +1,112 @@
//! The WebAssembly specification's tests as a third corpus for the differential.
//!
//! cargo run --release --example spectest -- --wast DIR --out DIR
//!
//! Reads every `.wast` file under `--wast` (the specification's `test/core`), and writes
//! each module its scripts define, assert invalid or assert malformed, in binary, to
//! `--out` as `<file>.<n>.wasm`, with this checker's verdicts in `verdicts.txt` in the form
//! differential.mjs reads (profile caps, both levels). A module given only as text that
//! does not parse is a test of the text format and is left out, as is a component.
//!
//! wasm-smith's modules test how two validators accept far more than how they refuse; the
//! specification's `assert_invalid` and `assert_malformed` modules are the refusals,
//! one construct at a time. It prints, for each of the script's expectations, how many of
//! its modules this checker refused by R2: a valid module refused is one that uses a
//! construct outside WebAssembly 3.0 or a part beyond a validation limit (§4.2), and an
//! invalid one not refused would be this validator's error.
use std::collections::BTreeMap;
use std::fmt::Write as _;
use std::path::{Path, PathBuf};
use wai_module_check::{check, Caps, Level, Verdict};
use wast::parser::{self, ParseBuffer};
use wast::{QuoteWat, Wast, WastDirective, Wat};
fn wast_files(dir: &Path, out: &mut Vec<PathBuf>) {
let mut entries: Vec<_> = std::fs::read_dir(dir).expect("the test directory").flatten().map(|e| e.path()).collect();
entries.sort();
for p in entries {
if p.is_dir() {
wast_files(&p, out);
} else if p.extension().is_some_and(|e| e == "wast") {
out.push(p);
}
}
}
/// Writes every module of one script; `None` where the script does not parse.
fn parse_script(
buf: &ParseBuffer<'_>,
stem: &str,
out: &Path,
caps: &Caps,
lines: &mut String,
tally: &mut BTreeMap<(&'static str, bool), u64>,
) -> Option<()> {
let script = parser::parse::<Wast>(buf).ok()?;
for (n, directive) in script.directives.into_iter().enumerate() {
let (mut module, expect) = match directive {
WastDirective::Module(m) | WastDirective::ModuleDefinition(m) => (m, "valid"),
WastDirective::AssertInvalid { module, .. } => (module, "invalid"),
WastDirective::AssertMalformed { module, .. } => (module, "malformed"),
_ => continue,
};
if matches!(module, QuoteWat::QuoteComponent(..) | QuoteWat::Wat(Wat::Component(_))) {
continue;
}
let Ok(bytes) = module.encode() else { continue };
let name = format!("{stem}.{n}");
std::fs::write(out.join(format!("{name}.wasm")), &bytes).expect("a module");
let int = check(&bytes, Level::Integer, caps);
let float = check(&bytes, Level::Float, caps);
writeln!(lines, "{name} - {int} | {float}").unwrap();
let r2 = matches!(int, Verdict::Refused { rule: 2, .. });
*tally.entry((expect, r2)).or_insert(0u64) += 1;
}
Some(())
}
fn main() {
let (mut wast_dir, mut out) = (None, None);
let mut args = std::env::args().skip(1);
while let Some(a) = args.next() {
match a.as_str() {
"--wast" => wast_dir = args.next().map(PathBuf::from),
"--out" => out = args.next().map(PathBuf::from),
_ => panic!("usage: spectest --wast DIR --out DIR"),
}
}
let (wast_dir, out) = (wast_dir.expect("--wast DIR"), out.expect("--out DIR"));
std::fs::create_dir_all(&out).expect("the output directory");
let mut files = Vec::new();
wast_files(&wast_dir, &mut files);
let caps = Caps::PROFILE;
let (mut lines, mut tally, mut unread) = (String::new(), BTreeMap::new(), 0);
for file in &files {
let stem = file
.strip_prefix(&wast_dir)
.unwrap_or(file)
.with_extension("")
.to_string_lossy()
.replace(['/', '\\'], "_");
let parsed = std::fs::read_to_string(file).ok().and_then(|text| {
let buf = ParseBuffer::new(&text).ok()?;
parse_script(&buf, &stem, &out, &caps, &mut lines, &mut tally)
});
if parsed.is_none() {
println!(" not read: {}", file.display());
unread += 1;
}
}
std::fs::write(out.join("verdicts.txt"), lines).expect("verdicts.txt");
for ((expect, r2), n) in &tally {
println!(" {expect}, {}: {n}", if *r2 { "refused R2" } else { "not refused R2" });
}
println!(
"spectest: {} modules from {} scripts in {} ({unread} scripts this parser does not read)",
tally.values().sum::<u64>(),
files.len(),
out.display()
);
}

744
wai/wai-module-check/planted/build.py Normal file
View file

@ -0,0 +1,744 @@
#!/usr/bin/env python3
"""build.py: the checker corpus of the deterministic module profile, built from source.
wai/extensions/deterministic-modules.md §9.1 gives each module of the checker corpus by its
construction: `minimal-int` and, for every other case but `component`, `minimal-int` with one
change. This script is that construction, byte by byte. It writes each module as
`<case>.wasm` beside itself, and `cases.txt`, the verdicts §9.1 states for them.
A verdict's offset is taken from the construction, never from a checker: each change marks
the item its row of §9.1 names (an instruction, a value type, an entry, a section's id byte)
as the bytes are put together, and the offset in `cases.txt` is where that mark lands in the
module. `at the module's length` is the module's length.
`cases.txt` has one line a verdict: `<case> <level> <caps> <verdict>`, where `<level>` is
`integer` or `float`, `<caps>` is `-` for the profile's caps (§4.2) or the caps the row
states, comma-joined `name=value`, and `<verdict>` is §4.3's line. A row of §9.1 at both
levels gives a line at each. Lines §9.1 does not state but §4.3 decides are marked
`# derived` after the verdict: the other level of a row that breaks only R3, and the
profile's caps for the rows that state lower ones. `grow-swallowed`, §9.2's planted module,
is here too: it meets R1 to R12, and R13, which it breaks, is no checker's rule.
python3 build.py write the modules and cases.txt
python3 build.py --check exit 1 unless the files here are exactly what it would write
python3 build.py --limits DIR write the validation limits' corpus to DIR (below)
The validation limits of §4.2 are part of R2. `--limits` writes, for each, `minimal-int`
with the part it bounds at the limit and one past it, and DIR/cases.txt in the same form:
at the limit the verdict is that of the rule the part breaks, if any (R12 for a tag section,
R10 for an extra export, held for unused globals); one past it, `refused R2 -`. These are
large modules (up to 10 MB), so they are generated where they are checked and are not
committed.
Standard library only.
"""
import os
import struct
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
# ------------------------------------------------------------------ bytes with marks
class Blob:
"""Bytes, with named offsets into them that follow the bytes when they are joined."""
def __init__(self, data=b"", marks=None):
self.data = bytes(data)
self.marks = dict(marks or {})
def __add__(self, other):
marks = dict(self.marks)
for k, v in other.marks.items():
assert k not in marks, k
marks[k] = v + len(self.data)
return Blob(self.data + other.data, marks)
def __len__(self):
return len(self.data)
def b(*xs):
return Blob(bytes(xs))
def cat(*blobs):
data, marks, at = [], {}, 0
for x in blobs:
for k, v in x.marks.items():
assert k not in marks, k
marks[k] = v + at
data.append(x.data)
at += len(x.data)
return Blob(b"".join(data), marks)
def mark(name, blob):
assert name not in blob.marks
return Blob(blob.data, {name: 0, **blob.marks})
def uleb(n):
out = bytearray()
while True:
c = n & 0x7F
n >>= 7
out.append(c | (0x80 if n else 0))
if not n:
return Blob(out)
def sleb(n):
out = bytearray()
while True:
c = n & 0x7F
n >>= 7
done = (n == 0 and not c & 0x40) or (n == -1 and c & 0x40)
out.append(c | (0 if done else 0x80))
if done:
return Blob(out)
def vec(items):
return uleb(len(items)) + cat(*items)
def name(s):
raw = s.encode("utf-8")
return uleb(len(raw)) + Blob(raw)
def sized(blob):
return uleb(len(blob)) + blob
# ------------------------------------------------------------------ encodings
I32, I64, F32, F64, V128 = 0x7F, 0x7E, 0x7D, 0x7C, 0x7B
FUNCREF, EXTERNREF = 0x70, 0x6F
END, DROP = 0x0B, 0x1A
def functype(params, results, item_param=None):
"""A function type; with `item_param`, the value type of that parameter is marked `item`."""
ps = [mark("item", b(t)) if i == item_param else b(t) for i, t in enumerate(params)]
return b(0x60) + vec(ps) + vec([b(t) for t in results])
def limits(minimum, maximum=None, i64=False):
flag = (0x04 if i64 else 0) | (0x01 if maximum is not None else 0)
out = b(flag) + uleb(minimum)
return out + uleb(maximum) if maximum is not None else out
def i32_const(n):
return b(0x41) + sleb(n)
def i64_const(n):
return b(0x42) + sleb(n)
def f32_const(x):
return b(0x43) + Blob(struct.pack("<f", x))
def f64_const(x):
return b(0x44) + Blob(struct.pack("<d", x))
def v128_const(lanes=bytes(16)):
return b(0xFD) + uleb(0x0C) + Blob(lanes)
def simd(op):
return b(0xFD) + uleb(op)
def memarg(align, offset=0):
return uleb(align) + uleb(offset)
def export(nm, kind, index):
return name(nm) + b(kind) + uleb(index)
def body(instrs, locals_=None):
"""A function body: its local declarations (none by default), then its instructions,
which end with `end`."""
return sized((locals_ if locals_ is not None else uleb(0)) + instrs)
def section(sid, content, tag=None):
head = b(sid)
if tag:
head = mark(tag, head)
return head + sized(content)
# ------------------------------------------------------------------ minimal-int
T_ABI, T_ALLOC, T_RUN = 0, 1, 2 # () -> i32, (i32) -> i32, (i32 x 6) -> i32
EXPORTS = ["memory", "wai_abi", "wai_alloc", "wai_run", "wai_out_ptr", "wai_out_len"]
def store_and_return(addr=None):
"""wai_run's own instructions: store one fixed byte at offset 0, return 0."""
return cat(addr or i32_const(0), i32_const(0x2A), b(0x3A), memarg(0), i32_const(0), b(END))
class Module:
"""minimal-int, as §9.1 states it, with every part open to a change."""
def __init__(self):
self.types = [functype([], [I32]), functype([I32], [I32]), functype([I32] * 6, [I32])]
self.imports = []
self.funcs = [T_ABI, T_ALLOC, T_RUN, T_ABI, T_ABI]
self.tables = []
self.memories = [limits(1, 2)]
self.tags = None
self.globals = []
self.exports = None # the six of §5 unless set
self.func_base = 0 # the index of the first defined function (after imports)
self.start = None
self.elems = None
self.run_prefix = Blob() # added to wai_run before its store
self.run_locals = None
self.run_rest = None # wai_run's instructions after the prefix, if changed
self.abi_body = cat(i32_const(1), b(END))
self.extra_bodies = [] # bodies of functions after the five
self.customs = []
self.datas = None
self.no_memory_export = False
self.drop_exports = set()
def default_exports(self):
out = []
for i, nm in enumerate(EXPORTS):
if nm in self.drop_exports or (nm == "memory" and self.no_memory_export):
continue
out.append(export(nm, 0x02, 0) if nm == "memory" else export(nm, 0x00, self.func_base + i - 1))
return out
def build(self):
exports = self.exports if self.exports is not None else self.default_exports()
run = self.run_prefix + (self.run_rest if self.run_rest is not None else store_and_return())
bodies = [
body(self.abi_body),
body(cat(i32_const(0), b(END))),
body(run, self.run_locals),
body(cat(i32_const(0), b(END))),
body(cat(i32_const(1), b(END))),
] + self.extra_bodies
parts = [Blob(b"\0asm") + Blob(struct.pack("<I", 1))]
parts.append(section(1, vec(self.types)))
if self.imports:
parts.append(section(2, vec(self.imports)))
parts.append(section(3, vec([uleb(t) for t in self.funcs]), "function-section"))
if self.tables:
parts.append(section(4, vec(self.tables)))
if self.memories:
parts.append(section(5, vec(self.memories)))
if self.tags is not None:
parts.append(section(13, vec(self.tags), "tag-section"))
if self.globals:
parts.append(section(6, vec(self.globals)))
parts.append(section(7, vec(exports)))
if self.start is not None:
parts.append(section(8, uleb(self.start), "start-section"))
if self.elems is not None:
parts.append(section(9, vec(self.elems)))
parts.append(section(10, vec(bodies)))
if self.datas is not None:
parts.append(section(11, vec(self.datas)))
for c in self.customs:
parts.append(section(0, c))
return cat(*parts)
# ------------------------------------------------------------------ the cases
def case_table():
"""(case, module blob, [(level, caps, verdict-spec, derived)]) for every case.
A verdict-spec is `held`, `R1`, `R2`, or (rule, mark) where mark names the item, or
`end` for the module's length."""
cases = []
BOTH = ("integer", "float")
def add(nm, blob, rows):
cases.append((nm, blob, rows))
def both(spec, caps="-"):
return [(lvl, caps, spec, False) for lvl in BOTH]
def int_only(spec):
return [("integer", "-", spec, False), ("float", "-", "held", True)]
m = Module()
minimal = m.build()
# -- planted
add("oversize", minimal, both("R1", f"module_bytes={len(minimal) - 1}")
+ [(lvl, "-", "held", True) for lvl in BOTH])
m = Module()
m.abi_body = cat(i64_const(1), b(END))
add("invalid", m.build(), both("R2"))
m = Module()
m.memories = [b(0x03) + uleb(1) + uleb(2)] # shared, with a maximum
m.run_prefix = cat(i32_const(0), b(0xFE) + uleb(0x10) + memarg(2), b(DROP)) # i32.atomic.load
add("shared-memory", m.build(), both("R2"))
add("component", Blob(b"\0asm") + Blob(bytes([0x0D, 0x00, 0x01, 0x00])), both("R2"))
m = Module()
m.run_prefix = cat(mark("item", f32_const(1.0)), f32_const(2.0), b(0x92), b(DROP))
add("scalar-float", m.build(), int_only(("R3", "item")))
m = Module()
m.run_prefix = cat(i32_const(0), b(0x0F), mark("item", b(0x92)), b(DROP))
add("float-unreachable", m.build(), int_only(("R3", "item")))
m = Module()
# block (result f32) unreachable end, its result dropped: the item is the block type.
m.run_prefix = cat(b(0x02), mark("item", b(F32)), b(0x00), b(END), b(DROP))
add("float-block-type", m.build(), int_only(("R3", "item")))
m = Module()
# return, then select (result f32) of a polymorphic stack: the item is its value type.
m.run_prefix = cat(i32_const(0), b(0x0F), i32_const(0), b(0x1C) + uleb(1), mark("item", b(F32)), b(DROP))
add("float-select-type", m.build(), int_only(("R3", "item")))
m = Module()
m.globals = [mark("item", b(F64)) + b(0x00) + f64_const(0.0) + b(END)]
add("float-constant", m.build(), int_only(("R3", "item")))
m = Module()
m.types.append(functype([F64], [], item_param=0))
add("float-signature", m.build(), int_only(("R3", "item")))
m = Module()
m.run_prefix = cat(v128_const(), v128_const(), mark("item", simd(0xE4)), b(DROP)) # f32x4.add
add("float-vector", m.build(), int_only(("R3", "item")))
m = Module()
m.run_prefix = cat(v128_const(), mark("item", simd(0xFA)), b(DROP)) # f32x4.convert_i32x4_s
add("float-conversion", m.build(), int_only(("R3", "item")))
m = Module()
# i32.trunc_sat_f32_s of f32.reinterpret_i32
m.run_prefix = cat(i32_const(0), mark("item", b(0xBE)), b(0xFC) + uleb(0), b(DROP))
add("float-truncation", m.build(), int_only(("R3", "item")))
m = Module()
m.run_prefix = cat(i32_const(0), mark("item", b(0x2A) + memarg(2)), b(DROP)) # f32.load
add("float-load", m.build(), int_only(("R3", "item")))
for nm, op, arity in [("relaxed-swizzle", 0x100, 2), ("relaxed-laneselect", 0x10A, 3),
("relaxed-dot", 0x112, 2)]:
m = Module()
m.run_prefix = cat(*[v128_const()] * arity, mark("item", simd(op)), b(DROP))
add(nm, m.build(), both(("R4", "item")))
m = Module()
m.run_prefix = cat(*[v128_const()] * 3, mark("item", simd(0x105)), b(DROP)) # f32x4.relaxed_madd
add("relaxed-madd", m.build(), [("float", "-", ("R4", "item"), False),
("integer", "-", ("R3", "item"), True)])
m = Module()
m.imports = [mark("item", name("env") + name("clock") + b(0x00) + uleb(T_ABI))]
m.func_base = 1
add("import-function", m.build(), both(("R5", "item")))
m = Module()
m.imports = [mark("item", name("env") + name("memory") + b(0x02) + limits(1, 2))]
m.memories = []
add("import-memory", m.build(), both(("R5", "item")))
m = Module()
m.imports = [mark("item", name("env") + name("g") + b(0x03) + b(I32, 0x00))]
add("import-global", m.build(), both(("R5", "item")))
m = Module()
m.memories = []
m.no_memory_export = True
m.run_rest = cat(i32_const(0), b(END))
add("no-memory", m.build(), both(("R6", "end")))
m = Module()
m.memories = [limits(1, 2), mark("item", limits(1, 2))]
add("two-memories", m.build(), both(("R6", "item")))
m = Module()
m.memories = [mark("item", limits(1, 2, i64=True))]
m.run_rest = store_and_return(addr=i64_const(0))
add("memory64", m.build(), both(("R6", "item")))
m = Module()
m.memories = [mark("item", limits(1))]
add("no-maximum", m.build(), both(("R6", "item")))
m = Module()
m.memories = [mark("item", limits(1, 17))]
add("over-pages", m.build(), both(("R6", "item"), "memory_pages=16")
+ [(lvl, "-", "held", True) for lvl in BOTH])
def fixed_table():
return b(FUNCREF) + limits(0, 0)
m = Module()
m.tables = [fixed_table(), mark("item", fixed_table())]
add("two-tables", m.build(), both(("R7", "item")))
m = Module()
m.tables = [mark("item", b(EXTERNREF) + limits(0, 0))]
add("externref-table", m.build(), both(("R7", "item")))
m = Module()
m.tables = [mark("item", b(FUNCREF) + limits(0, 1))]
add("table-unfixed", m.build(), both(("R7", "item")))
ref_null_func = b(0xD0, FUNCREF)
for nm, prefix in [
("table-grow", cat(ref_null_func, i32_const(0), mark("item", b(0xFC) + uleb(15) + uleb(0)), b(DROP))),
("table-set", cat(i32_const(0), ref_null_func, mark("item", b(0x26) + uleb(0)))),
("table-fill", cat(i32_const(0), ref_null_func, i32_const(0), mark("item", b(0xFC) + uleb(17) + uleb(0)))),
]:
m = Module()
m.tables = [fixed_table()]
m.run_prefix = prefix
add(nm, m.build(), both(("R7", "item")))
m = Module()
m.types.append(functype([], []))
m.funcs.append(3)
m.extra_bodies = [body(b(END))]
m.start = 5
add("start", m.build(), both(("R8", "start-section")))
m = Module()
m.types.append(functype([FUNCREF], [], item_param=0))
m.funcs.append(3)
m.extra_bodies = [body(b(END))]
add("funcref-parameter", m.build(), both(("R9", "item")))
m = Module()
m.globals = [mark("item", b(EXTERNREF)) + b(0x00) + b(0xD0, EXTERNREF) + b(END)]
add("externref-global", m.build(), both(("R9", "item")))
m = Module()
m.run_locals = uleb(1) + uleb(1) + mark("item", b(FUNCREF))
add("funcref-local", m.build(), both(("R9", "item")))
m = Module()
m.types[T_RUN] = functype([I32] * 5 + [I64], [I32])
ex = m.default_exports()
ex[3] = mark("item", ex[3])
m.exports = ex
add("i64-export", m.build(), both(("R10", "item")))
m = Module()
m.exports = m.default_exports() + [mark("item", export("wai_extra", 0x00, 0))]
add("extra-export", m.build(), both(("R10", "item")))
m = Module()
m.globals = [b(I32, 0x00) + i32_const(0) + b(END)]
m.exports = m.default_exports() + [mark("item", export("wai_global", 0x03, 0))]
add("exported-global", m.build(), both(("R10", "item")))
m = Module()
m.drop_exports = {"wai_run"}
add("missing-run", m.build(), both(("R10", "end")))
m = Module()
m.funcs += [T_ABI] * 4
m.extra_bodies = [body(cat(i32_const(0), b(END)))] * 4
add("over-functions", m.build(), both(("R11", "function-section"), "functions=8")
+ [(lvl, "-", "held", True) for lvl in BOTH])
m = Module()
m.run_prefix = mark("item", b(0x12) + uleb(0)) # return_call wai_abi
add("tail-call", m.build(), both(("R12", "item")))
m = Module()
m.types.append(functype([], []))
m.tags = [b(0x00) + uleb(3)]
m.run_prefix = b(0x08) + uleb(0) # throw 0
add("exception", m.build(), both(("R12", "tag-section")))
m = Module()
m.types.append(mark("item", b(0x5F) + uleb(0))) # a struct type, no fields
add("struct-type", m.build(), both(("R12", "item")))
m = Module()
m.elems = [uleb(3) + b(0x00) + vec([uleb(0)])] # declarative: wai_abi
m.run_prefix = cat(b(0xD2) + uleb(0), mark("item", b(0x14) + uleb(T_ABI)), b(DROP))
add("call-ref", m.build(), both(("R12", "item")))
# -- conforming
add("minimal-int", minimal, both("held"))
m = Module()
m.run_prefix = cat(
v128_const(), v128_const(), simd(0xBA), b(DROP), # i32x4.dot_i16x8_s
v128_const(), v128_const(), simd(0x0E), b(DROP), # i8x16.swizzle
v128_const(), v128_const(), simd(0x0D) + Blob(bytes(range(16))), b(DROP), # i8x16.shuffle
v128_const(), v128_const(), simd(0x82), b(DROP), # i16x8.q15mulr_sat_s
)
add("vector-int", m.build(), both("held"))
m = Module()
m.types.append(functype([], [I32, I32]))
m.run_prefix = cat(
i32_const(0), i32_const(0), i32_const(0), b(0xFC) + uleb(10) + uleb(0) + uleb(0), # memory.copy
i32_const(0), i32_const(0), i32_const(0), b(0xFC) + uleb(11) + uleb(0), # memory.fill
i32_const(0), b(0xC0), b(DROP), # i32.extend8_s
b(0x02) + sleb(3), i32_const(1), i32_const(2), b(END), b(DROP), b(DROP), # a block of two results
)
add("bulk-and-sign", m.build(), both("held"))
m = Module()
m.tables = [b(FUNCREF) + limits(1, 1)]
m.elems = [uleb(0) + i32_const(0) + b(END) + vec([uleb(0)])]
m.run_prefix = cat(i32_const(0), b(0x11) + uleb(T_ABI) + uleb(0), b(DROP)) # call_indirect
add("fixed-table", m.build(), both("held"))
m = Module()
m.memories = [limits(1, 1)]
add("fixed-memory", m.build(), both("held"))
m = Module()
m.customs = [name("profile") + Blob(b"det-module/1-det")]
add("custom-section", m.build(), both("held"))
m = Module()
m.run_prefix = cat(mark("item", f64_const(1.0)), f64_const(2.0), b(0xA0), b(DROP))
add("minimal-float", m.build(), [("float", "-", "held", False), ("integer", "-", ("R3", "item"), False)])
# -- §9.2: breaks R13 only, which no checker decides
m = Module()
m.run_prefix = cat(i32_const(1), b(0x40) + uleb(0), b(DROP)) # memory.grow 1, result dropped
add("grow-swallowed", m.build(), both("held"))
return cases
def verdict(spec, blob):
if spec == "held":
return "held"
if spec == "R1":
return "refused R1 0"
if spec == "R2":
return "refused R2 -"
rule, where = spec
at = len(blob) if where == "end" else blob.marks[where]
return f"refused {rule} {at}"
def outputs():
files = {}
lines = [
"# The checker corpus of deterministic-modules.md §9.1, and §9.2's grow-swallowed,",
"# written by build.py: `<case> <level> <caps> <verdict>`, one line a verdict.",
]
for nm, blob, rows in case_table():
files[f"{nm}.wasm"] = blob.data
for level, caps, spec, derived in rows:
line = f"{nm} {level} {caps} {verdict(spec, blob)}"
lines.append(line + (" # derived" if derived else ""))
files["cases.txt"] = ("\n".join(lines) + "\n").encode("utf-8")
return files
def limit_cases():
"""(case, blob, verdict-spec) for each validation limit of §4.2, at it and one past it."""
out = []
nop_type = functype([], [])
def both(nm, at_limit, past, spec):
out.append((f"{nm}-at-limit", at_limit, spec))
out.append((f"{nm}-past-limit", past, "R2"))
def module(change):
m = Module()
change(m)
return m.build()
# types: entries of the type section, and the types they define
def plain_types(n):
return lambda m: m.types.extend([nop_type] * (n - 3))
both("types", module(plain_types(1_000_000)), module(plain_types(1_000_001)), "held")
def empty_groups(n):
def change(m):
m.types.append(mark("item", b(0x4E) + uleb(0)))
m.types.extend([b(0x4E) + uleb(0)] * (n - 4))
return change
both("type-entries", module(empty_groups(1_000_000)), module(empty_groups(1_000_001)), ("R12", "item"))
def one_group(n):
return lambda m: m.types.append(mark("item", b(0x4E) + vec([nop_type] * (n - 3))))
both("types-in-a-group", module(one_group(1_000_000)), module(one_group(1_000_001)), ("R12", "item"))
def functions(n):
def change(m):
m.funcs += [T_ABI] * (n - 5)
m.extra_bodies = [body(cat(i32_const(0), b(END)))] * (n - 5)
return change
both("functions", module(functions(1_000_000)), module(functions(1_000_001)), ("R11", "function-section"))
def globals(n):
return lambda m: m.globals.extend([b(I32, 0x00) + i32_const(0) + b(END)] * n)
both("globals", module(globals(1_000_000)), module(globals(1_000_001)), "held")
def tags(n):
def change(m):
m.types.append(nop_type)
m.tags = [b(0x00) + uleb(3)] * n
return change
both("tags", module(tags(1_000_000)), module(tags(1_000_001)), ("R12", "tag-section"))
def tables(n):
return lambda m: m.tables.extend([b(FUNCREF) + limits(0, 0), mark("item", b(FUNCREF) + limits(0, 0))]
+ [b(FUNCREF) + limits(0, 0)] * (n - 2))
both("tables", module(tables(100_000)), module(tables(100_001)), ("R7", "item"))
def memories(n):
return lambda m: m.memories.extend([mark("item", limits(1, 2))] + [limits(1, 2)] * (n - 2))
both("memories", module(memories(100)), module(memories(101)), ("R6", "item"))
def elements(n):
return lambda m: setattr(m, "elems", [uleb(1) + b(0x00) + uleb(0)] * n)
both("element-segments", module(elements(100_000)), module(elements(100_001)), "held")
def datas(n):
return lambda m: setattr(m, "datas", [uleb(1) + uleb(0)] * n)
both("data-segments", module(datas(100_000)), module(datas(100_001)), "held")
def items(n):
return lambda m: setattr(m, "elems", [uleb(1) + b(0x00) + uleb(n) + Blob(bytes(n))])
both("segment-items", module(items(10_000_000)), module(items(10_000_001)), "held")
def export_name(n):
return lambda m: setattr(m, "exports", m.default_exports() + [mark("item", export("x" * n, 0x00, 0))])
both("name-of-an-export", module(export_name(100_000)), module(export_name(100_001)), ("R10", "item"))
def import_name(n):
def change(m):
m.imports = [mark("item", name("env") + name("g" * n) + b(0x03) + b(I32, 0x00))]
return change
both("name-of-an-import", module(import_name(100_000)), module(import_name(100_001)), ("R5", "item"))
def custom_name(n):
return lambda m: setattr(m, "customs", [name("c" * n)])
both("name-of-a-custom-section", module(custom_name(100_000)), module(custom_name(100_001)), "held")
def body_bytes(n):
# wai_run's body: its declaration of no locals (1 byte), nops, then its own 13 bytes.
def change(m):
m.run_prefix = Blob(b"\x01" * (n - 1 - len(store_and_return())))
return change
both("body", module(body_bytes(7_654_321)), module(body_bytes(7_654_322)), "held")
def locals_(n):
# wai_run's six parameters and n - 6 locals.
return lambda m: setattr(m, "run_locals", uleb(1) + uleb(n - 6) + b(I32))
both("locals", module(locals_(50_000)), module(locals_(50_001)), "held")
def params(n):
return lambda m: m.types.append(functype([I32] * n, []))
both("parameters", module(params(1_000)), module(params(1_001)), "held")
def results(n):
return lambda m: m.types.append(functype([], [I32] * n))
both("results", module(results(1_000)), module(results(1_001)), "held")
def fields(n):
return lambda m: m.types.append(mark("item", b(0x5F) + vec([b(I32, 0x00)] * n)))
both("struct-fields", module(fields(10_000)), module(fields(10_001)), ("R12", "item"))
def catches(n):
# A block, and in it a try_table whose catch_all clauses all name the block.
return lambda m: setattr(m, "run_prefix", cat(
b(0x02, 0x40), mark("item", b(0x1F, 0x40)), uleb(n), Blob(b"\x02\x00" * n), b(END), b(END)))
both("catches", module(catches(10_000)), module(catches(10_001)), ("R12", "item"))
def depth(d):
# A chain of struct subtypes: the first declares no supertype (depth 0), each next
# names the one before.
def change(m):
m.types.append(mark("item", b(0x50) + uleb(0) + b(0x5F) + uleb(0)))
for k in range(1, d + 1):
m.types.append(b(0x50) + uleb(1) + uleb(3 + k - 1) + b(0x5F) + uleb(0))
return change
both("subtype-depth", module(depth(63)), module(depth(64)), ("R12", "item"))
def interface(total):
# The six exports of §5 weigh 23 (memory 1; wai_abi, wai_out_ptr, wai_out_len 3 each;
# wai_alloc 4; wai_run 9); each further export of the memory weighs 1.
def change(m):
extra = total - 23
names = [f"m{i:x}" for i in range(extra)]
ex = m.default_exports()
ex.append(mark("item", export(names[0], 0x02, 0)))
ex.extend(export(nm, 0x02, 0) for nm in names[1:])
m.exports = ex
return change
both("interface", module(interface(999_998)), module(interface(999_999)), ("R10", "item"))
return out
def write_limits(directory):
os.makedirs(directory, exist_ok=True)
lines = ["# The validation limits of deterministic-modules.md §4.2, written by build.py --limits."]
for nm, blob, spec in limit_cases():
assert len(blob) <= 16_777_216, nm
with open(os.path.join(directory, f"{nm}.wasm"), "wb") as f:
f.write(blob.data)
for level in ("integer", "float"):
lines.append(f"{nm} {level} - {verdict(spec, blob)}")
with open(os.path.join(directory, "cases.txt"), "w", encoding="utf-8") as f:
f.write("\n".join(lines) + "\n")
print(f"build.py: wrote {len(lines) - 1} verdicts of the validation limits to {directory}")
return 0
def main(argv):
if len(argv) == 3 and argv[1] == "--limits":
return write_limits(argv[2])
check = argv[1:] == ["--check"]
if argv[1:] and not check:
print("usage: build.py [--check | --limits DIR]", file=sys.stderr)
return 2
want = outputs()
have = {n for n in os.listdir(HERE) if n.endswith(".wasm") or n == "cases.txt"}
if check:
bad = []
for n, data in sorted(want.items()):
p = os.path.join(HERE, n)
if not os.path.isfile(p):
bad.append(f"{n}: missing")
elif open(p, "rb").read() != data:
bad.append(f"{n}: differs from what build.py writes")
bad += [f"{n}: not written by build.py" for n in sorted(have - set(want))]
for line in bad:
print(f"build.py --check: {line}", file=sys.stderr)
if not bad:
print(f"build.py --check: {len(want) - 1} modules and cases.txt are what build.py writes")
return 1 if bad else 0
for n in sorted(have - set(want)):
os.remove(os.path.join(HERE, n))
for n, data in want.items():
with open(os.path.join(HERE, n), "wb") as f:
f.write(data)
print(f"build.py: wrote {len(want) - 1} modules and cases.txt")
return 0
if __name__ == "__main__":
sys.exit(main(sys.argv))

BIN
wai/wai-module-check/planted/bulk-and-sign.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/call-ref.wasm Normal file
View file

Binary file not shown.

114
wai/wai-module-check/planted/cases.txt Normal file
View file

@ -0,0 +1,114 @@
# The checker corpus of deterministic-modules.md §9.1, and §9.2's grow-swallowed,
# written by build.py: `<case> <level> <caps> <verdict>`, one line a verdict.
oversize integer module_bytes=150 refused R1 0
oversize float module_bytes=150 refused R1 0
oversize integer - held # derived
oversize float - held # derived
invalid integer - refused R2 -
invalid float - refused R2 -
shared-memory integer - refused R2 -
shared-memory float - refused R2 -
component integer - refused R2 -
component float - refused R2 -
scalar-float integer - refused R3 131
scalar-float float - held # derived
float-unreachable integer - refused R3 134
float-unreachable float - held # derived
float-block-type integer - refused R3 132
float-block-type float - held # derived
float-select-type integer - refused R3 138
float-select-type float - held # derived
float-constant integer - refused R3 47
float-constant float - held # derived
float-signature integer - refused R3 32
float-signature float - held # derived
float-vector integer - refused R3 167
float-vector float - held # derived
float-conversion integer - refused R3 149
float-conversion float - held # derived
float-truncation integer - refused R3 133
float-truncation float - held # derived
float-load integer - refused R3 133
float-load float - held # derived
relaxed-swizzle integer - refused R4 167
relaxed-swizzle float - refused R4 167
relaxed-laneselect integer - refused R4 185
relaxed-laneselect float - refused R4 185
relaxed-dot integer - refused R4 167
relaxed-dot float - refused R4 167
relaxed-madd float - refused R4 185
relaxed-madd integer - refused R3 185 # derived
import-function integer - refused R5 33
import-function float - refused R5 33
import-memory integer - refused R5 33
import-memory float - refused R5 33
import-global integer - refused R5 33
import-global float - refused R5 33
no-memory integer - refused R6 129
no-memory float - refused R6 129
two-memories integer - refused R6 44
two-memories float - refused R6 44
memory64 integer - refused R6 41
memory64 float - refused R6 41
no-maximum integer - refused R6 41
no-maximum float - refused R6 41
over-pages integer memory_pages=16 refused R6 41
over-pages float memory_pages=16 refused R6 41
over-pages integer - held # derived
over-pages float - held # derived
two-tables integer - refused R7 45
two-tables float - refused R7 45
externref-table integer - refused R7 41
externref-table float - refused R7 41
table-unfixed integer - refused R7 41
table-unfixed float - refused R7 41
table-grow integer - refused R7 142
table-grow float - refused R7 142
table-set integer - refused R7 142
table-set float - refused R7 142
table-fill integer - refused R7 144
table-fill float - refused R7 144
start integer - refused R8 120
start float - refused R8 120
funcref-parameter integer - refused R9 32
funcref-parameter float - refused R9 32
externref-global integer - refused R9 47
externref-global float - refused R9 47
funcref-local integer - refused R9 132
funcref-local float - refused R9 132
i64-export integer - refused R10 78
i64-export float - refused R10 78
extra-export integer - refused R10 116
extra-export float - refused R10 116
exported-global integer - refused R10 124
exported-global float - refused R10 124
missing-run integer - refused R10 141
missing-run float - refused R10 141
over-functions integer functions=8 refused R11 30
over-functions float functions=8 refused R11 30
over-functions integer - held # derived
over-functions float - held # derived
tail-call integer - refused R12 131
tail-call float - refused R12 131
exception integer - refused R12 47
exception float - refused R12 47
struct-type integer - refused R12 30
struct-type float - refused R12 30
call-ref integer - refused R12 140
call-ref float - refused R12 140
minimal-int integer - held
minimal-int float - held
vector-int integer - held
vector-int float - held
bulk-and-sign integer - held
bulk-and-sign float - held
fixed-table integer - held
fixed-table float - held
fixed-memory integer - held
fixed-memory float - held
custom-section integer - held
custom-section float - held
minimal-float float - held
minimal-float integer - refused R3 131
grow-swallowed integer - held
grow-swallowed float - held

BIN
wai/wai-module-check/planted/component.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/custom-section.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/exception.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/exported-global.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/externref-global.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/externref-table.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/extra-export.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/fixed-memory.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/fixed-table.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-block-type.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-constant.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-conversion.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-load.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-select-type.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-signature.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-truncation.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-unreachable.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/float-vector.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/funcref-local.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/funcref-parameter.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/grow-swallowed.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/i64-export.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/import-function.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/import-global.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/import-memory.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/invalid.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/memory64.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/minimal-float.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/minimal-int.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/missing-run.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/no-maximum.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/no-memory.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/over-functions.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/over-pages.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/oversize.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/relaxed-dot.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/relaxed-laneselect.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/relaxed-madd.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/relaxed-swizzle.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/scalar-float.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/shared-memory.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/start.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/struct-type.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/table-fill.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/table-grow.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/table-set.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/table-unfixed.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/tail-call.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/two-memories.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/two-tables.wasm Normal file
View file

Binary file not shown.

BIN
wai/wai-module-check/planted/vector-int.wasm Normal file
View file

Binary file not shown.

623
wai/wai-module-check/src/lib.rs Normal file
View file

@ -0,0 +1,623 @@
//! The checker of WAI's deterministic module profile
//! (`wai/extensions/deterministic-modules.md`).
//!
//! A module's verdict at a level under caps is one line of ASCII, `held` or
//! `refused R<n> <offset>` (§4.3), decided in this order:
//!
//! 1. R1, the module's length against `module_bytes`.
//! 2. R2, the module as WebAssembly 3.0: it decodes and is valid, within the profile's
//! validation limits (§4.2). wasmparser's validator decides it, with the features of
//! WebAssembly 3.0 and no others ([`features`]); its limits are the profile's.
//! 3. R3 to R12, over the items of the module in binary order: the first item that breaks
//! one is refused at its offset, by the lowest-numbered rule it breaks.
//! 4. The rules an absence breaks, at the module's length: R6 (no memory), then R10 (an
//! export of §5 missing).
//!
//! The levels differ only in R3, which the float level does not apply.
use std::fmt;
use wasmparser::{
BinaryReader, BlockType, CompositeInnerType, DataKind, ElementItems, ElementKind,
ExternalKind, Imports, Operator, OperatorsReader, Parser, Payload, RefType, TableInit,
TypeRef, ValType, Validator, WasmFeatures,
};
/// The two levels of §2.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Level {
/// `det-module/1-int`: R3 applies.
Integer,
/// `det-module/1-det`: R3 does not.
Float,
}
impl Level {
/// The level's identifier (§2).
pub fn identifier(self) -> &'static str {
match self {
Level::Integer => "det-module/1-int",
Level::Float => "det-module/1-det",
}
}
/// `integer` or `float`, as the planted corpus names a level.
pub fn name(self) -> &'static str {
match self {
Level::Integer => "integer",
Level::Float => "float",
}
}
/// The level a word names: `integer` or `float`, or the level's identifier.
pub fn parse(s: &str) -> Option<Level> {
match s {
"integer" | "det-module/1-int" => Some(Level::Integer),
"float" | "det-module/1-det" => Some(Level::Float),
_ => None,
}
}
}
/// The three caps of §4.2.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Caps {
/// The module's length, in bytes (R1).
pub module_bytes: u64,
/// The functions the module defines (R11).
pub functions: u64,
/// The memory's declared maximum, in 64 KiB pages (R6).
pub memory_pages: u64,
}
impl Caps {
/// The profile's caps.
pub const PROFILE: Caps = Caps {
module_bytes: 16_777_216,
functions: 50_000,
memory_pages: 65_536,
};
/// The profile's caps with `name=value` changes, comma-joined; `-` for none.
pub fn parse(s: &str) -> Option<Caps> {
let mut caps = Caps::PROFILE;
if s == "-" {
return Some(caps);
}
for part in s.split(',') {
let (name, value) = part.split_once('=')?;
let value: u64 = value.parse().ok()?;
match name {
"module_bytes" => caps.module_bytes = value,
"functions" => caps.functions = value,
"memory_pages" => caps.memory_pages = value,
_ => return None,
}
}
Some(caps)
}
}
impl Default for Caps {
fn default() -> Caps {
Caps::PROFILE
}
}
/// A checker's verdict (§4.3).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Verdict {
/// The module meets R1 to R12 at the level.
Held,
/// The first rule the module breaks, and the offset of the item that breaks it
/// (`None` for R2, which carries none).
Refused {
/// The rule's number.
rule: u8,
/// The byte offset into the module.
offset: Option<u64>,
},
}
impl fmt::Display for Verdict {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Verdict::Held => f.write_str("held"),
Verdict::Refused { rule, offset: Some(at) } => write!(f, "refused R{rule} {at}"),
Verdict::Refused { rule, offset: None } => write!(f, "refused R{rule} -"),
}
}
}
/// A rule an item breaks, and the item's offset.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
pub struct Finding {
/// The item's byte offset into the module.
pub offset: u64,
/// The rule's number.
pub rule: u8,
}
/// The features of WebAssembly 3.0, and no others. wasmparser's `WASM3` set also holds
/// threads, which WebAssembly 3.0 does not define (R2: shared memory and atomic
/// instructions are outside it).
pub fn features() -> WasmFeatures {
WasmFeatures::WASM3.difference(WasmFeatures::THREADS)
}
/// The module's verdict at `level` under `caps` (§4.3).
pub fn check(bytes: &[u8], level: Level, caps: &Caps) -> Verdict {
match findings(bytes, level, caps) {
Err(verdict) => verdict,
Ok(found) => match found.first() {
None => Verdict::Held,
Some(f) => Verdict::Refused {
rule: f.rule,
offset: Some(f.offset),
},
},
}
}
/// The level a sink holds the module at (§6, check 9b): the integer level where it is
/// held there; else, where the integer level refused it by R3, the float level where it is
/// held there. With the verdict of the last level checked.
pub fn level_of(bytes: &[u8], caps: &Caps) -> (Option<Level>, Verdict) {
let int = check(bytes, Level::Integer, caps);
match int {
Verdict::Held => (Some(Level::Integer), int),
Verdict::Refused { rule: 3, .. } => match check(bytes, Level::Float, caps) {
Verdict::Held => (Some(Level::Float), Verdict::Held),
other => (None, other),
},
other => (None, other),
}
}
/// Every rule from R3 to R12 the module's items and absences break, in binary order (an
/// item's rules in rule order), for a module that meets R1 and R2. The first is the
/// verdict; the rest are diagnostic. `Err` is the verdict of a module that breaks R1 or
/// R2.
pub fn findings(bytes: &[u8], level: Level, caps: &Caps) -> Result<Vec<Finding>, Verdict> {
if bytes.len() as u64 > caps.module_bytes {
return Err(Verdict::Refused {
rule: 1,
offset: Some(0),
});
}
let r2 = Verdict::Refused {
rule: 2,
offset: None,
};
if Validator::new_with_features(features())
.validate_all(bytes)
.is_err()
{
return Err(r2);
}
let mut scan = Scan {
bytes,
level,
caps: *caps,
found: Vec::new(),
types: Vec::new(),
funcs: Vec::new(),
memories: 0,
exported: [false; 6],
};
// The module is valid, so it decodes; an error here would be wasmparser's parser and
// validator disagreeing, which is no verdict this checker can give but R2.
scan.run().map_err(|_| r2)?;
let mut found = scan.found;
found.sort();
Ok(found)
}
/// A function type, as parameters and results.
type SigRef = (&'static [ValType], &'static [ValType]);
/// The exports of §5, by name, with the function type of each (`None` for `memory`).
const EXPORTS: [(&str, Option<SigRef>); 6] = [
("memory", None),
("wai_abi", Some((&[], &[ValType::I32]))),
("wai_alloc", Some((&[ValType::I32], &[ValType::I32]))),
(
"wai_run",
Some((
&[
ValType::I32,
ValType::I32,
ValType::I32,
ValType::I32,
ValType::I32,
ValType::I32,
],
&[ValType::I32],
)),
),
("wai_out_ptr", Some((&[], &[ValType::I32]))),
("wai_out_len", Some((&[], &[ValType::I32]))),
];
/// A function type's parameters and results.
type Sig = (Vec<ValType>, Vec<ValType>);
struct Scan<'a> {
bytes: &'a [u8],
level: Level,
caps: Caps,
found: Vec<Finding>,
/// Each type index's function type, where its entry is a plain function type (`None`
/// for an entry R12 refuses).
types: Vec<Option<Sig>>,
/// Each function index's type index, imported functions first.
funcs: Vec<u32>,
/// The memories the module defines.
memories: u32,
/// Which exports of §5 the module has.
exported: [bool; 6],
}
type R<T> = Result<T, wasmparser::BinaryReaderError>;
impl Scan<'_> {
fn refuse(&mut self, rule: u8, offset: u64) {
self.found.push(Finding { offset, rule });
}
fn run(&mut self) -> R<()> {
let headers = section_headers(self.bytes)?;
let header = |content_start: u64| -> u64 {
headers
.iter()
.find(|(_, start)| *start == content_start)
.map(|(id_at, _)| *id_at)
.expect("every section's content follows its header")
};
for payload in Parser::new(0).parse_all(self.bytes) {
match payload? {
Payload::TypeSection(r) => {
for item in r.into_iter_with_offsets() {
let (at, group) = item?;
self.type_entry(at, &group)?;
}
}
Payload::ImportSection(r) => {
for item in r.into_iter_with_offsets() {
let (at, imports) = item?;
// R5: every import entry breaks it.
self.refuse(5, at);
if let Imports::Single(_, import) = imports {
if let TypeRef::Func(t) = import.ty {
self.funcs.push(t);
}
}
}
}
Payload::FunctionSection(r) => {
if u64::from(r.count()) > self.caps.functions {
// R11: broken by the function section.
self.refuse(11, header(r.range().start));
}
for t in r {
self.funcs.push(t?);
}
}
Payload::TableSection(r) => {
for (i, item) in r.into_iter_with_offsets().enumerate() {
let (at, table) = item?;
let ty = table.ty;
// R7: at most one table, of funcref, i32-addressed, fixed.
let fixed = ty.element_type == RefType::FUNCREF
&& !ty.table64
&& ty.maximum == Some(ty.initial);
if i > 0 || !fixed {
self.refuse(7, at);
}
if let TableInit::Expr(e) = table.init {
self.ops(e.get_operators_reader())?;
}
}
}
Payload::MemorySection(r) => {
for (i, item) in r.into_iter_with_offsets().enumerate() {
let (at, mem) = item?;
self.memories += 1;
// R6: exactly one memory, i32-addressed, with a maximum within the cap.
let ok = i == 0
&& !mem.memory64
&& mem.maximum.is_some_and(|m| m <= self.caps.memory_pages);
if !ok {
self.refuse(6, at);
}
}
}
Payload::TagSection(r) => {
// R12: a tag section.
self.refuse(12, header(r.range().start));
}
Payload::GlobalSection(r) => {
for item in r.into_iter_with_offsets() {
let (at, global) = item?;
// A global entry starts with its value type.
self.declared_type(global.ty.content_type, at);
self.ops(global.init_expr.get_operators_reader())?;
}
}
Payload::ExportSection(r) => {
for item in r.into_iter_with_offsets() {
let (at, export) = item?;
if !self.export_ok(export.name, export.kind, export.index) {
self.refuse(10, at);
}
}
}
Payload::StartSection { range, .. } => {
// R8: a start section.
self.refuse(8, header(range.start));
}
Payload::ElementSection(r) => {
for item in r {
let element = item?;
if let ElementKind::Active { offset_expr, .. } = element.kind {
self.ops(offset_expr.get_operators_reader())?;
}
if let ElementItems::Expressions(_, exprs) = element.items {
for e in exprs {
self.ops(e?.get_operators_reader())?;
}
}
}
}
Payload::DataSection(r) => {
for item in r {
if let DataKind::Active { offset_expr, .. } = item?.kind {
self.ops(offset_expr.get_operators_reader())?;
}
}
}
Payload::CodeSectionEntry(body) => {
// The local declarations: each value type is an item, a declaration of
// no locals included.
let mut br = body.get_binary_reader();
for _ in 0..br.read_var_u32()? {
br.read_var_u32()?;
let at = br.original_position();
let ty: ValType = br.read()?;
self.declared_type(ty, at);
}
self.ops(body.get_operators_reader()?)?;
}
Payload::End(_) => {
let len = self.bytes.len() as u64;
if self.memories == 0 {
self.refuse(6, len);
}
if self.exported.iter().any(|seen| !seen) {
self.refuse(10, len);
}
}
_ => {}
}
}
Ok(())
}
/// An entry of the type section: R12 unless it is a plain function type (§4.1: a
/// type entry that is not a function type, a recursive or subtype declaration among
/// them); then each value type of its parameters and results.
fn type_entry(&mut self, at: u64, group: &wasmparser::RecGroup) -> R<()> {
if self.bytes[at as usize] != 0x60 {
self.refuse(12, at);
self.types.extend(group.types().map(|_| None));
return Ok(());
}
let sub = group.types().next().expect("a function type entry defines one type");
let CompositeInnerType::Func(ft) = &sub.composite_type.inner else {
unreachable!("an entry whose first byte is 0x60 is a function type");
};
// The value types' offsets, read again with the same reader.
let mut br = BinaryReader::new(&self.bytes[at as usize..], at);
br.read_u8()?;
for _ in 0..2 {
for _ in 0..br.read_var_u32()? {
let at = br.original_position();
let ty: ValType = br.read()?;
self.declared_type(ty, at);
}
}
self.types
.push(Some((ft.params().to_vec(), ft.results().to_vec())));
Ok(())
}
/// A value type of a function type, a local declaration or a global: R3 for a
/// floating-point type at the integer level, R9 for a reference type.
fn declared_type(&mut self, ty: ValType, at: u64) {
match ty {
ValType::F32 | ValType::F64 if self.level == Level::Integer => self.refuse(3, at),
ValType::Ref(_) => self.refuse(9, at),
_ => {}
}
}
/// A value type of a block type or a typed `select`: R3 only.
fn immediate_type(&mut self, ty: ValType, at: u64) {
if matches!(ty, ValType::F32 | ValType::F64) && self.level == Level::Integer {
self.refuse(3, at);
}
}
fn export_ok(&mut self, name: &str, kind: ExternalKind, index: u32) -> bool {
let Some(k) = EXPORTS.iter().position(|(n, _)| *n == name) else {
return false;
};
self.exported[k] = true;
match EXPORTS[k].1 {
None => kind == ExternalKind::Memory,
Some((params, results)) => {
kind == ExternalKind::Func
&& self
.funcs
.get(index as usize)
.and_then(|t| self.types.get(*t as usize))
.and_then(|sig| sig.as_ref())
.is_some_and(|(p, r)| p.as_slice() == params && r.as_slice() == results)
}
}
}
/// The instructions of a function body or a constant expression.
fn ops(&mut self, mut reader: OperatorsReader<'_>) -> R<()> {
while !reader.eof() {
let (op, at) = reader.read_with_offset()?;
for rule in instruction_rules(&op, self.level) {
self.refuse(rule, at);
}
// The value type a block type or a typed select gives, after the opcode.
match &op {
Operator::Block { blockty } | Operator::Loop { blockty } | Operator::If { blockty } => {
if let BlockType::Type(ty) = blockty {
self.immediate_type(*ty, at + 1);
}
}
Operator::TryTable { try_table } => {
if let BlockType::Type(ty) = try_table.ty {
self.immediate_type(ty, at + 1);
}
}
Operator::TypedSelect { ty } => {
// 0x1c, the vector's length (one, in as many bytes as it takes), the type.
let after = &self.bytes[at as usize + 1..];
let len = after.iter().take_while(|b| **b & 0x80 != 0).count() as u64 + 1;
self.immediate_type(*ty, at + 1 + len);
}
_ => {}
}
}
Ok(())
}
}
/// Each section's id byte offset and content start, in order.
fn section_headers(bytes: &[u8]) -> R<Vec<(u64, u64)>> {
let mut out = Vec::new();
let mut br = BinaryReader::new(&bytes[8..], 8);
while !br.eof() {
let id_at = br.original_position();
br.read_u8()?;
let size = br.read_var_u32()?;
let start = br.original_position();
out.push((id_at, start));
br.read_bytes(size as usize)?;
}
Ok(out)
}
macro_rules! define_operator_identity {
($( @$proposal:ident $op:ident $({ $($arg:ident: $argty:ty),* })? => $visit:ident ($($ann:tt)*) )*) => {
/// An operator's proposal, as wasmparser groups it, and its name (wasmparser's
/// visitor name without `visit_`: `f32x4_add`, `table_grow`).
pub fn operator_identity(op: &Operator<'_>) -> (&'static str, &'static str) {
match op {
$( Operator::$op { .. } => (stringify!($proposal), &stringify!($visit)[6..]), )*
_ => ("unknown", "unknown"),
}
}
};
}
wasmparser::for_each_operator!(define_operator_identity);
/// The rules from R3 to R12 an instruction breaks by its opcode alone, in rule order.
pub fn instruction_rules(op: &Operator<'_>, level: Level) -> Vec<u8> {
let (proposal, name) = operator_identity(op);
let mut rules = Vec::new();
// R3: an instruction that takes or gives a floating-point value, scalar or as lanes.
if level == Level::Integer && (name.contains("f32") || name.contains("f64")) {
rules.push(3);
}
// R4: every relaxed vector instruction.
if proposal == "relaxed_simd" {
rules.push(4);
}
// R7: the instructions that change a table.
if matches!(name, "table_grow" | "table_fill" | "table_set") {
rules.push(7);
}
if r12(name) {
rules.push(12);
}
rules
}
/// R12's instructions, as §4.1 lists them.
fn r12(name: &str) -> bool {
name.starts_with("struct_")
|| name.starts_with("array_")
|| matches!(
name,
// exception handling
"throw" | "throw_ref" | "try_table"
// tail calls
| "return_call" | "return_call_indirect"
// typed function references
| "call_ref" | "return_call_ref" | "ref_as_non_null" | "br_on_null" | "br_on_non_null"
// garbage-collected instructions
| "ref_i31" | "i31_get_s" | "i31_get_u"
| "ref_test_non_null" | "ref_test_nullable" | "ref_cast_non_null" | "ref_cast_nullable"
| "br_on_cast" | "br_on_cast_fail" | "any_convert_extern" | "extern_convert_any" | "ref_eq"
)
}
#[cfg(test)]
mod tests {
use super::*;
macro_rules! define_all_identities {
($( @$proposal:ident $op:ident $({ $($arg:ident: $argty:ty),* })? => $visit:ident ($($ann:tt)*) )*) => {
fn all_identities() -> Vec<(&'static str, &'static str)> {
vec![$( (stringify!($proposal), &stringify!($visit)[6..]), )*]
}
};
}
wasmparser::for_each_operator!(define_all_identities);
#[test]
fn r12_holds_every_instruction_of_the_proposals_it_names() {
// Every instruction of garbage collection and of tail calls is R12's, and so are
// the new ones of typed function references and exception handling (3.0's form
// of exception handling: the legacy one is outside WebAssembly 3.0, R2).
for (proposal, name) in all_identities() {
if matches!(proposal, "gc" | "tail_call" | "function_references" | "exceptions") {
assert!(r12(name), "{proposal} {name} is not R12's");
}
// The proposals outside WebAssembly 3.0 are R2's, whatever their names.
if r12(name) {
assert!(
matches!(
proposal,
"gc" | "tail_call" | "function_references" | "exceptions"
| "custom_descriptors" | "shared_everything_threads"
),
"{proposal} {name} is R12's"
);
}
}
}
#[test]
fn the_float_instructions_are_those_of_float_types() {
// Every instruction R3 names by its opcode names f32 or f64; and none of the
// proposals' integer instructions does.
let floats: Vec<_> = all_identities()
.into_iter()
.filter(|(_, n)| n.contains("f32") || n.contains("f64"))
.collect();
assert!(floats.iter().any(|(_, n)| *n == "f32x4_add"));
assert!(floats.iter().any(|(_, n)| *n == "i32_trunc_sat_f32_s"));
assert!(floats.iter().all(|(p, _)| matches!(
*p,
"mvp" | "simd" | "relaxed_simd" | "saturating_float_to_int"
)));
}
}

137
wai/wai-module-check/src/main.rs Normal file
View file

@ -0,0 +1,137 @@
//! `wai-module-check`: a module's verdict under the deterministic module profile.
//!
//! wai-module-check [--level integer|float] [--caps NAME=VALUE,...] FILE...
//! wai-module-check --cases DIR
//!
//! With `--level`, one verdict line a file (`held`, or `refused R<n> <offset>`), prefixed
//! by the file's name where there are several; without it, the level a sink holds the
//! module at (§6, check 9b), or the verdict that refuses it. `--caps` changes the
//! profile's caps (`module_bytes`, `functions`, `memory_pages`).
//!
//! `--cases DIR` checks every line of `DIR/cases.txt` (`<case> <level> <caps> <verdict>`,
//! the module being `DIR/<case>.wasm`) and names each that differs.
//!
//! Exit status: 0 when every module is held (or, with `--cases`, every verdict is the one
//! stated); 1 otherwise; 2 for a usage or input error.
use std::path::{Path, PathBuf};
use std::process::ExitCode;
use wai_module_check::{check, level_of, Caps, Level, Verdict};
fn usage() -> ExitCode {
eprintln!(
"usage: wai-module-check [--level integer|float] [--caps NAME=VALUE,...] FILE...\n wai-module-check --cases DIR"
);
ExitCode::from(2)
}
fn read(path: &Path) -> Result<Vec<u8>, ExitCode> {
std::fs::read(path).map_err(|e| {
eprintln!("wai-module-check: {}: {e}", path.display());
ExitCode::from(2)
})
}
fn cases(dir: &Path) -> ExitCode {
let list = dir.join("cases.txt");
let text = match std::fs::read_to_string(&list) {
Ok(t) => t,
Err(e) => {
eprintln!("wai-module-check: {}: {e}", list.display());
return ExitCode::from(2);
}
};
let (mut checked, mut wrong) = (0, 0);
for (n, line) in text.lines().enumerate() {
let line = line.split(" #").next().unwrap_or("").trim();
if line.is_empty() || line.starts_with('#') {
continue;
}
let mut parts = line.splitn(4, ' ');
let (Some(case), Some(level), Some(caps), Some(want)) =
(parts.next(), parts.next(), parts.next(), parts.next())
else {
eprintln!("wai-module-check: {}:{}: not `<case> <level> <caps> <verdict>`", list.display(), n + 1);
return ExitCode::from(2);
};
let (Some(level), Some(caps)) = (Level::parse(level), Caps::parse(caps)) else {
eprintln!("wai-module-check: {}:{}: no such level or caps", list.display(), n + 1);
return ExitCode::from(2);
};
let bytes = match read(&dir.join(format!("{case}.wasm"))) {
Ok(b) => b,
Err(code) => return code,
};
let got = check(&bytes, level, &caps).to_string();
checked += 1;
if got != want {
wrong += 1;
println!("{case} {} {}: {got}, not {want}", level.name(), line.split(' ').nth(2).unwrap_or("-"));
}
}
if wrong == 0 {
println!("wai-module-check: {checked} verdicts, each the one {} states", list.display());
ExitCode::SUCCESS
} else {
println!("wai-module-check: {wrong} of {checked} verdicts differ from {}", list.display());
ExitCode::FAILURE
}
}
fn main() -> ExitCode {
let args: Vec<String> = std::env::args().skip(1).collect();
if args.len() == 2 && args[0] == "--cases" {
return cases(Path::new(&args[1]));
}
let (mut level, mut caps, mut files) = (None, Caps::PROFILE, Vec::<PathBuf>::new());
let mut it = args.iter();
while let Some(a) = it.next() {
match a.as_str() {
"--level" => match it.next().and_then(|l| Level::parse(l)) {
Some(l) => level = Some(l),
None => return usage(),
},
"--caps" => match it.next().and_then(|c| Caps::parse(c)) {
Some(c) => caps = c,
None => return usage(),
},
s if s.starts_with("--") => return usage(),
s => files.push(PathBuf::from(s)),
}
}
if files.is_empty() {
return usage();
}
let mut all_held = true;
for file in &files {
let bytes = match read(file) {
Ok(b) => b,
Err(code) => return code,
};
let line = match level {
Some(l) => {
let v = check(&bytes, l, &caps);
all_held &= v == Verdict::Held;
v.to_string()
}
None => match level_of(&bytes, &caps) {
(Some(l), _) => format!("held at the {} level ({})", l.name(), l.identifier()),
(None, v) => {
all_held = false;
v.to_string()
}
},
};
if files.len() > 1 {
println!("{}: {line}", file.display());
} else {
println!("{line}");
}
}
if all_held {
ExitCode::SUCCESS
} else {
ExitCode::FAILURE
}
}

193
wai/wai-module-check/tests/module_rules.rs Normal file
View file

@ -0,0 +1,193 @@
//! The checker held to the checker corpus of deterministic-modules §9.1
//! (`planted/cases.txt`, which `planted/build.py` writes from each module's construction).
//!
//! - Every module gets the verdict stated, at every level and under every caps stated.
//! - Every planted module breaks exactly the rule its row names, at the item it names, and
//! no other: the checker's full list of findings for it is that one, but for the two rows
//! §9.1 says break a second rule, and the relaxed instruction that also takes
//! floating-point lanes at the integer level.
//! - Every rule from R1 to R12 is broken by a planted module (§11).
//! - The levels differ only in R3 (§4.3).
//! - The verdict is one line of ASCII.
use std::path::PathBuf;
use wai_module_check::{check, findings, level_of, Caps, Finding, Level, Verdict};
struct Case {
name: String,
level: Level,
caps: Caps,
caps_text: String,
verdict: String,
derived: bool,
}
fn planted() -> PathBuf {
PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("planted")
}
fn cases() -> Vec<Case> {
let text = std::fs::read_to_string(planted().join("cases.txt")).expect("planted/cases.txt");
let mut out = Vec::new();
for line in text.lines() {
if line.starts_with('#') || line.trim().is_empty() {
continue;
}
let (body, comment) = match line.split_once(" #") {
Some((b, c)) => (b, c.trim()),
None => (line, ""),
};
let mut parts = body.splitn(4, ' ');
let name = parts.next().unwrap().to_string();
let level = Level::parse(parts.next().unwrap()).expect("a level");
let caps_text = parts.next().unwrap().to_string();
let caps = Caps::parse(&caps_text).expect("caps");
let verdict = parts.next().unwrap().to_string();
out.push(Case {
name,
level,
caps,
caps_text,
verdict,
derived: comment == "derived",
});
}
assert!(out.len() > 80, "cases.txt holds {} verdicts", out.len());
out
}
fn module(name: &str) -> Vec<u8> {
std::fs::read(planted().join(format!("{name}.wasm"))).unwrap_or_else(|e| panic!("{name}.wasm: {e}"))
}
#[test]
fn every_module_gets_the_verdict_stated() {
let mut wrong = Vec::new();
for c in cases() {
let got = check(&module(&c.name), c.level, &c.caps).to_string();
if got != c.verdict {
wrong.push(format!(
"{} {} {}: {got}, not {}",
c.name,
c.level.name(),
c.caps_text,
c.verdict
));
}
}
assert!(wrong.is_empty(), "{}", wrong.join("\n"));
}
/// The rules §9.1 states a planted row breaks besides its own, at the level stated:
/// `import-memory` defines no memory (R6, at the module's length); `no-memory` lacks the
/// export `memory` (R10, there too); `f32x4.relaxed_madd` takes `f32x4` lanes (R3, at the
/// integer level, where it is the row's other rule).
fn also_broken(name: &str, level: Level) -> &'static [u8] {
match (name, level) {
("import-memory", _) => &[6],
("no-memory", _) => &[10],
("relaxed-madd", Level::Integer) => &[4],
_ => &[],
}
}
#[test]
fn every_planted_module_breaks_its_rule_and_no_other() {
// A module may break its rule at more than one item (`scalar-float` holds three
// floating-point instructions); it breaks no other rule.
let mut wrong = Vec::new();
let mut seen = 0;
for c in cases() {
let bytes = module(&c.name);
let Some(rest) = c.verdict.strip_prefix("refused R") else {
// A held module breaks nothing.
assert_eq!(findings(&bytes, c.level, &c.caps), Ok(vec![]), "{}", c.name);
continue;
};
let (rule, offset) = rest.split_once(' ').unwrap();
let rule: u8 = rule.parse().unwrap();
if rule <= 2 {
// R1 and R2 stop the reading; nothing else is decided.
continue;
}
let first = Finding {
offset: offset.parse().unwrap(),
rule,
};
let got = findings(&bytes, c.level, &c.caps).expect("meets R1 and R2");
let mut rules: Vec<u8> = got.iter().map(|f| f.rule).collect();
rules.sort();
rules.dedup();
let mut want = vec![rule];
want.extend_from_slice(also_broken(&c.name, c.level));
want.sort();
seen += 1;
if got.first() != Some(&first) || rules != want {
wrong.push(format!("{} {}: {got:?}; the rules {want:?}, first {first:?}", c.name, c.level.name()));
}
}
assert!(seen > 60, "{seen} refusals checked");
assert!(wrong.is_empty(), "{}", wrong.join("\n"));
}
#[test]
fn every_rule_has_a_planted_module() {
// §11: every rule of §4.1 that a checker decides is broken by a planted module of §9.1,
// in a verdict the text states (not one this corpus derives).
let cases = cases();
for rule in 1..=12 {
let prefix = format!("refused R{rule} ");
assert!(
cases.iter().any(|c| !c.derived && c.verdict.starts_with(&prefix)),
"no planted module of §9.1 is refused R{rule}"
);
}
}
#[test]
fn the_levels_differ_only_in_r3() {
// §4.3: a module refused R3 at the integer level is checked at the float level; every
// other verdict is the same at both.
for c in cases() {
let bytes = module(&c.name);
let int = check(&bytes, Level::Integer, &c.caps);
let float = check(&bytes, Level::Float, &c.caps);
if !matches!(int, Verdict::Refused { rule: 3, .. }) {
assert_eq!(int, float, "{}", c.name);
}
assert!(!matches!(float, Verdict::Refused { rule: 3, .. }), "{}", c.name);
}
}
#[test]
fn a_sink_holds_each_module_at_the_level_its_rows_give() {
// §6, check 9b: the integer level where it is held there, else the float level where
// the integer level refused it by R3 and the float level holds it.
let held_int = ["minimal-int", "vector-int", "bulk-and-sign", "fixed-table", "fixed-memory", "custom-section"];
for name in held_int {
assert_eq!(level_of(&module(name), &Caps::PROFILE).0, Some(Level::Integer), "{name}");
}
for name in ["minimal-float", "scalar-float", "float-vector", "float-load", "float-unreachable"] {
assert_eq!(level_of(&module(name), &Caps::PROFILE).0, Some(Level::Float), "{name}");
}
// relaxed-madd: refused R3 at the integer level, then R4 at the float level.
let (level, verdict) = level_of(&module("relaxed-madd"), &Caps::PROFILE);
assert_eq!(level, None);
assert!(matches!(verdict, Verdict::Refused { rule: 4, .. }));
}
#[test]
fn the_verdict_is_one_line_of_ascii() {
for c in cases() {
let v = check(&module(&c.name), c.level, &c.caps).to_string();
assert!(v.is_ascii() && !v.contains('\n'), "{v:?}");
let ok = v == "held"
|| v.strip_prefix("refused R").is_some_and(|rest| {
let (n, at) = rest.split_once(' ').unwrap_or(("", ""));
n.parse::<u8>().is_ok_and(|n| (1..=12).contains(&n))
&& (at == "-" || at.bytes().all(|b| b.is_ascii_digit()))
});
assert!(ok, "{v:?}");
}
}