The rules

A rule is one assertion about the hardware and what the machine does on it, written in a small language you can read on this page: for every site and every instant, the ions in the site number at most its capacity is written for all s in sites, t in instants: occupancy(s, t) <= capacity(s). The checker evaluates exactly that text; nothing else decides a rule.

Rules are not fixed. A rule set chooses the rules a machine assumes and sets their numbers, and the compiler takes one as input: it plans with the rules it knows how to satisfy, and everything it produces is then checked against every rule of the set, including rules it has never seen. The papers on Reproduce assume different rules from this website’s machine and from each other, and each is judged by its own rule set. 4 rules are core: they hold in every rule set and cannot be dropped (R0, R1, R8, R24).

holdsthe rule was evaluated and is true

failsthe rule is false; the page names the values that make it so

does not applythe execution has nothing the rule is about, and the page says what

could not be checkeda value the rule needs is missing, and the page says which

the language
the words
rule sets
every rule
writing a rule

Reading a rule

A rule is a formula of first-order logic over finite sets: the sites of the device, the operations of the execution, the instants at which its state is judged, and the operations of the input circuit.

for all x in D: P            P holds for every x in the set D
for all x in D where C: P    ... for every x in D for which C holds
for some x in D: P           P holds for at least one x in D
for all a, b in D: P         for every pair a, b in D (also a = b, unless excluded)
P and Q,  P or Q,  not P,  P implies Q
x = y,  x != y,  x <= y,  x in S,  x not in S,  a + b,  a * b
count(x in D where C)        how many x in D satisfy C
sum(e for x in D where C)    the sum of e over them (also max, min)
{e for x in D where C}       the set of the values of e; size(S) counts it
"C3"                         the site (or ion) named C3

A rule may begin with when C:. When C is false the rule does not apply to that execution, which is reported as such, never as holding. A word that an execution does not have (the steps of a paper’s timed schedule, or the circuit when none was given) makes the rule not apply, and the page says which word.

The words

Every word a rule may use, with what it means. Two kinds of execution are judged by the same rules: a programme, run one step at a time with everything in a step happening together (what this website’s compiler produces), and a paper’s timed schedule, whose operations each have a start and an end and overlap whenever the machine allows. Where a word is read differently from the two, both readings are given.

The device

`ends(r)`	The two nodes rail r joins.
`junctions`	The nodes where three or more rails meet, whatever the device calls them. An ion crosses a junction; whether it may stop there is a rule.
`nodes`	Every node of the device: its sites and its junctions.
`rails`	The rails (segments) along which ions are carried between nodes.
`rails_at(n)`	The rails that end at node n.
`sites`	Every place an ion can stand: the traps, the docks, the slots of a loop. A node where rails cross only to pass through it is not a site.
`angle(n, r1, r2)`	The angle at node n between rails r1 and r2, as drawn. Only in a programme.
`can(s, a)`	Whether site s is equipped for ability a: "gate" (a laser gate), "spam" (preparation and measurement) or "cool" (cooling). In a timed schedule: A paper's device that declares no abilities is taken to allow everything; its own rules then say where each operation may run.
`capacity(x)`	How many ions the site or rail x may hold at once, as the device declares it.
`control()`	How the device's electrodes are driven: "direct" (every electrode its own signal) or a broadcast scheme where many share one waveform. Only in a programme.
`cross(r1, r2)`	Whether rails r1 and r2 cross each other at a point that is not a node they share. Only in a programme.
`degree(n)`	How many rails meet at node n.
`heat_budget()`	The hottest an ion may be when a two-ion gate starts (its motional quanta n̄), as the device declares it; no limit when it declares none. Only in a programme.
`lies_on(n, r)`	Whether node n lies on rail r's line without being one of its ends -- a rail drawn straight through a node it does not stop at. Only in a programme.
`max_classes()`	How many different motions the device's control system can drive in one step. Only in a programme.
`max_junction_degree()`	The most rails a junction of this device may join, as its document declares (4 when it says nothing: a surface trap has T- and X-junctions). Only in a programme.
`min_rail_angle()`	The smallest angle two rails meeting at a node may make, as the device's document declares (60 degrees when it says nothing). Only in a programme.
`neighbours(s1, s2)`	Whether sites s1 and s2 are neighbouring zones that a two-ion gate may span (some devices gate across two zones of one rail).
`priced(j)`	Whether the device declares the time it takes to cross junction j, at j's number of rails. Only in a programme.
`rotated(n)`	Whether node n is a slot of a loop or rail that this programme moves as a whole (a conveyor), which carries every ion through every slot. Only in a programme.
`zone(s)`	The zone type of site s (for example "gate", "storage", "O").

The execution

`claims`	Every figure the programme states about itself: its total time, cost and steps, and per-instruction annotations. Only in a programme.
`coolings`	Every cooling operation.
`crossed(o)`	The junctions transport operation o carries its ion into, on the way or to stop.
`declared_sites(o)`	The sites the programme itself names for operation o, if it names any (a claim the replay checks). In a timed schedule: Empty: where a paper's operation says it happens is checked with its ions (found).
`gates`	Every laser gate, on one ion or on two.
`hops`	Every rail crossed by an ion: one transport operation over three rails is three hops. Only in a programme.
`ions`	Every ion of the execution. At the machine level, ions(b) is block b's ions.
`ions(o)`	The ions operation o acts on or carries.
`locks(o)`	The components the schedule itself says operation o holds while it runs. Only in a paper’s timed schedule.
`measurements`	Every measurement of an ion.
`operations`	Every operation of the execution, of any kind.
`passes(o)`	The nodes transport operation o carries its ion through without stopping: its path without the two ends.
`path(o)`	The nodes transport operation o carries its ion through, first to last.
`rails_used(o)`	The rails transport operation o uses.
`resets`	Every reset (preparation) of an ion.
`single_qubit_gates`	Every gate that acts on one ion.
`splits`	Every operation that lifts an ion out of the chain it stood in. In a programme: A move whose motion includes a split (the device's movement class says so).
`steps`	The steps of a programme: one instruction each, run one after another; everything in one step happens together. Only in a programme.
`swaps`	Every reordering of two ions inside one chain.
`transport`	Every operation that carries an ion along the rails. In a programme: One operation per moving ion per step, from where it stood to where it stops. In a timed schedule: Each split, merge, rail crossing, junction entry and exit, or hop the paper records.
`two_qubit_gates`	Every gate that acts on two ions together.
`abs(x)`	The size of a number, without its sign.
`approx(x, y)`	Whether two durations agree to within the execution's rounding (one part in a million).
`at_chain_end(o)`	Whether split o takes the ion at the end of its chain that faces the rail it leaves by. In a programme: A programme does not record the order inside a chain, so only a chain of at most two ions is known to have every ion at an end. In a timed schedule: Read from the chain order, tracked event by event as the paper's model does.
`carries_gates(k)`	Whether step k also names gates. Only in a programme.
`claimed(c)`	The value claim c states. Only in a programme.
`class_declared(k)`	Whether transport step k's movement class is one the device declares (or the device declares none to check against). Only in a programme.
`clock(o)`	How long the execution's clock says operation o takes: the paper's own duration law; none where an operation is not one the model has. Only in a paper’s timed schedule.
`clocked(o)`	Whether the clock makes a claim about operation o. For a schedule this website wrote itself, every operation must be one the paper's model times; a paper's own schedule may contain operations its law does not time. Only in a paper’s timed schedule.
`disjoint(A, B)`	Whether sets A and B have nothing in common.
`drivable(k)`	Whether the device's control channels can drive step k: one channel carries one waveform, so every ion a channel moves must move the same way, and a site may sit a step out only if it has its own switch. Only in a programme.
`duration(o)`	How long operation o lasts. In a programme: Its step's duration under the device's clock (the slowest operation of the step).
`end(o)`	The instant operation o is over. In a programme: The instant after o's step.
`found(o)`	Whether operation o finds its ions where it says they are and leaves them where the next operation expects them. In a programme: The replay refuses a programme that does not, so this always holds once it runs. In a timed schedule: Replayed event by event.
`from(o)`	Where transport operation o (or hop o) picks its ion up.
`is_transport(k)`	Whether step k moves ions. Only in a programme.
`kind(o)`	What operation o is: "gate2", "gate1", "measure", "reset", "cool", "swap", or a transport kind ("move", "split", "merge", "shuttle", "junction_enter", "junction_exit", "hop").
`loop(h)`	The closed loop hop h runs along, or none. Only in a programme.
`max(x, y)`	The larger of two numbers.
`min(x, y)`	The smaller of two numbers.
`mode(k)`	Whether transport step k moves ions inside traps ("intra") or between them ("inter"). Only in a programme.
`motion(o)`	The waveform transport operation o needs: its movement class and, hop by hop, its direction -- along a loop as "+1"/"-1", on a spur as inward/outward, elsewhere as the lab-frame axis. Two ions with the same motion can ride one waveform. In a timed schedule: The class the paper's schedule records for the operation.
`rail(h)`	The rail hop h crosses. Only in a programme.
`replayed(c)`	The value the replay computes for what claim c is about. Only in a programme.
`setup_ok()`	Whether the execution's starting placement puts every ion in a site that exists, once.
`shift(h)`	How many slots along its loop hop h moves its ion, with a sign for the direction. Only in a programme.
`simultaneous(a, b)`	Whether operations a and b happen at the same time. In a programme: In the same step. In a timed schedule: Their time intervals overlap (an interval ends where the next may begin).
`site(o)`	Where operation o happens. For a gate, the site its ions stand in when it starts; none for transport and for operations on every ion at once.
`size(A)`	How many things set A holds.
`start(o)`	The instant operation o begins. In a programme: The instant before o's step.
`step(o)`	The step operation o belongs to. Only in a programme.
`swap_paid(o)`	Whether the reordering that brings split o's ion to the end of its chain was paid for. In a programme: The step records the gate swaps it pays. In a timed schedule: The split carries a reorder the paper's model charges.
`to(o)`	Where transport operation o (or hop o) leaves its ion.
`well_formed(o)`	Whether operation o names ions, sites and rails that exist and ends no earlier than it starts.

Instants and the state

`instants`	Every moment at which the state of the machine is judged. In a programme: The moment before each step, the moment during each step that moves ions, and the end. In a timed schedule: The start, and every time an operation begins or ends.
`final()`	The last instant of the execution, when everything is over.
`heat(i, t)`	Ion i's motional energy n̄ (in quanta) at instant t, under the device's heating model. Known at the start of every two-ion gate. Only in a programme.
`occupancy(x, t)`	How many ions are in site, junction or rail x at instant t. In a programme: During a step that moves ions, a site counts the ions that rest there before or after the step, whichever is more, plus every ion that passes through it: the programme does not order what happens inside a step, so nothing may be assumed to leave first. A rail counts the ions crossing it. In a timed schedule: An ion counts in a trap from the moment it starts to arrive until the moment it has left, and on a rail or in a junction while it is there.
`position(i, t)`	The site where ion i stands at instant t; none while it is in motion.

The input circuit

`circuit_ops`	The operations of the input circuit that the execution is judged against. In a programme: Every operation of the circuit. In a timed schedule: Its two-qubit gates: the only operations a paper's schedule names ions for.
`performers(c)`	The operations of the execution that carry out circuit operation c. In a programme: Every instruction the compiler stamped with c. In a timed schedule: The two-qubit gate matched to c: the k-th gate on a pair of ions is the circuit's k-th gate on that pair.
`computes_circuit()`	Whether the programme computes the input circuit: every gate of the circuit is performed once, in order, by its own ions, together in a trap that can gate, and the pulses fired compose to the circuit's operation. Only in a programme.
`first(c)`	The first operation that carries out circuit operation c.
`gate_count(c)`	How many two-qubit gates of the execution carry out circuit operation c.
`last(c)`	The last operation that carries out circuit operation c.
`needs_gate(c)`	Whether circuit operation c is a two-qubit gate, which the execution must perform once.
`next_on_qubit(c1, c2)`	Whether c2 is the operation that comes right after c1 on one of their qubits, in the circuit as written.
`next_run(c1, c2)`	Whether c2 belongs to the run of gates that follows c1's run on a qubit they share. A run is a stretch of consecutive CNOTs in which that qubit plays the same role -- always the control, or always the target -- and such gates commute with each other.
`performed(c)`	Whether some operation of the execution carries out circuit operation c.
`serves_circuit(o)`	Whether two-qubit gate o carries out some gate of the circuit.

The clock

`declares_duty_budget()`	Whether the device declares how much heat a gate zone may absorb over time (a duty-cycle budget). Only in a programme.
`gate_error_reads_heat()`	Whether the gate error the clock reports depends on the ions' heat when the gate starts, rather than being a constant. Only in a programme.
`heat_accrues_with_time()`	Whether the clock heats every ion for elapsed time, moving or not. Only in a programme.
`heat_is_upper_bound()`	Whether the heat figures the clock reports are upper bounds: heat from successive motions is added, and the interference that can make it smaller is not modelled. Only in a programme.
`models_heating()`	Whether the device's clock tracks how hot each ion gets. Only in a programme.

Rule sets

Each rule set names the rules it assumes and the numbers they read. The standard set is this website’s machine: every compiled programme and every leaderboard design is checked against it. Each paper’s set says what that paper’s model assumes, and each paper’s schedules, and ours beside them, are judged by it. Download a set to read it whole, or as the start of your own.

rule set	its rules	used for
This website's machine standard.rules	R0 R1 R2 R3 R4 R4b R4d R5 R6 R6b R7 R7b R7c R8 R9 R10 R11 R12 R13 R14 R15 R16 R17 R18 R19 R20 R21 R22 R23 R24 R25 Broadcast-controlled surface traps, as the compiler and the studio model them: every rule of the catalogue that is about a programme, a device drawing or the compiler's own claims. `max_chain = 15` — the most ions a gate's chain may hold (R13)	every programme this website compiles
QCCDSim qccdsim.rules	R0 R1 R2 R3 R6b R8 R14 R24 R25 R27 R29 The rules QCCDSim's scheduler enforces: a trap does one gate, split or merge at a time; a shuttle reserves its whole path, so a rail and a junction hold one ion at a time; a split takes the end ion of its chain or pays for a reorder (the reordered ion is lifted out where it stood); every operation lasts what QCCDSim's duration law says; each qubit's gates run in the circuit's order. `serial_kinds = {"gate2", "split", "merge"}` — the operation kinds that hold their trap one at a time (R27), named as kind(o) names them `chain_order = "qccdsim"` — how the order inside a chain is followed through a reorder before a split: "qccdsim" lifts the departing ion out where it stood, "physical" moves the end ion's state into its place (read by R14)	QCCDSim, Muzzle the Shuttle, Cyclone, Position Graph
QCCDSim, physical gate swap qccdsim-physical.rules	R0 R1 R2 R3 R6b R8 R14 R24 R25 R27 R29 QCCDSim's rules, except that a reorder before a split is a real gate swap: the end ion's state moves to where the departing ion stood, instead of the departing ion being lifted out in place. `serial_kinds = {"gate2", "split", "merge"}` — the operation kinds that hold their trap one at a time (R27), named as kind(o) names them `chain_order = "physical"` — how the order inside a chain is followed through a reorder before a split: "qccdsim" lifts the departing ion out where it stood, "physical" moves the end ion's state into its place (read by R14)	Muzzle the Shuttle
QCCDSim, gates as a set qccdsim-gateset.rules	R0 R1 R2 R3 R6b R8 R14 R24 R27 R29 QCCDSim's rules for benchmark files that list a round's CNOTs with no order between stabilisers: every gate must be performed, in any order. `serial_kinds = {"gate2", "split", "merge"}` — the operation kinds that hold their trap one at a time (R27), named as kind(o) names them `chain_order = "qccdsim"` — how the order inside a chain is followed through a reorder before a split: "qccdsim" lifts the departing ion out where it stood, "physical" moves the end ion's state into its place (read by R14)	Moveless
Cyclone cyclone.rules	R0 R1 R2 R3 R6b R8 R24 R26 R27 R29 A trap does one gate, split or merge at a time; a rail and a junction hold one ion at a time; the compiler keeps a list of ions per trap, not a chain, so no chain order is tracked; every operation lasts what Cyclone's duration law says; each qubit's gates run in the circuit's order, except that consecutive CNOTs in which it plays the same role may run in any order. `serial_kinds = {"gate2", "split", "merge"}` — the operation kinds that hold their trap one at a time (R27), named as kind(o) names them	Cyclone
Surface-code QCCD jones.rules	R0 R1 R2 R3 R6b R8 R14 R24 R26 R27 R29 R30 A trap does one operation of any kind at a time; a rail and a junction hold one ion at a time; a reorder before a split is a gate swap; operations that the schedule says hold the same component never overlap; every operation lasts what the paper's duration law says; each qubit's gates run in the circuit's order, except that consecutive CNOTs in which it plays the same role may run in any order. `serial_kinds = {"gate2", "gate1", "split", "merge", "swap", "measure", "reset"}` — the operation kinds that hold their trap one at a time (R27), named as kind(o) names them `chain_order = "physical"` — how the order inside a chain is followed through a reorder before a split: "qccdsim" lifts the departing ion out where it stood, "physical" moves the end ion's state into its place (read by R14)	Surface-code QCCD
TISCC tiscc.rules	R0 R1 R2 R8 R24 R29 R32 R33 One ion per zone, so a zone does not serialise its own operations; a junction is crossed by one ion at a time; rotations, preparation and measurement run only in operation (O) zones; the two-ion gate acts on ions in neighbouring zones of one rail; every gate of the circuit is performed, in any order; every operation lasts what TISCC's duration law says. `single_ion_zones = {"O"}` — the zones single-ion operations may run in (R32)	TISCC
TrapSIMD trapsimd.rules	R0 R1 R2 R8 R24 R26 R29 R31 R33 Transport between traps is broadcast: every such move of a cycle starts and ends together and is one class of move, and cycles never overlap; one ion per position, so no chain order is tracked; a junction holds one ion at a time; the two-ion gate acts on ions in a gate zone and a neighbouring one; every operation lasts what the paper's timing table says; each qubit's gates run in the circuit's order, except that consecutive CNOTs in which it plays the same role may run in any order. The paper's replay also checks its own model's control limits (which shifts and swaps a cycle may combine), beside these.	TrapSIMD
IonShuttler, exact router ionshuttler.rules	R0 R1 R2 R3 R8 R24 R25 R29 A rail and a junction hold one ion at a time; every operation lasts one time step of the paper's model; each qubit's gates run in the circuit's order. The paper's replay also checks its own model's rules about the processing zone, beside these.	MQT IonShuttler
IonShuttler, heuristic router ionshuttler-heuristic.rules	R0 R1 R8 R24 R25 R29 As the exact router's rules, except that the heuristic lets two chains pass the processing zone in one step, so rails and junctions are not held to one ion at a time here; the paper's replay checks its own rules about that zone instead.	MQT IonShuttler

Every rule

All 38 rules the website knows, each with the assertion the checker evaluates. Where a rule has examples, one programme that keeps it and one that breaks it are judged here by the standard rule set, and each opens as the page the studio would open on it.

R0 Every operation finds its ions where it says they arecore

setup_ok()
and (for all o in operations: well_formed(o) and found(o))
and (for all i in ions: position(i, final()) != none)

Each operation names its ions and where they are; replaying the execution from the start must find them there, and every ion must end it standing in a site.

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler ionshuttler-heuristic

R1 A site holds at most its capacitycore

for all s in sites, t in instants:
  occupancy(s, t) <= capacity(s)

An ion standing in a site, or passing through it, takes one of its places.

sources: the ion-transport deck (v3), arXiv:2004.04706, arXiv:2511.15910

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler ionshuttler-heuristic

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

the same hop into a site with room for it.

p.init({"d0": "C2", "d2": "C1"})
p.move("d2", "C1", "C2")

R1 holds

open the page, with its Report pane

fails

C2 already holds two ions, its capacity; a third arrives.

p.init({"d0": "C2", "d1": "C2", "d2": "C1"})
p.move("d2", "C1", "C2")

R1 failss = C2, t = during step 0: occupancy(s, t) is 3 and capacity(s) is 2

open the page, with its Report pane

R2 A junction holds one ion at a time

for all j in junctions, t in instants:
  occupancy(j, t) <= 1

Where three or more rails meet, only one ion may be at any moment, resting or passing through.

sources: the ion-transport deck (v3), arXiv:2510.23519

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler

examples on: two concentric loops: an inner data loop D (DT0–DT2, DB0–DB2; capacity 2, no gates) and an outer trap loop A (AT0–AT2, AB0–AB2), joined at x = 1 where DT1 and AT1 are degree-3 junctions

holds

one ion at the junction.

p.init({"d1": "DT0"})
p.move("d1", "DT0", "DT1")

R2 holdsthis programme also breaks R23

open the page, with its Report pane

fails

DT1 is where the coupling meets the inner loop, a degree-3 node; d0 is resting there when d1 arrives.

p.init({"d0": "DT1", "d1": "DT0"})
p.move("d1", "DT0", "DT1")

R2 failsj = DT1, t = during step 0: occupancy(j, t) is 2 and 1 is 1this programme also breaks R23

open the page, with its Report pane

R3 A rail carries at most its capacity

for all r in rails, t in instants:
  occupancy(r, t) <= capacity(r)

No more ions travel along one rail at once than the rail is built for (one, on most devices).

sources: the ion-transport deck (v3), arXiv:2510.23519

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones ionshuttler

examples on: an eight-site racetrack S0–S7: one closed loop L0 of trap sites (gates, SPAM, cooling; capacity 2) and no junctions, so every bend is ordinary transport

holds

the same two hops, one cycle each.

p.init({"d0": "S1", "d1": "S1"})
p.move("d0", "S1", "S2")
p.move("d1", "S1", "S2")

R3 holds

open the page, with its Report pane

fails

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"]])

R3 failsr = rail E1, t = during step 0: occupancy(r, t) is 2 and capacity(r) is 1

open the page, with its Report pane

R4 Every transport step uses a movement the device declares

for all k in steps where is_transport(k): class_declared(k)

A step's motion is one of the movement classes the device's control system is built to produce.

sources: the ion-transport deck (v3), arXiv:2504.17886

in the rule sets: standard

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

shuttle is declared.

p.init({"d0": "C1"})
p.move("d0", "C1", "C2", cls="shuttle")

R4 holds

open the page, with its Report pane

fails

no class named teleport exists on this device.

p.init({"d0": "C1"})
p.move("d0", "C1", "C2", cls="teleport")

R4 failsk = step 0 (instruction #1): class_declared(k) is false

open the page, with its Report pane

R4b A step either moves ions or gates them, never both

for all k in steps where is_transport(k):
  mode(k) in {"intra", "inter"} and not carries_gates(k)

Moving ions within traps and between them use different control pathways, and neither runs alongside gates.

sources: arXiv:2504.17886

in the rule sets: standard

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

transport and the gate as separate cycles, which is all the language can say.

p.init({"d0": "C0", "d1": "C0"})
p.cool()
p.move("d0", "C0", "C1")
p.move("d0", "C1", "C0")
p.gate("CX", [["d0", "d1"]])

R4b holdsthis programme also breaks R7

open the page, with its Report pane

fails

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": "C1", "d1": "C2"}, "quanta": {"d0": 0.0, "d1": 0.0}}
{"type": "simd", "id": 1, "cls": "shuttle", "mode": "inter", "participants": [{"ion": "d0", "src": "C1", "dst": "C0", "via": []}], "gate": "CX", "pairs": [["d0", "d1"]]}

R4b failsk = step 0 (instruction #1): carries_gates(k) holds

open the page, with its Report pane

R4d The control channels can drive every transport step

for all k in steps where is_transport(k): drivable(k)

One channel carries one waveform: every ion a channel moves must move the same way, and a site may sit a step out only if it has its own switch.

sources: the ion-transport deck (v3), arXiv:2403.00756, arXiv:2305.03828

in the rule sets: standard

examples on: an eight-site racetrack S0–S7: one closed loop L0 of trap sites (gates, SPAM, cooling; capacity 2) and no junctions, so every bend is ordinary transport

holds

both hop one slot the same way round: one waveform does it.

p.init({"d0": "S0", "d1": "S4"})
p.simd("shuttle", [["d0", "S0", "S1"], ["d1", "S4", "S5"]])

R4d holds

open the page, with its Report pane

fails

one waveform drives the racetrack, and the two ions ask it to move opposite ways at once.

p.init({"d0": "S0", "d1": "S4"})
p.simd("shuttle", [["d0", "S0", "S1"], ["d1", "S4", "S3"]])

R4d failsk = step 0 (instruction #1): drivable(k) is falsethis programme also breaks R11, R22

open the page, with its Report pane

R5 No two ions swap places along one rail in one step

for all a, b in hops where simultaneous(a, b) and rail(a) = rail(b):
  not (from(a) = to(b) and to(a) = from(b))

Two ions cannot pass each other on a rail.

sources: the ion-transport deck (v3)

in the rule sets: standard

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

the same swap in two cycles, resting together at C2 in between.

p.init({"d0": "C1", "d1": "C2"})
p.move("d0", "C1", "C2")
p.move("d1", "C2", "C1")

R5 holds

open the page, with its Report pane

fails

d0 and d1 swap across the C1–C2 segment. An exchange also breaks R3 and the channel clause of R4: one segment, two ions, two directions, one waveform.

p.init({"d0": "C1", "d1": "C2"})
p.simd("shuttle", [["d0", "C1", "C2"], ["d1", "C2", "C1"]])

R5 failsa = ion d0 C1→C2 (move d0 C1→C2, step 0), b = ion d1 C2→C1 (move d1 C2→C1, step 0): from(a) = to(b) and to(a) = from(b) holdsa = ion d1 C2→C1 (move d1 C2→C1, step 0), b = ion d0 C1→C2 (move d0 C1→C2, step 0): from(a) = to(b) and to(a) = from(b) holdsthis programme also breaks R3, R4d, R11, R22

open the page, with its Report pane

R6 Each operation runs only where the site is equipped for it

(for all g in gates: can(site(g), "gate"))
and (for all o in operations where kind(o) in {"measure", "reset"}: can(site(o), "spam"))
and (for all c in coolings, i in ions(c): can(position(i, start(c)), "cool"))

Gates only in sites with a gate laser, measurement and reset only where there is readout, cooling only where there is a cooling beam.

sources: the ion-transport deck (v3), arXiv:2504.17886

in the rule sets: standard

holds

AT0 on the outer loop is a trap site: gates, SPAM and cooling allowed.

p.init({"d0": "AT0", "d1": "AT0"})
p.cool()
p.gate("CX", [["d0", "d1"]])

R6 holds

open the page, with its Report pane

fails

DT0 is a data site on the inner loop: capacity 2, gate=false.

p.init({"d0": "DT0", "d1": "DT0"})
p.cool()
p.gate("CX", [["d0", "d1"]])

R6 failsg = CX d0,d1 at DT0, step 1: can(site(g), "gate") is false

open the page, with its Report pane

R6b A two-ion gate acts on two ions standing in one site

(for all g in two_qubit_gates, i in ions(g): position(i, start(g)) = site(g))
and (for all g in two_qubit_gates where size(declared_sites(g)) > 0:
       site(g) in declared_sites(g))

Both ions of a two-qubit gate are in the same trap when it starts, and in the trap the programme names for it, if it names one.

sources: arXiv:2504.17886

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

both ions at C0.

p.init({"d0": "C0", "d1": "C0"})
p.cool()
p.gate("CX", [["d0", "d1"]])

R6b holds

open the page, with its Report pane

fails

d1 is still at C1, one site over, when the gate at C0 fires.

p.init({"d0": "C0", "d1": "C1"})
p.cool()
p.gate("CX", [["d0", "d1"]], ["C0"])

R6b failsg = CX d0,d1 at C0, step 1, i = ion d1: position(i, start(g)) is C1 and site(g) is C0

open the page, with its Report pane

R7 A two-ion gate starts with cool enough ions

for all g in two_qubit_gates, i in ions(g):
  heat(i, start(g)) <= heat_budget()

Both ions' motional energy at the start of a two-qubit gate is within the device's budget; a cooling operation must come first otherwise.

sources: the ion-transport deck (v3), arXiv:2511.15910

in the rule sets: standard

examples on: a 2×3 lattice: six lattice nodes, of which J0_1 and J1_1 are degree-3 T-junctions and the other four degree-2 corners, with one trap site (T…) on every wire between them

holds

the same walk, cooled after it.

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])
p.cool()
p.gate("CX", [["d0", "d1"]])

R7 holds

open the page, with its Report pane

fails

d0 is cooled, then walks through the T-junction J0_1 (3 quanta) and meets the gate hot.

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.cool()
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])
p.gate("CX", [["d0", "d1"]])

R7 failsg = CX d0,d1 at T0_1h, step 2, i = ion d0: heat(i, start(g)) is 9.20925 and heat_budget() is 1

open the page, with its Report pane

R7b A gate zone stays within its heat duty cycle

when declares_duty_budget():
for all s in sites: duty(s) <= duty_budget(s)

A gate zone may absorb only so much heat over time; no device declares such a budget yet.

sources: arXiv:2504.17886

in the rule sets: standard

examples on: an eight-site racetrack S0–S7: one closed loop L0 of trap sites (gates, SPAM, cooling; capacity 2) and no junctions, so every bend is ordinary transport

does not apply

three gates in a row in one site: the verdict is skipped, not passed.

p.init({"d0": "S0", "d1": "S0"})
p.cool()
p.gate("CX", [["d0", "d1"]])
p.gate("CX", [["d1", "d0"]])
p.gate("CX", [["d0", "d1"]])

R7b does not applyit applies only when declares_duty_budget()

open the page, with its Report pane

R7c A programme with two-ion gates cools

when models_heating():
count(two_qubit_gates) = 0 or count(coolings) > 0

Under broadcast wiring cooling is not optional: a programme that gates and never cools cannot reach a useful error rate.

sources: arXiv:2510.23519, arXiv:2606.06455

in the rule sets: standard

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

one broadcast cool.

p.init({"d0": "C0", "d1": "C0"})
p.cool()
p.gate("CX", [["d0", "d1"]])

R7c holds

open the page, with its Report pane

fails

a gate and no cooling operation anywhere in the programme.

p.init({"d0": "C0", "d1": "C0"})
p.gate("CX", [["d0", "d1"]])

R7c failscount(coolings) is 0 and 0 is 0

open the page, with its Report pane

R8 An ion does one thing at a timecore

for all a, b in operations where a != b and simultaneous(a, b):
  disjoint(ions(a), ions(b))

No ion takes part in two operations at once: it cannot be gated in one place while it is carried to another.

sources: the ion-transport deck (v3)

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler ionshuttler-heuristic

examples on: an eight-site racetrack S0–S7: one closed loop L0 of trap sites (gates, SPAM, cooling; capacity 2) and no junctions, so every bend is ordinary transport

holds

two different ions.

p.init({"d0": "S1", "d1": "S4"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S4", "S5"]])

R8 holds

open the page, with its Report pane

fails

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"]])

R8 failsa = move d0 S1→S2, step 0, b = move d0 S1→S2, step 0: disjoint(ions(a), ions(b)) is falsea = move d0 S1→S2, step 0, b = move d0 S1→S2, step 0: disjoint(ions(a), ions(b)) is falsethis programme also breaks R3

open the page, with its Report pane

R9 The programme's figures are the replay's figures

for all c in claims: approx(claimed(c), replayed(c))

Every time, cost, step count or heat figure the programme states about itself equals what replaying it computes.

in the rule sets: standard

examples on: a 2×3 lattice: six lattice nodes, of which J0_1 and J1_1 are degree-3 T-junctions and the other four degree-2 corners, with one trap site (T…) on every wire between them

holds

the true totals.

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])
p.cool()
p.gate("CX", [["d0", "d1"]])
p.claim(total_steps=5, total_cost=4)

R9 holds

open the page, with its Report pane

fails

the programme claims 3 steps and cost 2; the replay finds 5 and 4 (the walk is two rails, a junction and the merge into d1's trap).

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])
p.cool()
p.gate("CX", [["d0", "d1"]])
p.claim(total_steps=3, total_cost=2)

R9 failsc = the claimed total_cost: claimed(c) is 2 and replayed(c) is 4c = the claimed total_steps: claimed(c) is 3 and replayed(c) is 5

open the page, with its Report pane

R10 The programme computes the circuit

computes_circuit()

The pulses the programme fires, read through which ion plays which qubit, compose to the circuit's operation; every gate is performed once, by its own ions, together in a trap that can gate.

sources: this website, arXiv:2406.19479

in the rule sets: standard

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

does not apply

a gate with no circuit to check it against: skipped, with the reason.

p.init({"d0": "C1", "d1": "C0"})
p.shuttle("d0", ["C1", "C0"])
p.cool()
p.gate("CX", [["d0", "d1"]])

R10 does not applyno proof of what the programme computes was given with it

open the page, with its Report pane

R11 Along a loop, every ion moves the same way in a step

(for all a, b in hops where simultaneous(a, b) and loop(a) = loop(b) and loop(a) != none:
   shift(a) = shift(b))
and (for all j in junctions: priced(j))

Transport along one loop is one direction at a time; and every junction's crossing time is declared by the device.

sources: arXiv:2511.15910

in the rule sets: standard

examples on: an eight-site racetrack S0–S7: one closed loop L0 of trap sites (gates, SPAM, cooling; capacity 2) and no junctions, so every bend is ordinary transport

holds

both the same way.

p.init({"d0": "S1", "d1": "S5"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S5", "S6"]])

R11 holds

open the page, with its Report pane

fails

d0 goes one way round the racetrack, d1 the other, in one cycle (R4's channel clause fires too).

p.init({"d0": "S1", "d1": "S5"})
p.simd("shuttle", [["d0", "S1", "S2"], ["d1", "S5", "S4"]])

R11 failsa = ion d0 S1→S2 (move d0 S1→S2, step 0), b = ion d1 S5→S4 (move d1 S5→S4, step 0): shift(a) is 1 and shift(b) is -1this programme also breaks R4d, R22

open the page, with its Report pane

R12 One gate at a time in a trap

for all a, b in gates where a != b and simultaneous(a, b):
  site(a) != site(b)

A trap's laser serves one gate at a time; different traps may gate together.

sources: arXiv:2511.15910, arXiv:2004.04706

in the rule sets: standard

examples on: two wide traps C0 and C1 in a line, zone `big`: capacity 32, gates allowed

holds

the two pairs in two traps: inter-trap parallelism is free.

p.init({"d0": "C0", "d1": "C0", "d2": "C1", "d3": "C1"})
p.cool()
p.gate("CX", [["d0", "d1"], ["d2", "d3"]])

R12 holds

open the page, with its Report pane

fails

two pairs gated in C0 at once.

p.init({"d0": "C0", "d1": "C0", "d2": "C0", "d3": "C0"})
p.cool()
p.gate("CX", [["d0", "d1"], ["d2", "d3"]])

R12 failsa = CX d0,d1 at C0, step 1, b = CX d2,d3 at C0, step 1: site(a) is C0 and site(b) is C0a = CX d2,d3 at C0, step 1, b = CX d0,d1 at C0, step 1: site(a) is C0 and site(b) is C0

open the page, with its Report pane

R13 A gate's chain holds at most max_chain ions

for all g in gates: occupancy(site(g), start(g)) <= max_chain

A gate in a chain longer than about fifteen ions is slow and poor, so no gate starts in a site holding more.

sources: arXiv:2511.15910, arXiv:2004.04706

in the rule sets: standard

examples on: two wide traps C0 and C1 in a line, zone `big`: capacity 32, gates allowed

holds

fifteen.

p.init({"d0": "C0", "d1": "C0", "d2": "C0", "d3": "C0", "d4": "C0", "d5": "C0", "d6": "C0", "d7": "C0", "d8": "C0", "d9": "C0", "d10": "C0", "d11": "C0", "d12": "C0", "d13": "C0", "d14": "C0"})
p.cool()
p.gate("CX", [["d0", "d1"]])

R13 holds

open the page, with its Report pane

fails

a chain of 17 in C0 when the gate fires.

p.init({"d0": "C0", "d1": "C0", "d2": "C0", "d3": "C0", "d4": "C0", "d5": "C0", "d6": "C0", "d7": "C0", "d8": "C0", "d9": "C0", "d10": "C0", "d11": "C0", "d12": "C0", "d13": "C0", "d14": "C0", "d15": "C0", "d16": "C0"})
p.cool()
p.gate("CX", [["d0", "d1"]])

R13 failsg = CX d0,d1 at C0, step 1: occupancy(site(g), start(g)) is 17 and max_chain is 15

open the page, with its Report pane

R14 A split takes the ion at the end of its chain, or pays to reorder

for all m in splits: at_chain_end(m) or swap_paid(m)

An ion leaves its chain from the end that faces the rail; an ion further in must first be swapped to that end, which costs gates.

sources: arXiv:2510.23519

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset jones

examples on: the six-site ring with load-zone spur ends (capacity 8, no gates)

holds

from a chain of two every ion is at an edge.

p.init({"d0": "A0", "d1": "A0"})
p.move("d0", "A0", "S0", cls="dock")

R14 holdsthis programme also breaks R23

open the page, with its Report pane

fails

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")

R14 failsm = move d0 A0→S0, step 0: at_chain_end(m) is false, and swap_paid(m) is falsethis programme also breaks R23

open the page, with its Report pane

R15 Heat figures are upper bounds

when models_heating():
heat_is_upper_bound()

The heat from successive motions can interfere and partly cancel; the clock adds it up instead, so every heat figure is an upper bound.

sources: arXiv:2605.25118

in the rule sets: standard

holds

a walk from the data loop through the coupling to the trap loop: the reported n̄ is an upper bound, and R15 says so.

p.init({"d0": "DT0"})
p.shuttle("d0", ["DT0", "DT1", "AT1"])
p.cool()

R15 holdsthis programme also breaks R23

open the page, with its Report pane

R16 Gate error depends on the ions' heat

when models_heating():
gate_error_reads_heat()

The error of a two-qubit gate is computed from how hot its ions are when it starts, not taken as a constant.

sources: arXiv:2510.23519, arXiv:2605.25118

in the rule sets: standard

examples on: a 2×3 lattice: six lattice nodes, of which J0_1 and J1_1 are degree-3 T-junctions and the other four degree-2 corners, with one trap site (T…) on every wire between them

holds

cooled first: the error read off n̄ ≈ 0.

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])
p.cool()
p.gate("CX", [["d0", "d1"]])

R16 holds

open the page, with its Report pane

holds

the gate on a hot ion: the error read off n̄ ≈ 3.2, what the T-junction cost it (R7 fires for the same reason).

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.cool()
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])
p.gate("CX", [["d0", "d1"]])

R16 holdsthis programme also breaks R7

open the page, with its Report pane

R17 Ions heat with elapsed time, moving or not

when models_heating():
heat_accrues_with_time()

Background heating accrues with time for every ion, whether or not it moves.

sources: arXiv:2605.25118

in the rule sets: standard

examples on: a four-site linear register C0–C3: every site a trap (gates, SPAM, cooling; capacity 2), two open ends, no junctions and no loop

holds

under the corrected model d1 never moves and still heats while d0 walks: its anomalous quanta are listed below.

p.init({"d0": "C0", "d1": "C3"})
p.shuttle("d0", ["C0", "C1", "C2"])
p.cool()

R17 holds

open the page, with its Report pane

does not apply

under the deck's cost model there is no clock, so R17 is skipped with that reason.

p.init({"d0": "C0", "d1": "C3"})
p.shuttle("d0", ["C0", "C1", "C2"])
p.cool()

R17 does not applyit applies only when models_heating()

open the page, with its Report pane

R18 A junction is where three or more rails meet

for all n in nodes: (n in junctions) = (degree(n) >= 3)

Whatever a node is called, it is a junction exactly when three or more rails meet at it, and crossing it is priced by that number.

sources: arXiv:quant-ph/0702175, arXiv:2305.03828, arXiv:1210.3655

in the rule sets: standard

examples on: a 2×3 lattice: six lattice nodes, of which J0_1 and J1_1 are degree-3 T-junctions and the other four degree-2 corners, with one trap site (T…) on every wire between them

bend

T0_0v → J0_0 → T0_0h transits the corner J0_0, where only two wires meet: a bend, priced as plain transport.

p.init({"d0": "T0_0v"})
p.shuttle("d0", ["T0_0v", "J0_0", "T0_0h"])

R18 holds

open the page, with its Report pane

junction

T0_0v → J0_1 → T0_1h transits J0_1, where three wires meet: a junction_cross charged at degree 3.

p.init({"d0": "T0_0v"})
p.shuttle("d0", ["T0_0v", "J0_1", "T0_1h"])

R18 holds

open the page, with its Report pane

R19 A junction joins at most max_junction_degree() rails

for all n in nodes: degree(n) <= max_junction_degree()

A surface trap has T- and X-junctions and nothing denser, unless the device declares otherwise.

sources: collaborators' review, September 2026, arXiv:2201.12579

in the rule sets: standard

examples on: four rails meeting at one node J at right angles: an X-junction, degree 4

holds

J joins four rails at right angles: an X-junction.

device: four rails meeting at one node J at right angles: an X-junction, degree 4

p.init({"d0": "N"})

R19 holds

open the page, with its Report pane

fails

J joins five rails. Where a fifth rail would go there is no room for its RF electrodes on a plane.

device: five rails meeting at one node J: a degree-5 junction, which no 2D surface trap has

p.init({"d0": "N"})

R19 failsn = J: degree(n) is 5 and max_junction_degree() is 4this programme also breaks R11, R20

open the page, with its Report pane

R20 Rails meet at a wide enough angle

for all n in nodes, r1, r2 in rails_at(n) where r1 != r2:
  angle(n, r1, r2) >= min_rail_angle()

Any two rails meeting at a node make at least the device's minimum angle (60 degrees unless it declares another).

sources: collaborators' review, September 2026, arXiv:2201.12579

in the rule sets: standard

examples on: the same fork drawn as a T-junction: the branches leave J 90 degrees apart

holds

the same fork as a T: 90 degrees between the branches.

device: the same fork drawn as a T-junction: the branches leave J 90 degrees apart

p.init({"d0": "W"})

R20 holds

open the page, with its Report pane

fails

the branches to A and B leave J 30 degrees apart: their RF rails would overlap before the ion could tell them apart.

device: a fork whose two branches leave J only 30 degrees apart

p.init({"d0": "W"})

R20 failsn = J, r1 = rail rA, r2 = rail rB: angle(n, r1, r2) is 30.0007 and min_rail_angle() is 60n = J, r1 = rail rB, r2 = rail rA: angle(n, r1, r2) is 30.0007 and min_rail_angle() is 60

open the page, with its Report pane

R21 Rails lie in a plane

(for all r in rails, n in nodes: not lies_on(n, r))
and (for all r1, r2 in rails where r1 < r2: not cross(r1, r2))

A rail meets only the nodes it ends at, and two rails cross only at a node they share: the drawing must be a surface trap.

sources: collaborators' review, September 2026, arXiv:quant-ph/0702175

in the rule sets: standard

examples on: the same four sites joined through a junction J where the rails meet

holds

the same four sites joined through a junction J, so the rails meet only where the graph says they do.

device: the same four sites joined through a junction J where the rails meet

p.init({"d0": "A"})

R21 holds

open the page, with its Report pane

fails

the rail A-B and the rail C-D cross at the origin, where there is no node: two RF nulls through the same point, no junction.

device: two rails drawn across each other with no node where they meet

p.init({"d0": "A"})

R21 failsr1 = rail rAB, r2 = rail rCD: cross(r1, r2) holds

open the page, with its Report pane

R22 A transport step is one waveform

when control() != "direct":
for all a, b in transport where simultaneous(a, b):
  motion(a) = motion(b)

Under broadcast control every ion that moves in a step performs the exact same motion; a site may sit the step out, never do something else.

sources: collaborators' review, September 2026, arXiv:2510.23519, arXiv:2305.12773

in the rule sets: standard

examples on: a 2×3 lattice: six lattice nodes, of which J0_1 and J1_1 are degree-3 T-junctions and the other four degree-2 corners, with one trap site (T…) on every wire between them

holds

both walk north through their own T-junction: one motion, one waveform.

p.init({"d0": "T0_0v", "d1": "T1_0v"})
p.simd("shuttle", [["d0", "T0_0v", "T0_1v", ["T0_0v.b", "T0_1v.a"]], ["d1", "T1_0v", "T1_1v", ["T1_0v.b", "T1_1v.a"]]])

R22 holds

open the page, with its Report pane

fails

d0 walks north through J0_1 while d1 walks east then north through J1_1: two motions, so two waveforms, in one cycle.

p.init({"d0": "T0_0v", "d1": "T0_1h"})
p.simd("shuttle", [["d0", "T0_0v", "T0_1v", ["T0_0v.b", "T0_1v.a"]], ["d1", "T0_1h", "T1_1v", ["T0_1h.b", "T1_1v.a"]]])

R22 failsa = move d0 T0_0v→T0_1v, step 0, b = move d1 T0_1h→T1_1v, step 0: motion(a) is shuttle +y,+y and motion(b) is shuttle +x,+y

open the page, with its Report pane

R23 A junction is crossed, not rested on

when count(ions) <= sum(min(capacity(s), max_chain) for s in sites where s not in junctions):
for all i in ions, t in instants:
  position(i, t) in junctions implies rotated(position(i, t))

No ion stops where three or more rails meet while the traps elsewhere have room for every ion. A slot of a loop or rail the programme moves as a whole is part of a conveyor, and is not such a stop.

sources: a reader's report, September 2026, the ion-transport deck (v3), arXiv:2510.23519

in the rule sets: standard

examples on: 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

holds

the same ion crosses S0 in one move and comes to rest in the dock A0.

p.init({"d0": "S1"})
p.simd("shuttle", [["d0", "S1", "A0", ["E0", "V0"]]])

R23 holds

open the page, with its Report pane

fails

d0 stops on S0, where the loop and the spur to A0 meet, with five empty traps around it.

p.init({"d0": "S1"})
p.move("d0", "S1", "S0")

R23 failsi = ion d0, t = after step 0: rotated(position(i, t)) is false

open the page, with its Report pane

R24 Every two-qubit gate of the circuit is performed, and no othercore

(for all c in circuit_ops where needs_gate(c): gate_count(c) >= 1)
and (for all g in two_qubit_gates: serves_circuit(g))

Each two-qubit gate of the input circuit is carried out, and the execution performs no two-qubit gate the circuit does not ask for.

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler ionshuttler-heuristic

R25 Each qubit's operations keep the circuit's order

for all c1, c2 in circuit_ops where next_on_qubit(c1, c2) and performed(c1) and performed(c2):
  end(last(c1)) <= start(first(c2))

On every qubit, each operation is over before the next one on that qubit begins, in the order the circuit is written -- even where two of them would commute.

in the rule sets: standard qccdsim qccdsim-physical ionshuttler ionshuttler-heuristic

R26 Each qubit's gates keep the circuit's order, up to commuting CNOTs

for all c1, c2 in circuit_ops where next_run(c1, c2) and performed(c1) and performed(c2):
  end(last(c1)) <= start(first(c2))

As R25, except that consecutive CNOTs in which a qubit plays the same role (always the control, or always the target) commute, and may run in any order among themselves.

in the rule sets: cyclone jones trapsimd

R27 One operation at a time in a trap

for all a, b in operations where a != b and kind(a) in serial_kinds and kind(b) in serial_kinds
    and site(a) = site(b) and site(a) != none:
  not simultaneous(a, b)

The operations of the kinds listed in serial_kinds hold their trap: two of them in one trap never overlap in time.

in the rule sets: qccdsim qccdsim-physical qccdsim-gateset cyclone jones

R29 Every operation lasts what the clock says

for all o in operations where clocked(o): approx(duration(o), clock(o))

Each operation's duration is the one the model's duration law gives it.

in the rule sets: qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler ionshuttler-heuristic

R30 Operations that hold the same component never overlap

for all a, b in operations where a != b and simultaneous(a, b):
  disjoint(locks(a), locks(b))

The schedule states, for every operation, the components it holds while it runs; two operations naming one component never overlap in time.

in the rule sets: jones

R31 Broadcast transport moves in lockstep

(for all a in operations where kind(a) = "hop": motion(a) != none)
and (for all a, b in operations where kind(a) = "hop" and kind(b) = "hop" and a != b
       and simultaneous(a, b):
     start(a) = start(b) and end(a) = end(b) and motion(a) = motion(b))

One waveform drives every broadcast move of a cycle: moves that overlap start and end together and are of one class, and every such move names its class.

in the rule sets: trapsimd

R32 Single-ion operations run only in the zones the model allows

for all o in operations where kind(o) in {"gate1", "reset", "measure"}:
  zone(site(o)) in single_ion_zones

Rotations, preparation and measurement happen only in the zones listed in single_ion_zones.

in the rule sets: tiscc

R33 A two-ion gate acts on ions in one zone or in neighbouring zones

for all g in two_qubit_gates, i, j in ions(g):
  position(i, start(g)) = position(j, start(g))
  or neighbours(position(i, start(g)), position(j, start(g)))

On devices whose gate spans two zones of one rail, the two ions stand in the same zone or in zones next to each other.

in the rule sets: tiscc trapsimd

One level up: the machine

A fault-tolerant machine is built from places -- each a small device whose every op is checked by the rules above, then used as a box with doors -- joined by roads that carry bundles of ions and wires that carry bits. Where the places stand is its floorplan, and a logical program run on it is a schedule of ops at places and bundles on roads, many at once. The same language judges both, with its own words. The floorplan rules (F) hold before any program runs; the schedule rules (G) hold on every run, and two of them, G5 and G13, are why work may run in parallel: a place does one op at a time and a road carries one bundle at a time, so whatever runs at once holds different things. The gadget design pages show every one of these rules, decided, beside the machine they judge.

Words about a floorplan

`depots`	The ion depots: where fresh ions are loaded and used ones are dumped.
`doors`	Every port of every placed gadget, junction arms included.
`owners(r)`	The places (or junctions) whose doors road r ends at.
`placed`	Every placed gadget, junctions included.
`places`	Every placed gadget of the machine that is not a junction: the places blocks are brought to, the depots, the decoder and the classical memory.
`roads`	Every conveyor road between two doors: a channel bundles of ions travel along.
`wires`	Every classical link: it carries bits from one door to another, never ions.
`classical(x)`	Whether place x (or the place activity x happens at) holds no ions: the decoder and the classical memory, whose ops are modeled.
`code(d)`	The code whose data ions door d carries, or none if it does not say.
`crosses(r1, r2)`	Whether the routes of roads r1 and r2 meet anywhere: two roads may only meet at a junction, through its arms.
`dir(d)`	Which way door d is crossed: "in", "out" or "inout".
`family(x)`	What place x is (or the place door, or activity, x belongs to): "prep", "se", "operation", "surgery", "readout", "zone", "factory", "injection", "depot", "decoder", "archive", or "road" for a junction.
`home_region(f)`	The region a place of family f belongs in: a zone in memory; preparation, syndrome extraction, transversal gates, lattice surgery and readout in compute; factories and injection in factory; depots in supply; the decoder and the classical memory in control; junctions in traffic.
`latency(w)`	How long a bit takes to cross wire w.
`length(r)`	How many sites road r has: its route length less one.
`medium(d)`	What crosses door d: "ions" or "bits".
`overlaps(p, q)`	Whether the footprints of places p and q overlap (touching along an edge is not overlapping).
`owner(d)`	The place (or junction) door d belongs to.
`passes_through(r, p)`	Whether road r's route runs through the inside of place p's footprint.
`reachable(a, b)`	Whether a bundle leaving door a can reach door b along roads, crossing junctions (places are endpoints, never thoroughfares).
`region(p)`	The region the floorplan puts place p in: "memory", "compute", "factory", "supply", "control", or "traffic" for a junction.
`role(d)`	What the ions crossing door d are for: "data" (a block's data ions), "magic" (a resource state), "fresh", "messenger", or "any".
`signal(d)`	What the bits crossing door d mean: "syndrome", "outcome", "frame", "decision", or "any"; none for a door of ions.
`width(d)`	How many ions cross door d in one bundle.

Words about a program scheduled on it

`blocks`	The logical blocks of the program: each a bundle of ions holding one encoded qubit.
`carries`	Every bundle carried along a road: from the first ion leaving one door to the last taken in at the other end.
`decisions(e)`	The decision messages that tell classically controlled op e's place whether to run it.
`decode_jobs`	Every decoding job the decoder runs.
`events`	Every op the machine runs at a place: a place's op, a junction passing a bundle, a job at the decoder or the classical memory.
`frame_rows`	Every line written into the classical memory: an outcome recorded, a frame updated, a guard resolved.
`guarded`	Every classically controlled op: it runs only when a condition on measured outcomes holds.
`handoffs`	Every time an ion changes hands: loaded at a depot, leaving a place onto a road, or arriving from a road into a place.
`instructions`	The instructions of the logical program.
`intakes`	Every bundle an op takes in through one of its doors.
`living`	The ions of the blocks still alive when the program ends (never read out).
`loaded`	The ions loaded at a depot while the program runs.
`messages`	Every burst of bits sent along a wire.
`named(x)`	The events whose measurements frame row or outcome x is a parity of.
`outcomes`	Every logical measurement result the classical memory records.
`reads(x)`	The decoded windows holding the outcomes classically controlled op x's guard (or guarded frame row x's condition) reads.
`residents`	The ions that live in places from the start (ancillas, a surgery seam, a factory's staff).
`sends(w)`	The syndrome messages that carry window w from the place that measured it to the decoder.
`windows`	Every syndrome window: the check outcomes one op measured, waiting in its place's readout buffer until a `decode` sends them.
`at(x)`	When frame row x was written, or outcome x recorded.
`before(h)`	The instant just before handoff h.
`begins(i)`	When the first op on ions of instruction i starts.
`connects(w, m)`	Whether wire w runs between the two doors message m goes from and to.
`crowd(c)`	The most ions of carry c on its road at one moment: each is on it from when it leaves until it is taken in at the far end, travelling or stopped.
`decoded(w)`	Whether some `decode` instruction sent window w to the decoder.
`decoder_present()`	Whether the floorplan has a decoder.
`delivered_by(k)`	The carry that brings intake k's bundle to its door (arriving when the op's own replay takes its first ion in), or none.
`destination(x)`	Where carry or message x ends: the place it reaches.
`exit_heat(e)`	The hottest a bundle leaves event e's place, as the op's replay measured it (0 if no ion leaves).
`expected(k)`	The ions intake k's op takes in, in the order its verified program takes them.
`finishes(i)`	When the last op on ions of instruction i ends.
`held(m)`	Whether message m is a syndrome a `decode` instruction sent out of the readout buffer it waited in (the one kind of bits that may leave after the op that measured them).
`home(i)`	Where resident ion i lives.
`instruction(x)`	The instruction activity x is part of.
`ion(h)`	The ion handoff h moves.
`ion_loss_limit()`	The hottest an ion may get before it is likely lost: about 85 uncooled junction round trips (arXiv:1210.3655), at 3 quanta a transit.
`ion_sites(c)`	How much shuttling carry c is: its ions times the sites of its road.
`location(i, t)`	The place or road holding ion i at instant t; none before it is loaded.
`logic_failed(e)`	Whether the logic check of the op event e runs failed (its flows or its fault distance).
`longest_gap(b)`	The longest time block b spends, from its birth to its readout (or the end), with none of its ions in an op that extracts syndromes (preparation, a syndrome round, lattice surgery, injection).
`measured(w)`	When window w's bits exist: the last measurement of the op that measured them.
`measured_by(m)`	The op whose measurement made message m's bits, or none.
`next_on_block(i, j)`	Whether j is the next instruction after i, in program order, that acts on the ions of a block i acts on (instructions that move no ion -- a decode, a Pauli kept in software -- are skipped).
`next_syndrome(j)`	The first syndrome to reach the decoder after the one job j works on, or none.
`order(c)`	The ions of carry c in the order they travel.
`origin(x)`	Where carry or message x starts: the place it leaves.
`peak_heat(e)`	The hottest any ion gets inside the op event e runs, as its replay measured it.
`place(x)`	Where activity x happens (an op, a pass, a classical job).
`ready(e)`	When the guard of classically controlled op e was resolved and at its place's door, as the scheduler says.
`realised(i)`	Whether some event of the machine carries out instruction i (a Pauli kept in software is carried out by the classical memory).
`refused(i)`	Whether the scheduler refused instruction i (and why is said with it).
`road(c)`	The road carry c travels along.
`status(e)`	The verification status of the op event e runs: "verified", "certified", "modeled" or "failed" (the reporting contract of the place library).
`syndrome_of(j)`	The syndrome decoding job j works on: the earliest one its own instruction sent that no earlier job has taken.
`traffic()`	How much shuttling the whole execution is: the sum of ion_sites over every carry.
`wait(c)`	How long the last ion of carry c waits at the far end of its road before it is taken in.
`waits(c)`	Whether some ion of carry c is taken in at the far end later than it gets there: the bundle waited on road c.
`wire(m)`	The wire message m crosses, or none if the floorplan has no such wire.
`written(w)`	When the decoder's correction for window w was written into the classical memory; none if it never was.

A floorplan's rules floorplan.rules

Places, junctions, roads and wires, judged before any program is scheduled: what any floorplan must respect, whoever drew it.

F1 A road or a wire joins two doors that agreecore

(for all r in roads, a in ends(r), b in ends(r) where a != b:
   medium(a) = medium(b)
   and (role(a) = role(b) or role(a) = "any" or role(b) = "any")
   and (role(a) != "data" or role(b) != "data" or
        (width(a) = width(b) and (code(a) = none or code(b) = none or code(a) = code(b))))
   and (dir(a) != dir(b) or dir(a) = "inout"))
and (for all w in wires, a in ends(w), b in ends(w) where a != b:
   medium(a) = medium(b)
   and (signal(a) = signal(b) or signal(a) = "any" or signal(b) = "any")
   and (dir(a) != dir(b) or dir(a) = "inout"))

Both ends carry the same thing -- ions of the same role, width and code, or bits of the same signal -- and they face opposite ways.

F2 Every door of a place is on one road, and a junction arm on one at mostcore

(for all d in doors where medium(d) = "ions" and family(owner(d)) != "road":
   count(r in roads where d in ends(r)) = 1)
and (for all d in doors where family(owner(d)) = "road":
   count(r in roads where d in ends(r)) <= 1)

A place's ions come and go through its doors, so each door is on exactly one road; a junction's arm is on at most one.

F3 Footprints do not overlapcore

for all p, q in placed where p != q: not overlaps(p, q)

No two places (or junctions) stand on the same piece of the chip.

F4 Roads meet only at junctionscore

(for all r in roads, p in placed where p not in owners(r): not passes_through(r, p))
and (for all r1, r2 in roads where r1 != r2: not crosses(r1, r2))

A road runs through no place it does not serve, and two roads never cross or touch: where roads meet, there is a junction, and they meet it through its arms.

F5 A bundle can wait in front of every door

for all r in roads, d in ends(r) where family(owner(d)) != "road":
  length(r) >= width(d)

A road that ends at a place's door holds at least a whole bundle, so a bundle that arrives while the place is busy can wait on it.

F6 Every out door reaches every in door

for all a, b in doors where medium(a) = "ions" and medium(b) = "ions" and dir(a) = "out" and dir(b) = "in" and family(owner(a)) != "road" and family(owner(b)) != "road" and owner(a) != owner(b):
  reachable(a, b)

A bundle leaving any place can be brought to any other place, along roads and through junctions.

F7 Every classical door of a place is wired to the control floor

for all d in doors where medium(d) = "bits" and not classical(owner(d)):
  for some w in wires where d in ends(w):
    for some e in ends(w) where e != d: classical(owner(e))

Every place that measures, reports an outcome or can be told to run has each of those doors wired to the decoder or the classical memory.

F8 The decoder's corrections reach the classical memory

for all d in doors where family(owner(d)) = "decoder" and signal(d) = "frame":
  for some w in wires where d in ends(w):
    for some e in ends(w) where e != d: family(owner(e)) = "archive"

The decoder's frame door is wired to a classical memory, which is where corrections are kept.

F9 Every place stands in a region of its kind

for all p in placed: region(p) = home_region(family(p))

Zones in memory; preparation, syndrome extraction, transversal gates, lattice surgery and readout in compute; factories and injection in factory; depots in supply; the decoder and the classical memory in control; junctions in traffic.

A schedule's rules machine.rules

A floorplan of verified places joined by roads and wires, and a logical program scheduled on it: what every gadget-level schedule must respect, whatever runs in parallel.

G1 Ports on a road agree, and every bundle arrives in the order its place takes it incore

(for all r in roads, a in ends(r), b in ends(r) where a != b:
   medium(a) = medium(b)
   and (role(a) = role(b) or role(a) = "any" or role(b) = "any")
   and (role(a) != "data" or role(b) != "data" or
        (width(a) = width(b) and (code(a) = none or code(b) = none or code(a) = code(b))))
   and (dir(a) != dir(b) or dir(a) = "inout"))
and (for all w in wires, a in ends(w), b in ends(w) where a != b:
   medium(a) = medium(b)
   and (signal(a) = signal(b) or signal(a) = "any" or signal(b) = "any")
   and (dir(a) != dir(b) or dir(a) = "inout"))
and (for all d in doors where role(d) != "any":
   count(r in roads where d in ends(r)) <= 1)
and (for all k in intakes:
   delivered_by(k) != none and order(delivered_by(k)) = expected(k))

A road or a wire joins two doors that carry the same thing (ions of the same role, width and code, or bits of the same signal) in opposite directions; a door that is not a free-for-all is on one road at most; and every bundle an op takes in arrives, in exactly the order the op's verified program takes it.

G2 Every ion leaves only from where it is, and ends where it shouldcore

(for all h in handoffs: location(ion(h), before(h)) = origin(h))
and (for all i in residents: location(i, final()) = home(i))
and (for all i in loaded where i not in living: location(i, final()) in depots)

Follow every ion through every handoff: it is loaded only if it did not exist, it leaves only the place it is in, it arrives only from the road it is on; every resident ion ends at home, and every loaded ion ends dumped at a depot or in a block still alive.

G3 No place holds more ions than its capacitycore

for all p in places, t in instants where family(p) != "depot":
  occupancy(p, t) <= capacity(p) and occupancy(p, t) >= 0

At every instant, counting an ion in a place from the moment it arrives until the moment it leaves, no place other than a depot holds more ions than it was built for, or gives away more than it has.

G4 A road holds at most its sites, and carries one way at a timecore

(for all r in roads, t in instants: occupancy(r, t) <= capacity(r))
and (for all c1, c2 in carries where road(c1) = road(c2) and simultaneous(c1, c2):
   origin(c1) = origin(c2))

No road ever holds more ions than it has sites, and no two bundles travel it in opposite directions at once.

G5 A place runs one op at a timecore

for all a, b in events where a != b and place(a) = place(b) and duration(a) > 0 and duration(b) > 0:
  not simultaneous(a, b)

Two ops of the same place, junctions and the classical places included, never overlap.

G6 No ion gets hotter than the ion-loss limit

for all e in events:
  exit_heat(e) <= ion_loss_limit() and peak_heat(e) <= ion_loss_limit()

Neither inside a place's op nor crossing one of its doors does an ion's motional energy pass the limit beyond which it is likely to be lost.

sources: arXiv:1210.3655

G7 Every instruction is carried out, and each block's in program ordercore

(for all i in instructions: not refused(i) and realised(i))
and (for all i, j in instructions where next_on_block(i, j): begins(j) >= finishes(i))

No instruction is refused or left without an event, and an instruction that acts on a block's ions starts only after the previous instruction on that block has finished with them.

G8 No block waits longer than its coherence budget without syndrome extraction

for all b in blocks: longest_gap(b) <= coherence_budget

Between ops that extract its syndromes, a block may wait or travel, but not for longer than the memory's coherence lets it.

G9 Every op used is verifiedcore

for all e in events:
  (status(e) = "verified" or status(e) = "certified" or (classical(e) and status(e) = "modeled"))
  and not logic_failed(e)

Every op the schedule runs at a place is verified as hardware and as logic (or certified); an op of the classical half is modeled, its latency a stated number.

G10 Every classical bit is used after it exists

when count(m in messages) > 0 or count(w in wires) > 0:
(for all m in messages:
   wire(m) != none and connects(wire(m), m) and approx(duration(m), latency(wire(m))))
and (for all m in messages where measured_by(m) != none: start(m) >= start(measured_by(m)))
and (for all m in messages where measured_by(m) != none and not held(m) and not classical(origin(m)):
   start(m) <= end(measured_by(m)))
and (for all m in messages:
   for some e in events where place(e) = destination(m) and instruction(e) = instruction(m):
     start(e) >= end(m))
and (for all f in frame_rows, e in named(f): start(e) <= at(f))
and (for all o in outcomes, e in named(o): start(e) <= at(o))

A message crosses a wire the floorplan has, between that wire's doors, in that wire's latency; it leaves no earlier than the op that measured its bits began and, unless it is a syndrome a decode sent out of its readout buffer, no later than that op ended; something at its destination uses it after it arrives; and no line of the classical memory names a measurement that has not begun.

G11 The decoder is called, and keeps up

when decoder_present() or count(e in guarded) > 0:
(for all j in decode_jobs:
   syndrome_of(j) != none and start(j) >= end(syndrome_of(j))
   and (next_syndrome(j) = none or start(j) <= end(next_syndrome(j))))
and (for all e in guarded:
   start(e) >= ready(e) and (for some m in decisions(e): end(m) <= start(e)))
and (for all w in windows:
   decoded(w) and (for some m in sends(w): start(m) >= measured(w))
   and (for all m in sends(w): start(m) >= measured(w)))
and (for all e in guarded, w in reads(e): ready(e) >= written(w))
and (for all f in frame_rows, w in reads(f): at(f) >= written(w))

Every syndrome the machine measures is sent to the decoder by a decode instruction, no earlier than it was measured; every decoding job starts after its syndrome arrives and before the next one does (or the decoder falls behind); a classically controlled op starts only once its guard is at its door; and nothing reads an outcome before the decoder has corrected it.

G12 Every bundle that travels is taken in at the far endcore

for all c in carries: count(k in intakes where delivered_by(k) = c) = 1

No ion is left on a road: every carry ends with an op at its destination (a place's op, a junction's pass, a depot taking used ions back) taking its bundle in, and exactly one op does.

G13 A road carries one bundle at a timecore

for all c1, c2 in carries where c1 != c2 and road(c1) = road(c2): not simultaneous(c1, c2)

A road is leased to one bundle from the moment its first ion enters until its last is taken off the far end; two bundles never share a road at once, so neither can block or overtake the other, whatever runs in parallel.

G14 A road holds the ions on it

for all c in carries: crowd(c) <= length(road(c))

At no moment are more of a bundle's ions on a road -- travelling, or stopped at the far end until they are taken in -- than the road has sites. A whole bundle can stop only on a road as long as the bundle, the one in front of a door; a short street between junctions holds the few ions crossing it at once.

Writing a rule

A rule set is a text file. It may start from another set (include), pick rules by name (use R1, R2), remove them (drop), set their numbers (param) and add rules of its own, in the language above and with the words above, and nothing else. A word the vocabulary does not have is refused when the file is read, with the line it is on.

ruleset "my-machine"
title "A machine without broadcast control"
include "standard"
drop R22                       # every electrode has its own signal
param max_chain = 20           # R13 allows a longer chain

rule X1 "No ion stands in the corner trap C3"
  about "C3 is under repair."
  for all i in ions, t in instants: position(i, t) != "C3"

Given this set, the compiler stops splitting transport steps into one motion each (R22 is gone), lets a gate chain grow to twenty ions, and keeps everything else as on the standard machine. X1 is a rule it has never seen: it does not plan for it, and the check afterwards decides it all the same, naming every instant an ion stands in C3.