The Compilation page

Part H, lesson H1. You need Part F (certificates and the proved checker) and Part G (which gate the pulses make).

Part H turns the tutorial on the site itself. Every page of it that says "R10 holds" — the compiled programme implements its circuit — is making a claim, and the point of a proved checker is that you need not take the claim on trust. This lesson does it for the Compilation page; H2 for the leaderboards; H3 for the official grader; H4 reproduces a verdict from nothing but the repository.

The rule of the part: a claim is checked in this page when its certificate is small enough for Lean's kernel to compute, and with the command-line checker qcheck otherwise. Both run the same check, proved sound by check_sound (lesson F1).

1. What the page publishes

The Compilation page compiles 19 circuits and shows what became of each: the Bell pair it walks through stage by stage, fourteen basic gates (one each), and four short algorithms. They are spread over the four small devices of this tutorial, so that transport is seen on a line (chain4), a loop (race8), a lattice (grid2x3) and a loop with docks (ring6d).

For every one of them, two files are published beside this lesson, under data/:

• <id>.qcert.json: the certificate the compiler wrote;
• <id>.qcheck.json: what the checker reads. It is the certificate's fields together with three facts read out of the device's own document, never from the compiler: the traps that can gate (gate_sites), the pairs of traps one cycle apart (hops), and each closed loop's order (loops). The device facts' builder, mk_qcheck_input, makes it.

Here are the 19, with what is in each checker input:

"ops" is the certificate's copy of the circuit, after lowering: the Toffoli of algo_ccx is fifteen ops. A swap is one op with one witness; its three CNOTs are in the pulses, which the checker never reads.

2. One of them, in Lean: the GHZ chain

algo_ghz prepares a four-qubit GHZ state: h q[0], then cx q[0],q[1], cx q[1],q[2], cx q[2],q[3], then a measurement of each qubit. Below is its checker input as a Lean value: the file algo_ghz.qcheck.json, field by field and in the order the checker's own reader, Input.ofJson, puts them. (qcheck reads a well-formed file to the same value with its strict reader, Input.parse; the value below and the parsed file print the same.) The panel in section 6 builds its values the same way.

The compiler laid the chain along the register, one qubit per trap, q0 in C3 down to q3 in C0. Each CNOT carries one ion one trap down to its partner, and that ion stays there: nothing is sent home while the next gate still needs it. Play it:

circuit is the circuit's name because the page's files were compiled from a file called circuit.qasm. The checker prints that name; it checks nothing about it.

When you run qcheck on the downloaded algo_ghz.qcheck.json (section 7), its second line is

  8 circuit ops, 4 gate witnesses, 3 moves, 0 rotations, 4 qubits

Exercise 1 ★ ghz_counts open

Prove that the value above has those counts: the same file, read twice.

Exercise 2 ★ ghz_holds open

Prove that the GHZ chain's certificate holds, the way lesson F1 proved the Bell pair's: check_sound applied to the kernel's computation that the checker says true.

That is the whole O1 half of R10 for this example, proved in your browser with nothing trusted but Lean's kernel.

Exercise 3 ★ ghz_last_cx_cycle open

Find the cycle at which the witness for op 3 (cx q[2],q[3]) fires, in trap C0 on q2 and q3: replace sorry by ⟨t, proof⟩ with your cycle. Read it off the figure (step to the last two-qubit gate) or off the #eval above. As in lesson F1, by simp [case_algo_ghz] shows membership in a literal list.

At that cycle the replay must have both ions in C0. q3 started there; q2 came down from C1 at the move stamped 16.

Exercise 4 ★ ghz_last_cx_meets open

Prove it: at the start of cycle 21, q2 and q3 are both in C0.

3. A loop that turns: the parity check by rotation

algo_rot is the shape of one stabilizer measurement: an ancilla q0 and three data qubits, h q[0], three CNOTs from q0, h q[0], then q0 is measured. It was compiled by the rotation pass. On ring6d the loop L0 = S0 .. S5 cannot gate; the docks A0 (off S0) and A3 (off S3) can. The ancilla waits at the dock A0; each data ion steps into the dock, meets it, and steps back; then the whole loop turns two slots (delta = -2) and brings the next data ion to S0. A rotation is one witness for the whole loop: every ion standing on the loop advances, every docked ion stays (lesson F1, rotateState).

Step the figure to cycle 11, just after the first turn: q2, which started on S2, now stands on S0, beside the dock — and no move of q2 has happened yet.

Exercise 5 ★★ q2_rides_the_loop open

Prove both halves: at the start of cycle 11 q2 is on S0, and every move of q2 in the certificate is at cycle 12 or later. So the loop, not a move, brought it there.

4. Several examples at once

The three basic two-qubit gates were compiled onto three different devices: cx on the lattice, cz on the race track, swap on the ring with docks. In each, one ion travels to the other, the gate fires, and the travelling ion goes back where it came from. Here is the swap, at its gate: q1 came from the dock A3 round the loop to A0, where q0 waits.

A statement about several certificates is a statement about a list of them. ∀ c ∈ [a, b, c], P c is decidable whenever P is, so the kernel can settle it in one computation.

Exercise 6 ★ two_qubit_gates_hold open

Prove that all three certificates are accepted by the checker.

Exercise 7 ★★ visitors_go_home open

Prove that in all three, by cycle 30 every ion is back in the trap it started in: for every pair (ion, trap) of init, the replay at cycle 30 has the ion in that trap.

5. Two examples with no witness at all

measure and reset have one op each and no witness. That is not an omission: lesson F1's condition 9, Covered, asks a witness only of an op that is not a measurement, a reset or a barrier (needsWitness). Where a readout happens, and that it happens in its place, is the semantic half's business (Part G, and the readout comparison of the semantic check, check_cert). So a certificate with nothing to witness, nothing to move and nothing left unrealised holds as soon as its qubit map is sound — for every such certificate, not just these two.

Exercise 8 ★★★ readout_only open

Prove it in general. Implements is eleven conditions joined by ∧; refine ⟨hu, hinj, htot, ?_, ...⟩ supplies the first three and leaves eight goals. Each of the eight follows from moves, rots or gates being empty (unfold the condition and simp with the hypothesis; for EventsSorted, unfold events, merge and sortedByT too), except Covered, which follows from hops: an op whose needsWitness is false cannot also have it true.

Exercise 9 ★★ readouts_hold open

Use readout_only for both published certificates. The map conditions and hops are small computations (decide +kernel); the rest are rfl.

6. All nineteen

The panel below does for every published example what Exercise 2 did for one: it reads each checker input into a Lean value exactly as Input.ofJson would, and proves by decide +kernel that it holds. Each row links the two files, and watch opens the real compiled programme in the studio, the circuit beside it, with the certificate's rows from Lean under it.

7. The same files, outside this page

A proof in this page and a run of qcheck decide the same check on the same input. To run qcheck yourself you need the workspace's command, qccd, and Lean. Every word in the commands below is typed as shown, except where a file you saved is: that path is yours.

Step 1: Lean, and the workspace. Install Lean's installer, elan: on macOS brew install elan-init; on Linux and Windows as github.com/leanprover/elan says (and step 2's command, run before elan is installed, prints the way for each platform). Then open a new terminal and install the workspace from the repository's compiler branch (its default branch, main, does not have the checker yet). On macOS or Linux:

git clone -c core.autocrlf=false -b compiler https://github.com/yezhuoyang/QCCD
cd QCCD
python3.13 -m venv .venv && source .venv/bin/activate     # any Python 3.10 or newer
pip install -e ".[agent]"

On Windows, in PowerShell:

git clone -c core.autocrlf=false -b compiler https://github.com/yezhuoyang/QCCD
cd QCCD
py -m venv .venv
.venv\Scripts\activate
pip install -e ".[agent]"

(-c core.autocrlf=false keeps every file's line endings as published. Git on Windows otherwise rewrites them on checkout, and a certificate records a hash of its circuit file's bytes, so a circuit checked out with other line endings gives a certificate that differs in that field.)

Step 2: build the checker.

qccd toolchain build-checker

builds qcheck from the clone's Lean sources — Lean core only, no Mathlib — runs it once on a certificate it must accept and one it must reject, and from then on the workspace uses it. The first time, elan downloads the Lean the checker is pinned to (leanprover/lean4:v4.29.0-rc2). It prints (the ... stand for where the checker is, on your computer)

building the checker in ... (about a minute the first time; it does not need Mathlib) ...
built the checker (checked: it accepted and rejected a test certificate): ...
the workspace uses it from now on; `qccd toolchain check <file>.qcheck.json` runs it

Without Lean it says how to install elan instead.

Step 3: get the file. Save algo_ghz.qcheck.json, or any row's file from the panel above.

Step 4: run it on the file you saved:

qccd toolchain check algo_ghz.qcheck.json

This runs the checker the workspace uses and passes its output and its exit status through. On the published file it prints

qcheck circuit on chain4
  8 circuit ops, 4 gate witnesses, 3 moves, 0 rotations, 4 qubits
  ACCEPTED -- the program follows its certificate: mapping, transport, co-location of
  each op's own ions, order (QCCDC.Cert.check_sound).  It names no gate: which gate fires
  is decided by comparing the emitted pulses with the circuit (the semantic check), and
  R10 needs both.

Step 5: read the verdict. ACCEPTED and exit status 0 mean check returned true on that input, so by check_sound the input satisfies Implements. REJECTED and exit status 1 come with diagnose's list of the conditions that failed. Exit status 2 means the file is missing or cannot be read as a checker input.

When this lesson was written, steps 1 to 4 were run as written on Windows, from a fresh clone, and printed what is quoted here; they were not run on macOS or Linux.

A prebuilt qcheck is published too, for Windows and Linux on x86-64, pinned with its size and SHA-256 in the repository's toolchain manifest; qccd toolchain install fetches it there, together with the compiler, and runs it once on a certificate it must accept and one it must reject. When this lesson was written there was no macOS build of either, so on a Mac step 2 is the way. Building it yourself is worth doing on every platform anyway: then it is the checker of the sources in front of you, and of lesson F1. qccd toolchain status says which checker the workspace uses.

8. What you have checked, and what you have not

You have checked the O1 half of R10 for each published certificate: mapping, transport, co-location of each op's own ions, order. That is a theorem about the checker input. Three things tie it to the Compilation page's verdict, and none of them is in these two files:

• that the certificate describes the source circuit (the binding, check_binding, of the semantic check check_cert: its circuit_ops are the QASM op by op, its map covers the QASM's qubits);
• that it describes the programme (every witness names a real instruction of the right kind, and the programme's own transport equals the certificate's moves);
• O2, which gates the pulses make (Part G).

For those you need the circuit, the device and the programme, and the page publishes the circuit as text but not the programme as a file. Lesson H4 compiles the GHZ chain again, in a workspace of your own with the published compiler, has the whole of R10 checked on it, and shows that its certificate is the one above.