The full stack

A fault-tolerant program on trapped ions, from the language it is written in to the ions that run it. Every layer is a program, every line of a layer is linked to the line it comes from, and every layer is checked.

FormalRV's own VM puts the CNOT at 268.5 ms on its abstract machine, where every qubit is virtual; here it takes 311.7 ms, with every ion moved.

Open a run. Its page is the design tool, playing the program on the machine, ion by ion. Pause anywhere and the Stack above the program names what is happening at that instant, one line per layer: the line of the algorithm, its Pauli-product measurement, the QEC statement, the gadget instruction, the Clifford step and the hardware instruction, each with its file and line. Click a line of any layer to jump to the first instruction that carries it.

The layers

1. The algorithm (.prog), in FormalRV's language, with its specification: gates, loops, controlled gadgets, and the input its specification assumes.
2. Pauli-product measurements (.qppm) and operations on code blocks (.qec, the distance-3 surface code), made by FormalRV's own compiler at a pinned commit, unchanged. Every .qec statement is linked to the .qppm statement it comes from, and that to its .prog line; each link says how it was made.
3. The gadget program: QCCD lowers the .qec to instructions of the machine's places: prepare a block, measure a Pauli product at a bench, take a magic state from a factory or a rotation source, read out, decode. A FormalRV gadget becomes a gate, defined once for every shape it is called with. The gadget program is checked against the .prog: the same operation in every branch, or the same results with the same probabilities and, result by result, the same state.
4. The schedule: the program runs on a machine of places joined by roads and junctions. Blocks travel between places and rest in memories that keep correcting them. The machine's rules judge the schedule. A program too large to unroll is scheduled one gate at a time, once per context in which it is called, and checked view by view and as a composition.
5. The hardware program (TSIR): every instruction belongs to one gadget, either a place's verified op on its own device or a road's carry, compiled with its whole bundle onto its conveyor. Every one passes the same hardware rules, R1–R23. Devices that share DACs or a laser take turns.
6. The ions: the page draws each one where that program puts it, at the time on screen.

The machine

The first three programs run on this machine: 21 places for ions, 63 junctions and 121 roads, with a decoder and an archive on a control floor wired to every place that measures.

FormalRV's Shor runs on a wider one: 53 places (32 memories, 4 benches, 4 factories), 146 junctions and 285 roads. How a machine is built and judged: the design.

What is checked, and what is not

• Checked: every link between two layers, by what both sides must share; what the gadget program computes, against the .prog; the machine's rules on the schedule; the hardware rules on every place op and on every road's own program; and every place, as hardware and as logic (the places).
• Not checked: logical error rates, since no noise is sampled; decoding, since the decoder and the archive are classical places with latencies, not run; and the fault distance of a whole run, which this stack does not require. The places that correct errors have distance 3; the Pauli-product bench, by design, does not.

Underneath