Compilation

In words. The compiler reads the machine as a graph. Some nodes are traps (the set T), where ions can sit, up to a capacity, and in some of them be gated (the set gate) or measured (the set meas); the other nodes are junctions (J), where rails cross and no ion rests; the edges E are the rails. Some rails form named loops (L) that the control system can turn as a whole. Every part of this tuple is read off the machine text (the Machine page, section 6); the prices in that text are read only by cooling insertion (5.8), and nothing else about the hardware is ever read by the compiler.

In words. A hop is what one machine cycle can do to an ion: carry it from a trap to a neighbouring trap, passing through junctions on the way without stopping, because an ion never rests on a junction (R2). The compiler plans on the graph of traps and hops, not on the raw rails. The distance between two traps is the fewest hops between them.

In words. Two operations must keep their order only if they touch a common qubit (or classical bit); otherwise they are independent. Drawing an arrow from each operation to the next one on each of its wires gives the dependency graph. The interaction graph forgets the order and only counts how many two-qubit gates each pair of qubits shares.

In words. Besides the programme, the compiler hands over a certificate: which ion plays which qubit, where each ion starts, every move it will make and when, and for every gate a claim of the form "this gate happened at this instruction, in this trap, on these ions". Replaying the moves from the start tells you where every ion is at every cycle, and each claim can be checked against that.

In words. Produce a programme the machine can run, a certificate that places every gate of the circuit once, in order, in a trap where its ions are together, and pulses that compute the right thing; and make it short. Hops are the cost that matters physically: each hop heats its ion, and a hot ion gates worse (R7, R16), so a programme that moves ions further is not only slower but less accurate.

In words. Give every qubit a starting trap so that qubits which will gate together start close together. The score of a layout adds up, over every pair of qubits, "how many gates they share" times "how many hops apart they start". Lower is better. Single-qubit gates do not count: where they happen is decided later, and on a machine where every trap gates they cost no transport at all.

seed   a₀ ← argmaxa ∑b w(a,b);   π(a₀) ← argmint ∈ Tu ecc(t)   (the most central trap)
repeat n − 1 times
   a ← argmaxa unplaced ∑b placed w(a,b)
   π(a) ← argmint free ∑b placed w(a,b) · d(t, π(b))

In words. Start with the busiest qubit in the middle of the machine. Then, again and again, take the unplaced qubit with the most gates to qubits already placed, and put it in the free trap closest to its partners.

In words. Instead of placing qubits one at a time, spread all of them along a line at once, so that qubits sharing many gates land next to each other (the Fiedler vector is the best such line, in the least-squares sense). Then walk the machine outward from its centre, and hand the traps out along that walk, in order.

π ← argmin { Φ(πgreedy), Φ(πspectral) }
for at most 40 sweeps, while some swap improved in the last sweep
   for each pair a < b:  if Φ(π ∘ (a b)) < Φ(π) then π ← π ∘ (a b)
return ⟨π, πgreedy, πspectral⟩                (a ranked list)

In words. Take whichever of the two layouts scores better, then keep swapping pairs of qubits whenever a swap lowers the score, until no swap does. Keep the other two layouts as spares: a layout can score well and still leave an ion somewhere the router cannot get past later.

In words. Every operation goes into the earliest layer it can: one layer after the latest operation it depends on. Layers run one after another; inside a layer, nothing depends on anything else, so everything in it may happen at the same time, as far as the hardware allows.

In words. Gates in the same layer fire in lock-step: the first pulse of every gate together, then the second pulse of every gate, and so on. Because each gate is in its own trap, this never asks one trap to do two things in a cycle, so a layer of many gates takes as long as one gate.

In words. A two-qubit gate happens in the trap that can gate, is not already taken by another gate of this layer, has room for both ions once the ions already parked in it are counted, and is closest to the pair, counting both ions' journeys. Among equals, the first in the document wins.

In words. When a layer is done, every ion that gated in it and is not needed by the very next layer is sent back to where it started. That keeps the few gate-capable traps of a machine free for the gates still to come, and the one-layer lookahead stops the rule from sending an ion home only to fetch it straight back.

In words. Some ions must get from where they are to the trap their gate was assigned; every other ion stands still and is in the way. Find each mover a route, one hop per cycle with waiting allowed, so that no rule is broken at any cycle, and finish as early as possible. This is multi-agent path finding, with the twist that ions share traps up to a capacity and that, on a broadcast-wired machine, everything moving in one cycle must move the same way.

LB ← maxi ∈ M d(pos(i), τ(i));   H ← 2·ecc(GT) + 8
for rung in ⟨(uniform, strict), (¬uniform, strict), (¬uniform, tolerant)⟩
   for H′ in ⟨H, 2H⟩            (the third rung tries H only)
      best ← ⊥
      for order in ⟨farthest first, nearest first, program order, its reverse⟩
         reserve every stationary ion at its trap for cycles 0..H′
         for i in order:  plan i by A*; if none, next order;  reserve its walk and its parking
         lay the hops out by departure cycle;  if ¬uniform, split each cycle by signature
         replay the emitted cycles against R1;  if strict and a trap overflows, next order
         if |cycles| < |best| then best ← cycles;   if |best| ≤ LB then return best
      if best ≠ ⊥ then return best
raise Unroutable

In words. Try four different orders of planning the movers and keep the plan with the fewest cycles, stopping early if a plan is provably as short as possible. If nothing routes within the search horizon, double it once. If the strict one-waveform search fails, relax it in two steps. Before anything is emitted, replay it and refuse a plan that would overfill a trap.

In words. Think of the loop as a conveyor belt with a few workstations (the docks) beside it. Ions riding the belt keep their places on it; one instruction advances the whole belt by any number of slots, and it needs no empty slot to do so, because everything moves together.

In words. Two ions on the belt can never meet, so every gate must pair a rider with a docked ion. That works exactly when the qubits split into two groups with all gates running between the groups, one group small enough for the docks: the shape of a syndrome-extraction round, ancillas docked and data riding. It is also why the general router's limit, about half occupancy on a loop, does not apply here.

while operations remain
   drain: emit every ready measurement, reset and single-qubit gate on a docked ion   (no rotation needed)
   for each ready contact c = (rider i, dock Dc):  θc ← rail(Dc) − σ(i)  (mod N)
   θ* ← the θc with the largest batch (ties: nearest, either way)      [monotone variant: nearest ahead]
   B ← a set of ready contacts at θ*, at most one per dock and one per rider
   emit rotate(θ* − θ, the shorter way);  dock(B);  the CNOT rounds of B together;  undock(B)

In words. First do everything that needs no turn: measure, reset and single-qubit gates on docked ions. Then work out, for each gate that is ready, how far the belt would have to turn to bring its rider beside its dock, turn to the position where the most ready gates line up (the nearest, either way, when it is a tie), and do every ready gate there: pull the riders into their docks, fire, push them back out. The belt never turns while a rider is docked, since a docked ion is off the belt and would come back beside the wrong slot. Since every qubit's gates stay in the circuit's order, an ancilla has one gate ready at a time, and turning the shorter way to it costs fewer turns and fewer hops than always turning forward, which would lap the belt for each one; the forward-only rule is still there as an option.

In words. Moving an ion warms it up, and a warm ion makes a worse two-qubit gate. The pass walks through the programme with a thermometer, and wherever a two-qubit gate would fire too hot it inserts a cooling step just before it. Cooling is global, so one step cools every ion; that is why one walk is enough, and the pass checks the result by walking through again.

In words. Any single-qubit gate is one laser pulse plus a bookkeeping change of phase that costs nothing; a CNOT is one two-ion pulse with four single-ion pulses around it. Both facts are theorems, checked by a proof assistant, and the table is also tested numerically. The global phase is kept because it becomes visible once the gate is controlled, and a wrong phase convention is exactly the kind of error that hides until then.

In words. The same rule checker the studio runs on any hand-written programme is run on the compiled one, and it does not know or care how the programme was made. A router bug shows up as a failed rule on this page, not as a programme a machine would refuse.

1. unrealised(κ) = ∅;
2. μ is injective and total on Q;
3. the events are sorted by cycle, so the replay is well defined;
4. every rotation names a loop in loops_A;
5. ∀ m ∈ moves: (m.src, m.dst) ∈ H_A and pos_m.t(m.ion) = m.src;
6. ∀ g ∈ gates: g.site ∈ gate_A and ∀ i ∈ g.ions: pos_g.t(i) = g.site;
7. ∀ g ∈ gates: the ions g names are, in some order, μ of the qubits of the operation it names;
8. every operation of C′ other than measure, reset and barrier has exactly one witness;
9. every witness names an operation of C′;
10. for operations o before o′ sharing a qubit, the witness cycle of o precedes that of o′, whether or not the two commute.

In words. Nothing was left out; each qubit has its own ion; the moves can be replayed in order; every rotation is of a real loop; no ion ever teleports (every move is a real hop, starting from where the ion actually is); every claim names exactly the ions its operation's qubits live on, and finds them together in a trap that can gate; every gate of the circuit is claimed exactly once, and every claim names an operation of the circuit; and gates on a common qubit happen in the order written. A claim names an operation, never the gate applied there, so a claim on a barrier, a measurement or a reset passes too, and which gate fires is for Check 2 to decide.

In words. The checker is nothing but a decision procedure for Definition 9, and a machine-checked proof says that whenever it answers yes, the definition really holds. So the whole claim lives in the definition, which a reader can judge. The facts about the machine that the definition refers to (which traps gate, which pairs are one hop apart, how each loop is ordered) are read out of the document by code the compiler never runs, so the compiler cannot make the machine bigger by saying so; that is what makes the guarantee hold for any machine.

In words. Finally, does the programme compute the right thing? The checker reads the pulses back out of the programme and works out what they do to the qubits, then compares with what the circuit does. For Clifford circuits this is done with stabilizer tableaux, which scale; otherwise the full matrix is compared, up to ten qubits. A wrong angle, a dropped frame update, a swapped control and target, or one gate compiled as another all change the answer. It is the only check that sees which gate the pulses make.