Compilation

A circuit comes in as OpenQASM and leaves as a hardware programme in the language the machine runs, together with a certificate. The compiler is not trusted: everything it emits is replayed against the rules, and R10, the programme implements the circuit, is decided by a checker written and proved sound in Lean plus a tableau composed from the emitted pulses. This page walks the pipeline on a Bell pair, then compiles and verifies every basic gate on the same six-site ring, and each result can be run here.

The input

OpenQASM 2.0 with qelib1.inc. Every gate is lowered to the native set of an ion trap: R(θ, φ), one laser pulse; VZ(λ), a virtual frame update that costs nothing; and MS(θ), the Mølmer–Sørensen entangler on two co-located ions. The lowering is two identities proved in Lean (u3_decomp, cx_decomp in Compiler/lean/QCCDC/Pulse/Decompose.lean) and the OCaml table that emits them is checked against the defining unitaries.

OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
creg c[2];
h q[0];
cx q[0],q[1];
measure q -> c;

The pipeline

1. Parsecircuit_ops, a DAG
   the QASM becomes a list of operations with their qubits, parameters and source lines, and the per-qubit order between them; a second front end in Python agrees on 507 of 507 test circuits.
2. Lowerpulses per op
   each single-qubit gate becomes u3(θ, φ, λ) and then VZ(λ) followed by R(θ, φ); cx becomes R, MS(π/2), R, R, R; composites unfold to those.
3. Placemap, init
   qubits are bound to ions (map) and ions to sites (init): the ion mapping. Candidates from a greedy and a spectral placement are scored by weighted interaction distance and the better one kept.
4. Route and schedulemoves, layers
   ops are scheduled in DAG layers; every two-qubit gate's operands are carried to one gate-capable trap. The general router moves one ion at a time along hops the device admits; on rings past about half occupancy the rigid-rotation pass turns the whole loop instead. Every move is recorded.
5. Emitprog.tsir.json + prog.qcert.json
   the hardware programme in the language, every instruction stamped with the circuit op it serves (meta.op), and the certificate: the mapping, the moves, one witness per gate with its site, ions and pulses.
6. Coolprog.cooled.tsir.json
   the cooling pass replays the programme under the heating model and inserts cooling where a gate would otherwise fire hot (R7).
7. Verify the rulesrules.json
   the same verifier the studio runs replays the cooled programme and reports the 22 structural rules; R10 is what remains.
8. Verify R10verdict.json
   O1: the certificate's moves are replayed from init; every gate must find its operands together in a trap that can gate, every hop must be one the device admits, every op witnessed exactly once and in order. The Lean checker QCCDC.Cert.check decides this, and check_sound proves that an accepted input implements the circuit. The device facts it judges against are re-derived from the architecture by code the compiler never runs. O2: the pulses are read out of the emitted programme, composed through the mapping into a stabilizer tableau and compared with the circuit's; outside the Clifford fragment an exact unitary is compared instead. A swapped operand, a dropped gate, a wrong angle or a mis-tracked frame all move the tableau.
9. Drawthe page
   the studio joins the programme and the circuit through the stamps, but only after checking every witness against the stamp on the instruction it names; a disagreement refuses to draw.

The ion mapping, verified

For the Bell pair the placer binds q0 and q1 to ions and seats them; the CNOT then needs both in one trap, so one ion travels round the loop to the other's dock. O1 recomputes every position from init and the move list and checks each gate's operands are where the witness says.

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 h
#3   gate VZ q0 @A0   ← op 0 h
#4   shuttle q1 A3→S3   ← op 1 cx
#5   shuttle q1 S3→S4   ← op 1 cx
#6   shuttle q1 S4→S5   ← op 1 cx
#7   shuttle q1 S5→S0   ← op 1 cx
#8   shuttle q1 S0→A0   ← op 1 cx
#9   gate R q0 @A0   ← op 1 cx
#15  cool all
#10  gate MS q0,q1 @A0   ← op 1 cx
#11  gate R q0 @A0   ← op 1 cx
#12  gate R q1 @A0   ← op 1 cx
#13  gate R q0 @A0   ← op 1 cx
#14  measure q0,q1   ← op 2 measure, 3 measure

The pulse sequence, matched to the gate

Each gate witness names the instruction that completes the op, the site, the ions and the pulses in time order. Two checks meet here: the lowering is a theorem (these pulses equal this gate, up to global phase), and O2 composes the pulses actually emitted back into the circuit's semantics, so a pulse the compiler emitted but did not witness, or witnessed but did not emit, is caught.

Verdict for the Bell pair: rules 20 passed; R10 passed — O1 by the proved Lean checker (QCCDC.Cert.check_sound); O2 by stabilizer tableau, composed from the emitted pulses.

Every basic gate, compiled and verified

One circuit per gate on the same ring, through the same pipeline: the input, the hardware programme it became, the ion mapping, the pulses witnessed, and the verdicts of the rules and of R10's two halves. The gates that need no laser show a lone frame update; the two-qubit gates show the transport that brings the ions together; the non-Clifford ones are checked against the exact unitary.

h q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 h
#3   gate VZ q0 @A0   ← op 0 h

x q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 x
#3   gate VZ q0 @A0   ← op 0 x

y q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 y
#3   gate VZ q0 @A0   ← op 0 y

z q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 z
#3   gate VZ q0 @A0   ← op 0 z

s q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 s
#3   gate VZ q0 @A0   ← op 0 s

t q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 t
#3   gate VZ q0 @A0   ← op 0 t

rx(0.5) q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 rx
#3   gate VZ q0 @A0   ← op 0 rx

ry(0.5) q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 ry
#3   gate VZ q0 @A0   ← op 0 ry

rz(0.7854) q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   gate R q0 @A0   ← op 0 rz
#3   gate VZ q0 @A0   ← op 0 rz

cx q[0],q[1];

#0   init q0@A0, q1@A3
#1   cool all
#2   shuttle q1 A3→S3   ← op 0 cx
#3   shuttle q1 S3→S4   ← op 0 cx
#4   shuttle q1 S4→S5   ← op 0 cx
#5   shuttle q1 S5→S0   ← op 0 cx
#6   shuttle q1 S0→A0   ← op 0 cx
#7   gate R q0 @A0   ← op 0 cx
#17  cool all
#8   gate MS q0,q1 @A0   ← op 0 cx
#9   gate R q0 @A0   ← op 0 cx
#10  gate R q1 @A0   ← op 0 cx
#11  gate R q0 @A0   ← op 0 cx
#12  shuttle q1 A0→S0   ← op 0 cx
#13  shuttle q1 S0→S5   ← op 0 cx
#14  shuttle q1 S5→S4   ← op 0 cx
#15  shuttle q1 S4→S3   ← op 0 cx
#16  shuttle q1 S3→A3   ← op 0 cx

cz q[0],q[1];

#0   init q0@A0, q1@A3
#1   cool all
#2   shuttle q1 A3→S3   ← op 0 cz
#3   shuttle q1 S3→S4   ← op 0 cz
#4   shuttle q1 S4→S5   ← op 0 cz
#5   shuttle q1 S5→S0   ← op 0 cz
#6   shuttle q1 S0→A0   ← op 0 cz
#7   gate R q1 @A0   ← op 0 cz
#8   gate VZ q1 @A0   ← op 0 cz
#9   gate R q0 @A0   ← op 0 cz
#21  cool all
#10  gate MS q0,q1 @A0   ← op 0 cz
#11  gate R q0 @A0   ← op 0 cz
#12  gate R q1 @A0   ← op 0 cz
#13  gate R q0 @A0   ← op 0 cz
#14  gate R q1 @A0   ← op 0 cz
#15  gate VZ q1 @A0   ← op 0 cz
#16  shuttle q1 A0→S0   ← op 0 cz
#17  shuttle q1 S0→S5   ← op 0 cz
#18  shuttle q1 S5→S4   ← op 0 cz
#19  shuttle q1 S4→S3   ← op 0 cz
#20  shuttle q1 S3→A3   ← op 0 cz

swap q[0],q[1];

#0   init q0@A0, q1@A3
#1   cool all
#2   shuttle q1 A3→S3   ← op 0 swap
#3   shuttle q1 S3→S4   ← op 0 swap
#4   shuttle q1 S4→S5   ← op 0 swap
#5   shuttle q1 S5→S0   ← op 0 swap
#6   shuttle q1 S0→A0   ← op 0 swap
#7   gate R q0 @A0   ← op 0 swap
#27  cool all
#8   gate MS q0,q1 @A0   ← op 0 swap
#9   gate R q0 @A0   ← op 0 swap
#10  gate R q1 @A0   ← op 0 swap
#11  gate R q0 @A0   ← op 0 swap
#12  gate R q1 @A0   ← op 0 swap
#28  cool all
#13  gate MS q1,q0 @A0   ← op 0 swap
#14  gate R q1 @A0   ← op 0 swap
#15  gate R q0 @A0   ← op 0 swap
#16  gate R q1 @A0   ← op 0 swap
#17  gate R q0 @A0   ← op 0 swap
#29  cool all
#18  gate MS q0,q1 @A0   ← op 0 swap
#19  gate R q0 @A0   ← op 0 swap
#20  gate R q1 @A0   ← op 0 swap
#21  gate R q0 @A0   ← op 0 swap
#22  shuttle q1 A0→S0   ← op 0 swap
#23  shuttle q1 S0→S5   ← op 0 swap
#24  shuttle q1 S5→S4   ← op 0 swap
#25  shuttle q1 S4→S3   ← op 0 swap
#26  shuttle q1 S3→A3   ← op 0 swap

measure q[0] -> c[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   measure q0   ← op 0 measure

reset q[0];

#0   init q0@A0, q1@A3
#1   cool all
#2   reset q0   ← op 0 reset

Reproduce it

The same commands, from the repository root, on any circuit and device:

python Compiler/bridge/export_arch.py arch/<device>.arch.json -o build/<device>.expanded.json
Compiler/ocaml/_build/default/bin/qccdc_cli.exe compile circuit.qasm --arch build/<device>.expanded.json -o build/out
python Compiler/bridge/insert_cooling.py build/out.tsir.json --arch arch/<device>.arch.json -o build/out.cooled.tsir.json
python Compiler/bridge/check_tsir.py build/out.cooled.tsir.json --arch arch/<device>.arch.json --model corrected
python Compiler/bridge/mk_qcheck_input.py build/out --arch build/<device>.expanded.json -o build/out.qcheck.json
python Compiler/bridge/check_cert.py build/out --qasm circuit.qasm --arch arch/<device>.arch.json --qcheck build/out.qcheck.json
python -m qccd studio --tsir build/out.cooled.tsir.json --qasm circuit.qasm --cert build/out.qcert.json

Phase 2 of the plan brings the compiler itself into the browser, so the Design page can do this without a command line.