Serialized circuit-evaluator machine front end

Definitions for validating one self-delimiting input pair code input and staging its two components on three work tapes. The higher-order dispatcher places an evaluator core inside the valid branch, so malformed outer inputs can never fall through into that core.

def Complexity.CircuitCode.circuitEvalLanguage : Language

The language decided by evaluating a paired tagged-family code and input. Malformed outer pairs and malformed inner codes are rejected.

Equations

• Complexity.CircuitCode.circuitEvalLanguage = {z : List Bool | Complexity.CircuitCode.evalFamilyPair? z = some true}

@[reducible, inline]

abbrev Complexity.CircuitCode.Machine.workTapeCount : ℕ

The serialized circuit evaluator uses three work tapes.

Equations

• Complexity.CircuitCode.Machine.workTapeCount = 3

def Complexity.CircuitCode.Machine.codeIdx : Fin workTapeCount

Work tape containing the tagged family code after staging.

Equations

• Complexity.CircuitCode.Machine.codeIdx = ⟨0, Complexity.CircuitCode.Machine.codeIdx._proof_1⟩

def Complexity.CircuitCode.Machine.wiresIdx : Fin workTapeCount

Work tape containing the primary input and, later, memoized wire values.

Equations

• Complexity.CircuitCode.Machine.wiresIdx = ⟨1, Complexity.CircuitCode.Machine.wiresIdx._proof_1⟩

def Complexity.CircuitCode.Machine.counterIdx : Fin workTapeCount

Work tape reserved for the evaluator's unary gate counter.

Equations

• Complexity.CircuitCode.Machine.counterIdx = ⟨2, Complexity.CircuitCode.Machine.counterIdx._proof_1⟩

def Complexity.CircuitCode.Machine.validPairStageTM : TM workTapeCount

Rewind a validated paired input and split its two components onto the code and wire tapes. This machine assumes the outer input is canonical.

Equations

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

def Complexity.CircuitCode.Machine.pairStageTM : TM workTapeCount

Validate and stage a paired input. Malformed inputs take a frame-preserving rewind branch and retain the validator's zero verdict.

Equations

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

def Complexity.CircuitCode.Machine.evalFamilyTMWith (core : TM workTapeCount) : TM workTapeCount

Validate and stage a paired input before invoking core. The core occurs inside the valid branch, so it is unreachable on malformed outer inputs.

Equations

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

def Complexity.CircuitCode.Machine.pairStageTime (inputLength : ℕ) : ℕ

Concrete front-end bound derived from the current validator, rewind, splitter, and conditional-composition contracts.

Equations

• Complexity.CircuitCode.Machine.pairStageTime inputLength = 4 * inputLength + 16

def Complexity.CircuitCode.Machine.evalFamilyTMWithTime (inputLength coreTime : ℕ) : ℕ

Front-end overhead when the valid branch additionally invokes a core with the supplied time bound.

Equations

• Complexity.CircuitCode.Machine.evalFamilyTMWithTime inputLength coreTime = 4 * inputLength + coreTime + 17

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

Fresh machine tapes before validation begins.

Equations

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

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

Auditable result of the pair-staging front end. The output is parked at cell one with its start invariant intact, so a later core can safely overwrite the staging verdict. Invalid encodings retain fresh work tapes and a zero verdict. Valid encodings expose appendable code and wire prefixes, including the left markers needed by later rewind proofs.

Equations

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