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