Gadgets and verification
A gadget in CUDA-Q Logical is a bounded, typed realization of a logical
action. Three artifacts travel together through compilation: the
implements= clause states the ideal logical claim, the
cudaq.logical.patch[...] signature states the encoded boundary (code,
encoding, ownership), and the body states the executable realization. The
compiled fabric artifact keeps all three inspectable, and for supported
realization classes the compiler proves the claim instead of trusting it.
What implements= takes
implements= states a claim; the body supplies the realization. The claim
is a declarative description of an ideal logical operation — it never executes.
Instructions like cudaq.logical.h belong in the body, and passing one as the
claim is rejected with a TypeError.
There are two ways to write the claim, and the choice is about where the ideal operation already lives.
Reuse a CUDA-Q kernel as the claim
When the ideal operation already exists as a @cudaq.kernel, pass it directly.
The Carbon code carries two logical qubits per block, so its gadgets implement
paired operations:
@cudaq.kernel
def paired_h(left: cudaq.qubit, right: cudaq.qubit):
h(left)
h(right)
@cudaq.kernel
def paired_cx(
control_left: cudaq.qubit,
control_right: cudaq.qubit,
target_left: cudaq.qubit,
target_right: cudaq.qubit,
):
x.ctrl(control_left, target_left)
x.ctrl(control_right, target_right)
# %%
@cql.gadget(
implements=paired_h,
logical_ports={
"left": "block.q0",
"right": "block.q1",
},
)
def paired_h_gadget(block: cql.patch[Carbon]) -> cql.patch[Carbon]:
block = cql.h(block.data)
for left, right in CARBON_H_SWAPS:
block = cql.cx(block.data, block.data, pairs=((left, right),))
block = cql.cx(block.data, block.data, pairs=((right, left),))
block = cql.cx(block.data, block.data, pairs=((left, right),))
return block
@cql.gadget(
implements=paired_cx,
logical_ports={
"control_left": "control.q0",
"control_right": "control.q1",
"target_left": "target.q0",
"target_right": "target.q1",
},
)
A kernel’s parameters are plain qubits, but a gadget’s inputs are patches, so
something has to say which logical port each parameter denotes. That is
logical_ports=: here left and right name the two logical qubits inside
one Carbon block. Without it, a claim whose parameters do not map unambiguously
onto the patch’s ports is a construction error
(cudaq.logical.errors.AmbiguousLogicalPortMap), never a silent guess.
Protocols take the same implements= field, with one extra form:
cudaq.logical.logical.produce(kind) claims the production of a typed resource
— the shape every distillation factory uses. See
Magic states and protocols.
What the signature and body add
cudaq.logical.patch[cudaq.logical.codes.Steane] states the encoded boundary:
the signature derives the inout encoded port and its linear ownership. The body
states the bounded realization, where cudaq.logical.h(block.data) expands to
one carrier operation per data carrier — “transversal” is a property the
compiler reads off the support map, not a separate instruction.
The compiled artifact keeps claim and realization side by side (abbreviated — the patch types spell out code, encoding, and epoch in full):
fabric.gadget @steane_h(%arg0: !fabric.patch<@Steane, …>) -> !fabric.patch<@Steane, …> {
%0 = fabric.h %arg0 data : !fabric.patch<@Steane, …>
fabric.return %0 : !fabric.patch<@Steane, …>
}
The typed claim is machine-readable from Python: passing the standard action
h to cudaq.logical.gadgets.clifford_action returns
CliffordAction(matrix=((0, 1), (1, 0)), phases=(0, 0), …) — the X/Z swap that
is H. The same accessor applies to a compiled gadget.
Typed records at the boundary
Syndrome-extraction results are first-class typed values, not raw bit vectors:
cudaq.logical.types.record[Code] names the record family of one code, and
gadget signatures may take and return records directly:
import cudaq.logical as cql
@cql.action
def memory_round(qubit: cql.types.logical_qubit) -> cql.types.logical_qubit:
return qubit
@cql.gadget(implements=memory_round)
def extraction_round(
block: cql.patch[cql.codes.Steane],
previous: cql.types.record[cql.codes.Steane],
) -> tuple[cql.patch[cql.codes.Steane], cql.types.record[cql.codes.Steane]]:
block, current = cql.extract_syndrome(block)
return block, current
The compiled boundary speaks the typed fabric.syndrome<@Steane, …> form, and
protocols compose such gadgets by passing records along — a two-round memory
protocol is two ordinary calls, with no annotation glue. Inside a gadget,
cudaq.logical.analysis.count reports the authored operations of the compiled
realization (the quick start shows it on the Steane terminal-memory gadget).
Preparation and destructive measurement
Two boundary patterns cover most library gadgets:
Preparation has no encoded input seam and produces an encoded output — the
cudaq.logical.gadgets.prepare_zero/prepare_plusfactories build exactly this shape for any validated code.Destructive measurement consumes its encoded input and returns classical results. It must not fabricate a live encoded output merely to make the boundary look symmetric.
The shipped Steane example pairs both halves of the pattern — a terminal action and the gadget that realizes it by one syndrome-extraction pass followed by data-qubit readout:
@cql.action
def terminal_memory(qubit: cql.types.logical_qubit) -> None:
cql.discard(qubit)
# %%
# Implement that operation using encoded syndrome extraction and measurement.
@cql.gadget(implements=terminal_memory)
def steane_memory(block: cql.patch[Steane]) -> None:
block, _ = cql.extract_syndrome(block)
block, _ = cql.mz(block.data)
cql.discard(block)
# %%
# Materialize both definitions and inspect the gadget's static operations.
Ownership is linear throughout: consuming a patch twice, or dropping one that is
still live, is a construction error (UseAfterConsume), never a silent no-op.
Selection: retry and postselection belong to the protocol
Execution policy is not hidden inside reusable gadgets; the consuming protocol
states it. Acceptance is explicit with cudaq.logical.postselect — the shipped
15-to-1 distillation protocol accepts exactly when all four even-parity checks
measure +X:
@cql.protocol(implements=cql.logical.produce(cql.logical.T_STATE))
def distill_15to1() -> cql.types.resource[cql.logical.T_STATE]:
raw_states = cql.request_many(
cql.logical.RAW_T_STATE,
count=15,
)
output = cql.prepare_plus(
cql.allocate_patch(cql.codes.BareQubit, region="t_state_factory"))
checks = []
for state in raw_states[:4]:
output, check = cql.unpack_resource(
state,
like=output,
encoding=cql.codes.BareQubit,
)
checks.append(check)
rows = [*checks, output]
for state, rotation in zip(raw_states[4:],
cql.protocols.FIFTEEN_TO_ONE_ROTATION_STEPS):
rows = list(rotation(*rows, state))
rows[4] = cql.protocols.bare_s(rows[4])
for check in rows[:4]:
cql.postselect(
cql.protocols.bare_measure_x(check),
expected=False,
)
return cql.pack_resource(
rows[4],
kind=cql.logical.T_STATE,
)
# %%
Bounded retry is the same shape. It acts on a success predicate derived from one gadget attempt, and you spell out the policy — attempt budget, exhaustion behavior, commit point — at the retry site:
policy = cql.gadgets.RetryPolicy(
max_attempts=8,
exhaustion=cql.gadgets.RetryExhaustion.REPORT_FAILURE,
commit_point=cql.gadgets.before_output(),
)
The compiler tracks predicate provenance: a retry predicate must derive from the
selected attempt, and the retry must carry every live patch result of that
attempt exactly once — an ambiguous or externally observable replay boundary
fails closed. Exhaustion is explicit (RetryExhaustion.REPORT_FAILURE / ABORT
/ RETURN_LAST), and commit points mark where an attempt becomes irreversible
(before_output(...), before_resource_output()).
Verification: claims are checked, not trusted
Gadget contracts can declare virtual detectors, action-outcome observables,
and output virtual-syndrome relations without changing a gadget’s realization.
See Declare a contract
for a worked example of authoring and verifying a custom memory gadget’s
contract. Use GadgetContractBuilder to declare the detector parities and outgoing
syndrome values for a gadget you author.
For a runnable introduction, Verify an authored gadget declares an explicit contract for a Repetition-code syndrome round and inspects the receipt for an incorrect logical claim. Then Physical surface-code memory verifies and composes three recipe-provided gadgets.
Construction and MLIR verification establish local shape, ownership, symbol, and algebra invariants; semantic checks establish that a realization does what it claims. Do not conflate the levels:
Evidence |
What it establishes |
|---|---|
Python construction |
typed fields, linear ownership, boundary liveness |
MLIR verification |
canonical cross-object and stage invariants ( |
code algebra checks |
symplectic rank, commutation, canonical pairing |
action equivalence |
the realization’s induced behavior matches its |
Action equivalence is automatic at construction for code-automorphism
realizations — gadgets whose realization is a single typed permutation of the
code’s carriers. The compiler derives the induced logical action from the code
algebra and compares it with the implements= claim, failing closed on
mismatch: a permutation that is genuinely the identity on the logical qubit
verifies, and one claiming to be a logical H is rejected with a ValueError
naming the action it failed to implement.
For other realization classes the claim is recorded, not derived, until you ask
for it: cudaq.logical.gadgets.verify_gadget checks the realization’s supported
logical behavior, and the gadget’s detector contract, from one Choi-state probe.
A syndrome round that declares the wrong action compiles, and is rejected by
verify_gadget with a sign or basis mismatch on the named Choi stabilizer.
See Detector contracts.
Supported forms are signed Clifford unitaries, single-logical signed X/Z
preparations and destructive or preserving X/Z measurements. The check follows
compiled logical port bindings and the full affine outcome map. Unsupported
claims raise by default; use raise_on_failure=False to inspect their receipts.
A default call returns only when receipt.verified is true.
Design rules that keep the model crisp
Derive canonical facts from the code algebra instead of asking users to repeat them.
Keep the logical action, the realization, and the execution policy in their owning objects — no hidden retry or acceptance inside a gadget.
Use typed endpoints, records, and logical ports instead of raw strings where typed identities exist.
Fail closed when a claim, a boundary, or a predicate provenance cannot be established.
Use ordinary Python modules for reusable gadget families; there is no registry to populate.
Where to go next
Defining codes — the validated algebra that gadgets build on, and the factories that consume it.
The quick start compiles a Steane gadget end to end and counts its authored operations.
Examples links the shipped gadget and protocol sources, including 15-to-1 distillation.