WAI Extension: WA²ISM™, the Deterministic Module Profile

Mirrored from the canonical text at commit 260cbd09 (2026-11-08).

Status: Draft. WA²ISM™, named WAISM™ in running text, is WAI’s deterministic module profile: 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 §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 §7.9, http-delivery §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 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 §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 §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. The record a sink holds for check 9c.
browser-sink §4.3 step 6. The tier a page’s wasm decoder holds.
determinism-tiers §5 and SPEC §7. WebAssembly as a fabric of decode-equivalence is a module held at the integer level.
integer-operators §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	`waism/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 §3.1, Tier) and, for a `GenerativeDeterministic` capability, its generation-equivalence (SPEC §7)
float level	`waism/1-det`	admitted	only an engine set to the deterministic profile’s NaN rule, shown by the probe (§6, check 10); no page (§7)	`entropy-consistency` where that is the class tier of its capability, on such an engine; otherwise none. Never `decode-equivalence` or generation-equivalence: SPEC §7, Replicate-soundness, admits a neural decode at `decode-equivalence` only where no floating-point operation is on its path, and this revision gives the float level neither

The levels differ only in R3. Each identifier names this text’s version 1; a module meets a level when a checker gives it held at that level (§4.3), and R13.

3. Terms

Module: a decoder module (jwp-receipts §7.9) that a sink would run on a WebAssembly engine, whatever its bytes. Bytes that are not a WebAssembly 3.0 module, such as a component or bytes that do not decode, are such a module where a sink would run them on one, and R2 refuses them (§4.3). A decoder module a sink runs on no WebAssembly engine is not one.
Item: a part of a module’s bytes a rule is about: an instruction, in a function body or a constant expression; a value type, in a function type, a local declaration (one that declares no locals among them), a global type, a block type or a typed select; an entry of the import, table, memory, global or export section; a type entry of the type section; or a section.
Caps: the three limits of §4.2’s first table. Its validation limits are part of R2, and are no caps.
Verdict: a checker’s answer for a module at a level under caps (§4.3).
Need: the tier a sink holds an object’s decoded output to, as browser-sink §2 defines it, for any sink: the object’s pin tier, else its track’s declared determinism, else none.
Held at a level: a sink holds a module at a level, for an object, when checks 1 to 10 of §6 pass for it at that level.

4. Rules

4.1 The rules

Each rule names what it rests on: a clause of WebAssembly 3.0, or a clause of WAI. §9.1 names, for each rule, at least one planted module that breaks it and no other.

rule	level	the module	rests on
R1	both	is at most `module_bytes` long (§4.2).	WebAssembly 3.0, Implementation Limitations (an implementation may limit the size of a module); §4.2
R2	both	is a WebAssembly 3.0 module: its bytes decode under the binary format, from the preamble `\0asm` and version 1, and it is valid, within the validation limits of §4.2. Shared memory, atomic instructions, a component, and every other construct WebAssembly 3.0 does not define, are outside it.	WebAssembly 3.0, Binary Format (Modules: the preamble and the section ids; Types: limits, whose four forms have no shared one), Validation and Implementation Limitations (an implementation may limit the number and size of a module’s parts); §4.2
R3	integer	contains no floating point: no `f32` or `f64` value type, and no instruction that takes or gives a floating-point value, an `f32` or an `f64` or a `v128` read or written as `f32x4` or `f64x2` lanes. That covers constants, arithmetic, comparisons, conversions to and from integers (the saturating truncations among them), reinterpretations, lane splats and extractions, and loads and stores of floating-point values.	WebAssembly 3.0, Numerics, NaN Propagation (the sign of a NaN result is non-deterministic, and its payload is chosen among arithmetic NaNs); SPEC §7, Replicate-soundness (no float operation anywhere on a decode path that backs `replicate`); integer-operators §6
R4	both	contains no relaxed vector instruction: the integer ones (`i8x16.relaxed_swizzle`, the four `relaxed_laneselect`s, `i16x8.relaxed_q15mulr_s`, the two relaxed dot products) as well as the floating-point ones.	WebAssembly 3.0, Numerics, Relaxed Operations (each result is one of a set, and the implementation chooses which); integer-operators §6 (no instruction whose result the instruction set leaves to the implementation)
R5	both	imports nothing: no function, table, memory, global or tag.	WebAssembly 3.0, Binary Format, Modules (the import section, whose values the host supplies at instantiation); §5 (the output is a function of the capability, the payload and the set alone)
R6	both	defines exactly one memory, with address type `i32` and a declared maximum of at most `memory_pages` (§4.2).	WebAssembly 3.0, Execution, `memory.grow` (growth is non-deterministic, and fails past a declared maximum); Binary Format, Types (limits); §4.2
R7	both	defines at most one table, whose element type is `funcref` (`ref null func`, in either of its encodings), whose address type is `i32` and whose minimum equals its maximum, and contains no `table.grow`, `table.fill` or `table.set`.	WebAssembly 3.0, Profiles, Defined Profiles (`table.grow` remains non-deterministic under the deterministic profile); §5
R8	both	has no start section.	WebAssembly 3.0, Binary Format, Modules (the start section names a function that runs at instantiation); §6 check 12 (the guard covers `wai_run`, not instantiation)
R9	both	gives no function type, local or global a reference type.	§5 (every value across the interface is an `i32`)
R10	both	exports exactly the six exports of §5, each of the kind and type given there, and nothing else.	§5
R11	both	defines at most `functions` functions (§4.2).	WebAssembly 3.0, Implementation Limitations; §4.2
R12	both	contains none of these constructs of WebAssembly 3.0: exception handling (a tag section, `throw`, `throw_ref`, `try_table`); tail calls (`return_call`, `return_call_indirect`); typed function references (`call_ref`, `return_call_ref`, `ref.as_non_null`, `br_on_null`, `br_on_non_null`); and garbage-collected types and instructions (a type entry that is not a function type, among them a recursive or subtype declaration; `struct.`, `array.`, `ref.i31`, `i31.get_s`, `i31.get_u`, `ref.test`, `ref.cast`, `br_on_cast`, `br_on_cast_fail`, `any.convert_extern`, `extern.convert_any`, `ref.eq`).	§1 (the profile admits what a decoder module uses: a construct a decoder has no need of is one more that a sink’s engine would run and that a conformance result would have to answer for, §11)
R13	both	after a `memory.grow` that fails, gives no output: within `wai_run` the call traps, and within `wai_alloc` it traps or returns 0. A module whose memory’s minimum equals its maximum and which contains no `memory.grow` meets this rule.	WebAssembly 3.0, Execution, `memory.grow` (it may fail, pushing −1) and Profiles (growth remains non-deterministic under the deterministic profile); integer-operators §6 (“A refused decode outputs nothing”)

An instruction breaks R3 by what its opcode alone takes or gives. One whose operand or result types are fixed elsewhere (a block, a typed select, a call, local.get, drop) breaks R3 only through the value type that fixes them: an earlier item, or, for a block type or a typed select, the value type that follows its opcode.

Rules R1 to R12 are about the module’s bytes, and a checker decides them (§4.3). R13 is about what the module does, and a conformance result attests it (§6, check 9c; §9.2). Custom sections are part of the bytes, so the digest covers them; WebAssembly’s semantics ignore them, and no rule, check or sink of this text reads them.

4.2 Caps and validation limits

cap	the profile’s value	what it bounds
`module_bytes`	16,777,216	the module’s length, in bytes
`functions`	50,000	the functions the module defines
`memory_pages`	65,536	the memory’s declared maximum, in 64 KiB pages

A sink MAY apply lower caps of its own. A module over a sink’s caps is not held at that sink: the caps change where a module is held, never what it outputs.

The validation limits are part of R2, and no sink changes them. WebAssembly 3.0 lets an implementation limit the number and the size of a module’s parts, so without fixed limits two validators could differ on a module within the caps; a module beyond one of these is not valid under this profile, and is refused R2 -.

limit	value	what it bounds
types	1,000,000	the entries of the type section, and the types they define
functions, globals, tags	1,000,000 each	those the module imports and defines, together
tables	100,000	the tables the module imports and defines, together
memories	100	the memories the module imports and defines, together
element segments, data segments	100,000 each	the entries of the element section, and of the data section; and the data count section’s count
segment items	10,000,000	the items of one element segment
name	100,000	the bytes of one name: an import’s module or field, an export’s, a custom section’s
body	7,654,321	the bytes of one function body, after its size
locals	50,000	a function’s parameters and the locals its body declares, together
parameters, results	1,000 each	those of one function type
struct fields	10,000	those of one struct type
catches	10,000	the catch clauses of one `try_table`
subtype depth	63	a type’s declared supertypes, followed to a type that declares none
interface	999,998	the sum, over every import and export, of 2 and the parameters and results of its type for a function or a tag, and of 1 for a table, a memory or a global; so a module has at most 999,998 imports and exports

4.3 The verdict

A checker’s verdict for a module at a level under caps is one line of ASCII: held, or refused R<n> <offset>, with <n> the rule and <offset> a decimal byte offset into the module, or -. It is a function of the module’s bytes, the level and the caps, and it is decided in this order:

R1: a module longer than module_bytes is refused R1 0, and is not read further.
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.
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.
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.
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.

wai_abi(). A result other than 1 is module_result_invalid.
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.
wai_run with the three offsets and lengths, under the guard of §6 check 12.
wai_out_ptr() and wai_out_len(). A region that does not lie within the memory is module_result_invalid.
Where wai_run returned 0, the region is the decoded medium in its capability’s canonical buffer (determinism-tiers §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 §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 §6.1: a hybrid entry signs nothing with Ed25519 alone, and a record has no other signature), holds module/decoder in its may_sign, and, where it is retired, has an until no earlier than the record’s started_at, the two compared as jwp-receipts §7.4 compares times. Otherwise module_unattested. The record carries no signer_id, so it is no item jwp-receipts §7.4 confirms: this check reads the head the grant was confirmed under, and nothing else of the key log.

10. Engine.

At the float level, where the object’s need is above none: the sink’s engine is set to the deterministic profile’s NaN rule (§7, nan-canonical), and the probe of §9.3, run in this process on that engine and setting before the module’s first run, gave the probe’s bytes. Otherwise module_engine_not_deterministic where the engine cannot be so set, and module_probe_mismatch where the probe gave other bytes. Where the need is none this check passes, and the output holds no tier.
At the integer level: a sink SHOULD decode one vector of the capability’s module corpus (§9.2) once per engine and setting in each process, before the module’s first run there, and compare the output with the vector’s digest. A difference is module_probe_mismatch. This catches an engine that does not implement WebAssembly 3.0 as written; the level’s semantics do not need it.

11. Instantiate with an empty import object. A sink SHOULD reserve the memory’s declared maximum where its engine allows it. A failure to instantiate or to reserve is module_resources. Then the calls of §5, steps 1 and 2.

12. Run wai_run under a guard: an instruction budget the engine counts, or a wall-clock limit the sink enforces (§7). A trap, a stack exhausted among them, is module_trap; an exhausted budget or limit is module_timeout. A sink whose engine reports that a memory.grow failed refuses the run (module_resources) whatever the module then returns. Every sink also relies on R13, which check 9c attests: a page cannot observe a failed grow. Availability can differ between sinks; the output never does.

13. Output. §5’s steps 4 and 5. The sink hashes the decoded medium (SHA-256), and its receipt names the module as §10 states.

A module held at the integer level and run through steps 11 to 13 holds, for its output, what §2 gives that level; one held at the float level holds what §2 gives the float level, only after check 10 passed with the object’s need above none.

7. Engine settings

term	the setting
`threads-off`	the engine refuses shared memory and atomic instructions
`relaxed-off`	the engine refuses relaxed vector instructions
`nan-canonical`	the engine gives every NaN a floating-point instruction generates as the positive canonical NaN, the deterministic profile’s rule
`fuel`	the run is bounded by a budget of instructions the engine counts
`wall-clock`	the run is bounded by a wall-clock limit the sink enforces

A sink, at either level:

instantiates with an empty import object, and links no host interface;
limits the memory’s growth to the module’s declared maximum, and its stack to a fixed size, the same for every run;
bounds every run of wai_run with fuel or wall-clock;
SHOULD set threads-off and relaxed-off where its engine can be so set, as a second guard behind R2 and R4.

At the float level a sink also sets nan-canonical, and check 10’s probe shows it. A sink MUST NOT take an engine setting that fixes the behaviour of relaxed vector instructions for the deterministic profile: both levels refuse those instructions (R4), and only the probe shows an engine’s NaN behaviour. A page takes check 10 as failed: the output of a float-level module in a page holds no tier, and a page decodes through one only an object whose need is none.

The engine a receipt names (§10) is written <engine>@<version>, optionally followed by /<compiler>: <engine> and <compiler> are 1 to 64 of a–z, 0–9, _ and -, and <version> is 1 to 64 of ASCII letters, digits, ., + and -, beginning with a digit. A budget’s instruction count is not energy, and no receipt states it.

8. Refusal codes

code	raised at	then
`module_profile_violation`	§6 check 9a, 9b: with the rule and the offset of the verdict (§4.3)	the module is not held for the object
`module_unattested`	§6 check 9c	the module is not held for the object
`module_engine_not_deterministic`	§6 check 10	the module is not held for an object whose need is above `none`
`module_probe_mismatch`	§6 check 10	the module is not held for the object
`module_resources`	§6 check 11 (instantiation, reservation, `wai_alloc` returning `0`) and check 12 (a failed `memory.grow` the engine reports)	the object’s decode through the module is refused
`module_trap`	§6 check 12	the object’s decode through the module is refused
`module_timeout`	§6 check 12	the object’s decode through the module is refused
`module_result_invalid`	§5 steps 1, 4 and 5 (§6 checks 11 and 13)	the object’s decode through the module is refused

In each case nothing is output, and dispatch continues as §6 states. A refusal the module returns through wai_run is its capability’s own, and routes as that capability’s text routes it.

9. Corpora

9.1 The checker corpus

A conforming checker gives each module below the verdict stated, at the level and under the caps stated. Each module is given by its construction: any bytes built as its row describes are that module, and the offset in its verdict is that of the item the row names, in those bytes (§4.3). Caps not stated are the profile’s (§4.2).

Planted modules.

case	level, caps	the module	verdict
`oversize`	both; `module_bytes` one below the module’s length	`minimal-int`, unchanged	`refused R1 0`
`invalid`	both	a function whose body leaves an `i64` where its type returns `i32`	`refused R2 -`
`shared-memory`	both	a shared memory and an `i32.atomic.load`	`refused R2 -`
`component`	both	a component’s preamble	`refused R2 -`
`scalar-float`	integer	`f32.add` of two `f32.const`s in `wai_run`	`refused R3`, at the first `f32.const`
`float-unreachable`	integer	`f32.add` and `drop` in `wai_run` after a `return`, where the operand stack is polymorphic and no earlier item gives a floating-point value	`refused R3`, at the `f32.add`
`float-block-type`	integer	a block in `wai_run` whose type is the result `f32`, holding only `unreachable`, its result dropped	`refused R3`, at the block type’s value type
`float-select-type`	integer	a typed `select` whose type is `f32` in `wai_run` after a `return`, where the operand stack is polymorphic, its result dropped	`refused R3`, at its value type
`float-constant`	integer	a global initialised by `f64.const`	`refused R3`, at the global’s value type
`float-signature`	integer	a function type with an `f64` parameter	`refused R3`, at that value type
`float-vector`	integer	`f32x4.add`	`refused R3`, at the instruction
`float-conversion`	integer	`f32x4.convert_i32x4_s`	`refused R3`, at the instruction
`float-truncation`	integer	`i32.trunc_sat_f32_s` on an `f32` built by `f32.reinterpret_i32`	`refused R3`, at `f32.reinterpret_i32`
`float-load`	integer	`f32.load`	`refused R3`, at the instruction
`relaxed-swizzle`	both	`i8x16.relaxed_swizzle`	`refused R4`, at the instruction
`relaxed-laneselect`	both	`i16x8.relaxed_laneselect`	`refused R4`, at the instruction
`relaxed-dot`	both	`i16x8.relaxed_dot_i8x16_i7x16_s`	`refused R4`, at the instruction
`relaxed-madd`	float	`f32x4.relaxed_madd`	`refused R4`, at the instruction
`import-function`	both	an imported function returning an `i32` (a clock)	`refused R5`, at the import
`import-memory`	both	its memory imported, not defined	`refused R5`, at the import; it breaks R6 too, which §4.3 reports only after every item
`import-global`	both	an imported immutable `i32` global	`refused R5`, at the import
`no-memory`	both	no memory: its memory, its export `memory` and the store in `wai_run` removed	`refused R6`, at the module’s length; it breaks R10 too, which §4.3 reports after R6
`two-memories`	both	a second memory	`refused R6`, at the second memory’s entry
`memory64`	both	its memory of address type `i64`, and the store in `wai_run` addressed by an `i64`	`refused R6`, at the memory’s entry
`no-maximum`	both	its memory with no maximum	`refused R6`, at the memory’s entry
`over-pages`	both; `memory_pages` 16	its memory’s maximum 17	`refused R6`, at the memory’s entry
`two-tables`	both	two `funcref` tables, each with its minimum its maximum	`refused R7`, at the second table’s entry
`externref-table`	both	a table of `externref`, its minimum its maximum	`refused R7`, at the table’s entry
`table-unfixed`	both	a `funcref` table whose minimum is below its maximum	`refused R7`, at the table’s entry
`table-grow`	both	a `funcref` table, its minimum its maximum, and `table.grow`	`refused R7`, at the instruction
`table-set`	both	the same table, and `table.set`	`refused R7`, at the instruction
`table-fill`	both	the same table, and `table.fill`	`refused R7`, at the instruction
`start`	both	a start section	`refused R8`, at the section’s id byte
`funcref-parameter`	both	a function of the module, not exported, with a `funcref` parameter	`refused R9`, at that value type
`externref-global`	both	a global of type `externref`	`refused R9`, at its value type
`funcref-local`	both	a local of type `funcref`	`refused R9`, at its value type
`i64-export`	both	`wai_run` with its last parameter an `i64`	`refused R10`, at the export’s entry
`extra-export`	both	a seventh export, a function	`refused R10`, at that export’s entry
`exported-global`	both	an exported global	`refused R10`, at that export’s entry
`missing-run`	both	no export `wai_run`	`refused R10`, at the module’s length
`over-functions`	both; `functions` 8	nine functions	`refused R11`, at the function section’s id byte
`tail-call`	both	`return_call`	`refused R12`, at the instruction
`exception`	both	a tag section and `throw`	`refused R12`, at the tag section’s id byte
`struct-type`	both	a struct type in the type section	`refused R12`, at that type entry
`call-ref`	both	`call_ref` of a `ref.func` naming `wai_abi`, which a declarative element segment declares	`refused R12`, at the instruction

Every planted module but component is the module minimal-int (below) with the change named, which breaks the rule named. Two of them, import-memory and no-memory, cannot break it alone, and their rows say which other rule they break and why the verdict is the one stated. Where a row adds an instruction, unless it says otherwise, the instruction is added to wai_run before its store, its operands are i32.consts, v128.consts 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 named `profile` whose contents 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.