open-standards/wai/extensions/waism.md
Transaction Science 98d646dc92 wai-int-module: the first WA²ISM module of record, the operator-set module held at the integer level on every engine
wai/wai-int-module is one WebAssembly module with the interface of waism §5 and nothing else:
no import, one memory with a declared maximum, and every allocation trapping where memory
cannot grow (R13). It decodes the integer payloads (WIV1, WIH1, WIA1, WIS1), int_synth,
int_mlicpp, opus.dred.int and avatar.face through wai-rs's integer decoders, whose networks
run on wai-ops/1; networks and weights arrive as each capability's set.

- record/: the scalar and SIMD128 builds (7,099 vector instructions), named by SHA-256 in
  manifest.json, each held at the integer level by the Rust checker and check-module.mjs.
  build.sh builds both with the machine's paths remapped and checks both with both checkers.
  A build on another host has other bytes (the compiler's crate hashes take in each path
  dependency's absolute path and the host) and gives every case the same outcome.
- corpus.json (corpus.py): every committed vector and refusal fixture of those
  capabilities, 120 cases, from the committed corpora.
- host/ (wasmtime 50.0.1 Cranelift and Winch, Wasmi 2.0.0 with floats off), run-node.mjs and
  browser/run-browser.mjs run every case as a sink does and print one run digest; every run,
  on Linux x86_64, Linux arm64 and macOS arm64, gives the same.
- plant.py plants a float or a relaxed vector instruction in a module, for the checkers.
- waism §5, The set: one file as its bytes, several as their file sequence. avatars §6 names
  generator.wfg and identity.wfi; avatars §7.8, opus-dred §4.8 and determinism-tiers §5 state
  the module as a fabric.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-11-08 16:45:56 -05:00

40 KiB
Raw Permalink Blame History

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

Status: Draft. WA²ISM™, named WAISM™ in running text, is WAI's deterministic module profile: a checked subset of standard WebAssembly, run by unmodified engines. It is not a fork of WebAssembly and not a new bytecode: it adds no instruction, type, section or semantics, and any engine that implements WebAssembly 3.0 runs a module that meets it. What the profile decides is what a sink may state about such a module's output. It has two levels (§2): an integer level, with no floating point, whose output is the same on every engine with no engine setting; and a float level, which admits floating point and holds a tier only on an engine set to the NaN rule of the deterministic profile of WebAssembly 3.0. A sink checks a decoder module against numbered rules (§4) before it instantiates it, holds a signed conformance result over the module's digest (§6, check 9c), runs it through a fixed interface (§5) under the settings of §7, refuses with the codes of §8, and names what it checked in its receipt (§10). Checks 9 to 13 follow jwp-receipts §7.9's checks 1 to 8, which authorise the module and which this text leaves as they are. The corpora a checker, a module and an engine are held to are in §9. This text defines the profile; it names no implementation. Keywords MUST, MUST NOT, SHOULD, MAY are RFC 2119/8174.

Texts read for this revision: WebAssembly 3.0, the specification build dated 2026-11-04: the appendix Profiles (Defined Profiles: the full profile, FUL, and the deterministic profile, DET); the appendix Implementation Limitations (Execution); Execution, Numerics (Floating-Point Operations: Rounding, NaN Propagation; Relaxed Operations) and Instructions (memory.grow); Binary Format, Types (limits) and Modules (the preamble, the section ids, custom sections, the start section). A section number in this text is this extension's unless it names another document.

1. Scope

In scope: the two levels (§2); the rules a module meets, the caps and a checker's verdict (§4); the interface a module exports (§5); the steps a sink takes to check and run a module (§6); the engine settings it uses (§7); the refusal codes (§8); the corpora (§9); what a receipt states (§10); and conformance (§11).

Out of scope: how a sink obtains a module and who may grant it (jwp-receipts §7.9, http-delivery §8.4); reconstruct modules, and decoder modules a sink runs on no WebAssembly engine, which this text does not cover; the arithmetic a decoder computes, which its capability's text fixes (integer-operators for the integer graphs); and a pinned parameter set, which is data and is held by jwp-receipts §7.9's checks 1 to 8 alone.

Relationship to WebAssembly and to the other texts:

  • WebAssembly 3.0. Core WebAssembly leaves open the sign and payload of a NaN, the results of the relaxed vector instructions, whether memory.grow and table.grow succeed, what an engine does past its resource limits, and every value a host supplies through an import. Every other result is fixed: integer instructions are exact, and floating-point ones are rounded to nearest, ties to even (Numerics, Rounding). The deterministic profile (DET) of WebAssembly 3.0 (appendix Profiles, Defined Profiles) fixes the first two: every NaN a floating-point instruction generates is canonical and positive, and every relaxed vector instruction has one behaviour. Under it, memory.grow and table.grow remain non-deterministic. The integer level refuses floating point and relaxed vector instructions, so nothing the deterministic profile changes is reachable from it, and it needs no engine setting. The float level needs the deterministic profile's NaN rule, and nothing else of it is reachable, since both levels refuse relaxed vector instructions (R4). Both levels refuse imports, fix the memory and the table, and turn a failed memory.grow into a refusal.
  • jwp-receipts §7.9. A module's identity is its digest, the SHA-256 of its bytes as instantiated, and its grant, key log, revocation and fallback are §7.9's. Its checks 9 and 10 are this text's (§6).
  • jwp-receipts §2.4.12. The decoder entry of a reconstruct-session claim names the level, the engine, its settings, the probe and the conformance result (§10).
  • conformance-results. The record a sink holds for check 9c.
  • browser-sink §4.3 step 6. The tier a page's wasm decoder holds.
  • determinism-tiers §5 and SPEC §7. WebAssembly as a fabric of decode-equivalence is a module held at the integer level.
  • integer-operators §6. On WebAssembly, two of that section's "MUST NOT"s are properties of the module a sink checks.

2. Levels

The profile's identifiers are defined here, and only here. Every other text, this one included, names a level as the integer level or the float level.

level identifier floating point engine what its output holds
integer level waism/1-int refused (R3) any engine that implements WebAssembly 3.0, a browser's included, with no setting the class tier of its capability (SPEC §3.1, Tier) and, for a GenerativeDeterministic capability, its generation-equivalence (SPEC §7)
float level waism/1-det admitted only an engine set to the deterministic profile's NaN rule, shown by the probe (§6, check 10); no page (§7) entropy-consistency where that is the class tier of its capability, on such an engine; otherwise none. Never decode-equivalence or generation-equivalence: SPEC §7, Replicate-soundness, admits a neural decode at decode-equivalence only where no floating-point operation is on its path, and this revision gives the float level neither

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

3. Terms

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

4. Rules

4.1 The rules

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

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

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

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

4.2 Caps and validation limits

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

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

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

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

4.3 The verdict

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

  1. R1: a module longer than module_bytes is refused R1 0, and is not read further.
  2. R2: a module that does not decode, or is not valid, is refused R2 -. Decoders and validators report such a failure at different offsets, so this verdict carries none.
  3. R3 to R12, over the items of the module in binary order: the first item that breaks one of them is refused at its offset, by the lowest-numbered rule it breaks. The offset of an instruction is that of its first byte (for a prefixed opcode, the prefix); of a value type, its first byte; of an entry or a type entry, its first byte; of a section, its id byte. R11 is broken by the function section; a table instruction that R7 refuses, by that instruction.
  4. Then the rules an absence breaks, in rule order, at the offset equal to the module's length: R6 where the module defines no memory, and R10 where an export of §5 is missing.
  5. Otherwise held.

A module that breaks rules at several items is refused at the first; a sink reports that rule. Since the levels differ only in R3, a module refused R3 at the integer level is checked at the float level, and every other verdict is the same at both.

5. The module ABI

A module exports exactly these:

export kind and type what it does
memory the module's one memory holds every buffer the sink passes in and reads out
wai_abi function () → i32 returns 1, the version of this interface
wai_alloc function (len: i32) → i32 returns the offset of a region of len bytes the module will not otherwise use, or 0 where it cannot
wai_run function (cap_ptr: i32, cap_len: i32, in_ptr: i32, in_len: i32, set_ptr: i32, set_len: i32) → i32 decodes one object; returns 0 when the output is the decoded medium, or 1 when it is a refusal code
wai_out_ptr function () → i32 the offset of the output
wai_out_len function () → i32 the output's length, in bytes

A sink decodes an object through a module on an instance of its own: it instantiates the module for that object, makes these calls once each, in this order, and discards the instance.

  1. wai_abi(). A result other than 1 is module_result_invalid.
  2. For each of three inputs, in this order: the capability, as the UTF-8 bytes of its term; the payload, the bytes the envelope carries for that capability; and the set, the files the decode reads beside the payload, as The set below gives them. The sink calls wai_alloc(len) with the input's length and writes the input at the offset returned. A result of 0 is module_resources. A capability that decodes against no set passes 0, 0 for it, with no call.
  3. wai_run with the three offsets and lengths, under the guard of §6 check 12.
  4. wai_out_ptr() and wai_out_len(). A region that does not lie within the memory is module_result_invalid.
  5. Where wai_run returned 0, the region is the decoded medium in its capability's canonical buffer (determinism-tiers §2: canonical RGB8 for an image, int16 PCM, the attribute tensor, a per-frame hash for video). Where it returned 1, the region is a refusal code in ASCII, one of the codes the text that defines the capability's payload lists for its decode, and the decode is refused with that code, as that text routes it. Any other result of wai_run, or a refusal text that is not such a code, is module_result_invalid.

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

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

6. How a sink checks and runs a module

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

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

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

9. Profile.

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

10. Engine.

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

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

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

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

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

7. Engine settings

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

A sink, at either level:

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

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

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

8. Refusal codes

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

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

9. Corpora

9.1 The checker corpus

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

Planted modules.

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

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

Conforming modules.

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