WAI Extension: Quantum Compile Certificates

Mirrored from the canonical text at commit c5e7133e (2026-11-11).

Status: Draft. Defines the certificate of a compile, wai.quantum.compile/1: one record for each compile that names every pass with the digest of the circuit it was given and of the circuit it gave, the layer its check stands on and the distance it adds, so that the whole is one chain from the program’s text to the compiled program’s text; the rules any reader holds that record to without running anything; what a verifier does with a sealed one; and what each synthesis method the passes use guarantees. A job that ran compiled carries the chain in its result. Reference implementation: wai_quantum::engine::compile, engine::certificate and engine::synth; vectors: quantum-conformance/compile/.

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

1. Scope and model

A compile takes an OpenQASM program whose measurements all come at the end and writes it in another gate set (its basis) through an ordered list of named passes. Every pass is checked where it acts before its output is used; a pass whose check does not hold is left out, and the program goes on as it was. The compile’s certificate records all of it.

The claim a certificate makes is one sentence: the output text is the program text, up to a global phase, to within epsilon.bound in the operator norm, and here is each step with how it was checked. It is not a proof object that a small checker replays: it is a chain of digests that fixes which circuits the claim is about, a statement for each step of what kind of check stood behind it, and a compile that gives the same bytes on every host, so that a verifier holding the request can make the certificate again and compare.

A compile does not place a program on a device’s qubits or route it; the exact compile to a device’s own gates and connectivity for a provider’s job is the provider protocol’s (quantum-providers §4), and its program is checked there before it is sent.

2. The request

{"qasm", "epsilon", "level", "basis", "stages", "twirl", "dd", "passes"}, all but qasm optional:

The bases:

A request MUST be refused, and nothing compiled, when its program measures in the middle, resets after a gate or acts on a measured bit; when it holds more than 200 000 gates; when basis, level, epsilon, twirl or dd is not one of the values above; when it gives target (a device’s name, which a compile does not take); when it names a pass the host does not hold; or when epsilon, shared by the program’s rotations, leaves one of them less than 1e-15. A compile MUST also be refused when a pass writes more than 2 000 000 gates, the most a program is read with: its output would not read back. The pass that passes it is named, and approximate stops as soon as it does.

3. The passes

The passes a level runs, in order:

Then the request’s passes, then twirl, then dd. A request’s passes may name a built-in pass too: "passes": ["phase_resynth"] lowers the T count past phase folding at any level and in any basis.

3.1 Each level against the levels below it

A basis’s objective is what its compiles are held to: the output’s counts (§4) compared in this order, fewer first.

A pass that writes a part of the circuit again (resynth_1q, resynth_2q) keeps the new part only when it is better on the same counts in the same order, with the rotations off the multiples of π/4 weighed before them in clifford_t, since each becomes a word of about 3·log₂(1/ε) T gates.

A pass’s gain can still cost a later pass more: two-qubit blocks written again with fewer CNOTs can leave phase folding fewer T gates to merge. So a compile at level 1 or 2 also compiles the program at each level below it, under the same options (the request’s passes, twirl and dd too), and gives the output that is best on the objective, of those that tie the highest level’s: a level MUST NOT give an output worse on its objective than a lower level gives for the same request. The certificate is the kept compile’s (its passes, its bound and its check of the whole output), under the level asked for, and its guard records the comparison (here of clifford_t_n8_d40, §7.5, at level 2, whose own passes give two T gates more than level 1’s):

"guard": {
  "how": "…",
  "objective": ["t_count", "cnots", "gates"],
  "candidates": [
    { "level": 2, "output": "<64 hex>", "counts": { "t_count": 36, "cnots": 150, "gates": 287 } },
    { "level": 1, "output": "<64 hex>", "counts": { "t_count": 34, "cnots": 156, "gates": 287 } },
    { "level": 0, "output": "<64 hex>", "counts": { "t_count": 72, "cnots": 160, "gates": 374 } }
  ],
  "kept": 1
}

A lower level that refuses the program is a candidate with the reason (refused) and is not kept; a refusal of the level asked for is the compile’s. A compile at level 0 has no guard.

4. The certificate

{
  "format": "wai.quantum.compile/1",
  "basis": "clifford_t",
  "level": 0,
  "source": { "hash": "<64 hex>", "qubits": 2, "counts": { "…": "…" } },
  "output": { "hash": "<64 hex>", "counts": { "…": "…" } },
  "epsilon": { "budget": 0.0001, "rotations": 2, "each": 5e-05, "bound": 7.4e-05 },
  "passes": [
    { "pass": "lower", "input": "<64 hex>", "output": "<64 hex>",
      "layer": "exact_simulation", "bound": 0.0,
      "before": { "…": "…" }, "after": { "…": "…" },
      "check": { "how": "…", "verdict": "exact", "checked": 1, "proved": 0, "distance": 5.6e-17 } },
    { "pass": "approximate", "input": "<64 hex>", "output": "<64 hex>",
      "layer": "bounded", "bound": 7.4e-05,
      "before": { "…": "…" }, "after": { "…": "…" },
      "check": { "how": "…", "verdict": "approximate", "rotations": 2, "epsilon_each": 5e-05, "t_count": 76, "distance": 7.4e-05 } }
  ],
  "rotations": [ { "angle": 0.3, "t_count": 38, "distance": 3.8e-05, "k": 20 }, { "…": "…" } ],
  "whole": { "how": "…", "distance": 7.3e-05, "verdict": "approximate", "layer": "exact_simulation" },
  "verdict": "approximate",
  "layer": "exact_simulation",
  "weakest": "bounded",
  "reading": "…"
}

• A digest is the BLAKE3 of a circuit’s text, in 64 lower-case hex digits. The text is the circuit written as OpenQASM 3 by the engine’s writer: the line OPENQASM 3.0;, qubit[n] q;, bit[m] c; when the program has bits, one gate a line with each angle written as the shortest decimal that reads back to the same double, and the final measurements. source.hash is the digest of the program as read, in standard gates; output.hash is the digest of the compiled program’s text, which is the text the result gives.
• passes lists every pass that ran, in order, applied or not. input is the digest of the circuit the pass was given and output of the circuit it gave; layer is the layer its check stands on (§5); bound is the distance it adds to epsilon.bound; before and after are the circuit’s counts; check is the check’s own record, its verdict one of proof, exact, approximate, rejected and skipped. A pass a host registered also carries component, its identity.
• epsilon.bound is the sum of the passes’ bound, in their order, in double precision. By the triangle inequality the output is within it of the program, up to a global phase, in the operator norm; on any input the output distribution is then within it in total variation, and an observable’s expectation within twice it times the observable’s norm.
• verdict is the weakest of the applied passes’ verdicts: approximate if any is, else exact if any is, else proof. weakest is the weakest layer among the applied passes, or null when none was applied.
• whole is the check of the whole output against the whole program, and layer is its layer (§5.2): the strongest check the whole compile passed.
• rotations lists the first 64 rotations the approximation wrote: the angle, the word’s T count, its distance and the denominator exponent k of the operator found.
• guard, at a level above 0, is the comparison of §3.1: the objective, each level’s output digest and counts on it (or why that level refused), and the level kept. The passes are the kept level’s, and level is the request’s.

A certificate sealed before certificates carried input, output, layer and bound holds none of them, nor layer and weakest. It is of the earlier form, and is held to its format and its budget alone (§6).

5. Layers

5.1 A pass’s layer

Weakest first:

exact_arithmetic and stabilizer are proofs, and a pass checked by either adds no distance. exact_simulation is a numeric check: the pass’s record says exact, never proof, unless every step of it was also proved (a host’s registered pass proved by a chain of checked rewrites says proof with this layer, since each rewrite’s window is compared on a tableau or on basis states). stabilizer, exact_simulation and unchecked are the layers of those names in a job’s verdict (quantum-providers §8); exact_arithmetic and bounded are a compile’s own.

5.2 The whole compile’s layer

The whole output is held to the whole program by the first of these that decides it, and a compile whose output any of them finds is not the program MUST be refused:

So a compile that approximates never has a proof’s layer; a wide program that is not Clifford stands on its passes’ checks, and its certificate says so.

6. Holding a certificate to its form, and to its request

6.1 The form

These hold of every certificate of the chained form (one whose passes carry input or layer), and a reader can check each without running anything. A certificate that breaks one MUST NOT be accepted.

1. format is wai.quantum.compile/1.
2. Every digest is 64 lower-case hex digits.
3. The digests chain: the first pass’s input is source.hash, each pass’s input is the output of the pass before it, and the last pass’s output is output.hash.
4. Every layer is one of §5.1’s, and every bound is a finite number that is not negative.
5. A pass whose layer is unchecked, exact_arithmetic or stabilizer has bound 0, and one whose layer is unchecked has output equal to input.
6. A pass’s layer is one its check’s verdict gives: rejected and skipped give unchecked; approximate gives bounded; exact gives exact_simulation; proof gives exact_arithmetic, stabilizer or (a registered pass) exact_simulation.
7. epsilon.bound is the sum of the passes’ bound, in order, in double precision, and is at most epsilon.budget.
8. verdict and weakest are what the passes conclude (§4).
9. layer is one of §5.2’s and is whole.layer; it is not stabilizer or exact_arithmetic when verdict is approximate.
10. whole.distance, where there is one, is at most epsilon.bound plus 1e-9.
11. Where it holds guard: the guard’s objective is its basis’s (§3.1); its candidates are level and each level below it, highest first, each with an output digest and a whole number for each count of the objective and nothing else, or with refused, the first never refused; kept is the level of a candidate not refused whose output is output.hash and whose counts are output.counts’; and no candidate not refused has fewer counts, compared in the objective’s order, nor the same counts at a higher level than kept. A certificate sealed before the guard has none, and is not held to this rule.

A certificate of the earlier form is held to rule 1 and to epsilon.bound ≤ epsilon.budget. In §6.2 it is held to its output’s digest and to the check of the whole output, and to nothing that depends on the engine that wrote it (its program’s digest, the names of its options): it is never answered differs for not being reproduced.

6.2 A sealed compile

A compile is returned as {"request", "result"}, the result holding qasm (the compiled program), certificate, options, with stages when asked, the engine that made it and its schema, sealed by a receipt in the form every job’s takes (quantum-providers §8). A verifier checks the receipt first; when it holds, it looks at the compile again and reports what it finds under compile:

{ "again": "reproduced", "form": "chained", "layer": "exact_simulation",
  "weakest": "bounded", "passes": 2, "differences": [], "why": "…" }

It MUST answer differs, and the job is then not valid though its seal holds, when any of these is so (differences names each):

• the certificate breaks a rule of §6.1;
• output.hash is not the digest of result.qasm;
• of the chained form: source.hash is not the digest of the request’s program as read, or the certificate’s basis, level or epsilon.budget is not the request’s;
• the result holds stages and they are not, in order, the circuits whose digests the passes name as their outputs;
• the engine that sealed it is the verifier’s own (its name and version, the certificate of the chained form, no registered component taking part) and, compiling the request again, the verifier gets another certificate or a refusal;
• the output, held to the program by the checks of §5.2, is not the program within the bound.

Otherwise its answer is:

• reproduced: compiled again by the verifier, the request gives this certificate and this output, byte for byte. Every pass’s check ran again.
• partly: not reproduced (another engine sealed it, a registered component took part, or the program is past what a verifier compiles again), and the output was held to the program by a check of §5.2 that decides it; whole is that check.
• host_statement: not reproduced, and wider than any check of §5.2 decides: the passes’ checks are the host’s statement under its seal.

A verifier compiles a request again only when its program holds at most 50 000 gates and at most 2 000 rotations off the multiples of π/4 once lowered (each is a synthesis); past that it does not, and says so in why.

6.3 A job that ran compiled

A job whose request holds compile runs its program compiled, and its result’s compiled holds, beside the summary (basis, level, budget, distance, the bound, verdict, counts and certificate, the BLAKE3 of the certificate’s RFC 8785 canonical JSON), the certificate’s chain:

"chain": { "source": "<64 hex>", "output": "<64 hex>",
           "layer": "exact_simulation", "weakest": "bounded",
           "passes": [ { "pass": "lower", "input": "<64 hex>", "output": "<64 hex>",
                         "layer": "exact_simulation", "bound": 0.0 }, { "…": "…" } ] }

The chain is held to rules 2 to 5 and 7 of §6.1 (with compiled.distance as the bound and compiled.epsilon as the budget), to weakest, and to a layer of §5.2. A verifier then reads the request again, which compiles its program: reproduced when that gives this compiled byte for byte; differs when the chain breaks a rule, the request asks for no compile, or the verifier’s own engine gives another; otherwise host_statement.

7. What each method guarantees

7.1 Exact arithmetic

A gate whose angles are whole eighths of a turn has a matrix with entries in D[ω] = Z[ω][1/√2], ω = e^{iπ/4}: the Paulis, h s sdg t tdg sx sxdg, the rotations and u at multiples of π/4 (each up to a global phase), cx cy cz ch swap iswap, cp at multiples of π/4, crx cry crz at multiples of π/2 (under a control the rotation’s own phase counts, and its half angle must be a whole eighth), rxx ryy rzz at multiples of π/4, ccx ccz cswap. A circuit of such gates on up to 6 qubits is multiplied out as one matrix of elements of Z[ω] over a common power of √2, with integers of any size and no rounding. Two such unitaries are equal up to a global phase exactly when they are proportional: Aᵢ·Bₚ = Bᵢ·Aₚ for every entry i, for one entry p where B is not zero.

Guarantee: a proof, the same bits on every host, of the circuit as the engine reads it: an angle within 10⁻¹² eighths of a whole eighth of a turn is read as that eighth, here as everywhere in the engine. Limits: 6 qubits, 2²² gate-entry updates for the pair, and no gate outside the ring; past any of them nothing is concluded and the next check is asked.

A gate in the ring may lower to gates outside it (a controlled phase at an odd eighth lowers through sixteenths of a turn): that decomposition is compared in doubles, and lower’s layer is then exact_simulation.

7.2 One-qubit synthesis

• A Clifford+T word is multiplied out over Z[ω]/√2ᵏ and written again in its normal form, which has the fewest T gates of any word for that operator. The word is checked to multiply back to the operator, exactly. Guarantee: a proof (exact_arithmetic), and the T count is optimal for the operator.
• Any other run is one unitary, written as Rz(β)·Ry(γ)·Rz(δ) (its Euler angles, read from the matrix with the crate’s own arctangent) and so as one u gate; for clifford_t as Rz·H·Rz·H·Rz, at most three rotations for the approximation. Guarantee: compared with the run on their 2×2 matrices and kept only within 1e-12; exact_simulation.

7.3 A rotation in Clifford+T

rz(θ) at an angle off the multiples of π/4 is written as a Clifford+T word by the published grid-problem method: for the denominator exponent k = 0, 1, 2, …, the elements u of Z[ω] with u/√2ᵏ in the part of the unit disk within ε of the rotation and with its conjugate in the unit disk are enumerated as a two-dimensional grid problem; for each, t†t = 2ᵏ − |u|² is solved in Z[ω] by factoring; the first k with a solution gives the operator, and of the operators found at that k the one whose word has the fewest T gates is taken, then the nearest. All of it is integer and fixed-point arithmetic (320 fractional bits).

Guarantee. The word is Clifford+T exactly; it multiplies back, in the ring, to the operator found; and its distance to rz(θ), up to a global phase, is computed again from the word itself in fixed point and rounded up. That recomputed distance is the pass’s bound and each rotation’s distance, and it is at most the rotation’s share of the budget, or the compile is refused. The same angle and ε give the same word on every host.

What is not guaranteed. The word is not proved the shortest. At each k at most 64 candidates have their norm equation tried, and a candidate whose factoring passes 2¹⁴ steps is passed over; a shorter word behind such a candidate is missed. Measured: against every Clifford+T operator of at most 11 T gates, the word’s T count is the optimum in 21 of 24 cases and one more in 3; over 1 192 angles and precisions from 10⁻¹ to 10⁻¹³ it is never more than a reference implementation’s of the same method. The count is close to 3·log₂(1/ε).

Measured. The T count of the word for rz(θ) against ε (the engine’s test the_t_count_against_epsilon_is_the_table_the_specification_gives pins every entry and its k; every word’s distance, recomputed from the word, is within its ε). Each synthesis took under a tenth of a second, measured on one core of an arm64 host in a release build.

The rotations vectors (§9) pin five of these words, and the second implementation (§9) multiplies each pinned word out again in integers and computes its distance in 90-digit decimals: every pinned distance is the word’s own, rounded up, and within its ε.

7.4 Two-qubit synthesis

Any two-qubit unitary is (A₁⊗A₂)·exp(i(a·XX + b·YY + c·ZZ))·(B₁⊗B₂) up to a phase (the KAK decomposition), with a, b, c reduced to (−π/4, π/4].

• Around CNOTs (resynth_2q, and the basis cz with each cx written h·cz·h): three, or two when a coordinate is zero, none when all are.
• Around rzz or rxx (the bases zz and xx): the three terms commute, so the middle is one gate for each coordinate that is not zero, between the one-qubit Cliffords that turn the term’s axis into the gate’s own. A coordinate of the sign that would give a negative angle is the gate between a Pauli on the first qubit that anticommutes with the term. So a controlled phase or a CNOT takes one rzz or one rxx, where it takes two cz; a swap takes three of any.

A block is also written gate by gate through fixed identities (cx as h·cz·h; cz as one rzz(π/2) or rxx(π/2) with quarter turns undone), and that is kept where it spends no more two-qubit gates.

Guarantee and accuracy class. The decomposition is numeric: a fixed-order Jacobi eigen-solver using only + − × ÷ √ and the crate’s own trigonometric functions, in doubles. It is deterministic, the same bits on every host, but it is not exact arithmetic. Every block written is compared with the block it replaces on their 4×4 matrices and kept only within 1e-9; the measured distances add to the pass’s bound. The layer is exact_simulation, the verdict exact, never proof. A job that runs such an output does not gain the bit-exact class from it: the bit-exact method takes dyadic angles only.

7.5 T-count reduction

Three passes lower the T count, and all are proofs when the circuit is Clifford+T:

• phase_fold follows the circuit as a sum over paths: a wire holds an affine function of the path variables (one for each input qubit, a fresh one where a gate that is not a permutation of basis states writes the wire), and a phase gate on a wire holding the parity f multiplies the path’s amplitude by e^{iθf}. Phases on one parity add, across Hadamards too. The check recomputes the phase polynomial of the input and the output: the same circuit once the phases are taken out, and the same angle on every parity, in whole eighths of a turn. Where the pass changed the circuit, the circuit before and after are also multiplied out over Z[ω]/√2ᵏ within §7.1’s limits: the check’s ring is proved, or not decided past the limits or off the ring, and a pass the ring finds changed the unitary is rejected.
• resynth_1q writes each run of one-qubit Clifford+T gates in its normal form (§7.2).
• phase_resynth searches for identities among phase polynomials:
  • Regions. The circuit is cut into regions of cx cz swap x y z s sdg t tdg (and rz, p at multiples of π/4); any other gate ends the regions on its qubits. A region gate goes to the highest level its qubits have reached and any other gate after the regions of its level, which moves gates only past gates on other qubits; that is checked so: every qubit’s gates in their order.
  • What a region is. On w ≤ 64 wires a region is |x⟩ ↦ ω^{f(x)}·|A·x ⊕ b⟩, f(x) = Σₚ cₚ·(p·x) summed over parities p of its inputs with coefficients modulo 8. A term with an odd coefficient is a T gate. Two sets of T terms differ by a Clifford (S, Z and CZ on parities) exactly when they have the same signature, the parity, for every α ≤ β ≤ γ, of the terms holding all three variables; the sets with the signature of the region’s are a coset of the punctured Reed–Muller code RM(r−4, r)*, r the dimension the terms span.
  • The search. Where r ≤ 6 every word of the code (at most 2²²) is tried in Gray-code order and the first lightest word of the coset is taken: the fewest T gates any rewriting of that region’s polynomial can take. Wider, third-order duplicate-and-destroy: for z the sum of two terms and a y that keeps the signature, adding z to the terms y names makes the two one, which cancel; the pairs are tried in order until none has such a y. That finds fewer, not always the fewest.
  • The region written again. The Clifford left between the region’s polynomial and the new T terms is read from its coefficients and written as S and Z on parities; each term is put on one wire by CNOTs and its phase gates applied there, then the wires are taken to A·x ⊕ b by Gaussian elimination. A region is replaced only when that takes fewer T gates.
  • The check. Each region written again has the same affine map and the same coefficient, modulo 8, on every product of one, two and three of its variables as the region it replaces. A parity is the multilinear polynomial ⊕_{i∈S} xᵢ = Σ_{∅≠T⊆S} (−2)^{|T|−1}·Π_{i∈T} xᵢ, whose terms of four variables or more vanish modulo 8, and a multilinear polynomial is fixed by its values on {0,1}ʷ: so this is equality up to a global phase, an identity in integers at any width. Where the circuit is within §7.1’s limits the circuit before and after are also multiplied out over Z[ω]/√2ᵏ (ring, as for phase_fold). The layer is exact_arithmetic, the verdict proof. The check also records regions (those with two T gates or more), rewritten and t_removed.
  • Limits. A region ends at every gate that is not one of these, so identities that need a Hadamard taken out of the way (by an ancilla) are not searched; a region wider than 64 qubits is kept; the polynomials and searches of one pass share 2²⁸ word operations; past them a search stops with what it has found and the regions left are kept, which the check’s budget says. A region written again can take more CNOTs: T gates are what it lowers.

phase_resynth runs at level 2 of clifford_t, after the last phase_fold, and in any basis and level when a request names it in passes.

Where the whole circuit is Clifford+T on up to 6 qubits, the whole output is also proved the whole program in exact arithmetic (§5.2), whatever the passes did.

Measured. The T count of Clifford+T programs: as written (each gate lowered as lower writes it), the output of level 1, the output of level 2’s own passes and of level 2 (the best of that and the levels below it, §3.1), and the T gates phase_resynth removed in level 2’s passes; then the CNOTs of the outputs of levels 1 and 2. The first four are of the cross-simulator’s corpus (quantum-cross-simulator/corpus/qasm/), the rest of quantum-conformance/compile/benchmarks/. The engine’s test the_t_count_reductions_are_the_table_the_specification_gives pins every entry; no compile approximates a rotation, and each within six qubits is proved the program in exact arithmetic.

What it shows: phase folding takes most of what there is to take, and phase_resynth finds more where several Toffolis share variables inside one region (ccz_triples_n4: 4·Σ xᵢxⱼxₖ over the four triples is seven T gates, not eight; ccz_line_n6, at 13 more CNOTs). On the random circuits, the Toffoli chain and the adder no region phase folding leaves takes fewer by the search (where its terms span six variables or fewer, none can); what more there is needs the Hadamards between regions taken out of the way, which no pass here does. On clifford_t_n8_d40 level 2’s own passes write two-qubit blocks again with six fewer CNOTs and no more T gates, but phase folding, after them, then has two T gates fewer to merge: 36 against level 1’s 34. Each block is better on the objective where it is written; the loss shows only in the whole, so the guard (§3.1) keeps level 1’s output, and level 2 is never worse than level 1. Running phase folding before resynth_2q gives 34 T gates and 150 CNOTs here, but more T gates on five of the corpus’s rotation-heavy programs (dyadic_n6_k20, gate_c2ry, gate_c2rz, rotations_wide_n20, tn_shallow_n26, from 2 to 28 more) and fewer on two (rotations_n6, rotations_counts_n6, 12 fewer), so the order stays as it is.

8. Determinism

A compile is the same bytes on every host: the synthesis of rotations is integer and fixed-point arithmetic; the numeric decompositions use only + − × ÷ √ and the crate’s own trigonometric functions, with fixed-order eigen-solvers; no output depends on a map’s order, a clock or a thread. That is what lets a verifier compile again and compare (§6.2). The conformance vectors pin the digest of each certificate; they are held on macOS arm64, Linux x86-64, Linux arm64 and wasm32.

9. Conformance

quantum-conformance/compile/vectors.json holds:

• compile: requests in every basis, each pinned to its certificate’s digest, its program’s and output’s digests, its layers and its bound; every layer of §5.1 and §5.2 is stood on by one of them, and phase_resynth lowers the T count in two (one at level 2, one asked for by name);
• rotations: angles and precisions with the word, its T count, k and its distance;
• blocks: two-qubit blocks and how many of each device basis’s gate each takes;
• refuse: requests that are refused (§2), with words the refusal holds;
• forged: sealed compiles changed and sealed again, each breaking one rule of §6, and what a verifier must answer; and certificates another engine sealed, answered reproduced, partly and host_statement. A vector whose edit breaks the form names the rule of §6.1 it breaks; each rule a changed member can break (2 to 9, and 11, the guard’s) has one.

quantum-conformance/compile/benchmarks/ holds the Clifford+T programs of §7.5’s table that are not the cross-simulator’s.

quantum-conformance/tools/compile_form.py is a second implementation of §6.1 and of §7.3’s guarantee, in Python, from this text alone. It holds the set’s pinned certificates to the eleven rules (certificate.json, of the forged vectors’ first request, and guarded.json, a level-2 compile’s with its guard) and makes the forged vectors’ edits to the certificate of their request: each must break the rule its vector names, and a vector that names none must leave the form holding. And it multiplies each rotations vector’s word out over Z[ω]/√2ᵏ in integers: the word must be Clifford+T with the T count pinned, unitary, and no farther from its rotation, computed in 90-digit decimals, than its pinned distance, which must be that distance rounded up and within ε.

10. What it leaves out

• Placing and routing on a device, and the device bases’ one-qubit forms (prx, gpi, gpi2 with Z rotations carried in their phases): a compile to cz, zz or xx writes standard one-qubit gates around the two-qubit gate. A provider’s job is compiled exactly, from dyadic angles, by quantum-providers §4, and carries no certificate of this form.
• A proof of equivalence at any angle and any width: past the limits of §5.2 a compile stands on its passes’ checks.
• A shortest Clifford+T word for a rotation (§7.3), and the approximation of a general one-qubit unitary as one word: it is written as at most three rotations, its Euler angles read in doubles, each angle that is a whole eighth of a turn written as the gates it is and each other one approximated (§7.2).
• The fewest T gates of a whole Clifford+T circuit: phase_resynth finds the fewest for each region’s phase polynomial where its terms span six variables or fewer (§7.5), but a region ends at every Hadamard, and taking Hadamards out of the way with ancillas, which lowers the count of arithmetic circuits further, is not done.
• Programs that measure in the middle.