Tutorial

One path: the tutorial, then the reference, then a real design stepped instruction by instruction. Its first parts open the design tool on an exercise and check your work against the page's own verdicts; its later parts are the verified compiler, in Lean, run in this browser. Your progress is kept in this browser, and on your account when you are signed in. Open the tutorial.

The tutorial

0%of the tutorial
Your progress
Level 1 · Newcomer
0 of 311 exercises0 of 538 stars0 of 13 badges
Finish your first exercise to become an Apprentice.
Start with A1: The machine in one picture →
Your progress is kept in this browser.
Map readerFinish Part A
Ion programmerFinish Part B
Rule keeperFinish Part R
Circuit schedulerFinish Part C
QCCD architectFinish Part D
ModellerSolve Part E's exercises
Proof checkerSolve Part F's exercises
SemanticistSolve Part G's exercises
AuditorSolve Part H's exercises
Compiler builderSolve Part I's exercises
Fault-tolerant architectSolve Part J's exercises
Tutorial completeFinish all 311 exercises
Every starEarn all 538 stars
Part A · 6 lessons · in the design tool

What you are looking at

The map you will build on: sites, junctions, segments, loops and zones, and what one move costs.

0 of 6 doneBadge: Map reader
sitejunctionrailspurA1The machine in one pictureA few micrometres above a chip, in a vacuum, a few ions are held in place by electric fields. This page is a map of that chip.Not started☆Start trap · 2data · 2load · 8gatecoolnew ionsA2Zones: what may happen whereNot every site can do everything. Some can hold a gate, some can measure, some only take in new ions.Not started☆Start loopA3Building by handEvery chip starts empty. You will build a square loop by hand.Not started☆☆Start 2 µs+0.2 n̄one push = time + heatA4The price of motionMoving an ion is not free. Each push along a rail warms the ion a little, and a warm ion makes a worse gate. A faster push warms it more.Not started☆Start 1 DAC8 electrodesone channelA5The control plane and broadcastingA chip has thousands of electrodes, but not thousands of wires. How the electrodes are wired decides what the chip can do at once.Not started☆Start A6The panelsYou have a device and a programme. Now read them.Not started☆Start
Part B · 8 lessons · in the design tool

Programming by hand

Ions on the map: a CNOT, a Bell pair and a docked rotation, written by hand in the eleven verbs.

0 of 8 doneBadge: Ion programmer
p.init({"d0": "S0"})p.shuttle("d0", […])B1The programme languageA device does nothing until you tell it what to do. Here is how.Not started☆☆Start CXB2One CNOTTwo ions, one gate. On paper it is one line of a circuit. On the chip it is a trip, a pause, then the gate.Not started☆☆Start d0d1Ha Bell pairB3Single-qubit gates and measurementA Bell pair is the simplest pair of entangled qubits: an H, a CX, then read both out.Not started☆☆Start data: no gatesR1R6R7R11B4Reading a failureThis programme is wrong. The page already knows why. The skill is to read what it says.Not started☆Start +2B5Loops and rotationSix ions, one instruction. Loops are why these machines can grow big.Not started☆☆Start p.simd1 stepB6Moving many ions at onceA rotation moves every ion. Sometimes you want to move three, not six.Not started☆☆Start one channel, one directionB7Broadcasting in a programmeTwo ions on one loop want to go opposite ways. The chip can give only one answer to both.Not started☆☆Start dockdockB8Docks and spursThe loop turns as one. To keep one ion out of the turn, park it to the side.Not started☆☆Start
Part R · 9 lessons · in the design tool

The rules the machine must obey

Every rule the machine obeys, broken on purpose and repaired, or the honest reason it cannot be checked here.

0 of 9 doneBadge: Rule keeper
holds 2roomR1A site holds what it holdsThree ions were sent into a site built for two. The chip did not stretch.Not started☆☆Start one at a timeR2Junctions: one at a timeTwo ions reach a crossing at the same moment. There is room for one.Not started☆Start no passing on one railR3Rails: no passing, no ghostsTwo ions on one rail walk toward each other. They cannot pass.Not started☆☆Start one stepshuttleshuttleteleportR4Steps: one kind of thingOne step is one setting of every voltage on the chip. So a step can do only one kind of thing.Not started☆☆Start 1 channelR5Broadcasting: what one channel can driveOne channel gives one answer to every site on it. Two ions asked for two different answers.Not started☆Start datatraptrapR6Where things may happenA gate needs a laser beam, and a measurement needs a camera. Not every site has them.Not started☆Start 3.2 qR7Heat: the budget, the clock, and why cooling is mandatoryThe ion crossed a junction and arrived shaking. The gate fired anyway, in the programme. On the real machine it would fail.Not started☆Start a chain of threeonly an end ion splitsR8Chains: splitting from the middleThree ions sit in a row, and the one you want is in the middle.Not started☆Start claimcost 2steps 3replaycost 3steps 3≠every claim is checkedR9Honesty: claims, certificates and the contractA programme said it would cost two. The replay said three.Not started☆Start
Part C · 4 lessons · in the design tool

Circuits by hand

A syndrome round and a plaquette, scheduled by hand under all the rules, with the heat paid for.

0 of 4 doneBadge: Circuit scheduler
d0c0d1c1d2measureC1A syndrome round of the repetition codeThree data ions, two check ions, four CNOTs, two measurements: the smallest error-correcting round, on a line of five sites.Not started☆Start samesteptwo traps, one instructionC2Parallelism under the rulesThe same round, faster. Not by breaking a rule, but by using what the rules allow.Not started☆Start a0 visitsall fourC3One plaquetteFour data ions around a crossing, and one check ion that must visit each of them.Not started☆Start × 2< 3.5 msreset, round againC4Two rounds and coolingError correction never stops. The second round starts where the first one ended.Not started☆☆Start
Part D · 4 lessons · in the design tool

Architecture decisions with the compiler

Let the compiler do it, then judge an architecture from measured numbers on the leaderboard's tasks.

0 of 4 doneBadge: QCCD architect
circuitprogrammeh q[0]cx q[0],q[1]measureshuttlecoolgate CXmeasurecertificateD1What the compiler doesYou have written every instruction by hand. Now read what a compiler wrote for a real circuit, and find the instruction that does the CNOT.Not started☆Start costD2The same circuit on nine machinesOne circuit, compiled for every shipped device and replayed under the same model. The numbers are in the table below. The question is why.Not started☆Start directbroadcast5,000+ DACs44 DACsD3Broadcast versus direct at scaleThe same chip, wired two ways. One needs over five thousand DACs. The other needs forty-four.Not started☆Start $ python -m qccd studio --tsir x.tsir.json --qasm x.qasm -o x.htmlD4Running the compiler yourselfEverything on this page came from a command line. Here are the commands.Not started☆Start
Part E · 4 chapters live · in Lean, in this browser

The machine as data

Devices as graphs, programmes as data, replay as a function, and the rules as statements Lean can decide.

0 of 33 exercisesBadge: Modeller
junctionjunctionbendbendE1Devices are graphsIn the studio a device is a drawing: traps on rails, rails meeting at junctions.Not started0 of 9 exercisesStart q0q1HC1→C0coolCXMreplay: the state after each statementE2Programmes and replayIn the studio a programme is a list of statements: p.init places the ions, p.shuttle carries one along a path of nodes, p.gate fires a gate, p.cool cools every ion, p.measure reads ions out.Not started0 of 8 exercisesStart bellearlyR6bR1R2R6R6bR1R2R6R6bE3Rules as propositionsIn Part R the studio checked every programme against the rules: a site holds what it holds, a junction takes one ion at a time, gates happen only where they may.Not started0 of 9 exercisesStart S1standardR1 R2 … R6 …cycloneR1 R2 … no R6E4Rule setsPapers about QCCD machines do not agree on the rules.Not started0 of 7 exercisesStart
Part F · 6 chapters live · in Lean, in this browser

Certificates and the proved checker

What a certificate records, what it means for one to hold, the decision procedure that settles it, and the proof that the procedure is right.

0 of 55 exercisesBadge: Proof checker
a Bell paircertificateLeanF1Certificates: the Bell pair, provedTake one real certificate from the Compilation page, watch it play, prove it holds, and prove three lies about it refused.Not started0 of 8 exercisesStart 1234567891011Implements:11 conditions, 1 brokenF2The specification, condition by conditionLesson F1 printed the specification Implements and read its eleven conditions in one line each.Not started0 of 10 exercisesStart Implements belldecidetrue#evalruns it, proves nothingdecide +kernelkernel computes itnative_decidetrusts the compilerF3Decision proceduresThe checker is one line, check inp := decide (Implements inp).Not started0 of 9 exercisesStart check c= truea BoolImplementsca Propcheck_soundcheck_completeF4Soundness and completenessA checker can be wrong in two directions.Not started0 of 10 exercisesStart the GHZ chainteleportshifted witnessforeign ionsswap_operandsthe pulses refuse itF5The mutation labA checker is worth exactly what it refuses.Not started0 of 10 exercisesStart Lean kernel + propextprovedparser Input.ofJsonbelieveddevice facts (hops)believedcheck_cert's semanticscomputedF6What you trustLesson F1 ended on a warning: a proof is exactly as strong as what it is about.Not started0 of 8 exercisesStart
Part G · 7 chapters live · in Lean, in this browser

Semantics: which gate the pulses make

Exact numbers, the native pulses as matrices, u3 from two pulses, CX from one entangling pulse, stabilizer tableaux, and measurement — without Mathlib.

0 of 65 exercisesBadge: Semanticist
1i−1−iω⟨a, b, c, d, k⟩(a + b·i +(c + d·i)·√2)÷ 2ᵏone spelling eachG1Exact numbersLesson F1 ended on a gap.Not started0 of 10 exercisesStart q0q1H: R, VZCX: R, MS, R, R, RG2The native pulsesA trapped-ion machine does three things to its qubits, and the compiler emits nothing else (the semantic check, check_cert, calls them NATIVE: "the pulses the hardware executes, and so the only gates the semantic half can compose").Not started0 of 10 exercisesStart VZ(φ+λ)R(θ, π/2−λ)u3(θ,φ,λ)H = VZ(π) · R(π/2, −π/2)as the h certificate's witness has itG3u3 from two pulsesEvery one-qubit gate of a circuit (h, s, t, x, a rotation) is a u3, and the compiler replaces every u3 by two native instructions: one physical pulse and one frame update.Not started0 of 9 exercisesStart q0q1MS(π/2)=e^(−iπ/4)G4CX from MSThe only entangling operation of the machine is the Mølmer-Sørensen pulse.Not started0 of 9 exercisesStart the circuitX₀ ↦ Z⊗1Z₀ ↦ X⊗XX₁ ↦ 1⊗XZ₁ ↦ Z⊗Z=the pulsesX₀ ↦ Z⊗1Z₀ ↦ X⊗XX₁ ↦ 1⊗XZ₁ ↦ Z⊗ZG5Stabilizer tableauxA matrix for n qubits has 4ⁿ entries; a BB[[144,12,12]] round has hundreds of qubits.Not started0 of 9 exercisesStart q|0⟩a readout is a CNOTq|0⟩resetCXMMCXin ordermoved earlyG6Measurement and resetA measurement is not a unitary: it reads a qubit and leaves it in the state it read.Not started0 of 10 exercisesStart = CX·(H⊗1)up to a phasetwo witnesses, composedswap_operandscheckersemanticsG7The semantic checkLesson F1 proved that the Bell certificate holds: where every ion is, cycle by cycle, and that every gate's ions are together in a trap that can gate.Not started0 of 8 exercisesStart
Part H · 4 chapters live · in Lean, in this browser

Verify the website yourself

Every compiled case this site publishes, checked by you: in the page for the small ones, with the downloadable checker for the large ones.

0 of 34 exercisesBadge: Auditor
19 certificatesthe GHZ chain: four CNOT meetingsH1The Compilation pagePart H turns the tutorial on the site itself.Not started0 of 9 exercisesStart 1rep9R10C0C1stationary_chain, 17 ionsprovedH2The boardsThe site's leaderboards rank hardware designs by how fast, or how reliably, they run one round of an error-correcting code.Not started0 of 8 exercisesStart 12345678910bundlemetricsR10lean_certificatesemanticsR10 needsthese twoten stagesH3The official graderThe leaderboards of lesson H2 were built by the study's own scripts.Not started0 of 9 exercisesStart circuit.qasm + device$ qccdc compile$ insert_cooling$ mk_qcheck_input$ check_cert --qcheck R10 passedH4Every verdict, reproducedLesson H1 checked the O1 half of R10 on files the site publishes.Not started0 of 8 exercisesStart
Part I · 5 chapters live · in Lean, in this browser

Build your own verified compiler

A compiler for a chain of traps written in Lean and proved correct by construction; then a compiler in any language, validated by the checker; then the Compiler board.

0 of 45 exercisesBadge: Compiler builder
compilemapmoveswitnessescheckerI1A compiler in LeanIn lesson F1 a certificate arrived from our compiler and you checked it.Not started0 of 10 exercisesStart every circuitcompileImplements(compilehome c)I1: checked once per outputI2: proved once, for every outputI2Correct by constructionIn lesson I1 the compiler wrote a certificate and the kernel checked it: one circuit, one check.Not started0 of 9 exercisesStart PythonOCamlRust{ }JSONcheckerprovedACCEPTEDREJECTEDI3Any language, checkedLesson I2's proof works because the compiler is a Lean function.Not started0 of 8 exercisesStart circuit opsqubit mapinitmovesrotationswitnessesfrom the devicegate sitesa hoploop orderI4The certificate formatLesson I3 was about what the proved checker reads.Not started0 of 9 exercisesStart 1your compilervs the referencespeedup, geometric mean1.4×every circuit × device pairnot eligibleI5The Compiler boardThe Leaderboard has two sections.Not started0 of 9 exercisesStart
Part J · 6 chapters live · in Lean, in this browser

Gadgets and fault-tolerant architecture

Places as boxes with doors and promises; the machine's rules as propositions, and why parallel work is safe; designing a floorplan and its traffic; gates built from places and proved, including the T gadget that was not T; why a program of proved gates is the program it says; and Shor's algorithm, fault-tolerant, end to end.

0 of 48 exercisesBadge: Fault-tolerant architect
MSFinoutverified once, used as a boxJ1Places: a gadget is a box with doors and a promiseA fault-tolerant computer is too big to compile ion by ion.Not started0 of 8 exercisesStart timewaitsone bundle per roadat onceJ2The machine's rules, and why parallel work is safeA fault-tolerant machine runs many things at once.Not started0 of 7 exercisesStart closeddoor to doorJ3Floorplans: designing the machine, and what its traffic costsA floorplan says where every place of a machine stands and how roads and wires join them.Not started0 of 9 exercisesStart dataif a: S̄x msoftware PauliJ4Gates from places, and the T gadget that was not TA fault-tolerant machine has no T gate.Not started0 of 9 exercisesStart h qt qcx q r=TagreeJ5Composition: a program of proved gates is the program it saysShor's algorithm for 15, compiled for the site's machine, is 157 instructions after its gates expand — 15 magic states, 29 π/4 gadgets, 44 lattice surgeries — and dozens of measured bits decide what runs.Not started0 of 7 exercisesStart DECorder of7 mod 15= 415 = 3 × 5J6Shor's algorithm, fault-tolerant, end to endShor factors N by finding the order of some a: the smallest r with aʳ = 1 mod N.Not started0 of 8 exercisesStart

The reference

backgroundThe physics, from one trapped ion to the noise modelTraps, qubits, gates, transport, the control system, where the noise comes from and how this website simulates it. the languageEvery statement, with a running exampleThe syntax, what each statement does to the machine, what it costs, and the IR beneath it. the rulesAll 27 rules, each with a programme that passes and one that failsThe verifier's own verdicts, runnable here. compilationFrom QASM to hardware instructions, verifiedThe pipeline on a Bell pair, then every basic gate compiled, mapped, witnessed and checked. evaluationEvery metric, and the noisy circuit a run becomesSpeed, heat, hardware and the logical error rate, each a term of a language; the noise model as text; a Goal 1 entry recomputed. device languageThe architecture description languageOne document describes a machine: its trap graph, zones, wiring and the curves of its primitives. control IRTSIR — the control IRThe eleven verbs a programme is written in, and what each one costs. the rulesThe rules, and what the verifier can honestly say about eachAll 27 rules, what each one checks, and what the verifier can honestly say about it. physics and metalThe electrodes a device impliesFrom the graph to electrodes: the metal a device implies, and its design rules.

A real design

Every leaderboard entry is a worked example: the executing instruction is marked in the programme, the circuit statement it discharges beside it, and #step=N links any step. The fastest verified round of each task: