The rules

A rule is one assertion about a machine and what a programme does on it. The machine is itself a text, defined on the Machine page: a rule’s machine words (sites, rails, capacity, degree) are read off that text, and its execution words (operations, instants, occupancy) off the programme’s replay. A rule is 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

On this page

The Language page gave you the statements a programme is made of. This page is what a programme may and may not do with them.

What a rule is. One sentence of logic about a machine M (the text of the Machine page) and a programme’s run on it, evaluated on the replay, true or false. You will be able to read every rule on this page in its own words.
What the rules are for. They are the hardware's side of the bargain: capacity, junctions, one waveform per cycle, cold ions at a gate. A programme that breaks one is refused, and the page says which values broke it. 4 of the 57 are core and hold on every machine.
Rule sets. Different machines, and the papers that model them, assume different rules. A rule set names the rules and their numbers; the compiler plans with it and the checker judges with it.
Every rule, with a programme that keeps it and one that breaks it, both playable, so a rule is never only a formula.
Your own rule, in the same language, which the checker then decides without the compiler ever having heard of it.

Who decides whether a programme could really run on the hardware: the compiler that wrote it, or someone else?

Someone else. The compiler is a heuristic that may be wrong; the rules are a short text that anyone can read, and a checker that shares no code with the compiler evaluates exactly that text on the replay. That is why a rule is written as a formula and shown here as one.

the language
the words
rule sets
every rule
writing a rule

Reading a rule

In this section the ten shapes a rule can take. They are ordinary logic (for all, for some, and, or, counts and sums) over four finite sets: the sites of the machine, the operations and the instants of the run, and the circuit. After this section every rule on the page reads as a sentence.

A rule is a formula of first-order logic over finite sets: the sites of the machine (the text of the Machine page), 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.

A formula is only as clear as its words. The next section is the vocabulary: every name a rule may use and what it reads off the replay. Skim it now and come back to it from any rule below; each word is a link.

The words

In this section the dictionary of the rule language, grouped by what the words are about: the machine, the execution, the instants, the circuit.

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 machine

Every word in this group is read off the machine text M of the Machine page, through one record: its sites, junctions, rails, capacities, degrees, zones, abilities, loops and declared numbers. Nothing about the hardware reaches a rule any other way, which is why a rule set is a text about a machine text.

`ends(r)`	The two nodes rail r joins.
`junctions`	The nodes where three or more rails meet, whatever the machine calls them. An ion crosses a junction; whether it may stop there is a rule.
`legs`	The legs of a C2LR lattice: the trap at the centre of every wire between two junctions, each holding one two-ion crystal (one ion of this model). Empty on any other machine. Only in a programme.
`nodes`	Every node of the machine: 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.
`c2lr_device()`	Whether the machine is a C2LR swap-or-stay lattice: it declares C2LR control, and its drawing is a lattice of junctions with one leg on every wire (arXiv:2403.00756). Only in a programme.
`c2lr_wiring()`	Whether a machine that declares C2LR control is driven as C2LR is: a fixed number of shared analog signals, plus one digital input and one switch per leg, over a lattice of legs. 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 machine 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 machine declares it.
`control()`	How the machine'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.
`cyclone_device()`	Whether the machine is a Cyclone ring: its drawing says so, as the machine's generator parameters do.
`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 machine 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 machine's control system can drive in one step. Only in a programme.
`max_junction_degree()`	The most rails a junction of this machine may join, as its document declares (6 when it says nothing: a junction of a trap built in more than one layer joins up to six). Only in a programme.
`min_rail_angle()`	The smallest angle two rails meeting at a node may make, as the machine'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 machines gate across two zones of one rail).
`priced(j)`	Whether the machine declares the time it takes to cross junction j, at j's number of rails. Only in a programme.
`ring_device()`	Whether the machine is one closed ring: every site on the one loop with two rails, and every junction an L at its corners, of degree 2.
`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.
`shims_in_every_layer()`	Whether every layer's price on this machine carries its shim charge: the time of 128 shims at 3 us each, before the pulse.
`traps_within_thirty()`	Whether no trap of the ring holds more than 30 ions.
`wise_device()`	Whether the machine is a WISE chip: its drawing says so, as the machine's generator parameters do.
`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 machine'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.
`bits_only(k)`	Whether transport step k, if it is of a C2LR class, chooses nothing per leg but the direction bit: it is the machine's template, not routes the programme wrote. Only in a programme.
`c2lr_step(k)`	Whether step k is a C2LR template step: a swap-or-stay or a reorder-or-not, played by the machine's shared waveforms. Only in a programme.
`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 machine declares (or the machine 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.
`data_stays(k)`	Whether step k moves no data qubit: only ancillas travel. Only in a programme.
`disjoint(A, B)`	Whether sets A and B have nothing in common.
`drivable(k)`	Whether the machine'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 machine'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.
`exchange(x)`	Whether x -- a step, an instant, an operation or a hop -- belongs to a C2LR swap-or-stay step, whose crystals exchange through the junctions by the machine's matching: the routes are derived from the machine, never read from the programme, so a programme cannot claim this for a move it wrote itself. In a programme: An instant is the one during such a step; an operation or hop is one of its moves. In a timed schedule: Never: a paper's timed schedule has no swap-or-stay steps, so R2, R3, R5 and R22 judge all of it.
`exits_as_entered(k)`	Whether every crystal that leaves, in step k, a leg holding two under C1's exception is the one that entered it, leaving by the step type it entered by -- and whether every crystal step k shifts toward a junction could reach it. Only in a programme.
`form(k)`	How swap-or-stay step k pairs the legs: "diagonal" (every junction pairs the same two of its legs, as demonstrated) or "checkerboard" (two pairs at the junctions of one colour, the proposal's, assumed). Only in a programme.
`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.
`heats_every_crystal(k)`	Whether C2LR step k heats every crystal on the machine -- the ones that move and the ones that stay -- as every waveform plays on every leg. Only in a programme.
`independent_axes(k)`	Whether, in swap-or-stay step k, a crystal on a horizontal leg and one on a vertical leg set their bits independently: true of the template, which carries one bit per crystal and no field per axis. Only in a programme.
`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").
`lockstep(k)`	Whether Cyclone step k is part of a rotation in lockstep: the unbroken run of transport steps it belongs to moves every ancilla the same number of times, each time one trap on round the ring in the same direction. A trap's ancillas leave in turn, so a rotation may take several steps, and a run may hold several rotations. Only in a programme.
`loop(h)`	The closed loop hop h runs along, or none. Only in a programme.
`matched(k)`	Whether swap-or-stay step k is the machine's matching: every crystal it shifts toward a junction has a partner leg there under the step's variation, and the machine offers that variation. 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.
`one_kind(k)`	Whether step k is one kind of operation across the chip: a gate step's physical pulses all the same gate at the same angle. A frame change is not a pulse. Only in a programme.
`one_parity(k)`	Whether WISE step k plays one kind of pair at one parity in one direction: its class names them, each of its moves is one of the machine's pairs of that kind, and no zone takes part twice. Only in a programme.
`one_waveform(k)`	Whether swap-or-stay step k is one shared waveform: the replay prices it as one primitive, whose time is the step's however many crystals move. Only in a programme.
`pairs_only_to_gate_or_split(k)`	Whether, once step k is over, a zone that holds two ions is on its way to a gate or a split: step k is a swap step's half (one parity merging or splitting while another waits), their two-ion gate, or their cooling, and any other step leaves every zone holding one. Only in a programme.
`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.
`shim_opens(k)`	Whether swap step k, if it opens a reconfiguration, comes straight after the layer that charges its shims: a step with no pulse, an identity. A step that merges for a gate is that gate's layer, and carries its charge in the gate's price. 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.
`entered(s, t)`	Whether leg s holds two crystals at instant t under C1's exception: one of them entered it by a swap-or-stay enter -- moved toward the junction into a leg whose crystal stayed -- and has not left. Only in a programme. In a programme: During a step, it holds if it held before the step or holds after it.
`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 machine'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 gate, measurement or reset the compiler stamped with c. The transport stamped with c only brings its ions together, and does not count. 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

`com_frequency_held()`	Whether the machine's swap-or-stay step records the centre-of-mass frequency it holds a crystal at during a shift. A property of the waveform, recorded, not decided from a programme; a machine that records none leaves the rule unchecked. Only in a programme.
`declares_duty_budget()`	Whether the machine 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 machine's clock tracks how hot each ion gets. Only in a programme.

Is there one list of rules for every trapped-ion machine?

No. A machine with a signal per electrode has no one-waveform rule; a swap-or-stay lattice has rules no ring has. So the rules come in sets, and a design is judged by the set its machine declares.

Rule sets

In this section the shipped rule sets, each with the rules it contains and the numbers it fixes, and which boards and papers each one judges. The standard set is this website's machine.

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 machine 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
C2LR swap-or-stay c2lr.rules	C1 C2 C3 C4 C5 C6 C7 C8 C9 C10 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 This website's machine on a C2LR lattice: every rule of the standard set, and C1-C10. A swap-or-stay step's routes are the machine's matching, so the junction, rail, passing and one-waveform rules (R2, R3, R5, R22) do not judge its crossings; R4 still asks for its class. Both pairings are allowed: one diagonal at every junction (demonstrated) and the two-pair checkerboard steps (assumed, and marked so in every report). `max_chain = 15` — the most ions a gate's chain may hold (R13) `c2lr_forms = {"diagonal", "checkerboard"}` — how a C2LR step may pair legs (C6): "diagonal", one diagonal at every junction (demonstrated), and "checkerboard", two pairs at the junctions of one colour (assumed)	the C2LR boards
C2LR swap-or-stay, as demonstrated c2lr-demonstrated.rules	C1 C2 C3 C4 C5 C6 C7 C8 C9 C10 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 The C2LR rule set with only what arXiv:2403.00756 demonstrated: every junction runs the same single diagonal (W-S, W-N, E-S or E-N). A step that pairs two diagonals at the junctions of one checkerboard colour breaks C6. `max_chain = 15` — the most ions a gate's chain may hold (R13) `c2lr_forms = {"diagonal"}` — how a C2LR step may pair legs (C6): "diagonal", one diagonal at every junction (demonstrated), and "checkerboard", two pairs at the junctions of one colour (assumed)	—
WISE wise.rules	R0 R1 R2 R3 R4 R4b R4d R5 R6 R6b R7 R7c R8 R11 R12 R13 R14 R15 R16 R17 R18 R19 R20 R21 R22 R23 R24 R25 W1 W2 W4 W10 W11 A chip of cells, one junction zone and h gate zones each. A zone holds one qubit, or two for a gate or in the middle of a swap. A swap step plays one kind of pair at one parity, one direction to a half; one kind of operation runs across the chip in a step; a layer of gates is one gate at one angle; and every layer pays for its shims before it starts. No ion rests on a junction zone, which holds at most one at a time. `max_chain = 2` — the most ions a gate's chain may hold (R13)	—
Cyclone, as the transport deck writes it cyclone-deck.rules	R0 R1 R2 R3 R4 R4b R5 R6 R6b R7 R8 R11 R12 R18 R19 R20 R21 R24 R25 R27 Y1 Y2 Y3 Y4 One closed ring of traps with L-shaped junctions at its corners. Data qubits never move. Every ancilla moves in lockstep, one trap per step, one way round. A trap does one operation at a time, and a step's gates come before its rotation. Each qubit's operations keep 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	—

Now the rules themselves. Each card is one rule: the formula the checker evaluates, a sentence on what it protects, where it comes from, and two small programmes, one that keeps it and one that breaks it. Press Play on either to watch the cycle the verdict names.

Every rule

In this section all 57 rules, grouped by what they are about (the machine's geometry, occupancy, transport, control, gates, heat, cost, correctness), in the reader's browser. The group headings are the map; the cards are the territory.

All 57 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 (the C2LR rules by the set c2lr, on a C2LR lattice), and each opens as the page the studio would open on it.

C1 A leg holds one crystal, or two between an enter and its exit

when c2lr_device():
(for all s in legs, t in instants: occupancy(s, t) <= 1 or entered(s, t))
and (for all k in steps: exits_as_entered(k))

A leg holds one crystal. It holds two only after a swap-or-stay step moved a crystal toward a junction into a partner leg whose crystal stayed (an enter), and until that crystal leaves again by the same step type it entered by (its exit): the crystal that entered is the one that leaves, and no other step type takes it out.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

examples on: a 3×3 C2LR swap-or-stay lattice of Ba-Sr crystals: one leg (a trap holding one crystal) on every wire, moved only by swap-or-stay steps, one shared waveform and one direction bit per leg

holds

the same enter, and the exit back under W-S.

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0"])
p.swap_or_stay("WS", ["d0"])

C1 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

d0 enters d1's leg under W-S and is shifted out under W-N: a crystal leaves a leg by the step type it entered by.

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0"])
p.swap_or_stay("WN", ["d0"])

C1 failsk = step 1 (instruction #2): exits_as_entered(k) is false

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C2 A C2LR step's only per-leg choice is its direction bit

when c2lr_device():
for all k in steps where is_transport(k): bits_only(k)

Every crystal shifts toward its pair's junction or away from it, and that is all a step chooses per leg: the step names the crystals shifted toward and nothing else, and its routes are the machine's matching. A step of a C2LR class that writes its own routes is refused.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

the same exchange as a swap-or-stay step: two direction bits, and the machine's pairs.

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0", "d1"])

C2 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

the swap written as two routes under the class swap_or_stay: the routes are the programme's, so it is judged as plain moves, and breaks the junction and rail rules too.

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

C2 failsk = step 0 (instruction #1): bits_only(k) is falsethis programme also breaks R2, R3, R5, R22

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C3 Horizontal and vertical legs choose independently

when c2lr_device():
for all k in steps where exchange(k): independent_axes(k)

In one step a crystal on a horizontal leg and one on a vertical leg set their direction bits independently: the step carries one bit per crystal and nothing per axis.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

in one step d0, on the horizontal leg T0_1h, shifts toward J1_1 and moves into the empty vertical leg T1_1v, while d1, on the vertical leg T1_0v, stays. No programme breaks C3: a step has no field per axis to set, so the replay holds it by construction.

p.init({"d0": "T0_1h", "d1": "T1_0v"})
p.swap_or_stay("WS", ["d0"])

C3 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C4 A step is C2LR, one shared waveform, C2LR back

when c2lr_device():
for all k in steps where exchange(k): one_waveform(k)

Every crystal shifts by its bit, one junction waveform shared by every junction exchanges the two wells nearest each junction in play, and the shift is undone: one waveform, whose time is the step's however many crystals move.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

two swaps in one step, at J1_1 and J1_0: one waveform, priced as one primitive, 312.5 µs, the same as a single swap. No programme breaks C4: the replay prices every step as one waveform.

p.init({"d0": "T0_1h", "d1": "T1_1v", "d2": "T0_0h", "d3": "T1_0v"})
p.swap_or_stay("WS", ["d0", "d1", "d2", "d3"])

C4 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C5 Every crystal ends a step at a leg centre

when c2lr_device():
for all i in ions, t in instants where position(i, t) != none:
  position(i, t) in legs

After every step each crystal rests at the centre of a leg; a C2LR machine has nowhere else to hold one.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

d0 crosses J1_1 to the leg it pairs with, and rests there.

p.init({"d0": "T0_1h"})
p.swap_or_stay("WS", ["d0"])

C5 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

d0 is carried into the junction J1_1 and left there.

p.init({"d0": "T0_1h"})
p.simd("swap_or_stay", [["d0", "T0_1h", "J1_1", ["T0_1h.b"]]])

C5 failsi = ion d0, t = after step 0: position(i, t) is J1_1 and legs is {T0_0h, T0_0v, T0_1h, T0_1v, T0_2h, T1_0h, ...}this programme also breaks C2, C7, R23

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C6 A step pairs legs by the machine's matching

when c2lr_device():
for all k in steps where exchange(k): matched(k) and form(k) in c2lr_forms

A swap-or-stay step pairs every leg with at most one other, at one junction, by one variation of the machine: one diagonal at every junction (W-S, W-N, E-S or E-N, all four demonstrated), or two pairs at the junctions of one checkerboard colour (the proposal's, not demonstrated, so assumed). A crystal shifted toward a junction has a partner leg there, the machine offers the variation, and the rule set allows its form (c2lr_forms).

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

T0_0h pairs with T1_0v at J1_0, which is empty: d0 moves there.

p.init({"d0": "T0_0h"})
p.swap_or_stay("WS", ["d0"])

C6 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

T0_0v is on the lattice's edge: under W-S its junction J0_0 has no W leg, so d0 has nowhere to go.

p.init({"d0": "T0_0v"})
p.swap_or_stay("WS", ["d0"])

C6 failsk = step 0 (instruction #1): matched(k) is false

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C7 No crystal ends a step in a junction

when c2lr_device():
for all i in ions, t in instants: position(i, t) not in junctions

A crystal crosses a junction inside a step and never rests on one: where three or more rails meet, nothing is left standing when a step ends.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

a swap through J1_1: both crystals pass it, and both rest in legs.

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0", "d1"])

C7 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

d0 ends the step in J1_1.

p.init({"d0": "T0_1h"})
p.simd("swap_or_stay", [["d0", "T0_1h", "J1_1", ["T0_1h.b"]]])

C7 failsi = ion d0, t = after step 0: position(i, t) is J1_1 and junctions is {J0_1, J1_0, J1_1, J1_2, J2_1}this programme also breaks C2, C5, R23

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C8 The trap frequency is held during a shift

when c2lr_device():
com_frequency_held()

The C2LR shift moves a crystal by a sixth of the leg while holding its centre-of-mass frequency (1.85 MHz for Ba-Sr, 1.4 MHz for Yb-Ba). It is a property of the step's waveform, recorded with its primitive rather than decided from a programme.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

a swap on the Ba-Sr lattice, whose primitive records 1.85 MHz held during the shift (p4).

machine: a 3×3 C2LR swap-or-stay lattice of Ba-Sr crystals: one leg (a trap holding one crystal) on every wire, moved only by swap-or-stay steps, one shared waveform and one direction bit per leg

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0", "d1"])

C8 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

does not apply

the same swap on a lattice whose swap-or-stay primitive records no COM frequency: C8 does not apply, and says why. It is never a pass for want of a number.

machine: the same 3×3 Ba-Sr lattice, its swap-or-stay primitive recording no COM frequency

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0", "d1"])

C8 does not applythe machine's swap_or_stay primitive records no COM frequency

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C9 Every crystal is heated by every waveform

when c2lr_device() and models_heating():
for all k in steps where c2lr_step(k): heats_every_crystal(k)

The shared waveforms play on every leg, so a step heats every crystal on the machine: one that moved by the step's swap heat, every other by its stay heat. A crystal that sat a step out is not cold.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

d0 and d1 swap and d2, on the edge, stays: all three are heated, d2 by the stay's 0.035 quanta.

p.init({"d0": "T0_1h", "d1": "T1_1v", "d2": "T0_0v"})
p.swap_or_stay("WS", ["d0", "d1"])

C9 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

C10 Control is shared signals plus one input and one switch per leg

when control() = "c2lr":
c2lr_wiring()

A C2LR machine is driven by a fixed set of shared analog signals (27 in the paper), plus one digital input and one switch per leg: its document says so, and its drawing is the lattice of legs they drive.

sources: arXiv:2403.00756

in the rule sets: c2lr c2lr-demonstrated

holds

the lattice as the paper wires it: 27 shared analog signals, one input and one switch per leg (p4).

machine: a 3×3 C2LR swap-or-stay lattice of Ba-Sr crystals: one leg (a trap holding one crystal) on every wire, moved only by swap-or-stay steps, one shared waveform and one direction bit per leg

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0", "d1"])

C10 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

the same swap on a lattice whose document gives each leg two digital inputs: C2LR's per-leg control is one bit, so the machine is not driven as C2LR is, whatever the programme does.

machine: the same 3×3 Ba-Sr lattice, its document giving each leg two digital inputs

p.init({"d0": "T0_1h", "d1": "T1_1v"})
p.swap_or_stay("WS", ["d0", "d1"])

C10 failsc2lr_wiring() is false

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

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 c2lr c2lr-demonstrated wise cyclone-deck

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 c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

R2 A junction holds one ion at a time

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

Where three or more rails meet, only one ion may be at any moment, resting or passing through. An ion here is a qubit ion with the coolant ion that shares its well: a qubit-coolant pair crosses a junction as one crystal, as the Ba-Yb pair does through an X-junction. Two qubit ions in one junction at once is what the rule refuses -- except during a swap-or-stay exchange on a C2LR machine, where the shared junction waveform exchanges the two wells nearest it by design, and the routes are the machine's own matching, never the programme's.

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

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones tiscc trapsimd ionshuttler c2lr c2lr-demonstrated wise cyclone-deck

examples on: a 3×3 lattice of junction nodes: the centre J1_1 is a degree-4 X-junction, the four edge midpoints degree-3 T-junctions and the four corners plain bends, with one trap site (T…) on every wire between them

holds

the same two crossings, one cycle after the other: one ion in J1_1 at a time.

p.init({"d0": "T0_1h", "d1": "T1_0v"})
p.shuttle("d0", ["T0_1h", "J1_1", "T1_1h"])
p.shuttle("d1", ["T1_0v", "J1_1", "T1_1v"])

R2 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

in one cycle d0 crosses the X-junction J1_1 along its row and d1 crosses it along its column: two ions in J1_1 at once. Two different motions in one cycle also break R22.

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

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

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

R3 A rail carries at most its capacity

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

No more ions travel along one rail at once than the rail is built for (one, on most machines). A swap-or-stay exchange on a C2LR machine carries its two crystals along the junction's two rails by design, and is not judged here.

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

in the rule sets: standard qccdsim qccdsim-physical qccdsim-gateset cyclone jones ionshuttler c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

R4 Every transport step uses a movement the machine declares

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

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

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

in the rule sets: standard c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

no class named teleport exists on this machine.

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

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

R5 No two ions pass each other on a rail in one step

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

Within one step, two ions may not travel the same rail in opposite directions, one from each end: an ion rides the rail's RF null, a single line, so the two would have to pass through each other. Exchanging two ions inside one trap by rotating their crystal is a different operation, the ion swap, and this rule does not concern it; nor does a swap-or-stay exchange on a C2LR machine, whose two crystals pass each other through the junction's shared waveform by design.

sources: the ion-transport deck (v3)

in the rule sets: standard c2lr c2lr-demonstrated wise cyclone-deck

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 exchange in two cycles: d0 joins d1 in the trap C2, and d1 leaves it in the next cycle. Inside the trap the two ions may trade places (on hardware an ion swap, which rotates the two-ion crystal); R5 is only about the rail between traps.

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

R5 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

d0 and d1 set off from the two ends of the C1–C2 segment in the same cycle, so they would meet head-on on it. 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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 machine's budget; a cooling operation must come first otherwise. Below the budget the heat is not ignored: it is priced into the gate's error (R16, and the noise model behind every logical error rate). The budget is a hard limit because that error law describes the gate only while the ions stay in the Lamb-Dicke regime; a hotter gate is refused, not priced. A machine that declares no budget leaves only the price.

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

in the rule sets: standard c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 machine declares such a budget yet.

sources: arXiv:2504.17886

in the rule sets: standard c2lr c2lr-demonstrated

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated

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

Playthe programme, played once; then step it or scrub 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 machine (a junction of five or six rails the machine does not price crosses at the X-junction's time and heat, since no table measures one).

sources: arXiv:2511.15910

in the rule sets: standard c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 trap built in more than one layer has junctions of up to six rails, so 6 is the limit unless the machine declares a lower one (4 for a surface trap, which has T- and X-junctions and nothing denser). A junction of five or six rails crosses at the X-junction's time and heat unless its machine prices that degree itself: no shipped table measures one.

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

in the rule sets: standard c2lr c2lr-demonstrated wise cyclone-deck

examples on: six rails meeting at one node J, 60 degrees apart: a junction of degree 6

holds

J joins six rails, 60 degrees apart: the most a junction may join. The machine prices no degree-6 crossing, so it crosses at the X-junction's price.

machine: six rails meeting at one node J, 60 degrees apart: a junction of degree 6

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

R19 holds

Playthe programme, played once; then step it or scrub it

open the page, with its Report pane

fails

J joins seven rails, one more than the limit. (Seven rails cannot all be 60 degrees apart, so R20 fails too.)

machine: seven rails meeting at one node J: a junction of degree 7

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

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

Playthe programme, played once; then step it or scrub it

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 machine's minimum angle (60 degrees unless it declares another).

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

in the rule sets: standard c2lr c2lr-demonstrated wise cyclone-deck

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.

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

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

R20 holds

Playthe programme, played once; then step it or scrub it

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.

machine: 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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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.

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

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

R21 holds

Playthe programme, played once; then step it or scrub it

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.

machine: 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

Playthe programme, played once; then step it or scrub it

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) and not exchange(a):
  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. A swap-or-stay step on a C2LR machine is one shared waveform by construction -- each crystal's only choice is its direction bit -- so the different routes its crystals take are not judged here (C2, C4 are its rules).

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

in the rule sets: standard c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise

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

Playthe programme, played once; then step it or scrub it

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

Playthe programme, played once; then step it or scrub it

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 c2lr c2lr-demonstrated wise cyclone-deck

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 c2lr c2lr-demonstrated wise cyclone-deck

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 cyclone-deck

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 machines 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

W1 A zone holds one qubit, except for a gate or the middle of a swap

when wise_device():
for all k in steps: pairs_only_to_gate_or_split(k)

The trap is split into zones. A reconfiguration holds one qubit per zone. Two qubits share a zone only because a step merged them, for a gate or as the first half of a swap, and they split again before anything else happens there. (S1)

sources: arXiv:2305.12773, QCCD Transport Architectures deck, WISE S1

in the rule sets: wise

W2 A swap step pairs zones by the chip's parity

when wise_device():
for all k in steps where is_transport(k): one_parity(k)

Every zone is odd or even, and zones of one parity class share their DACs. So a step's pairs are all of one parity: the same waveform plays on all of them. WISE needs this because two swap partners must play different waveforms. (S2)

sources: arXiv:2305.12773, QCCD Transport Architectures deck, WISE S2

in the rule sets: wise

W4 One kind of operation runs across the chip in a step

when wise_device():
for all k in steps where is_transport(k): mode(k) = "inter" and not carries_gates(k)

Only one kind of operation (swap, split, merge or gate) runs across the chip in a step; different kinds run one after another. A design choice that keeps the DAC count fixed, not a hardware limit. Transport's half is W2; a gate's is W10's. (S4)

sources: arXiv:2305.12773, QCCD Transport Architectures deck, WISE S4

in the rule sets: wise

W10 A gate layer is one gate at one angle

when wise_device():
for all k in steps: one_kind(k)

The circuit is broken into a few basis gates and run as layers, one gate kind across the chip per layer. A frame change is not a pulse, so it is free of this. Many traps may gate at once, but all must run the same gate. (S10)

sources: arXiv:2305.12773, QCCD Transport Architectures deck, WISE S10

in the rule sets: wise

W11 Every layer pays for its shims first

when wise_device():
shims_in_every_layer() and (for all k in steps: shim_opens(k))

Shim voltages are set before each reconfiguration or gate layer and held fixed throughout it: 128 shims at 3 us each. A gate, readout or reset carries the charge in its price, and a reconfiguration opens with a layer that charges them and plays no pulse. (S11)

sources: arXiv:2305.12773, QCCD Transport Architectures deck, WISE S11 and T4

in the rule sets: wise

Y1 The machine is one ring

when cyclone_device():
ring_device()

Traps sit on one closed ring, with L-shaped junctions only at its corners and no X or T junctions. Split loops were rejected: HGP and BB stabilizers share data across any cut. (S1, S9, HW2)

sources: arXiv:2511.15910, QCCD Transport Architectures deck, Cyclone S1, S9 and HW2

in the rule sets: cyclone-deck

Y2 Data stays, ancillas move

when cyclone_device():
for all k in steps where is_transport(k): data_stays(k)

Data qubits are spread evenly and never move; only ancillas travel. (S2)

sources: arXiv:2511.15910, QCCD Transport Architectures deck, Cyclone S2

in the rule sets: cyclone-deck

Y3 Every ancilla moves in lockstep

when cyclone_device():
for all k in steps where is_transport(k): lockstep(k)

All ancillas move together, one way round, one trap per step, so there are no roadblocks or rebalances. (S3)

sources: arXiv:2511.15910, QCCD Transport Architectures deck, Cyclone S3

in the rule sets: cyclone-deck

Y4 A trap holds at most 30 ions

when cyclone_device():
traps_within_thirty()

Traps hold up to n ions each, and n is at most 30 in QCCD Studio. (HW1)

sources: QCCD Transport Architectures deck, Cyclone HW1

in the rule sets: cyclone-deck

One level up: the machine

A fault-tolerant machine is built from places -- each a small machine 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's sites at one moment, as the road's compiled program has them (an ion waiting at a door is on its stub); without one, each is on it from when it leaves until it is taken in at the far end.
`decoded(w)`	Whether some `decode` instruction sent window w to the decoder.
`decoder_present()`	Whether the floorplan has a decoder.
`delivered(k)`	The ions intake k takes off its carry, each when the carry says it was taken, in the order the carry brings them: the whole bundle for a place's op, one ion for a junction's lone pass.
`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: the op replayed from the n̄ its ions really arrive at, after every op, road and junction before 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: the op replayed from the n̄ its ions really arrive at (heat followed across the town).
`place(x)`	Where activity x happens (an op, a pass, a classical job).
`plane_conflicts()`	How many times two machines that share a plane (of DACs, or one laser: the floorplan's `plane`) play different cycles at once -- every op's TSIR at its times, every road's compiled program. 0 when nothing shares a plane.
`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.
`road_ok(c)`	Whether carry c, compiled with its whole bundle onto its road's own machine (one class a cycle, blocked ions holding by their switches), passes the basic rules R1-R23, delivers every ion before the far side takes it, and keeps off each door's stub while the op on that side drives it.
`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.
`taken(c)`	The ions of carry c as the ops at its far end take them in, each op's share in turn: carry c's own order, if every ion is taken once.
`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 delivered(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, nor on its way between places does an ion's motional energy pass the limit beyond which it is likely to be lost. Its n-bar is followed through every op, road and junction: a road and a junction pass add what their replay charges, and an op is replayed from the n-bar its ions arrive at, so a bundle that crossed twenty junctions is as hot as it is.

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: taken(c) = order(c)

No ion is left on a road: every carry ends with the ops at its destination taking each of its ions in exactly once, in the order it travels -- one op for a whole bundle (a place's, a depot taking used ions back), or a junction's lone passes, one ion at a time, as the road delivers them.

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's sites than it has. By the road's own compiled program, an ion that has arrived waits on the far door's stub, which has room for the bundle, until it is taken in, so a short street between junctions holds only the few ions crossing it at once. Without the program, an ion counts as on the road from when it leaves until it is taken in.

H1 The hardware between gadgets obeys the basic rulescore

for all c in carries: road_ok(c)

A gadget is a box with doors, but the chip is one: what carries ions between the boxes is driven by DACs and electrodes like what moves them inside one. Every carry, compiled with its whole bundle onto its road's own machine -- one class a cycle, a shift rigid, a blocked ion holding by its switch -- passes R1-R23; it delivers every ion before the far side takes it; and a door's stub is driven by one side at a time, the road never loading or delivering while the op there moves an ion on or off it.

H2 Machines that share a plane play one waveform at a timecore

plane_conflicts() = 0

A floorplan may say that machines share one plane of DACs, or one laser, instead of driving their own. Then they are one set of channels: at no instant do two of them play different cycles -- each op's TSIR at its times, each road's compiled program -- unless it is the very same cycle (class, direction, start and end), played once for both. Members take turns; a trip over two roads of one plane waits between them.

Writing a rule

In this section a rule set is a text file you can write. One example: a machine without broadcast control, with one rule of its own.

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.

What to remember

A rule is one formula over four finite sets, evaluated on the replay of a programme. It holds, fails (naming the values), does not apply, or could not be checked; it is never trusted on anyone's word.
The rules are the hardware's constraints made explicit: capacity (R1), junctions (R2), one waveform per cycle (R22), cold ions at a gate (R7), and the rest. 4 core rules hold on every machine; the others come in rule sets, one per machine model.
The compiler plans with a rule set and is then judged by it, including rules it never saw. A failed rule on a compiled programme is a compiler bug made visible, not a programme a machine would refuse.
You can write a rule set. The checker decides a new rule the same way it decides the shipped ones.

The Compilation page shows the other side: how the compiler keeps a programme inside these rules while it routes, and which checks run on its output afterwards.

Next in the storyCompilation: from a circuit to a verified programme Before thisLanguage: how a programme tells the machine what to do