From 13285059b4ef0943348ce278e9dad3416dd66430 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Wed, 4 Nov 2026 23:09:21 -0500 Subject: [PATCH 01/12] wai/det-module-profile, converted to the layout of the fix: no shared append point The change of wai/det-module-profile (4e8e4fb09..45a7b4eb7, 2 commits), on the fix branch: its changelog entries as files of wai/changes/, its wai-conformance.yml edits as step files, corpus files and test tags, and every other file as the branch has it. - 9061cb07f wai: the deterministic module profile, a checked subset of WebAssembly for the decoder modules a sink runs - 45a7b4eb7 wai: the deterministic module profile: a record's key read from the grant's head; the scope of check 9; what the verifiers and corpora cover Co-Authored-By: Claude Opus 5.5 --- wai/SPEC.md | 4 +- ...dule-profile-checked-subset-webassembly.md | 37 ++ wai/extensions/browser-sink.md | 24 +- wai/extensions/determinism-tiers.md | 14 +- wai/extensions/deterministic-modules.md | 479 ++++++++++++++++++ wai/extensions/integer-operators.md | 2 + wai/extensions/jwp-receipts.md | 88 +++- wai/signer-conformance/README.md | 2 +- 8 files changed, 630 insertions(+), 20 deletions(-) create mode 100644 wai/changes/2026-11-04-deterministic-module-profile-checked-subset-webassembly.md create mode 100644 wai/extensions/deterministic-modules.md diff --git a/wai/SPEC.md b/wai/SPEC.md index da00fc368..32b800d91 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -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 diff --git a/wai/changes/2026-11-04-deterministic-module-profile-checked-subset-webassembly.md b/wai/changes/2026-11-04-deterministic-module-profile-checked-subset-webassembly.md new file mode 100644 index 000000000..e983ff79e --- /dev/null +++ b/wai/changes/2026-11-04-deterministic-module-profile-checked-subset-webassembly.md @@ -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. diff --git a/wai/extensions/browser-sink.md b/wai/extensions/browser-sink.md index 53893f6cb..5eea86b46 100644 --- a/wai/extensions/browser-sink.md +++ b/wai/extensions/browser-sink.md @@ -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 diff --git a/wai/extensions/determinism-tiers.md b/wai/extensions/determinism-tiers.md index 9c00b6bf0..c491c641a 100644 --- a/wai/extensions/determinism-tiers.md +++ b/wai/extensions/determinism-tiers.md @@ -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 diff --git a/wai/extensions/deterministic-modules.md b/wai/extensions/deterministic-modules.md new file mode 100644 index 000000000..eb35e0d80 --- /dev/null +++ b/wai/extensions/deterministic-modules.md @@ -0,0 +1,479 @@ +# 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; a value type, in a function + type, a local declaration, 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. +- **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. 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) and *Validation* | +| 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`, 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") | + +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 + +| 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. + +### 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 `, with `` the rule and `` 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 `@`, optionally followed by +`/`: `` and `` are 1 to 64 of `a`–`z`, `0`–`9`, `_` and `-`, and +`` 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-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. diff --git a/wai/extensions/integer-operators.md b/wai/extensions/integer-operators.md index 2936cfd55..e6f1ab0c7 100644 --- a/wai/extensions/integer-operators.md +++ b/wai/extensions/integer-operators.md @@ -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 diff --git a/wai/extensions/jwp-receipts.md b/wai/extensions/jwp-receipts.md index 71d62b8fc..112fb0dac 100644 --- a/wai/extensions/jwp-receipts.md +++ b/wai/extensions/jwp-receipts.md @@ -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 | diff --git a/wai/signer-conformance/README.md b/wai/signer-conformance/README.md index f1a2c9acc..f71b03565 100644 --- a/wai/signer-conformance/README.md +++ b/wai/signer-conformance/README.md @@ -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=`. 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 -- 2.54.0 (Apple Git-157) From 7124b7b591a63de139d1763a3cf099423e225de5 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 5 Nov 2026 07:32:01 -0500 Subject: [PATCH 02/12] deterministic-modules: fix R2's validation limits, and say how R3 reads a block type MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit R2 asks for a valid module, but WebAssembly 3.0 lets an implementation limit the number and the size of a module's parts, and a validator a checker is built on does: without fixed limits, two conforming checkers could give one module within the caps different verdicts, so the verdict was not a function of the bytes. §4.2 now fixes the limits, and a module beyond one is refused R2. R3 now says how an instruction whose types an immediate or another item fixes (a block, a typed select, a call) is refused: through that value type, which follows the opcode for a block type or a typed select. The item term covers instructions in constant expressions and a declaration of no locals, and R7's funcref covers both of its encodings. These are the readings both checkers take. Co-Authored-By: Claude Opus 5.5 --- wai/extensions/deterministic-modules.md | 42 +++++++++++++++++++++---- 1 file changed, 36 insertions(+), 6 deletions(-) diff --git a/wai/extensions/deterministic-modules.md b/wai/extensions/deterministic-modules.md index eb35e0d80..bab9cc157 100644 --- a/wai/extensions/deterministic-modules.md +++ b/wai/extensions/deterministic-modules.md @@ -85,10 +85,12 @@ level when a checker gives it `held` at that level (§4.3), and R13. 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; a value type, in a function - type, a local declaration, a global type, a block type or a typed `select`; an entry of the +- **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. +- **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, @@ -106,12 +108,12 @@ 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. 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) and *Validation* | +| 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`, 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 | +| 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 | @@ -119,12 +121,17 @@ for each rule, at least one planted module that breaks it and no other. | 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 +### 4.2 Caps and validation limits | cap | the profile's value | what it bounds | |---|---|---| @@ -135,6 +142,29 @@ rule, check or sink of this text reads them. 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 | +| imports, exports | 1,000,000 each | the entries of the import section, and of the export section | +| 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 | + ### 4.3 The verdict A checker's verdict for a module at a level under caps is one line of ASCII: `held`, or -- 2.54.0 (Apple Git-157) From 6e22da53641a7716ca2575a94d35017eade7cf00 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 5 Nov 2026 07:34:45 -0500 Subject: [PATCH 03/12] wai-module-check: the checker corpus of the deterministic module profile, built from source MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit deterministic-modules §9.1 gives each module by its construction: minimal-int, and minimal-int with one change for every case but component. planted/build.py is that construction, byte by byte, standard library only. It writes each module and cases.txt, the verdicts §9.1 states, at each level the row names and under its caps. Every offset in cases.txt is the place where the item its row names lands in the bytes, marked while they are put together, so no verdict is taken from a checker; the two checkers come after this commit. Lines §4.3 decides but §9.1 does not state (a row's other level where it breaks only R3, the profile's caps for the rows with lower ones) are marked as derived. grow-swallowed, §9.2's module, is held: R13 is no checker's rule. `build.py --check` fails unless the committed files are what it writes. Co-Authored-By: Claude Opus 5.5 --- wai/wai-module-check/planted/build.py | 564 ++++++++++++++++++ .../planted/bulk-and-sign.wasm | Bin 0 -> 188 bytes wai/wai-module-check/planted/call-ref.wasm | Bin 0 -> 163 bytes wai/wai-module-check/planted/cases.txt | 110 ++++ wai/wai-module-check/planted/component.wasm | Bin 0 -> 8 bytes .../planted/custom-section.wasm | Bin 0 -> 177 bytes wai/wai-module-check/planted/exception.wasm | Bin 0 -> 161 bytes .../planted/exported-global.wasm | Bin 0 -> 172 bytes .../planted/externref-global.wasm | Bin 0 -> 159 bytes .../planted/externref-table.wasm | Bin 0 -> 158 bytes .../planted/extra-export.wasm | Bin 0 -> 163 bytes .../planted/fixed-memory.wasm | Bin 0 -> 151 bytes wai/wai-module-check/planted/fixed-table.wasm | Bin 0 -> 173 bytes .../planted/float-constant.wasm | Bin 0 -> 166 bytes .../planted/float-conversion.wasm | Bin 0 -> 173 bytes wai/wai-module-check/planted/float-load.wasm | Bin 0 -> 157 bytes .../planted/float-signature.wasm | Bin 0 -> 155 bytes .../planted/float-truncation.wasm | Bin 0 -> 157 bytes .../planted/float-unreachable.wasm | Bin 0 -> 156 bytes .../planted/float-vector.wasm | Bin 0 -> 191 bytes .../planted/funcref-local.wasm | Bin 0 -> 153 bytes .../planted/funcref-parameter.wasm | Bin 0 -> 159 bytes .../planted/grow-swallowed.wasm | Bin 0 -> 156 bytes wai/wai-module-check/planted/i64-export.wasm | Bin 0 -> 151 bytes .../planted/import-function.wasm | Bin 0 -> 166 bytes .../planted/import-global.wasm | Bin 0 -> 163 bytes .../planted/import-memory.wasm | Bin 0 -> 163 bytes wai/wai-module-check/planted/invalid.wasm | Bin 0 -> 151 bytes wai/wai-module-check/planted/memory64.wasm | Bin 0 -> 151 bytes .../planted/minimal-float.wasm | Bin 0 -> 171 bytes wai/wai-module-check/planted/minimal-int.wasm | Bin 0 -> 151 bytes wai/wai-module-check/planted/missing-run.wasm | Bin 0 -> 141 bytes wai/wai-module-check/planted/no-maximum.wasm | Bin 0 -> 150 bytes wai/wai-module-check/planted/no-memory.wasm | Bin 0 -> 129 bytes .../planted/over-functions.wasm | Bin 0 -> 175 bytes wai/wai-module-check/planted/over-pages.wasm | Bin 0 -> 151 bytes wai/wai-module-check/planted/oversize.wasm | Bin 0 -> 151 bytes wai/wai-module-check/planted/relaxed-dot.wasm | Bin 0 -> 191 bytes .../planted/relaxed-laneselect.wasm | Bin 0 -> 209 bytes .../planted/relaxed-madd.wasm | Bin 0 -> 209 bytes .../planted/relaxed-swizzle.wasm | Bin 0 -> 191 bytes .../planted/scalar-float.wasm | Bin 0 -> 163 bytes .../planted/shared-memory.wasm | Bin 0 -> 158 bytes wai/wai-module-check/planted/start.wasm | Bin 0 -> 161 bytes wai/wai-module-check/planted/struct-type.wasm | Bin 0 -> 153 bytes wai/wai-module-check/planted/table-fill.wasm | Bin 0 -> 167 bytes wai/wai-module-check/planted/table-grow.wasm | Bin 0 -> 166 bytes wai/wai-module-check/planted/table-set.wasm | Bin 0 -> 164 bytes .../planted/table-unfixed.wasm | Bin 0 -> 158 bytes wai/wai-module-check/planted/tail-call.wasm | Bin 0 -> 153 bytes .../planted/two-memories.wasm | Bin 0 -> 154 bytes wai/wai-module-check/planted/two-tables.wasm | Bin 0 -> 162 bytes wai/wai-module-check/planted/vector-int.wasm | Bin 0 -> 327 bytes 53 files changed, 674 insertions(+) create mode 100644 wai/wai-module-check/planted/build.py create mode 100644 wai/wai-module-check/planted/bulk-and-sign.wasm create mode 100644 wai/wai-module-check/planted/call-ref.wasm create mode 100644 wai/wai-module-check/planted/cases.txt create mode 100644 wai/wai-module-check/planted/component.wasm create mode 100644 wai/wai-module-check/planted/custom-section.wasm create mode 100644 wai/wai-module-check/planted/exception.wasm create mode 100644 wai/wai-module-check/planted/exported-global.wasm create mode 100644 wai/wai-module-check/planted/externref-global.wasm create mode 100644 wai/wai-module-check/planted/externref-table.wasm create mode 100644 wai/wai-module-check/planted/extra-export.wasm create mode 100644 wai/wai-module-check/planted/fixed-memory.wasm create mode 100644 wai/wai-module-check/planted/fixed-table.wasm create mode 100644 wai/wai-module-check/planted/float-constant.wasm create mode 100644 wai/wai-module-check/planted/float-conversion.wasm create mode 100644 wai/wai-module-check/planted/float-load.wasm create mode 100644 wai/wai-module-check/planted/float-signature.wasm create mode 100644 wai/wai-module-check/planted/float-truncation.wasm create mode 100644 wai/wai-module-check/planted/float-unreachable.wasm create mode 100644 wai/wai-module-check/planted/float-vector.wasm create mode 100644 wai/wai-module-check/planted/funcref-local.wasm create mode 100644 wai/wai-module-check/planted/funcref-parameter.wasm create mode 100644 wai/wai-module-check/planted/grow-swallowed.wasm create mode 100644 wai/wai-module-check/planted/i64-export.wasm create mode 100644 wai/wai-module-check/planted/import-function.wasm create mode 100644 wai/wai-module-check/planted/import-global.wasm create mode 100644 wai/wai-module-check/planted/import-memory.wasm create mode 100644 wai/wai-module-check/planted/invalid.wasm create mode 100644 wai/wai-module-check/planted/memory64.wasm create mode 100644 wai/wai-module-check/planted/minimal-float.wasm create mode 100644 wai/wai-module-check/planted/minimal-int.wasm create mode 100644 wai/wai-module-check/planted/missing-run.wasm create mode 100644 wai/wai-module-check/planted/no-maximum.wasm create mode 100644 wai/wai-module-check/planted/no-memory.wasm create mode 100644 wai/wai-module-check/planted/over-functions.wasm create mode 100644 wai/wai-module-check/planted/over-pages.wasm create mode 100644 wai/wai-module-check/planted/oversize.wasm create mode 100644 wai/wai-module-check/planted/relaxed-dot.wasm create mode 100644 wai/wai-module-check/planted/relaxed-laneselect.wasm create mode 100644 wai/wai-module-check/planted/relaxed-madd.wasm create mode 100644 wai/wai-module-check/planted/relaxed-swizzle.wasm create mode 100644 wai/wai-module-check/planted/scalar-float.wasm create mode 100644 wai/wai-module-check/planted/shared-memory.wasm create mode 100644 wai/wai-module-check/planted/start.wasm create mode 100644 wai/wai-module-check/planted/struct-type.wasm create mode 100644 wai/wai-module-check/planted/table-fill.wasm create mode 100644 wai/wai-module-check/planted/table-grow.wasm create mode 100644 wai/wai-module-check/planted/table-set.wasm create mode 100644 wai/wai-module-check/planted/table-unfixed.wasm create mode 100644 wai/wai-module-check/planted/tail-call.wasm create mode 100644 wai/wai-module-check/planted/two-memories.wasm create mode 100644 wai/wai-module-check/planted/two-tables.wasm create mode 100644 wai/wai-module-check/planted/vector-int.wasm diff --git a/wai/wai-module-check/planted/build.py b/wai/wai-module-check/planted/build.py new file mode 100644 index 000000000..cea99f411 --- /dev/null +++ b/wai/wai-module-check/planted/build.py @@ -0,0 +1,564 @@ +#!/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 +`.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: ` `, where `` is +`integer` or `float`, `` is `-` for the profile's caps (§4.2) or the caps the row +states, comma-joined `name=value`, and `` 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 + +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): + out = Blob() + for x in blobs: + out = out + x + return out + + +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(" 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.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(" `, 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 main(argv): + check = argv[1:] == ["--check"] + if argv[1:] and not check: + print("usage: build.py [--check]", 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)) diff --git a/wai/wai-module-check/planted/bulk-and-sign.wasm b/wai/wai-module-check/planted/bulk-and-sign.wasm new file mode 100644 index 0000000000000000000000000000000000000000..3b9eed0140b6fc5657350b6f74049f1d633e868c GIT binary patch literal 188 zcmX|&K@Ng26h!BLN{RFY_6T|dcingmK*NHBQd1$uRj=m3T=-j~|0k0-GZ_qbPXK7I zdQj>qiRe^L2%J)-YY+pqA|h_iTKmz5_+&JXVd{p<1ndgUbGU*^8n*>(avHX^yR8w` m-_7F!)w){2kr9D8isXN{_>mEKS*{#8Hr7geIOXy?DANzY@Fze3 literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/call-ref.wasm b/wai/wai-module-check/planted/call-ref.wasm new file mode 100644 index 0000000000000000000000000000000000000000..c0cc97805bc10b08987743d8070e308159434be9 GIT binary patch literal 163 zcmX|$I}XAy07LEks*;7F69-`62y9unMjKFvN=bu4E5wvLaw6IcczCj(;a`ye*vSDb z1Iq?eYFMPvpa8TYDVm!xaf~T{1e&*>dVimQwzd$`1FSZ$Glbo3T9^L0WXS&t;|$em aN)U&$R&cZ%V2}8s!^y#2uGmGj_5T5#njt^{ literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/cases.txt b/wai/wai-module-check/planted/cases.txt new file mode 100644 index 000000000..4f37ea104 --- /dev/null +++ b/wai/wai-module-check/planted/cases.txt @@ -0,0 +1,110 @@ +# The checker corpus of deterministic-modules.md §9.1, and §9.2's grow-swallowed, +# written by build.py: ` `, 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-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 diff --git a/wai/wai-module-check/planted/component.wasm b/wai/wai-module-check/planted/component.wasm new file mode 100644 index 0000000000000000000000000000000000000000..13d20e9f03ed5ca6672a62c2e3a0f6c5408bcdf1 GIT binary patch literal 8 PcmZQbEY9U+U}OLQ2e<)H literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/custom-section.wasm b/wai/wai-module-check/planted/custom-section.wasm new file mode 100644 index 0000000000000000000000000000000000000000..02ca25579523216e1530a40830e0f209c099718e GIT binary patch literal 177 zcmX|$u@1r@7=-Vq1){7DuC6AHadqqBYqV%FX#%A|h;ic8r3~Ki_Xhu*T zDHn)bL%9(g!~otB5tDZzoN+#U8RSRLgMQ4wt~P7^6I5+T3z*uhPjOgdK=WVLENJ&9 j-l8W}0Hq50^9@_CqFy-4HTc(T&17Qd{FJP@T)Q%U&T%O1 literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/exception.wasm b/wai/wai-module-check/planted/exception.wasm new file mode 100644 index 0000000000000000000000000000000000000000..a5e2d24eaafb2edfa90e940569eb21dc66220a89 GIT binary patch literal 161 zcmX|$I}(C007Q55L(Nco06ULhN8>dhIuy(##ECEtRjy7*;THRO3-=8Kz^fX-JTMnC zxvDfk8Vw3SE0Us>glwM1gfYal2{b=9_3kwR=i0oFZ?Mv|&JgyXab5b)k|6)fk2BQe UrWHEcVz4bvCA#|q$Ev8FJJCKMrvLx| literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/exported-global.wasm b/wai/wai-module-check/planted/exported-global.wasm new file mode 100644 index 0000000000000000000000000000000000000000..a7bdb31013fb705d29dd65d30ef26b0f23a59ffa GIT binary patch literal 172 zcmX|$I}XAy07LEkDw>rGuyO>po`D0jDXLJVq(Pw-V#?J?GT`CKeujGo0^nIrV4j!@ zOm1P8MuP&-ili`x83Sy0?@U-iOkaWSM))j7*}4%2&tPf+?P6-wwhj5dbfG1nbD! z;HrdGI}0knSmw5}hNS8q&ZQ~k@>S^eFc0B511D)Q<`*coYzve>Y~I%4y%y;I6{iK} Te61;2J7{UiMV literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/fixed-memory.wasm b/wai/wai-module-check/planted/fixed-memory.wasm new file mode 100644 index 0000000000000000000000000000000000000000..a7942a12a2a77e6d64d67ab49729303db1c45031 GIT binary patch literal 151 zcmX|$Jr2S!7(?y+RgjenuyO>pE?lDxs6(ZsL7`Q}l&h0|10J62XM|580ABP6){(Wr zRSBzh7F2*WZ0R1(r77j|Rp|CG58*ijCuuR}7bv!D3zR=>-qzv07U=(q(*kq8T7#ax O0p2(Cw>yq5LarYgK_DUk literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/fixed-table.wasm b/wai/wai-module-check/planted/fixed-table.wasm new file mode 100644 index 0000000000000000000000000000000000000000..12556055b4afad8085ae3df5ba806b1ce9a4ea1d GIT binary patch literal 173 zcmX|%I}XAy07LD3RWem#;sQt7Gl5 Z{;xPpF#D4=Xz459eMNh|VCy2}^aJyVAp!sZ literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/float-conversion.wasm b/wai/wai-module-check/planted/float-conversion.wasm new file mode 100644 index 0000000000000000000000000000000000000000..5b3639fd03c51b9e4bace1331d7a49d1f2951e47 GIT binary patch literal 173 zcmY*Sy9&ZU088#w^cSyT?G}HdtS(fL0_$cQ+R0o+^5Qi-YTL*iF;z@B`leAhrMi literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/float-signature.wasm b/wai/wai-module-check/planted/float-signature.wasm new file mode 100644 index 0000000000000000000000000000000000000000..7041928e95067aa4b7b1f35cb3f02045ff913921 GIT binary patch literal 155 zcmX|$F%H5o6hrMaNd>t8D=SA}>%ukKfI3u48WdU~B&1xO76R{1#|lerWxD0Cu&7kRD*Qc^M(>X45ja&pAW>SLjEm Y{aGtG+7+;e6`wCo4(@WrW~#1-9|L3}L;wH) literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/float-unreachable.wasm b/wai/wai-module-check/planted/float-unreachable.wasm new file mode 100644 index 0000000000000000000000000000000000000000..6dde93336dd8aeba02f69b7f1072742c82b77d73 GIT binary patch literal 156 zcmX|$I}XAy07LEkD#!o>69-`62y9unMjKFvN=Z|NR){Hg;KZ~U@bF|m!@nW{@FY91 zbSx`OsbP^ug96Zsq-gHO#6G6{5oq3iX#HaVcD03&o?x|k86oUu(=xZyoFV@!^dr>% Xq7@wN3fSX{!}sjqt~YF=+WP+h$>$*{ literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/float-vector.wasm b/wai/wai-module-check/planted/float-vector.wasm new file mode 100644 index 0000000000000000000000000000000000000000..7b16ede69a108ea7897431dae115bb140c2895fe GIT binary patch literal 191 zcmZvVzY4-I7{u@LuV@^dd<0iFw=RND(MIV|Xc~zv;*^*5H3ZWPg5V9ueLuMS;O?FP zxRouKTBd9!6){PpK>=t*QdB2neCI=a3RDl*H}28{tCEHxT){%)JVMxohIwjkQ-u6p iLpMUL&sw3T%?5kGdz1hF=nr{uSEJq^v2;qYOnd-@q9lO; literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/funcref-local.wasm b/wai/wai-module-check/planted/funcref-local.wasm new file mode 100644 index 0000000000000000000000000000000000000000..1af22f21fa577673d723a0fe965eb7112db4b499 GIT binary patch literal 153 zcmX|$I}U>|07LEk5RJO^2HkpuZdrN_NGk@UgrESbI_2s>hI+94p5d2B0KCZ_EIrFn zrqr-Vqd@^^MN%{`W8x4~{s}Z+KX(2-0&QI(qz_na-X;ip+O)0Ryk^Khg<*oa+_i$E RJqq?p&JOPJ#7R}va|dA}AejIF literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/funcref-parameter.wasm b/wai/wai-module-check/planted/funcref-parameter.wasm new file mode 100644 index 0000000000000000000000000000000000000000..c52d2a4f85431fa87ac659278e079d9fbbd7058d GIT binary patch literal 159 zcmX|$F%H8Z5Cr!Q0!sKm9*`)4uiVmZ8oSrUm-; UFd7}X3OHBMJzr>Dgj@{w2M+Wh4*&oF literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/grow-swallowed.wasm b/wai/wai-module-check/planted/grow-swallowed.wasm new file mode 100644 index 0000000000000000000000000000000000000000..2eb4dd3e2d7d59906f32557aee453db35ff97c58 GIT binary patch literal 156 zcmX|$I}XAy07LEkD#*gX!~qyM0ux!dMjKFvN=bu4E5wwmlV-rfll=_;js(D?9KbTL zRG8AjB8>(GpcP5c-HnN3O!+I&ef-q>#{}$J3n4whX7f5j*v+PO>0e8R{I4+1Q2Vo1 UaI_V$huUs9Ik?Len`pNEKf&4{$p8QV literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/i64-export.wasm b/wai/wai-module-check/planted/i64-export.wasm new file mode 100644 index 0000000000000000000000000000000000000000..b0d5ca563fda53ffee6b06e8594edc5915dcd068 GIT binary patch literal 151 zcmX|$I}XAy07LEks*;rpuyO>pE?lDxs6(ZsL7^35Ay;pb0S{01Gu%560MBv)^Tb?W za?Ouf8Vw3SE0UtS8x!Ub(^sJTxMg&Y1?XGzK0d)_)4oF3YU93*uPs6Tm!DUt(?u%` Qv<0xXV7T5;dlT(C02(nMA^-pY literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/import-function.wasm b/wai/wai-module-check/planted/import-function.wasm new file mode 100644 index 0000000000000000000000000000000000000000..bda6e019c89da13c5d885ad685fa312b6d7723a4 GIT binary patch literal 166 zcmX|&I}XAy5JYGEi@>7e0<;`~E)Ca6LgXUCv5}L2sC;!C7fkUq`&NTtnF)Yr*@L-f zE-<-=t*QZ#pCW;e(56=*)g)D4dbJk;jP0HWHo1xUNwxUJo5 bO;G>Ky8wN>XoZ%x0M-_?*Bka;MScAMLgpit literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/import-global.wasm b/wai/wai-module-check/planted/import-global.wasm new file mode 100644 index 0000000000000000000000000000000000000000..f0c512b5060fc7443e82823ed028fa0c16f55c4e GIT binary patch literal 163 zcmX|$I}XAy07LEkDw>rGuyO>pE?lDxC_Op!>LabhjBev=&0XgUv2mg0Q>I+d4ki1@gaw WPf-0yD-5(1u(o12U$FNk+VumHY$9d= literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/import-memory.wasm b/wai/wai-module-check/planted/import-memory.wasm new file mode 100644 index 0000000000000000000000000000000000000000..a7af8147722aea53d221925f2bec34fe07882491 GIT binary patch literal 163 zcmX|$I}XAy07LDhO$AvPxBx3hVC&Lrv;k$Pln)9ms8g;^8VNi++0QU9PXIj23Ct67 zfyy<^;zVh~TY2ka+5{=2YC!>XgZf!?A2W~UJ_Co^oQn^z+O!4;z1z4h<8w)n|K)5z VbG)<-dg=mbUC>`|*n1WA`T}8%BpCnz literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/invalid.wasm b/wai/wai-module-check/planted/invalid.wasm new file mode 100644 index 0000000000000000000000000000000000000000..427d560d926915008967da5d64afde19461204c0 GIT binary patch literal 151 zcmX|#I}XAy6a;tui{Q0ffR-cBg@S7&2BnB($H*i?RK7Zn3$_@|4*WY308e@Z%g9pU zN*jxI7F2*WBvp5JE>1D!uR{0n^WYydaA+1ndV;OyZGn=#rfnTwYli;6FfB00vo*L; Q40?!E^p`7kZ=r(n0~*U9Bme*a literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/memory64.wasm b/wai/wai-module-check/planted/memory64.wasm new file mode 100644 index 0000000000000000000000000000000000000000..8f20ea4618a68ea9be9967ea2b4274a42bfdd1d0 GIT binary patch literal 151 zcmX|$Jr2S!7(?y+RgjenuyO>pcHkOqKpiS24GOJLr(B)(8}RUCKO=k+0q~*+unw#{ zT$QkDXF&y6Lrc{>oJ(WMWm9OrVd}$k0#4Fm%r8)ES!XDJ*t{tWl+9(|gNh7hPIOSD*L?6L4h&LSf2M7D~1b}wD z1Er2qCY1^(aV0?vkb;OpE?lDxs6(ZsL7`Q}l&h0|10J62XM|580ABP6){(Wr zRSBzh7F2*WBvtotE=?(yuR^znc?i!LI7y2!zd*5NTcG@5^R^D}wLt$@oEDh#)f)8l P4e-99zuj?k5pw+i8m%BB literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/missing-run.wasm b/wai/wai-module-check/planted/missing-run.wasm new file mode 100644 index 0000000000000000000000000000000000000000..a3a09414cd5ed5c439cd9b4a0e0433095ef98166 GIT binary patch literal 141 zcmX|$I}U>|07LEkP|4a0u=WV33nzh4F(4(R;-iWwS0`ksho@&7ZVLp!ryRgEFlCrj z!X%9b1)vp4QN6VZQ;6#+Q2pH8yKx2{#k`Ln(B2-8z5nhj>jIr39U1@t literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/no-maximum.wasm b/wai/wai-module-check/planted/no-maximum.wasm new file mode 100644 index 0000000000000000000000000000000000000000..53b8e30ac0c7f815543acc56a20773972d07ac6a GIT binary patch literal 150 zcmX|%K@Ni;6hvo0FqLgD&~1;uBFAaI5BAnDa;Rcx(`+SUC3avq#8(a?6IMd#DCI PO$Lm~=$|hXuSK1H5n&)7 literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/no-memory.wasm b/wai/wai-module-check/planted/no-memory.wasm new file mode 100644 index 0000000000000000000000000000000000000000..edbc391850ffb38fdcb13fa803c942c4f6ff895c GIT binary patch literal 129 zcmY+2OAbIV07Pe0HFRs`E*4HwB^Huu#V3}%I=YaU#ml@0yDtR5TJ&J-86OlejZqX5 t%mCF&b=le2VFt?doC_nE>UMf$`mNzS%zA7PpSj5+uNs-7qke!tsBgj=9CiQz literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/over-functions.wasm b/wai/wai-module-check/planted/over-functions.wasm new file mode 100644 index 0000000000000000000000000000000000000000..d4352cfc1687c1d3ddd5f1fe322f9624849252dd GIT binary patch literal 175 zcmYL;y$-@40EF)VX(+2t;qKzr#n))jbZ7#_V4KE?SC4JgW8a!@2ibJaSGA*Po=v$?5vw+S${c^~g!wP~Fp>~7<_^p7P${+1tSsP=3W UI@$tQThN^@*n1WK>pMTk8`38sg8%>k literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/over-pages.wasm b/wai/wai-module-check/planted/over-pages.wasm new file mode 100644 index 0000000000000000000000000000000000000000..266604488f4fccc9706cf7c9f4404c72ac89979d GIT binary patch literal 151 zcmX|$Jr2S!7(?y+RgejZ3$Stowk}+w4X8tK8ThW>iP-bKju10ew*G5`Po literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/oversize.wasm b/wai/wai-module-check/planted/oversize.wasm new file mode 100644 index 0000000000000000000000000000000000000000..392e3747b595453e7fa885cc1d50c1a905ee9c0c GIT binary patch literal 151 zcmX|$Jr2S!7(?y+RgjenuyO>pE?lDxs6(ZsL7`Q}l&h0|10J62XM|580ABP6){(Wr zRSBzh7F2*WBvtotE=?(yuR^znc?i!LI7y2!zd*5NTcG@5^R^D}wLt$@oEDh#)f)8l P4e-99zuj?k5pw+i8m%BB literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/relaxed-dot.wasm b/wai/wai-module-check/planted/relaxed-dot.wasm new file mode 100644 index 0000000000000000000000000000000000000000..5aa116a8d85b396b99e9782bcd8e8afb66cd3764 GIT binary patch literal 191 zcmZQbEY4+QU|?VrVNPIRtWRL92NG=cV8B?<%*M*V$i%?F%EHLV$i(i(#+I9!n_pDP z#K2yjm>Hj#l*z!r31;Qw#Qf<=o;^B9=8L8AGkCGiC%MGVYvUQTKr0}GcYD+_}o jBR7y>;5KIX%LB9@1z-`G#3bd&;HYKA0MY~22sQ!$eOe?i literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/relaxed-laneselect.wasm b/wai/wai-module-check/planted/relaxed-laneselect.wasm new file mode 100644 index 0000000000000000000000000000000000000000..cc8dd5783754a1bb9fd6ebd53254e22f29b02546 GIT binary patch literal 209 zcma)#I}XAy5JYF!p9oAz#Su6HoeQ`GMPg8jNOp`&B1Gk$J0sz^K%!%c(atO0!rcP_ zpsnaYxuaZ4=NigFD-Z)p5)n5itwSGTdNP`a8(Mc6fK|P`k5^EoX&%95p>dwt+ms-_ i%l9MX`m7`@nNl!Eyf@|lPyQk=-dWiF0gI)os`LW@*(Fr~ literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/relaxed-madd.wasm b/wai/wai-module-check/planted/relaxed-madd.wasm new file mode 100644 index 0000000000000000000000000000000000000000..9112ecdae5673039355d07b586270d46cf042857 GIT binary patch literal 209 zcma)#I}XAy5JYF!p9oAz#Su6HoeQ`GMPg8jNOp`&B1GkiVdwt+ms-_ i%l9MX`m7`@nNl!Eyf@|lPyQk=-dWiF0gI)os`LW@W+hMn literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/relaxed-swizzle.wasm b/wai/wai-module-check/planted/relaxed-swizzle.wasm new file mode 100644 index 0000000000000000000000000000000000000000..a621e19c89941465aac6c77d37125675d3b8cfe4 GIT binary patch literal 191 zcmZvVy$S*`5QJwpKZnNB%15xZvr8lR6n9asI7luM?+~l_;)1ypg5VUx><2RocMk-B zwxR>&j&d=bt0)VtKny5JMBJRT4t%vy!l6ioqQ4-jx48`a@p4v#|RkmQF3!i4S|cBpv_& literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/scalar-float.wasm b/wai/wai-module-check/planted/scalar-float.wasm new file mode 100644 index 0000000000000000000000000000000000000000..241b0b56a4d33f7cb0c3c30e1aab249dd252574f GIT binary patch literal 163 zcmX|%O$x#=5QX35uV}V{;1L8b;6{VsHQFd$6p}__i@1ts@WiIGa26l$eQ)5OkpR#} zcA(NxsW63)iZmJ|0Ii5fG*@F{A5(q{G%r82{x$$BP9dZ_h;5!n2)o!cPwivMkpC9? e5o&$V3XW_A>=qZ`bE?4kyK`{+BNopizx@Eie5JmrALZapXUckyD*wJ_mhzH;#n+%{Iy8Y|uubE{t4sgE8@}9qhww=Rz>6NiI literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/table-fill.wasm b/wai/wai-module-check/planted/table-fill.wasm new file mode 100644 index 0000000000000000000000000000000000000000..bd5bdb112ab7023ed0fc622865b7b4e8290a5f02 GIT binary patch literal 167 zcmX|%I}XAy5JYGEi@+69PLU(fx#1d#K`A0Rabyx9DqoQUQQ){>i>H~l1OJ=}fUO+B zJTMoST#s2A4GKVMu4SbaNzvSlna4S%w?OmqQ}6E+aH=VU_yDU-`vPGP8~3eWw*>ib dVO*fjomOzP1+Z()c%M}|dL%I9_#JVF? literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/table-set.wasm b/wai/wai-module-check/planted/table-set.wasm new file mode 100644 index 0000000000000000000000000000000000000000..cd175fdc4b96ab275b46077b0ac9aeedf6476fe1 GIT binary patch literal 164 zcmX|%I}XAy07LEkD#(Py89?F)Y+blU8&HQzNmHe*5L2$mkw`P(;mLk7+!6?YXW4_f zXD%?ghFKa73P5Sj<)sx#(L9U^Lx|}k(7fH)x#tKRYV$t6z-rSrLD=2KZSCeYLH?H? aCaB|8E3~u)u&09Wd?{>ickHI>diVipr6N%P literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/table-unfixed.wasm b/wai/wai-module-check/planted/table-unfixed.wasm new file mode 100644 index 0000000000000000000000000000000000000000..bb39404be834b931cedeb7c4c403f5845219715f GIT binary patch literal 158 zcmX|$Jr2S!7(?y+RgjenuyO>pE?lDxs6(ZssX{Bnl&h0|10J62XM}em0ABP6){(Wr zRSBzh7F2+-TnSo3QgsjK(v))fDs-PP58*ijCuuR}7bv#u3zR=>-nU`h3iN-)X@NOk StwB%U0Ph?6+Z{(2A=eLxKp>w0 literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/tail-call.wasm b/wai/wai-module-check/planted/tail-call.wasm new file mode 100644 index 0000000000000000000000000000000000000000..e8be637e5d0e1f83adc807b949fe9652e79b0857 GIT binary patch literal 153 zcmX|$y$*sf0EF-QN3?MDR$Z+~itcGlm_tlof$nt6=w1uZx8!|%gUzO6g|OAeV;{FYLH;j4 WuTYnpRv2gtU~R#0f1u_j+Up11^dS@g literal 0 HcmV?d00001 diff --git a/wai/wai-module-check/planted/vector-int.wasm b/wai/wai-module-check/planted/vector-int.wasm new file mode 100644 index 0000000000000000000000000000000000000000..cde1a7c50954ce80a89cc0f58b80eed7d93ae2d9 GIT binary patch literal 327 zcma)%OAdlS5JaozhcJ9Lt~i26aL2}L02&q~d<;U2t4X|-p27>6ILyMt$bwo_x?j4I zYLu6j0MM2fAXAXBri>FAt|W*7QVq*v#_P@^`xqBec^f~_VH79pVs}b2 NWV=1)>aM^0 Date: Thu, 5 Nov 2026 08:00:20 -0500 Subject: [PATCH 04/12] wai-module-check: the validation limits' corpus, built from source MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `build.py --limits DIR` writes, for each validation limit of deterministic-modules §4.2, minimal-int with the part it bounds at the limit and one past it, and the verdicts by construction: at the limit, the rule the part breaks, if any; one past it, refused R2. The modules reach 10 MB, so the corpus is generated where it is checked and not committed. The planted set's bytes are unchanged (`build.py --check`): the joining of bytes is now linear, which the limits' million-entry sections need. Co-Authored-By: Claude Opus 5.5 --- wai/wai-module-check/planted/build.py | 182 +++++++++++++++++++++++++- 1 file changed, 176 insertions(+), 6 deletions(-) diff --git a/wai/wai-module-check/planted/build.py b/wai/wai-module-check/planted/build.py index cea99f411..9b2f5661f 100644 --- a/wai/wai-module-check/planted/build.py +++ b/wai/wai-module-check/planted/build.py @@ -19,8 +19,16 @@ levels gives a line at each. Lines §9.1 does not state but §4.3 decides are ma 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 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. """ @@ -57,10 +65,14 @@ def b(*xs): def cat(*blobs): - out = Blob() + data, marks, at = [], {}, 0 for x in blobs: - out = out + x - return out + 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): @@ -198,6 +210,7 @@ class Module: 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() @@ -238,6 +251,8 @@ class Module: 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) @@ -530,10 +545,165 @@ def outputs(): 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]", file=sys.stderr) + 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"} -- 2.54.0 (Apple Git-157) From a82675f59c4c45432581f4d8b415f1c50c6df34f Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 5 Nov 2026 08:04:16 -0500 Subject: [PATCH 05/12] wai-module-check: the Rust checker of the deterministic module profile MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A module's verdict at the integer or the float level under caps (deterministic-modules §4.3): R1 on the length; R2 by the validator of wasmparser 0.262.0, pinned exactly, with the features of WebAssembly 3.0 and no others (its WASM3 set less threads, which 3.0 does not define), whose limits are the profile's validation limits; then R3 to R12 over the module's items in binary order, read from the same parser with each item's offset, an instruction classed by its name and proposal as the parser lists them; then the absences R6 and R10 at the module's length. `findings` lists every rule every item breaks, the first being the verdict. The binary prints a verdict, the level a sink holds a module at (§6 check 9b), or checks a cases.txt. tests/module_rules.rs holds it to planted/cases.txt: every module gets its stated verdict at each level and under each caps; every planted module breaks exactly its row's rule (the two rows §9.1 says break a second, and the relaxed instruction that takes float lanes, named); every rule R1 to R12 has a planted module; the levels differ only in R3. A unit test holds R12's list to every instruction of the proposals it names. examples/differential.rs is the differential's first half: modules from wasm-smith 0.262.0 and this checker's verdicts, from a committed seed. Co-Authored-By: Claude Opus 5.5 --- wai/wai-module-check/Cargo.lock | 146 ++++ wai/wai-module-check/Cargo.toml | 22 + wai/wai-module-check/examples/differential.rs | 231 +++++++ wai/wai-module-check/src/lib.rs | 623 ++++++++++++++++++ wai/wai-module-check/src/main.rs | 137 ++++ wai/wai-module-check/tests/module_rules.rs | 193 ++++++ 6 files changed, 1352 insertions(+) create mode 100644 wai/wai-module-check/Cargo.lock create mode 100644 wai/wai-module-check/Cargo.toml create mode 100644 wai/wai-module-check/examples/differential.rs create mode 100644 wai/wai-module-check/src/lib.rs create mode 100644 wai/wai-module-check/src/main.rs create mode 100644 wai/wai-module-check/tests/module_rules.rs diff --git a/wai/wai-module-check/Cargo.lock b/wai/wai-module-check/Cargo.lock new file mode 100644 index 000000000..9d87d98ca --- /dev/null +++ b/wai/wai-module-check/Cargo.lock @@ -0,0 +1,146 @@ +# 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 = "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 = "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 = "wai-module-check" +version = "0.1.0" +dependencies = [ + "arbitrary", + "wasm-smith", + "wasmparser", +] + +[[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", +] diff --git a/wai/wai-module-check/Cargo.toml b/wai/wai-module-check/Cargo.toml new file mode 100644 index 000000000..4b34ecab3 --- /dev/null +++ b/wai/wai-module-check/Cargo.toml @@ -0,0 +1,22 @@ +[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" + +[[example]] +name = "differential" +path = "examples/differential.rs" diff --git a/wai/wai-module-check/examples/differential.rs b/wai/wai-module-check/examples/differential.rs new file mode 100644 index 000000000..66afe4563 --- /dev/null +++ b/wai/wai-module-check/examples/differential.rs @@ -0,0 +1,231 @@ +//! The differential's first half: modules from wasm-smith, and this checker's verdicts. +//! +//! cargo run --release --example differential -- --out DIR [--count N] [--seed HEX] +//! +//! Writes `DIR/.wasm` for i in 0..N (10,000 by default) and `DIR/verdicts.txt`, one line +//! a module: ` | `. `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. +//! +//! 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 { + 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, 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!() +} + +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 seed) = (None, 10_000u64, 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"), + "--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] [--seed HEX]"), + } + } + let out = out.expect("--out DIR"); + std::fs::create_dir_all(&out).expect("the output directory"); + let mut lines = String::new(); + for i in 0..count { + let (bytes, caps) = generate(seed, i); + std::fs::write(out.join(format!("{i}.wasm")), &bytes).expect("a module"); + let int = check(&bytes, Level::Integer, &caps); + let float = check(&bytes, Level::Float, &caps); + writeln!(lines, "{i} {} {int} | {float}", caps_text(&caps)).unwrap(); + } + std::fs::write(out.join("verdicts.txt"), lines).expect("verdicts.txt"); + println!("differential: {count} modules from seed {seed:#018x} in {}", out.display()); +} diff --git a/wai/wai-module-check/src/lib.rs b/wai/wai-module-check/src/lib.rs new file mode 100644 index 000000000..e3c83f3c7 --- /dev/null +++ b/wai/wai-module-check/src/lib.rs @@ -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 ` (§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 { + 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 { + 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, + }, +} + +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, 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, 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); 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, Vec); + +struct Scan<'a> { + bytes: &'a [u8], + level: Level, + caps: Caps, + found: Vec, + /// Each type index's function type, where its entry is a plain function type (`None` + /// for an entry R12 refuses). + types: Vec>, + /// Each function index's type index, imported functions first. + funcs: Vec, + /// The memories the module defines. + memories: u32, + /// Which exports of §5 the module has. + exported: [bool; 6], +} + +type R = Result; + +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> { + 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 { + 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" + ))); + } +} diff --git a/wai/wai-module-check/src/main.rs b/wai/wai-module-check/src/main.rs new file mode 100644 index 000000000..fcddc0e47 --- /dev/null +++ b/wai/wai-module-check/src/main.rs @@ -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 `), 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` (` `, +//! the module being `DIR/.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, 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 ` `", 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 = 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::::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 + } +} diff --git a/wai/wai-module-check/tests/module_rules.rs b/wai/wai-module-check/tests/module_rules.rs new file mode 100644 index 000000000..621cdd272 --- /dev/null +++ b/wai/wai-module-check/tests/module_rules.rs @@ -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 { + 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 { + 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 = 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::().is_ok_and(|n| (1..=12).contains(&n)) + && (at == "-" || at.bytes().all(|b| b.is_ascii_digit())) + }); + assert!(ok, "{v:?}"); + } +} -- 2.54.0 (Apple Git-157) From 6080cefd2a71dca358ac173b99531042166ad0c4 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 5 Nov 2026 08:04:23 -0500 Subject: [PATCH 06/12] wai-module-check: check-module.mjs, the second checker, and the differential MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit check-module.mjs generalises wai-vector's check-mvp.mjs, which reads a module of WebAssembly 1.0, to WebAssembly 3.0 and to the profile's rules, with no dependency: an ES module a page imports (check, levelOf) and a command line like the Rust checker's. It decodes every section and instruction and validates the module as WebAssembly 3.0 does, written from that text: recursion groups canonicalised so that equivalent types are one, subtyping over the abstract and the defined heap types, typed and untyped stacks, local initialisation, the constant expressions, and the validation limits of §4.2. While it validates it records each item that breaks R3 to R12, with the level and the cap the item depends on, so one reading serves both levels. differential.mjs is the differential's second half: it runs check-module.mjs on every module examples/differential.rs writes, at both levels under the same caps, and names each verdict that differs. On the committed seed the two checkers agree on all 20,000 verdicts of 10,000 modules. Co-Authored-By: Claude Opus 5.5 --- wai/wai-module-check/check-module.mjs | 1374 +++++++++++++++++++++++++ wai/wai-module-check/differential.mjs | 55 + 2 files changed, 1429 insertions(+) create mode 100644 wai/wai-module-check/check-module.mjs create mode 100644 wai/wai-module-check/differential.mjs diff --git a/wai/wai-module-check/check-module.mjs b/wai/wai-module-check/check-module.mjs new file mode 100644 index 000000000..c10fc47d3 --- /dev/null +++ b/wai/wai-module-check/check-module.mjs @@ -0,0 +1,1374 @@ +// check-module.mjs: a module's verdict under WAI's deterministic module profile +// (wai/extensions/deterministic-modules.md), with no dependency. It is the checker a page +// runs before it instantiates a decoder module, and the second implementation beside the +// Rust checker of this directory, written from the profile's text and from WebAssembly 3.0, +// sharing no code with it. It generalises wai-vector's check-mvp.mjs, which reads a module +// of WebAssembly 1.0, to every construct of WebAssembly 3.0 and to the profile's rules. +// +// The verdict for a module at a level under caps (§4.3) is one line of ASCII: `held`, or +// `refused R `: +// 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 under WebAssembly 3.0's binary format, or is not +// valid, within the validation limits of §4.2, is `refused R2 -`. This file decodes +// every section and instruction and validates them as WebAssembly 3.0 does, the types +// of garbage collection, exception handling and typed function references included. +// 3. R3 to R12 over the module's items in binary order: the first item that breaks one is +// refused at its offset, by the lowest-numbered rule it breaks. +// 4. Then R6 where the module defines no memory, and R10 where an export of §5 is +// missing, at the offset equal to the module's length. +// +// In a page: import { check, levelOf } from './check-module.mjs'; +// check(bytes, 'integer') → 'held' | 'refused R ' +// From a shell: node check-module.mjs [--level integer|float] [--caps NAME=VALUE,...] FILE... +// node check-module.mjs --cases DIR +// +// With --level, one verdict line a file; without it, the level a sink holds the module at +// (§6, check 9b) or the verdict that refuses it. --cases checks every line of DIR/cases.txt +// (` `; the module is DIR/.wasm). Exit status: 0 when +// every module is held (with --cases, when every verdict is the one stated), 1 otherwise, +// 2 for a usage or input error. + +/** The profile's caps (§4.2). */ +export const PROFILE_CAPS = Object.freeze({ module_bytes: 16777216, functions: 50000, memory_pages: 65536 }); + +/** The validation limits of §4.2, part of R2. */ +const LIMIT = Object.freeze({ + types: 1000000, functions: 1000000, globals: 1000000, tags: 1000000, + tables: 100000, memories: 100, elems: 100000, datas: 100000, segmentItems: 10000000, + name: 100000, body: 7654321, locals: 50000, params: 1000, results: 1000, + fields: 10000, catches: 10000, depth: 63, interface: 999998, +}); + +/** The exports of §5: name, kind (0 a function, 2 the memory) and a function's type. */ +const ABI = [ + ['memory', 2, null], + ['wai_abi', 0, [[], ['i32']]], + ['wai_alloc', 0, [['i32'], ['i32']]], + ['wai_run', 0, [['i32', 'i32', 'i32', 'i32', 'i32', 'i32'], ['i32']]], + ['wai_out_ptr', 0, [[], ['i32']]], + ['wai_out_len', 0, [[], ['i32']]], +]; + +// A module outside R2: one that does not decode, or is not valid. The message is for a +// reader of this file; the verdict carries none of it. +class Refused2 extends Error {} +function bad(why) { throw new Refused2(why); } + +// ------------------------------------------------------------------------------ bytes + +class Reader { + constructor(b, at, end) { this.b = b; this.at = at; this.end = end; } + eof() { return this.at >= this.end; } + byte() { if (this.at >= this.end) bad('unexpected end'); return this.b[this.at++]; } + peek() { if (this.at >= this.end) bad('unexpected end'); return this.b[this.at]; } + skip(n) { if (n > this.end - this.at) bad('unexpected end'); this.at += n; } + // Unsigned LEB128 of 32 bits: at most 5 bytes, the unused bits of the last zero. + u32() { + let v = 0, scale = 1; + for (let i = 0; i < 5; i++) { + const c = this.byte(); + if (i === 4 && (c & 0xf0) !== 0) bad('u32 too large'); + v += (c & 0x7f) * scale; + if (!(c & 0x80)) return v; + scale *= 128; + } + return v; + } + // Unsigned LEB128 of 64 bits, exact, as a BigInt: at most 10 bytes. + u64() { + let v = 0n, shift = 0n; + for (let i = 0; i < 10; i++) { + const c = this.byte(); + if (i === 9 && (c & 0xfe) !== 0) bad('u64 too large'); + v |= BigInt(c & 0x7f) << shift; + if (!(c & 0x80)) return v; + shift += 7n; + } + return v; + } + // The same encoding, as a Number: exact below 2^53, which is all a comparison here needs. + u64n() { + let v = 0, scale = 1; + for (let i = 0; i < 10; i++) { + const c = this.byte(); + if (i === 9 && (c & 0xfe) !== 0) bad('u64 too large'); + v += (c & 0x7f) * scale; + if (!(c & 0x80)) return v; + scale *= 128; + } + return v; + } + // Signed LEB128: at most `max` bytes, the unused bits of the last a sign extension; the + // last byte's bits from `keep` up must all equal bit `keep - 1`. Returns the value as a + // Number (s33 is exact; s32 and s64 values are not used). + signed(max, keep) { + let v = 0, scale = 1; + for (let i = 0; i < max; i++) { + const c = this.byte(); + if (i === max - 1) { + if (c & 0x80) bad('signed LEB128 too long'); + const high = c >> (keep - 1); // bit keep-1 up to bit 6 + if (high !== 0 && high !== (0x7f >> (keep - 1))) bad('signed LEB128 too large'); + } + v += (c & 0x7f) * scale; + scale *= 128; + if (!(c & 0x80)) return (c & 0x40) ? v - scale : v; + } + return v; + } + s32() { return this.signed(5, 4); } + s33() { return this.signed(5, 5); } + s64() { return this.signed(10, 1); } + // A name: a vector of bytes that is UTF-8, at most the name limit long. + name() { + const n = this.u32(); + if (n > LIMIT.name) bad('name too long'); + if (n > this.end - this.at) bad('unexpected end'); + utf8(this.b, this.at, this.at + n); + const s = this.at; + this.at += n; + return String.fromCharCode.apply(null, Array.from(this.b.subarray(s, s + n))); + } +} + +// Valid UTF-8: no overlong form, no surrogate, nothing above U+10FFFF. +function utf8(b, at, end) { + while (at < end) { + const c = b[at]; + if (c < 0x80) { at++; continue; } + let n, min; + if (c >= 0xc2 && c <= 0xdf) { n = 1; min = 0x80; } + else if (c >= 0xe0 && c <= 0xef) { n = 2; min = 0x800; } + else if (c >= 0xf0 && c <= 0xf4) { n = 3; min = 0x10000; } + else bad('not UTF-8'); + if (at + n >= end) bad('not UTF-8'); + let cp = c & (0x3f >> n); + for (let i = 1; i <= n; i++) { + const d = b[at + i]; + if ((d & 0xc0) !== 0x80) bad('not UTF-8'); + cp = cp * 64 + (d & 0x3f); + } + if (cp < min || cp > 0x10ffff || (cp >= 0xd800 && cp <= 0xdfff)) bad('not UTF-8'); + at += n + 1; + } +} + +// ------------------------------------------------------------------------------ types +// +// A value type is a string ('i32', 'i64', 'f32', 'f64', 'v128'), 'bot' (the unknown type of +// an unreachable operand), or a reference {nullable, heap}: heap is an abstract heap type +// ('func', 'nofunc', 'extern', 'noextern', 'any', 'eq', 'i31', 'struct', 'array', 'none', +// 'exn', 'noexn', or 'bot') or a canonical type id, a number: two type indices whose +// definitions are equivalent (iso-recursively, by their recursion groups) have one id. + +const ABSTRACT = { + 0x70: 'func', 0x6f: 'extern', 0x6e: 'any', 0x6d: 'eq', 0x6c: 'i31', 0x6b: 'struct', + 0x6a: 'array', 0x69: 'exn', 0x73: 'nofunc', 0x72: 'noextern', 0x71: 'none', 0x74: 'noexn', +}; +const NUMTYPE = { 0x7f: 'i32', 0x7e: 'i64', 0x7d: 'f32', 0x7c: 'f64', 0x7b: 'v128' }; +const FUNCREF = Object.freeze({ nullable: true, heap: 'func' }); +const BOTREF = Object.freeze({ nullable: false, heap: 'bot' }); +const isValTypeByte = (c) => c in NUMTYPE || c in ABSTRACT || c === 0x63 || c === 0x64; +const isRef = (t) => typeof t === 'object'; +const isFloat = (t) => t === 'f32' || t === 'f64'; + +function analyze(b) { + const findings = []; // {at, rule, int?, cap?, value?} + const canon = []; // canonical types: {kind, params, results, fields, final, sup, depth} + const groups = new Map(); + const types = []; // type index → canonical id + const funcs = []; // function index → canonical id of its type + const tables = []; // {at: 'i32'|'i64', elem} + const mems = []; // {at} + const tags = []; // canonical id + const globals = []; // {type, mut} + const elems = []; // reference type + const refs = new Set(); + let dataCount = null, dataSegments = null, definedFuncs = null, codeEntries = null; + let nImportedFuncs = 0, definedMems = 0, iface = 1; + const exported = new Set(), abiSeen = new Set(); + + const valueItem = (t, at) => { + if (isFloat(t)) findings.push({ at, rule: 3, int: true }); + else if (isRef(t)) findings.push({ at, rule: 9 }); + }; + const addInterface = (n) => { iface += n; if (iface > LIMIT.interface + 1) bad('interface size'); }; + const funcType = (x) => { + if (x >= types.length) bad('unknown type'); + const id = types[x]; + if (canon[id].kind !== 'func') bad('not a function type'); + return canon[id]; + }; + + // -------------------------------------------------------------------- subtyping + function subHeap(a, c) { + if (a === c || a === 'bot') return true; + if (c === 'bot') return false; + if (typeof a === 'number') { + if (typeof c === 'number') { + for (let x = canon[a].sup; x !== null; x = canon[x].sup) if (x === c) return true; + return false; + } + const k = canon[a].kind; + if (k === 'func') return c === 'func'; + if (k === 'struct') return c === 'struct' || c === 'eq' || c === 'any'; + return c === 'array' || c === 'eq' || c === 'any'; + } + if (typeof c === 'number') return canon[c].kind === 'func' ? a === 'nofunc' : a === 'none'; + switch (a) { + case 'none': return c === 'i31' || c === 'struct' || c === 'array' || c === 'eq' || c === 'any'; + case 'i31': case 'struct': case 'array': return c === 'eq' || c === 'any'; + case 'eq': return c === 'any'; + case 'nofunc': return c === 'func'; + case 'noextern': return c === 'extern'; + case 'noexn': return c === 'exn'; + default: return false; + } + } + function sub(a, c) { + if (a === 'bot') return true; + if (typeof a === 'string' || typeof c === 'string') return a === c; + return (!a.nullable || c.nullable) && subHeap(a.heap, c.heap); + } + const same = (a, c) => (typeof a === 'string' ? a === c : typeof c === 'object' && a.nullable === c.nullable && a.heap === c.heap); + const sameStorage = (a, c) => same(a, c); + const subStorage = (a, c) => (a === 'i8' || a === 'i16' || c === 'i8' || c === 'i16' ? a === c : sub(a, c)); + const fieldMatch = (f, g) => f.mut === g.mut && (f.mut ? sameStorage(f.st, g.st) : subStorage(f.st, g.st)); + function compMatch(e, s) { + if (e.kind !== s.kind) return false; + if (e.kind === 'func') { + return e.params.length === s.params.length && e.results.length === s.results.length + && e.params.every((t, i) => sub(s.params[i], t)) && e.results.every((t, i) => sub(t, s.results[i])); + } + if (e.kind === 'struct') return e.fields.length >= s.fields.length && s.fields.every((g, i) => fieldMatch(e.fields[i], g)); + return fieldMatch(e.fields[0], s.fields[0]); + } + function top(h) { + if (typeof h === 'number') return canon[h].kind === 'func' ? 'func' : 'any'; + switch (h) { + case 'func': case 'nofunc': return 'func'; + case 'extern': case 'noextern': return 'extern'; + case 'exn': case 'noexn': return 'exn'; + default: return 'any'; + } + } + const unpack = (st) => (st === 'i8' || st === 'i16' ? 'i32' : st); + const defaultable = (t) => !isRef(t) || t.nullable; + + // -------------------------------------------------------------------- reading types + function heapType(r, raw) { + const c = r.peek(); + if (c in ABSTRACT) { r.at++; return ABSTRACT[c]; } + const x = r.s33(); + if (x < 0) bad('bad heap type'); + if (raw) return { mod: x }; + if (x >= types.length) bad('unknown type'); + return types[x]; + } + function valType(r, raw) { + const c = r.byte(); + if (c in NUMTYPE) return NUMTYPE[c]; + if (c in ABSTRACT) return { nullable: true, heap: ABSTRACT[c] }; + if (c === 0x63 || c === 0x64) return { nullable: c === 0x63, heap: heapType(r, raw) }; + bad('bad value type'); + } + function refType(r) { + const t = valType(r, false); + if (!isRef(t)) bad('not a reference type'); + return t; + } + function storageType(r) { + const c = r.peek(); + if (c === 0x78) { r.at++; return 'i8'; } + if (c === 0x77) { r.at++; return 'i16'; } + return valType(r, true); + } + function mutability(r) { + const m = r.byte(); + if (m > 1) bad('bad mutability'); + return m === 1; + } + + // One subtype of a type entry; the value types of a plain function type with their offsets. + function subType(r) { + let final = true, supers = []; + let c = r.byte(); + if (c === 0x50 || c === 0x4f) { + final = c === 0x4f; + const n = r.u32(); + if (n > 1) bad('more than one supertype'); + for (let i = 0; i < n; i++) supers.push(r.u32()); + c = r.byte(); + } + const items = []; + if (c === 0x60) { + const lists = []; + for (const limit of [LIMIT.params, LIMIT.results]) { + const n = r.u32(); + if (n > limit) bad('too many parameters or results'); + const ts = []; + for (let i = 0; i < n; i++) { const at = r.at; const t = valType(r, true); items.push([t, at]); ts.push(t); } + lists.push(ts); + } + return { final, supers, kind: 'func', params: lists[0], results: lists[1], fields: null, items }; + } + if (c === 0x5f) { + const n = r.u32(); + if (n > LIMIT.fields) bad('too many fields'); + const fields = []; + for (let i = 0; i < n; i++) { const st = storageType(r); fields.push({ st, mut: mutability(r) }); } + return { final, supers, kind: 'struct', params: null, results: null, fields, items }; + } + if (c === 0x5e) { + const st = storageType(r); + return { final, supers, kind: 'array', params: null, results: null, fields: [{ st, mut: mutability(r) }], items }; + } + bad('bad composite type'); + } + + // A recursion group: bounds, canonical ids (one per equivalent group), then validity. + function defineGroup(subs) { + const base = types.length, n = subs.length; + const hk = (h) => (typeof h === 'string' ? h : (h.mod >= base ? 'r' + (h.mod - base) : 'c' + types[h.mod])); + const vk = (t) => (typeof t === 'string' ? t : (t.nullable ? '?' : '!') + hk(t.heap)); + const check = (t) => { if (isRef(t) && typeof t.heap === 'object' && t.heap.mod >= base + n) bad('unknown type'); }; + subs.forEach((s, k) => { + for (const x of s.supers) if (x >= base + k) bad('supertypes must be defined before subtypes'); + (s.params || []).forEach(check); (s.results || []).forEach(check); + (s.fields || []).forEach((f) => check(f.st)); + }); + const key = subs.map((s) => (s.final ? 'F' : 'N') + s.supers.map((x) => hk({ mod: x })).join(',') + ':' + s.kind + '(' + + (s.kind === 'func' ? s.params.map(vk).join(',') + ')(' + s.results.map(vk).join(',') + : s.fields.map((f) => (f.mut ? 'm' : 'c') + vk(f.st)).join(',')) + ')').join('|'); + let start = groups.get(key); + const fresh = start === undefined; + if (fresh) { + start = canon.length; + groups.set(key, start); + const cv = (t) => (typeof t === 'string' ? t + : { nullable: t.nullable, heap: typeof t.heap === 'string' ? t.heap : (t.heap.mod >= base ? start + t.heap.mod - base : types[t.heap.mod]) }); + for (const s of subs) { + canon.push({ + kind: s.kind, final: s.final, depth: 0, + sup: s.supers.length ? (s.supers[0] >= base ? start + s.supers[0] - base : types[s.supers[0]]) : null, + params: s.params && s.params.map(cv), results: s.results && s.results.map(cv), + fields: s.fields && s.fields.map((f) => ({ st: f.st === 'i8' || f.st === 'i16' ? f.st : cv(f.st), mut: f.mut })), + }); + } + } + for (let k = 0; k < n; k++) types.push(start + k); + if (!fresh) return; + for (let k = 0; k < n; k++) { + const e = canon[start + k]; + if (e.sup === null) continue; + const s = canon[e.sup]; + if (s.final) bad('final supertype'); + if (!compMatch(e, s)) bad('subtype does not match its supertype'); + e.depth = s.depth + 1; + if (e.depth > LIMIT.depth) bad('subtype too deep'); + } + } + + function limits(r, i64Bound) { + const flags = r.byte(); + if (flags !== 0 && flags !== 1 && flags !== 4 && flags !== 5) bad('bad limits'); + const at = flags & 4 ? 'i64' : 'i32'; + const read = () => (at === 'i64' ? r.u64() : BigInt(r.u32())); + const min = read(); + const max = flags & 1 ? read() : null; + if (max !== null && min > max) bad('minimum above maximum'); + const bound = at === 'i64' ? i64Bound : (i64Bound === null ? null : 65536n); + if (bound !== null && (min > bound || (max !== null && max > bound))) bad('memory too large'); + return { at, min, max }; + } + const memType = (r) => limits(r, 1n << 48n); + function tableType(r) { + const elem = refType(r); + const l = limits(r, null); + return { at: l.at, min: l.min, max: l.max, elem }; + } + function globalType(r) { + const type = valType(r, false); + return { type, mut: mutability(r) }; + } + + // -------------------------------------------------------------------- constant expressions + function constExpr(r, expect) { + const st = []; + const pop = (t) => { if (!st.length) bad('constant: empty stack'); const v = st.pop(); if (!sub(v, t)) bad('constant: type mismatch'); return v; }; + for (;;) { + const at = r.at, op = r.byte(); + switch (op) { + case 0x0b: + if (st.length !== 1 || !sub(st[0], expect)) bad('constant: type mismatch'); + return; + case 0x41: r.s32(); st.push('i32'); break; + case 0x42: r.s64(); st.push('i64'); break; + case 0x43: r.skip(4); st.push('f32'); findings.push({ at, rule: 3, int: true }); break; + case 0x44: r.skip(8); st.push('f64'); findings.push({ at, rule: 3, int: true }); break; + case 0x23: { + const x = r.u32(); + if (x >= globals.length) bad('unknown global'); + if (globals[x].mut) bad('constant: mutable global'); + st.push(globals[x].type); break; + } + case 0xd0: st.push({ nullable: true, heap: heapType(r, false) }); break; + case 0xd2: { + const x = r.u32(); + if (x >= funcs.length) bad('unknown function'); + refs.add(x); st.push({ nullable: false, heap: funcs[x] }); break; + } + case 0x6a: case 0x6b: case 0x6c: pop('i32'); pop('i32'); st.push('i32'); break; + case 0x7c: case 0x7d: case 0x7e: pop('i64'); pop('i64'); st.push('i64'); break; + case 0xfd: { + if (r.u32() !== 12) bad('constant expression required'); + r.skip(16); st.push('v128'); break; + } + case 0xfb: { + const s = r.u32(); + findings.push({ at, rule: 12 }); + if (s === 0 || s === 1) { + const x = r.u32(), e = gcType(x, 'struct'); + if (s === 0) for (let i = e.fields.length - 1; i >= 0; i--) pop(unpack(e.fields[i].st)); + else if (!e.fields.every((f) => defaultable(unpack(f.st)))) bad('not defaultable'); + st.push({ nullable: false, heap: types[x] }); + } else if (s === 6 || s === 7 || s === 8) { + const x = r.u32(), e = gcType(x, 'array'); + if (s === 6) { pop('i32'); pop(unpack(e.fields[0].st)); } + else if (s === 7) { pop('i32'); if (!defaultable(unpack(e.fields[0].st))) bad('not defaultable'); } + else { const k = r.u32(); for (let i = 0; i < k; i++) pop(unpack(e.fields[0].st)); } + st.push({ nullable: false, heap: types[x] }); + } else if (s === 28) { pop('i32'); st.push({ nullable: false, heap: 'i31' }); } + else if (s === 26 || s === 27) { + const from = s === 26 ? 'extern' : 'any', to = s === 26 ? 'any' : 'extern'; + const v = pop({ nullable: true, heap: from }); + st.push({ nullable: v.nullable, heap: to }); + } else bad('constant expression required'); + break; + } + default: bad('constant expression required'); + } + } + } + function gcType(x, kind) { + if (x >= types.length) bad('unknown type'); + const e = canon[types[x]]; + if (e.kind !== kind) bad(`not a ${kind} type`); + return e; + } + + // -------------------------------------------------------------------- function bodies + function body(r, typeId) { + const ft = canon[typeId]; + const locals = ft.params.slice(); + let count = locals.length; + for (let g = r.u32(); g > 0; g--) { + const n = r.u32(); + const at = r.at; + const t = valType(r, false); + valueItem(t, at); + count += n; + if (count > LIMIT.locals) bad('too many locals'); + for (let i = 0; i < n; i++) locals.push(t); + } + const inited = new Uint8Array(locals.length); + for (let i = 0; i < locals.length; i++) inited[i] = i < ft.params.length || defaultable(locals[i]) ? 1 : 0; + const initLog = []; + const vals = [], ctrls = []; + + const pushCtrl = (kind, start, end) => { + ctrls.push({ kind, start, end, height: vals.length, unreachable: false, init: initLog.length }); + for (const t of start) vals.push(t); + }; + const popVal = () => { + const f = ctrls[ctrls.length - 1]; + if (vals.length === f.height) { if (f.unreachable) return 'bot'; bad('type mismatch: empty stack'); } + return vals.pop(); + }; + const pop = (t) => { const v = popVal(); if (!sub(v, t)) bad('type mismatch'); return v; }; + const popVals = (ts) => { const out = new Array(ts.length); for (let i = ts.length - 1; i >= 0; i--) out[i] = pop(ts[i]); return out; }; + const pushVals = (ts) => { for (const t of ts) vals.push(t); }; + const popRef = () => { const v = popVal(); if (v === 'bot') return BOTREF; if (!isRef(v)) bad('type mismatch: not a reference'); return v; }; + const popCtrl = () => { + const f = ctrls[ctrls.length - 1]; + popVals(f.end); + if (vals.length !== f.height) bad('type mismatch: values left at the end of a block'); + ctrls.pop(); + while (initLog.length > f.init) inited[initLog.pop()] = 0; + return f; + }; + const labelTypes = (l) => { + if (l >= ctrls.length) bad('unknown label'); + const f = ctrls[ctrls.length - 1 - l]; + return f.kind === 'loop' ? f.start : f.end; + }; + const unreachable = () => { const f = ctrls[ctrls.length - 1]; vals.length = f.height; f.unreachable = true; }; + const blockType = () => { + const at = r.at, c = r.peek(); + if (c === 0x40) { r.at++; return [[], []]; } + if (isValTypeByte(c)) { + const t = valType(r, false); + if (isFloat(t)) findings.push({ at, rule: 3, int: true }); + return [[], [t]]; + } + const x = r.s33(); + if (x < 0) bad('bad block type'); + const e = funcType(x); + return [e.params, e.results]; + }; + const resultsMatch = (from, to) => from.length === to.length && from.every((t, i) => sub(t, to[i])); + const memarg = (natural) => { + let flags = r.u32(); + let mem = 0; + if ((flags & 0x40) !== 0) { flags -= 0x40; mem = r.u32(); } + if (flags >= 64) bad('alignment too large'); + const offset = r.u64n(); + if (mem >= mems.length) bad('unknown memory'); + if (flags > natural) bad('alignment above natural'); + const at = mems[mem].at; + if (at === 'i32' && offset > 0xffffffff) bad('offset out of range'); + return at; + }; + const memIdx = () => { const m = r.u32(); if (m >= mems.length) bad('unknown memory'); return mems[m].at; }; + const table = () => { const t = r.u32(); if (t >= tables.length) bad('unknown table'); return tables[t]; }; + const dataIdx = () => { const d = r.u32(); if (dataCount === null) bad('data count section required'); if (d >= dataCount) bad('unknown data segment'); }; + const elemIdx = () => { const e = r.u32(); if (e >= elems.length) bad('unknown element segment'); return elems[e]; }; + const tag = () => { const x = r.u32(); if (x >= tags.length) bad('unknown tag'); return canon[tags[x]]; }; + const local = () => { const x = r.u32(); if (x >= locals.length) bad('unknown local'); return x; }; + const global = () => { const x = r.u32(); if (x >= globals.length) bad('unknown global'); return globals[x]; }; + const callee = () => { const f = r.u32(); if (f >= funcs.length) bad('unknown function'); return canon[funcs[f]]; }; + const labelMatch = (ts, l) => { const lt = labelTypes(l); if (!resultsMatch(ts, lt)) bad('type mismatch: catch'); }; + const minAt = (a, c) => (a === 'i64' && c === 'i64' ? 'i64' : 'i32'); + + pushCtrl('func', [], ft.results); + for (;;) { + if (r.eof()) bad('function body ends before its end'); + const at = r.at, op = r.byte(); + if (op >= 0x45 && op <= 0xc4) { + const n = NUMERIC[op]; + if (!n) bad('unknown opcode'); + if (n[3]) findings.push({ at, rule: 3, int: true }); + popVals(n[1]); pushVals(n[2]); + } else if (op >= 0x28 && op <= 0x3e) { + const [, t, natural, store] = LOADSTORE[op - 0x28]; + if (t === 'f32' || t === 'f64') findings.push({ at, rule: 3, int: true }); + const a = memarg(natural); + if (store) { pop(t); pop(a); } else { pop(a); vals.push(t); } + } else switch (op) { + case 0x00: unreachable(); break; + case 0x01: break; + case 0x02: case 0x03: { const [p, q] = blockType(); popVals(p); pushCtrl(op === 0x02 ? 'block' : 'loop', p, q); break; } + case 0x04: { const [p, q] = blockType(); pop('i32'); popVals(p); pushCtrl('if', p, q); break; } + case 0x05: { const f = popCtrl(); if (f.kind !== 'if') bad('else without if'); pushCtrl('else', f.start, f.end); break; } + case 0x08: { findings.push({ at, rule: 12 }); const e = tag(); popVals(e.params); unreachable(); break; } + case 0x0a: { findings.push({ at, rule: 12 }); pop({ nullable: true, heap: 'exn' }); unreachable(); break; } + case 0x0b: { + let f = ctrls[ctrls.length - 1]; + if (f.kind === 'if') { popCtrl(); pushCtrl('else', f.start, f.end); } + f = popCtrl(); + pushVals(f.end); + break; + } + case 0x0c: { popVals(labelTypes(r.u32())); unreachable(); break; } + case 0x0d: { const lt = labelTypes(r.u32()); pop('i32'); popVals(lt); pushVals(lt); break; } + case 0x0e: { + const n = r.u32(); + const ls = []; + for (let i = 0; i < n; i++) ls.push(r.u32()); + const dflt = r.u32(); + pop('i32'); + const arity = labelTypes(dflt).length; + for (const l of ls) { + const lt = labelTypes(l); + if (lt.length !== arity) bad('br_table arity'); + pushVals(popVals(lt)); + } + popVals(labelTypes(dflt)); + unreachable(); + break; + } + case 0x0f: popVals(ft.results); unreachable(); break; + case 0x10: { const e = callee(); popVals(e.params); pushVals(e.results); break; } + case 0x11: case 0x13: { + if (op === 0x13) findings.push({ at, rule: 12 }); + const e = funcType(r.u32()), t = table(); + if (!sub(t.elem, FUNCREF)) bad('call_indirect of a table not of functions'); + pop(t.at); popVals(e.params); + if (op === 0x11) pushVals(e.results); + else { if (!resultsMatch(e.results, ft.results)) bad('return_call_indirect results'); unreachable(); } + break; + } + case 0x12: { + findings.push({ at, rule: 12 }); + const e = callee(); popVals(e.params); + if (!resultsMatch(e.results, ft.results)) bad('return_call results'); + unreachable(); break; + } + case 0x14: case 0x15: { + findings.push({ at, rule: 12 }); + const x = r.u32(), e = funcType(x); + pop({ nullable: true, heap: types[x] }); popVals(e.params); + if (op === 0x14) pushVals(e.results); + else { if (!resultsMatch(e.results, ft.results)) bad('return_call_ref results'); unreachable(); } + break; + } + case 0x1a: popVal(); break; + case 0x1b: { + pop('i32'); + const t1 = popVal(), t2 = popVal(); + const num = (t) => t === 'bot' || t === 'i32' || t === 'i64' || t === 'f32' || t === 'f64'; + const vec = (t) => t === 'bot' || t === 'v128'; + if (!((num(t1) && num(t2)) || (vec(t1) && vec(t2)))) bad('select of references'); + if (t1 !== t2 && t1 !== 'bot' && t2 !== 'bot') bad('select type mismatch'); + vals.push(t1 === 'bot' ? t2 : t1); + break; + } + case 0x1c: { + if (r.u32() !== 1) bad('select with other than one type'); + const tat = r.at; + const t = valType(r, false); + if (isFloat(t)) findings.push({ at: tat, rule: 3, int: true }); + pop('i32'); pop(t); pop(t); vals.push(t); + break; + } + case 0x1f: { + findings.push({ at, rule: 12 }); + const [p, q] = blockType(); + const n = r.u32(); + if (n > LIMIT.catches) bad('too many catches'); + for (let i = 0; i < n; i++) { + const kind = r.byte(); + if (kind > 3) bad('bad catch'); + const e = kind < 2 ? tag() : null; + const l = r.u32(); + const ts = e ? e.params.slice() : []; + if (kind === 1 || kind === 3) ts.push({ nullable: false, heap: 'exn' }); + labelMatch(ts, l); + } + popVals(p); pushCtrl('block', p, q); + break; + } + case 0x20: { const x = local(); if (!inited[x]) bad('uninitialized local'); vals.push(locals[x]); break; } + case 0x21: case 0x22: { + const x = local(); + pop(locals[x]); + if (!inited[x]) { inited[x] = 1; initLog.push(x); } + if (op === 0x22) vals.push(locals[x]); + break; + } + case 0x23: vals.push(global().type); break; + case 0x24: { const g = global(); if (!g.mut) bad('global.set of an immutable global'); pop(g.type); break; } + case 0x25: { const t = table(); pop(t.at); vals.push(t.elem); break; } + case 0x26: { findings.push({ at, rule: 7 }); const t = table(); pop(t.elem); pop(t.at); break; } + case 0x3f: vals.push(memIdx()); break; + case 0x40: { const a = memIdx(); pop(a); vals.push(a); break; } + case 0x41: r.s32(); vals.push('i32'); break; + case 0x42: r.s64(); vals.push('i64'); break; + case 0x43: r.skip(4); findings.push({ at, rule: 3, int: true }); vals.push('f32'); break; + case 0x44: r.skip(8); findings.push({ at, rule: 3, int: true }); vals.push('f64'); break; + case 0xd0: vals.push({ nullable: true, heap: heapType(r, false) }); break; + case 0xd1: popRef(); vals.push('i32'); break; + case 0xd2: { + const x = r.u32(); + if (x >= funcs.length) bad('unknown function'); + if (!refs.has(x)) bad('undeclared function reference'); + vals.push({ nullable: false, heap: funcs[x] }); + break; + } + case 0xd3: { findings.push({ at, rule: 12 }); const eq = { nullable: true, heap: 'eq' }; pop(eq); pop(eq); vals.push('i32'); break; } + case 0xd4: { findings.push({ at, rule: 12 }); const v = popRef(); vals.push({ nullable: false, heap: v.heap }); break; } + case 0xd5: { + findings.push({ at, rule: 12 }); + const lt = labelTypes(r.u32()); + const v = popRef(); + popVals(lt); pushVals(lt); + vals.push({ nullable: false, heap: v.heap }); + break; + } + case 0xd6: { + findings.push({ at, rule: 12 }); + const lt = labelTypes(r.u32()); + const last = lt[lt.length - 1]; + if (!lt.length || !isRef(last)) bad('br_on_non_null label'); + pop({ nullable: true, heap: last.heap }); + const rest = lt.slice(0, -1); + popVals(rest); pushVals(rest); + break; + } + case 0xfb: gcOp(at); break; + case 0xfc: miscOp(at); break; + case 0xfd: simdOp(at); break; + default: bad('unknown opcode'); + } + if (ctrls.length === 0) { + if (!r.eof()) bad('instructions after the end of the function'); + return; + } + } + + function miscOp(at) { + const s = r.u32(); + if (s <= 7) { + findings.push({ at, rule: 3, int: true }); + pop(s < 2 || s === 4 || s === 5 ? 'f32' : 'f64'); + vals.push(s < 4 ? 'i32' : 'i64'); + return; + } + switch (s) { + case 8: { dataIdx(); const a = memIdx(); pop('i32'); pop('i32'); pop(a); return; } + case 9: dataIdx(); return; + case 10: { const d = memIdx(), c = memIdx(); pop(minAt(d, c)); pop(c); pop(d); return; } + case 11: { const a = memIdx(); pop(a); pop('i32'); pop(a); return; } + case 12: { const e = elemIdx(), t = table(); if (!sub(e, t.elem)) bad('table.init type'); pop('i32'); pop('i32'); pop(t.at); return; } + case 13: elemIdx(); return; + case 14: { const d = table(), c = table(); if (!sub(c.elem, d.elem)) bad('table.copy type'); pop(minAt(d.at, c.at)); pop(c.at); pop(d.at); return; } + case 15: { findings.push({ at, rule: 7 }); const t = table(); pop(t.at); pop(t.elem); vals.push(t.at); return; } + case 16: vals.push(table().at); return; + case 17: { findings.push({ at, rule: 7 }); const t = table(); pop(t.at); pop(t.elem); pop(t.at); return; } + default: bad('unknown opcode'); + } + } + + function gcOp(at) { + const s = r.u32(); + findings.push({ at, rule: 12 }); + const ref = (x, nullable = true) => ({ nullable, heap: types[x] }); + const field = (e, i) => { if (i >= e.fields.length) bad('unknown field'); return e.fields[i]; }; + const packed = (f) => f.st === 'i8' || f.st === 'i16'; + switch (s) { + case 0: { const x = r.u32(), e = gcType(x, 'struct'); for (let i = e.fields.length - 1; i >= 0; i--) pop(unpack(e.fields[i].st)); vals.push(ref(x, false)); return; } + case 1: { const x = r.u32(), e = gcType(x, 'struct'); if (!e.fields.every((f) => defaultable(unpack(f.st)))) bad('not defaultable'); vals.push(ref(x, false)); return; } + case 2: case 3: case 4: { + const x = r.u32(), e = gcType(x, 'struct'), f = field(e, r.u32()); + if ((s === 2) === packed(f)) bad('struct.get of a packed field, or get_s of an unpacked one'); + pop(ref(x)); vals.push(unpack(f.st)); return; + } + case 5: { const x = r.u32(), e = gcType(x, 'struct'), f = field(e, r.u32()); if (!f.mut) bad('immutable field'); pop(unpack(f.st)); pop(ref(x)); return; } + case 6: { const x = r.u32(), e = gcType(x, 'array'); pop('i32'); pop(unpack(e.fields[0].st)); vals.push(ref(x, false)); return; } + case 7: { const x = r.u32(), e = gcType(x, 'array'); if (!defaultable(unpack(e.fields[0].st))) bad('not defaultable'); pop('i32'); vals.push(ref(x, false)); return; } + case 8: { const x = r.u32(), e = gcType(x, 'array'), n = r.u32(); for (let i = 0; i < n; i++) pop(unpack(e.fields[0].st)); vals.push(ref(x, false)); return; } + case 9: case 18: { + const x = r.u32(), e = gcType(x, 'array'); + dataIdx(); + if (isRef(e.fields[0].st)) bad('array of references from data'); + if (s === 18 && !e.fields[0].mut) bad('immutable array'); + if (s === 9) { pop('i32'); pop('i32'); vals.push(ref(x, false)); } else { pop('i32'); pop('i32'); pop('i32'); pop(ref(x)); } + return; + } + case 10: case 19: { + const x = r.u32(), e = gcType(x, 'array'), et = elemIdx(); + const st = e.fields[0].st; + if (!isRef(st) || !sub(et, st)) bad('element type'); + if (s === 19 && !e.fields[0].mut) bad('immutable array'); + if (s === 10) { pop('i32'); pop('i32'); vals.push(ref(x, false)); } else { pop('i32'); pop('i32'); pop('i32'); pop(ref(x)); } + return; + } + case 11: case 12: case 13: { + const x = r.u32(), f = gcType(x, 'array').fields[0]; + if ((s === 11) === packed(f)) bad('array.get of a packed element, or get_s of an unpacked one'); + pop('i32'); pop(ref(x)); vals.push(unpack(f.st)); return; + } + case 14: { const x = r.u32(), f = gcType(x, 'array').fields[0]; if (!f.mut) bad('immutable array'); pop(unpack(f.st)); pop('i32'); pop(ref(x)); return; } + case 15: pop({ nullable: true, heap: 'array' }); vals.push('i32'); return; + case 16: { const x = r.u32(), f = gcType(x, 'array').fields[0]; if (!f.mut) bad('immutable array'); pop('i32'); pop(unpack(f.st)); pop('i32'); pop(ref(x)); return; } + case 17: { + const x = r.u32(), d = gcType(x, 'array').fields[0], y = r.u32(), c = gcType(y, 'array').fields[0]; + if (!d.mut) bad('immutable array'); + if (!subStorage(c.st, d.st)) bad('array.copy types'); + pop('i32'); pop('i32'); pop(ref(y)); pop('i32'); pop(ref(x)); return; + } + case 20: case 21: case 22: case 23: { + const h = heapType(r, false); + pop({ nullable: true, heap: top(h) }); + vals.push(s < 22 ? 'i32' : { nullable: s === 23, heap: h }); + return; + } + case 24: case 25: { + const flags = r.byte(); + if (flags > 3) bad('bad cast flags'); + const lt = labelTypes(r.u32()); + const rt1 = { nullable: (flags & 1) !== 0, heap: heapType(r, false) }; + const rt2 = { nullable: (flags & 2) !== 0, heap: heapType(r, false) }; + if (!sub(rt2, rt1)) bad('br_on_cast types'); + const diff = { nullable: rt2.nullable ? false : rt1.nullable, heap: rt1.heap }; + const last = lt[lt.length - 1]; + if (!lt.length || !isRef(last)) bad('br_on_cast label'); + if (!sub(s === 24 ? rt2 : diff, last)) bad('br_on_cast label type'); + pop(rt1); + const rest = lt.slice(0, -1); + popVals(rest); pushVals(rest); + vals.push(s === 24 ? diff : rt2); + return; + } + case 26: case 27: { + const v = pop({ nullable: true, heap: s === 26 ? 'extern' : 'any' }); + const to = s === 26 ? 'any' : 'extern'; + vals.push(v === 'bot' || v.heap === 'bot' ? { nullable: false, heap: to } : { nullable: v.nullable, heap: to }); + return; + } + case 28: pop('i32'); vals.push({ nullable: false, heap: 'i31' }); return; + case 29: case 30: pop({ nullable: true, heap: 'i31' }); vals.push('i32'); return; + default: bad('unknown opcode'); + } + } + + function simdOp(at) { + const s = r.u32(); + const e = SIMD[s]; + if (!e) bad('unknown vector opcode'); + const [name, sig, a1, a2] = e; + if (name.includes('f32') || name.includes('f64')) findings.push({ at, rule: 3, int: true }); + if (s >= 0x100) findings.push({ at, rule: 4 }); + const lane = (n) => { if (r.byte() >= n) bad('lane index out of range'); }; + switch (sig) { + case 'load': { const a = memarg(a1); pop(a); vals.push('v128'); return; } + case 'store': { const a = memarg(a1); pop('v128'); pop(a); return; } + case 'const': r.skip(16); vals.push('v128'); return; + case 'shuffle': for (let i = 0; i < 16; i++) lane(32); pop('v128'); pop('v128'); vals.push('v128'); return; + case 'splat': pop(a1); vals.push('v128'); return; + case 'extract': lane(a2); pop('v128'); vals.push(a1); return; + case 'replace': lane(a2); pop(a1); pop('v128'); vals.push('v128'); return; + case 'loadlane': { const a = memarg(a1); lane(a2); pop('v128'); pop(a); vals.push('v128'); return; } + case 'storelane': { const a = memarg(a1); lane(a2); pop('v128'); pop(a); return; } + case 'un': pop('v128'); vals.push('v128'); return; + case 'bin': pop('v128'); pop('v128'); vals.push('v128'); return; + case 'tern': pop('v128'); pop('v128'); pop('v128'); vals.push('v128'); return; + case 'test': pop('v128'); vals.push('i32'); return; + case 'shift': pop('i32'); pop('v128'); vals.push('v128'); return; + default: bad('unknown vector opcode'); + } + } + } + + // -------------------------------------------------------------------- the sections + const r = new Reader(b, 0, b.length); + if (b.length < 8 || b[0] !== 0 || b[1] !== 0x61 || b[2] !== 0x73 || b[3] !== 0x6d) bad('no preamble'); + if (b[4] !== 1 || b[5] !== 0 || b[6] !== 0 || b[7] !== 0) bad('not version 1 of the binary format'); + r.at = 8; + // The order of the sections of WebAssembly 3.0, by id. + const ORDER = { 1: 1, 2: 2, 3: 3, 4: 4, 5: 5, 13: 6, 6: 7, 7: 8, 8: 9, 9: 10, 12: 11, 10: 12, 11: 13 }; + let last = 0; + while (!r.eof()) { + const idAt = r.at, id = r.byte(), size = r.u32(); + if (size > r.end - r.at) bad('section beyond the module'); + const s = new Reader(b, r.at, r.at + size); + r.at += size; + if (id === 0) { s.name(); continue; } + if (!ORDER[id]) bad('unknown section'); + if (ORDER[id] <= last) bad('section out of order'); + last = ORDER[id]; + switch (id) { + case 1: { + const n = s.u32(); + if (n > LIMIT.types) bad('too many types'); + for (let i = 0; i < n; i++) { + const at = s.at, first = s.peek(); + let subs; + if (first === 0x4e) { + s.at++; + const k = s.u32(); + if (types.length + k > LIMIT.types) bad('too many types'); + subs = []; + for (let j = 0; j < k; j++) subs.push(subType(s)); + } else { + if (types.length + 1 > LIMIT.types) bad('too many types'); + subs = [subType(s)]; + } + if (first !== 0x60) findings.push({ at, rule: 12 }); + else for (const [t, tat] of subs[0].items) valueItem(t, tat); + defineGroup(subs); + } + break; + } + case 2: { + for (let n = s.u32(); n > 0; n--) { + const at = s.at; + s.name(); s.name(); + findings.push({ at, rule: 5 }); + const kind = s.byte(); + if (kind === 0x00) { + const x = s.u32(), e = funcType(x); + funcs.push(types[x]); + nImportedFuncs++; + if (funcs.length > LIMIT.functions) bad('too many functions'); + addInterface(2 + e.params.length + e.results.length); + } else if (kind === 0x01) { + tables.push(tableType(s)); + if (tables.length > LIMIT.tables) bad('too many tables'); + addInterface(1); + } else if (kind === 0x02) { + mems.push(memType(s)); + if (mems.length > LIMIT.memories) bad('too many memories'); + addInterface(1); + } else if (kind === 0x03) { + globals.push(globalType(s)); + if (globals.length > LIMIT.globals) bad('too many globals'); + addInterface(1); + } else if (kind === 0x04) { + if (s.byte() !== 0) bad('bad tag attribute'); + const x = s.u32(), e = funcType(x); + if (e.results.length) bad('tag type with results'); + tags.push(types[x]); + if (tags.length > LIMIT.tags) bad('too many tags'); + addInterface(2 + e.params.length); + } else bad('bad import kind'); + } + break; + } + case 3: { + const n = s.u32(); + if (funcs.length + n > LIMIT.functions) bad('too many functions'); + findings.push({ at: idAt, rule: 11, cap: 'functions', value: n }); + for (let i = 0; i < n; i++) { const x = s.u32(); funcType(x); funcs.push(types[x]); } + definedFuncs = n; + break; + } + case 4: { + const n = s.u32(); + if (tables.length + n > LIMIT.tables) bad('too many tables'); + for (let i = 0; i < n; i++) { + const at = s.at; + let init = false; + if (s.peek() === 0x40) { s.at++; if (s.byte() !== 0) bad('bad table encoding'); init = true; } + const t = tableType(s); + if (init) constExpr(s, t.elem); + else if (!t.elem.nullable) bad('table of a non-defaultable type without an initialiser'); + const fixed = i === 0 && t.elem.nullable && t.elem.heap === 'func' && t.at === 'i32' && t.max !== null && t.max === t.min; + if (!fixed) findings.push({ at, rule: 7 }); + tables.push(t); + } + break; + } + case 5: { + const n = s.u32(); + if (mems.length + n > LIMIT.memories) bad('too many memories'); + for (let i = 0; i < n; i++) { + const at = s.at, m = memType(s); + mems.push(m); + definedMems++; + if (i > 0 || m.at === 'i64' || m.max === null) findings.push({ at, rule: 6 }); + else findings.push({ at, rule: 6, cap: 'memory_pages', value: Number(m.max) }); + } + break; + } + case 13: { + findings.push({ at: idAt, rule: 12 }); + const n = s.u32(); + if (tags.length + n > LIMIT.tags) bad('too many tags'); + for (let i = 0; i < n; i++) { + if (s.byte() !== 0) bad('bad tag attribute'); + const x = s.u32(); + if (funcType(x).results.length) bad('tag type with results'); + tags.push(types[x]); + } + break; + } + case 6: { + const n = s.u32(); + if (globals.length + n > LIMIT.globals) bad('too many globals'); + for (let i = 0; i < n; i++) { + const at = s.at, g = globalType(s); + valueItem(g.type, at); + constExpr(s, g.type); + globals.push(g); + } + break; + } + case 7: { + for (let n = s.u32(); n > 0; n--) { + const at = s.at, nm = s.name(), kind = s.byte(), x = s.u32(); + if (exported.has(nm)) bad('duplicate export name'); + exported.add(nm); + let ty = null; + if (kind === 0) { if (x >= funcs.length) bad('unknown function'); refs.add(x); ty = canon[funcs[x]]; addInterface(2 + ty.params.length + ty.results.length); } + else if (kind === 1) { if (x >= tables.length) bad('unknown table'); addInterface(1); } + else if (kind === 2) { if (x >= mems.length) bad('unknown memory'); addInterface(1); } + else if (kind === 3) { if (x >= globals.length) bad('unknown global'); addInterface(1); } + else if (kind === 4) { if (x >= tags.length) bad('unknown tag'); const e = canon[tags[x]]; addInterface(2 + e.params.length + e.results.length); } + else bad('bad export kind'); + const abi = ABI.find(([name]) => name === nm); + let ok = false; + if (abi) { + abiSeen.add(nm); + ok = kind === abi[1] && (abi[2] === null || (ty.final && ty.sup === null + && ty.params.length === abi[2][0].length && ty.params.every((t, i) => t === abi[2][0][i]) + && ty.results.length === abi[2][1].length && ty.results.every((t, i) => t === abi[2][1][i]))); + } + if (!ok) findings.push({ at, rule: 10 }); + } + break; + } + case 8: { + findings.push({ at: idAt, rule: 8 }); + const x = s.u32(); + if (x >= funcs.length) bad('unknown function'); + const e = canon[funcs[x]]; + if (e.params.length || e.results.length) bad('start function type'); + break; + } + case 9: { + const n = s.u32(); + if (n > LIMIT.elems) bad('too many element segments'); + for (let i = 0; i < n; i++) { + const flags = s.u32(); + if (flags > 7) bad('bad element segment flags'); + const active = (flags & 1) === 0, exprs = (flags & 4) !== 0; + let t = null; + if (active) { + const ti = flags & 2 ? s.u32() : 0; + if (ti >= tables.length) bad('unknown table'); + t = tables[ti]; + constExpr(s, t.at); + } + let type; + if (!exprs) { + if (flags & 3) { if (s.byte() !== 0) bad('bad element kind'); } + type = { nullable: false, heap: 'func' }; + const k = s.u32(); + if (k > LIMIT.segmentItems) bad('too many segment items'); + for (let j = 0; j < k; j++) { const x = s.u32(); if (x >= funcs.length) bad('unknown function'); refs.add(x); } + } else { + type = flags & 3 ? refType(s) : FUNCREF; + const k = s.u32(); + if (k > LIMIT.segmentItems) bad('too many segment items'); + for (let j = 0; j < k; j++) constExpr(s, type); + } + if (t && !sub(type, t.elem)) bad('element segment type'); + elems.push(type); + } + break; + } + case 12: { + dataCount = s.u32(); + if (dataCount > LIMIT.datas) bad('too many data segments'); + break; + } + case 10: { + const n = s.u32(); + if (n !== (definedFuncs ?? 0)) bad('function and code sections differ'); + codeEntries = n; + for (let i = 0; i < n; i++) { + const size = s.u32(); + if (size > s.end - s.at) bad('unexpected end'); + if (size > LIMIT.body) bad('function body too large'); + body(new Reader(b, s.at, s.at + size), funcs[nImportedFuncs + i]); + s.at += size; + } + break; + } + case 11: { + const n = s.u32(); + if (n > LIMIT.datas) bad('too many data segments'); + if (dataCount !== null && dataCount !== n) bad('data count and data section differ'); + dataSegments = n; + for (let i = 0; i < n; i++) { + const flags = s.u32(); + if (flags === 0 || flags === 2) { + const m = flags === 2 ? s.u32() : 0; + if (m >= mems.length) bad('unknown memory'); + constExpr(s, mems[m].at); + } else if (flags !== 1) bad('bad data segment flags'); + s.skip(s.u32()); + } + break; + } + default: bad('unknown section'); + } + if (!s.eof()) bad('section size mismatch'); + } + if ((definedFuncs ?? 0) !== (codeEntries ?? 0)) bad('function and code sections differ'); + if (dataCount !== null && dataSegments === null && dataCount !== 0) bad('data count without data'); + if (definedMems === 0) findings.push({ at: b.length, rule: 6 }); + if (abiSeen.size < ABI.length) findings.push({ at: b.length, rule: 10 }); + return findings; +} + +// ------------------------------------------------------------------------------ tables + +// Scalar numeric instructions 0x45..0xc4: [name, params, results, float]. +const NUMERIC = []; +{ + const def = (op, name, p, q) => { NUMERIC[op] = [name, p, q, name.includes('f32') || name.includes('f64')]; }; + const rel = ['eq', 'ne', 'lt_s', 'lt_u', 'gt_s', 'gt_u', 'le_s', 'le_u', 'ge_s', 'ge_u']; + const frel = ['eq', 'ne', 'lt', 'gt', 'le', 'ge']; + const ibin = ['add', 'sub', 'mul', 'div_s', 'div_u', 'rem_s', 'rem_u', 'and', 'or', 'xor', 'shl', 'shr_s', 'shr_u', 'rotl', 'rotr']; + const fun = ['abs', 'neg', 'ceil', 'floor', 'trunc', 'nearest', 'sqrt']; + const fbin = ['add', 'sub', 'mul', 'div', 'min', 'max', 'copysign']; + def(0x45, 'i32.eqz', ['i32'], ['i32']); + rel.forEach((n, i) => def(0x46 + i, 'i32.' + n, ['i32', 'i32'], ['i32'])); + def(0x50, 'i64.eqz', ['i64'], ['i32']); + rel.forEach((n, i) => def(0x51 + i, 'i64.' + n, ['i64', 'i64'], ['i32'])); + frel.forEach((n, i) => def(0x5b + i, 'f32.' + n, ['f32', 'f32'], ['i32'])); + frel.forEach((n, i) => def(0x61 + i, 'f64.' + n, ['f64', 'f64'], ['i32'])); + ['clz', 'ctz', 'popcnt'].forEach((n, i) => def(0x67 + i, 'i32.' + n, ['i32'], ['i32'])); + ibin.forEach((n, i) => def(0x6a + i, 'i32.' + n, ['i32', 'i32'], ['i32'])); + ['clz', 'ctz', 'popcnt'].forEach((n, i) => def(0x79 + i, 'i64.' + n, ['i64'], ['i64'])); + ibin.forEach((n, i) => def(0x7c + i, 'i64.' + n, ['i64', 'i64'], ['i64'])); + fun.forEach((n, i) => def(0x8b + i, 'f32.' + n, ['f32'], ['f32'])); + fbin.forEach((n, i) => def(0x92 + i, 'f32.' + n, ['f32', 'f32'], ['f32'])); + fun.forEach((n, i) => def(0x99 + i, 'f64.' + n, ['f64'], ['f64'])); + fbin.forEach((n, i) => def(0xa0 + i, 'f64.' + n, ['f64', 'f64'], ['f64'])); + const conv = [ + [0xa7, 'i32.wrap_i64', 'i64', 'i32'], [0xa8, 'i32.trunc_f32_s', 'f32', 'i32'], [0xa9, 'i32.trunc_f32_u', 'f32', 'i32'], + [0xaa, 'i32.trunc_f64_s', 'f64', 'i32'], [0xab, 'i32.trunc_f64_u', 'f64', 'i32'], [0xac, 'i64.extend_i32_s', 'i32', 'i64'], + [0xad, 'i64.extend_i32_u', 'i32', 'i64'], [0xae, 'i64.trunc_f32_s', 'f32', 'i64'], [0xaf, 'i64.trunc_f32_u', 'f32', 'i64'], + [0xb0, 'i64.trunc_f64_s', 'f64', 'i64'], [0xb1, 'i64.trunc_f64_u', 'f64', 'i64'], [0xb2, 'f32.convert_i32_s', 'i32', 'f32'], + [0xb3, 'f32.convert_i32_u', 'i32', 'f32'], [0xb4, 'f32.convert_i64_s', 'i64', 'f32'], [0xb5, 'f32.convert_i64_u', 'i64', 'f32'], + [0xb6, 'f32.demote_f64', 'f64', 'f32'], [0xb7, 'f64.convert_i32_s', 'i32', 'f64'], [0xb8, 'f64.convert_i32_u', 'i32', 'f64'], + [0xb9, 'f64.convert_i64_s', 'i64', 'f64'], [0xba, 'f64.convert_i64_u', 'i64', 'f64'], [0xbb, 'f64.promote_f32', 'f32', 'f64'], + [0xbc, 'i32.reinterpret_f32', 'f32', 'i32'], [0xbd, 'i64.reinterpret_f64', 'f64', 'i64'], [0xbe, 'f32.reinterpret_i32', 'i32', 'f32'], + [0xbf, 'f64.reinterpret_i64', 'i64', 'f64'], [0xc0, 'i32.extend8_s', 'i32', 'i32'], [0xc1, 'i32.extend16_s', 'i32', 'i32'], + [0xc2, 'i64.extend8_s', 'i64', 'i64'], [0xc3, 'i64.extend16_s', 'i64', 'i64'], [0xc4, 'i64.extend32_s', 'i64', 'i64'], + ]; + for (const [op, name, p, q] of conv) def(op, name, [p], [q]); +} + +// Loads and stores 0x28..0x3e: [name, value type, natural alignment, store]. +const LOADSTORE = [ + ['i32.load', 'i32', 2, false], ['i64.load', 'i64', 3, false], ['f32.load', 'f32', 2, false], ['f64.load', 'f64', 3, false], + ['i32.load8_s', 'i32', 0, false], ['i32.load8_u', 'i32', 0, false], ['i32.load16_s', 'i32', 1, false], ['i32.load16_u', 'i32', 1, false], + ['i64.load8_s', 'i64', 0, false], ['i64.load8_u', 'i64', 0, false], ['i64.load16_s', 'i64', 1, false], ['i64.load16_u', 'i64', 1, false], + ['i64.load32_s', 'i64', 2, false], ['i64.load32_u', 'i64', 2, false], ['i32.store', 'i32', 2, true], ['i64.store', 'i64', 3, true], + ['f32.store', 'f32', 2, true], ['f64.store', 'f64', 3, true], ['i32.store8', 'i32', 0, true], ['i32.store16', 'i32', 1, true], + ['i64.store8', 'i64', 0, true], ['i64.store16', 'i64', 1, true], ['i64.store32', 'i64', 2, true], +]; + +// Vector instructions, by their opcode after 0xfd: [name, signature, argument, argument]. +const SIMD = []; +{ + const d = (op, name, sig, a1, a2) => { SIMD[op] = [name, sig, a1, a2]; }; + [[0x00, 'v128.load', 4], [0x01, 'v128.load8x8_s', 3], [0x02, 'v128.load8x8_u', 3], [0x03, 'v128.load16x4_s', 3], + [0x04, 'v128.load16x4_u', 3], [0x05, 'v128.load32x2_s', 3], [0x06, 'v128.load32x2_u', 3], [0x07, 'v128.load8_splat', 0], + [0x08, 'v128.load16_splat', 1], [0x09, 'v128.load32_splat', 2], [0x0a, 'v128.load64_splat', 3], + [0x5c, 'v128.load32_zero', 2], [0x5d, 'v128.load64_zero', 3]].forEach(([op, n, a]) => d(op, n, 'load', a)); + d(0x0b, 'v128.store', 'store', 4); + d(0x0c, 'v128.const', 'const'); + d(0x0d, 'i8x16.shuffle', 'shuffle'); + d(0x0e, 'i8x16.swizzle', 'bin'); + [['i8x16', 'i32'], ['i16x8', 'i32'], ['i32x4', 'i32'], ['i64x2', 'i64'], ['f32x4', 'f32'], ['f64x2', 'f64']] + .forEach(([s, t], i) => d(0x0f + i, s + '.splat', 'splat', t)); + [[0x15, 'i8x16.extract_lane_s', 'extract', 'i32', 16], [0x16, 'i8x16.extract_lane_u', 'extract', 'i32', 16], + [0x17, 'i8x16.replace_lane', 'replace', 'i32', 16], [0x18, 'i16x8.extract_lane_s', 'extract', 'i32', 8], + [0x19, 'i16x8.extract_lane_u', 'extract', 'i32', 8], [0x1a, 'i16x8.replace_lane', 'replace', 'i32', 8], + [0x1b, 'i32x4.extract_lane', 'extract', 'i32', 4], [0x1c, 'i32x4.replace_lane', 'replace', 'i32', 4], + [0x1d, 'i64x2.extract_lane', 'extract', 'i64', 2], [0x1e, 'i64x2.replace_lane', 'replace', 'i64', 2], + [0x1f, 'f32x4.extract_lane', 'extract', 'f32', 4], [0x20, 'f32x4.replace_lane', 'replace', 'f32', 4], + [0x21, 'f64x2.extract_lane', 'extract', 'f64', 2], [0x22, 'f64x2.replace_lane', 'replace', 'f64', 2], + ].forEach(([op, n, sig, t, l]) => d(op, n, sig, t, l)); + const irel = ['eq', 'ne', 'lt_s', 'lt_u', 'gt_s', 'gt_u', 'le_s', 'le_u', 'ge_s', 'ge_u']; + irel.forEach((n, i) => d(0x23 + i, 'i8x16.' + n, 'bin')); + irel.forEach((n, i) => d(0x2d + i, 'i16x8.' + n, 'bin')); + irel.forEach((n, i) => d(0x37 + i, 'i32x4.' + n, 'bin')); + ['eq', 'ne', 'lt', 'gt', 'le', 'ge'].forEach((n, i) => { d(0x41 + i, 'f32x4.' + n, 'bin'); d(0x47 + i, 'f64x2.' + n, 'bin'); }); + d(0x4d, 'v128.not', 'un'); + ['and', 'andnot', 'or', 'xor'].forEach((n, i) => d(0x4e + i, 'v128.' + n, 'bin')); + d(0x52, 'v128.bitselect', 'tern'); + d(0x53, 'v128.any_true', 'test'); + [8, 16, 32, 64].forEach((w, i) => { + d(0x54 + i, `v128.load${w}_lane`, 'loadlane', i, 16 >> i); + d(0x58 + i, `v128.store${w}_lane`, 'storelane', i, 16 >> i); + }); + const rows = [ + [0x5e, 'f32x4.demote_f64x2_zero', 'un'], [0x5f, 'f64x2.promote_low_f32x4', 'un'], + [0x60, 'i8x16.abs', 'un'], [0x61, 'i8x16.neg', 'un'], [0x62, 'i8x16.popcnt', 'un'], [0x63, 'i8x16.all_true', 'test'], + [0x64, 'i8x16.bitmask', 'test'], [0x65, 'i8x16.narrow_i16x8_s', 'bin'], [0x66, 'i8x16.narrow_i16x8_u', 'bin'], + [0x67, 'f32x4.ceil', 'un'], [0x68, 'f32x4.floor', 'un'], [0x69, 'f32x4.trunc', 'un'], [0x6a, 'f32x4.nearest', 'un'], + [0x6b, 'i8x16.shl', 'shift'], [0x6c, 'i8x16.shr_s', 'shift'], [0x6d, 'i8x16.shr_u', 'shift'], + [0x6e, 'i8x16.add', 'bin'], [0x6f, 'i8x16.add_sat_s', 'bin'], [0x70, 'i8x16.add_sat_u', 'bin'], [0x71, 'i8x16.sub', 'bin'], + [0x72, 'i8x16.sub_sat_s', 'bin'], [0x73, 'i8x16.sub_sat_u', 'bin'], [0x74, 'f64x2.ceil', 'un'], [0x75, 'f64x2.floor', 'un'], + [0x76, 'i8x16.min_s', 'bin'], [0x77, 'i8x16.min_u', 'bin'], [0x78, 'i8x16.max_s', 'bin'], [0x79, 'i8x16.max_u', 'bin'], + [0x7a, 'f64x2.trunc', 'un'], [0x7b, 'i8x16.avgr_u', 'bin'], + [0x7c, 'i16x8.extadd_pairwise_i8x16_s', 'un'], [0x7d, 'i16x8.extadd_pairwise_i8x16_u', 'un'], + [0x7e, 'i32x4.extadd_pairwise_i16x8_s', 'un'], [0x7f, 'i32x4.extadd_pairwise_i16x8_u', 'un'], + [0x80, 'i16x8.abs', 'un'], [0x81, 'i16x8.neg', 'un'], [0x82, 'i16x8.q15mulr_sat_s', 'bin'], [0x83, 'i16x8.all_true', 'test'], + [0x84, 'i16x8.bitmask', 'test'], [0x85, 'i16x8.narrow_i32x4_s', 'bin'], [0x86, 'i16x8.narrow_i32x4_u', 'bin'], + [0x87, 'i16x8.extend_low_i8x16_s', 'un'], [0x88, 'i16x8.extend_high_i8x16_s', 'un'], + [0x89, 'i16x8.extend_low_i8x16_u', 'un'], [0x8a, 'i16x8.extend_high_i8x16_u', 'un'], + [0x8b, 'i16x8.shl', 'shift'], [0x8c, 'i16x8.shr_s', 'shift'], [0x8d, 'i16x8.shr_u', 'shift'], + [0x8e, 'i16x8.add', 'bin'], [0x8f, 'i16x8.add_sat_s', 'bin'], [0x90, 'i16x8.add_sat_u', 'bin'], [0x91, 'i16x8.sub', 'bin'], + [0x92, 'i16x8.sub_sat_s', 'bin'], [0x93, 'i16x8.sub_sat_u', 'bin'], [0x94, 'f64x2.nearest', 'un'], [0x95, 'i16x8.mul', 'bin'], + [0x96, 'i16x8.min_s', 'bin'], [0x97, 'i16x8.min_u', 'bin'], [0x98, 'i16x8.max_s', 'bin'], [0x99, 'i16x8.max_u', 'bin'], + [0x9b, 'i16x8.avgr_u', 'bin'], [0x9c, 'i16x8.extmul_low_i8x16_s', 'bin'], [0x9d, 'i16x8.extmul_high_i8x16_s', 'bin'], + [0x9e, 'i16x8.extmul_low_i8x16_u', 'bin'], [0x9f, 'i16x8.extmul_high_i8x16_u', 'bin'], + [0xa0, 'i32x4.abs', 'un'], [0xa1, 'i32x4.neg', 'un'], [0xa3, 'i32x4.all_true', 'test'], [0xa4, 'i32x4.bitmask', 'test'], + [0xa7, 'i32x4.extend_low_i16x8_s', 'un'], [0xa8, 'i32x4.extend_high_i16x8_s', 'un'], + [0xa9, 'i32x4.extend_low_i16x8_u', 'un'], [0xaa, 'i32x4.extend_high_i16x8_u', 'un'], + [0xab, 'i32x4.shl', 'shift'], [0xac, 'i32x4.shr_s', 'shift'], [0xad, 'i32x4.shr_u', 'shift'], [0xae, 'i32x4.add', 'bin'], + [0xb1, 'i32x4.sub', 'bin'], [0xb5, 'i32x4.mul', 'bin'], [0xb6, 'i32x4.min_s', 'bin'], [0xb7, 'i32x4.min_u', 'bin'], + [0xb8, 'i32x4.max_s', 'bin'], [0xb9, 'i32x4.max_u', 'bin'], [0xba, 'i32x4.dot_i16x8_s', 'bin'], + [0xbc, 'i32x4.extmul_low_i16x8_s', 'bin'], [0xbd, 'i32x4.extmul_high_i16x8_s', 'bin'], + [0xbe, 'i32x4.extmul_low_i16x8_u', 'bin'], [0xbf, 'i32x4.extmul_high_i16x8_u', 'bin'], + [0xc0, 'i64x2.abs', 'un'], [0xc1, 'i64x2.neg', 'un'], [0xc3, 'i64x2.all_true', 'test'], [0xc4, 'i64x2.bitmask', 'test'], + [0xc7, 'i64x2.extend_low_i32x4_s', 'un'], [0xc8, 'i64x2.extend_high_i32x4_s', 'un'], + [0xc9, 'i64x2.extend_low_i32x4_u', 'un'], [0xca, 'i64x2.extend_high_i32x4_u', 'un'], + [0xcb, 'i64x2.shl', 'shift'], [0xcc, 'i64x2.shr_s', 'shift'], [0xcd, 'i64x2.shr_u', 'shift'], [0xce, 'i64x2.add', 'bin'], + [0xd1, 'i64x2.sub', 'bin'], [0xd5, 'i64x2.mul', 'bin'], [0xd6, 'i64x2.eq', 'bin'], [0xd7, 'i64x2.ne', 'bin'], + [0xd8, 'i64x2.lt_s', 'bin'], [0xd9, 'i64x2.gt_s', 'bin'], [0xda, 'i64x2.le_s', 'bin'], [0xdb, 'i64x2.ge_s', 'bin'], + [0xdc, 'i64x2.extmul_low_i32x4_s', 'bin'], [0xdd, 'i64x2.extmul_high_i32x4_s', 'bin'], + [0xde, 'i64x2.extmul_low_i32x4_u', 'bin'], [0xdf, 'i64x2.extmul_high_i32x4_u', 'bin'], + [0xe0, 'f32x4.abs', 'un'], [0xe1, 'f32x4.neg', 'un'], [0xe3, 'f32x4.sqrt', 'un'], [0xe4, 'f32x4.add', 'bin'], + [0xe5, 'f32x4.sub', 'bin'], [0xe6, 'f32x4.mul', 'bin'], [0xe7, 'f32x4.div', 'bin'], [0xe8, 'f32x4.min', 'bin'], + [0xe9, 'f32x4.max', 'bin'], [0xea, 'f32x4.pmin', 'bin'], [0xeb, 'f32x4.pmax', 'bin'], + [0xec, 'f64x2.abs', 'un'], [0xed, 'f64x2.neg', 'un'], [0xef, 'f64x2.sqrt', 'un'], [0xf0, 'f64x2.add', 'bin'], + [0xf1, 'f64x2.sub', 'bin'], [0xf2, 'f64x2.mul', 'bin'], [0xf3, 'f64x2.div', 'bin'], [0xf4, 'f64x2.min', 'bin'], + [0xf5, 'f64x2.max', 'bin'], [0xf6, 'f64x2.pmin', 'bin'], [0xf7, 'f64x2.pmax', 'bin'], + [0xf8, 'i32x4.trunc_sat_f32x4_s', 'un'], [0xf9, 'i32x4.trunc_sat_f32x4_u', 'un'], + [0xfa, 'f32x4.convert_i32x4_s', 'un'], [0xfb, 'f32x4.convert_i32x4_u', 'un'], + [0xfc, 'i32x4.trunc_sat_f64x2_s_zero', 'un'], [0xfd, 'i32x4.trunc_sat_f64x2_u_zero', 'un'], + [0xfe, 'f64x2.convert_low_i32x4_s', 'un'], [0xff, 'f64x2.convert_low_i32x4_u', 'un'], + // The relaxed vector instructions (R4), 0x100 to 0x113. + [0x100, 'i8x16.relaxed_swizzle', 'bin'], [0x101, 'i32x4.relaxed_trunc_f32x4_s', 'un'], + [0x102, 'i32x4.relaxed_trunc_f32x4_u', 'un'], [0x103, 'i32x4.relaxed_trunc_f64x2_s_zero', 'un'], + [0x104, 'i32x4.relaxed_trunc_f64x2_u_zero', 'un'], [0x105, 'f32x4.relaxed_madd', 'tern'], + [0x106, 'f32x4.relaxed_nmadd', 'tern'], [0x107, 'f64x2.relaxed_madd', 'tern'], [0x108, 'f64x2.relaxed_nmadd', 'tern'], + [0x109, 'i8x16.relaxed_laneselect', 'tern'], [0x10a, 'i16x8.relaxed_laneselect', 'tern'], + [0x10b, 'i32x4.relaxed_laneselect', 'tern'], [0x10c, 'i64x2.relaxed_laneselect', 'tern'], + [0x10d, 'f32x4.relaxed_min', 'bin'], [0x10e, 'f32x4.relaxed_max', 'bin'], [0x10f, 'f64x2.relaxed_min', 'bin'], + [0x110, 'f64x2.relaxed_max', 'bin'], [0x111, 'i16x8.relaxed_q15mulr_s', 'bin'], + [0x112, 'i16x8.relaxed_dot_i8x16_i7x16_s', 'bin'], [0x113, 'i32x4.relaxed_dot_i8x16_i7x16_add_s', 'tern'], + ]; + for (const [op, n, sig] of rows) d(op, n, sig); +} + +/** The names of every instruction this file decodes, for a reader that compares tables. */ +export function instructionNames() { + return { + numeric: NUMERIC.map((e, op) => e && [op, e[0]]).filter(Boolean), + loadstore: LOADSTORE.map((e, i) => [0x28 + i, e[0]]), + simd: SIMD.map((e, op) => e && [op, e[0]]).filter(Boolean), + }; +} + +// ------------------------------------------------------------------------------ the verdict + +/** + * The analysis of a module's bytes: `null` where it breaks R2, else every item and absence + * that breaks one of R3 to R12, each with the level and the cap it depends on. + */ +export function analyse(bytes) { + try { + return analyze(bytes); + } catch (e) { + if (e instanceof Refused2) return null; + throw e; + } +} + +/** The verdict from an analysis, for a module of `length` bytes, at `level` under `caps`. */ +export function verdictOf(analysis, length, level, caps = PROFILE_CAPS) { + if (length > caps.module_bytes) return 'refused R1 0'; + if (analysis === null) return 'refused R2 -'; + let best = null; + for (const f of analysis) { + if (f.int && level !== 'integer') continue; + if (f.cap && !(f.value > caps[f.cap])) continue; + if (!best || f.at < best.at || (f.at === best.at && f.rule < best.rule)) best = f; + } + return best ? `refused R${best.rule} ${best.at}` : 'held'; +} + +/** The module's verdict at `level` ('integer' or 'float') under `caps` (§4.3). */ +export function check(bytes, level, caps = PROFILE_CAPS) { + if (level !== 'integer' && level !== 'float') throw new Error(`no level ${level}`); + if (bytes.length > caps.module_bytes) return 'refused R1 0'; + return verdictOf(analyse(bytes), bytes.length, level, caps); +} + +/** + * The level a sink holds the module at (§6, check 9b): { level: 'integer' | 'float' | null, + * verdict }, the verdict being that of the last level checked. + */ +export function levelOf(bytes, caps = PROFILE_CAPS) { + const a = bytes.length > caps.module_bytes ? null : analyse(bytes); + const int = verdictOf(a, bytes.length, 'integer', caps); + if (int === 'held') return { level: 'integer', verdict: int }; + if (!int.startsWith('refused R3 ')) return { level: null, verdict: int }; + const float = verdictOf(a, bytes.length, 'float', caps); + return { level: float === 'held' ? 'float' : null, verdict: float }; +} + +/** The profile's caps with `name=value` changes, comma-joined; `-` for none. */ +export function parseCaps(text) { + const caps = { ...PROFILE_CAPS }; + if (text === '-') return caps; + for (const part of text.split(',')) { + const [name, value] = part.split('='); + if (!(name in caps) || !/^[0-9]+$/.test(value ?? '')) return null; + caps[name] = Number(value); + } + return caps; +} + +const LEVELS = { integer: 'integer', float: 'float', 'det-module/1-int': 'integer', 'det-module/1-det': 'float' }; + +// ------------------------------------------------------------------------------ from a shell + +async function main(argv) { + const { readFileSync } = await import('node:fs'); + const { join } = await import('node:path'); + const read = (p) => { + try { return new Uint8Array(readFileSync(p)); } catch (e) { console.error(`check-module: ${p}: ${e.message}`); process.exit(2); } + }; + const usage = () => { + console.error('usage: node check-module.mjs [--level integer|float] [--caps NAME=VALUE,...] FILE...\n node check-module.mjs --cases DIR'); + process.exit(2); + }; + if (argv.length === 2 && argv[0] === '--cases') { + const list = join(argv[1], 'cases.txt'); + let text; + try { text = readFileSync(list, 'utf8'); } catch (e) { console.error(`check-module: ${list}: ${e.message}`); process.exit(2); } + let checked = 0, wrong = 0; + const cache = new Map(); + for (const raw of text.split('\n')) { + const line = raw.split(' #')[0].trim(); + if (!line || line.startsWith('#')) continue; + const m = /^(\S+) (\S+) (\S+) (.+)$/.exec(line); + const level = m && LEVELS[m[2]]; + const caps = m && parseCaps(m[3]); + if (!m || !level || !caps) { console.error(`check-module: ${list}: not a case: ${line}`); process.exit(2); } + if (!cache.has(m[1])) { + const bytes = read(join(argv[1], `${m[1]}.wasm`)); + cache.set(m[1], { length: bytes.length, analysis: analyse(bytes) }); + } + const { length, analysis } = cache.get(m[1]); + const got = verdictOf(analysis, length, level, caps); + checked++; + if (got !== m[4]) { wrong++; console.log(`${m[1]} ${level} ${m[3]}: ${got}, not ${m[4]}`); } + } + console.log(wrong ? `check-module: ${wrong} of ${checked} verdicts differ from ${list}` + : `check-module: ${checked} verdicts, each the one ${list} states`); + process.exit(wrong ? 1 : 0); + } + let level = null, caps = PROFILE_CAPS; + const files = []; + for (let i = 0; i < argv.length; i++) { + if (argv[i] === '--level') { level = LEVELS[argv[++i]]; if (!level) usage(); } + else if (argv[i] === '--caps') { caps = parseCaps(argv[++i] ?? ''); if (!caps) usage(); } + else if (argv[i].startsWith('--')) usage(); + else files.push(argv[i]); + } + if (!files.length) usage(); + let allHeld = true; + for (const f of files) { + const bytes = read(f); + let line; + if (level) { + line = check(bytes, level, caps); + allHeld &&= line === 'held'; + } else { + const { level: held, verdict } = levelOf(bytes, caps); + if (held) line = `held at the ${held} level (${held === 'integer' ? 'det-module/1-int' : 'det-module/1-det'})`; + else { line = verdict; allHeld = false; } + } + console.log(files.length > 1 ? `${f}: ${line}` : line); + } + process.exit(allHeld ? 0 : 1); +} + +if (typeof process === 'object' && process.argv && process.argv[1]) { + const { pathToFileURL } = await import('node:url'); + const { realpathSync } = await import('node:fs'); + let self; + try { self = pathToFileURL(realpathSync(process.argv[1])).href; } catch { self = null; } + if (self === import.meta.url) await main(process.argv.slice(2)); +} diff --git a/wai/wai-module-check/differential.mjs b/wai/wai-module-check/differential.mjs new file mode 100644 index 000000000..be0b9daa9 --- /dev/null +++ b/wai/wai-module-check/differential.mjs @@ -0,0 +1,55 @@ +// 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: ` | `, +// the module being DIR/.wasm. 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 = /^(\d+) (\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); + count(`${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); -- 2.54.0 (Apple Git-157) From dcc3cd2400fb3683f12d7dad630c860d8e01ef07 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 5 Nov 2026 08:11:36 -0500 Subject: [PATCH 07/12] deterministic-modules: drop the import and export counts from the validation limits Every import and every export adds at least 1 to the interface limit's sum, so that limit already holds a module to 999,998 imports and exports together, and a separate count of 1,000,000 for each could never decide a verdict. The interface row now says so. Both checkers were held to every limit of the table, at its value and one past it, by the validation limits' corpus. Co-Authored-By: Claude Opus 5.5 --- wai/extensions/deterministic-modules.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/wai/extensions/deterministic-modules.md b/wai/extensions/deterministic-modules.md index bab9cc157..a0d997892 100644 --- a/wai/extensions/deterministic-modules.md +++ b/wai/extensions/deterministic-modules.md @@ -151,7 +151,6 @@ under this profile, and is `refused R2 -`. |---|---|---| | 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 | -| imports, exports | 1,000,000 each | the entries of the import section, and of the export section | | 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 | @@ -163,7 +162,7 @@ under this profile, and is `refused R2 -`. | 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 | +| 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 -- 2.54.0 (Apple Git-157) From 1970eb53d2a15f0d8e4bffaeb278781417248763 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 5 Nov 2026 08:11:58 -0500 Subject: [PATCH 08/12] wai-module-check: mutated copies in the differential, and the specification's tests wasm-smith writes valid modules, or ones invalid only as it is told to be, so the differential tested how the two validators accept far more than how they refuse: with check-module.mjs changed to accept an untyped select of references, or to read an uninitialised local, the 10,000 modules still all agreed. The differential now also writes two mutated copies of each module, one or two bytes changed (a byte replaced, inserted or removed anywhere after the preamble, or a code-section byte replaced by a one-byte opcode), most of them outside R2. On the committed seed the checkers agree on all 60,000 verdicts of its 30,000 modules, and it catches a changed section order, an unchecked if without else or an unchecked alignment. examples/spectest.rs writes every module the specification's test scripts define, assert invalid or assert malformed, with the Rust checker's verdicts, for differential.mjs. On the scripts of the specification build of 2026-11-04 (commit 859d3232a55c, test/core, 259 scripts, one of which the text parser of this release does not read) it writes 5,712 modules: the Rust checker refuses every invalid and malformed one by R2 and no valid one, and the two checkers agree on all 11,424 verdicts. With check-module.mjs changed in any of ten ways a validator can go wrong (a select of references, an uninitialised local, a u32's unused bits, br_if's pushed types, duplicate exports, a custom section's name, a final supertype, a field's mutability in subtyping, catch labels, undeclared function references), they disagree. Its scripts are not in this repository, so it is run by hand on a copy of them. Co-Authored-By: Claude Opus 5.5 --- wai/wai-module-check/Cargo.lock | 32 +++++ wai/wai-module-check/Cargo.toml | 7 ++ wai/wai-module-check/differential.mjs | 15 ++- wai/wai-module-check/examples/differential.rs | 103 ++++++++++++++-- wai/wai-module-check/examples/spectest.rs | 112 ++++++++++++++++++ 5 files changed, 252 insertions(+), 17 deletions(-) create mode 100644 wai/wai-module-check/examples/spectest.rs diff --git a/wai/wai-module-check/Cargo.lock b/wai/wai-module-check/Cargo.lock index 9d87d98ca..759f12618 100644 --- a/wai/wai-module-check/Cargo.lock +++ b/wai/wai-module-check/Cargo.lock @@ -23,6 +23,12 @@ 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" @@ -68,6 +74,12 @@ 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" @@ -103,6 +115,12 @@ 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" @@ -110,6 +128,7 @@ dependencies = [ "arbitrary", "wasm-smith", "wasmparser", + "wast", ] [[package]] @@ -144,3 +163,16 @@ 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", +] diff --git a/wai/wai-module-check/Cargo.toml b/wai/wai-module-check/Cargo.toml index 4b34ecab3..1fe1146ca 100644 --- a/wai/wai-module-check/Cargo.toml +++ b/wai/wai-module-check/Cargo.toml @@ -16,7 +16,14 @@ wasmparser = { version = "=0.262.0", default-features = false, features = ["std" # 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" diff --git a/wai/wai-module-check/differential.mjs b/wai/wai-module-check/differential.mjs index be0b9daa9..f31aa0871 100644 --- a/wai/wai-module-check/differential.mjs +++ b/wai/wai-module-check/differential.mjs @@ -5,10 +5,12 @@ // // node differential.mjs DIR // -// DIR/verdicts.txt holds one line a module: ` | `, -// the module being DIR/.wasm. 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. +// DIR/verdicts.txt holds one line a module, ` | `, the module being DIR/.wasm: `` for wasm-smith's i-th, `-` for a +// mutated copy of it, `