An ancilla qubit is a temporary helper that you borrow to carry out some intermediate computation. The rule is that when you are done, you must return it to |0⟩ — the same state it started in. If you don’t, the ancilla stays entangled with your system register, and every subsequent gate on your system now has an invisible side-channel. b01t enforces the return contract automatically: if you follow the discipline described on this page, the ancilla is guaranteed clean by construction, not by inspection.
What makes an ancilla dangerous
The danger is not that ancillae are hard to use — it is that the failure mode is invisible. Consider a function that uses an ancilla to compute a temporary flag:
- You copy some information from your system into the ancilla using a CX gate.
- You apply a phase based on the ancilla.
- You “undo” the copy.
If step 3 is a genuine inverse of step 1, the ancilla returns to |0⟩ and the program is a unitary channel. If step 3 is almost an inverse — say, you used H instead of CX in step 1, thinking it would cancel out — then the ancilla is entangled with the system after step 3. The circuit compiles, runs, and produces output. The output is wrong in a way that is very hard to diagnose.
b01t rules out the “almost” case by restricting which gates are allowed in each section of an ancilla block.
The ancilla block
Inside a @coherent function, you open an ancilla block with the ancilla context manager:
from b01t import coherent, QReg, cx, z
from b01t.kit import ancilla, compute, phase, uncompute
@coherent
def my_oracle(sys: QReg):
with ancilla(1) as anc:
compute(lambda: cx(sys[0], anc[0]))
phase(lambda: z(anc[0]))
uncompute()
compute, then either phase or apply, then uncompute. Each section is a lambda that contains gate calls. You cannot skip a section or reorder them — b01t raises DSLValidationError if the structure is violated.
The CPU pattern: compute / phase / uncompute
The CPU pattern (Compute–Phase–Uncompute) is the standard way to use a phase oracle via an ancilla:
compute
Copy information from your system register into the ancilla using only permutation gates — gates that map computational basis states to computational basis states without creating superposition. This is the reversibility contract: permutation gates can always be exactly undone.Allowed gates: x, cx, ccx, swap, mcx
phase
Apply a diagonal gate to the ancilla. Diagonal gates act on the phase of each basis state without mixing them, which is why they compose cleanly with the permutation-based compute step.Allowed gates: z, cz, ccz, s, sdg, t, tdg, mcz
uncompute
Call uncompute() with no arguments. b01t automatically generates the gate-by-gate inverse of your compute block and appends it. You do not write the uncomputation by hand.
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
The CMA pattern: compute / apply / uncompute
The CMA pattern (Compute–Apply–Uncompute) is a second structural form for ancilla blocks. Instead of a phase section, you use an apply section, which may contain any exact gate — but those gates must operate on wires that are disjoint from the wires used in the compute block. This is the PreservesFirst condition: the apply section must not touch the wires that were modified during compute.
from b01t import coherent, QReg, cx, h
from b01t.kit import ancilla, compute, apply, uncompute
@coherent
def entangler(sys: QReg, aux: QReg):
with ancilla(1) as anc:
compute(lambda: cx(sys[0], anc[0]))
# apply() can use any exact gate, but only on wires not in compute
apply(lambda: h(aux[0]))
uncompute()
The disjointness requirement for apply blocks is checked at build time. If any gate in the apply section touches a wire that was also touched in the compute section, b01t raises DSLValidationError.
Gate restrictions
The gate restrictions are what give the discipline its mathematical guarantee. They are not style rules — they are the boundary conditions of the Lean proof.
| Section | Allowed gates | Why |
|---|
compute | x, cx, ccx, swap, mcx | Permutation gates: classical-reversible, no superposition |
phase | z, cz, ccz, s, sdg, t, tdg, mcz | Diagonal gates: act on phases, do not mix basis states |
apply | Any exact gate | Must be on disjoint wires (PreservesFirst condition) |
h — are not allowed in compute or phase blocks. They are available at the top level of a @coherent function, but not inside an ancilla block.
Using h in a compute block is the single most common ancilla bug in quantum programming. b01t rejects it immediately:@coherent
def broken(sys: QReg):
with ancilla(1) as anc:
compute(lambda: h(anc[0])) # wrong: H is not a permutation gate
phase(lambda: z(anc[0]))
uncompute()
# DSLValidationError: gate H is not allowed in exact compute blocks
Automatic uncomputation
The uncompute() function takes no arguments. When you call it, b01t looks at the compute block you already wrote and generates its exact inverse:
- For self-inverse gates (
x, cx, ccx, cz, ccz, swap, mcx, mcz), the inverse is the same gate.
- For
s, the inverse is sdg; for t, the inverse is tdg; and vice versa.
- The sequence is reversed — the last gate in
compute becomes the first gate in uncompute.
You never write the uncomputation by hand. This is intentional: hand-written uncomputation is a common source of bugs (reversed order, wrong inverse, missed gates). b01t generates it mechanically and validates the result.
What happens when you break the rules
Every violation raises DSLValidationError at build time with a specific message:
# Wrong gate in compute block
@coherent
def ex1(sys: QReg):
with ancilla(1) as anc:
compute(lambda: h(anc[0])) # DSLValidationError: gate H is not allowed in exact compute blocks
phase(lambda: z(anc[0]))
uncompute()
# Wrong gate in phase block
@coherent
def ex2(sys: QReg):
with ancilla(1) as anc:
compute(lambda: cx(sys[0], anc[0]))
phase(lambda: h(anc[0])) # DSLValidationError: gate H is not allowed in exact phase blocks
uncompute()
# Missing uncompute
@coherent
def ex3(sys: QReg):
with ancilla(1) as anc:
compute(lambda: cx(sys[0], anc[0]))
phase(lambda: z(anc[0]))
# DSLValidationError: ancilla block exited with incomplete cycle
# Empty ancilla block
@coherent
def ex4(sys: QReg):
with ancilla(1) as anc:
pass
# DSLValidationError: ancilla block must contain at least one compute/phase/uncompute cycle
Multiple cycles in one ancilla block
You can reuse the same ancilla register for multiple compute/phase/uncompute cycles within a single with ancilla(...) block:
from b01t import coherent, QReg, cx, cz, z, s
from b01t.kit import ancilla, compute, phase, uncompute
@coherent
def double_oracle(a: QReg, b: QReg):
with ancilla(1) as anc:
compute(lambda: cx(a[0], anc[0]))
phase(lambda: z(anc[0]))
uncompute()
# second cycle on the same ancilla
compute(lambda: cx(b[0], anc[0]))
phase(lambda: s(anc[0]))
uncompute()