Streaming serialized-circuit evaluator core

This file defines the finite controller that evaluates an already-staged tagged circuit code. The code tape is parsed once from left to right. The wire tape begins with the primary input and receives one appended Boolean value per gate. Unary references walk that memo tape directly, while the third work tape stores and consumes the declared unary gate count.

The local TapeAction layer packages the one-sided-tape safety obligation with each head action. Consequently evalFamilyCoreTM satisfies TM.δ_right_of_start structurally rather than through a large case proof.

structure Complexity.CircuitCode.Machine.TapeAction (head : Γ) : Type

One tape-head action together with its left-end safety proof.

• write : Γw

  Writable symbol emitted at the current head.

• dir : Dir3

  Direction taken after the write.

• rightOfStart : head = Γ.start → self.dir = Dir3.right

  The action moves right whenever it reads the left-end marker.

def Complexity.CircuitCode.Machine.TapeAction.preserve (head : Γ) : TapeAction head

Preserve the scanned cell and keep an off-marker head stationary.

Equations

• Complexity.CircuitCode.Machine.TapeAction.preserve head = { write := Complexity.TM.readBackWrite head, dir := Complexity.TM.idleDir head, rightOfStart := ⋯ }

def Complexity.CircuitCode.Machine.TapeAction.moveRight (head : Γ) : TapeAction head

Preserve the scanned cell and move right.

Equations

• Complexity.CircuitCode.Machine.TapeAction.moveRight head = { write := Complexity.TM.readBackWrite head, dir := Complexity.Dir3.right, rightOfStart := ⋯ }

def Complexity.CircuitCode.Machine.TapeAction.moveLeft (head : Γ) : TapeAction head

Preserve the scanned cell and move left, bouncing right at ▷.

Equations

• Complexity.CircuitCode.Machine.TapeAction.moveLeft head = { write := Complexity.TM.readBackWrite head, dir := Complexity.TM.moveLeftDir head, rightOfStart := ⋯ }

def Complexity.CircuitCode.Machine.TapeAction.writeRight (head : Γ) (symbol : Γw) : TapeAction head

Write a symbol and move right.

Equations

• Complexity.CircuitCode.Machine.TapeAction.writeRight head symbol = { write := symbol, dir := Complexity.Dir3.right, rightOfStart := ⋯ }

def Complexity.CircuitCode.Machine.TapeAction.writeStay (head : Γ) (symbol : Γw) : TapeAction head

Write a symbol and keep an off-marker head stationary.

Equations

• Complexity.CircuitCode.Machine.TapeAction.writeStay head symbol = { write := symbol, dir := Complexity.TM.idleDir head, rightOfStart := ⋯ }

inductive Complexity.CircuitCode.Machine.CorePhase : Type

Finite phases of the fused tagged-code parser and memoized evaluator.

• rewindCode : CorePhase
• rewindWires : CorePhase
• familyTag : CorePhase
• emptyAnswer : CorePhase
• emptyEnd (answer : Bool) : CorePhase
• count : CorePhase
• rewindCounter : CorePhase
• gateCheck (sawGate : Bool) : CorePhase
• gateOp : CorePhase
• gateNeg0 (op : Bool) : CorePhase
• gateNeg1 (op negated0 : Bool) : CorePhase
• rewindRef0 (op negated0 negated1 : Bool) : CorePhase
• ref0 (op negated0 negated1 : Bool) : CorePhase
• rewindRef1 (op negated1 value0 : Bool) : CorePhase
• ref1 (op negated1 value0 : Bool) : CorePhase
• seekAppend (value : Bool) : CorePhase
• done : CorePhase

def Complexity.CircuitCode.Machine.instDecidableEqCorePhase.decEq (x✝ x✝¹ : CorePhase) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.CircuitCode.Machine.instDecidableEqCorePhase : DecidableEq CorePhase

Equations

• Complexity.CircuitCode.Machine.instDecidableEqCorePhase = Complexity.CircuitCode.Machine.instDecidableEqCorePhase.decEq

@[implicit_reducible]

instance Complexity.CircuitCode.Machine.instFintypeCorePhase : Fintype CorePhase

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.CircuitCode.Machine.instReprCorePhase : Repr CorePhase

Equations

• Complexity.CircuitCode.Machine.instReprCorePhase = { reprPrec := Complexity.CircuitCode.Machine.instReprCorePhase.repr }

def Complexity.CircuitCode.Machine.instReprCorePhase.repr : CorePhase → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.CircuitCode.Machine.CoreAction (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : Type

Named actions for the three evaluator work tapes and the output tape.

• next : CorePhase

  Controller phase entered after this action.

• code : TapeAction (wHeads codeIdx)

  Action for the serialized-code tape.

• wires : TapeAction (wHeads wiresIdx)

  Action for the input-and-memo wire tape.

• counter : TapeAction (wHeads counterIdx)

  Action for the unary gate-counter tape.

• output : TapeAction oHead

  Action for the Boolean verdict output tape.

def Complexity.CircuitCode.Machine.CoreAction.preserve (next : CorePhase) (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

Change only the controller phase and install TapeAction.preserve on every tape. This is exact tape preservation when the framed heads are off the left marker.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.CoreAction.workWrite {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) (i : Fin workTapeCount) : Γw

Project the writable symbol for a named work tape.

Equations

• action.workWrite i = if i = Complexity.CircuitCode.Machine.codeIdx then action.code.write else if i = Complexity.CircuitCode.Machine.wiresIdx then action.wires.write else action.counter.write

def Complexity.CircuitCode.Machine.CoreAction.workDir {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) (i : Fin workTapeCount) : Dir3

Project the direction for a named work tape.

Equations

• action.workDir i = if i = Complexity.CircuitCode.Machine.codeIdx then action.code.dir else if i = Complexity.CircuitCode.Machine.wiresIdx then action.wires.dir else action.counter.dir

theorem Complexity.CircuitCode.Machine.CoreAction.workDir_rightOfStart {wHeads : Fin workTapeCount → Γ} {oHead : Γ} (action : CoreAction wHeads oHead) (i : Fin workTapeCount) : wHeads i = Γ.start → action.workDir i = Dir3.right

Every projected work action moves right when its head reads ▷.

def Complexity.CircuitCode.Machine.evalOpBit (op value0 value1 : Bool) : Bool

Boolean AND/OR selected by the serialized operation bit.

Equations

• Complexity.CircuitCode.Machine.evalOpBit op value0 value1 = if op = true then value0 && value1 else value0 || value1

def Complexity.CircuitCode.Machine.CoreAction.reject (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

Halt with an explicit rejecting write, installing TapeAction.preserve on the work tapes.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.CoreAction.finish (answer : Bool) (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

Halt with the supplied Boolean write, installing TapeAction.preserve on the work tapes.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.CoreAction.moveCodeRight (next : CorePhase) (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

Move the code head right and install TapeAction.preserve on every other tape.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.CoreAction.moveWiresRight (next : CorePhase) (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

Move the wire head right and install TapeAction.preserve on every other tape.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.CoreAction.readCodeBit (next : Bool → CorePhase) (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

Read one Boolean code symbol, moving right on success and rejecting any non-Boolean symbol.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.coreAction (phase : CorePhase) (wHeads : Fin workTapeCount → Γ) (oHead : Γ) : CoreAction wHeads oHead

One finite-control action of the streaming evaluator.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.evalFamilyCoreTM : TM workTapeCount

Streaming evaluator for a valid outer pair after validPairStageTM.

The core itself remains total: malformed tagged codes and invalid references write zero and halt.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.evalFamilyCoreTime (codeLength inputLength : ℕ) : ℕ

Uniform quadratic time budget for evaluating a staged tagged-family code. The arguments are the serialized code length and primary-input length.

Equations

• Complexity.CircuitCode.Machine.evalFamilyCoreTime codeLength inputLength = 20 * (codeLength + inputLength + 1) ^ 2

def Complexity.CircuitCode.Machine.FamilyCorePre (codeBits inputBits : List Bool) (initialInput inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) : Prop

Staged tapes expected by the serialized-family evaluator core. The input tape is threaded as an explicit frame while the code and primary-input work tapes are parked at their append frontiers and the counter tape is fresh.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.FamilyCorePost (codeBits inputBits : List Bool) (initialInput inp : Tape) (_work : Fin workTapeCount → Tape) (out : Tape) : Prop

Halted defaulted-verdict contract for the serialized-family evaluator core. Malformed codes and successful false evaluations both write zero. The terminal work tapes are intentionally unconstrained because rejecting parses halt at different code, memo, and counter cursor positions.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.evalFamilyTM : TM workTapeCount

Total serialized-family evaluator: validate and stage the outer pair, then run the streaming core only on the valid branch.

Equations

• Complexity.CircuitCode.Machine.evalFamilyTM = Complexity.CircuitCode.Machine.evalFamilyTMWith Complexity.CircuitCode.Machine.evalFamilyCoreTM

def Complexity.CircuitCode.Machine.evalFamilyTime (n : ℕ) : ℕ

Concrete end-to-end time budget for validating, staging, and evaluating a serialized circuit-family input of length n.

Equations

• Complexity.CircuitCode.Machine.evalFamilyTime n = Complexity.CircuitCode.Machine.evalFamilyTMWithTime n (Complexity.CircuitCode.Machine.evalFamilyCoreTime n 0)

def Complexity.CircuitCode.Machine.EvalFamilyPost (bits : List Bool) (inp : Tape) (_work : Fin workTapeCount → Tape) (out : Tape) : Prop

Halted end-to-end contract for the serialized-family evaluator. The input cells retain the original encoding and the output carries the defaulted paired evaluation verdict with its canonical head and left-marker invariant. Terminal work tapes are intentionally unconstrained across valid and rejecting branches.

Equations

• One or more equations did not get rendered due to their size.