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

wai: the deterministic module profile, a checked subset of WebAssembly for the decoder modules a sink runs #640

Closed
dcharlot wants to merge 2 commits from wai/det-module-profile into main
pull from: wai/det-module-profile
merge into: Transaction-Science:main
Conversation 0 Commits 2 Files changed 9 +641 -22
9 changed files with 641 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

4
wai/SPEC.md
View file

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

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

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

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

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

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

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

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

@ -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.

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

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

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

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

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

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

11
wai/wai-rs/tests/fixtures/dev-stack/fake-stack.py vendored
View file

@ -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