open-standards/wai/wai-quantum/docs/compiler.md

# Compiling with a certificate

`wai_quantum::engine::compile` takes an OpenQASM program through named
passes, checks each pass where it acts, and writes one certificate per
compile: what every pass did, the digests of the circuit it was given and
the circuit it gave, the layer its check stands on, and how far the output is
from the program. With the basis `clifford_t` (the gate set it compiles to)
every rotation becomes a
Clifford+T word within a stated budget `ε`, so the compiled circuit runs on
the bit-exact method; with `cz`, `zz` or `xx` the program is written around
a device basis's own two-qubit gate. The certificate's form, its rules and
what a verifier does with one are
[quantum-compile](../../extensions/quantum-compile.md).

```sh runnable
wai-quantum compile prog.qasm --epsilon 1e-6 > prog.ct.qasm   # passes and budget on standard error
wai-quantum compile prog.qasm --level 2 --json > cert.json     # the sealed certificate
wai-quantum verify cert.json                                   # its signature, then the compile made again here
wai-quantum run prog.qasm --compile 1e-6 --shots 1000          # compiled first, then run bit-exact
wai-quantum compile prog.qasm --basis zz > prog.zz.qasm        # around rzz, a zz device's two-qubit gate
```

The same compile is `POST /v1/compile` on the job service (sealed with the
service's key), the MCP tool `compile_qasm` on both servers,
`QuantumEngine.compile` in a page and `compile` in the desktop app. The
Studio's compile lens shows each pass with its counts and check and draws
the circuit after any pass. A job request with
`"compile": {"epsilon", "level", "basis"}` runs its program compiled, and
its result's `compiled` says how far that is from the program.

## Passes

| Pass | What it does | How it is checked | Verdict |
|---|---|---|---|
| `lower` | every gate in `h x y z s sdg t tdg cx cz swap rz`; a `rz` at a multiple of π/4 written as the named gates it is | each kind of gate against its decomposition, on its own qubits: in exact arithmetic over `Z[ω]/√2ᵏ` where the gate's angles and its decomposition's are whole eighths of a turn, and by their dense matrices | `proof` when every decomposition used was proved in exact arithmetic, else `exact` |
| `simplify` | the engine's rewrites: a gate and its inverse cancel, rotations merge, Hadamards conjugate, a gate is carried past what it commutes with | each rewrite on the qubits it touches, by tableau or on every basis state | `exact` |
| `phase_fold` | phase gates on the same parity (the same XOR of path variables) merged into the first of them; `T` gates on one parity become `S` or vanish | the phase polynomial recomputed: the same gates once the phases are taken out, and the same total angle on every parity | `proof` when every angle is a multiple of π/4 (the comparison is in whole eighths of a turn), else `exact` |
| `resynth_1q` | each run of one-qubit gates written again when that is cheaper: a run of Clifford+T gates in its Matsumoto–Amano normal form (the fewest `T` of any word for it), any other run as one rotation | Clifford+T runs multiplied out in exact ring arithmetic; others on their 2×2 matrices | `proof` or `exact` |
| `resynth_2q` | each block of gates on one pair of qubits written again by the KAK decomposition, at most three CNOTs, when that uses fewer | each block against its replacement on their 4×4 matrices | `exact` |
| `approximate` | every `rz` off the multiples of π/4 written as a Clifford+T word within its share of the budget (Ross–Selinger) | each word multiplied out in exact arithmetic over `Z[1/√2, i]`, and its distance to the rotation recomputed from the word in fixed point and rounded up | `approximate`, with the distance |
| `native_2q` (bases `cz`, `zz`, `xx`) | each block of gates on one pair of qubits written around the basis's own two-qubit gate (`cz`, `rzz` or `rxx` at an angle from 0 to π/2): by the KAK decomposition, one gate for each canonical coordinate that is not zero (three CNOT-equivalents at most for `cz`), or gate by gate through fixed identities where that spends no more; at level 0 gate by gate only | each block against what it is written as on their 4×4 matrices, in doubles | `exact` |
| `twirl` (asked for with a seed) | each `cx`, `cz` and `swap` framed by a seeded random two-qubit Pauli `P` before it and its image `G P G†` after it: the same gate, and on average its noise made a Pauli channel | each distinct framed gate (gate and frame) against the bare gate by the equivalence ladder on its two qubits, a tableau each; then the whole circuit by the ladder where it decides | `proof` |
| `dd` (asked for with a sequence, `xx` or `xy4`) | in each window where a qubit idles, between its first gate and the end of the circuit, for at least as many layers as the sequence has pulses, the sequence's pulses spread across the window; each qubit's gates keep their order | the sequence against nothing by the ladder (a tableau), and the whole circuit by the ladder where it decides | `proof` |

`twirl` and `dd` run after the level's passes, `twirl` first, only when a
request names them (`"twirl": SEED`, `"dd": "xx"` or `"xy4"`; on the command
line `--twirl SEED` and `--dd xy4`). The same seed gives the same frames on
every host. A twirled circuit is the program exactly (up to a global phase):
what changes is how a device's noise acts on it, averaged over seeds, which a
noiseless simulation cannot show. Decoupling suppresses coherent noise on
idle qubits; the engine's noise models act after gates, so in its own
simulations the pulses only add gates, and the record says so.

A pass whose check fails is not applied: its record says `rejected`, and the
program goes on as it was. A pass that does not run (the rewrites past
20 000 gates) says `skipped` and why.

## Levels

| Level | `clifford_t` | `standard` | `cz`, `zz`, `xx` |
|---|---|---|---|
| 0 | `lower`, `approximate` | `lower` | `lower`, `native_2q` |
| 1 (default) | `simplify`, `lower`, `simplify`, `phase_fold`, `lower`, `approximate`, `phase_fold`, `simplify`, `lower` | `simplify`, `lower`, `simplify`, `phase_fold`, `simplify` | `simplify`, `lower`, `simplify`, `phase_fold`, `simplify`, `lower`, `native_2q`, `resynth_1q` |
| 2 | level 1 with `resynth_2q` and `resynth_1q` before the approximation, and `resynth_1q` after it | level 1 with `resynth_2q`, `lower` and `resynth_1q` | as level 1 |

## Device bases

`--basis cz`, `zz` or `xx` writes the program as one-qubit gates at any
angle around one kind of two-qubit gate: `cz` (the gate of the device bases
`rz sx x cz` and `prx cz`), `rzz(θ)` (a `zz` device's gate at `θ/2π` of a
turn) or `rxx(θ)` (an `xx` device's). Every angle of the two-qubit gate is
between 0 and π/2, a device's 0 to ¼ turn. Each pair's block of gates takes
at most three:

| Block | `cz` | `zz` | `xx` |
|---|---|---|---|
| a CNOT or a controlled Z | 1 | 1 | 1 |
| a controlled phase, or one `rzz`, `rxx` or `ryy` at any angle | 2 | 1 | 1 |
| an iSWAP, or `rxx` and `ryy` together | 2 | 2 | 2 |
| a swap, or `rxx`, `ryy` and `rzz` together | 3 | 3 | 3 |

The decomposition is numeric (a fixed-order eigen-solver, in doubles): the
same bits on every host, but not exact arithmetic. Each block is compared
with what it is written as on their 4×4 matrices and kept only within `1e-9`,
the measured distances add to the bound, and the pass's verdict is `exact`,
never `proof`. Nothing is placed on a device's qubits or routed here, and the
one-qubit gates are the standard ones, not a device's `prx` or `gpi`.

`lower` comes again before the approximation and last because a rewrite may
write `h·rz·h` as `rx`. For `clifford_t` the resynthesis passes weigh
rotations first (each costs about `3·log₂(1/ε)` T gates), then CNOTs, then
`T` gates; for `standard`, CNOTs then gates.

## Reading ε

`ε` bounds the **operator-norm distance up to a global phase**,
`min_φ ‖U_out − e^{iφ}·U_program‖`. It is a budget the compile spends:

- the approximation pass divides what is left of it (after the distances of
  the passes before) evenly among the rotations it writes: `epsilon.each`;
- every word comes within its share, measured from the word itself;
- the passes' distances add up by the triangle inequality to
  `epsilon.bound`, which is never more than `epsilon.budget`.

From `bound` alone, for every input state: the output distribution is
within `bound` of the program's in total variation (so is each outcome's
probability), and an observable's expectation within `2·bound·‖O‖`.
Amplitudes agree up to one global phase.

Up to 8 qubits the whole output is also measured against the whole program
on their dense unitaries (`whole.distance`, computed to about `1e-15`), and
the compile is refused if that measurement exceeds the bound by more than
`1e-9` (the allowance for rounding). Wider
programs rest on the composition of the passes' own checks.

A rotation is approximated to an `ε` between `1e-15` and `0.5`; a budget too
small for the rotations sharing it is refused with the share it would
leave. The `T` count of a word is close to `3·log₂(1/ε)`: about 20 at
`1e-2`, 60 at `1e-6`, 100 at `1e-10`, 150 at `1e-15`, each found in a few
milliseconds. On small `ε` the exhaustive test
(every Clifford+T operator with at most 11 `T` gates) finds the word's `T`
count at the optimum in 21 of 24 cases and one above it in the rest.

## Layers, and the chain of digests

Each pass's record names the layer its check stands on, weakest first:

| Layer | The check | Is it a proof |
|---|---|---|
| `unchecked` | none: the pass was skipped, or its check did not hold and it was left out; its output is its input | nothing is claimed |
| `bounded` | the output's distance from the input, computed from the output in fixed point and rounded up | no: within the bound |
| `exact_simulation` | compared in double precision (dense matrices, every basis state of the qubits a step touches, a phase polynomial's sums) | no: equal to the rounding of doubles |
| `exact_arithmetic` | an identity in integers (a word over `Z[ω]/√2ᵏ`, a phase polynomial in whole eighths of a turn, two unitaries proportional entry by entry) | yes |
| `stabilizer` | equal stabilizer tableaus | yes, for Clifford circuits |

The certificate's own `layer` is the strongest check the whole output passed
against the whole program: `stabilizer` (both Clifford, up to 4096 qubits),
`exact_arithmetic` (every gate of both with entries in `Z[ω]/√2ᵏ`, up to 6
qubits: a Clifford+T program's whole compile is then a proof whatever its
passes' layers), `exact_simulation` (their dense unitaries, up to 8 qubits),
or `pass_equivalence` when only the passes' own checks, composed, stand
behind it. `weakest` is the weakest layer among the passes applied.

Each record also holds `input` and `output`, the BLAKE3 of the circuit before
and after the pass, written out as OpenQASM 3. They chain: the first input is
`source.hash`, each output is the next input, the last is `output.hash`. And
`bound`, the distance the pass adds; the bounds add to `epsilon.bound`.

`wai-quantum verify` (and every surface that verifies a job) checks the
receipt, then looks at the compile again and says what it found under
`compile`: `reproduced` (compiled again here, the request gives this
certificate byte for byte), `partly` (another engine's certificate: the
output was held to the program here), `host_statement` (the form holds, and
nothing more could be decided here) or `differs` (not the certificate the
request bears out: the job is refused, though its seal holds). A job that ran
compiled carries the chain in `compiled.chain` and is held to it the same
way.

## The certificate

For `h q[0]; rz(0.3) q[0]; cx q[0], q[1]; ry(1.1) q[1];` at `--epsilon 1e-4`
(level 1), abridged:

```json
{
  "format": "wai.quantum.compile/1",
  "basis": "clifford_t",
  "level": 1,
  "source": { "hash": "3088646d…", "qubits": 2,
              "counts": { "gates": 4, "cnots": 1, "t_count": 0, "rotations": 2, "depth": 4, "…": "…" } },
  "output": { "hash": "a6aff9b0…",
              "counts": { "gates": 197, "cnots": 1, "t_count": 76, "rotations": 0, "depth": 197, "…": "…" } },
  "epsilon": { "budget": 0.0001, "rotations": 2, "each": 5e-05, "bound": 7.453429548248133e-05 },
  "passes": [
    { "pass": "simplify", "input": "3088646d…", "output": "3088646d…", "layer": "exact_simulation", "bound": 0.0,
      "before": { "…": "…" }, "after": { "…": "…" },
      "check": { "how": "rewrites, each checked on the qubits it touches by tableau or on every basis state", "verdict": "exact", "steps": 0 } },
    { "pass": "lower", "…": "…", "layer": "exact_simulation", "bound": 0.0,
      "check": { "how": "each kind of gate against its decomposition, on its own qubits: …", "verdict": "exact", "checked": 1, "proved": 0, "distance": 5.551115123125783e-17 } },
    { "pass": "approximate", "…": "…", "layer": "bounded", "bound": 7.453429548248133e-05,
      "check": { "how": "each rotation's Clifford+T word multiplied out in exact ring arithmetic, and its operator-norm distance to the rotation recomputed from the word in fixed point and rounded up",
                 "verdict": "approximate", "rotations": 2, "epsilon_each": 5e-05, "t_count": 76, "distance": 7.453429548248133e-05 } },
    { "pass": "phase_fold", "…": "…", "layer": "exact_arithmetic", "bound": 0.0,
      "check": { "how": "the phase polynomial recomputed: … in whole eighths of a turn", "verdict": "proof", "merged": 39 } },
    { "…": "…" }
  ],
  "rotations": [
    { "angle": 0.3, "t_count": 38, "distance": 3.77439802702028e-05, "k": 20 },
    { "angle": 1.1, "t_count": 38, "distance": 3.679031521227853e-05, "k": 20 }
  ],
  "whole": { "how": "the dense unitaries of the whole program and the whole output", "distance": 7.269652454265581e-05, "verdict": "approximate", "layer": "exact_simulation" },
  "verdict": "approximate",
  "layer": "exact_simulation",
  "weakest": "bounded",
  "reading": "The output equals the program up to a global phase to within 7.453429548248133e-5 in the operator norm (the budget was 1e-4). …"
}
```

Each rotation came within its share (`3.8e-5` and `3.7e-5` against `5e-5`),
the two add to the bound `7.5e-5`, and the whole output measured against the
whole program is `7.1e-5`, inside it. `k` is the denominator exponent of the
operator found: its entries are in `Z[ω]` over `√2^k`.

- `counts` take each gate as `lower` would write it: `cnots` counts a `swap`
  as three, `t_count` counts the `T` gates of the Clifford+T lowering (an
  `rx(π/4)` is one), `rotations` the `rz` gates left at angles off the
  multiples of π/4.
- `verdict` is the weakest of the passes': `approximate` if anything was
  approximated, else `exact` if anything was compared to the rounding of
  doubles, else `proof`.
- `source.hash` is BLAKE3 of the program as read, written out as OpenQASM 3;
  `output.hash` BLAKE3 of the output text.
- The compile result is `{"ok", "options", "qasm", "certificate"}`, sealed
  in a job's form (`{"request", "result"}`, the receipt in the result), so
  `wai-quantum verify`, `POST /v1/verify` and `engine_verify` check it. With
  `"stages": true` in the request it also holds `stages`, the circuit after
  each pass, in order (sealed with the rest, not part of the certificate).
- A compiled job's result carries `compiled`: the basis, level, budget,
  `distance` (the bound), verdict, counts before and after,
  `certificate`, the BLAKE3 of the certificate's RFC 8785 canonical JSON,
  which `wai-quantum compile` prints as its `digest`, and `chain`, the
  certificate's chain: the program's digest, each pass's digests, layer and
  bound, and the output's digest.

## Determinism

The compile is the same bytes everywhere: the synthesis is integer and
fixed-point arithmetic (320 fractional bits), the decompositions use only
`+ − × ÷ √` and the crate's own trigonometric functions, the eigen-solvers
are fixed-order Jacobi and QL iterations, and no output depends on map
order or a clock. CI compiles one program natively and as a WASI
component and compares the sealed bytes, and the browser build's tests
compile one request to the native build's pinned digest.

## What it does not do

- Programs that measure in the middle, reset after a gate or act on
  measured bits are refused.
- There is no layout or routing onto a device here, and a compile to `cz`,
  `zz` or `xx` writes standard one-qubit gates, not a device's own; the
  exact native compile to a processor's basis and coupling map, from dyadic
  angles, is `quantum_toolchain::native`, and Clifford routing certificates
  are `quantum_compile`.
- The word for a rotation is not proved the shortest: at each denominator
  exponent at most 64 candidates are tried, and one whose norm equation does
  not factor within its budget is passed over.
- No pass searches for identities among phase polynomials, which lower the
  `T` count further on arithmetic circuits.
- Past 8 qubits, a program that is not Clifford stands on its passes' own
  checks, composed (`pass_equivalence`): nothing holds the whole output to
  the whole program.
- A multi-qubit rotation is approximated through its lowering (each `rz` it
  lowers to, separately), not synthesised as one.