Skip to main content
This guide walks you through building a complete, certified quantum program from scratch. By the end, you will have written a phase oracle, proven it is a unitary channel, and compiled it to a Qiskit QuantumCircuit — without running a single simulation. The example is a one-qubit phase oracle: it borrows an ancilla qubit, copies information from the system into it, kicks back a phase, and uncomputes. b01t verifies all three steps automatically.
1

Import b01t

Start by importing the components you need. The @coherent decorator marks a function as an exact coherent program. QReg represents a quantum register. The gates (cx, z) come from the closed gate set. Certification is the enum you will check to confirm your program is safe.The ancilla discipline helpers — ancilla, compute, phase, uncompute — come from b01t.kit:
from b01t import coherent, QReg, cx, z, Certification
from b01t.kit import ancilla, compute, phase, uncompute
2

Define a @coherent function

Write your quantum program as a regular Python function and decorate it with @coherent. The function takes QReg arguments — one per quantum register your program operates on.Inside the function, use ancilla as a context manager to borrow a helper qubit. Then describe what happens in three named blocks:
  • compute — copy system information into the ancilla using permutation gates only
  • phase — apply a diagonal rotation to the ancilla
  • uncompute — automatically reverse the compute step, returning the ancilla to |0⟩
@coherent
def oracle(sys: QReg):
    with ancilla(1) as anc:
        compute(lambda: cx(sys[0], anc[0]))
        phase(lambda: z(anc[0]))
        uncompute()
The compute block here uses cx (CNOT), which is a permutation gate — it flips anc[0] if and only if sys[0] is |1⟩. The phase block applies z (a diagonal gate) to kick back a phase. The uncompute() call auto-generates the inverse of the compute block, so the ancilla returns to |0⟩.
You do not write the uncompute operations yourself. b01t derives them automatically from the compute block, ensuring the inverse is structurally correct.
3

Build the program

To produce a certified ExactProgram, call .build_exact() on your decorated function. Pass each register as a (name, size) tuple:
prog = oracle.build_exact(("sys", 1))
This call runs the structural checks. If anything in your program violates the ancilla discipline — wrong gate in a compute block, missing uncompute, entangled ancilla — you get a DSLValidationError here, before any circuit is created.
4

Check the certification

The returned ExactProgram carries a certification field. For a function decorated with @coherent, a successful build always produces Certification.SAFE — a static proof that the program is a unitary channel and the ancilla is clean:
assert prog.certification == Certification.SAFE  # proven unitary, no simulation
This is not a runtime check of a simulation result. It is a structural certificate produced by the build process, backed by a machine-checked proof in Lean 4 (the Hero Theorem).
5

Compile to Qiskit

Once you have a certified program, lower it to b01t’s intermediate representation and compile it to a Qiskit QuantumCircuit using QiskitBackend:
from b01t import QiskitBackend, lower_exact_program

ir = lower_exact_program(prog)
circuit = QiskitBackend().emit(ir)
print(circuit)
The lower_exact_program step converts the ExactProgram AST into the IR that the backend understands. QiskitBackend().emit(ir) then produces a standard Qiskit QuantumCircuit that you can pass to any Qiskit executor or transpiler.

​
Complete example

Here is the full program in one block: 
from b01t import coherent, QReg, cx, z, Certification
from b01t.kit import ancilla, compute, phase, uncompute
from b01t import QiskitBackend, lower_exact_program

@coherent
def oracle(sys: QReg):
    with ancilla(1) as anc:
        compute(lambda: cx(sys[0], anc[0]))
        phase(lambda: z(anc[0]))
        uncompute()

prog = oracle.build_exact(("sys", 1))
assert prog.certification == Certification.SAFE  # proven unitary, no simulation

ir = lower_exact_program(prog)
circuit = QiskitBackend().emit(ir)
print(circuit)

​
Next steps

Ancilla discipline

Learn the rules for compute, phase, and uncompute blocks in depth

Safety model

Understand the Hero Theorem and what Certification.SAFE guarantees

Writing coherent programs

Patterns for larger programs, multiple ancilla cycles, and composition

Qiskit backend

Compilation options, transpilation, and running on real hardware