The mutation lab

Part F, lesson F5. You need lessons F1, F2 and F4.

A checker is worth exactly what it refuses. The repository tests that with a mutation suite (mutate_cert): it takes a certificate the checker accepts, seeds one defect at a time, each a way a compiler can really be wrong, and requires the checker to refuse every mutant. Its docstring quotes the criterion from the compiler's plan: a checker that accepts a mutant is a checker that proves nothing.

The suite has fourteen mutations (its list MUTATIONS). This lesson applies all fourteen to a published certificate, exactly as the script applies them, and refuses each mutant in Lean twice: once by the kernel's computation of check, and once by the condition it breaks, with a rejection lemma. One mutant is accepted, and the suite expects that. You will see why, and who refuses the bug it stands for.

1. The certificate

algo_ghz from the Compilation page: a GHZ chain, h q[0] and then cx q[0],q[1], cx q[1],q[2], cx q[2],q[3], and a measurement of each qubit, on the four-trap register chain4. Every CNOT shares a qubit with the next, so the compiler lays the chain along the register: each qubit's ion moves one trap to meet the next.

Here it is as Lean data, written by the same function that writes the published inputs of lesson F1's panel, from the published file algo_ghz.qcheck.json.

As in F2, failing lists the conditions that say false:

2. Fourteen mutants

Each definition below is the script's mutation applied to ghz: the same field changed in the same way (the script's code is quoted in each comment). Two mutations find nothing to change in this certificate, and the script says so ("nothing to mutate in this circuit"): every trap of chain4 can gate, so there is no trap to move a gate to that cannot; and the CNOTs of the GHZ chain that share a qubit do not commute, since one's target is the other's control. For those two the lesson uses algo_rot from F2 (out of sight here), whose loop sites cannot gate and whose three CNOTs share their control.

What each breaks, by Lean's own decision of each condition:

These are the conditions the command-line checker names too: run on the same mutants, qcheck prints the same failures under REJECTED. Several mutants break more than one condition. A move sent somewhere it cannot go also leaves its ion out of place for the next gate; a reversed move list also scrambles the replay; and wrong_departure here also fails to be a hop, because the trap the script picks, C0, is not next to C2.

3. Refused by computation

The first kind of refusal is the kernel computing check on each mutant: thirteen falses.

4. Refused by the condition they break

A computed false says the mutant is refused; it does not say why. A rejection lemma says why: it names the condition and the move or witness that breaks it. Here are the mutants this lesson refuses for you; after them, the ones you refuse.

duplicate_gate gives the Hadamard two witnesses, and coverage wants exactly one:

shift_gate_time moves the last CNOT to cycle 0, when q2 is still in C1. It also puts that CNOT before the one it follows on qubit 2, and the order condition fails as well; either lemma refuses it. Click the CX row at cycle 0. The studio's own rule check, replaying the same moves, flags it too (R6b: a two-qubit gate acts only on ions together in one gate zone).

wrong_departure has q0 leave from C0, where it is not; ungateable_site puts algo_rot's first Hadamard on the loop site S0, which cannot gate.

alias_qubits puts qubits 0 and 1 on one ion; mark_unrealised has the compiler admit it gave up on op 0.

reorder_gates exchanges the cycles of the Hadamard and the first CNOT, which share qubit 0. swap_dependent_gates exchanges which op the same two witnesses realise. Joined with their ops' qubits, both produce the same pair, op 0 at cycle 8 and op 1 at cycle 2, and the same lemma refuses both. (The second also breaks OwnIons: each of the two witnesses now names the other op's ions.)

Exercise 1 ★ teleport_breaks open

Identify what teleport_move breaks: prove that, of the eleven conditions, exactly transport (6) and co-location (7) fail. The first move now takes q0 from C3 straight to C0, so it is not a hop, and q0 is not in C2 for the first CNOT. The studio, asked to make the move, refuses it: there is no segment between C3 and C0.

Exercise 2 ★★ teleport_refused open

Refuse it by its first fault, with rejects_teleport: the move is in the list, and ("C3", "C0") is not a hop of chain4.

Exercise 3 ★★ drop_refused open

drop_gate removes the Hadamard's witness. Refuse it with rejects_dropped_gate. The ops of ghzDrop are ghz's, so give simp both names for the membership.

Exercise 4 ★★ unsorted_refused open

unsort_moves reverses the move list. Refuse it with lesson F4's rejects_unsorted (restated here out of sight): the merged events are not in cycle order.

Exercise 5 ★★ foreign_refused open

foreign_ions finds, at the Hadamard's cycle, an ion that is not the Hadamard's own standing alone in a trap that can gate: q3 in C0. It rewrites the witness to name q3 there. Every ion the witness names is where it says, so co-location holds, and so does everything else; only OwnIons fails. The studio plays it without complaint: it gates whatever ion it is told to, and only the certificate checker knows which ion is the Hadamard's. Refuse it with rejects_foreign_ions. For the last hypothesis, use F3's method: a rearrangement would make permB say true (permB_complete), and it says false.

Exercise 6 ★★ commuting_swap_refused open

swap_commuting_gates exchanges which op two of algo_rot's CNOTs realise: the one on qubits 0 and 1 and the one on 0 and 2. They commute, so the unitary is the same; since 2026-10-19 the order condition refuses the swap anyway (F2, section 8). Its witness join now has op 1 at cycle 17 and op 2 at cycle 8. Refuse it with rejects_reordering.

5. The mutant that passes

swap_operands exchanges the two ions of the first two-ion witness: the first CNOT is now witnessed on q1, q0 instead of q0, q1.

Exercise 7 ★ swap_operands_accepted open

Prove the checker accepts it.

That is what the suite expects: it lists swap_operands as the one mutation the proved checker is not supposed to catch. A witness names the ions an operation ran on, never which one is the control; OwnIons compares them as a rearrangement (F2). So the order of a witness's ions carries no meaning, and exchanging them changes nothing a correct verdict depends on. algo_rot's own witnesses list the loop rider first, the other way round from the ops' qubits, and they are correct.

The bug the mutation stands for is real: a CNOT whose control and target are exchanged. That bug lives in the pulses, which the checker's input does not carry (the certificate file lists them beside each witness, as text) and Lean's checker never reads. What refuses it is the semantic half of the verdict, the semantic check (check_cert), which composes the programme's emitted pulses into a stabilizer tableau (or, off the Clifford gates, an exact unitary) and compares it with the source circuit (Part G builds that comparison). We ran all three versions of the bug through the semantic check, with the proved checker, on the published Bell certificate (bell.qcert.json) and its programme:

The first row is right to pass: nothing in it is wrong. The third is the real bug, and only the semantic half can see it, because only it reads the pulses. Neither half alone is the verdict R10.

6. Write your own

A mutation is a function from certificates to certificates, so a refusal can be proved for every certificate at once, not one mutant at a time.

Exercise 8 ★★ mark_unrealised_refused open

Here is mark_unrealised as a Lean function, for any op index k. Prove that every certificate it produces is refused.

Exercise 9 ★★★ alias_refused_always open

alias_qubits as a function: when the map starts with two entries, the second qubit is put on the first one's ion. Prove that, whenever those two entries are for different qubits, the result is refused. Hint: rejects_aliased_qubits wants ¬ MapInjective; suppose h : MapInjective ... and apply it to the two entries, which are in the map (simp [aliasFirstTwo, hq]) and share an ion (rfl); it says the qubits are equal, which hab denies.

Exercise 10 ★★★ dupFirst_refused open

duplicate_gate as a function: the first witness, written twice. Prove it refused for every accepted certificate whose first witness realises an op that needs one. The accepted certificate's Covered (from check_sound hd, condition 9) says that op has exactly one witness; with the duplicate it has two.

Hints: name the count hc ((check_sound hd).2.2.2.2.2.2.2.2.1 o ho hn), then apply rejects_dropped_gate to the op. simp [dupFirst, hg, hi] at hc ⊢ brings both counts to the length of the same filtered rest; if anything is left, <;> omega finishes it.

Applied to the published certificate, your theorem refuses the script's mutant: dupFirst ghz is ghzDup.