Logical Clifford+T synthesis

Use cudaq.logical.compiler.synthesize when you want a device-independent logical program expressed in a specific gate set. The result is an ordinary immutable P0 Build: inspect it, serialize it, or pass it to placement and QEC compilation later.

Synthesize a program

The supported gate set is positive-generator Clifford+T:

import cudaq.logical as cql


# Author the rotation at portable P0, before any code or machine is selected.
@cql.program
def ansatz(theta: float) -> bool:
    q = cql.allocate(1, state=cql.types.zero)
    q[0] = cql.rz(q[0], theta)
    return cql.measure_z(q[0])


# Legalize only the logical unitary actions into the requested gate set.
clifford_t = cql.compiler.synthesize(
    ansatz,
    gate_set=cql.compiler.gate_sets.clifford_t,
    parameters={"theta": cql.algebra.pi / 4},
    precision=1e-10,
)

assert clifford_t.stage == cql.stages.P0
assert "pauli_rotation" not in clifford_t.to_mlir()
print(clifford_t.synthesis.t_count)
print(clifford_t.synthesis.clifford_count)

You pass no device=. Preparation, measurement, discard, structured classical control, source locations, and linear ownership remain P0 semantics; only the logical unitary actions are legalized.

cudaq.logical.compiler.gate_sets.clifford_t emits:

H;
positive S;
positive T; and
CX.

Inverse phase gates use positive generators. Pauli and Clifford actions, CZ, and CCZ are decomposed exactly. Static multi-qubit Pauli rotations become local basis changes, a CX parity ladder, one synthesized Z rotation, and uncomputation. The shared CUDA-Q cudaq-synth/gridsynth implementation performs the legalization, and the build records it on its logical_gate_set_legalization evidence record. A final independent verifier (qlx-verify-clifford-t) rejects any logical action left outside the requested gate set.

Precision

precision is the default projective operator-norm bound for each off-lattice rotation:

result = cql.compiler.synthesize(
    ansatz,
    gate_set=cql.compiler.gate_sets.clifford_t,
    parameters={"theta": 0.3},
    precision=1e-8,
)

An explicitly authored rotation precision takes precedence:

@cql.program
def rotation_precision() -> bool:
    q = cql.allocate(1, state=cql.types.zero)
    q[0] = cql.rz(q[0], 0.3, precision=1e-12)
    return cql.measure_z(q[0])

cql.compile(rotation_precision)

Exact rational multiples written with cudaq.logical.algebra.pi retain exact source metadata and take the exact-word fast path (see Magic states and protocols). For float-authored angles, synthesis uses an exact lattice word only when that word meets the requested precision.

Grid synthesis needs a static angle. Specialize runtime ABI parameters through parameters= as shown above. Without specialization, synthesis fails rather than returning a Build that still contains an arbitrary rotation.

Inspect and replay the result

Build.synthesis reports the selected gate set, default precision, and gate counts:

summary = clifford_t.synthesis
print(summary.gate_set)
print(summary.precision)
print(summary.h_count, summary.s_count, summary.t_count, summary.cx_count)

payload = clifford_t.serialize()
replayed = cql.compiler.Build.replay(payload)
assert replayed.synthesis == summary

The Build evidence records the gate-set obligation, the positive-generator convention, the precision policy, and the projective error metric. The Build also serializes the resolved legalization pass recipe, so a replayed build carries the same summary.

Use the pipeline form

cudaq.logical.compiler.synthesize is the convenience API: it executes the pipeline owned by the gate-set value. Compiler-oriented code can request the same pipeline directly:

equivalent = cql.compile(
    ansatz,
    pipeline=cql.compiler.pipelines.clifford_t(precision=1e-10),
    parameters={"theta": cql.algebra.pi / 4},
)

assert equivalent.to_mlir() == clifford_t.to_mlir()

This is a real P0-to-P0 transformation. If you pass an existing P0 Build, you get a new Build, and the source is left unchanged:

source = cql.compile(
    ansatz,
    parameters={"theta": cql.algebra.pi / 4},
)
legalized = cql.compiler.synthesize(
    source,
    gate_set=cql.compiler.gate_sets.clifford_t,
)

Pauli-based computation, still at P0

An estimation flow that consumes Pauli-based computation can add one more device-free P0 transform after synthesis:

pbc = cql.compile(
    clifford_t,
    pipeline=cql.compiler.pipelines.pbc(),
)

assert pbc.stage == cql.stages.P0
assert "#qlx.action<h>" not in pbc.to_mlir()
assert "#qlx.action<t>" not in pbc.to_mlir()
assert "#qlx.action<pauli_rotation>" in pbc.to_mlir()

The qlx-to-pbc pass absorbs the Clifford frame and returns an immutable P0 build holding signed π/4 Pauli-product rotations and pairwise-commuting terminal product measurements. qlx-verify-pbc then checks that contract. Neither pass chooses a code, requests magic states, or inspects a machine.

Static unitary cflow.repeat regions can stay folded through this transform. The supported slice carries logical qubits positionally and requires the current SSA owner at every use. An identity residual Clifford frame retains the source count. Counts zero and one are exact directly; bounded nonidentity residuals are normalized into signed-Clifford periods, a folded quotient, and an optional count-one remainder. Period search is limited to 64 phases and one normalization may clone at most 4096 body operations. Nested repeats are handled innermost-first.

Hidden qubit captures, measurement inside the repeat, unsupported periods, excessive expansion, workload-bearing logical idle, or physical event_id metadata fail closed. Positive-basis source actions must use exact logical-qubit-only signatures with no classical payload or parameter bindings. Every source owner must be measured or explicitly discarded; after the first MPP, no new logical preparation may appear and all owners must be terminally discarded. Authored discard reasons remain distinct from compiler-introduced cleanup of nondestructive-MPP survivors.

When not to synthesize

Do not synthesize early when the intended realization should choose a native rotation or another non-Clifford strategy at P2 selection time — synthesis is an early logical commitment that prices every rotation as a Clifford+T word. In that case, compile the original P0 program instead and let selection see the rotation.

Continue from here

Magic states and protocols — the phase convention, exact angles, and where the T states come from.
Examples — example 01 estimates a CUDA-Q rotation in this gate set end to end.