Bernstein–Vazirani

Reference: the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the Language reference.

What we’re building and why

The Bernstein–Vazirani algorithm solves a problem that would take n queries classically but only one quantum query: given an oracle that computes s · x (mod 2) for an unknown n-bit string s, recover s entirely. It is the textbook demonstration of phase kickback — the mechanism where a computational-basis query gets transformed into a phase that carries information about s, which Hadamard gates then convert into measurable bits.

The algorithm is elegantly simple. Prepare n query qubits in |+⟩^⊗n (all Hadamards), prepare one ancilla in |−⟩ = |1⟩ after H, then apply the oracle as CNOT gates from each query qubit to the ancilla. The phase kickback encodes s into the query qubits’ phases. Applying Hadamards again converts those phases back to computational-basis bits. Measuring yields s directly — in a single shot, deterministically.

This fixture hides s = 110 (qubit 0 and 1 are 1, qubit 2 is 0): n = 3 query qubits plus one ancilla. The oracle applies CNOT @(0, anc) and CNOT @(1, anc) — one CNOT per set bit of s. A single shot recovers s exactly. The program is monomorphized: the parametric hadamard_all(n), tensored/split, and circuit-valued oracles of the general algorithm are flattened into one concrete circuit. This is how Quon handles parameterized algorithms: the elaborator partially evaluates Nat arguments, unrolls for loops, and produces a fixed circuit that the typechecker and optimizer can analyze fully.

Typed annotations

fn bv_oracle_s110(): Circuit<4, 4, 10, Clifford> = circuit {
    X @3
    |> H @0 |> H @1 |> H @2 |> H @3
    |> CNOT @(0, 3) |> CNOT @(1, 3)
    |> H @0 |> H @1 |> H @2
}

The type Circuit<4, 4, 10, Clifford> encodes the algorithm’s structure:

• 4 qubits in and out — three query qubits plus one ancilla. The circuit transforms all four; none are discarded. The depth of 10 counts each gate sequentially under |>.
• Depth bound 10 — X @3 (depth 1) plus four Hadamards (depth 4) plus two CNOTs (depth 2) plus three Hadamards (depth 3) = 1 + 4 + 2 + 3 = 10. Note that these gates act on different qubits but are composed sequentially with |>, so their depths sum rather than take a maximum. A par composition would reduce this, but the algorithm’s structure requires the phases to accumulate in order.
• Clifford class — every gate here (X, H, CNOT) is Clifford. The typechecker infers this and the entire algorithm is efficiently simulable on a stabilizer tableau. This also means clifford_t_opt could apply non-adjacent simplification, but there are no T gates to optimize.

The oracle embeds the entire algorithm in one circuit: the initial X @3 sets the ancilla to |1⟩, the first round of Hadamards creates the |+⟩^⊗ 3 ⊗ |-⟩ state, the CNOTs encode the phase kickback, and the final Hadamards on the query qubits convert phases to bits. The ancilla’s final Hadamard is not applied — it is not needed for the measurement, only for the phase kickback during the CNOT.

Source

The embedded source is test/verify/bernstein_vazirani.qn; the typechecker reference is frontend/tests/fixtures/bernstein_vazirani.qn.

The oracle circuit encodes the full algorithm for the secret string s = 110. The initial X @3 sets the ancilla to |−⟩. The first batch of Hadamards puts all three query qubits into |+⟩ and the ancilla into |−⟩ — the phase kickback eigenstate. The two CNOTs implement the oracle: one CNOT from query qubit 0 to the ancilla, and one from query qubit 1, because s = 110 means bits 0 and 1 are set and bit 2 is not. A CNOT for each set bit is the oracle’s definition. The final Hadamards on the query qubits convert the phase information back into computational-basis bits, so that measuring yields s directly. The ancilla does not get a final Hadamard — it was only needed to make the phase kickback work during the CNOTs.

fn bv_oracle_s110(): Circuit<4, 4, 10, Clifford> = circuit {
    X @3
    |> H @0 |> H @1 |> H @2 |> H @3
    |> CNOT @(0, 3) |> CNOT @(1, 3)
    |> H @0 |> H @1 |> H @2
}

The run block applies the oracle to a 4-qubit register and measures all four qubits. The first three bits (b0, b1, b2) are the query results — they equal the hidden string s = 110. The ancilla bit is irrelevant to the answer but is included in the output tuple because the register has four qubits and every qubit must be measured (the linear type system requires no leaks). A single shot recovers the secret deterministically: the measurement result is (1, 1, 0, ancilla) where ancilla is don’t-care.

fn main(): Q<(Bit, Bit, Bit, Bit)> = run {
    (q0, q1, q2, anc) <- bv_oracle_s110() @ qreg(4)
    b0  <- measure(q0)
    b1  <- measure(q1)
    b2  <- measure(q2)
    anc_bit <- measure(anc)
    return (b0, b1, b2, anc_bit)
}

Compile and simulate

./target/release/quonc test/verify/bernstein_vazirani.qn --emit-qasm > /tmp/bernstein_vazirani.qasm
QUONC=target/release/quonc python test/verify/bernstein_vazirani.py

--dump-ir MLIR excerpts

After lowering to quantum.circ, the ten-gate sequence runs through the fixpoint optimization pipeline. gate_cancellation scans for adjacent self-inverse gate pairs on the same qubit wire:

// The oracle has a sandwich structure on each query qubit:
// H(q_i) |> CNOT(q_i, anc) [if s_i = 1] |> H(q_i)
//
// gate_cancellation: no adjacent H·H pair on the same wire — the CNOT
// sits between them. The H·CNOT·H sandwich is the standard phase-kickback
// pattern; it does NOT cancel.
//
// rotation_merging: no consecutive same-axis rotations — the CNOTs break
// any rotation chain.
//
// clifford_t_opt: stabilizer tableau analysis could in principle find
// non-adjacent Clifford identities, but the oracle is structurally minimal
// for this secret string — two CNOTs, one per set bit.

The optimizer leaves the circuit unchanged. The H · CNOT · H sandwich on each query qubit is the irreducible phase-kickback pattern — the Hadamards cannot cancel because the CNOT sits between them, and the CNOTs themselves are on different qubit pairs. The circuit is already the minimal encoding of “query s = 110”.

What the compiler proves

1. Linear use of all four qubits. The register is allocated, the circuit is applied, and all four qubits are measured. No qubit is left unmeasured or used twice. The linear type system tracks the context through the entire run block.
2. Depth bound ≤ 10. The typechecker proves the circuit depth is at most 10 by summing the depths of the sequentially composed gates. This bound is verified, not estimated.
3. Clifford classification verified. The type system infers Clifford from the gate set (X, H, CNOT are all Clifford) and the composition rule (Clifford ⊑ Clifford under |>). This means the entire algorithm is efficiently classically simulable — a fact that is true of Bernstein–Vazirani and is faithfully reflected in the type.
4. No-cloning enforced. The four qubits are allocated once and consumed once. Any attempt to reuse a measured qubit or copy a quantum value would be a type error caught before lowering.

Expected result

For every shot, classical bits (c0, c1, c2) should equal (1, 1, 0). The ancilla measurement is irrelevant. The bernstein_vazirani.py verifier checks that the set of recovered query-bit triples contains exactly the hidden string.

What to try next

• Change the secret string. Modify the oracle to hide s = 101 by adding CNOT @(2, 3) and removing CNOT @(1, 3). The measurement should recover (1, 0, 1).
• Parametrize the oracle. Write a version that takes the secret string as a List<Bit> and builds the oracle with a for loop, then call it with different strings.
• Insert redundant gates. Add H @0 |> H @0 after the oracle and watch gate_cancellation erase the pair, leaving the output unchanged.

→ Next: Grover search — amplify the marked state with one iteration in the exact two-qubit case.