open-standards/wai/extensions/waism.md

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

> 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](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 | `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](../SPEC.md) §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](browser-sink.md)
  §2 defines it, for any sink: the object's pin `tier`, else its track's declared determinism,
  else `none`.
- **Held at a level**: a sink holds a module at a level, for an object, when checks 1 to 10 of §6
  pass for it at that level.

## 4. Rules

### 4.1 The rules

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

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

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 files the decode
   reads beside the payload, as *The set* below gives them. 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`.

**The set.** The files a decode reads beside its payload are its capability's parameter set,
which SPEC §3.1's checks 6–8 have held to its pin's digest, and any file the capability's text
has the payload name by its digest, which the decode refuses where the file's digest is another
([avatars](avatars.md) §6's identity prior). Where those are one file, the set is that file's
bytes. Where they are more, the set is their **file sequence**: for each file, in ascending
byte order of its name, the name's length as one byte, from 1 to 255; the name, in UTF-8; the
file's length as four bytes, little-endian; and the file's bytes; with nothing between or
after. A file's name is its path in the set's listing (SPEC §3.1, the form `wai.prior.set`),
or the name the capability's text gives it. So the set of `wai.neural.int_hyper` is the file
sequence of `entropy.json`, `g_s.whm` and `h_s.whm`, and the set of `wai.avatar.face` the
file sequence of `generator.wfg` and `identity.wfi`. A file sequence names no file twice. An
input that is not the form its capability's set takes is not one this interface carries: the
module traps (§6, check 12), and nothing is output.

Nothing else reaches the module: it imports nothing (R5), runs nothing at instantiation (R8), and
starts from its own bytes on every instance. So the output is a function of the capability, the
payload and the set. A decode that reads anything else, such as the decoded state of another
object, is not one this interface carries.

## 6. How a sink checks and runs a module

A sink that decodes an object through a module takes these steps in order and reports the first
that fails. A failure at steps 1 to 10 means the module is not held for the object: the capability
is unsupported for that envelope at that sink, and dispatch continues to the declared fallback or
a sibling rendition (jwp-receipts §7.9, *Fail closed*, *Fallback, never inert*). A failure at
steps 11 to 13 refuses the object's decode through the module, and dispatch continues the same
way; nothing is output.

**0. Identity.** The SHA-256 of the exact bytes the sink will instantiate (jwp-receipts §7.9,
*Identity*).

**1–8. Authorisation.** jwp-receipts §7.9's checks 1 to 8, unchanged.

**9. Profile.**
- **9a. The module:** rules R1 and R2.
- **9b. Its contents:** rules R3 to R12. The sink checks the module at the integer level, and,
  where its verdict there is `refused R3`, at the float level. The module's level is the first
  whose verdict is `held`. Otherwise the sink reports `module_profile_violation` with the
  verdict of the last level it checked, its rule and its offset. A sink **MAY** keep the verdict
  of 9a and 9b by the module's digest, its level and its caps, since nothing else decides it.
- **9c. Attestation.** The sink holds a `conform-result/1` record
  ([conformance-results](conformance-results.md) §2) that attests this module for the capability
  being decoded: the record is admitted under conformance-results §4.1 against the module corpus
  of §9.2 for that capability, as the sink holds it; its `kind` is `decoder` and its `suite` is
  `module/` followed by the capability's term; an entry of its `implementation.files` has the
  module's digest as its `sha256`; its `key` is `supplied`; and its `signer_pubkey` is a key the
  grant's origin lists with `module/decoder`: the head jwp-receipts §7.4 step 3 reached for the
  grant at jwp-receipts §7.9's check 3 lists an entry whose `key` is that `signer_pubkey`, which
  is not `revoked`, carries no `pq_key` ([pq-signatures](pq-signatures.md) §6.1: a hybrid entry
  signs nothing with Ed25519 alone, and a record has no other signature), holds `module/decoder` in its
  `may_sign`, and, where it is `retired`, has an `until` no earlier than the record's
  `started_at`, the two compared as jwp-receipts §7.4 compares times. Otherwise
  `module_unattested`. The record carries no `signer_id`, so it is no item jwp-receipts §7.4
  confirms: this check reads the head the grant was confirmed under, and nothing else of the
  key log.

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

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

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

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

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

## 7. Engine settings

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

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

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

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

## 8. Refusal codes

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

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

## 9. Corpora

### 9.1 The checker corpus

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

**Planted modules.**

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

Every planted module but `component` is the module `minimal-int` (below) with the change
named, which breaks the rule named. Two of them, `import-memory` and `no-memory`, cannot break
it alone, and their rows say which other rule they break and why the verdict is the one stated.
Where a row adds an instruction, unless it says otherwise, the instruction is added to `wai_run`
before its store, its operands are `i32.const`s, `v128.const`s or `ref.null func`, as its type
takes, and a result it leaves is dropped. None of those is a floating-point item, so the
instruction is the first item of the module that breaks a rule. An instruction that takes a
floating-point operand has an earlier item that gives one, which §4.3 refuses first, except in
code the operand stack reaches as polymorphic, as `float-unreachable` places it.

**Conforming modules.**

| case | the module | verdict |
|---|---|---|
| `minimal-int` | the interface of §5 and nothing else: one memory of minimum 1 page and maximum 2; no table, global, data segment, element segment or custom section; `wai_abi` returns 1, `wai_alloc` returns 0, `wai_run` stores one fixed byte at offset 0 with `i32.store8` and returns 0, `wai_out_ptr` returns 0 and `wai_out_len` returns 1; no function reads a parameter | `held` at both levels |
| `vector-int` | `minimal-int` with `i32x4.dot_i16x8_s`, `i8x16.swizzle`, `i8x16.shuffle` and `i16x8.q15mulr_sat_s` | `held` at both levels |
| `bulk-and-sign` | `minimal-int` with `memory.copy`, `memory.fill`, `i32.extend8_s` and a block of two results | `held` at both levels |
| `fixed-table` | `minimal-int` with one `funcref` table, its minimum its maximum, an element segment and `call_indirect` | `held` at both levels |
| `fixed-memory` | `minimal-int` whose memory's minimum is its maximum, with no `memory.grow` | `held` at both levels |
| `custom-section` | `minimal-int` with a custom section 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.