# Core concepts

Everything in CUDA-Q Logical follows from a small set of ideas. Learn these
eight, and the rest of the system becomes predictable.

The package is `cudaq.logical`, which this documentation names in full when it
refers to a symbol. Code examples import it under the conventional short alias
and use that instead:

```python
import cudaq.logical as cql
```

## 1. Four stages, one direction

Executable intent is refined through exactly four semantic stages
(`cudaq.logical.stages.Stage`):

| Stage                    | Question it answers                                              | Primary IR family |
| ------------------------ | ---------------------------------------------------------------- | ----------------- |
| **P0** unplaced logical  | What logical computation is requested?                           | `qlx`             |
| **P1** placed logical    | Where may each logical owner reside on a logical machine?        | `lvm`             |
| **P2** QEC realization   | Which code, gadgets, and protocols realize it, and at what cost? | `fabric`          |
| **P3** physical schedule | Which carriers and timed events physically realize it?           | `phys`            |

A later stage only adds realization facts — it never silently reinterprets the
logical behavior you asked for. Every stage root is verified and immutable, so
when a lowering fails you fall back to the retained earlier root instead of
repairing in place. `cudaq.logical.compile` produces the P0 root of a
`@cudaq.logical.program`, `cudaq.logical.compiler.place` refines it to a
code-agnostic P1 placement, and selecting codes, gadgets, and protocols produces
P2. Physical lowering and scheduling produce P3. Emitting Stim text consumes a
P2 build; it is an interchange product, not a stage.

## 2. Facets, not extra stages

QEC specifications, gadget realizations, protocol networks, and patch graphs are
**facets** (`cudaq.logical.stages.Facet`). A facet is an independently verified
fact attached to an immutable stage root, not another point in the P0–P3
lowering order. Physical lowering and scheduling attach their own facets the
same way. Several facets can coexist on one root without recompiling the
program. Every pipeline pass declares the facets it requires, provides, and
invalidates; a facet survives a pass unless that pass explicitly invalidates or
recomputes it. A compiled gadget build, for example, is a P2 root carrying
exactly `QEC_SPEC` and `QEC_REALIZATION` — see `build.facets` in concept 5.

## 3. Linear ownership

Quantum values are _linear_: each value has one live owner, and every operation
consumes that owner and produces its successor.

```python
import cudaq.logical as cql

@cql.program
def ownership() -> tuple[bool, bool]:
    q = cql.allocate(1, state=cql.types.zero)
    q[0] = cql.h(q[0])                    # consume q[0], produce its successor
    q[0], z = cql.mpp(cql.types.Z(q[0]))  # nondestructive: the owner survives
    return z, cql.measure_z(q[0])         # destructive: q[0] is gone
```

Rebinding — `q[0] = cudaq.logical.h(q[0])` — is how you write that contract.
Using a consumed value raises `cudaq.logical.errors.UseAfterConsume` at trace
time. The canonical IR checks the same contract independently: every linear SSA
value must have exactly one owner along every execution path. Double
consumption, use-after-measure, and leaks are typed failures, not runtime
surprises.

## 4. Codes, profiles, encodings — three different things

- A **`Code`** is validated algebra: a physical width `n`, a logical width `k`,
  and independent stabilizer and logical-operator bases, all checked at
  construction. Distance is _evidence_, held as a
  `cudaq.logical.codes.Distance`: a bare integer normalizes to `claimed` — a
  recorded assertion, never a proof — while the evidence-bearing constructors
  (`exact`, `lower_bound`, `upper_bound`, `circuit`) require a method and
  provenance.
- A **`CodeProfile`** is an analysis convention over one code: effective
  syndrome generators, meta-checks, and derived boundary maps. Change the
  convention and you get a new profile, not a new code.
- An **`Encoding`** is a reusable logical view: named logical ports, a block ABI
  name, and layout facts. Preparation and conversion are _gadgets_ — an encoding
  never executes circuits.

Every code synthesizes a default profile and encoding, so you write your own
only when you need a genuinely different view. The catalog
(`cudaq.logical.codes`) ships `Steane`, `Repetition`,
`rotated_surface(distance)`, `ReedMuller15`, and `BareQubit`:

```python
import cudaq.logical as cql

steane = cql.codes.Steane                      # the [[7,1,3]] CSS code
assert (steane.n, steane.k) == (7, 1)
assert (steane.d.value, steane.d.status) == (3, "claimed")
```

The two structures most worth keeping apart, side by side:

| Structure  | Holds                                                                                                                                                                  |
| ---------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| `Code`     | physical width `n`, logical width `k`, `Distance` evidence, independent stabilizers, logical X/Z pairs; CSS constructors are adapters into the same normalized algebra |
| `Encoding` | the protected `code`, a selected `profile`, a `name`, the `block` ABI name, ordered `logical_ports`, and layout facts; sealed after validation                         |

## 5. Objectives, gadgets, protocols — claims and proofs

A **gadget** is a realization — a typed circuit over encoded patches — plus a
claim: `implements=<objective>`. That claim is checked. The compiler derives the
gadget's signed symplectic action, matches it against the objective's Clifford
action, and records the equivalence evidence — or fails with a typed diagnostic:

```python
import cudaq.logical as cql

@cql.objective
def terminal_memory(q: cql.types.logical_qubit) -> None:
    cql.discard(q)

@cql.gadget(implements=terminal_memory)
def steane_memory(block: cql.patch[cql.codes.Steane]) -> None:
    block, _ = cql.extract_syndrome(block)
    block, _ = cql.mz(block.data)
    cql.discard(block)

build = cql.compile(steane_memory)
assert build.stage == cql.stages.P2
assert build.facets == (cql.stages.Facet.QEC_SPEC, cql.stages.Facet.QEC_REALIZATION)
```

When several operand-to-port embeddings verify, the compiler refuses to pick one
silently and raises `cudaq.logical.errors.AmbiguousLogicalPortMap`. An explicit
`logical_ports=` mapping is a constraint the verifier checks, never evidence it
trusts.

A **protocol** composes gadget calls with operational policy. The shipped
15-to-1 distillation in `examples/standalone/03_magic_state_distillation.py`
exercises typed resource requests and postselection. Protocols may also use
bounded retry with explicit commit points; retry policy is normalized at
construction into immutable, type-checked structures:

| Type          | Fields                                                                                                                     |
| ------------- | -------------------------------------------------------------------------------------------------------------------------- |
| `RetryPolicy` | positive `max_attempts`; a `RetryExhaustion` — `REPORT_FAILURE`, `ABORT`, or `RETURN_LAST`; an optional typed commit point |
| `CommitPoint` | `before_output(endpoint)` or `before_resource_output()`: the boundary before which an attempt may be replayed safely       |

## 6. Evidence follows the program

Every semantic transition emits evidence records — `pass`, `fail`, or
`unresolved` — or an explicit declaration that evidence is missing.
`build.evidence` lists the records, and `build.status` summarizes the build
(root, stage, facets, and counts by result), as in the gadget build above.
`build.serialize()` captures the whole build — selected definitions, evidence,
and all — and `cudaq.logical.compiler.Build.replay` reopens it in a clean
process with no ambient Python state. The same honesty applies to distances and
estimates: a `claimed` distance stays a claim, and each estimation tier reports
exactly which facts it consumed.

## 7. There is no registry — imports are the linker

CUDA-Q Logical has no global implementation table, and that is deliberate. A
registry would make _import order_ part of your program's semantics: two
sessions that import modules in a different order could select different
physics, and a serialized build could not say what was visible when it was
compiled.

Instead, discovery is scoped and explicit. Each compilation collects candidates
from exactly three places:

1. definitions bound at module scope in **your program's module**;
2. definitions bound at module scope in **your device's module**;
3. definitions exported by a **`cudaq.logical` library submodule you explicitly
   imported** into one of those modules — the import statement is the link act,
   and bare `import cudaq.logical` links nothing.

Each compilation derives this candidate set fresh, filters it by objective and
boundary types, and captures the _selected_ closure into the build:
`build.source_modules` and `build.definitions` record exactly what was visible
and what won. Day to day, you feel three consequences:

- a gadget defined in a helper file you never imported is invisible — the
  failure is a typed "no feasible P2 implementation", not a mystery winner;
- deleting an import genuinely detaches its implementations;
- replaying a build needs no ambient Python state at all.

## 8. Global phase is not observable

**CUDA-Q Logical treats states and operators as projective: an overall phase is
neither observable nor tracked.** The only observables are measurement outcomes,
and those are invariant under an overall phase. Concretely:

- **Synthesis** targets a projective operator-norm bound
  (`cudaq.logical.compiler.synthesize(gate_set=..., precision=...)`), so
  `R_Z(kπ/4) = T^k` holds up to phase.
- **Rotations are 4π-periodic exactly and 2π-periodic up to phase.**
  `cudaq.logical.algebra.Angle` keeps angles as exact rational multiples of π,
  so this stays precise — and the angle you authored is preserved, never
  auto-reduced:

```python
import cudaq.logical as cql

assert cql.algebra.Angle(9, 4).pi_fraction == (9, 4)
assert float(cql.algebra.Angle(9, 4) - cql.algebra.Angle(1, 4)) == float(2 * cql.algebra.pi)
```

The boundary: dropping global phase is safe for a linear, classically
conditioned program measured at the end. CUDA-Q Logical's conditionals are
classical — they condition on measurement outcomes — so no shipped surface needs
to track phase. Quantum-controlled arbitrary unitaries would change that, and
they are out of scope.

## Where the pieces live

| You write                                                | You get                                           | Canonical home                      |
| -------------------------------------------------------- | ------------------------------------------------- | ----------------------------------- |
| `@cudaq.logical.program`                                 | portable P0 logical program                       | your module                         |
| `@cudaq.logical.machine`                                 | logical machine for P1 placement                  | `cudaq.logical.architecture`, yours |
| `@cudaq.logical.code`                                    | validated `Code` + default profile/encoding       | `cudaq.logical.codes`, yours        |
| `@cudaq.logical.gadget` / `@cudaq.logical.protocol`      | verified realization / composition                | yours, `cudaq.logical.protocols`    |
| `cudaq.logical.devices.DeviceBuilder`                    | a device layered across P1, P2, and P3            | `cudaq.logical.devices`             |
| `cudaq.logical.compile` / `cudaq.logical.compiler.place` | immutable, replayable `Build` roots               | `cudaq.logical.compiler`            |
| `cudaq.logical.compiler.schedule`                        | a verified schedule over a P3 event graph         | `cudaq.logical.compiler`            |
| `cudaq.logical.estimate(..., tier=...)`                  | logical, static, analytical, or schedule evidence | `cudaq.logical.estimate`            |
| `cudaq.logical.targets.*`                                | compilation targets that lower a `cudaq.kernel`   | `cudaq.logical.targets`             |

Naming follows PEP 8 throughout — artifact classes are camel case (`Code`,
`Encoding`), while operations, decorators, and constants are snake_case
(`@cudaq.logical.machine`, `cudaq.logical.extract_syndrome`). One deliberate
near-collision to know about: `cudaq.logical.types.X(q)` constructs a Pauli
factor for products, while `cudaq.logical.x(q)` applies the gate.

## Where to go next

- The [architecture reference](../reference/architecture.md) describes the
  dialect stack and pipeline presets that realize these concepts.
- The [use cases](../use-cases/define-a-code.md) put them to work task by task.
- [Examples](../use-cases/examples/index.md) shows them in runnable, shipped
  code.