Correct by construction

Part I, lesson I2. You need lesson I1: this lesson proves its compiler correct.

In lesson I1 the compiler wrote a certificate and the kernel checked it: one circuit, one check. That is translation validation, and it says nothing about the next circuit until that one is compiled and checked in turn.

This lesson proves one theorem about the compiler itself. For every circuit it can be given (up to a size), and every placement, the certificate it writes satisfies Implements, the whole of the checker's specification from lesson F1. That is what a verified compiler is: the proof covers every run before any run happens, so no output needs checking. The classic example is CompCert, a C compiler proved correct in Coq; ours is smaller, and its proof runs in this page, in Lean core alone.

The compiler of lesson I1 is restated, unchanged, in a block this page runs and does not show: Gate, Circuit, opsFrom, trap, ion, chain4Sites, chain4Hops, right, left, route, Policy, honest, walk, Gate.cycles, Gate.moves, Gate.witness, movesFrom, witnessesFrom, compileWith, compile and id4. Only its studio half is left out: everything proved here is about the certificate.

1. The theorem

Here is what this lesson proves, stated first; the rest of the page is its proof.

theorem compile_correct (home : Nat → Nat) (c : Circuit)
    (hn : c.qubits ≤ 8)
    (hhome : ∀ k ∈ List.range c.qubits, home k < 4)
    (hq : ∀ g ∈ c.body, ∀ q ∈ g.qubits, q < c.qubits) :
    Implements (compile home c)

Read the three hypotheses as the fragment the theorem covers:

• hn: at most eight qubits. chain4 holds eight ions, two in each of four traps. The bound is used only to know that the ion names q0 ... q7 are different from each other.
• hhome: the placement puts every qubit in a trap of chain4, C0 to C3.
• hq: every statement names only qubits the circuit declares.

Inside the fragment, every circuit Gate can write: one-qubit gates by any name, CNOTs between any two qubits however far apart their traps are, measurements anywhere, of any length. And the conclusion is all eleven conditions of Implements, the same proposition check_sound concludes in F1.

What it does not say is as important, and section 8 lists it. In short: it is about the certificate and nothing else.

A circuit to keep in view, from I1.

2. The replay, as a fold

The checker replays a certificate with snapshots (posAt, replay, stateIn in F1). To reason about every certificate at once, we want a plainer description: the positions at the start of cycle t are the initial placement with every move before t applied in order. applyMoves applies a list of moves; List.takeWhile p l is the longest prefix of l whose elements all satisfy p.

With no rotations, the checker's event list is just the moves (merge with nothing to merge). Then the replay's state at cycle t is the fold of the moves up to the first one at or after t. The proof is by induction on the move list, with the starting state st allowed to vary (a recursive theorem: the | m :: ms, st => case uses itself on ms).

posAt_fold is a fact about the checker, not about our compiler: any proof about any compiler without rotations can start from it. Notice that it needs no sortedness. If the moves were out of order, the fold would stop at the first late one, exactly as the checker's snapshots do.

The positions are association lists, read with look and written with upd (F1). What upd does to a later look is the one fact we need about them: the key just written answers with its new value, every other key as before.

Three facts about takeWhile on a joined list, and one about applyMoves: a prefix that passes the test is kept whole; a list that fails it from the start gives nothing; and a list in which some element fails stops inside it.

3. The shape of the output

Next, what each piece of the certificate looks like. A walk's moves all move one ion, at the cycles t, t + 1, ..., and each is one of the walk's hops; a statement's moves and witness fall inside its own cycles [T, T + cycles); nothing in the rest of the circuit comes earlier. omega proves goals of linear arithmetic over Nat from the hypotheses in view; rcases and obtain take a hypothesis apart (rfl in a pattern substitutes an equation away).

The finite facts, which the kernel settles by trying every case: the eight ion names are different, the four trap names are gate sites, and every route between two traps of chain4 is made of its hops (I1, Exercise 2). List.mem_range turns k ∈ List.range n into k < n.

And the map: looking a qubit up in qmap finds its own ion, and looking an ion up in init finds its home trap. The second needs the names to be different, hence the bound eight.

4. Order and numbering, for every policy

Four of the eleven conditions are about bookkeeping: the moves come in cycle order (EventsSorted), every op that needs a witness has exactly one (Covered), every witness names an op (Grounded), and ops are realised in program order (RespectsOrder). They follow from how the compiler numbers ops and advances its clock, and not at all from where ions go. So they are proved here for every policy p, the jumper and the forgetful router of I1 included.

EventsSorted first. Inc lo l says the moves of l are at or after cycle lo, each strictly after the one before; it survives joining two lists end to end, and it is all the checker's sortedByT asks.

Covered: the witnesses for op i all come from statement i (later statements have larger indices), and statement i writes exactly one unless it is a measurement, which needs none.

Grounded: each witness comes from a statement, whose op carries its index. RespectsOrder: a witness for a later op is at a later cycle, because each statement's cycles end before the next one's begin. (The checker only asks this of ops that share a qubit; we prove it of all.)

OwnIons, for every policy too: a witness for op i names exactly the ions of op i's qubits, given a map f that sends each declared qubit to its own ion (ionOf_range is that map).

5. Transport, for the honest router

The two remaining halves are about where ions really are: every move departs from the trap the replay has its ion in (half of MovesAreHops), and every witness's ions are in its trap at its cycle (half of GatesLegal). These depend on the route, and they are false for the jumper and the forgetful router. From here on the policy is honest.

A route is chained: each hop starts where the last one ended. endOf a hops is where a chain from a ends, and a route from a to b ends at b.

Walking a chain moves one ion and no other. walk_effect: after the whole walk, the ion is at the chain's end and every other ion is where it was. walk_departs: each move of the walk departs from where the walk so far has put the ion.

Two ways to cut the move list at a cycle s: everything before s, then a block that reaches s, then the rest; or everything before s and nothing after.

The heart of the proof is the promise I1 made: at the start of every statement, every ion is at home. AtHome home n st says so of a state st. The invariant below is proved by induction over the statements still to compile, carrying the moves already written (pre, all before the clock T) and the promise about the state they leave. For each statement it shows the two transport conditions for the statement's own moves and witness, and that the promise holds again after it, which is what the induction needs for the rest:

• a one-qubit gate: no moves; its ion is at home, where its witness says;
• a measurement: nothing at all;
• a CNOT: the walk there departs from home and arrives at the target's home (walk_effect, route_spec); the gate's cycle comes after the walk there and before the walk back (tw_end), so both ions are in the target's trap; the walk back ends at home, and every other ion never moved, so the promise holds again.

6. Hops and sites

The device halves of MovesAreHops and GatesLegal: every move is a hop of chain4 and every witness's trap can gate, as long as every qubit's home is one of the four traps.

7. The proof

Everything is in place. One last small fact: a witness of the checker's order join (witnessQubits, F1) carries its gate witness's index and cycle.

And the theorem. refine ⟨rfl, ?_, ...⟩ splits Implements into its eleven conditions: the first (nothing unrealised) holds by definition, and each · below proves one of the other ten, numbered as in F1. show restates a goal in an equal form: here it unfolds the checker's let R := replay inp into posAt.

8. Using it, and what it does not say

The theorem turns a proof about one certificate into three small checks about the circuit. Here is GHZ-4 again; I1 proved its certificate by having the kernel replay it.

Exercise 1 ★ ghz4_by_theorem open

Prove that the GHZ-4 certificate holds with compile_correct, not by computing it. The three hypotheses are small decidable facts about the circuit: by decide proves each.

Exercise 2 ★ check_always_true open

The checker never refuses this compiler on the fragment. Prove it with check_complete, the converse of check_sound (both are in QCCDC.Cert.Sound): if Implements holds, check says true.

A theorem can do what no number of checks can: cover a family of circuits of every length at once. swaps k is k far swaps (I1's three CNOTs between q0 and q3, each on the longest route chain4 has), so manySwaps k writes 18 k moves. Here is k = 2.

Exercise 3 ★★ swaps_hold open

Prove that for every k, the certificate for manySwaps k holds. The third hypothesis needs an induction on k. The first two are about 4, not about k, but decide refuses a goal with a free variable in it, so state them about 4 with a type ascription: (by decide : 4 ≤ 8).

Exercise 4 ★★ bookkeeping_any_policy open

Section 4 proved four conditions for every policy. Show three of them for an arbitrary policy p and circuit: the jumper of I1, whose certificates the checker refuses, still numbers, covers and orders its witnesses correctly. Its fault is all in transport.

What the theorem does not say. It is exactly Implements (compile home c), and no more:

1. Which gate. Implements names no gate (F1, section 8). This compiler emits no pulses at all; its studio programme names abstract gates (H, CX). Whether the pulses make the circuit's gates is the semantic half of R10 (Part G), untouched here.
2. The rules. Capacity (R1) and every other rule of Part E are not part of Implements, so the theorem holds of programmes that break them. Exercise 5 is one.
3. The programme. The theorem is about the certificate. Nothing here proves that the studio programme studioWith writes (I1) moves ions as the certificate says; for a real compiler, that is a separate computed check (lesson I4).
4. Other routers. Only honest. The jumper and the forgetful router are wrong, and the checker says so (I1).
5. Bigger devices. chain4, at most eight qubits, homes among its four traps.

And it trusts what every proof here trusts: Lean's kernel, and that Implements says what you want (Part F). It also trusts that the hidden block above is I1's compiler; it is a copy of it.

Here is point 2 made concrete. Put qubit 0 in C0 and qubits 1 and 2 both in C1 (the placement crowd), and compile one CNOT from qubit 0 to qubit 1. The placement is inside the fragment, so the theorem covers it.

Exercise 5 ★★ capacity_not_promised open

Prove that the certificate holds, by the theorem, and that at the start of cycle 1, the CNOT's cycle, three ions are in C1, whose capacity is two (count them in the replay).

9. Two ways to trust a compiler

Both stop at the same place: Implements, the certificate's specification. A verified compiler does not need check_sound at all, but it can only exist in the language of the proof; the platform's own compiler is OCaml, and the next lesson is how anyone's compiler, in any language, gets the first column.

10. More about the compiler

Exercise 6 ★★ route_length open

Prove how many hops a route has. Two small inductions first (right a n and left a n have n hops), as haves inside the proof, then split on a ≤ b.

Exercise 7 ★★★ witnesses_within open

span p home gs is how many cycles the statements gs take. Prove that every witness the compiler writes for gs from clock T is before T + span p home gs, for every policy. By induction on gs, with i and T allowed to vary: witness_spec for the first statement, the induction hypothesis for the rest.

Exercise 8 ★★★ moves_even open

The honest router writes an even number of moves: every walk out is matched by a walk home of the same length. Prove it by induction on the statements. You will need that a walk has as many moves as its route has hops, and Exercise 6 for the two routes' lengths (this exercise counts as solved once Exercise 6 is).

Exercise 9 ★★★ no_cx_still open

A circuit without a CNOT moves nothing: prove that every ion is, at every cycle, where it started (compare F1, Exercise 8). First show by induction that movesFrom writes no moves for statements on one qubit each; then posAt_fold.