c4c1294e00
wai/tools/quantum-docs/check_docs.py runs every block marked runnable on the
pages docs.json names (the engine, the command line, the service, Python,
the Studio, the desktop app, the editors, the providers, the compiler,
estimates, verdicts, the feature matrix, the course and the agent skill) in
a scratch directory of fixtures, holds each shown output to the real one,
verifies every receipt a block writes, builds and runs the Rust blocks, and
checks every block that cannot run for the commands and flags it names,
every wai-quantum command in the prose, every relative link and every
dependency shown; a translation must hold its English page's code. ci.sh
builds the command line, the service and the wheel and starts a service, as
wai-quantum-docs.yml runs it, beside the course's and the locales' tests.
Drift fixed: the crate pinned "0.4", named an unrelated crate for the command
line, ran its research tools outside lab, claimed the whole suite under
wasip2, and split its feature table from its header; the command line's
README said the reader refuses while, inv and pow, used placeholders and
optional flags that do not run, and merged versions that do not exist; the
estimate page's output lacked its receipts line; build steps now match CI.
An observable may lead with its coefficient ("0.5 X2"), as documented.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
175 lines
11 KiB
Markdown
175 lines
11 KiB
Markdown
# 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, how it was checked, 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.
|
||
|
||
```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, as for any job
|
||
wai-quantum run prog.qasm --compile 1e-6 --shots 1000 # compiled first, then run bit-exact
|
||
```
|
||
|
||
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, by their dense matrices | `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 |
|
||
| `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` |
|
||
|---|---|---|
|
||
| 0 | `lower`, `approximate` | `lower` |
|
||
| 1 (default) | `simplify`, `lower`, `simplify`, `phase_fold`, `lower`, `approximate`, `phase_fold`, `simplify`, `lower` | `simplify`, `lower`, `simplify`, `phase_fold`, `simplify` |
|
||
| 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` |
|
||
|
||
`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.
|
||
|
||
## 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": "65e0c256…",
|
||
"counts": { "gates": 200, "cnots": 1, "t_count": 78, "rotations": 0, "depth": 200, "…": "…" } },
|
||
"epsilon": { "budget": 0.0001, "rotations": 2, "each": 5e-05, "bound": 7.453429548248133e-05 },
|
||
"passes": [
|
||
{ "pass": "simplify", "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", "…": "…",
|
||
"check": { "how": "each kind of gate against its decomposition, on its own qubits", "verdict": "exact", "checked": 1, "distance": 5.551115123125783e-17 } },
|
||
{ "pass": "approximate", "…": "…",
|
||
"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": 78, "distance": 7.453429548248133e-05 } },
|
||
{ "pass": "phase_fold", "…": "…",
|
||
"check": { "how": "the phase polynomial recomputed: … in whole eighths of a turn", "verdict": "proof", "merged": 41 } },
|
||
{ "…": "…" }
|
||
],
|
||
"rotations": [
|
||
{ "angle": 0.3, "t_count": 38, "distance": 3.77439802702028e-05, "k": 20 },
|
||
{ "angle": 1.1, "t_count": 40, "distance": 3.679031521227853e-05, "k": 20 }
|
||
],
|
||
"whole": { "how": "the dense unitaries of the whole program and the whole output", "distance": 7.123665880156653e-05, "verdict": "approximate" },
|
||
"verdict": "approximate",
|
||
"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, and
|
||
`certificate`, the BLAKE3 of the certificate's RFC 8785 canonical JSON,
|
||
which `wai-quantum compile` prints as its `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; the exact native
|
||
compile to a processor's basis and coupling map is
|
||
`quantum_toolchain::native`, and Clifford routing certificates are
|
||
`quantum_compile`.
|
||
- A multi-qubit rotation is approximated through its lowering (each `rz` it
|
||
lowers to, separately), not synthesised as one.
|