Add mid-circuit measurement and classical feedforward

examples/active-teleportation.q.orca.md

@@ -0,0 +1,69 @@
+# machine ActiveTeleportation
+
+> Standard 3-qubit active (deterministic) quantum teleportation.
+> Alice holds q0 (state to teleport) and q1 (her Bell pair qubit).
+> Bob holds q2 (his Bell pair qubit).
+> Mid-circuit Bell measurement on q0+q1 feeds forward X and Z corrections to q2.
+
+## context
+
+| Field  | Type        | Default       |
+|--------|-------------|---------------|
+| qubits | list<qubit> | [q0, q1, q2] |
+| bits   | list<bit>   | [b0, b1]      |
+
+## events
+
+- create_bell_pair
+- encode_alice
+- measure_alice_x
+- measure_alice_z
+- correct_x
+- correct_z
+
+## state |init> [initial]
+
+> q0 in arbitrary state |ψ⟩; q1 and q2 in |00⟩
+
+## state |bell_ready>
+
+> Bell pair prepared between q1 and q2: (|00⟩ + |11⟩)/√2
+
+## state |alice_encoded>
+
+> Alice applied CNOT(q0,q1) and H(q0) to entangle her qubit with the channel
+
+## state |measured>
+
+> Mid-circuit Bell measurement complete: b0 = measure(q0), b1 = measure(q1)
+
+## state |teleported> [final]
+
+> Bob's qubit q2 holds |ψ⟩ after X and Z feedforward corrections
+
+## transitions
+
+| Source          | Event             | Guard | Target           | Action        |
+|-----------------|-------------------|-------|------------------|---------------|
+| |init>          | create_bell_pair  |       | |bell_ready>     | make_bell     |
+| |bell_ready>    | encode_alice      |       | |alice_encoded>  | encode_alice  |
+| |alice_encoded> | measure_alice_x   |       | |measured>       | meas_q0       |
+| |measured>      | measure_alice_z   |       | |measured>       | meas_q1       |
+| |measured>      | correct_x         |       | |measured>       | feedfwd_x     |
+| |measured>      | correct_z         |       | |teleported>     | feedfwd_z     |
+
+## actions
+
+| Name         | Signature      | Effect                             |
+|--------------|----------------|------------------------------------|
+| make_bell    | (qs) -> qs     | Hadamard(qs[1]); CNOT(qs[1], qs[2]) |
+| encode_alice | (qs) -> qs     | CNOT(qs[0], qs[1]); Hadamard(qs[0]) |
+| meas_q0      | (qs) -> qs     | measure(qs[0]) -> bits[0]          |
+| meas_q1      | (qs) -> qs     | measure(qs[1]) -> bits[1]          |
+| feedfwd_x    | (qs) -> qs     | if bits[1] == 1: X(qs[2])         |
+| feedfwd_z    | (qs) -> qs     | if bits[0] == 1: Z(qs[2])         |
+
+## verification rules
+
+- mid_circuit_coherence: q0 and q1 are not reused after mid-circuit measurement
+- feedforward_completeness: both measured bits drive correction gates on Bob's qubit

examples/bit-flip-syndrome.q.orca.md

@@ -0,0 +1,70 @@
+# machine BitFlipSyndrome
+
+> 5-qubit bit-flip syndrome circuit: 3 data qubits (q0–q2) + 2 ancilla (q3, q4).
+> Measure two syndrome bits mid-circuit; apply X corrections conditioned on
+> the syndrome results. This demonstrates mid-circuit measurement and classical
+> feedforward in Q-Orca.
+
+## context
+
+| Field  | Type        | Default               |
+|--------|-------------|-----------------------|
+| qubits | list<qubit> | [q0, q1, q2, q3, q4] |
+| bits   | list<bit>   | [b0, b1]              |
+
+## events
+
+- entangle
+- measure_s0
+- measure_s1
+- correct_q0
+- correct_q2
+
+## state |init> [initial]
+
+> Data qubits in |000⟩, ancilla in |00⟩
+
+## state |entangled>
+
+> Ancilla qubits entangled with data for syndrome extraction
+
+## state |s0_measured>
+
+> First syndrome bit captured: bits[0] = measure(q3)
+
+## state |s1_measured>
+
+> Second syndrome bit captured: bits[1] = measure(q4)
+
+## state |q0_corrected>
+
+> X correction applied to q0 if bits[0] == 1
+
+## state |corrected> [final]
+
+> Both corrections applied; logical qubit restored
+
+## transitions
+
+| Source          | Event      | Guard | Target          | Action        |
+|-----------------|------------|-------|-----------------|---------------|
+| |init>          | entangle   |       | |entangled>     | entangle_data |
+| |entangled>     | measure_s0 |       | |s0_measured>   | measure_s0    |
+| |s0_measured>   | measure_s1 |       | |s1_measured>   | measure_s1    |
+| |s1_measured>   | correct_q0 |       | |q0_corrected>  | correct_q0    |
+| |q0_corrected>  | correct_q2 |       | |corrected>     | correct_q2    |
+
+## actions
+
+| Name          | Signature      | Effect                                                       |
+|---------------|----------------|--------------------------------------------------------------|
+| entangle_data | (qs) -> qs     | CNOT(qs[0], qs[3]); CNOT(qs[1], qs[3]); CNOT(qs[1], qs[4]); CNOT(qs[2], qs[4]) |
+| measure_s0    | (qs) -> qs     | measure(qs[3]) -> bits[0]                                    |
+| measure_s1    | (qs) -> qs     | measure(qs[4]) -> bits[1]                                    |
+| correct_q0    | (qs) -> qs     | if bits[0] == 1: X(qs[0])                                   |
+| correct_q2    | (qs) -> qs     | if bits[1] == 1: X(qs[2])                                   |
+
+## verification rules
+
+- mid_circuit_coherence: ancilla qubits q3 and q4 are not reused after measurement
+- feedforward_completeness: every syndrome measurement drives a correction gate

openspec/changes/mid-circuit-measurement/design.md

@@ -0,0 +1,44 @@
+## Context
+
+End-of-circuit measurement already exists (`Measurement` AST node, parsed from `measure(qs[N])`). Mid-circuit measurement requires measuring a qubit into a classical bit register *during* the circuit, then using that classical bit to conditionally apply a gate. The existing `QActionSignature` stores at most one `gate` and one `measurement` per action — this design adds two new optional fields for the two new effect kinds.
+
+## Goals / Non-Goals
+
+**Goals:**
+- Add `list<bit>` as a recognised context field type (parse `list<bit>` → `QTypeList(element_type="bit")`)
+- Parse `measure(qs[N]) -> bits[M]` effect → `QEffectMeasure(qubit_idx=N, bit_idx=M)`
+- Parse `if bits[M] == val: Gate(qs[K])` effect → `QEffectConditional(bit_idx=M, value=val, gate=...)`
+- Store both on `QActionSignature` as optional fields
+- Qiskit compiler: use `QuantumCircuit(n_qubits, n_bits)` and emit `qc.measure()` + `with qc.if_test(...):`
+- QASM compiler: emit `c[M] = measure q[N];` inline and `if(c==val) gate q[K];`
+- Verifier: `MidCircuitCoherenceRule` (no unitary after unmeasured mid-circuit qubit) and `FeedforwardCompletenessRule` (every measure result is used)
+- Examples: `bit-flip-syndrome.q.orca.md`, `active-teleportation.q.orca.md`
+
+**Non-Goals:**
+- Multi-qubit classical register operations or arithmetic on bit results
+- Reset gates (`reset q[N]`) — deferred to a follow-on
+- Dynamic repetition / while-measure loops
+- Noise model changes for mid-circuit measurement
+
+## Decisions
+
+**Decision: Two new fields on `QActionSignature` rather than a polymorphic effect list**
+Adding `mid_circuit_measure: Optional[QEffectMeasure]` and `conditional_gate: Optional[QEffectConditional]` follows the same pattern as the existing `gate` and `measurement` fields. It avoids a larger refactor of the action/effect pipeline while keeping the new semantics visible at the AST level.
+
+**Decision: `measure(qs[N]) -> bits[M]` is parsed separately from the terminal `measure(qs[N])`**
+The existing `_parse_measurement_from_effect` matches `measure(qs[N])` without an arrow. The new `_parse_mid_circuit_measure_from_effect` matches only the arrow form, so neither parser conflicts with the other.
+
+**Decision: Qiskit dynamic circuits via `qc.if_test` (OpenQASM 3 style)**
+IBM's `qc.if_test((clbit, val))` context manager is the current Qiskit idiom for classical feedforward. It maps cleanly to the `with qc.if_test(...):` pattern and works without importing extra packages beyond `qiskit`.
+
+**Decision: QASM uses OpenQASM 2 `if()` syntax**
+The proposal mentions OpenQASM 3 `measure q[N] -> c[M];` style but `stdgates.inc` targets QASM 3. To keep the QASM output runnable on the widest set of simulators, we emit `c[M] = measure q[N];` (QASM 3 assignment style) and `if(c==val) gate q[K];` (QASM 2 if-clause, which is also accepted by many QASM 3 parsers).
+
+**Decision: Bit count inferred from `list<bit>` context fields**
+`_infer_bit_count` inspects context fields whose `QTypeList.element_type == "bit"` and counts them from the default value (e.g. `[b0, b1]` → 2). If no `list<bit>` field exists, bit count defaults to 0 (no classical register).
+
+## Risks / Trade-offs
+
+- **`qc.if_test` requires Qiskit ≥ 0.45** — accepted; older Qiskit already fails on other features
+- **QASM `if()` clause targets QASM 2 semantics** — a future QASM 3 upgrade pass can switch to `if (c[M] == val) { ... }` style
+- **Verifier checks are conservative** — `MidCircuitCoherenceRule` only fires if it can statically prove a qubit is used after measurement; it will miss dynamic paths involving guards

openspec/changes/mid-circuit-measurement/tasks.md

@@ -0,0 +1,65 @@
+## 1. AST
+
+- [x] 1.1 Add `QEffectMeasure` and `QEffectConditional` dataclasses to `q_orca/ast.py`;
+      extend `QActionSignature` with `mid_circuit_measure: Optional[QEffectMeasure] = None`
+      and `conditional_gate: Optional[QEffectConditional] = None`
+
+## 2. Parser
+
+- [x] 2.1 Add `_parse_mid_circuit_measure_from_effect(effect_str)` in
+      `q_orca/parser/markdown_parser.py` — matches `measure(qs[N]) -> bits[M]`,
+      returns `QEffectMeasure(qubit_idx=N, bit_idx=M)`; also ensure `list<bit>`
+      is parsed as `QTypeList(element_type="bit")` (add `"bit"` as recognized element type
+      in `_parse_q_type_string`)
+- [x] 2.2 Add `_parse_conditional_gate_from_effect(effect_str)` — matches
+      `if bits[M] == val: Gate(qs[K])`, returns
+      `QEffectConditional(bit_idx=M, value=val, gate=QuantumGate(...))`
+- [x] 2.3 Call both helpers in `_parse_actions_table` and store results on
+      `QActionSignature.mid_circuit_measure` and `QActionSignature.conditional_gate`
+
+## 3. Qiskit compiler
+
+- [x] 3.1 Add `_infer_bit_count(machine)` helper in `q_orca/compiler/qiskit.py` that
+      returns the classical bit count from `list<bit>` context fields (count items in
+      default value like `[b0, b1]`)
+- [x] 3.2 In `compile_to_qiskit`, switch from `QuantumCircuit({n})` to
+      `QuantumCircuit({n_qubits}, {n_bits})` when `n_bits > 0`; in the gate emission
+      loop, emit `qc.measure(N, M)` for `mid_circuit_measure` actions and
+      `with qc.if_test((qc.clbits[M], val)):\n    qc.<gate>(K)` for
+      `conditional_gate` actions
+
+## 4. QASM compiler
+
+- [x] 4.1 In `compile_to_qasm` (`q_orca/compiler/qasm.py`), emit
+      `c[M] = measure q[N];` inline (in the gate sequence loop) for
+      `mid_circuit_measure` actions, and `if(c==val) <gate> q[K];` for
+      `conditional_gate` actions; also declare `bit[n_bits] c;` when the machine has
+      mid-circuit measurements
+
+## 5. Verifier
+
+- [x] 5.1 Add `check_mid_circuit_coherence(machine)` in `q_orca/verifier/quantum.py` —
+      activated by `"mid_circuit_coherence"` rule; walk the BFS gate sequence and
+      error if any action applies a unitary gate to a qubit that a prior action
+      already measured mid-circuit (uses `mid_circuit_measure`)
+- [x] 5.2 Add `check_feedforward_completeness(machine)` — activated by
+      `"feedforward_completeness"` rule; warn if the machine has actions with
+      `mid_circuit_measure` but no action with `conditional_gate` referencing that
+      bit index
+- [x] 5.3 Register both checks in `verify_quantum` so they run automatically
+
+## 6. Examples and tests
+
+- [x] 6.1 Add `examples/bit-flip-syndrome.q.orca.md` — 5-qubit bit-flip syndrome
+      circuit: 3 data qubits + 2 ancilla; prepare |000>, measure two syndromes
+      mid-circuit into `bits`, apply corrections conditioned on syndrome values
+- [x] 6.2 Add `examples/active-teleportation.q.orca.md` — 3-qubit active teleportation:
+      prepare Bell pair, mid-circuit Bell measurement on data + Alice qubit, feedforward
+      X and Z corrections on Bob's qubit
+- [x] 6.3 Create `tests/test_mid_circuit_measurement.py` covering:
+      parser round-trip for `QEffectMeasure` and `QEffectConditional`,
+      Qiskit emission with `qc.measure` and `qc.if_test`,
+      QASM emission with `c[M] = measure` and `if(c==val)`,
+      and verifier acceptance of well-formed machines
+- [x] 6.4 Run `pytest tests/test_mid_circuit_measurement.py` and confirm all tests pass;
+      run full `pytest` suite and confirm no regressions

q_orca/ast.py

@@ -194,6 +194,21 @@ class ValueRef:
     value: any = None
 
 
+@dataclass
+class QEffectMeasure:
+    """Mid-circuit measurement: measure qubit N into classical bit M."""
+    qubit_idx: int
+    bit_idx: int
+
+
+@dataclass
+class QEffectConditional:
+    """Classical feedforward: if bits[M] == val, apply gate to qubit K."""
+    bit_idx: int
+    value: int  # 0 or 1
+    gate: QuantumGate
+
+
 @dataclass
 class QActionSignature:
     name: str
@@ -204,6 +219,8 @@ class QActionSignature:
     effect_type: Optional[str] = None
     gate: Optional[QuantumGate] = None
     measurement: Optional[Measurement] = None
+    mid_circuit_measure: Optional[QEffectMeasure] = None
+    conditional_gate: Optional[QEffectConditional] = None
 
 
 @dataclass

q_orca/compiler/qasm.py

@@ -3,7 +3,7 @@
 import re
 
 from q_orca.ast import QMachineDef, QuantumGate, QTypeScalar, QTypeList, QTypeQubit
-from q_orca.compiler.qiskit import _parse_effect_string
+from q_orca.compiler.qiskit import _parse_effect_string, _infer_bit_count
 
 
 def compile_to_qasm(machine: QMachineDef) -> str:
@@ -16,14 +16,19 @@ def compile_to_qasm(machine: QMachineDef) -> str:
     lines.append("")
 
     qubit_count = _infer_qubit_count(machine)
+    bit_count = _infer_bit_count(machine)
     lines.append(f"qubit[{qubit_count}] q;")
 
     has_measurement = any(a.measurement for a in machine.actions)
+    has_mid_circuit = any(a.mid_circuit_measure is not None for a in machine.actions)
     has_measure_event = any(
         "measure" in e.name.lower() or "collapse" in e.name.lower()
         for e in machine.events
     )
-    if has_measurement or has_measure_event:
+    if has_mid_circuit and bit_count > 0:
+        lines.append(f"bit[{bit_count}] c;")
+        lines.append("")
+    elif has_measurement or has_measure_event:
         lines.append(f"bit[{qubit_count}] c;")
         lines.append("")
 
@@ -34,15 +39,29 @@ def compile_to_qasm(machine: QMachineDef) -> str:
     if any(hasattr(f.type, "kind") and f.type.kind == "int" for f in machine.context):
         lines.append("")
 
+    action_map = {a.name: a for a in machine.actions}
     gate_sequence = _extract_gate_sequence(machine)
     lines.append("// Gate sequence derived from state machine transitions")
     for action_name, gates, comment in gate_sequence:
         if comment:
             lines.append(f"// {comment}")
-        for gate in gates:
-            lines.append(_gate_to_qasm(gate, qubit_count))
-
-    if has_measurement or has_measure_event:
+        action = action_map.get(action_name)
+        if action and action.mid_circuit_measure is not None:
+            mcm = action.mid_circuit_measure
+            lines.append(f"c[{mcm.bit_idx}] = measure q[{mcm.qubit_idx}];")
+        elif action and action.conditional_gate is not None:
+            cg = action.conditional_gate
+            gate_str = _gate_to_qasm(cg.gate, qubit_count).rstrip(";")
+            # OpenQASM 3.0 per-bit conditional: bare bit for 1, negated for 0
+            cond = f"c[{cg.bit_idx}]" if cg.value else f"!c[{cg.bit_idx}]"
+            lines.append(f"if ({cond}) {{ {gate_str}; }}")
+        else:
+            for gate in gates:
+                lines.append(_gate_to_qasm(gate, qubit_count))
+
+    # Emit terminal measurement block only when there are no mid-circuit
+    # measurements (which are emitted inline in the gate sequence above).
+    if not has_mid_circuit and (has_measurement or has_measure_event):
         lines.append("")
         lines.append("// Measurement")
         for i in range(qubit_count):
@@ -82,8 +101,18 @@ def _extract_gate_sequence(machine: QMachineDef) -> list:
                         gates = [action.gate]
                     steps.append((t.action, gates, f"{t.source} -> {t.target} via {t.event}"))
 
-            is_measure = "measure" in t.event.lower() or "collapse" in t.event.lower()
-            if not is_measure and t.target not in visited:
+            # Continue BFS past mid-circuit measurement events; stop only at
+            # terminal (end-of-circuit) measurement events.
+            transition_action = action_map.get(t.action) if t.action else None
+            is_mid_circuit = (
+                transition_action is not None
+                and transition_action.mid_circuit_measure is not None
+            )
+            is_terminal_measure = (
+                ("measure" in t.event.lower() or "collapse" in t.event.lower())
+                and not is_mid_circuit
+            )
+            if not is_terminal_measure and t.target not in visited:
                 queue.append(t.target)
 
     return steps