Any language, checked

Part I, lesson I3. You need lessons F1 and I1.

Lesson I2's proof works because the compiler is a Lean function. Our own compiler, qccdc, is written in OCaml, and yours may be Python, Rust or C++. No Lean theorem can be about those. What they can do is write a certificate, as a file, and hand it to the proved checker. If the checker accepts it, check_sound says the certificate satisfies Implements, and it says so whatever wrote the file: the proof is about the checker, never about the compiler. That is translation validation: every output checked, by a checker proved once.

This lesson follows a certificate from a file to a verdict: what the checker reads, how it reads it, what it does with a field that is missing, and which steps are proved and which are only computed.

1. The checker as a program

The command-line checker qcheck is about fifty lines of Lean. It reads one file, parses it as JSON (Json.parse, Lean's own parser), turns the JSON into an Input (Input.parse, in the module QCCDC.Cert.Syntax), and runs check, the function check_sound is proved about. It prints ACCEPTED, or REJECTED with diagnose's list of failed conditions, or REJECTED -- the input is malformed naming a field that is missing or an entry it cannot read; it exits with 0 when it accepts, 1 when it refuses, 2 when the file is not JSON.

From a compiler in any language to a verdict is three steps. The compiler writes its certificate, prog.qcert.json (lesson I4 gives its format). The device facts' builder (mk_qcheck_input) adds the device's facts, read from the device's own document, and writes the checker's input, prog.qcheck.json. Then qcheck decides:

qcheck prog.qcheck.json

The platform's grader takes exactly these steps for every design it grades (qccd submit --local runs it on your machine). qccd toolchain install fetches a prebuilt qcheck where one is published; elsewhere lake build, in the checker's own Lean package, builds it from Lean core alone.

2. The document

The file qcheck reads is one JSON object, with these keys and no others. qcheck's reader, Input.parse, refuses a file that leaves one out or writes an entry it cannot read; this page runs the module's other reader, Input.ofJson, which gives the same Input from a well-formed file and, from a malformed one, drops what it cannot read:

Every other key is ignored: a certificate's params, line, via, instr and pulses travel in the same file for the other checks (lesson I4), and qcheck never reads them. A key that is missing, or a value of the wrong shape, becomes an empty list, or 0 for n_qubits. The parser's own comment: silence is never taken for assent. An empty field does not pass quietly; the conditions then fail on it (section 5).

Here is the published GHZ chain's input, exactly as the Compilation page ships it (algo_ghz.qcheck.json), written in Lean with json%, Lean's notation for a JSON value.

qcheck's two steps, run here:

3. Computed, then proved

Which of those two steps is proved? check is: check_sound is about it. The reading is not: Input.parse and Input.ofJson are run, never proved, and so is Json.parse before them. In this page Lean cannot even look inside Input.ofJson during a proof: the page's Lean builds every file as a module, and a module shares a definition's body only when its file exposes it, which the module QCCDC.Cert.Syntax, with its private helpers, does not. Natively the kernel can unfold all of it except the qubit map, whose keys it reads with String.toNat?, which the kernel cannot compute. Either way, qcheck's verdict trusts the parser as code that runs, and the trusted base of the verdict says so (Part F).

So we split the work as qcheck does. Write down the Input the parse gives; check, by running both, that the parse gives exactly it; and prove that value holds, in the kernel. sameInput compares two Inputs field by field (== is equality as a computation, && is "and").

The parse gives exactly ghzIn. It is the certificate qccdc wrote for GHZ-4: unlike I1's compiler, it lays the chain along the register and never sends an ion home, so each control moves once and stays.

Exercise 1 ★ ghz_input_holds open

Prove that the published GHZ input, as the parser reads it, holds.

4. A file is text

Json.parse turns text into JSON, or says why it cannot. qcheckText runs qcheck's whole path on a string and says what qcheck would print, in one line.

Here is a file from a compiler with the most common bug between two languages: it copies the circuit's ops numbered from 0, as its QASM parser gave them, and numbers its own witnesses from 1. Everything else is the published Bell certificate of F1.

Two conditions fail. The witness for op 1 names one ion, and op 1 is the CNOT, on two (OwnIons); and the Hadamard, op 0, has no witness at all (Covered). The parse, as a value:

The studio plays every move and gate where the file says; under it, Lean's rows show the witnesses that are not their op's.

Exercise 2 ★★ off_by_one_refused open

Prove the file refused, with rejects_dropped_gate: an op that needs a witness and has not exactly one. The op is the Hadamard, ⟨0, "h", [0]⟩. Its membership in the literal op list is by simp [offByOne]; the other two side conditions are computations.

5. What a missing field does

A compiler that writes the qubit map with the ion names as keys ({"q0": "q0"}) instead of the qubit numbers has written nothing a reader can take as a qubit. qcheck says so at once: REJECTED -- the input is malformed: map["q0"] is malformed. The lenient reader this page runs drops the entries instead, and the map comes out empty:

Even then an empty map is never mistaken for a good one: the checker refuses it, for every certificate of a circuit with any qubit at all.

Exercise 3 ★★ no_map_refused open

Prove it, for every inp. Condition 3, MapTotal, is inp.qmap.length = inp.nQubits; it is h.2.2.1 of a proof h of Implements inp. Rewrite with hq, and the length of [] is 0.

The same holds of the device's facts. A file without gate_sites (a compiler that wrote its own qcheck input and forgot them) has no trap that can gate, so every certificate with a gate is refused.

Exercise 4 ★★ no_sites_refused open

Prove it with rejects_ungateable_site (simp knows nothing is a member of []).

6. What the file's labels and order mean

The circuit and arch fields are names for the report. The specification never reads them, so a certificate holds or fails the same under any names. That is why the semantic check (check_cert), which runs qcheck for the platform, first rebuilds the input from the certificate and the device it was given and refuses a file that differs from it (lesson I4): the names alone bind nothing.

Exercise 5 ★★ names_are_labels open

Prove that renaming the circuit and the device does not change the verdict. The two specifications are the same proposition by definition (Iff.rfl); turn that into equal verdicts with Bool.eq_iff_iff (two Booleans are equal when they are true together) and check_iff (F1: check inp = true ↔ Implements inp).

Order is different. The checker replays the moves in the order the file lists them, and condition 4, EventsSorted, requires that order to be by cycle. A compiler that writes its moves in the order a hash table returns them, every move correct, is refused.

Exercise 6 ★★★ unsorted_refused open

Prove that a certificate without rotations whose second move is at an earlier cycle than its first is refused, for every such certificate. h.2.2.2.1 is EventsSorted, a statement about sortedByT (events inp); rewrite events with your hypotheses, let simp unfold merge and sortedByT, and omega finds the contradiction.

And one witness per operation. A compiler that writes a witness for every pulse it emits, rather than one for every op of the circuit, gives a CNOT several, and condition 9 (Covered) asks for exactly one.

Exercise 7 ★★★ duplicate_refused open

Prove that if the first two witnesses of a certificate name the same op, an op that needs a witness, the certificate is refused. Use rejects_dropped_gate; after rewriting the witness list, simp computes the filter and its length.

7. Your own certificate

Now be the compiler. The circuit is h q[0]; cx q[0],q[2]; measure q[0]; measure q[2]; on three qubits (qubit 1 is declared and idle), on chain4. Its ops are fixed, and so are the device's facts; the map, the placement, the moves and the witnesses are yours. Write the Input that your compiler's file would parse to, inside the proof: the statement only says that one exists.

A certificate in the shape of ghzIn above works, with your own fields. If the kernel refuses, #eval diagnose on your value (in a def of your own) says which condition failed.

Exercise 8 ★★ hand_written open

Prove that a certificate exists for this circuit on chain4: give it, then prove the six conjuncts (five are rfl; the last is check_sound (by decide +kernel)).

As the file your compiler would write, that is a .qcheck.json like section 2's: the same keys, your values.

8. What the verdict covers

When qcheck accepts a file, check_sound gives Implements of the Input the parser made from it, whoever wrote the file and in whatever language. That is the whole of what is proved. Three things are around it, and none is part of the proof:

• the parse: Json.parse and qcheck's reader Input.parse are run, not proved (section 3);
• the binding: that the file is this certificate's, on this device, for this circuit (the names bind nothing, Exercise 5). The semantic check (check_cert) checks it, by computation;
• the programme: that the hardware programme does what the certificate says, gate by gate and move by move. The certificate's instr, pulses and via, which qcheck ignores, are what that check reads.

Lesson I4 is the format those other checks require: the full contract for a compiler that wants its programmes judged the way the platform judges its own.