Design typed instruction programs for logical QEC and physical lowering

[qciaran]

Summary

• propose a Rust-owned, first-order InstrProgram dataflow model with thin ergonomic Python bindings
• allow calls to be authored against linkable declarations before semantic definitions or implementations are present
• define QEC instructions as typed gadget contracts with instruction-scoped selectable implementations
• write normal implementation bodies in the same InstrGraph representation, recursively composing lower-level instructions down to consumer-supported primitives
• expose standard PECOS GateType operations as a built-in typed instruction library rather than graph syntax
• treat ProtocolProgram as a validated portable-dialect phase of the same graph model
• model instruction instances as HDL-like cells whose typed resource/value wires cross their boundaries and whose implementations may have hierarchical space-time realizations
• infer concurrency from dataflow, retain structured control above straight-line TickCircuit, and preserve frames, measurements, detectors, observables, and provenance
• lower through PHIR and/or ProtocolProgram to reference Tick output or target backends; treat DEM construction as a separate analysis consumer
• use Guppy only as an optional HUGR-based input whose gadget semantics require an explicit QEC contract
• define one normative initial slice: distance-3 Z-basis surface memory with CX syndrome extraction and parity against the existing TickCircuit

Document map

• design/instr-program.md: reader-oriented overview, surface-memory example, linkage/expansion model, and space-time picture
• design/instr-program-mvp.md: normative first implementation and acceptance tests
• design/instr-program-rationale.md: PECOS/SLR context, detailed Rust model, crate direction, alternatives, roadmap, and open questions
• design/instr-program-spacetime.svg: coarse and expanded view of nested instruction volumes and resource wires

Scope

This is a design-only draft. The MVP uses the fully declared, statically provided subset while preserving separate declaration, linking, and implementation phases. Guppy generation, PHIR integration, general packages, dynamic control, target mapping, higher-level noise dialects, placed space-time tooling, and interactive visualization are deferred from the first implementation.

Testing

Documentation-only change. Cross-link, Markdown fence, whitespace, reference-constructor, confidential-term, XML, rendered-diagram, and Git diff checks pass.

[peter-campora]

I don't understand what "typed resources" means here. There's some sort of type system for the highest most opaque representation?

[qciaran]

ChatGPT: Yes. Here "resource" means a value flowing along graph edges, not necessarily an allocated hardware resource. Every value has a registered (possibly domain-opaque) type. The generic graph understands port compatibility plus traits such as linear versus copyable, but it does not interpret surface-code semantics. For example, QEC may define a linear LogicalPatch<RotatedSurfacePatch[d=3], Active>, while a measurement bit is copyable and a PauliByproduct may be linear. This lets the generic verifier catch wrong ports, incompatible input/output types, and double use of a consumed patch. "Typed values/resources" would be clearer than the current shorthand, so I will clarify that wording in the document.

[peter-campora]

Then sequences of statements representing instruction sequences on the code form a program, module, or graph? Is the ability to modularize definitions across files in scope?

[qciaran]

ChatGPT: That is the intended split:

• InstrGraph is one typed body: calls, value edges, and structured control regions.
• InstrModule is a reusable, parameterized definition with a signature and an InstrGraph body.
• InstrProgram is the compilation/linkage unit that owns or imports module definitions, symbol identities, entry points, and exports.

Cross-file modularization is in scope at the artifact level: modules should be independently serializable, hashable/versioned, and importable by stable identity, so Rust or Python code in different files/packages can build and link them. A dedicated textual language and its filesystem/package syntax are not required for the first implementation. I will make that distinction explicit near this diagram.

[peter-campora]

@qciaran seems like it wants a linear/affine type system lol

[qciaran]

ChatGPT: Yes—that is basically the ownership pressure here. QEC-block handles must not be duplicated or consumed twice, so successful control paths naturally want linear use. Affine use becomes useful for explicitly abandoned/discarded blocks and abort or failure paths (at most once rather than exactly once), while measurement and configuration values can be copyable/unrestricted. I do not think the MVP needs a general-purpose linear type calculus: it can begin with Linear | Copyable, require each linear value to be consumed or exported, and add an explicit discard plus richer affine/control-flow rules when those use cases are implemented. Rust and the thin Python API should infer and enforce this; ordinary circuit authors should not have to spell the ownership types themselves.

[qciaran]

Hmmm, linear types seem to add coding complexity though... when simple checks on whether resources have be reused or not might be sufficient...

[qciaran]

ChatGPT: I agree with this correction. Calling it a linear/affine type system overstates what the authoring API needs. The value can keep its ordinary domain type (patch, result, frame, and so on), while the graph verifier separately applies a small use policy such as SingleUse | Reusable. A patch-producing call returns a new handle; attempting to reuse the consumed handle is then just a clear validation error. Exact lifecycle requirements—such as whether a live patch must eventually be measured, exported, or explicitly discarded—can remain dialect validation rather than become general type-system machinery. This retains the useful safety check without making users write or reason about linear types.

[peter-campora]

I really don't know what elaboration means here? Is it some sort of down-selecting details of a code? I thought that would be more of the "explicit InstrSet resolution below, but I probably am misunderstanding that.

[qciaran]

ChatGPT: Elaboration is intended to be structural/template processing, not implementation selection. It resolves module/instruction symbols, binds and canonicalizes supplied parameters, specializes reusable module instances, unifies type variables, and computes concrete output types. For example, calling a generic teleport<P, rounds> module with a distance-3 patch and rounds=3 produces a concrete typed module instance. The following InstrSet resolution stage then chooses implementations such as SZZ versus CX syndrome extraction or transversal versus surgery. A named profile may elaborate into explicit resolution preferences, but it must not itself silently select an implementation. I agree the term and boundary need a short definition in the summary.

[peter-campora]

I see, I think I kind of understand the "types" now. We want to make sure a transversal CX for examples takes 2 code blocks as input, etc?

I guess my question becomes, is this program representation intended for program based construction (in which case a lack of type checking and just thinking about "well formalness" of a given series of operations suffices) or is it intended for by hand authoring (in which case, a more rigorous type system is good for putting guard rails on programmers so long as it isn't too onerous to deal with)?

[qciaran]

ChatGPT: Yes, a logical/transversal CX instruction has two typed code-block inputs and two replacement block outputs; arity is part of its public signature. Geometry matching or whether a particular transversal construction supports those blocks belongs to the selected implementation's supports check, not necessarily to the generic type system.

The representation is intended to be the shared artifact for both hand authoring and programmatic generation. Generated programs benefit from the same validation because generators, imports, rewrites, and implementation composition can still produce invalid ownership or port wiring. For hand authoring, the Python/Rust builders should infer result types and make valid composition easy.

I think of the checks in three layers:

1. Generic construction checks arity, named ports, type compatibility, linear use, and branch/loop joins.
2. Resolution checks implementation-specific facts such as matching patch geometry, orientation, adjacency, or supported bases.
3. QEC verification checks that the resolved plan actually realizes the declared logical transformation.

So the type system should provide useful guardrails, but should stay a compact runtime/serialized type algebra rather than requiring users to write elaborate Rust-style type expressions. In this context, well-formedness is essentially what the first layer of type checking establishes.

[qciaran]

Yeah, I basically told it I want to think of "gadgets" as blocks that take typed code block inputs and returned typed code block outputs as a gadget might do some sort of transformation on the code blocks

[qciaran]

ChatGPT: Exactly—that is the central QEC mental model. Building on Ciaran's comment:

• QecInstr is the gadget interface/contract: named typed code-block inputs and outputs plus the declared logical relation or transformation.
• QecInstrImpl is one selectable way to realize that gadget.
• QecInstrPlan is the concrete realization for the bound input patches and parameters.
• InstrGraph composes gadget instances by wiring compatible output values into later inputs.

This also covers more than ordinary gates: syndrome extraction can preserve the block type and declare logical identity; code switching can return a different code-block type; merge/split can change arity; preparation and destructive measurement can create or consume blocks. A transversal CX is then one implementation of a two-block logical-CX gadget, with its additional geometry restrictions checked during implementation resolution.

“Gadget” is a useful explanatory analogy. I would probably retain QecInstr as the API term because gadget is used in several narrower ways in QEC, but the document can use this analogy to make the abstraction more immediate.

[qciaran]

Ah, it got to the comment before me. lol

[peter-campora]

It may be nice to start with a high-level purpose statement as the first part of the summary. The first sentence seems like a good scoping of creating a program format users can stitch together and then lower to different formats, which sounds very similar to SLR. So, there's not a clear sense to how this differs to SLR in terms of use case, just in representation/implementation details.

[qciaran]

It was inspired by SLR and this may be its replacement. As well as inspired by older representations I had... plus wanting to go in an HDL direction so we can reuse one representation at multiple levels of abstraction. But yeah, good call out.

[qciaran]

ChatGPT: Addressed in fdc488b. The summary now starts with the user-facing purpose: an HDL-like hierarchy that lets different users reason at the logical, gadget/protocol, resource and space-time, physical-circuit, or executable level while opening black boxes only when needed. It also now describes the QEC direction as an evolutionary successor to SLR—informally an "SLR 2.0"—and distinguishes it through typed gadget interfaces, hierarchy, late implementation selection, shared space-time/visualization views, and physical lowering. The design does not make SLR a dependency or assume immediate replacement; deprecation would follow working feature and migration parity.

[peter-campora]

Left a bunch of questions and comments.

[qciaran]

ChatGPT: Incorporated additional design review in aa519b5. The main clarifications are:

• Resource safety is now a small, orthogonal SingleUse | Reusable policy rather than a proposed general linear/affine type system. QEC lifecycle obligations remain dialect validation.
• A normative identity model separates persistent CodeBlockInstanceId, transient ValueId, stable CodeElementId, implementation-local ProtocolWireId, semantic MeasurementId, and later target bindings.
• The former physical-plan seam is now explicitly ProtocolPhysicalPlan: portable physical intent with operation dependencies, resource roles/lifetimes, atomic-stage constraints, capability requirements, and semantic ledgers, but no final target addresses or authoritative time.
• ScheduledPhysicalPlan and optional ExecutionTrace are separate refinements that add bindings, ordering, results, branches, and timing without replacing PECOS semantic identities.
• Implementation compatibility uses structured SupportAssessment data, including reason codes, capability/resource requirements, and deferred feasibility. Explicit implementation choices remain hard constraints.
• External instruction sets have a versioned package/fingerprint/digest contract rather than process-global registration.
• Hierarchy, symbolic repetition, lazy expansion, and streaming/sharded plan consumption are explicit scalability requirements.
• Backend conformance compares logical action, partial order, lifetimes, measurement/detector/observable ledgers, frames, and provenance. Exact tick equality is required only when both routes promise the same scheduling policy.

The MVP remains intentionally narrow: it implements the portable protocol plan and a reference schedule, while target mapping, execution-trace import, dynamic control, and richer planning remain deferred behind the now-explicit artifact boundaries.

[ciaranra]

Deep review

Reviewed at aa519b5b4. Three independent adversarial reviews were run blind to each other; every finding below was re-verified against the code before being recorded here.

Verdict: revise. The problem is real and the architectural instincts are sound. The factual grounding is unusually good for a document this size — roughly a dozen claims about existing APIs were spot-checked (tick_circuit_to_stim, GuppyDemBuilder.build including the no-Stim claim, generate_stim_from_patch, LogicalCircuitBuilder.to_stim, the PHIR logical_gate dialect op, all of #508–#516) and all held. The design should not be built as written, for three reasons.

---

1. The MVP's cost is invisible

instr-program-mvp.md:306-307 step 4 reads "Adapt/reuse existing patch geometry and surface planning", and :249 requires the direct route to import neither Python nor Guppy. None of that planning exists in Rust. crates/pecos-qec/src/surface.rs:58 SurfaceCode has no coordinate map, and check_schedule() (:209) derives a trivial all-X-then-all-Z two-round grouping with no CNOT order or ancilla assignment. Everything else is Python:

File	Lines
qec/surface/circuit_builder.py	4155
qec/surface/logical_circuit.py	1596
qec/surface/patch.py	546
qec/surface/_check_plan.py	486
qec/surface/_clifford_deformation.py	326
qec/surface/_ancilla_batching.py	225
qec/surface/schedule.py	188
total	~7522

Plus _detection_events.py, the Guppy emitter (slr/ast/codegen/guppy.py), and the QIS-trace-to-TickCircuit replay (_qis_trace_replay.py). The "minimum viable" slice silently contains a multi-thousand-line Python-to-Rust port of the surface planning stack.

Please name it as a work item with its own estimate, or drop the Rust-only requirement from the MVP.

2. Cross-call detector construction has no owner, and the MVP demo needs it

qec/surface/logical_circuit.py:1341-1356 builds a 3-body cross-patch detector at a transversal-CX boundary: post_ctrl_X XOR pre_ctrl_X XOR pre_tgt_X. That detector spans four InstrCalls across two block instances.

The design assigns detector definitions to per-call QecInstrPlans composed into ProtocolPhysicalPlan (instr-program-mvp.md:210-211,223) and forbids backends from reconstructing detector boundaries (:226-228). No per-call plan can emit this detector, and no composition rule appears anywhere in the 4004 lines — only a post-hoc "availability of detector-boundary rules" check (surface-logical-circuit-guppy.md:2404-2405) with no mechanism behind it.

This is not a future concern: the MVP demo is exactly prepare / syn_extract / transversal-CX / syn_extract / measure, and instr-program-mvp.md:325 requires its DEM to match an existing PECOS reference.

Two adjacent gaps in the same area:

• Stabilizer-frame epoch. After transversal H the X/Z check labelling swaps. The reference tracks this as PatchState.x_z_swapped (logical_circuit.py:64, used at :1288-1314). QecBlockType carries code spec + logical count + Declared|Active only (surface-logical-circuit-guppy.md:731-739), so the next syn_extract implementation has no way to see the swap. :3581 lists "H followed by syndrome extraction with swapped stabilizer interpretation" as a test with no mechanism behind it.
• Observable propagation. The reference carries x_entangled_with / z_entangled_with / z_obs_includes / x_obs_includes across operations (logical_circuit.py:65-74). surface.measure is "one active patch → one logical result" (instr-program-mvp.md:191) with no access to that history. The MVP demo happens to be safe because Z_c and X_t are both CX-invariant, which conceals the gap rather than avoiding it.

Related: the MVP has no concurrency or round-alignment construct at all. graph.parallel() appears only in the companion document; the sole hit in the MVP is :217, inside ProtocolPhysicalPlan. The control and target syn_extract(rounds=3) calls in the demo are dataflow-independent and therefore unordered, but the 3-body detectors require their rounds to be aligned. As written the MVP cannot express the experiment it demands.

3. Two prior generations of this design are in the repo and go uncited

python/quantum-pecos/src/pecos/qeccs/ is a shipped, layered, code-agnostic QEC abstraction with selectable implementations:

• default_qecc.py:40 DefaultQECC — an instruction set with per-instruction plan caching, described in its own docstring
• default_logical_instruction.py:32 DefaultLogicalInstruction — a definition identity plus a parameter bag bound to an owning code
• surface_4444/instructions.py:36,235,305 — InstrSynExtraction, InstrInitZero, InstrInitPlus: the MVP's exact vocabulary, mirrored in surface_medial_4444/ and color_488/
• color_488/circuit_implementation1.py:28 OneAncillaPerCheck — a named, selectable implementation object, i.e. a QecInstrImpl, already built for a different code family
• Typed interfaces at protocols.py:408,436,481
• Still load-bearing: analysis/threshold_tools.py:32, tools/threshold_tools.py:32

grep -c "qeccs\|QECC\|Surface4444\|OneAncillaPerCheck" over both documents returns 0 — not in "Relationship to existing code", not in "Alternatives considered", not in "Motivation".

Separately, surface-logical-circuit-guppy.md:25-27 describes "reviving earlier PECOS QuantumCircuit and LogicalCircuit ideas". LogicalCircuit is live code (circuits/logical_circuit.py:42, used in analysis/fault_tolerance_checks.py and analysis/tool_collection.py) — and an instructive failure: it stores logical gates in a list parallel to the underlying circuit (:70) while append only calls add_ticks(1) on the real TickCircuit (:75). That is precisely the two-parallel-state-models trap this design correctly forbids at :288-290 and :441-445.

Something caused the team to build pecos.qec.surface alongside pecos.qeccs rather than extend it. That history is the highest-value input to this design. A two-page retrospective is the cheapest possible de-risking step, and it doubles as the specification for what the new layer must not repeat.

---

Blocking correctness issues in the documents

• SurfacePatch.rotated(3) does not exist. 16 occurrences across both documents, including line 28 of the normative MVP demo. rotated is a read-only bool property (patch.py:386); the constructor is SurfacePatch.create(distance=..., dx=..., dz=..., orientation=..., *, rotated=True) (patch.py:302); SurfacePatchBuilder.rotated() (patch.py:520) takes no arguments. SurfacePatch.rotated(3) raises TypeError. Every code example in both documents fails on its first line.
• TickCircuit cannot express classical control at all. crates/pecos-core/src/gates.rs:42 Gate has no condition field. crates/pecos-quantum/src/circuit.rs:140 fn condition(&self, _gate) -> Option<(ClassicalBitId, bool)> { None } is a trait default with zero implementors repo-wide. crates/pecos-qasm/src/lib.rs:57 already disables a module over this (// TODO: requires DagCircuit classical bit API). So the conditional-region and Pauli-frame apparatus at surface-logical-circuit-guppy.md:1341-1560 has exactly one lowering target today, the Guppy route, and the direct-vs-Guppy equivalence premise holds only for straight-line circuits. Stages 5 and 6 depend on a classical-control model that does not exist and is not scoped anywhere in this design.
• The crate boundary is left open and the document's own layout is cyclic. :309-312 places resolved-QEC-to-PHIR lowering — including "resolved QEC calls and plans to typed QEC dialect operations" (:2695) — inside pecos_phir::instr_lowering, requiring pecos-phir → pecos-qec. Open question 8 (:3635-3637) simultaneously proposes the generic layer live inside pecos-phir alongside pecos_qec::instr (:314), requiring pecos-qec → pecos-phir. Today the crates are siblings with no edge; crates/pecos-phir/Cargo.toml depends only on pecos-core and pecos-engines — notably not pecos-quantum, so a pecos-instr touching TickCircuit under PHIR also inverts the current layering. Separately, pecos-phir already ships a "qec" dialect namespace (crates/pecos-phir/src/dialect.rs:245) unrelated to the pecos-qec crate; the clash is unaddressed. Stage 0 must settle this before any code.
• The measurement-identity ladder is wrong about where identity collapses. :2657-2683 says a record offset is "computed only at export" to Stim. The native DEM already stores offsets: DetectorDef.records: SmallVec<[i32; 2]>, documented as "negative indices from end of record" (crates/pecos-qec/src/fault_tolerance/dem_builder/types.rs:1923), fed as offset JSON from qec/dem.py:1310. Identity collapses one stage earlier than claimed, and instr-program-mvp.md:335-336 gates acceptance on identity round-trip across that boundary. MeasurementId also collides with two existing identities: crates/pecos-core/src/meas_id.rs:48 MeasId (whose field is private, contra the quote in design/measurement-id-annotations.md) and crates/pecos-qec/src/fault_tolerance/propagator/types.rs:279 MeasurementId {tick, qubit, basis}. An explicit SemanticMeasurementId → MeasId → record offset map would settle it.
• "Deterministic resolution" is several named holes. No terminal state for Deferred (:983,1017 vs :993-994 — a program with a deferred candidate is defined into a state it can never leave). .using(...) spans three name spaces — "szz" (instr-program-mvp.md:35), surface.syndrome_szz (:2906), pecos.surface/syndrome_szz@1 (:2147) — with no scoping rule, and "transversal" is reused for both surface.h and surface.cx, so it must be instruction-scoped, which is never stated. No candidate or map iteration order, despite byte-equivalent Rust/Python artifacts being an acceptance criterion. No cycle detection or termination measure for composite implementations that expand into instructions selecting themselves. Selection is per-call and local while support is inter-call.
• The two documents contradict each other on the first slice. instr-program-mvp.md:57 program.resolve() versus :2716 program.resolve(context=surface.lowering_context()) — assess_support requires a LoweringContext (:699-703) that the MVP never mentions, so the MVP's resolution step cannot call the MVP's own support API. PHIR is deferred entirely by the MVP (:284) and required in the first slice by the companion (:3644-3650). SupportAssessment is two-valued in one (:142-145) and three-valued in the other (:982-994). Both claim normative status; please say which governs.
• Two worked examples violate the documents' own SingleUse/SSA rules. The teleport module body (:1238-1282) consumes bell and destination repeatedly without rebinding and exports the pre-correction version; the SpaceTimeProgram example (:1842-1859) computes data_prepared / target_prepared / corrected and then passes the original data and target onward. append's return discipline is also inconsistent across three adjacent examples (:2166 discards, :2301 rebinds, :2321 does both, all with the same 1-in/1-out shape). Pinning the authoring model as cursor-mutating or SSA-rebinding resolves all of these; the repaired examples make good validator fixtures.
• Pauli frames have no defined seam. Frame merge at a branch join is undefined — the join rule checks only arity and type compatibility (:1373) while frames attach to value versions (:1480-1496) and are not part of the type. PhysicalPauliFrame is defined over mapped physical-qubit identities (:1506-1511) yet appears in the resolved program before target binding (:2511-2528), while ProtocolPhysicalPlan explicitly lacks physical addresses (:2544-2549). Before mapping it should be expressed over CodeElementId or ProtocolWireId. The existing frame machinery in crates/pecos-decoder-core/src/pauli_frame.rs and crates/pecos-qec/src/fault_tolerance/pauli_frame.rs is not accounted for either.
• The Rust and Python patch types are not losslessly interconvertible today. Python supports independent dx/dz down to 1 (patch.py:302-348); Rust SurfaceCode::new rejects dx < 3 or dz < 3 and then uses d = dx.min(dz) (crates/pecos-qec/src/surface.rs:110-124), discarding asymmetry. Python also treats one-ancilla-per-stabilizer as patch metadata (patch.py:276-284) while the new architecture puts syndrome ancillas in protocol layout (:390-417). The "lossless adapter" (instr-program-mvp.md:203-206) needs a concrete PatchSpec schema and parity fixtures — rotated, standard, asymmetric, repetition, distance-1 — before it can be called lossless. Relatedly, the current transversal-CX support predicate claims identical geometry but checks only equal num_data (logical_circuit.py:408-428), so it should not be reused unchanged.

Smaller corrections

• _check_plan.py is already a working miniature of the proposed resolver: resolve_surface_check_plan (:314) → ResolvedSurfaceCheckPlan (:303), with canonical_check_plan_json (:280), _semantic_hash (:297) and a renderer version guard (:381); sibling ResolvedSurfaceCliffordFrame at _clifford_deformation.py:156. Named options → canonicalize → semantic hash → resolved artifact, in the exact domain. Worth generalizing rather than building a parallel resolver.
• The Bevy justification does not hold. :2040-2041 argues an integration spike is "particularly reasonable" because PECOS and Bevy 0.19 both use wgpu 29. PECOS's half is true (Cargo.toml:125), but wgpu has exactly one consumer (crates/pecos-gpu-sims), which a viewer crate would not share, and bevy appears zero times in Cargo.toml and Cargo.lock. The design also requires Bevy stay out of the core graph (:2048, :3327), so version alignment buys nothing.
• pecos_rslib.qec does not export StabilizerCode (:429-431). It is bound at the root module (python/pecos-rslib/src/stabilizer_code_bindings.rs:218); register_qec_module (fault_tolerance_bindings.rs:7536) has no such class.
• hugr_to_dag_circuit is described as importing "a restricted straight-line quantum subset" (:2880-2882); there is no enforced restriction, only silent dropping — crates/pecos-quantum/src/hugr_convert.rs:600-659 continues past any non-extension node, any non-tket.quantum op, and any unmapped gate name, and its own doc comment warns qubit-identity tracking may fail on Guppy CFG/DFG HUGRs. Building HugrInstrImporter on it contradicts the test criterion at :3404-3406.
• The Python HUGR→SLR path is cited as recognizing structured conditionals and loops (:2882-2883). circuit_converters/hugr_to_ast.py:663-671 hard-rejects any HUGR containing a TailLoop node, and the surviving CFG-back-edge WhileStmt derives its condition from a name heuristic (:962-968).
• add_memory's position dependence is asymmetric: is_first is a single global flag while is_last is per patch (logical_circuit.py:960,980), so a patch first appearing in a later MEMORY op never gets preparation emitted (:1114). The compatibility mapping at :2930-2933 inherits this.
• surface.inject_t(...) (:2264) should flag that the existing helper prepares |+⟩, not |T⟩, and is documented as distance-1 and non-fault-tolerant (logical_circuit.py:373-380). Open question 5 gestures at this; the API example does not.
• reference_schedule (instr-program-mvp.md:59,240) and noise_model (:60,247) are free variables with no type, contents, or relation to make_surface_code's qubit numbering — yet :325 requires matching an existing reference and :320 requires byte-equivalence. For comparison, build_dem_from_guppy today takes roughly 30 noise kwargs (qec/dem.py:1399-1439).
• QecLogicalTransform is never stated to be an ideal/noiseless action contract. A bare syndrome round is logically identity only conditioned on successful decoding, and the design explicitly notes decoding has not occurred (:830-834) while imposing a proof obligation that a plan realize the declared transformation (:780-784). One sentence settles whether the Define QEC circuit synthesis and semantic verification boundary #513 verification boundary is well posed.

A process note

design/*.md is outside the doc-test framework (scripts/docs/generate_doc_tests.py does not scan it), and this PR's testing note reports only markdown fence, whitespace, and diff checks. That is how 16 calls to a non-existent constructor reached a document that declares itself normative. Either restrict normative examples to a form the doc tests can execute, or mark the blocks explicitly as illustrative pseudocode.

Suggested sequence

0. Write the pecos/qeccs/ + LogicalCircuit retrospective — two pages, cheapest step, and it may change the shape of everything after it.
1. Fix SurfacePatch.rotated(3) (16 sites) and repair the two examples that violate the documents' own SingleUse rules.
2. Complete Stage 0 and fold the crate-boundary answer into the design, including the "qec" dialect namespace clash.
3. Specify cross-call detector composition, the stabilizer-frame epoch, and observable propagation — pointing at logical_circuit.py:1316-1362 and :51-74 as the behaviour that must be reproduced, and naming what replaces PatchState.
4. Give the MVP a round-alignment construct, or drop transversal CX from it.
5. Define reference_schedule and noise_model; without them no MVP acceptance criterion is testable.
6. Name the Python-to-Rust surface-planning port as an explicit work item and restage the MVP into independently testable slices.
7. Scope the TickCircuit classical-control prerequisite, or declare Stages 5–6 blocked on separate work.

---

How this review was run

The branch was checked out read-only at aa519b5b4 so every reviewer read the two documents alongside the code at that commit. Three reviewers then ran concurrently and blind — to each other and to the fusing reviewer's own read — each given only the documents and the claim to verify ("this design is sound, internally consistent, and implementable on PECOS as it actually exists"), with file:line citations required for every finding: two Claude-family arms (a fresh-context generalist, and a complexity-and-scope lens on Opus at high reasoning effort) and one Codex arm (gpt-5.6-sol, high reasoning effort, read-only sandbox). All three returned "revise" independently.

Findings were then fused rather than concatenated: each one was re-checked against the code before being recorded here, and the ones that did not hold were dropped. Corroboration across arms raised confidence; several of the sharpest items above are solo catches from a single arm.

Two caveats worth stating. Two of the three arms are Claude-family, so cross-model independence rests on the Codex arm alone — though that arm did produce solo findings the others missed, including the dx < 3 / d = dx.min(dz) patch-conversion gap. And a panel can share a blind spot: the one identified here is the process note above, which no arm raised on its own.

[ciaranra]

Deep review, round 2

Reviewed at aa519b5b4, the same head as the earlier deep review on this PR. That review was run with Claude Opus-tier arms; this one re-ran the same protocol on Claude Fable 5.1 to see what a stronger panel adds. Four reviewers ran concurrently and blind, to each other and to the round-1 review: three fresh-context Claude Fable 5.1 arms (a generalist, a QEC-semantics lens, and a complexity/implementability lens) and one Codex arm (gpt-5.6-sol, high reasoning, read-only sandbox). The design text was authored with ChatGPT, so cross-model independence from the author rests on the Claude arms; Codex served as the extra. A Fable 5.1 fusing reviewer then re-checked every finding below against the checkout before recording it. Details at the end.

Verdict: REVISE, 4 of 4 arms. Round 1's verdict stands and all three of its headline blockers were re-found independently. Round 2 adds thirteen findings round 1 did not have; three are blockers.

New in round 2

N1. Blocker. No existing PECOS reference produces the MVP demo. (all four arms) The demo mandates SZZ extraction plus transversal CX (instr-program-mvp.md:34-51) and requires the result to match an existing reference (:324-325). LogicalCircuitBuilder has no SZZ path at all; compute_cnot_schedule is hard-coded (qec/surface/logical_circuit.py:1070,1109). The SZZ device-flow lowering raises on any CX (circuit_builder.py:858-861) and on any pending Clifford at end of stream (:872-875). The single-patch SZZ abstract-vs-traced equivalence test is a strict xfail on #498 (tests/qec/surface/test_szz_interaction_basis.py:456-480). The acceptance criterion is unsatisfiable as written. Round 1 assumed the reference existed.

N2. Blocker. prepare/measure cannot resolve as sole candidates. (complexity arm, solo) The MVP models basis as a parameter of one prepare and one measure instruction (instr-program-mvp.md:188,191) and says they "may resolve as sole candidates" (:199). The companion lists surface.prepare_x/y/z and surface.measure_x/y/z as separate implementation IDs (surface-logical-circuit-guppy.md:2905,2911), and assess_support(inputs, context) (:699-703) never receives parameters. Three candidates therefore all support the input, rule 3 of the resolution order is unreachable, and every prepare in the demo fails with an ambiguity error. BoundInstrInput is used once and never defined.

N3. Blocker. The design's own H-then-CX examples are rejected by the reference, for a physical reason. (Codex, QEC arm) surface-logical-circuit-guppy.md:1688-1715 and :2227-2240 apply transversal H to one patch and then transversal CX. _emit_transversal_cx raises when the two patches' x_z_swapped differ (logical_circuit.py:1482-1488). After H the control's physical X checks sit on the former Z-check pattern and no longer match the target's, so transversal CX does not preserve the stabilizer group. This sharpens round 1's stabilizer-frame-epoch item: without a Clifford frame on the block value the examples are not merely under-specified, they are invalid.

N4. Major. Observable existence is program-global, not per-plan. (Codex, QEC arm) After CX the builder omits a non-deterministic logical observable while still incrementing the observable index (logical_circuit.py:1556-1576) and appends another patch's raw records for teleportation (:1583-1590). Whether a logical product is deterministic depends on the whole logical Clifford sequence, so no per-call QecInstrPlan can decide it, yet instr-program-mvp.md:223 and surface-logical-circuit-guppy.md:2525-2526 assign observables to plans. The MVP demo hides this because both of its observables are CX-invariant.

N5. Major. SZZ carries a pending local Clifford across the instruction boundary. (QEC arm, solo) The SZZ device-flow lowering defers free-standing single-qubit Cliffords until the next SZZ or measurement host (circuit_builder.py:768-777). A syn_extract.using("szz") value version therefore carries per-data-qubit Clifford state into the next instruction. The design's physical frame is Pauli-only (surface-logical-circuit-guppy.md:1506-1511). This is the same slot N3 needs; one fix covers both.

N6. Major. Rust and Python order Z checks differently. (QEC arm, solo) Python emits right boundary, then bulk, then left boundary (qec/surface/layouts/rotated_lattice.py:139-156); Rust rasters row by row over the dual lattice (crates/pecos-qec/src/surface.rs:376-458). Check indices differ, so detector order, coordinates, and the CX 3-body detector's pairing by shared stab_index (logical_circuit.py:1348) all differ. Any adapter must transfer data (supports, indices, positions, schedule touches), not regenerate geometry. Extends round 1's dx.min(dz) finding.

N7. Major. The traced route is single-shot and branch-specialised. (QEC arm, solo) build_dem_from_guppy runs the program once with a fixed seed (qec/dem.py:1243-1246; tracing.py:237) and traces the realised branch, which surface-logical-circuit-guppy.md:1596-1598 forbids. Tag binding refuses programs whose static measurement count differs from the traced count (dem_builder/builder.rs:3611-3620), so per-occurrence identity under runtime loops does not exist today. Direct-versus-traced equivalence holds only for straight-line and frame-update-only programs. Round 1 established only the TickCircuit half of this.

N8. Major. A serialised program cannot regain executable InstrImpl behaviour. (Codex, generalist) Implementations are Rust trait objects (surface-logical-circuit-guppy.md:356-373); instr-program-mvp.md:161-166 requires a separate-crate instruction set to be serialisable and resolvable without dynamic loading; program.resolve() takes no argument. A descriptor-versus-provider split is needed: resolve(providers, context) with manifest and digest matching and a deterministic error when a provider is absent.

N9. Major. Byte-equivalence and "match" are untestable, and one of them is vacuous. (Codex, generalist, complexity) No wire format, map ordering, float encoding, ID allocation rule, or digest specification exists. Separately, since Python is a thin view over the Rust serialiser (instr-program-mvp.md:271-276), the Rust/Python byte-equivalence criterion can only fail on a wiring bug. This is the A-agrees-with-B failure mode.

N10. Major. SurfaceCircuitStep plus the CircuitRenderer family is the uncited prototype. (generalist, complexity, Codex) circuit_builder.py:172 defines one abstract op list and :1709-2073 four renderers (Stim, Guppy, DagCircuit, TickCircuit) over it, which is exactly the "one portable plan, several backends that must not drift" pattern the MVP proposes, already working for SZZ memory. Neither document mentions it. Round 1 cited only _check_plan.py.

N11. Major. The generic dialect-agnostic substrate has no consumer. (complexity arm, solo) Goal 12 (surface-logical-circuit-guppy.md:246-248) justifies it by physical, classical, pulse, and calibration dialects; none exists or is a workstream in #508-#516. The only non-QEC InstrSet is the test fixture. The arm's simplest alternative (a QEC-specific LogicalCircuit plus SurfaceOpImpl trait plus PhysicalPlan, roughly 1.5-2.5k lines of Rust, ProtocolPhysicalPlan retained, syndrome_szz versus syndrome_cx as the two real candidates) meets all four stated goals.

N12. Major. Stage 1a requires five things the MVP defers, and the stage order is inverted twice. (complexity arm, solo) surface-logical-circuit-guppy.md:3228-3243 requires InstrModule, IfRegion, LogicalPauliFrame, the QecTypeExpr algebra, and a canonical Rust SurfacePatch; instr-program-mvp.md:280-296 defers all five, so the MVP's own rule at :339 fails against its companion. Stage 1b emits PHIR before anything consumes it; Stage 5's physical-conditional lowering needs Stage 6's conditional regions; Stage 4 (Bevy viewer) outranks Stage 5 (factory migration). The document grew from 2448 to 3660 lines across 13 commits with no code.

N13. Minor. Further grounding gaps. (Codex, generalist, complexity) Neither pecos-qec nor pecos-quantum depends on serde (only serde_json; zero derives). pecos-phir exposes a process-global dialect registry (crates/pecos-phir/src/dialect.rs:215-238), contrary to the no-global-registry rule if reused. PHIR already has ValueRef and SSAValue (ops.rs:379,392), clashing with the proposed ValueId if the layer lands in pecos-phir. The MVP requires rounds > 0 while build_memory_circuit accepts zero (decode.py:1478). Guppy measurement-layout certification today comes from a second abstract-Tick pass (guppy_gen/surface.py:2864-2897), so "reuse tag utilities" is not a small adaptation.

Round 1 findings corroborated in round 2

• Hidden Python-to-Rust port inside the MVP: all four arms. The complexity arm adds that Rust has zero SurfacePatch and that the MVP requires a fourth Guppy emitter alongside guppy_gen/, the SLR codegen, and GuppyRenderer.
• Cross-call detector composition has no owner: Codex, generalist, QEC arm.
• pecos/qeccs/ uncited: complexity arm only, as in round 1 where one arm found it. It adds default_qecc.py:181-205 (implementation selection by instruction symbol) and protocols.py:436.
• SurfacePatch.rotated(3): Codex, generalist.
• No round-alignment construct in the MVP: QEC arm, adding that a patch first extracted in a later segment gets no first-round detectors at all (logical_circuit.py:1257-1260).
• x_z_swapped has no home: Codex, QEC arm.
• The two documents prescribe different first slices: Codex, complexity arm (seven-row table).
• reference_schedule and noise_model undefined: Codex, generalist, complexity.
• MeasurementId collides and record offsets collapse early: Codex, generalist, QEC arm, adding that TickCircuit::mz mints MeasId as the record position (tick_circuit.rs:3202-3222).
• Crate layering open: Codex, generalist, complexity. The complexity arm adds that pecos-phir depends on pecos-engines, so hosting the authoring layer there drags the execution engine into it; all three recommend a standalone pecos-instr on pecos-core.
• add_memory is_first asymmetry: Codex.
• Frame join rule undefined: QEC arm.
• Patch types not interconvertible: Codex, QEC arm.
• Spelling drift (graph.block versus graph.add_block, three namespaces for the SZZ implementation): generalist, complexity.

Round 1 findings no arm re-raised

Bevy/wgpu justification; hugr_to_ast TailLoop rejection; inject_t prepares plus rather than T; Deferred has no terminal state; the QecLogicalTransform ideal-action wording. None was refuted; they stand from round 1.

Conflicts resolved

• Worked examples versus single-use rules. The generalist checked the teleport body (surface-logical-circuit-guppy.md:1238-1282) and found no violation; round 1 said it consumes bell and destination repeatedly. Both are right under different authoring models. The body uses body.append without rebinding, which is legal if the builder is cursor-mutating (instr-program-mvp.md:130) and illegal under SSA rebinding (:106). The finding is the unpinned authoring model, not the example.
• HUGR converter behaviour. Round 1 said hugr_to_dag_circuit silently continues past unknown nodes (hugr_convert.rs:758,762,864); the QEC arm said it rejects control flow (NotSimpleError, :1296-1315). Both paths exist in the file. The design should say which one HugrInstrImporter builds on.

Must-fix, ranked and deduplicated across both rounds

1. Pick a first slice that has a reference. Either single-patch memory with syndrome_szz versus syndrome_cx as two real candidates (matches surface-logical-circuit-guppy.md:3646-3652), or two-patch with CX extraction so LogicalCircuitBuilder is the oracle. Then name the reference constructor, the comparison predicate, reference_schedule, and the noise schema. (N1; round 1 items 5 and 6)
2. Fix prepare/measure resolution: pass canonical parameters to assess_support or make basis part of instruction identity. Define BoundInstrInput. (N2)
3. Add a per-block physical Clifford frame, shaped like LocalCliffordFrame in _clifford_deformation.py:515-529, to block value versions and to every implementation's frame-transfer contract. H, S, SZZ carry-over, and CX support all need it. Correct the H-then-CX examples. (N3, N5; round 1 epoch item)
4. Give detector discovery and observable existence a program-level owner: stabilizer tracking over the composed protocol plan, with the hand-written boundary rules kept as a test oracle. (N4; round 1 item 2)
5. Add a parallel or aligned-rounds construct to the MVP substrate and define the reference scheduling context as round-interleaved with one shared round clock. (round 1 item 4)
6. Split serialised descriptors from runtime providers: resolve(providers, context). (N8)
7. Name the port honestly: geometry, layouts, schedule, check plan, and batching (about 2.4k lines), the SZZ and transversal-CX subsets, a Rust Guppy emitter, serde for pecos-qec, and an adapter that transfers Python's check ordering by data. (round 1 item 1; N6, N13)
8. Reconcile the two documents into one roadmap: split Stage 1a into landable slices, move PHIR after its consumer, put Stage 6 before Stage 5, put Bevy behind factory migration, and align Stage 1a with the MVP deferral list. (N12; round 1 contradiction item)
9. Cut zero-consumer machinery from the MVP: ResourceQuantity precision, service/locality/latency constraints, package manifests, UsePolicy::Reusable, and the ScheduledPhysicalPlan "concrete bindings" that contradict instr-program-mvp.md:113-115. Either name a second dialect or land the QEC-specific shape first. (N11)
10. Replace the vacuous criteria: byte-equivalence of one serialiser read twice, a reordering permission with no second backend, and a support-failure criterion met only by the toy set. (N9)
11. Define the MeasurementId -> MeasId -> record map the GeneratedTickProgram owns; rename or retire propagator::types::MeasurementId. State that the traced route is straight-line only until branch-aware tracing exists. (N7; round 1 identity item)
12. Settle Stage 0: standalone pecos-instr on pecos-core, QEC-to-PHIR lowering in a bridge crate, no reuse of PHIR's global dialect registry. (round 1 crate item; N13)
13. Write the pecos/qeccs/ plus LogicalCircuit plus SurfaceCircuitStep/CircuitRenderer retrospective. (round 1 item 3; N10)
14. Pin the authoring model (cursor-mutating or SSA-rebinding) and one spelling each for block declaration, implementation references with a namespace rule, and the selection-source enum. (conflict 1; round 1 examples item)
15. Fix SurfacePatch.rotated(3) at all sixteen sites, or label it a new constructor.

What every arm might have missed

• All four arms read; none executed. The xfail status, the run-once tracing, and the check-ordering difference were verified by reading, not by running.
• The PR base is 31 commits behind dev. No arm checked whether any cited line moved. The commit titles do not touch the surface stack, but this was not verified file by file.
• No arm questioned the product direction (an HDL-like hierarchy that may replace SLR). The panel judged the documents against their stated goals, not the goals themselves.
• No arm compared the Clifford+T consumer expectations in Transversal SZ/SZdg logical gates emit a plain per-qubit S, not the documented fold-transversal gadget #593-BoundaryGate::TGateInjection is documented as a feed-forward decision point but never consulted during decoding #596 against this design's inject_t; round 1 touched it only as a documentation nit.

---

How this review was run

The branch was checked out read-only at aa519b5b4 in a separate worktree so every reviewer read the two documents alongside the code at that commit. Four reviewers then ran concurrently and blind, each given only the documents, the repository, issues #508-#516, and the claim to verify ("this design is sound, internally consistent between the two documents, grounded in PECOS as it actually exists, and the MVP is a genuinely minimal, independently testable first slice"), with file:line citations required for every finding. None was shown the round-1 review or another arm's output.

Arm	Model	Lens
A	Claude Fable 5.1 (claude-fable-5-1), fresh context	generalist: factual grounding, internal consistency, resolution and identity semantics, architecture
B	Claude Fable 5.1 (claude-fable-5-1), fresh context	QEC semantics: detectors, observables, stabilizer relabelling, Pauli frames, measurement identity, patch round-trip
C	Claude Fable 5.1 (claude-fable-5-1), fresh context	complexity and implementability: hidden cost, acceptance-criteria testability, premature abstraction, stage realism
D	Codex gpt-5.6-sol, high reasoning, read-only sandbox	independent correctness and completeness review with the same six task areas
Fusion	Claude Fable 5.1	cross-checked every finding against the worktree, resolved conflicts, deduplicated against round 1, ranked the must-fix list

All four arms returned REVISE independently. Findings were fused rather than concatenated: corroboration across arms raised confidence, solo findings were kept on merit after verification, and the two conflicts between arms and round 1 were resolved by reading the cited code. No arm executed any code; all verification was by reading.

[peter-campora]

Do we explicitly need to produce parallel blocks for any operations that are data-parallelizable or is there some implicitness based on data-flow? The intention of this construct isn't clear to me.

[ciaranra]

Good question. I think it is taking it from some of the experimentation in SLR. I think it might be nice to let it both fall out of data-flow based things but also be able to explicitly schedule it. Part of what we probably want out of this is to be able to try out ideas by hand and have more direct manipulation... But also be able to let this to be worked out programmatically when we don't want to bother. If we just allow space-time coordinate pinning and rely more on the space-time block picture... That might be better that having some sort of "parallel" block... More explicit and expressive...

[peter-campora]

So, are we just thinking about logical quantum circuits with a dataflow based representation for this representation? No higher order constructs like function definitions with parameters, etc.? This would drastically simplify things so that we're just thinking about composing dataflow based building blocks instead of thinking about variables with scope, etc.

[ciaranra]

I think so... Have more of a picture of how information is processed and ran on devices rather than abstracting to a high level language...

[ciaranra]

Still need to think about branching etc... 🤔

[peter-campora]

I really hate string based parameters to control things if instead there's actually a limited set of enum values like for this using("transversal")

I would suggest instead of these things are built-in that there be some kind of language level module where you can import enum values to pass.

[ciaranra]

That is fair... Strings as options suck. However we probably won't want to know a prior the enums. An implementation or whatever sits slightly higher than an implementation should have a list of enums/variants it provides rather than it being universally known by the "language."

[peter-campora]

I really worry that if this is an intended authoring environment for people writing QEC experiments that repeated .append(...) calls will be tiresome.

[ciaranra]

🤔 fair

[peter-campora]

Could we considered maybe adding some syntactic sugar for .add_block and .apply. These feel file for use when tools are generating logical programs in this representation, but this feels like it could be tiresome.

[ciaranra]

I think first maybe we go about this by building the "language" in Rust as just a data structure sort of like SLR is now and then think about turning it into a proper language once we like the shape of it and can add syntactic sugar then. Maybe macros could be a middle ground... Or creative use of Rust 😄

[ciaranra]

But good to think about nicer ways to express this all 🤔

[peter-campora]

I really hate the idea of producing Guppy just because it's submitted by users. It's not intended as a compilation target and its type system and limited functionality makes it really unsuitable for being a target for lowering and will make reasoning about the scheduling of operations difficult. I don't love HUGR but it's far more suitable for this. My preference would be generating QIR or quantum MLIR dialects.

[ciaranra]

That is fair. I think it is a left over from SLR's goal of basically being a transpiler. Outputting Guppy is probably a burden we don't need

[qciaran]

ChatGPT: Addressed in 49a84ad. InstrProgram no longer lowers to Guppy, and the direct-versus-Guppy equivalence requirement has been removed. The design now lowers resolved gadgets to PHIR and/or a portable ProtocolPhysicalPlan; the PECOS reference route lowers that plan directly to normalized TickCircuit and native DEM, while target backends can consume the portable plan separately. Guppy remains only as an optional input through compiled HUGR. An imported HUGR body can be registered as a gadget implementation only with an explicit QEC contract, port/resource mapping, lifecycle and frame semantics, measurement roles, and a conformance obligation. QIR and suitable quantum MLIR dialects are retained as possible later exports after their semantic and crate-dependency boundaries are audited.

[ciaranra]

Thanks for all of the comments @peter-campora! These are really useful!

[qciaran]

ChatGPT: Follow-up in dbd80fb separates lowering from DEM analysis. Selected gadget implementations now contribute typed lower-level Rust InstrGraph bodies to a portable ProtocolProgram, similar in role to useful lower/mid-level SLR circuits. TickCircuit remains a scheduled straight-line projection; control stays in the protocol program or a control-capable lower IR/backend unless it can be specialized, unrolled, or rewritten into frame bookkeeping. DEM construction is now a separate consumer that declares which artifact/noise-model dialect it accepts. The concrete current adapter is conceptually TickDemCompiler.compile(generated_tick_program, physical_noise_model), while higher-level gadget or protocol DEM compilers are possible only with explicit scheduling and control semantics. The MVP ends at GeneratedTickProgram; native DEM parity remains a downstream integration test rather than an HDL method.

[qciaran]

ChatGPT: The readability pass is in 98e4f3d. The former architecture document mixed overview, normative requirements, implementation rationale, and roadmap, so it is now split by reader intent: instr-program.md is a 1,336-word overview centered on one example and six concepts; instr-program-mvp.md is the compact normative slice and acceptance tests; and instr-program-rationale.md holds PECOS/SLR history, detailed Rust identities/providers, crate boundaries, rejected alternatives, roadmap, and open questions. The set is roughly 28% shorter overall, and repeated identity, resolution, DEM, and deferred-scope explanations were consolidated rather than copied among files.

[qciaran]

ChatGPT: I pushed a follow-up that makes the older PECOS/SLR/HDL relationship concrete. InstrProgram now has an explicit authored → linked → resolved progression: calls may be recorded against a port declaration before their semantic definition or implementation is present, but linking must make every call typed before resolution or lowering. Normal gadget implementations are themselves InstrGraph bodies, so the same representation recursively composes PECOS gate instructions into rounds, rounds into gadgets, and gadgets into experiments; ProtocolProgram is a validated portable-dialect phase rather than a separate implementation language.

The revision also treats each instruction call as an HDL-like cell. Typed resource/value wires enter and leave its ports, and a chosen implementation can attach a hierarchical space-time realization containing child cells. Shape is realization-specific (parameters, implementation, schedule, and mapping matter), with unplaced/constrained/placed states. I added a coarse/expanded space-time diagram while keeping placement and interactive visualization outside the MVP. The MVP uses the fully declared static subset but now preserves the declaration/linkage/body boundaries needed for the open model.