The rules
Twenty-three rules a programme must obey on a QCCD machine, each traced to a source. The verifier replays every cycle and reports each rule as one of four things; a green tick is only ever printed for a check that ran. Each rule below has a programme that passes it and one that fails it, both judged by the real verifier and both runnable here as the page the studio would open on them. The rules are code: docs/rules is the prose, qccd/verify/rules.py the checks, engine.js their browser twins, and a parity test holds the two implementations to identical verdicts.
All rules
R1 occupancy(site) <= site.capacity at every instant
after every cycle, no site holds more ions than its capacity.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2004.04706, arXiv:2511.15910
the same hop into a site with room for it.
p.init({"d0": "S2", "d2": "S1"})
p.move("d2", "S1", "S2")S2 already holds two ions, its capacity; a third arrives.
p.init({"d0": "S2", "d1": "S2", "d2": "S1"})
p.move("d2", "S1", "S2")R2 at most one ion occupies any junction at any instant
a junction (a node of degree 3 or more) holds at most one ion, and at most one ion crosses it in a cycle.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2510.23519
one ion at the junction.
p.init({"d1": "S1"})
p.move("d1", "S1", "S0")S0 is where the spur meets the loop; d0 is resting there when d1 arrives.
p.init({"d0": "S0", "d1": "S1"})
p.move("d1", "S1", "S0")R3 at most segment.capacity ions occupy any shuttling segment
no segment carries more ions in one cycle than its capacity (1 on every shipped device).
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2510.23519
the same two hops, one cycle each.
p.init({"d0": "S1", "d1": "S1"})
p.move("d0", "S1", "S2")
p.move("d1", "S1", "S2")two ions on the S1–S2 segment in the same cycle.
p.init({"d0": "S1", "d1": "S1"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S1", "S2"]])R4 at most max_simd_classes_per_cycle classes active; a class fixes (type, direction); participation is variadic
every movement class a cycle uses is declared by the device, and a cycle uses no more classes than the control plane allows.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2504.17886
shuttle is declared.
p.init({"d0": "S1"})
p.move("d0", "S1", "S2", cls="shuttle")no class named teleport exists on this device.
p.init({"d0": "S1"})
p.move("d0", "S1", "S2", cls="teleport")R4d a cycle must be drivable by the declared control channels: one channel carries one waveform, and opting out needs a per-site switch
a cycle is drivable by the declared channels: along a loop every ion on a shared channel moves the same signed hop, and the docks on a channel act the same way.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2403.00756, arXiv:2305.03828
R4d is a clause of R4 (the channel rule), so the verifier files its sentences under R4; the page asks for R4d alone to show them.
both hop one slot the same way: one waveform does it.
p.init({"d0": "S0", "d1": "S3"})
p.simd("shuttle", [["d0", "S0", "S1"], ["d1", "S3", "S4"]])one waveform drives the loop, and the two ions ask it to move opposite ways at once.
p.init({"d0": "S0", "d1": "S3"})
p.simd("shuttle", [["d0", "S0", "S1"], ["d1", "S3", "S2"]])R4b intra-trap and inter-trap transport never overlap in time
a cycle has one mode, and never mixes transport with a gate.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2504.17886
transport and the gate as separate cycles, which is all the language can say.
p.init({"d0": "A0", "d1": "A0"})
p.cool()
p.move("d0", "A0", "S0")
p.move("d0", "S0", "A0")
p.gate("CX", [["d0", "d1"]])one cycle that both shuttles d0 and fires a CX. The language has no statement for this: only the IR can write it, and R4b is what refuses it.
{"type": "init", "id": 0, "placement": {"d0": "S1", "d1": "S2"}, "quanta": {"d0": 0.0, "d1": 0.0}}
{"type": "simd", "id": 1, "cls": "shuttle", "mode": "inter", "participants": [{"ion": "d0", "src": "S1", "dst": "S0", "via": []}], "gate": "CX", "pairs": [["d0", "d1"]]}R5 no two ions exchange positions along one segment in a single step
no two ions exchange positions along one segment in one cycle.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3)
the same swap in two cycles, resting together at S2 in between.
p.init({"d0": "S1", "d1": "S2"})
p.move("d0", "S1", "S2")
p.move("d1", "S2", "S1")d0 and d1 swap across the S1–S2 segment. An exchange also breaks R3, R11 and the channel clause of R4: one segment, two ions, two directions, one waveform.
p.init({"d0": "S1", "d1": "S2"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S2", "S1"]])R6 gate / measure / cool only where the zone type has the capability
gates, measurement and cooling happen only in a site whose zone type has that capability, at the site the replay says the ion is in.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2504.17886
A0 is a trap site: gates, SPAM and cooling allowed.
p.init({"d0": "A0", "d1": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"]])S1 is a data site: capacity 2, gate=false.
p.init({"d0": "S1", "d1": "S1"})
p.cool()
p.gate("CX", [["d0", "d1"]])R6b a 2Q gate acts only on ions co-located in the same gate zone
both ions of a two-qubit gate are in the same site; a named site is cross-checked against the replay.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2504.17886
both ions at A0.
p.init({"d0": "A0", "d1": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"]])d1 is still at S1 when the gate at A0 fires (R6 fires too: S1 cannot gate).
p.init({"d0": "A0", "d1": "S1"})
p.cool()
p.gate("CX", [["d0", "d1"]], ["A0"])R7 a 2Q gate requires both ions' n-bar <= ms_gate.max_quanta
at gate time both ions carry no more motional quanta than the gate's budget (ms_gate.max_quanta).
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3), arXiv:2511.15910
the same walk, cooled after it.
p.init({"d0": "S1", "d1": "A0"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()
p.gate("CX", [["d0", "d1"]])d0 is cooled, then walks across the junction at S0 (3 quanta) and meets the gate hot.
p.init({"d0": "S1", "d1": "A0"})
p.cool()
p.shuttle("d0", ["S1", "S0", "A0"])
p.gate("CX", [["d0", "d1"]])R7b per-gate-zone thermal duty-cycle budget, not just instantaneous occupancy
a per-gate-zone thermal duty-cycle budget, not just the instantaneous occupancy.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2504.17886
No architecture declares a per-zone duty-cycle budget yet, so the verifier reports R7b as skipped, with that reason, rather than as passed. A busy trap zone is shown so the skip is visible.
three gates in a row in one zone: the verdict is skipped, not passed.
p.init({"d0": "A0", "d1": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"]])
p.gate("CX", [["d1", "d0"]])
p.gate("CX", [["d0", "d1"]])R7c cooling is mandatory under broadcast wiring
under a model that tracks heating, a programme with two-qubit gates schedules cooling somewhere; under a model without heating the rule is skipped.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2510.23519, arXiv:2606.06455
one broadcast cool.
p.init({"d0": "A0", "d1": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"]])a gate and no cooling operation anywhere in the programme.
p.init({"d0": "A0", "d1": "A0"})
p.gate("CX", [["d0", "d1"]])R8 the ion->site map is a bijection over time outside explicit load/unload
the ion→site map stays a bijection over time: the ion set is invariant, no ion participates twice in a cycle, no position changes without a participant.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: the ion-transport deck (v3)
two different ions.
p.init({"d0": "S1", "d1": "S4"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S4", "S5"]])d0 is listed twice in one cycle (R3 fires too: the segment carries it twice).
p.init({"d0": "S1"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d0", "S1", "S2"]])R9 claimed steps/cost/duration/quanta equal the replayed values
every claimed total, per-batch figure and per-instruction annotation equals what the replay computes.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: this platform
the true totals.
p.init({"d0": "S1", "d1": "A0"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()
p.gate("CX", [["d0", "d1"]])
p.claim(total_steps=4, total_cost=3)the programme claims 3 steps and cost 2; the replay finds 4 and 3.
p.init({"d0": "S1", "d1": "A0"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()
p.gate("CX", [["d0", "d1"]])
p.claim(total_steps=3, total_cost=2)R10 the compiled program implements the input circuit
the compiled programme implements the input circuit: every circuit operation realised once, in order per qubit, with both ions of each two-qubit gate together.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: this platform, zac
The page's verifier skips R10: it needs the circuit and a symbolic permutation with Pauli-frame tracking. On the leaderboard R10 is judged by the proved Lean checker on the compiler's certificate, which is what the entries' badges report.
a gate with no circuit to check it against: skipped, with the reason.
p.init({"d0": "S1", "d1": "A0"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()
p.gate("CX", [["d0", "d1"]])R11 shuttling is unidirectional; a trap connects to <= 2 shuttling paths
shuttling along a loop is unidirectional within a cycle, and every junction degree the device has can be priced.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2511.15910
both the same way.
p.init({"d0": "S1", "d1": "S4"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S4", "S5"]])d0 goes one way round the loop, d1 the other, in one cycle (R4's channel clause fires too).
p.init({"d0": "S1", "d1": "S4"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S4", "S3"]])R12 intra-trap parallelism = 1; inter-trap parallelism unconstrained
at most one gate per trap per cycle.
device: the same ring with a `big` spur zone: capacity 32, gates allowed · cost model: corrected · sources: arXiv:2511.15910, arXiv:2004.04706
the two pairs in two traps: inter-trap parallelism is free.
p.init({"d0": "A0", "d1": "A0", "d2": "A3", "d3": "A3"})
p.cool()
p.gate("CX", [["d0", "d1"], ["d2", "d3"]])two pairs gated in A0 at once.
p.init({"d0": "A0", "d1": "A0", "d2": "A0", "d3": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"], ["d2", "d3"]])R13 2Q gate time degrades sharply above ~15 ions per trap
no more than 15 ions in a trap at gate time.
device: the same ring with a `big` spur zone: capacity 32, gates allowed · cost model: corrected · sources: arXiv:2511.15910, arXiv:2004.04706
fifteen.
p.init({"d0": "A0", "d1": "A0", "d2": "A0", "d3": "A0", "d4": "A0", "d5": "A0", "d6": "A0", "d7": "A0", "d8": "A0", "d9": "A0", "d10": "A0", "d11": "A0", "d12": "A0", "d13": "A0", "d14": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"]])a chain of 17 in A0 when the gate fires.
p.init({"d0": "A0", "d1": "A0", "d2": "A0", "d3": "A0", "d4": "A0", "d5": "A0", "d6": "A0", "d7": "A0", "d8": "A0", "d9": "A0", "d10": "A0", "d11": "A0", "d12": "A0", "d13": "A0", "d14": "A0", "d15": "A0", "d16": "A0"})
p.cool()
p.gate("CX", [["d0", "d1"]])R14 an ion must be at a trap edge to split; getting there costs a 3-CX swap
an ion splits out of a trap only from its edge; leaving a chain of more than two needs an accounted gate_swap.
device: the same ring with load-zone spur ends (capacity 8, no gates) · cost model: corrected · sources: arXiv:2510.23519
from a chain of two every ion is at an edge.
p.init({"d0": "A0", "d1": "A0"})
p.move("d0", "A0", "S0", cls="dock")d0 splits from a chain of three with no swap accounted.
p.init({"d0": "A0", "d1": "A0", "d2": "A0"})
p.move("d0", "A0", "S0", cls="dock")R15 quanta compose with an interference term, not additively
motional quanta compose with an interference term; the replay adds them, which is an upper bound.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2605.25118
The corpus gives no secular phase model for these primitives, so every quanta figure is additive and the verifier reports R15 as partial, with that reason, on every programme that heats.
a walk across a junction: the reported n̄ is an upper bound, and R15 says so.
p.init({"d0": "S1"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()R16 2Q gate error is a function of accumulated n-bar at gate time
a two-qubit gate's error is evaluated from the n̄ its ions carry at gate time, not taken as a constant.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2510.23519, arXiv:2605.25118
R16 is a formula the replay applies, not a verdict it can fail: the two examples show it applied. Compare the gate error the replay reports for the hot gate and the cooled one.
cooled first: the error read off n̄ ≈ 0.
p.init({"d0": "S1", "d1": "A0"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()
p.gate("CX", [["d0", "d1"]])the gate on a hot ion: the error read off n̄ ≈ 3.2 (R7 fires for the same reason).
p.init({"d0": "S1", "d1": "A0"})
p.cool()
p.shuttle("d0", ["S1", "S0", "A0"])
p.gate("CX", [["d0", "d1"]])R17 anomalous heating accrues with elapsed time whether or not an ion moves
anomalous heating accrues with elapsed time whether or not an ion moves; skipped under a model that does not model time.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:2605.25118
under the corrected model d1 never moves and still heats while d0 walks: its anomalous quanta are listed below.
p.init({"d0": "S1", "d1": "A3"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()under the deck's cost model there is no clock, so R17 is skipped with that reason.
p.init({"d0": "S1", "d1": "A3"})
p.shuttle("d0", ["S1", "S0", "A0"])
p.cool()R18 a node is a junction only if three or more trap axes meet at it
a node is a junction only where three or more trap axes meet; junction cost is charged by that degree, read off the expanded graph, never declared.
device: a six-site loop with dock spurs at S0 and S3; the spur ends A0 and A3 are trap sites (gates, measurement, cooling; capacity 2), the loop sites hold 2 and cannot gate · cost model: corrected · sources: arXiv:quant-ph/0702175, arXiv:2305.03828, arXiv:1210.3655
R18 holds by construction: the price of a hop is looked up by the degree the graph reports. The two examples show the same ion crossing a degree-3 node and a plain segment.
S1 → S2 is a plain segment between two degree-2 sites: cost 1, no junction charged.
p.init({"d0": "S1"})
p.move("d0", "S1", "S2")S1 → S0 → A0 transits S0, where the spur meets the loop: cost 3, a junction_cross charged at degree 3.
p.init({"d0": "S1"})
p.shuttle("d0", ["S1", "S0", "A0"])