Skip to main content
Quantum programs have a class of bug that no type system in any existing framework catches: a helper qubit that was supposed to return to |0⟩ at the end of a computation, but didn’t. The circuit compiles, it runs, and the output looks plausible — but you have been computing with a mixed channel instead of a unitary one the whole time. b01t is built around the single goal of making this class of bug impossible to ship.

​
The core quantum bug

In quantum computing, an ancilla is a temporary helper qubit that you borrow to carry out some intermediate computation. The contract is simple: you return it to |0⟩ when you’re done. If you don’t, the ancilla stays entangled with your system register. Any subsequent operation on the system now has an invisible dependency on a qubit you thought was gone. The program silently degrades from a unitary channel — a reversible, information-preserving transformation — into a mixed channel that loses quantum information. This bug is called a dirty ancilla. It is remarkably easy to write and virtually impossible to catch by inspection.
A dirty ancilla doesn’t throw an error and doesn’t produce an obviously wrong result. It produces a subtly wrong result that may only manifest as statistical noise across many shots, or only when the program is composed with other circuits.

​
Why existing frameworks miss it

Qiskit, Cirq, and Q# all operate on a flat list of gate operations. They have no structural notion of “this qubit is a temporary helper that must be returned clean.” As long as the circuit is syntactically valid, they accept it. Consider the classic mistake: 
# This compiles and runs in Qiskit, Cirq, and Q# — and is silently wrong
@coherent
def broken(sys: QReg):
    with ancilla(1) as anc:
        compute(lambda: h(anc[0]))  # puts ancilla in superposition
        phase(lambda: z(anc[0]))
        uncompute()

# DSLValidationError: gate H is not allowed in exact compute blocks
The intent here is to phase-kick through an ancilla. The programmer puts the ancilla in superposition with H, applies a phase gate, and then “undoes” the H. The reasoning sounds right — H is self-inverse, so H · Z · H should work. But H is not a permutation gate. It creates superposition, so between the compute and uncompute steps the ancilla is entangled with the system. The “uncomputation” does not undo that entanglement. The ancilla is dirty. The program is a mixed channel. b01t rejects this at build time. The compute block accepts only permutation gates. Permutation gates are classical-reversible: they map computational basis states to computational basis states without creating superposition. If you only use permutation gates to copy information into an ancilla, you can always reverse that copy exactly, and the ancilla returns to |0⟩.

​
The Hero Theorem

b01t’s correctness guarantee is machine-checked in Lean 4:
Hero Theorem: every well-typed @coherent program is a proven unitary channel.
“Well-typed” here means the program passed b01t’s build-time checks — specifically, that all ancilla blocks follow the compute/phase/uncompute discipline with the correct gate restrictions. You don’t need to simulate the density matrix. You don’t need to inspect the circuit. If build_exact() returns without raising, the program is structurally certified.
The Lean proof is machine-checked, not just a manual argument. The certification is as strong as the proof assistant, not as strong as the programmer’s intuition.

​
Certification levels

Every ExactProgram carries a certification field that records which level of guarantee the program was built to:

Certification.SAFE

Produced by @coherent. All scratch registers are managed through the ancilla discipline. Ancilla cleanliness is structurally certified. The Hero Theorem applies.

Certification.PRIMITIVE

Produced by @primitive. Uses the exact gate set and is coherent (unitary), but scratch registers are caller-managed. The DSL does not certify ancilla cleanliness — that responsibility is yours.
You can inspect the certification level at runtime: 
from b01t import coherent, QReg, cx, z, Certification
from b01t.kit import ancilla, compute, phase, uncompute

@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

​
The two safety guarantees

A Certification.SAFE program gives you two independent guarantees: 1. Ancilla cleanliness. Every ancilla qubit that enters a with ancilla(...) block exits that block in |0⟩. This is enforced by the gate restrictions on compute and phase blocks, plus the automatic inversion performed by uncompute(). It is a structural property of the program’s AST — it cannot be violated without raising a DSLValidationError. 2. Unitary channel. Because all ancillae are clean and the gate set is exactly {H, S, T, CNOT} and their derivatives, the total transformation is a unitary operator on the system register. No quantum information is lost. The program is safe to compose with other certified programs without worrying about hidden entanglement.
Use @coherent for all production quantum subroutines. Reserve @primitive for low-level building blocks where you are manually managing scratch registers and you know what you are doing.

​
What build_exact() checks

When you call oracle.build_exact(("sys", 1)), b01t:
1

Validates the gate set

Rejects any gate not in the exact set (H, X, Z, S, T, SDG, TDG, CX, CZ, SWAP, CCX, CCZ, MCX, MCZ). Parameterized rotations like rx, ry, and rz are forbidden.
2

Validates ancilla block structure

Confirms that every with ancilla(...) block contains at least one complete compute/phase/uncompute cycle, in that order.
3

Validates gate restrictions

Confirms that compute blocks use only permutation gates (X, CX, CCX, SWAP, MCX) and phase blocks use only diagonal gates (Z, CZ, CCZ, S, SDG, T, TDG, MCZ).
4

Auto-generates uncomputation

Computes the gate-by-gate inverse of the compute block and inserts it as uncompute_ops in the AST.
5

Returns a certified ExactProgram

Returns an immutable ExactProgram with certification = Certification.SAFE. No simulation was performed.
If any step fails, you get a DSLValidationError with a clear message pointing to the exact violation — before any circuit is submitted to a backend.