Detector contracts and Clifford projection

A gadget has a logical action, a realization, encoded input and output boundaries, and an affine outcome map. implements= names the action, while the gadget body describes its realization. A detector contract describes how realization measurements and virtual boundary syndromes determine detector parities and output virtual syndromes.

Gadget terminology

An action is the ideal logical circuit a gadget claims to implement. It can prepare or discard qubits and return measurement outcomes; it need not be a unitary operation. A realization is the circuit over the gadget’s physical code blocks. The affine outcome map converts realization outcomes into action outcomes, which are the gadget’s logical observables.

These concepts are separate from the gadget detector contract, which fixes the virtual detectors, output virtual-syndrome relations, and input/output code presentations. A code presentation selects stabilizer generators and boundary-error coordinates. GadgetContract and CodeProfile are compiler containers supplying those mathematical objects; their other fields do not change the definitions.

Use @cudaq.logical.action to author a reusable ideal circuit. Its default kind="auto" infers whether the circuit is unitary or an instrument. kind="unitary" requires a body of unitary actions, and kind="instrument" permits preparation, measurement, and changed quantum boundaries. CliffordAction remains the narrower signed symplectic description of a Clifford unitary. The verification receipt’s logical_action reports the check of the declared action. The verifier supports signed Clifford unitaries, single-logical signed X/Z eigenstate preparation, and destructive or preserving X/Z measurement. Other objective forms are explicitly unsupported.

Compatibility spellings

The former objective vocabulary remains accepted at compatibility boundaries:

Canonical authoring name	Accepted compatibility name
@cudaq.logical.action	@cudaq.logical.objective
kind="unitary"	kind="action"
ProgramDefinition.action_kind	ProgramDefinition.objective_kind (the explicit unitary kind uses the legacy value "action")
ActionOperandRef, ActionOperands	ObjectiveOperandRef, ObjectiveOperands
ActionMismatch, MissingAction	ObjectiveMismatch, MissingObjective
logical.ActionFamily, logical.SyndromeExtractionAction	logical.ObjectiveFamily, logical.SyndromeExtractionObjective
CompilationContext.action, declare_action	objective, declare_objective
QEC lowering action=, action_family= and corresponding read-only views	objective=, objective_family= and the stored fields

These are alternate spellings of the same values, rather than separately registered actions. Passing both keyword spellings is an error. The public definition kind is "action"; constructing a definition with the legacy kind="objective" normalizes it to that kind.

Saved MLIR and build bundles keep their existing qlx.objective_body, fabric.objective, objective_kind, objective_family, and logical-link objective spellings. Python and C++ expose ActionBodyOp and Fabric ActionOp aliases for these operations. Provider manifest identities also retain their existing wire names. These format choices preserve replay and linkage without requiring a serialized-schema migration.

Placement and scheduling optimization objectives describe costs or solver policies. Their objective names have that separate meaning and are unchanged.

Virtual syndromes and boundary errors

These quantities describe different information at an encoded boundary:

Quantity	Meaning
Measurement outcomes M	Physical realization measurement bits, in execution order.
Virtual syndrome V	Stabilizer signs expected from the available classical information.
Boundary error E	Residual phase-free Pauli error relative to the ideal output on the same outcome branch.
Syndrome coordinate S	Commutation of the boundary error with the code presentation’s listed stabilizer generators.
Logical-effect coordinate L	Logical Pauli effect of that boundary error in the chosen coordinates.

V is a classical expectation; S is a coordinate of a residual Pauli error. A change in an inferred stabilizer sign is written ΔV, not S. The code-presentation map sends E to (S, L). A code presentation may list redundant generators, so its attainable coordinates need not fill the whole declared bit space.

The contract spellings endpoint.syndrome, InputSyndromeRef, and OutputSyndromeAssignment describe virtual syndromes. They do not declare residual-error coordinates. CodeProfile remains the compiler’s larger code algebra container; its selected generators and boundary coordinates supply a code presentation. Contract syndrome bundles currently use the endpoint’s effective stabilizer basis.

Detector map and outcome map

The affine detector map has the form

DM: (M, V_in) -> (D, V_out)

Detector declares one virtual-detector parity. Output syndrome bindings declare the V_out rows. Both may use realization records, incoming virtual syndromes, and constants. Detector rows are intended to vanish on ideal outcomes; the declared family may be redundant and is not assumed to be a basis.

The gadget’s affine outcome map has the separate form

OM: M -> O

LogicalObservable declares one indexed action-outcome parity. Observable rows use measurement records and constants, with no V_in terms. Random action outcomes are valid observables too; they need not be deterministic detectors. When a gadget has an OutcomeMap with RESULT rows, a GadgetContract derives its observables from those rows. Explicit declarations must reproduce that ordered affine table. The broader existing OutcomeMap.input_syndromes API cannot be used in these observable rows.

A gadget detector contract consists of the detector map and the input and output code presentations. GadgetContract is a compiler container that also holds observable and success declarations; those additional fields do not change the mathematical definition of a detector contract. Success rows are acceptance mismatch parities; retry and selection policy stay in the protocol.

Recipe-provided contracts

Surface-library gadgets expose their declared default contract through .contract. Recipes also expose gadget_contract(gadget) functions:

from cudaq.logical.architectures import surface

recipe = surface.definitions(3)
contract = recipe.memory_round.contract
assert contract is surface.gadget_contract(recipe.memory_round)

The Surface recipe returns cached contracts for the gadget objects it creates. A gadget it did not create raises ValueError. For custom gadgets, declare a GadgetContract explicitly or supply a default contract factory, as below.

The surface recipe supplies preparation and memory detectors, Clifford syndrome transfers, and readout observables. Clifford transfers are derived from physical gates, while measurement comparisons are selected by the recipe.

Declare a contract

For a custom gadget, use GadgetContractBuilder to declare how recorded measurements relate to its virtual boundary. This Steane memory round names its extracted syndrome round:

import cudaq.logical as cql


@cql.gadget(implements=cql.logical.idle)
def memory_round(
    block: cql.patch[cql.codes.Steane],
) -> cql.patch[cql.codes.Steane]:
    block, _ = cql.extract_syndrome(block, record="round")
    return block

memory_round.record("round.s0") refers symbolically to the first check result; constructing the reference does not run the gadget. The check indices follow the endpoint code profile’s effective stabilizer ordering.

The incoming virtual syndrome contains the expected stabilizer signs inferred from earlier results. In an ideal round, each current measurement agrees with its incoming expectation, so their XOR forms a detector. The current results then become the outgoing baseline:

builder = cql.gadgets.GadgetContractBuilder(memory_round.interface)
incoming = memory_round.inputs.only().syndrome
outgoing = memory_round.outputs.only().syndrome
records = tuple(memory_round.record(f"round.s{i}") for i in range(incoming.width))

for i, record in enumerate(records):
    builder.detector(incoming[i] ^ record)
builder.bind(outgoing, records)
contract = builder.freeze()

detector declares a parity expected to vanish without errors. bind supplies the complete outgoing virtual syndrome that a subsequent gadget can reference. freeze() produces an immutable GadgetContract; these declarations add no quantum operations or noise probabilities to the realization.

This memory round returns no logical measurement outcome, so it has no observable rows. For a readout gadget, observables come from its declared outcome map. Explicit observable declarations must agree with that map, as explained in Detector map and outcome map.

Compile the contract and verify the module:

build = cql.compile(contract)
assert build.module.operation.verify()

Compilation materializes the authored contract declarations. Python construction and MLIR verification check row structure, record ownership, syndrome bounds, observable indices, and agreement with the outcome map. analysis.edem_from_gadget additionally checks ideal determinism and completeness before constructing an EDEM. It does not prove the declared logical action; use verify_gadget for both checks.

Pass the explicit contract as an occurrence in a closed, compatible contract sequence for compiler.emit_stim. For EDEM construction, pass the gadget and contract=contract to analysis.edem_from_gadget:

model = cql.analysis.edem_from_gadget(memory_round, contract=contract)

No separate compile step is required. Add faults= for an explicit fault set, or noise= and optional depolarizations= for the standard noise policy. An explicit fault set cannot be combined with the standard-noise arguments. The contract is authored here; it is not inferred from the gadget definition.

Declare a default contract

Use @cql.gadget(contract=factory) to attach a reusable contract declaration to a custom gadget. The factory receives the gadget definition and returns its GadgetContract:

def memory_contract(gadget):
    incoming = gadget.inputs.only().syndrome
    outgoing = gadget.outputs.only().syndrome
    records = tuple(gadget.record(f"round.s{i}") for i in range(incoming.width))
    builder = cql.gadgets.GadgetContractBuilder(gadget.interface)
    for i, record in enumerate(records):
        builder.detector(incoming[i] ^ record)
    builder.bind(outgoing, records)
    return builder.freeze()


@cql.gadget(implements=cql.logical.idle, contract=memory_contract)
def declared_memory_round(
    block: cql.patch[cql.codes.Steane],
) -> cql.patch[cql.codes.Steane]:
    block, _ = cql.extract_syndrome(block, record="round")
    return block


model = cql.analysis.edem_from_gadget(declared_memory_round)

declared_memory_round.contract exposes the default declaration. An explicit contract= argument selects a contract for that call. A gadget without a declared default requires contract=; missing declarations raise an error rather than triggering detector inference.

Verify a contract and the logical action

The authored-gadget example runs this workflow and demonstrates a failed logical-action receipt. The physical-memory example applies it to recipe-provided preparation, extraction and readout contracts.

verify_gadget checks a GadgetContract against its gadget’s realization:

RepetitionPatch = cql.patch[cql.codes.Repetition]


@cql.gadget(implements=cql.logical.idle)
def syndrome_round(block: RepetitionPatch) -> RepetitionPatch:
    block, _ = cql.extract_syndrome(block)
    return block


block_in = syndrome_round.inputs.only()
block_out = syndrome_round.outputs.only()
checks = syndrome_round.records.syndrome(0).checks

contract = cql.gadgets.GadgetContract(
    syndrome_round,
    detectors=tuple(
        cql.gadgets.Detector(block_in.syndrome[i] ^ checks[i])
        for i in range(block_in.syndrome.width)),
    boundary={block_out.syndrome: checks},
)
receipt = cql.gadgets.verify_gadget(contract)
assert receipt.detector_contract.outcome_code_rank == 4
assert receipt.logical_action.action == "ql.logical.idle"

Both checks read one Choi probe of the realization. Every logical input is Bell-paired with a reference qubit, the encoded input is placed in an arbitrary stabilizer coset, and the realization’s Clifford projection runs through an outcome-complete symbolic stabilizer simulation over F2:

• Detector contract. Every declared detector and output virtual-syndrome relation must be a deterministic parity of the probed realization, and together with the deterministic combinations of the observables they must generate all of them (the rank condition). The receipt reports outcome_code_rank == detector_rank + deterministic_logical_outcome_rank. For the round above the Choi probe yields a 6 × 2 affine outcome relation with a four-dimensional left kernel, spanned by the two detectors and the two output relations: 4 = 4 + 0.

• Logical behavior. The selected compiled gadget specification supplies the objective and its logical-operand bindings. Unitaries must reproduce every signed Choi relation. Preparations must have the declared logical eigenvalue. Measurements must correlate their mapped result with the corresponding reference Pauli and, for preserving measurements, with the surviving output Pauli. Untouched logical qubits must retain their identity Choi relations. logical_action.verified_checks counts the proved signed relations; logical_rank is its historical spelling, not a general rank.

A unitary may act on selected logical ports within a larger encoded boundary. The remaining logical qubits must retain their identity action. Explicit bindings select the operands; omitted bindings use canonical boundary order.

Failures raise cudaq.logical.errors.GadgetVerificationError and name the condition; its receipt holds the full result. Unsupported claims also raise by default. verify_gadget(..., raise_on_failure=False) returns failed or unsupported receipts for inspection. Invalid declarations, compilation errors and unsupported realization projections still raise diagnostics; inspection receipts require a realization that can be analyzed. A normal return in the default mode always has receipt.verified == True. Omitting a detector fails the rank condition (4 ≠ 3 + 0). Declaring the same round as implements=cql.logical.x passes the contract check, which is blind to the logical action, and fails the action check with a sign mismatch on Z_ref -Z̄; declaring cql.logical.h fails because X_ref Z̄ does not stabilize the Choi state.

The affine outcome map is part of the measurement meaning. Its constant is checked along with its record terms: a uniformly random bit from an unrelated ancilla is not an implementation of logical Z readout. Constants do not change the separate rank/completeness calculation. Every supported check holds for all input syndrome sectors and all ideal random outcomes, including hidden reset outcomes.

Non-Clifford objectives (for example cql.logical.t), general instruments, dynamic feed-forward and subsystem-code verification remain unsupported. Measurement objectives contain one signed single-logical X/Z measurement, with optional affine result processing and either full preservation or full discard of the input logicals. Gates surrounding that ideal measurement, multiple ideal measurements and partial quantum discard remain unsupported. Classical-only objectives cannot pass through an empty set of quantum checks. Inspection receipts report logical_action.status == "unsupported", a reason, and receipt.verified == False. The checks establish ideal determinism and the declared supported logical behavior. They do not prove fault tolerance or noisy circuit distance.

Project the realization

cudaq.logical.compiler.project_clifford returns typed carrier instructions and the existing CompiledInterfaceManifest, without parsing Stim text:

projection = cql.compiler.project_clifford(build, gadget="memory_round")
instructions = projection.instructions
measurements = projection.interface.measurements
record_index = projection.record_indices["round.s0"]
assert measurements[record_index].index == record_index

For a gadget-root Build, gadget= defaults to its root symbol. Other roots require an explicit gadget symbol. The selected gadget must have a linked GadgetSpec, and every measurement needs a stable record name.

Each instruction has a kind, carrier operands or Pauli factors, a qualified site ID, and a measurement start index when applicable. Calls and static repeats are expanded with distinct invocation paths. Site IDs are stable for a fixed realization; compiler rewrites may change them. Record aliases, such as assembled syndrome rows, refer to existing measurement indices and do not add measurements. Ambiguous aliases and record names beginning with the reserved __qlx_ prefix are rejected. Input and output encoded ports are listed separately in GadgetSpec order, including their carrier partitions and patch identities. Preparation and destructive readout therefore retain their asymmetric boundaries.

Currently, fabric.permute projects to ordinary SWAP instructions without retaining that they represent a noiseless relabeling. This limits downstream noise policies; see the permutation limitation.

Projection verifies the module and rejects unsupported operations, recursive calls, non-Clifford gates, and dynamic control. It preserves the source Build and shares the native traversal used for Stim emission. The result describes the ideal realization; projection does not insert noise, propagate faults, produce an EDEM, or prove detector-contract correctness.

Boundary for EDEM producers

Projection stays independent of EDEM storage and ownership. A subsequent Logical analysis owns code algebra, contract verification and fault propagation, then submits coefficients through EDEM’s semantic construction API. Producers name endpoints such as output syndrome of code block 2; they do not assemble GF(2) type tables or packed offsets. EDEM validates the model and returns an owned packed buffer. GF(2) supplies the checked map view and allocation-free apply operation.

The producer integration uses the standalone cudaq-edem distribution as its build and runtime dependency. That wheel supplies cudaq_edem, the native libraries, headers and CMake exports; Logical uses that shared copy rather than bundling another. cudaq-qec can depend on the same distribution.

The native producer hands its caller-held ownership record to Python through the capsule protocol in cudaq/edem/python.h. cudaq_edem.EDEM.adopt validates the packed bytes before consuming ownership, keeps the producer’s lifetime dependency alive, and retains the original payload address. Serialized input can still use EDEM.from_bytes, which copies into aligned storage. Native checked views and C++ objects do not cross this boundary.