The official grader

Part H, lesson H3. You need lessons H1 and H2.

The leaderboards of lesson H2 were built by the study's own scripts. The official leaderboard is different: anyone may submit a design, and a grader the submitter does not control decides whether it is eligible. This lesson reads that grader stage by stage, models its verdict in Lean, and proves what an eligible entry must have passed.

1. Where it runs, and what it reads

The official service is at https://qccd.academy/official/. A workspace grades a design locally first (qccd submit --local), then qccd publish uploads the frozen bundle. The service stores it, and its grader runs grade on it — the official grader, the same function a local grade runs — always under the reference profile. Nothing the client says about its own grade is accepted.

A bundle is a directory of canonical JSON files:

The first four are required. The bundle's digest is the manifest's, so one digest names the whole submission.

2. The stages

grade runs these stages in this order (ler only on a memory board), and each ends with one status: passed, failed, partial, skipped, unsupported, timeout, cancelled or internal_error.

Two details matter for R10. The Lean stage is not run on a certificate that is not bound to the task: checking it would prove something about some other circuit. And the semantics stage reads four fields of the semantic check's verdict — o1_transport (which includes the witnesses checked against the programme's instructions and the programme's transport against the certificate's moves), unrealised_ops, o2_semantics, and order. A verdict without order comes from a semantic check older than the strict order rule, and counts as not checked.

3. The verdict, in Lean

Here is a real grade: the GHZ starter board ("GHZ state on four qubits (starter)", the four-qubit GHZ circuit), compiled onto a new workspace's starter design, the four-trap chain, and graded under the reference profile with qccd submit --local --board GHZ, in a workspace made from a fresh clone of the repository, on 2026-10-20 (lesson H4 does it step by step). Every stage passed.

That board's circuit is byte for byte the Compilation page's algo_ghz (both files have the SHA-256 a6c1803b...), and the bundle's certificate is the same certificate as the one you proved in lesson H1, field for field. So this is the certificate the Lean stage checked:

And its report's stages, as Lean data:

Exercise 1 ★ ghz_stage_order open

The report lists its stages in the order grade ran them. Prove it.

Exercise 2 ★ ghz_eligible open

Prove the entry eligible. (== on strings: use decide +kernel.)

4. A tampered bundle

Now change one thing. Take that bundle, swap the cycles of its last two witnesses — cx q[1],q[2] claims cycle 21 and cx q[2],q[3] cycle 14 — and seal it again with fresh digests, so that the bundle stage passes and something later has to catch it. Graded the same way, the report said lean_certificate: failed and semantics: failed, every other stage passed, not eligible. The Lean stage gave the checker's two reasons:

CERT.LEAN_REJECTED  a gate witness's ions are not together at a gate-capable trap
CERT.LEAN_REJECTED  two ops sharing a qubit are out of order: op 2 (cx [1, 2]) comes
                    before op 3 (cx [2, 3]) in the circuit, but its witness is at cycle 21,
                    not before 14

and the semantics stage reported O1 (op 3: operands not co-located at t=14). Its order was ok: the semantic check's order check reads the programme, which was not touched; only the certificate lies.

Exercise 3 ★★ swapped_rejected open

Prove the checker refuses the tampered certificate for order, with rejects_reordering: the witness join of op 2 is ⟨2, 21, [1, 2]⟩ and of op 3 is ⟨3, 14, [2, 3]⟩.

Exercise 4 ★ swapped_not_eligible open

Prove the tampered entry is not eligible.

5. What eligibility requires, for every report

The examples are two reports. The rule is about all of them.

Exercise 5 ★★ eligible_needs_required open

Prove that an eligible report has every required stage passed. simp [Report.eligible] at h turns h into a conjunction whose second half is a ∀ over the required list.

Exercise 6 ★★ no_entry_without_lean_and_semantics open

Under the checks every release on the site requires, no entry is eligible unless the Lean stage and the semantics stage passed — the two halves of R10. Use Exercise 5 twice.

Exercise 7 ★★ draft_never_eligible open

A draft grade skips the certificate stages, and is never eligible whatever its stages say. Prove that no report under another profile is eligible.

6. The certificate chain, as the code runs it

The official grader runs the last three certificate stages like this: under any profile but reference all three are skipped. Otherwise, ready says the bundle has a certificate and a certified programme (the bundle stage already refuses one that lacks either file, and grade checks again here). Without them the binding failed, and the other two are skipped. With them the binding is the binding check's result; the Lean stage is skipped when the binding did not pass and qcheck's result otherwise; the semantics stage is the semantic check's result. Below, binding, lean and sem are what each check would say if it ran.

Exercise 8 ★★★ lean_stage_needs_binding open

Prove that the Lean stage can pass only under the reference profile, for a bundle that has a certificate, whose binding passed, and which qcheck accepted. Unfold certChain, then split on the profile test and on ready (by_cases, cases); simp finishes each case.

7. The semantics stage's own rule

The semantics stage turns the semantic check's verdict into a status like this:

Exercise 9 ★★ semantics_needs_order open

Prove that the semantics stage passes only when O1, O2 and the order check all passed. Five Booleans make 32 cases: cases v, revert h, then cases on each field and decide closes every one.

8. A real report, and how to read one

GET https://qccd.academy/official/v1/submissions/<id>/report returns the latest report of a submission: a public submission's to anyone, a private one's to the account that submitted it, and 409 not_ready before it is graded. It is the object grade returns, stored as it was. The GHZ report above, shortened:

{ "kind": "qccd.evaluation_report", "version": 1,
  "task": {"id": "ghz4@1", "digest": "sha256:be83e5f5..."},
  "bundle": {"digest": "sha256:...", "files": {"certificate": "sha256:...", ...}},
  "evaluator": {"name": "qccd-reference-evaluator", "version": "1.0.0", "source_digest": "sha256:...",
                "toolchain": {"qccdc": "sha256:ba265b7f...", "qcheck": "sha256:...", ...}},
  "profile": "reference",
  "stages": [
    {"id": "bundle", "required": true, "status": "passed",
     "coverage": "manifest schema, member set, sha256 of every file, task id and digest", ...},
    ...
    {"id": "lean_certificate", "required": true, "status": "passed",
     "coverage": "QCCDC.Cert.check (proved sound: check_sound) accepted the certificate against
                  hop/gate-site facts re-derived from the submitted device", ...},
    {"id": "semantics", "required": true, "status": "passed",
     "detail": {"o1_transport": "ok", "o2_semantics": "ok", "order": "ok", "unrealised_ops": 0,
                "method": "stabilizer tableau, composed from the emitted pulses, against the
                           source QASM", "circuit_sha256": "a6c1803b..."}, ...},
    {"id": "metrics", ...}],
  "eligibility": {"eligible": true, "policy": "every required check passed under the reference
                  profile", "required": ["bundle", ..., "metrics"], "reasons": []},
  "metrics": {"T_jones": {"value": 2.13, "unit": "ms", "better": "low", "ranked": true}, ...},
  "rank_by": "T_jones", "diagnostics": [], ... }

toolchain.qccdc there is the SHA-256 of the compiler binary, here the published Windows one; toolchain.qcheck the checker's. Every diagnostic has a stable id (CERT.LEAN_REJECTED, SEM.O1, RULE.R6b, ...) and names its stage.

When this lesson was written, the official leaderboards had no entries (GET https://qccd.academy/official/v1/leaderboard/<task> returned no rows for any task), so the report above is from a local grade with the same evaluator. evaluator.comparable says what two gradings of one bundle must agree on: everything but the timing, the run's ids and the evaluator's digests.

9. What a report does not say

A report carries the bundle's digests, not its files: to re-check an entry's certificate you need the bundle, which only its submitter has. It says nothing about physical realisability beyond the task's model — the rules and the physics tables are the model. And eligible means exactly the rule of Exercise 5: every required stage passed, under the reference profile, no more.