> ## Documentation Index
> Fetch the complete documentation index at: https://b01t.com/llms.txt
> Use this file to discover all available pages before exploring further.

# b01t's safety model: proven unitary channels at build time

> Learn how b01t catches dirty ancillae and silent decoherence at build time, and why every well-typed @coherent program is a proven unitary channel.

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.

<Warning>
  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.
</Warning>

## 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:

```python theme={null}
# 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.

<Note>
  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.
</Note>

## Certification levels

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

<CardGroup cols={2}>
  <Card title="Certification.SAFE" icon="shield-check">
    Produced by `@coherent`. All scratch registers are managed through the ancilla discipline. Ancilla cleanliness is structurally certified. The Hero Theorem applies.
  </Card>

  <Card title="Certification.PRIMITIVE" icon="wrench">
    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.
  </Card>
</CardGroup>

You can inspect the certification level at runtime:

```python theme={null}
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.

<Tip>
  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.
</Tip>

## What `build_exact()` checks

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

<Steps>
  <Step title="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.
  </Step>

  <Step title="Validates ancilla block structure">
    Confirms that every `with ancilla(...)` block contains at least one complete compute/phase/uncompute cycle, in that order.
  </Step>

  <Step title="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).
  </Step>

  <Step title="Auto-generates uncomputation">
    Computes the gate-by-gate inverse of the `compute` block and inserts it as `uncompute_ops` in the AST.
  </Step>

  <Step title="Returns a certified ExactProgram">
    Returns an immutable `ExactProgram` with `certification = Certification.SAFE`. No simulation was performed.
  </Step>
</Steps>

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.