open-standards/wai/extensions/quantum-wasmq.md

# WAI Extension: Hybrid Quantum-Classical Execution (`wai.quantum.wasmq`)

Status: **Draft.** Reference implementation: `wai-wasmq` (the profile, `src/profile.rs`;
the prepared module, `src/meter.rs`; the interpreter, `src/interp.rs`; the engines,
`src/engine.rs`; the lowering, `src/abi.rs`; the envelope, `src/envelope.rs`; the run and
its receipt, `src/run.rs`), the OpenQASM reader's callouts (`wai-quantum`,
`qasm::read_callouts`), and the command line's `pack-wasmq`, `check-wasmq`, `run` and
`verify` (`wai-quantum-cli`, `src/wasmq.rs`). A job's form (§6.5) is the engine's, where
every verifier of its receipts reaches it (`wai-quantum`, `engine::wasmq`). Interface: [`quantum-wasmq.wit`](quantum-wasmq.wit).
Vectors: [`../quantum-conformance/wasmq/`](../quantum-conformance/wasmq/).

Keywords **MUST**, **MUST NOT**, **SHOULD** and **MAY** are RFC 2119/8174.

## 0. What this extension adds

A hybrid quantum program runs classical code between its gates: it decodes a syndrome
and corrects the error before the next round, or plans the moves that fill an atom
array. OpenQASM 3 declares such a function with `extern` and leaves its body, its binary
form and how it is linked outside the language. This extension fills that gap for WAI
Quantum, and nothing else:

- **One envelope.** A WAI1 envelope of capability `wai.quantum.wasmq` carries the
  OpenQASM 3 program, the WebAssembly modules that define its `extern`s, and the modules'
  parameter files (priors), each pinned by BLAKE3 in a canonical contract (§2).
- **One profile.** A module is a core WebAssembly module in the Lime1 feature set, which
  imports nothing, whose memory, size and stack are bounded, and which uses nothing whose
  result a host may choose (§3).
- **The same bytes and the same fuel everywhere.** Fuel, the stack's weight and the NaN a
  float instruction makes are defined on the module as written (§4), so every runner
  gives a callout the same results, the same fuel and the same fault. The reference runs
  each module on two engines, a native one and an interpreter that also runs on wasm32,
  and every vector holds on both, on every host.
- **A receipt.** A run seals its result in the job receipt the engine already signs
  (`engine::receipt`): the counts, the fuel each callout used, the modules' digests, a
  digest of every call's inputs and outputs, and the fault that stopped the run, if one
  did (§6).

This version of the profile runs Clifford programs, in whole numbers from end to end
(§5.1, §6.1). A run simulates the quantum program and runs the classical code for real.
§7 says what holds when the quantum part runs on hardware, and §10 what this version
leaves out. Its second version, `wai.quantum.wasmq/2` (§11), adds a method that runs `t`,
Toffoli and gates at dyadic angles on the engine's whole-number state vector, the same bits
on every host; angle arguments for callouts; and the energy a run took, read where its host
meters it and stated unmetered where it does not. A first-version envelope runs, seals and
verifies under it exactly as it did.

## 1. Principles

1. **Nothing outside reaches the result.** A module imports nothing: no clock, no
   random source, no file, no network, no host function. Its only inputs are its bytes,
   its priors, the seed the run gives it and the bits the program passes (§3.2, §5.3).
2. **The host chooses nothing.** Every place where WebAssembly lets an engine choose (a
   NaN's bits, a relaxed vector instruction, how deep calls may go, when memory runs out,
   when to stop a long computation) is fixed by the profile or refused (§3, §4).
3. **Fuel is the measure, not time.** A callout's budget is a number of weighted
   instructions (§4.2). It is the same on every host; wall-clock time is not, and the
   profile does not claim one.
4. **The direction is the hardware's.** The quantum program calls the module, as a
   real-time controller calls classical code between gates. A module drives no gates.
5. **One form for one bundle.** A bundle has exactly one envelope, so its BLAKE3 names
   it, and a receipt that names the digest names the program, the modules, the priors and
   the run (§2.4).
6. **What is read is what runs.** A reader refuses on reading every bundle a run could
   not finish for a reason of the bundle's own (§2.3). A run that starts ends in a
   receipt, unless the host itself fails (§6.3).

## 2. The envelope

### 2.1 Container and manifest

The envelope is a WAI1 container (SPEC §2). Its manifest is, in this order and with no
other member:

```json
{"wai":"1.0","media":"binary","intent":"replicate",
 "model_requirement":{"capability":"wai.quantum.wasmq","fallback":null},
 "conditioning":{"kind":"wasmq"},
 "target":{"qubits":17,"shots":32,"seed":1234}}
```

`fallback` is `null`: a sink without this capability holds no way to run the program's
callouts, so the envelope is inert there (SPEC §4). `target` is informational (SPEC §3)
and is the contract's: the program's qubits (§2.2), the shots and the seed.
`conditioning` carries no `prior`: SPEC §3.1's pin names a parameter set the sink
supplies, and a wasmQ envelope carries its modules' priors itself, each pinned in the
contract (§2.2).

### 2.2 Payload and contract

```text
payload = "WQM1" | u32 contract_len | contract | frames
frames  = program | for each module, in order: the module, then each of its priors in order
```

`contract_len` is little-endian. The contract is JSON in the canonical form of RFC 8785
(JCS), with exactly these members:

| member | |
|---|---|
| `profile` | `"wai.quantum.wasmq/1"` |
| `program` | `{ "blake3", "bytes", "inputs" }`: the OpenQASM 3 source's digest and length, and the values of its integer `input`s (an object, empty when there are none) |
| `modules` | for each module: `{ "name", "blake3", "bytes", "priors": [{ "name", "blake3", "bytes" }] }` |
| `callouts` | one for each `extern` the program declares, in the order it declares them: `{ "extern", "module", "export" }`, the module by its index |
| `run` | `{ "shots", "seed", "method", "state", "fuel": { "per_call", "per_job", "per_instance" } }` (§6.1, §4.2) |

`blake3` is the BLAKE3 digest of the frame as 64 lowercase hexadecimal digits; `bytes`
its length. A `name` is for people. `method` is `stabilizer`, the one method of this
version (§5.1). `state` is `shot` (a fresh instance of each module every shot) or `job`
(one instance for the run, its shots in order). `shots` is 1 to 2^20. `seed` and the
size of each input are at most 2^53 − 1, so that every JSON reader holds them exactly, and
each budget at most 2^39 (§4.8). `per_job` is held to less with any module: its eight
operations for each unit of fuel take all of a run's work at 2^39, and a run's other work
is never nothing (§4.8). Every module is named by
at least one callout. The program's text is at most 1 MiB, and the modules'
bytes at most 512 KiB among them.

**The program's qubits** are the qubits it declares, all its registers together; a program
that declares none and names physical qubits (`$0`, `$5`) has one more than the highest
index it names, the qubits below it among them.

### 2.3 Reading an envelope

A reader MUST refuse an envelope, with the code of §3.3, when:

- it is longer than 128 MiB, its first four bytes are not `WAI1`, its capability is not
  `wai.quantum.wasmq`, its manifest is not the one §2.1 gives for its contract byte for
  byte, or any byte follows the payload (`W013`);
- the payload's magic is not `WQM1`, the contract is not in its RFC 8785 form, holds a
  member §2.2 does not list or lacks one, or the frames do not end exactly where the
  payload ends (`W013`);
- a frame's BLAKE3 is not the one the contract pins: the program, a module, a prior
  (`W014`);
- a module breaks the profile (§3: its code), the modules hold more than 4096 pages among
  them (`W003`, §4.7), or more than 512 KiB of bytes (`W010`);
- the program is longer than 1 MiB, is refused by the reader, calls nothing, has a gate
  outside §5.1's, or is past a bound §4.8 reads it within (`W016`);
- the callouts are not one for each `extern` in the order declared, a module is named
  by none, a callout's export is not the type its `extern` lowers to, or a module the
  host must write to or read a list from does not export what §5.2 asks (`W015`);
- the run is outside §2.2's ranges, or past what §4.8 lets a run ask of its host (`W017`).

A writer checks the same rules and writes nothing that breaks one. An envelope that
passes them runs: nothing about a bundle is left for a run to find (§6.3).

### 2.4 One envelope for one bundle

A writer MUST write the frames in §2.2's order, the contract in its canonical form with
its callouts in the order the program declares its `extern`s, and the manifest exactly
as §2.1 gives it. A reader that holds these rules reads every bundle from exactly one
sequence of bytes, so the envelope's BLAKE3 (`envelope_blake3`) names the bundle, and a
receipt that binds it binds every frame.

## 3. The module profile

### 3.1 A core module

A module is a core WebAssembly module (WebAssembly 3.0, §5 Binary Format), not a
component. It MAY be the core module of a component: its exports are the canonical
lowering of the functions [`quantum-wasmq.wit`](quantum-wasmq.wit) declares, so a
component host can wrap it, and a host of this profile calls it directly.

### 3.2 The rules

A module MUST validate under the **Lime1** feature set of the WebAssembly tool
conventions: WebAssembly 1.0 with mutable globals, multi-value, sign extension,
non-trapping float-to-int conversion, `memory.copy` and `memory.fill`, extended constant
expressions and the overlong `call_indirect` encoding. Every instruction is in the
encoding that feature set gives it, and every function body ends with the `end` of its
own block. And:

| rule | why |
|---|---|
| It imports nothing. | Nothing outside the module reaches its result. A clock, a random source or any host function would. |
| It has at most one memory, 32-bit, unshared, of 64 KiB pages, with a maximum of at most 4096 pages (256 MiB). | A memory without a maximum grows as far as a host lets it, which differs by host. |
| It has no start function. | Nothing runs when an instance is made: every instruction runs in a metered call (§5.3). |
| Nothing shared, no atomic instruction. | Lime1 has no threads. |
| No vector instruction or type, relaxed or not. | A relaxed vector instruction's result is the engine's choice; the profile takes none. |
| No instruction or type of another feature outside Lime1: references, exceptions, tail calls, garbage collection, passive segments. | Lime1's values are numbers. |
| At most one table, of `funcref`, at most 2^16 entries, filled once from active segments of function indices; no instruction reads or changes it but `call_indirect`. | `table.grow` stays non-deterministic in the deterministic profile (below). |
| In every function, at most 4096 parameters, locals and operands at once. | It bounds what one frame holds in an interpreter. |
| At most 512 KiB of bytes, which is also what the modules of a bundle hold among them; at most 2^16 types, functions, globals, data segments and element segments each; at most 2^10 exports, each name at most 256 bytes; a function type of at most 2^8 parameters and 2^8 results; a function's entry in the code section of at most 2^14 bytes. | They bound what a reader, an engine and a frame need (§4.3), with room for what preparing a module adds (§4.4): a body of calls grows some 53 times prepared, and an engine compiles a function whole. |
| Every active data and element segment fits where it is placed. | Instantiation then cannot fail. |
| No export begins `__wasmq`, and an export a host calls has exactly its type (§5.2, §5.3). | The first are the prepared module's names (§4.4); a host passes the second arguments of those types. |

WebAssembly 3.0 defines a deterministic profile: every NaN an instruction makes is
canonical and positive, and every relaxed vector instruction has a fixed behaviour. Even
under it, `memory.grow` and `table.grow` remain non-deterministic, to indicate resource
exhaustion, and the depth of calls an engine allows is an implementation limit. This
profile takes the deterministic profile's rule for NaNs (§4.5) and closes the others: no
vector instruction is taken, the table never grows, the memory grows only within the
maximum the module declares (§4.7), and the stack is weighed (§4.3).

The limits of the last rows are each below the limits of the validator and the native
engine the reference uses, and stay below them once a module is prepared: a test makes a
module of the most bytes, its largest body all calls, with the most exports, names, table
entries and memory and as many of each other item as fit beside them, and prepares,
compiles and runs it on every engine (`wai-wasmq/tests/engines.rs`).

### 3.3 Refusal codes

| code | the module or envelope |
|---|---|
| `W001` | is not a valid core module in Lime1, for a reason no other code names (a component, a malformed module, a body that does not end, an encoding of another feature) |
| `W002` | imports something |
| `W003` | has more than one memory, a 64-bit one, one with a page size of its own, one without a maximum or past 4096 pages; or (envelope) has modules with more than 4096 pages among them |
| `W004` | has a start function |
| `W005` | has a shared memory, global, table or type, or an atomic instruction |
| `W006` | has a vector instruction or type, relaxed or not |
| `W007` | has an instruction or a type of a feature outside Lime1 that no other code names |
| `W008` | has more than one table, one not of `funcref`, past 2^16 entries, or an instruction that reads or changes it other than `call_indirect` |
| `W009` | has a function whose parameters, locals and operands can pass 4096 |
| `W010` | is past a size the last rows of §3.2 give; or (envelope) has modules of more than 512 KiB among them |
| `W011` | has a data or element segment that does not fit where it is placed |
| `W012` | exports a name the profile reserves, or an export a host calls with another type than its own |
| `W013` | (envelope) is not one this profile writes, or is past its size (§2.3) |
| `W014` | (envelope) has a frame whose digest is not the one its contract pins |
| `W015` | (envelope) has callouts that are not one for each `extern` in order, a module no callout names, an export of another type than its `extern` lowers to, or a module the host cannot reach as §5.2 asks |
| `W016` | (envelope) has a program longer than 1 MiB, that the reader refuses, that calls nothing, with a gate outside §5.1's, or past a bound it is read within (§4.8) |
| `W017` | (envelope) has a run outside the profile's ranges, or past what §4.8 lets a run ask of its host |

A module or an envelope that breaks more than one rule is refused with the code of one
of them. Each refusal vector (§9) breaks exactly one.
`wai-quantum check-wasmq MODULE.wasm` holds a module to the profile and names the code.

## 4. Running a module the same everywhere

### 4.1 Instances

An instance is made from the module with no imports. Its memory starts at its initial
size, zeroed, with the active data segments copied in; its table holds the active element
segments; its globals hold their initial values. A host MUST be able to hold the memory's
maximum before it calls the instance (§4.7).

### 4.2 Fuel

Every call a host makes into an instance has a limit of fuel. Fuel is defined on the
module as written, not on any engine:

- A function's body is a sequence of **runs**. A run starts at the function's first
  instruction and right after each `block`, `loop`, `if`, `else`, `end`, `br`, `br_if`,
  `br_table`, `return`, `call`, `call_indirect` and `unreachable`; it ends with the first
  of them that follows, or with the body.
- The **weight** of an instruction is 0 for `nop`, `drop`, `block`, `loop`,
  `unreachable`, `return`, `else` and `end`, and 1 for every other. Entering a function
  weighs 1.
- When execution reaches the start of a run, the run's weight (with 1 more for the first
  run of a body) is charged. Before `memory.copy` and `memory.fill` execute, the byte
  count they take is charged; before `memory.grow` executes, 1024 for each page it asks
  for is charged, whether or not the growth succeeds: zeroing a page costs a host what
  1024 instructions do.
- When a charge takes the fuel below zero, the call stops with `fuel_exhausted`.

So a charge happens at the start of a run, before any of the run's instructions, and a
call that traps in the middle of a run has been charged the whole run. On every path that
does not stop early, the fuel a call uses is the number of instructions it executed under
these weights, and one for each function it entered.

**Limits.** The contract gives three budgets. A callout's limit is `per_call`, and it
covers every call the host makes for it (§5.2). The limit of an instance's lifecycle
calls is `per_instance`, for each of them (§5.3). `per_job` is the run's: when less than
a call's limit is left of it, what is left is the call's limit. The fuel a call used is
its limit less what it left, and is taken from what is left of the run's; a call that
stops with `fuel_exhausted` used its whole limit.

The weights are the default operator costs of the native engine the reference uses, with
one for a byte of `memory.copy` or `memory.fill` and 1024 for a page of `memory.grow`. A
test holds the profile's fuel equal to that engine's own count, on the module as written,
over control flow, calls and memory instructions, with one difference it states: for
`memory.grow` the profile charges 1024 for each page asked for, and that engine's own
meter one for each page it gets (`wai-wasmq/tests/engines.rs`).

Fuel is a count of work, the same on every host. It is not a time: a host that must
answer within a deadline measures its own instructions per second and sets the budget.

### 4.3 The stack

Calls are bounded by weight, not by count, so that the bound holds for a frame of any
size on any engine. The **weight of a function's frame** is

```text
576 + its parameters + its results + its locals + its operands + the bytes of its entry in the code section
```

its parameters and results those of its type, its locals the ones it declares, its
operands the most values its body holds on the operand stack at once (as a validator
counts them after each instruction: a call's results among them), and its entry's bytes
the value of the entry's own size field. The **stack's weight** is zero
when a host calls an export. Before a `call` or `call_indirect` executes, the weight of
the function that holds the instruction is added to it; when the callee returns, the
same weight is taken off. A call that would take the stack's weight past **8 388 608**
(2^23) stops with `stack_exhausted`, before the instruction does anything else: a
`call_indirect` that is both past the stack and through an entry it cannot call stops
for the stack.

So the frames suspended at calls never weigh more than 2^23 together, and one more
frame runs on top of them. An interpreter that keeps a frame's parameters, locals and
operands in slots needs at most one slot for each unit. The reference's native engine
needs at most eight bytes for each unit: a test runs modules made to keep as much in a
frame as the largest body allows (locals held across a call, a new value held at every
step, the results of calls held on the operand stack across a call, the largest function
types), each recursing to the limit, on a stack of exactly that size, and shows a smaller
one fails (`wai-wasmq/tests/engines.rs`). It gives each call nearly twice that.

A function of a few instructions recurses some 14 000 deep; a function at the largest
body the profile takes, some 490.

### 4.4 The prepared module

A host MAY run a module with an engine that implements §4.2, §4.3 and §4.5 itself (the
reference interpreter does). The reference's native engine does not, so it runs the
**prepared module**: the module with every instruction kept byte for byte, and added

1. two mutable globals, after the module's own, exported as `__wasmq_fuel` (i64) and
   `__wasmq_stack` (i32);
2. at the start of each run whose weight is not zero, the charge
   `global.get F; i64.const w; i64.sub; global.set F; global.get F; i64.const 0; i64.lt_s; if; unreachable; end`;
3. before `memory.copy` and `memory.fill`, the same charge of the byte count, and before
   `memory.grow`, of 1024 times the page count, each taken from the operand with
   `local.tee` of one added `i32` local;
4. around each `call` and `call_indirect`, with `w` the weight of the function they are
   in, `global.get S; i32.const w; i32.add; global.set S; global.get S; i32.const 8388608; i32.gt_u; if; unreachable; end`
   before it and `global.get S; i32.const w; i32.sub; global.set S` after it;
5. after each instruction of §4.5, a call of an added function that returns its argument,
   or the canonical NaN if the argument is a NaN;

with every custom section dropped. The host sets `__wasmq_fuel` to the call's limit and
`__wasmq_stack` to 0 before each call. When the prepared module traps at `unreachable`
with `__wasmq_fuel` below zero, the fault is `fuel_exhausted`; with `__wasmq_stack` past
2^23, `stack_exhausted`; otherwise the module's own `unreachable`.

The prepared module is one way to hold §4.2, §4.3 and §4.5, and its bytes are the
reference's own: this text does not fix them, and no receipt names them. What a
conforming runner must reproduce is what those sections define.

### 4.5 NaNs

The result of `f32` and `f64` `add`, `sub`, `mul`, `div`, `min`, `max`, `sqrt`, `ceil`,
`floor`, `trunc` and `nearest`, of `f32.demote_f64` and of `f64.promote_f32` is, when it
is a NaN, the canonical positive NaN (`0x7fc00000`, `0x7ff8000000000000`): WebAssembly
3.0's deterministic profile. Every other instruction already has one result everywhere.
A test shows that a module whose result depends on a NaN's bits reads what the host chose
when neither the preparation nor the engine canonicalises, and the canonical NaN when
either does (`wai-wasmq/tests/adversarial.rs`).

### 4.6 Engines

The reference runs every module on two engines and holds them to the same bytes:

- **native**: the repository's one pinned release of wasmtime, compiling the prepared
  module with Cranelift, with NaN canonicalisation on, relaxed vector instructions fixed
  and refused, vector instructions, tail calls and every proposal past Lime1 off, its
  own fuel on as a backstop under the profile's, and a run's calls made on one thread with
  a stack of the size §4.3 bounds;
- **interpreter**: `wai-wasmq`'s own, which runs the module as written and implements
  §4.2, §4.3 and §4.5 itself, and which also runs on wasm32 (where the native engine
  does not run). It also runs the prepared module, with its own metering off, as a check
  of the preparation on the vectors; that use is held to none of §4.8's bounds.

`wai-quantum run ENVELOPE.wai --engine native|interpreter` chooses; the receipt is the
same.

### 4.7 Memory

`memory.grow` past the module's declared maximum returns −1, on every engine. Within the
maximum, it succeeds: a host that cannot grow the memory within the maximum (it has run
out of memory) MUST stop the run and seal nothing (§6.3), because what it would seal
would be its own condition, not the module's.

The modules of a bundle hold at most 4096 pages among them, by the maxima they declare
(`W003`), so that a 32-bit host holds any bundle's memory: a limit for each module alone
would leave the number of modules to decide which hosts can run an envelope.

### 4.8 What a run asks of its host

Fuel is the work of the modules. A run also asks work and memory of its host that no
fuel counts: reading the program, its steps on the tableau, a fresh instance's memory,
compiling its modules, the result. So that an envelope that opens on one host opens and
finishes on every host, a 32-bit one among them, a reader bounds all of it from the
bundle alone, before anything runs, and refuses past the bounds; nothing here differs by
engine. A receipt shows part of what these bounds count, and §6.5 holds a job to that part
(rules 29 to 32).

**Reading.** The program is read within these bounds, each checked as it is read, so that
a short program cannot make a reader hold or do more than a host has before it is refused
(`W016`):

| bound | |
|---|---|
| its text | 1 MiB (a reader holds some eighty bytes of tokens for each) |
| nesting | 64 levels in the text and 256 in all through the bodies calls read (`Q006`): a reader's stack. A statement, each statement that holds it, and each level of its expressions' trees (parentheses, operators, brackets, calls, casts and types) count one; a run of operators of one precedence and an `else if` chain each count one, at any length; an array has at most 7 dimensions |
| qubits | 32 768 |
| bits: the program's and its blocks' own together, any one value's, and those of any one array, its elements times each element's | 2^20 |
| steps, its loops unrolled | 2^21 |
| the bits its calls take and give, summed over its steps | 2^23 |
| the work of reading: one for each statement and loop iteration, for each value worked out one and one more for each bit or element it makes, and one for each bit declared | 2^26 |

Past one, the reader's code is `Q323`, or `Q111` for the qubits. **A run ends**: the
reader unrolls every loop, a `while` included, to the bounds it reads or is told
(`@wai.max_iterations`), so every jump in a program's steps goes forward.

**Memory.** A run's shots times the bits a shot holds (all the program's bits, its blocks'
own among them, though an outcome shows only the program's, §6.1) are at most 2^28
(`W017`). With the most memory (§4.7), the largest
envelope (§2.3), the most code (§3.2), the most qubits, bits and steps and the bits of
calls, these leave a run within a 32-bit host's address space at every limit at once,
which a test holds the reference to under wasm32 (`wai-wasmq/tests/sweep.rs`).

**Work.** A run's work is at most 2^42 operations on a word (`W017`), where, with `n` the
program's qubits and `r` = ⌈`n`/32⌉ (at least 1) the words of a tableau's run for one
qubit:

| for each shot | operations |
|---|---|
| its fresh tableau | 2·`n`·`r` |
| each gate | `r` |
| each measurement or reset | 2·`n`·`r` |
| each callout | 4096 for each call of the module's (its export, `cabi_realloc` for each list argument, and `cabi_post_<export>` after a list result), 4 for each bit it takes and gives, and 1 |
| each other step | 1 |

| for each instance, one for each shot, or one for the run when `state` is `job` | operations |
|---|---|
| each module, and each call of `wasmq-seed`, `init`, and two for each prior | 4096 |
| each byte of each module | 1 |
| each page of the memory a module starts with | 8192 |

| for the run | operations |
|---|---|
| each byte of each module, compiled | 131 072 |
| each unit of the most fuel it may be given, `per_job` | 8 |

A random measurement rewrites the tableau's rows that hold an X at its qubit; a determined
one's outcome is the sign of the product of up to `n` stabilizers, which the reference
finds a machine word of rows at a time without copying the tableau. Either reads the
tableau about once, which is the `n`·`r` of its weight. A page a module grows is paid for in fuel (§4.2), as
a page it starts with is counted here. This is a bound on a host's effort from the bundle
alone, not a measure of it: fuel is the profile's measure of the modules' work (§4.2).
The reference was measured at a 64th of the limit, each kind of work alone, on x86_64
Linux natively and under wasm32: at the limit it would take at most about three hours.

## 5. Callouts

### 5.1 In the program

A program declares each function it calls with `extern`, its arguments and its result
written as types:

```qasm
extern decode64(bit[4]) -> bit[9];
bit[4] s;
bit[9] corr;
s = measure a;
corr = decode64(s);
if (corr[0]) x d[0];
```

An argument is `bit[n]`, `uint[k]` or `int[k]` (k from 1 to 64); the result is `bit[n]`
or nothing. An argument is a bit register or an integer known on reading (a constant, a
loop's variable, an `input`); the result goes into a bit register, in a declaration or
an assignment, and a later condition reads it. Calls inside `for` loops unroll; calls
under `if` run only on the shots that take the branch.

**The gates.** This version runs the Clifford gates that take no angle: `id`, `x`, `y`,
`z`, `h`, `s`, `sdg`, `sx`, `sxdg`, `cx`, `cy`, `cz` and `swap`, and gates a program
defines from them, with measurement, reset and conditions on bits, on at most 32 768
qubits. A program with any other gate is refused (`W016`), whatever its angle: `rz(pi/2)`
acts as `s`, and is refused all the same, so that no reader decides in floating point
which gate a program holds. With these gates a state is a stabilizer tableau and every
step of a run is whole-number arithmetic (§6.1).

OpenQASM 3 schedules an `extern` call and lets it run concurrently with other
operations. This profile fixes one schedule: a call runs when the program reaches it, in
program order, and completes before the next statement; it is atomic. A program read
with any other reader of this repository keeps refusing an `extern` call (`Q125`).

### 5.2 Lowering

A callout has one of two forms, by its widths, as [`quantum-wasmq.wit`](quantum-wasmq.wit)
declares them:

- **scalar**, when every argument and the result have at most 64 bits: each lowers to one
  `i64` (WIT `u64`), bit `i` of the register bit `i` of the integer, an `int[k]`
  sign-extended. The export's type is `(i64, …) -> (i64)`, or `-> ()` with no result.
- **list**, otherwise: each `bit[n]` argument lowers to a `list<u8>` (an `i32` pointer and
  an `i32` length) and the result to one `i32` that points to a pointer and a length;
  `uint[k]` and `int[k]` arguments stay `i64`. The list's bytes are `ceil(n/8)` long, bit
  `i` in byte `i/8` at bit `i % 8`, the rest of the last byte zero: the Component Model's
  canonical ABI.

A host reaches a module's memory only as its export named `memory`. A module with a
list-form callout exports it, and `cabi_realloc` when the callout has a list argument
(`W015`). The exports a host calls have exactly these types (`W012`):

| export | type |
|---|---|
| `cabi_realloc` | `(i32, i32, i32, i32) -> (i32)` |
| `cabi_post_<export>` | `(i32) -> ()` |
| `wasmq-seed` | `(i64) -> ()` |
| `wasmq-prior` | `(i32, i32, i32) -> ()` |
| `init` | `() -> ()` |

A host makes a callout in these steps, each guest call under the callout's one limit,
its stack's weight starting at zero:

1. For each list argument, in order: it calls `cabi_realloc(0, 0, 1, len)`, charges
   `len` fuel, and writes the bytes at the address returned.
2. It calls the export.
3. For a scalar result: a bit set at or above the result's width ends the run.
4. For a list result at address `r`: `r` is a multiple of 4; it reads a pointer and a
   length at `r`; the length is `ceil(n/8)`; it charges that many fuel and reads the
   bytes; no bit past the width is set in the last byte; then it calls
   `cabi_post_<export>(r)` if the module exports it.

A step that cannot be done as written (bytes that do not fit in the memory at an
address, an address not a multiple of 4, another length, a bit past the width) ends the
run with `bad_result`, with the fuel used up to that step.

### 5.3 Lifecycle

Instances are made at the start of a shot, before its first step, one for each module in
the contract's order (each shot when `state` is `shot`, once at the first shot when it is
`job`); a fault in making one ends the run there, and no later module's is made. When an
instance is made, the host calls, in this order and each if the module exports it, each
under the limit `per_instance`:

1. `wasmq-seed(seed: u64)`, with the run's seed, or, when `state` is `shot`, the shot's
   seed (§6.1);
2. `wasmq-prior(index: u32, bytes: list<u8>)` for each of the module's priors, in the
   contract's order, the bytes passed as a list argument is (§5.2, step 1);
3. `init()`.

A module with priors exports `wasmq-prior`, `cabi_realloc` and its memory (`W015`).

### 5.4 Priors

A prior is a parameter file a module reads: a code's parity checks, a target register, a
noise model, a calibration. It travels in the envelope and is pinned in the contract, so
a module is never run against another prior than the one it was packed with (`W014`).

## 6. A run and its receipt

### 6.1 Shots and outcomes

A run goes shot by shot, in order. Each shot starts from `|0…0⟩` with every bit 0, and
has a **stream**: the outputs of SplitMix64 from the state `s XOR 0x51574d31`, where `s`,
the shot's seed, is SplitMix64's output for the state
`seed + (shot + 1) · 0x9e3779b97f4a7c15` (all sums modulo 2^64).

A measurement of a qubit in the computational basis has an outcome that is determined by
the state, or is 0 or 1 with equal chance; with §5.1's gates there is no other case. A
determined outcome is the outcome, and takes nothing from the stream. A random outcome
takes the stream's next value `x`, and is 1 when `x < 2^63`. A `reset` measures its qubit
the same way, without writing a bit, and applies `x` to it when the outcome is 1; a
reset of a qubit whose outcome is determined takes nothing from the stream.

A shot's outcome is its program's bits, `n` of them: every bit it declares at its top
level, whether or not anything writes it, numbered in the order the program declares them
(its first declared bit is bit 0, a register's bits in their order) and written bit
`n − 1` first; the counts sum the shots that read each outcome. A bit that a block or a
subroutine declares is its own (`Q322`): the steps read and write it, and no outcome holds
it. Each measurement names the bit it writes: a `measure` with no target bit is refused
in a program that calls externs (`Q324`), since its outcome is the bits it declares. A
program that measures nothing has its bits as its outcome all the same, those its calls
write and 0 for each bit nothing writes: no qubit is read for it.

### 6.2 Faults

A run stops at the first fault, seals what it ran, and reports:

| reason | |
|---|---|
| `fuel_exhausted` | a charge took the fuel below zero (§4.2); `budget` says whose limit it was: `call`, `instance`, or `run` when the limit was what was left of the run's |
| `stack_exhausted` | §4.3 |
| `unreachable`, `memory_out_of_bounds`, `table_out_of_bounds`, `indirect_call_null`, `indirect_call_type`, `integer_divide_by_zero`, `integer_overflow`, `invalid_conversion_to_integer` | the module trapped (WebAssembly 3.0, §4 Execution) |
| `bad_result` | §5.2 |

A fault has the members `reason`, `shot`, `phase` (`seed`, `prior`, `init` or `call`),
`module` (its name), `fuel` (what the stopped call used), `callout` (the `extern`'s
name) when the phase is `call`, and `budget` when the reason is `fuel_exhausted`, and no
other. The counts are of the shots that finished. A fault receipt is a receipt like any
other: it verifies, and running the envelope again reproduces it.

### 6.3 What is never sealed

A host that could not run the bundle seals nothing: a refused envelope (§2.3, §3.3), a
host that cannot hold the memory's maximum or grow within it (§4.7), an engine that
fails for its own reasons. These are the host's condition, not the bundle's, and a
receipt that recorded them would differ by host. Nothing a bundle holds can lead here:
what a bundle could cause is refused on reading (§2.3, §4.7, §4.8) or sealed as a fault.

### 6.4 The result

The job body is the engine's (`engine::job`), with exactly four members:
`{ "status", "method", "request", "result" }`. The request is
`{ "wasmq": <the contract>, "envelope_blake3" }`. `status` is `done` when the result's
`status` is `ok` and `fault` otherwise; `method` is the result's. The receipt signs the
request and the result, as [the provider protocol's §8.2](quantum-providers.md#82-how-it-is-sealed-and-how-a-job-is-read)
seals every job; `status` and `method` only repeat what is signed. They are the host's
word, unsealed: a verdict takes nothing from them, and a check notes where they, or any
other member of the body, differ from what is sealed (§6.5).

The result has exactly these members:

| member | |
|---|---|
| `format` | `"wai.quantum.wasmq.result/1"` |
| `profile` | `"wai.quantum.wasmq/1"` |
| `status` | `ok`, or `fault` when the run stopped |
| `method`, `qubits`, `shots`, `seed` | the contract's method, the program's qubits (§2.2), the contract's shots and seed |
| `shots_run` | the shots that finished |
| `counts` | outcome to shots (§6.1) |
| `callouts` | the callouts made, one that stopped the run among them |
| `fuel` | `{ "used", "instances", "budget": { "per_call", "per_job", "per_instance" }, "callouts": { name: { "calls", "fuel", "max" } } }`: all the fuel used, the part of it lifecycle calls used, the contract's budgets, and for each `extern` the run called, its calls, their fuel and the most one of them used (an `extern` it did not call has no entry) |
| `modules` | for each, in the contract's order: `{ "name", "blake3" }` |
| `transcript_blake3` | BLAKE3 over `wai:wasmq-transcript\x01` and, for each callout that returned, in order: its shot (u64), the index of its `extern` (u32), its input's length (u32) and bytes, its output's length (u32) and bytes, and its fuel (u64), little-endian, the input the arguments' bits in order and the output the result's, packed as a list's bytes are (§5.2); after a fault, the bytes `fault`, the shot (u64), the reason's bytes and the fault's fuel (u64) |
| `fault` | §6.2, when the run stopped |
| `accuracy` | `{ "class": "exact" }` |
| `energy` | `{ "unmetered": "the runner reads no energy meter; fuel is the profile's measure of work" }` |
| `receipt` | the engine's job receipt (`engine::receipt`): Ed25519 over BLAKE3 of the request and the result in RFC 8785 form |

**Result-equivalence.** Every conforming runner, on every host and every engine, gives
an envelope the same result: the same bytes in its RFC 8785 form, the receipt aside. So
the receipt's digest is the same everywhere, and under one key the whole job is.

### 6.5 Verifying

A wasmQ job is a job like any other: every verifier of the engine's job receipts reads it
and judges it by [the provider protocol's §8.4](quantum-providers.md#84-what-a-verifier-checks),
and so gives it one verdict, wherever it is checked. `wai-quantum verify` (and its
`--json` and `--lines`), the job service's `POST /v1/verify`, both MCP servers given the
job's text, the Python package, the desktop app and a page read the job from its text as
§8.2 reads every job's, so its seal and its numbers are held as every receipt's are. A
surface given the job already parsed (a view, an MCP server given its members) cannot see
what parsing loses, as the provider protocol's §9 says, and gives every other reason; the
Python package judges a dict as the text it writes for it. A result
whose `format` is `wai.quantum.wasmq.result/1` is a wasmQ job's, and §8.4 adds one reason
for it, `wasmq_form`: the job breaks a rule below. Only what is sealed (the request, and
the result less its receipt) and the form of its seal decide it. A signature shows that a key sealed a job and says
nothing of what the job holds, so without the envelope to run again these rules are what
hold a result to its contract and to itself: a key can seal any result of this form, and
only running the envelope again shows that a result is the one it gives.

In these rules a number's value is the double it reads as (§8.2). A *count* is a number
whose value is a whole number from 0 to 2^53 − 1, however it is written (`1`, `1.0` and
`1e0` are one count, sealed as one); "at most" and "equals" compare counts, and a rule on
a count fails when the number is not one. A *digest* is a string of 64 lowercase
hexadecimal digits. Two values are *equal* as JSON values are, numbers by their value and
an object's members in any order. "Exactly the members" means every one named and no
other; a value that is not an object has none. A member is *present* when its object names
it, whatever its value, `null` among them: "has no `fault`" and "has a `callout`" read
so. A list or a map named below that is not an
array or an object is read as an empty one, after its own rule has failed. `C` is the
request's `wasmq` (the contract), `run` is `C`'s `run`, `r` is the result and `F` is
`r`'s `fuel`. *The budget* `per_call`, `per_job` or `per_instance` is that member of `run`'s
`fuel`. The job breaks the form when any of these fails:

1. No number in the request, or in the result less its receipt, has a magnitude past
   2^53 − 1.
2. The request has exactly the members `wasmq` and `envelope_blake3`, and
   `envelope_blake3` is a digest.
3. `C` has exactly the members §2.2 gives: `profile`, `program`, `modules`, `callouts`
   and `run`; its `program` exactly `blake3`, `bytes` and `inputs`; `run` exactly
   `shots`, `seed`, `method`, `state` and `fuel`; and `run`'s `fuel` exactly `per_call`,
   `per_job` and `per_instance`.
4. `C`'s `profile` is `wai.quantum.wasmq/1`.
5. The program's `blake3` is a digest; its `bytes` a count from 1 to 2^20; its `inputs` an
   object each of whose values is a number whose value is whole and at most 2^53 − 1 in
   size.
6. `C`'s `modules` is an array that is not empty. Each module has exactly the members
   `name`, `blake3`, `bytes` and `priors`: `name` a string, `blake3` a digest, `bytes` a
   count of at least 1, and `priors` an array each of whose priors has exactly the members
   `name` (a string), `blake3` (a digest) and `bytes` (a count). The modules' `bytes` that
   are counts add up to at most 2^19, so each is at most that; rule 31 bounds a prior's.
7. `C`'s `callouts` is an array that is not empty. Each callout has exactly the members
   `extern`, `module` and `export`: `extern` and `export` strings, and `module` a count
   less than the number of modules. No two callouts have the same `extern`, and each
   module's index is the `module` of a callout.
8. `run`'s `shots` is a count from 1 to 2^20, its `seed` a count, its `method`
   `stabilizer`, its `state` `shot` or `job`, and each of its fuel's three budgets a count,
   `per_call` and `per_instance` each of at most 2^39 (§4.8; rule 30 holds `per_job` to
   less).
9. `r` has exactly the members of §6.4 (`format`, `profile`, `status`, `method`,
   `qubits`, `shots`, `shots_run`, `seed`, `counts`, `callouts`, `fuel`, `modules`,
   `transcript_blake3`, `accuracy`, `energy` and `receipt`), and may have `fault`.
10. The receipt is an object whose `canon` is `rfc8785`: the first form (§8.2) is older than
    this profile, and no host sealed a wasmQ job in it.
11. `r`'s `format` is `wai.quantum.wasmq.result/1`, its `profile` `wai.quantum.wasmq/1`,
    its `accuracy` `{ "class": "exact" }` and its `energy` the one §6.4 gives; and its
    `method`, `shots` and `seed` equal `run`'s.
12. `r`'s `qubits` is a count from 1 to 2^15 (a program declares a qubit at least, `Q100`),
    and its `transcript_blake3` a digest.
13. `F` has exactly the members `used`, `instances`, `budget` and `callouts`; its `budget`
    equals `run`'s `fuel`; and `used` is a count of at most the budget `per_job` (0 when
    that is not a count).
14. `F`'s `callouts` is an object. Each of its members is named by the `extern` of one of
    `C`'s callouts, and has exactly the members `calls`, `fuel` and `max`: `calls` a count
    of at least 1; `max` a count of at most the budget `per_call` (0 when that is not a
    count) and at most its own `fuel`; and `fuel` a count (rule 20 bounds it by its calls
    and their `max`).
15. `F`'s `instances` and the `fuel` of each member of `F`'s `callouts`, added, are `F`'s
    `used`; and the `calls` of each member, added, are `r`'s `callouts`. Each of them is a
    count.
16. `r`'s `modules` has as many entries as `C`'s, each with exactly the members `name`
    and `blake3`, its `blake3` a digest, and its `name` and `blake3` equal to those of
    `C`'s module at its index.
17. `F`'s `instances` is a count of at most M × S × the budget `per_instance` (0 when that
    is not a count): S is the sum, over `C`'s modules, of 2 and the number of its priors
    (each instance's seed, its init and each prior, §4.2, §5.3); M, the instances made, is 1
    when `run`'s `state` is `job`, whatever the status; for any other `state` it is `r`'s
    `shots_run` (0 when it is not a count), plus 1 when `r`'s `status` is `fault`.
18. When `r`'s `status` is `ok`: `r` has no `fault`, and its `shots_run` equals its
    `shots`. When it is `fault`: the fault has exactly the members `reason`, `shot`,
    `phase`, `module` and `fuel`, and may have `callout` and `budget`; `reason` is one §6.2
    names; `shots_run` is less than `shots`; `shot` equals `shots_run`; `phase` is `seed`,
    `prior`, `init` or `call`; `module` equals the `name` of one of `C`'s modules; `fuel`
    is a count, and in a phase other than `call` at most the budget `per_instance` (0 when
    that is not a count: a call's is held by its callout's `max`, below, and rule 14; rules
    20 and 25, with rule 15, hold either within `F`'s `used`); it has a
    `callout` exactly when its phase is `call`, and that is the `extern` of one of `C`'s
    callouts that names a member of `F`'s `callouts` whose `max` is at least the fault's
    `fuel` (the call that stopped is one of the calls made, §6.4); and it has
    a `budget` exactly when its reason is `fuel_exhausted`, and that is `run`, or `call` in
    a call and `instance` otherwise. Any other `status` breaks the form.
19. `r`'s `counts` is an object; each of its names holds only `0` and `1` (the empty name
    among them), all of one length; each of its values is a count of at least 1; and its values, added, are `r`'s
    `shots_run`.

Rules 20 to 35 tie members to each other, as the writer does. In them *the fault* is `r`'s
`fault` when `r`'s `status` is `fault` and that is an object, and there is none
otherwise; a rule about the fault holds when there is none. A *call's fault* is a fault
whose `phase` is `call`, and a *lifecycle fault* one that has a `phase` other than `call`.

20. For each member of `F`'s `callouts`, let `s` be 1 when the fault is a call's fault
    whose `callout` is that member's name, and 0 otherwise, and `e` the fault's `fuel` when
    `s` is 1 (0 when that is not a count) and 0 otherwise. `T`, its `fuel` less `e`, the fuel
    of its calls that returned, is not less than 0, and is from `k` to `k` × `max`, where `k`
    is its `calls` less `s` (0 when that is less than 0): the call that stopped used the
    fault's fuel, and each call that returned used at least 1 (§4.2: entering a function
    weighs 1) and at most the most one call used. When `max` is more than `e`, the most was a
    call's that returned, and each of the others used at least 1, so `T` is also at least
    `max` + `k` − 1. `calls`, `fuel` and `max` are counts.
21. `F`'s `instances` is a count of at least `W` × `P` + `E`, the least that making the
    instances took outside a stopped call (§5.3: a shot's instances are made module by
    module in `C`'s order, each one's `wasmq-seed`, then its priors, then its `init`; passing
    a prior calls `cabi_realloc`, at least 2 since it returns a value, then charges the
    prior's bytes, then calls `wasmq-prior`, at least 1, §4.2, §5.2):
    - `P`, what each set of instances took at least: the sum, over every prior of every one
      of `C`'s modules, of 3 and the prior's `bytes` (0 when that is not a count), and 1
      more when the fault is a lifecycle fault in phase `seed` or `init`: its module exports
      that function, and each set called it;
    - `W`, the sets made whole: `r`'s `shots_run` (0 when that is not a count), plus 1 when
      there is a call's fault; when `run`'s `state` is `job` it is that or 1, whichever is
      less;
    - `E`, when the fault is a lifecycle fault, what the set it stopped took at least: the
      same sum, of 3 and its `bytes`, over the priors of each module before the one the fault
      names (the first of `C`'s modules with that `name`), and, when its phase is `init`, over
      that module's own; 0 otherwise, and when no module has that `name`.
22. A call's fault's `module` equals the `name` of `C`'s module whose index is the
    `module` of each of `C`'s callouts whose `extern` is the fault's `callout` (rule 7
    allows one): a call runs in its callout's module (§2.2, §6.2). It fails when there is
    no such callout, or no such module.
23. A fault whose `phase` is `prior` has as its `module` the `name` of one of `C`'s
    modules whose `priors` is not empty: a prior is passed only to a module that has one
    (§5.3).
24. A fault whose `reason` is `bad_result` has the `phase` `call` or `prior`: only these
    pass bytes or take a result (§5.2).
25. A lifecycle fault's `fuel` is a count, and `F`'s `instances` (a count) is at least it
    added to rule 21's `W` × `P` + `E`: what the stopped lifecycle call used is part of the
    instances' fuel, beside what the calls before it took.
26. When `run`'s `state` is `job`, a lifecycle fault's `shot` is the count 0: the run's
    one instance of each module is made at the first shot (§5.3).
27. A lifecycle fault whose `shot` is the count 0 comes with `r`'s `callouts` the count 0:
    the first shot's instances are made before its first step (§5.3). (Rule 32 holds this
    too, so rule 27 is never broken alone.)
28. A fault whose `reason` is `fuel_exhausted` used its whole limit (§4.2). When its
    `budget` is `call`, its `fuel` is a count equal to the budget `per_call`; when it is
    `instance`, to the budget `per_instance` (each 0 when it is not a count). When it is
    `run`, `F`'s `used` is a count equal to the budget `per_job` (a count), and the fault's
    `fuel` is a count, less than its own limit: the budget `per_call` in a call's fault, and
    the budget `per_instance` in a lifecycle fault, each read as 0 when it is not a count (a
    fault with no `phase` has no limit here, and breaks rule 18): the run's budget was the
    limit only because less of it was left than the call's own.
29. When `r`'s `counts` has a name, the length of the longest, in characters (Unicode code
    points), is at most 2^20, and `run`'s `shots` (0 when that is not a count) times that
    length at most 2^28: a program holds at most 2^20 bits, and a run's shots times them are
    at most 2^28 (§4.8). (Rule 19 holds each name to `0` and `1`, one byte each; a verifier
    counts a name that breaks it in characters too.)
30. The part of a run's work that a receipt shows is at most 2^42 (§4.8):
    `S` × 2·`n`·`w` + `I` × Σ (4096 × (1 + 2 × `p`) + `b`) + 131072 × Σ `b` + 4097 × `K` + 8 ×
    the budget `per_job`. `S` is `run`'s `shots`; `n` is `r`'s `qubits`; `w` is ⌈`n`/32⌉, or
    1 when that is 0; `I` is 1 when `run`'s `state` is `job` and `S` otherwise; each sum is
    over `C`'s modules, `p` a module's number of priors and `b` its `bytes`; and `K` is `r`'s
    `callouts`. Every number here that is not a count is read as 0. The host's work is at
    least this: each shot's fresh tableau, each instance's module and its calls of
    `wasmq-prior` and of `cabi_realloc` for it, the run's compiling, each call made (its
    module's part, 4096, and its step, 1: a callout's step is counted in each shot whether or
    not it runs) and the run's fuel.
31. The envelope the contract names is at most 2^27 bytes (§2.3): 20 bytes of magic and
    lengths, its manifest (§2.1's members, in that order and with no space: 192 bytes and the
    decimal digits of its `qubits`, `r`'s, and its `shots` and `seed`, `run`'s, each read as 0
    when it is not a count), `C` in RFC 8785 form (§2.2; no bytes when the request has no
    `wasmq`), and its frames (the program's `bytes`, each module's `bytes` and each prior's
    `bytes`, each 0 when it is not a count), added, are at most 2^27.
32. `r`'s `callouts` is at most 2^21 × `H` (each 0 when it is not a count), where `H`, the
    shots that ran steps, is `r`'s `shots_run` and 1 more when there is a call's fault: a
    shot runs each of its steps at most once, every jump going forward, and a program has
    at most 2^21 steps (§4.8), each call one of them.
33. Each prior passed whole fits within one lifecycle call's limit: 3 and its `bytes` (0 when
    that is not a count) are at most the budget `per_instance` (0 when that is not a count),
    for every prior of every one of `C`'s modules when `W` (rule 21) is at least 1, and for
    each prior `E` counts otherwise. Passing a prior is one stretch under one limit:
    `cabi_realloc`, its bytes and `wasmq-prior` (§5.2, §5.3).
34. A fault's `fuel`, when it is a count, is at least what its `reason` shows was charged
    (§4.2), when it has one: 1 for every reason but `fuel_exhausted`, one §6.2 does not name
    or `null` among them (a call stops any other way only after its entry was charged); 2
    for `bad_result` (a value came back: the entry, and an instruction that made it); and 788
    for `stack_exhausted`. A frame weighs at most
    576 + 4096 + 2^8 + 2^14 = 21 312 (§3.2, §4.3), so the stack's weight passes 2^23 only at
    a call in the 394th frame entered or deeper, and each frame entered was charged at least
    2: its entry, and the run that holds its call.
35. When no call returned, the transcript is what §6.4 gives such a run: when `r`'s
    `callouts` is 0, or 1 and the fault is a call's fault (each a count), `r`'s
    `transcript_blake3` is BLAKE3 over the bytes `wai:wasmq-transcript` and the byte 0x01
    and, when there
    is a fault, the bytes `fault`, the fault's `shot` (u64), its `reason`'s UTF-8 bytes and
    its `fuel` (u64), little-endian (`shot` and `fuel` each 0 when it is not a count, and
    `reason` no bytes when it is not a string).

**What the rules leave free, and why.** What else the writer fixes, the rules leave free,
each for the reason given, and only running the envelope again (`--bundle`) holds a job to
it:

- the `transcript_blake3`'s value once a call returned: it digests each call's input and
  output, which no receipt holds (rule 35 holds it when none returned); and each `blake3`
  against the bytes it pins, which no receipt holds;
- `r`'s `qubits` within rule 12, the outcomes' length within rule 29, and the number of
  callouts within rules 30 and 32, against the program: its text is not sealed, only its
  digest and length, so how many qubits and bits it declares, and how many calls each shot
  makes, are its own;
- which shot read which outcome, and the counts' spread: only the run shows them;
- whether a module exports `wasmq-seed` or `init`, but for the one a fault in that phase
  names (rule 21): only its code shows it. So a fault in phase `seed` or `init` may name any
  module;
- the instances' fuel within rules 17, 21 and 25: what each lifecycle call used past its
  least, and how far the module a fault names got, are its code's;
- the fuel of each call within rules 14, 18, 20, 28 and 34, and a fault's fuel within rules
  18, 20, 21, 25, 28 and 34: where in its work a call traps, and how many bytes its arguments
  pass, are its module's and its program's;
- a trap's `reason` against its phase: any guest call can trap any way, and only
  `bad_result` is the host's (rule 24);
- the rest of §4.8's bounds (the steps of a shot past rule 32's count, the gates and
  measurements, the bits of calls, the pages a module starts with, the program's reading):
  each counts what only the program or the modules hold, so rules 29 to 32 take what a
  receipt shows, and a job a writer can write never breaks them;
- the least length of a program and of a module, and the spelling of an `extern`: a program
  that packs declares an `extern`, a qubit and a call, a module that packs has a type, a
  function, an export and its code, and an `extern` is a name the reader reads, its letters
  any of Unicode's. So each has a least length, and an `extern` a form, that a rule could
  state; but they follow from the grammar, WebAssembly's binary format and Unicode's tables
  rather than from anything a run does, bound nothing a host does, and a rule at them would
  hold every verifier to those tables. Rules 5, 6 and 7 hold the program's and a module's
  `bytes` to at least 1 and an `extern` to a string, and leave the rest free.

Beside §8.4's reasons a verifier of the engine states, for a wasmQ job, `wasmq`:
`outcome`, the sealed result's `status`; `problems`, what breaks each rule the job breaks,
in words, each naming its rule first (`rule 19: ...`), the first 64 of them and then how
many more; and `notes`, where the host's unsealed words
differ from what is sealed or are missing ("the host's unsealed status says `done`; the
sealed result says `fault`"). A note is no part of the verdict: the verdict is the sealed
content's alone, so that every surface that checks a job gives the same one.

`wai-quantum verify JOB.json` prints the receipt's check, the outcome and each problem and
note; `--json` gives the verdict as JSON. `--lines` reads a file of one job a line, each
line on its own as a job's text (a line that is not UTF-8, or blank, is that line's
`unreadable`; the newline that ends the file ends its last line), and gives one verdict a
line, each a job's whatever its kind; a file with no line is refused. A job found
unreadable, no job, with no receipt, or longer than the surface reads (`too_large`) is
reported alone (§8.4), whatever kind of job it says it is: `verify` says that its form was
not judged, and runs no envelope for it. `verify` reads at most 384 MiB and 2^22 values
(§8.4), more than any job holds, in about 1 GiB of memory at most on every host: a file past the
bytes is `too_large` by its size, before it is read, and one past the values once read,
before it is parsed; a file of lines past the bytes is refused, and a line past the values
is that line's `too_large`. With `--bundle ENVELOPE.wai` it also checks
that the envelope is the one the receipt binds (its BLAKE3 is the request's
`envelope_blake3`, and its contract is `C`), and runs it again here: the result must be
the same, byte for byte, the receipt aside; with `--json` the verdict then also says
`bundle` and `reproduced`, and is valid only when both hold. A wasmQ job carries no
history, so `--history` is refused for one.

## 7. On hardware

**The bring-your-own-quantum boundary is unchanged.** WAI Quantum never pays for or
resells hardware time; a person's providers speak `wai.quantum.provider/1`
([quantum-providers](quantum-providers.md)), whose program is a fixed sequence of native
gates measured at the end. A wasmQ bundle calls its modules between gates, which that
protocol does not carry, so `run ENVELOPE.wai --provider NAME` is refused. A wasmQ run
simulates the quantum part on the host that runs it: the person's machine (the command line,
its MCP server, the Python and npm packages, the Studio and the desktop app), or the job
service, which runs an envelope as a job (`POST /v1/wasmq`, the MCP tool `run_wasmq`) within
its own limits, refusing one past them before it runs rather than stopping it part way, and
seals the job with its key; a second-version run's energy there is what the service read of
the worker that ran it (§11.5).

**Nothing here has run a module beside a quantum processor.** This repository has run
wasmQ modules only on the hosts its tests name. What holds for a module on a machine
that runs classical code between gates, and what does not:

- A scalar-form module (§5.2) is a function of integers that imports nothing. Whether a
  given machine takes it is that machine's to say.
- The quantum part's measurements on hardware are not reproducible, so a hardware run
  has no single result to reproduce. Its classical part does: given the inputs each call
  received, a module gives the same outputs and the same fuel on every host, so a
  record of the calls (`run --transcript`) replays through the modules alone and is
  checked call by call (`run ENVELOPE.wai --replay TRANSCRIPT`), each of a shot the run
  has, in the order of its shots. Each call shows only itself; that a record is the whole
  of a run's shows in its digest, which a replay states and the receipt of a run that ended
  `ok` seals as `transcript_blake3`. A machine that ran the module would have to report
  those inputs and outputs for anyone to check them.
- Fuel is not time (§4.2). A real-time deadline is the machine's; the profile states
  the work.

## 8. Reference modules

Two modules of record are built from code the engine already has, for
`wasm32-unknown-unknown` with Lime1 (`wai-wasmq/modules/`, `build.sh`), and committed in
[`../quantum-conformance/wasmq/modules/`](../quantum-conformance/wasmq/modules/) with
the digests of the sources that made them. rustc's wasm32 output depends on the host it
runs on, so they are built on x86_64 Linux, where CI rebuilds them and compares.

### 8.1 The qLDPC decoder

`quantum_qec`'s decoders: union-find matching for a code whose qubits each lie in at most
two checks (the surface code), Relay-BP in fixed-point arithmetic otherwise (the
bivariate-bicycle codes), as the engine itself chooses. Prior 0 is a code's parity
checks in `CssCode::check_matrix_bytes`'s form. Exports: `decode` (list) and `decode64`
(scalar). Tests hold every result to the same functions compiled natively, on every
weight-two error of the distance-3 surface code and on random errors of the [[72,12]]
bivariate-bicycle code (`CssCode::gross()`), and run memory rounds of the distance-3 and
distance-5 surface codes and of that code (a 129-qubit circuit) with the decoder called
between the syndrome and the correction, each shot ending in the code, on every engine
with the same bytes.

### 8.2 The atom rearrangement planner

`quantum_atom::solve`, an exact Hungarian assignment of loaded atoms to target sites.
Prior 0 is the target register in `target_bytes`'s form. Exports: `plan` (list) and
`plan64` (scalar). A circuit loads each trap with probability ½, measures the occupancy,
calls the planner, applies its moves and reads the array: every shot whose plan is
feasible fills the target, and atoms are moved, never made or lost.

## 9. Conformance

[`../quantum-conformance/wasmq/`](../quantum-conformance/wasmq/) holds:

- `envelopes/`: envelopes, each with the result it MUST give on every engine and every
  host (`vectors.json`, `runs`): the status, the fault, the fuel, the transcript's
  digest, the result's digest, the receipt's digest and, under the vectors' key, the
  whole job's digest. Among them are runs that end in every fault reason §6.2 names, in
  every phase and of every budget; callouts of the list form, with a `cabi_post` call and
  with each way a list result is not one; a signed argument; two modules made in order; a
  program that declares no qubit and names physical ones, its bits in two registers; a
  program that measures nothing; one with bits nothing writes, and one whose block holds a
  bit of its own, which pin §6.1's outcome; and a program whose resets and measurements pin
  §6.1's stream;
- `refuse/`: modules and envelopes a runner MUST refuse, each with its code
  (`vectors.json`, `refuse`), at least one for every code of §3.3, each one defect away
  from a module or an envelope that is accepted; the modules also as WebAssembly text
  where they have one. An envelope past §2.3's size has no vector, for its size: a test
  in `wai-wasmq/tests/sweep.rs` makes one;
- `modules/`: the modules of record (§8).

Six wasmQ jobs the command line sealed are among the job receipts of
[`../quantum-conformance/receipts/`](../quantum-conformance/receipts/) (`jobs/cli-wasmq-*`):
a run of the surface-code round, one of a single instance for the whole run, and faults in
a call, of the run's budget, in an instance's init and in a prior. Beside them are jobs
crafted from them, sealed again, each of rules 2 to 31 broken alone by one at least, so the
two verifiers of that corpus, which share no code, are held to each other on `wasmq_form`
and on the rules each states broken, and on every change of one member of each of the six.

`wasmq_vectors verify wai/quantum-conformance/wasmq` checks them on every engine of the
build and prints a digest of what it computed (each run's job and each refusal's code),
the same on every host that conforms.

## 10. Versioning

`wai.quantum.wasmq/1` is this text. A change to anything that moves a result's bytes or
a module's fuel (the weights, the runs, the stack's weights, the lowering, the stream,
the transcript, the result's members) is a new profile version, and a receipt names the
version it was made under.

This version leaves out, and a later one may add under a name of its own (the second
version, §11, adds the first three in part):

- gates that take an angle and gates outside the Clifford group, which need a method
  whose arithmetic this text would have to fix bit for bit. The state-vector method,
  which the engine runs in floating point, is not part of this version for that reason:
  `stabilizer` is its one method (§2.2);
- floating-point arguments and results of a callout;
- noise, and observables other than the counts.

## 11. The second version (`wai.quantum.wasmq/2`)

`wai.quantum.wasmq/2` is this text with the changes of this section; what §11 does not
change holds for it as written. A runner of the second version runs a first-version
envelope (its contract's `profile` `wai.quantum.wasmq/1`) as the first version runs it, and
seals the same result: the vectors of §9 hold under it, byte for byte. The reference is
`wai-wasmq` (`src/exact.rs` beside the files §0 names) and the engine's `engine::wasmq2`.

### 11.1 The envelope and the callouts

The envelope is §2's. The contract's `profile` is `wai.quantum.wasmq/2`, and its `run`'s
`method` is `stabilizer` (the tableau of §5.1 and §6.1) or `exact` (§11.3). A writer that
is given no method writes `stabilizer` when every gate of the program is one of §5.1's, and
`exact` otherwise; a reader refuses a method the program's gates do not fit (`W016`).

A callout's argument may also be `angle[k]`, `k` from 1 to 64: an angle of `m` of `2^k`
parts of a turn, `2πm/2^k`, as OpenQASM 3's `angle[k]` holds it, its bits those of `m`, the
lowest first. It lowers as a `uint[k]` does (§5.2): one `i64` that holds `m`, zero-extended,
in either form, WIT `u64` ([`quantum-wasmq.wit`](quantum-wasmq.wit), `angle-callout`). Its
value is

- a bit register of `k` bits, read as the run writes them: a measurement's, or a callout's
  result; or
- an angle known on reading: a sized `angle[w]` value by its own bits, or a real value read
  as §11.2 reads an angle, as `m'` of `2^32` parts of a turn.

Either way it is a whole number of `2^-k` turns, or the program is refused (`W016`): with
`w` the bits it is known to (`32` for a real value), `m` is the value shifted up by `k − w`
when `w ≤ k`, and when `w > k` its `w − k` lowest bits must be zero and `m` is the value
shifted down by them. Nothing is rounded to fit, and no floating-point value crosses into a
module. In the transcript (§6.4) an angle argument's `k` bits are the input's bits as any
argument's are. The first version refuses a program with an angle argument (`W016`).

A callout's result is still `bit[n]` or nothing (§5.1). A module that computes a rotation
returns its angle's numerator as bits, and the program applies it as the engine decomposes
any dyadic phase, one phase gate under a condition for each bit (`if (th[0]) p(pi / 4) q;`
for the eighths of a turn, and so on): a run of feedback with non-Clifford steps, and no
angle read back as a float (vector `v2-feedback-rotation.wai`).

### 11.2 Gates and angles

The `exact` method runs §5.1's gates and `t`, `tdg`, `p` (`phase`), `rz`, `rx`, `ry`, `ch`,
`cp` (`cphase`), `crz`, `rzz`, `ccx`, `ccz` and `cswap`, and gates a program defines from
them, with measurement, reset and conditions on bits, on at most 26 qubits (§11.3). A
program with any other gate (`u`, `cu`, `crx`, `cry`, `iswap`, `rxx`, `ryy`) is refused
(`W016`).

**An angle.** A gate's angle `θ` is the binary64 value the reader computes for its
expression: OpenQASM 3's arithmetic in IEEE 754 binary64, each operation rounded to
nearest with ties to even, and the reader's functions (`sin`, `cos`, `arccos`, `exp`, `ln`
and the rest) its own implementations, which give the same bits on every host
(`wai-quantum`, `repro`). It is read as `m` of `2^32` parts of a turn by the engine's rule
(`qasm::dyadic`), in binary64:

1. `t = (θ / τ) mod 1`, `τ` the binary64 nearest 2π and `mod` the Euclidean remainder;
2. for `j = 0, 1, …, 32`, the first `j` with `|t·2^j − r_j| ≤ 10^-14·2^j`, where `r_j` is
   `t·2^j` rounded to the nearest whole number with halves away from zero, gives
   `m = (r_j mod 2^j)·2^(32−j)`; when none does, the angle is not dyadic;
3. and the angle is `m` only when it is that angle to within its double's own rounding
   (`qasm::dyadic_exact`): with `a = m/2^32` and `g = min(|t − a|, 1 − |t − a|)`,
   `g ≤ 16·2^-52·|θ/τ|`.

An angle that fails 2 or 3 is refused (`W016`): an angle the engine's own exact method would
move to its grid, or run as no phase, runs on no wasmQ host. Each step is exact or one
correctly rounded operation, so every host reads the same `m`; the reader's floats end here.

**The lowering.** Each gate is the engine's dyadic gates (`qasm::Program::dyadic`, the gate
set of [`quantum-sim`](quantum-sim.md) §2.2), in this order, with `phase(λ)` on `t` under
the controls `C` one `P(32 − j)` on `t` under `C` for each set bit `j` of `λ`'s `m`, `j`
from 0 to 31 in order, and none when `m` is 0:

| gate | dyadic gates, in order |
|---|---|
| `id` | none |
| `x`, `y`, `z`, `h`, `s`, `sdg`, `t`, `tdg` on `q` | `X`, `Y`, `Z`, `H`, `S`, `S†`, `T`, `T†` on `q` |
| `sx`, `sxdg` on `q` | `H`, then `S` (`S†` for `sxdg`), then `H`, on `q` |
| `p(λ)`, `rz(λ)` on `q` | `phase(λ)` on `q` |
| `rx(θ)` on `q` | `H`; `phase(θ)`; `H` |
| `ry(θ)` on `q` | `S†`; `H`; `phase(θ)`; `H`; `S` |
| `cx`, `cy`, `cz`, `ch` on `c, t` | `X`, `Y`, `Z`, `H` on `t` under `c` |
| `cp(λ)` on `c, t` | `phase(λ)` on `t` under `c` |
| `crz(θ)` on `c, t` | `phase(−θ/2)` on `c`; `phase(θ)` on `t` under `c` |
| `swap` on `a, b` | `X` on `b` under `a`; `X` on `a` under `b`; `X` on `b` under `a` |
| `rzz(θ)` on `a, b` | `X` on `b` under `a`; `phase(θ)` on `b`; `X` on `b` under `a` |
| `ccx`, `ccz` on `a, b, c` | `X`, `Z` on `c` under `a, b` |
| `cswap` on `a, b, c` | `X` on `b` under `c`; `X` on `c` under `a, b`; `X` on `b` under `c` |

`−θ/2` is the binary64 the reader's arithmetic gives, read by the same rule. `rz`, `rx`,
`ry` and `rzz` are their phase forms: each drops the global phase `e^{−iθ/2}` of its matrix,
which no count shows. A gate a program defines, or writes with a modifier, is the gates the
reader expands it to.

### 11.3 The method `exact`

**The state.** `2^n` amplitudes for a program of `n` qubits, each a pair `(re, im)` of
64-bit whole numbers at `2^-30`, with qubit `q` at bit `q` of an amplitude's index; a shot
starts from `|0…0⟩`, the amplitude at index 0 `(2^30, 0)` and every other `(0, 0)`. A
dyadic gate updates it as [`quantum-sim`](quantum-sim.md) §3.0 gives, with the phase table
of `wai.quantum.circuit2` (§3.2 there, Appendix B.2): the engine's own arithmetic, its
error bound the one stated there (§5 there, about 1.71 units of `2^-30` a gate).

**A measurement** of qubit `q` takes the state's weight `W`, the sum of `re² + im²` over
every amplitude, and `W1`, the same sum over the amplitudes whose index has bit `q` set,
each exactly (a 128-bit sum holds them). The outcome is 0 when `W1` is 0 and 1 when `W1` is
`W`, and neither takes anything from the shot's stream (§6.1). Otherwise it takes the
stream's next value `x` and is 1 when `⌊x·W / 2^64⌋ < W1`, an exact comparison of whole
numbers (the product of a 64-bit and a 127-bit number), so that `x/2^64` falls below
`W1/W`. Then every amplitude of the other outcome becomes `(0, 0)`, and with `K` the weight
kept (`W1`, or `W − W1`) and `s = ⌊√K⌋`, each component `v` of every amplitude kept becomes
`⌊(v·2^30 + ⌊s/2⌋) / s⌋`, the floor of the quotient. An outcome the state determines leaves
the state as it is.

**A reset** measures its qubit as a measurement does, without writing a bit, and when it
read 1 exchanges each pair of amplitudes whose indices differ only in that bit (`X`).

Shots, outcomes, counts and the stream are §6.1's. Where a random outcome's two weights
are equal, `W1` is exactly `W/2` and `⌊x·W/2^64⌋ < W/2` holds exactly when `x < 2^63`: the
draw is the tableau's, value for value, so a Clifford program whose every random outcome
is even gives the same counts by either method (vector
`v2-exact-of-a-clifford-program.wai`, `wai-wasmq/tests/exact.rs`).

**Its accuracy.** The counts are those of this arithmetic: the same on every host, and the
ideal circuit's only to within the fixed point's error, which grows with the gates, as
quantum-sim §5 states. A result says so by its class, `bit-exact` (§11.4).

**The ceiling.** A program the `exact` method runs declares at most **26** qubits
(`W016` past it), the engine's own exact method's limit. Its state is then 1 GiB, the
largest state a 32-bit host makes as one allocation: 27 qubits are 2 GiB, past the most one
object may span there, and the reference's attempt under wasm32 ends with a capacity
overflow. Measured on the reference, on an arm64 macOS host and an x86_64 Linux host, each
natively and under wasm32-wasip2 on the pinned wasmtime, both hosts shared with other work
(a one-minute load of about two a core):

- **Memory.** Under wasm32, states of 24, 25 and 26 qubits are made and run beside 512 MiB
  of other memory, and 27 is not (`probe_the_state_past_the_ceiling`). The largest bundle
  the bounds admit, by the `exact` method at 26 qubits (its state, a module's 256 MiB of
  memory, an envelope of 128 MiB and 2^20 bits a shot) runs under wasm32 in 8.4 s, the
  wasmtime process's resident set 2.1 GB (`wai-wasmq/tests/sweep.rs`,
  `the_largest_exact_bundle_fits_a_32_bit_host`, which CI runs under wasm32).
- **Time,** in nanoseconds an amplitude at 26 qubits, each dyadic gate alone
  (`wai-wasmq/tests/exact.rs`, `measure_the_exact_method`; the same within a few percent at
  20 to 24):

  | | arm64, native | arm64, wasm32 | x86_64, native | x86_64, wasm32 |
  |---|---|---|---|---|
  | `H` | 2.1 | 11.0 | 2.8 | 20.7 |
  | `T` | 1.1 | 5.3 | 1.5 | 10.7 |
  | `P(k)` | 1.5 | 5.3 | 1.6 | 10.6 |
  | `X` under a control | 0.7 | 2.8 | 0.7 | 1.4 |
  | `X` under two | 0.3 | 0.3 | 0.6 | 0.6 |
  | a measurement | 0.8 | 4.6 | 1.2 | 9.8 |

  So a gate on 26 qubits takes 0.14 s natively and up to 1.4 s under wasm32, and §11.7
  weighs a gate's amplitude at 8 of §4.8's units: a run at the bound of 2^42 then takes at
  most about three hours on the slowest of these (`H` alone, under wasm32 on x86_64), as a
  first-version run at the bound does (§4.8).

### 11.4 The result

A second-version result is §6.4's, with these members changed:

| member | |
|---|---|
| `format` | `"wai.quantum.wasmq.result/2"` |
| `profile` | `"wai.quantum.wasmq/2"` |
| `method` | the contract's: `stabilizer` or `exact` |
| `accuracy` | `{ "class": "exact" }` for `stabilizer`; `{ "class": "bit-exact" }` for `exact` |
| `energy` | §11.5 |

**Result-equivalence** (§6.4) holds for the result less its `energy` and its receipt: every
conforming runner, on every host and every engine, gives an envelope those same bytes. The
energy is what the host read of its own run; `verify --bundle` runs the envelope again and
compares the rest. A runner that reads no meter writes the unmetered form, which is the same
everywhere, so the vectors (§9, §11.8) pin whole results.

### 11.5 Energy

`energy` is `{ "run", "callouts" }`. `run` is the run's figure; `callouts` has one member
for each `extern` the run called, the names of `fuel`'s `callouts`, each that callout's
figure. A **figure** is either

- the **unmetered form**, exactly `{ "unmetered": why }`, `why` a non-empty string; or
- a **reading**: an object with `joules_micro`, a count of at least 1; `energy_provenance`,
  a reading's class of [energy-measurement](energy-measurement.md) §2
  (`CalibratedInstrument`, `OnChipCounter` or `HwShunt`; an estimate is no reading); and
  `energy_uncertainty`, whose `relative_ppm` and `window_us` are counts of at least 1 and
  whose `relative_ppm` times `joules_micro` is at least 288 676 (§2.3 there: the rounding of
  a reading to whole microjoules). It may say more (what it covers and leaves out, its
  attribution, its source).

A figure never reads zero joules: a run that read nothing is unmetered, and says why.

**What the reference reads.** `wai-quantum run ENVELOPE.wai` runs a second-version envelope
in a process of its own and reads it whole once it has exited, on the meter its host has:
on macOS the process's CPU energy (`proc_pid_rusage`, `ri_energy_nj`), attributed to the
process, read after it exits and before it is reaped; on Linux the processor packages'
counters (`/sys/class/powercap`), the whole packages over the run's window, attributed to
nothing; the figures are the engine's (`engine::energy::figure`, `package_figure`), as the
job service seals them. Where the host reads no meter (no counter, no privilege to read
one, a counter that is not live, a wasm32 build), `run` is the unmetered form with that
reason. A library run (`wai_wasmq::run`) reads no meter: its `run` says
`the runner read no energy meter for this run`.

**Each callout's** figure is the unmetered form, saying that no meter resolves one call: a
call takes microseconds, and every counter the reference reads is of a whole process or a
whole processor package, updated in steps far longer than a call. The run's figure covers
the callouts' work with the rest of the run; fuel (§4.2) is each callout's measure of work,
on every host. A host with a meter that does resolve a call (a calibrated instrument read
around it, say) seals its reading in the callout's member.

### 11.6 Verifying

A second-version job is held to §6.5's rules 1 to 35, each read with the names of this
version (a verifier of the engine reads it through `engine::wasmq2`, whatever surface it
is checked on), with these changes, and rule 36:

- rule 4: `C`'s `profile` is `wai.quantum.wasmq/2`;
- rule 8: `run`'s `method` is `stabilizer` or `exact`;
- rule 11: `r`'s `format` is `wai.quantum.wasmq.result/2`, its `profile`
  `wai.quantum.wasmq/2`, its `accuracy` the one §11.4 gives its method, and its `method`,
  `shots` and `seed` equal `run`'s; rule 11 says nothing of `energy`, which rule 36 holds;
- rule 12: when the method is `exact`, `r`'s `qubits` are at most 26;
- rule 30: when the method is `exact`, the first term, a shot's fresh state, is
  `S × 2·2^n` (§11.7), not `S × 2·n·w`;
- rule 1 holds every number in the energy too;
- **rule 36**: `r`'s `energy` has exactly the members `run` and `callouts`; `run` is a
  figure; `callouts` is an object whose members are exactly the names of `F`'s `callouts`,
  each a figure (§11.5).

What a job's result format is decides which version's rules hold it: a result whose
`format` is `wai.quantum.wasmq.result/1` is held to §6.5 as written, so a first-version job
whose contract or result names `wai.quantum.wasmq/2` breaks rule 4 or rule 11.

### 11.7 What a run asks of its host

§4.8 holds, with the `exact` method's state in place of the tableau: for each shot, its
fresh state takes `2·2^n` operations, and each dyadic gate a step lowers to (§11.2) and each
measurement or reset `8·2^n`, where the tableau's take `2·n·r`, `r` and `2·n·r`. A run's
work is still at most 2^42 (`W017`); the weights are the reference's measured times (§11.3),
so that the bound holds a run to about three hours on every host measured.

### 11.8 Vectors

`../quantum-conformance/wasmq/` holds second-version vectors beside the first's, each made
and checked as §9 says, on every engine and every host:

- `envelopes/v2-t-toffoli.wai`: `h`, `t`, `h` and a Toffoli under two set controls, by the
  `exact` method: outcomes in the ratio of sin²(π/8);
- `envelopes/v2-feedback-rotation.wai`: a callout that turns a measured bit into three
  eighths of a turn, applied as its bits' phases between two Hadamards (§11.1);
- `envelopes/v2-angle-arguments.wai`: an `angle[8]` known on reading and an `angle[4]` of
  measured bits, given back by the module (§11.1);
- `envelopes/v2-rotations-and-a-reset.wai`: a random reset and each kind of gate §11.2
  takes;
- `envelopes/v2-stabilizer.wai` and `envelopes/v2-exact-of-a-clifford-program.wai`: one
  Clifford program by each method, with the same counts (§11.3);
- `refuse/`: an angle that is not dyadic (`v2-angle-not-dyadic`), one moved past its
  double's rounding (`v2-angle-off-the-double-s-rounding`), a gate the method does not take
  (`v2-gate-outside-the-exact-gates`), a `t` gate by the `stabilizer` method, one qubit past
  the ceiling (`v2-past-the-exact-method-s-qubits`), a run of the state vector past §4.8's
  work, an angle argument off its turns, and an angle argument in a first-version envelope,
  each beside the same bundle without its defect.

The job receipts of [`../quantum-conformance/receipts/`](../quantum-conformance/receipts/)
hold the second version's jobs the command line sealed from these envelopes
(`jobs/cli-wasmq2-*`), each with the energy its host read, and jobs crafted from them that
break §11.6's rules each alone; both verifiers of that corpus, which share no code, give every
one the same verdict and state the same rules broken, and are held to each other at each
bound of rules 4, 8, 11, 12, 30 and 36 as this section reads them.

### 11.9 What the second version leaves out

- noise, and observables other than the counts;
- floating-point arguments and results of a callout: an angle crosses as its numerator, an
  integer as itself, and a module that needs a real number scales one of them itself;
- the gates of §11.2's refusal, angles off the `2^-32`-turn grid, and more than 26 qubits by
  the `exact` method;
- a reading of one callout's energy on any host the reference runs on (§11.5);
- running beside a quantum processor (§7 holds as written). Every surface runs a bundle of
  either version: `wai-quantum run`, both MCP servers (`run_wasmq`), the job service
  (`POST /v1/wasmq`), the Python package (`wasmq`), the npm package (`QuantumEngine.wasmq`,
  on the interpreter alone), the Studio and the desktop app; and every surface of §6.5
  verifies it. Only the command line, its MCP server and the job service read a run's
  energy; the others state it unmetered, with the reason.