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<n> <offset>`, with `<n>` the rule and `<offset>` a decimal byte offset into the
+module, or `-`. It is a function of the module's bytes, the level and the caps, and it is
+decided in this order:
+
+1. R1: a module longer than `module_bytes` is `refused R1 0`, and is not read further.
+2. R2: a module that does not decode, or is not valid, is `refused R2 -`. Decoders and
+   validators report such a failure at different offsets, so this verdict carries none.
+3. R3 to R12, over the items of the module in binary order: the first item that breaks one of
+   them is refused at its offset, by the lowest-numbered rule it breaks. The offset of an
+   instruction is that of its first byte (for a prefixed opcode, the prefix); of a value type,
+   its first byte; of an entry or a type entry, its first byte; of a section, its id byte. R11
+   is broken by the function section; a table instruction that R7 refuses, by that instruction.
+4. Then the rules an absence breaks, in rule order, at the offset equal to the module's length:
+   R6 where the module defines no memory, and R10 where an export of §5 is missing.
+5. Otherwise `held`.
+
+A module that breaks rules at several items is refused at the first; a sink reports that rule.
+Since the levels differ only in R3, a module refused R3 at the integer level is checked at the
+float level, and every other verdict is the same at both.
+
+## 5. The module ABI
+
+A module exports exactly these:
+
+| export | kind and type | what it does |
+|---|---|---|
+| `memory` | the module's one memory | holds every buffer the sink passes in and reads out |
+| `wai_abi` | function `() → i32` | returns `1`, the version of this interface |
+| `wai_alloc` | function `(len: i32) → i32` | returns the offset of a region of `len` bytes the module will not otherwise use, or `0` where it cannot |
+| `wai_run` | function `(cap_ptr: i32, cap_len: i32, in_ptr: i32, in_len: i32, set_ptr: i32, set_len: i32) → i32` | decodes one object; returns `0` when the output is the decoded medium, or `1` when it is a refusal code |
+| `wai_out_ptr` | function `() → i32` | the offset of the output |
+| `wai_out_len` | function `() → i32` | the output's length, in bytes |
+
+A sink decodes an object through a module on an instance of its own: it instantiates the module
+for that object, makes these calls once each, in this order, and discards the instance.
+
+1. `wai_abi()`. A result other than `1` is `module_result_invalid`.
+2. For each of three inputs, in this order: the capability, as the UTF-8 bytes of its term; the
+   payload, the bytes the envelope carries for that capability; and the set, the pinned parameter
+   set in its pin's form, which SPEC §3.1's checks 6–8 have held to its digest. The sink calls
+   `wai_alloc(len)` with the input's length and writes the input at the offset returned. A result
+   of `0` is `module_resources`. A capability that decodes against no set passes `0, 0` for it,
+   with no call.
+3. `wai_run` with the three offsets and lengths, under the guard of §6 check 12.
+4. `wai_out_ptr()` and `wai_out_len()`. A region that does not lie within the memory is
+   `module_result_invalid`.
+5. Where `wai_run` returned `0`, the region is the decoded medium in its capability's canonical
+   buffer ([determinism-tiers](determinism-tiers.md) §2: canonical RGB8 for an image, int16 PCM,
+   the attribute tensor, a per-frame hash for video). Where it returned `1`, the region is a
+   refusal code in ASCII, one of the codes the text that defines the capability's payload lists
+   for its decode, and the decode is refused with that code, as that text routes it. Any other
+   result of `wai_run`, or a refusal text that is not such a code, is `module_result_invalid`.
+
+Nothing else reaches the module: it imports nothing (R5), runs nothing at instantiation (R8), and
+starts from its own bytes on every instance. So the output is a function of the capability, the
+payload and the set. A decode that reads anything else, such as the decoded state of another
+object, is not one this interface carries.
+
+## 6. How a sink checks and runs a module
+
+A sink that decodes an object through a module takes these steps in order and reports the first
+that fails. A failure at steps 1 to 10 means the module is not held for the object: the capability
+is unsupported for that envelope at that sink, and dispatch continues to the declared fallback or
+a sibling rendition (jwp-receipts §7.9, *Fail closed*, *Fallback, never inert*). A failure at
+steps 11 to 13 refuses the object's decode through the module, and dispatch continues the same
+way; nothing is output.
+
+**0. Identity.** The SHA-256 of the exact bytes the sink will instantiate (jwp-receipts §7.9,
+*Identity*).
+
+**1–8. Authorisation.** jwp-receipts §7.9's checks 1 to 8, unchanged.
+
+**9. Profile.**
+- **9a. The module:** rules R1 and R2.
+- **9b. Its contents:** rules R3 to R12. The sink checks the module at the integer level, and,
+  where its verdict there is `refused R3`, at the float level. The module's level is the first
+  whose verdict is `held`. Otherwise the sink reports `module_profile_violation` with the
+  verdict of the last level it checked, its rule and its offset. A sink **MAY** keep the verdict
+  of 9a and 9b by the module's digest, its level and its caps, since nothing else decides it.
+- **9c. Attestation.** The sink holds a `conform-result/1` record
+  ([conformance-results](conformance-results.md) §2) that attests this module for the capability
+  being decoded: the record is admitted under conformance-results §4.1 against the module corpus
+  of §9.2 for that capability, as the sink holds it; its `kind` is `decoder` and its `suite` is
+  `module/` followed by the capability's term; an entry of its `implementation.files` has the
+  module's digest as its `sha256`; its `key` is `supplied`; and its `signer_pubkey` is a key the
+  grant's origin lists with `module/decoder`: the head jwp-receipts §7.4 step 3 reached for the
+  grant at jwp-receipts §7.9's check 3 lists an entry whose `key` is that `signer_pubkey`, which
+  is not `revoked`, carries no `pq_key` ([pq-signatures](pq-signatures.md) §6.1: a hybrid entry
+  signs nothing with Ed25519 alone, and a record has no other signature), holds `module/decoder` in its
+  `may_sign`, and, where it is `retired`, has an `until` no earlier than the record's
+  `started_at`, the two compared as jwp-receipts §7.4 compares times. Otherwise
+  `module_unattested`. The record carries no `signer_id`, so it is no item jwp-receipts §7.4
+  confirms: this check reads the head the grant was confirmed under, and nothing else of the
+  key log.
+
+**10. Engine.**
+- At the float level, where the object's need is above `none`: the sink's engine is set to the
+  deterministic profile's NaN rule (§7, `nan-canonical`), and the probe of §9.3, run in this
+  process on that engine and setting before the module's first run, gave the probe's bytes.
+  Otherwise `module_engine_not_deterministic` where the engine cannot be so set, and
+  `module_probe_mismatch` where the probe gave other bytes. Where the need is `none` this check
+  passes, and the output holds no tier.
+- At the integer level: a sink **SHOULD** decode one vector of the capability's module corpus
+  (§9.2) once per engine and setting in each process, before the module's first run there, and
+  compare the output with the vector's digest. A difference is `module_probe_mismatch`. This
+  catches an engine that does not implement WebAssembly 3.0 as written; the level's semantics do
+  not need it.
+
+**11. Instantiate** with an empty import object. A sink **SHOULD** reserve the memory's declared
+maximum where its engine allows it. A failure to instantiate or to reserve is `module_resources`.
+Then the calls of §5, steps 1 and 2.
+
+**12. Run** `wai_run` under a guard: an instruction budget the engine counts, or a wall-clock
+limit the sink enforces (§7). A trap, a stack exhausted among them, is `module_trap`; an
+exhausted budget or limit is `module_timeout`. A sink whose engine reports that a `memory.grow`
+failed refuses the run (`module_resources`) whatever the module then returns. Every sink also
+relies on R13, which check 9c attests: a page cannot observe a failed grow. Availability can
+differ between sinks; the output never does.
+
+**13. Output.** §5's steps 4 and 5. The sink hashes the decoded medium (SHA-256), and its
+receipt names the module as §10 states.
+
+A module held at the integer level and run through steps 11 to 13 holds, for its output, what §2
+gives that level; one held at the float level holds what §2 gives the float level, only after
+check 10 passed with the object's need above `none`.
+
+## 7. Engine settings
+
+| term | the setting |
+|---|---|
+| `threads-off` | the engine refuses shared memory and atomic instructions |
+| `relaxed-off` | the engine refuses relaxed vector instructions |
+| `nan-canonical` | the engine gives every NaN a floating-point instruction generates as the positive canonical NaN, the deterministic profile's rule |
+| `fuel` | the run is bounded by a budget of instructions the engine counts |
+| `wall-clock` | the run is bounded by a wall-clock limit the sink enforces |
+
+A sink, at either level:
+- instantiates with an empty import object, and links no host interface;
+- limits the memory's growth to the module's declared maximum, and its stack to a fixed size, the
+  same for every run;
+- bounds every run of `wai_run` with `fuel` or `wall-clock`;
+- **SHOULD** set `threads-off` and `relaxed-off` where its engine can be so set, as a second guard
+  behind R2 and R4.
+
+At the float level a sink also sets `nan-canonical`, and check 10's probe shows it. A sink
+**MUST NOT** take an engine setting that fixes the behaviour of relaxed vector instructions for
+the deterministic profile: both levels refuse those instructions (R4), and only the probe shows
+an engine's NaN behaviour. A page takes check 10 as failed: the output of a float-level module
+in a page holds no tier, and a page decodes through one only an object whose need is `none`.
+
+The **engine** a receipt names (§10) is written `<engine>@<version>`, optionally followed by
+`/<compiler>`: `<engine>` and `<compiler>` are 1 to 64 of `a`–`z`, `0`–`9`, `_` and `-`, and
+`<version>` is 1 to 64 of ASCII letters, digits, `.`, `+` and `-`, beginning with a digit. A
+budget's instruction count is not energy, and no receipt states it.
+
+## 8. Refusal codes
+
+| code | raised at | then |
+|---|---|---|
+| `module_profile_violation` | §6 check 9a, 9b: with the rule and the offset of the verdict (§4.3) | the module is not held for the object |
+| `module_unattested` | §6 check 9c | the module is not held for the object |
+| `module_engine_not_deterministic` | §6 check 10 | the module is not held for an object whose need is above `none` |
+| `module_probe_mismatch` | §6 check 10 | the module is not held for the object |
+| `module_resources` | §6 check 11 (instantiation, reservation, `wai_alloc` returning `0`) and check 12 (a failed `memory.grow` the engine reports) | the object's decode through the module is refused |
+| `module_trap` | §6 check 12 | the object's decode through the module is refused |
+| `module_timeout` | §6 check 12 | the object's decode through the module is refused |
+| `module_result_invalid` | §5 steps 1, 4 and 5 (§6 checks 11 and 13) | the object's decode through the module is refused |
+
+In each case nothing is output, and dispatch continues as §6 states. A refusal the module returns
+through `wai_run` is its capability's own, and routes as that capability's text routes it.
+
+## 9. Corpora
+
+### 9.1 The checker corpus
+
+A conforming checker gives each module below the verdict stated, at the level and under the caps
+stated. Each module is given by its construction: any bytes built as its row describes are that
+module, and the offset in its verdict is that of the item the row names, in those bytes (§4.3).
+Caps not stated are the profile's (§4.2).
+
+**Planted modules.**
+
+| case | level, caps | the module | verdict |
+|---|---|---|---|
+| `oversize` | both; `module_bytes` one below the module's length | `minimal-int`, unchanged | `refused R1 0` |
+| `invalid` | both | a function whose body leaves an `i64` where its type returns `i32` | `refused R2 -` |
+| `shared-memory` | both | a shared memory and an `i32.atomic.load` | `refused R2 -` |
+| `component` | both | a component's preamble | `refused R2 -` |
+| `scalar-float` | integer | `f32.add` of two `f32.const`s in `wai_run` | `refused R3`, at the first `f32.const` |
+| `float-unreachable` | integer | `f32.add` and `drop` in `wai_run` after a `return`, where the operand stack is polymorphic and no earlier item gives a floating-point value | `refused R3`, at the `f32.add` |
+| `float-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=<origin>`. A parameter set that is not
 held adds the refusal SPEC §3.1's check 5 reports: `refusal=prior_revoked` where its
 digest is revoked, `refusal=prior_not_authorised` for any other check. A parameter set
diff --git a/wai/wai-rs/tests/fixtures/dev-stack/fake-stack.py b/wai/wai-rs/tests/fixtures/dev-stack/fake-stack.py
index cce944f03..f8c7a71e4 100755
--- a/wai/wai-rs/tests/fixtures/dev-stack/fake-stack.py
+++ b/wai/wai-rs/tests/fixtures/dev-stack/fake-stack.py
@@ -15,6 +15,7 @@ import json
 import os
 import re
 import socket
+import socketserver
 import sys
 import threading
 import time
@@ -55,6 +56,14 @@ class Room(http.server.BaseHTTPRequestHandler):
         pass
 
 
+class Server(http.server.ThreadingHTTPServer):
+    """HTTPServer looks up a name for its address before it listens, and nothing here reads the
+    name. On some hosts that lookup takes 35 s, past what `wai dev` waits for a service."""
+
+    def server_bind(self):
+        socketserver.TCPServer.server_bind(self)
+
+
 def main(argv):
     if argv[:1] in (["keygen"], ["relay-lines"]):
         open(argv[1], "a").close()
@@ -73,7 +82,7 @@ def main(argv):
         while True:
             c, _ = s.accept()
             c.close()
-    http.server.ThreadingHTTPServer(listen_addr(config, "listen"), Room).serve_forever()
+    Server(listen_addr(config, "listen"), Room).serve_forever()
     return 0