One-gate execution for the streaming circuit evaluator

This file proves the machine-level execution of one valid serialized gate. The proof follows the controller's dependency order: consume one gate-count mark, read the three fixed gate bits, rewind and resolve the first reference, rewind and resolve the second reference, then append the computed value to the wire memo.

The small named-action lemmas at the start are deliberately phase-generic within this controller. They are the reusable proof-engineering seam between CoreAction and exact named configurations.

theorem Complexity.CircuitCode.Machine.Internal.coreCfg_step_preserve (phase next : CorePhase) (input code wires counter output : Tape) (hphase : phase ≠ CorePhase.done) (haction : coreAction phase (coreHeads code wires counter) output.read = CoreAction.preserve next (coreHeads code wires counter) output.read) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg phase input code wires counter output) = some (coreCfg next input code wires counter output)

Applying a named preserve action changes only the controller phase when all parked heads are away from the left marker.

theorem Complexity.CircuitCode.Machine.Internal.coreCfg_step_moveCodeRight (phase next : CorePhase) (input code wires counter output : Tape) (hphase : phase ≠ CorePhase.done) (haction : coreAction phase (coreHeads code wires counter) output.read = CoreAction.moveCodeRight next (coreHeads code wires counter) output.read) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg phase input code wires counter output) = some (coreCfg next input (code.move Dir3.right) wires counter output)

Applying a named code-right action advances exactly the code tape and changes the controller phase.

theorem Complexity.CircuitCode.Machine.Internal.coreCfg_step_moveWiresRight (phase next : CorePhase) (input code wires counter output : Tape) (hphase : phase ≠ CorePhase.done) (haction : coreAction phase (coreHeads code wires counter) output.read = CoreAction.moveWiresRight next (coreHeads code wires counter) output.read) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg phase input code wires counter output) = some (coreCfg next input code (wires.move Dir3.right) counter output)

Applying a named wire-right action advances exactly the wire tape and changes the controller phase.

theorem Complexity.CircuitCode.Machine.Internal.gateCheck_step_one (sawGate : Bool) (used total : ℕ) (input code wires counter output : Tape) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) = some (coreCfg CorePhase.gateOp input code wires (counter.writeAndMove Γ.blank Dir3.right) output)

A positive gate-check consumes one unary counter mark and enters the fixed-width gate header.

theorem Complexity.CircuitCode.Machine.Internal.gateOp_step (op : Bool) (rest : List Bool) (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (op :: rest)) (hinput : input.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg CorePhase.gateOp input code wires counter output) = some (coreCfg (CorePhase.gateNeg0 op) input (code.move Dir3.right) wires counter output)

The gate-operation phase consumes the operation bit.

theorem Complexity.CircuitCode.Machine.Internal.gateNeg0_step (op negated0 : Bool) (rest : List Bool) (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (negated0 :: rest)) (hinput : input.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateNeg0 op) input code wires counter output) = some (coreCfg (CorePhase.gateNeg1 op negated0) input (code.move Dir3.right) wires counter output)

The first-negation phase consumes the first negation bit.

theorem Complexity.CircuitCode.Machine.Internal.gateNeg1_step (op negated0 negated1 : Bool) (rest : List Bool) (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (negated1 :: rest)) (hinput : input.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateNeg1 op negated0) input code wires counter output) = some (coreCfg (CorePhase.rewindRef0 op negated0 negated1) input (code.move Dir3.right) wires counter output)

The second-negation phase consumes the second negation bit and begins the first wire rewind.

theorem Complexity.CircuitCode.Machine.Internal.gateHeader_run (sawGate op negated0 negated1 : Bool) (rest : List Bool) {wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (op :: negated0 :: negated1 :: rest)) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape), evalFamilyCoreTM.reachesIn 4 (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg (CorePhase.rewindRef0 op negated0 negated1) input code' wires (counter.writeAndMove Γ.blank Dir3.right) output) ∧ code'.HasBinarySuffix rest ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

Consuming a counter mark and the three fixed gate bits reaches the first reference rewind in exactly four steps.

theorem Complexity.CircuitCode.Machine.Internal.rewindRef0_step_cursor (op negated0 negated1 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits position) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.rewindRef0 op negated0 negated1) input code wires counter output) = some (coreCfg (CorePhase.rewindRef0 op negated0 negated1) input code (wires.move Dir3.left) counter output)

An off-marker first-reference rewind takes one ordinary wire-left step.

theorem Complexity.CircuitCode.Machine.Internal.rewindRef0_step_marker (op negated0 negated1 : Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hwires : BinaryAtMarker wires wireBits) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.rewindRef0 op negated0 negated1) input code wires counter output) = some (coreCfg (CorePhase.ref0 op negated0 negated1) input code (wires.move Dir3.right) counter output)

Reaching the wire marker ends the first-reference rewind and returns the wire head to its first bit.

theorem Complexity.CircuitCode.Machine.Internal.rewindRef0_run (op negated0 negated1 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits position) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (wires' : Tape), evalFamilyCoreTM.reachesIn (position + 2) (coreCfg (CorePhase.rewindRef0 op negated0 negated1) input code wires counter output) (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires' counter output) ∧ BinaryCursor wires' wireBits 0

Rewinding for the first reference takes exactly position + 2 steps and returns the wire tape to position zero.

theorem Complexity.CircuitCode.Machine.Internal.rewindRef1_step_cursor (op negated1 value0 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits position) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.rewindRef1 op negated1 value0) input code wires counter output) = some (coreCfg (CorePhase.rewindRef1 op negated1 value0) input code (wires.move Dir3.left) counter output)

An off-marker second-reference rewind takes one ordinary wire-left step.

theorem Complexity.CircuitCode.Machine.Internal.rewindRef1_step_marker (op negated1 value0 : Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hwires : BinaryAtMarker wires wireBits) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.rewindRef1 op negated1 value0) input code wires counter output) = some (coreCfg (CorePhase.ref1 op negated1 value0) input code (wires.move Dir3.right) counter output)

Reaching the wire marker ends the second-reference rewind and returns the wire head to its first bit.

theorem Complexity.CircuitCode.Machine.Internal.rewindRef1_run (op negated1 value0 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits position) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (wires' : Tape), evalFamilyCoreTM.reachesIn (position + 2) (coreCfg (CorePhase.rewindRef1 op negated1 value0) input code wires counter output) (coreCfg (CorePhase.ref1 op negated1 value0) input code wires' counter output) ∧ BinaryCursor wires' wireBits 0

Rewinding for the second reference takes exactly position + 2 steps and returns the wire tape to position zero.

theorem Complexity.CircuitCode.Machine.Internal.ref0_step_one (op negated0 negated1 : Bool) (rest : List Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (true :: rest)) (hwires : BinaryCursor wires wireBits position) (hposition : position < wireBits.length) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) = some (coreCfg (CorePhase.ref0 op negated0 negated1) input (code.move Dir3.right) (wires.move Dir3.right) counter output)

Reading a unary one in the first reference advances both the code and wire cursors.

theorem Complexity.CircuitCode.Machine.Internal.ref0_step_zero (op negated0 negated1 : Bool) (rest : List Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (false :: rest)) (hwires : BinaryCursor wires wireBits position) (hposition : position < wireBits.length) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) = some (coreCfg (CorePhase.rewindRef1 op negated1 (negated0 ^^ wireBits[position])) input (code.move Dir3.right) wires counter output)

The zero delimiter of the first reference captures the selected wire value and advances only the code cursor.

theorem Complexity.CircuitCode.Machine.Internal.ref0_run (op negated0 negated1 : Bool) (reference : ℕ) (rest : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (NatCode.encode reference ++ rest)) (hwires : BinaryCursor wires wireBits 0) (hreference : reference < wireBits.length) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (wires' : Tape), evalFamilyCoreTM.reachesIn (reference + 1) (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) (coreCfg (CorePhase.rewindRef1 op negated1 (negated0 ^^ wireBits[reference])) input code' wires' counter output) ∧ code'.HasBinarySuffix rest ∧ BinaryCursor wires' wireBits reference

A complete first reference is resolved in exactly reference + 1 steps, leaving the wire cursor at the referenced position.

theorem Complexity.CircuitCode.Machine.Internal.ref1_step_one (op negated1 value0 : Bool) (rest : List Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (true :: rest)) (hwires : BinaryCursor wires wireBits position) (hposition : position < wireBits.length) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) = some (coreCfg (CorePhase.ref1 op negated1 value0) input (code.move Dir3.right) (wires.move Dir3.right) counter output)

Reading a unary one in the second reference advances both the code and wire cursors.

theorem Complexity.CircuitCode.Machine.Internal.ref1_step_zero (op negated1 value0 : Bool) (rest : List Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (false :: rest)) (hwires : BinaryCursor wires wireBits position) (hposition : position < wireBits.length) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) = some (coreCfg (CorePhase.seekAppend (evalOpBit op value0 (negated1 ^^ wireBits[position]))) input (code.move Dir3.right) wires counter output)

The zero delimiter of the second reference captures the selected wire value, computes the gate, and advances only the code cursor.

theorem Complexity.CircuitCode.Machine.Internal.ref1_run (op negated1 value0 : Bool) (reference : ℕ) (rest : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (NatCode.encode reference ++ rest)) (hwires : BinaryCursor wires wireBits 0) (hreference : reference < wireBits.length) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (wires' : Tape), evalFamilyCoreTM.reachesIn (reference + 1) (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) (coreCfg (CorePhase.seekAppend (evalOpBit op value0 (negated1 ^^ wireBits[reference]))) input code' wires' counter output) ∧ code'.HasBinarySuffix rest ∧ BinaryCursor wires' wireBits reference

A complete second reference is resolved in exactly reference + 1 steps, leaving the wire cursor at the referenced position.

theorem Complexity.CircuitCode.Machine.Internal.seekAppend_step_bit (value : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits position) (hposition : position < wireBits.length) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.seekAppend value) input code wires counter output) = some (coreCfg (CorePhase.seekAppend value) input code (wires.move Dir3.right) counter output)

Seeking the append frontier across an existing wire advances only the wire cursor.

theorem Complexity.CircuitCode.Machine.Internal.seekAppend_step_frontier (value : Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits wireBits.length) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.seekAppend value) input code wires counter output) = some (coreCfg (CorePhase.gateCheck true) input code (wires.writeAndMove (Γ.ofBool value) Dir3.right) counter (output.write (Γ.ofBool value)))

At the first blank after the wire memo, the controller appends the new wire value, mirrors it to the current output cell, and returns to gate check.

theorem Complexity.CircuitCode.Machine.Internal.seekAppend_run (value : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hwires : BinaryCursor wires wireBits position) (hinput : input.read ≠ Γ.start) (hcode : code.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (wires' : Tape), evalFamilyCoreTM.reachesIn (wireBits.length - position + 1) (coreCfg (CorePhase.seekAppend value) input code wires counter output) (coreCfg (CorePhase.gateCheck true) input code wires' counter (output.write (Γ.ofBool value))) ∧ BinaryCursor wires' (wireBits ++ [value]) (wireBits ++ [value]).length

Seeking from an arbitrary in-bounds wire cursor appends in exactly wireBits.length - position + 1 steps.

theorem Complexity.CircuitCode.Machine.Internal.evalOpBit_opBit_eq_eval (gate : RawGate) (value0 value1 : Bool) : evalOpBit gate.opBit (gate.negated₀ ^^ value0) (gate.negated₁ ^^ value1) = gate.eval value0 value1

Evaluating the serialized operation bit of a raw gate agrees with the raw gate evaluator.

theorem Complexity.CircuitCode.Machine.Internal.gateAttempt_run_encoded (sawGate : Bool) (gate : RawGate) (rest : List Bool) {wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (gate.encode ++ rest)) (hwires : BinaryCursor wires wireBits position) (hgate : gate.WellFormedAt wireBits.length) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (wires' : Tape), evalFamilyCoreTM.reachesIn (position + 2 * gate.input₀ + wireBits.length + 11) (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg (CorePhase.gateCheck true) input code' wires' (counter.writeAndMove Γ.blank Dir3.right) (output.write (Γ.ofBool (gate.eval wireBits[gate.input₀] wireBits[gate.input₁])))) ∧ code'.HasBinarySuffix rest ∧ BinaryCursor wires' (wireBits ++ [gate.eval wireBits[gate.input₀] wireBits[gate.input₁]]) (wireBits ++ [gate.eval wireBits[gate.input₀] wireBits[gate.input₁]]).length ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

One canonical, in-range serialized gate executes in controller order with an exact aggregate cost. The second-reference traversal cancels against the remaining append seek, so the total depends only on the initial wire position, the first reference, and the memo length.