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

# Quick Start: Your First Safe Quantum Program

> Build and certify a phase oracle with b01t in minutes. Walk through imports, the @coherent decorator, build_exact(), certification, and Qiskit compilation.

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.

<Steps>
  <Step title="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`:

    ```python theme={null}
    from b01t import coherent, QReg, cx, z, Certification
    from b01t.kit import ancilla, compute, phase, uncompute
    ```
  </Step>

  <Step title="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⟩

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

    <Note>
      You do not write the uncompute operations yourself. b01t derives them automatically from the compute block, ensuring the inverse is structurally correct.
    </Note>
  </Step>

  <Step title="Build the program">
    To produce a certified `ExactProgram`, call `.build_exact()` on your decorated function. Pass each register as a `(name, size)` tuple:

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

  <Step title="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:

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

  <Step title="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`:

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

## Complete example

Here is the full program in one block:

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

<CardGroup cols={2}>
  <Card title="Ancilla discipline" icon="book" href="/concepts/ancilla-discipline">
    Learn the rules for compute, phase, and uncompute blocks in depth
  </Card>

  <Card title="Safety model" icon="shield" href="/concepts/safety-model">
    Understand the Hero Theorem and what Certification.SAFE guarantees
  </Card>

  <Card title="Writing coherent programs" icon="pencil" href="/guides/writing-coherent-programs">
    Patterns for larger programs, multiple ancilla cycles, and composition
  </Card>

  <Card title="Qiskit backend" icon="circuit-board" href="/guides/qiskit-backend">
    Compilation options, transpilation, and running on real hardware
  </Card>
</CardGroup>