Direct-unrolling transition-case generator -- definitions

A fixed transition case has a choice literal, a state literal, and one read formula for every named tape. Machine-dependent state and symbol data are unrolled when the generator is defined. The variable-width conjunction suffix keeps one rolling member-output reference: it steps backward by the common read-formula size, then by the final one-gate state member. No formula stack is materialized on a work tape.

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.CaseFormulaClean (values : BinaryValues WorkCount) extends Complexity.CircuitUnrolling.Serializer.DirectGenerator.ReadFormulaClean values : Prop

Clean entry state for one fixed transition-case formula.

• position : values Work.position = 0
• loop₀ : values Work.loop₀ = 0
• limit₀ : values Work.limit₀ = 0
• reference₀ : values Work.reference₀ = 0
• reference₁ : values Work.reference₁ = 0
• emitCounter : values Work.emitCounter = 0
• copyCounter : values Work.copyCounter = 0
• multiplyCounter : values Work.multiplyCounter = 0
• addCounter : values Work.addCounter = 0
• temporary₀ : values Work.temporary₀ = 0
• temporary₁ : values Work.temporary₁ = 0
• temporary₂ : values Work.temporary₂ = 0
• loop₃ : values Work.loop₃ = 0

  The dynamic reference-decrement counter is reusable.

• temporary₃ : values Work.temporary₃ = 0

  The rolling dynamic offset starts clear.

• polynomialScratch : values Work.polynomialScratch = 0

  The fixed-polynomial evaluator scratch starts clear.

• tapeIndex : values Work.tapeIndex = 0

  The numeric tape selector starts clear.

• symbolIndex : values Work.symbolIndex = 0

  The numeric symbol selector starts clear.

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseChoice (choiceValue : Bool) : BinaryRoutine WorkCount

Emit the fixed choice literal on deterministic choice wire zero. A false literal is compiled as a copy followed by a negated copy of that fresh wire.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseRead (stateCount workCount tapeIndex symbolIndex : ℕ) : BinaryRoutine WorkCount

Set the numeric tape and symbol selectors, then emit their complete read formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseReads (stateCount workCount count start : ℕ) : (ℕ → ℕ) → BinaryRoutine WorkCount

Emit a consecutive fixed block of tape-read formulas. Machine-specific symbol data stays in the defining function and is never stored on tape.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseReads stateCount workCount 0 x✝¹ x✝ = Complexity.BinaryRoutine.identity

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) : BinaryRoutine WorkCount

Fixed forward member stream in choice/state/input/work/output order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCaseReadSize : BinaryRoutine WorkCount

Store the common read-formula gate count 4 * (T + 1) + 1 in temporary₃, clearing the arithmetic coefficient temporary on exit.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseConnector : BinaryRoutine WorkCount

Emit one conjunction connector from the retained member reference and the immediately preceding identity or connector gate.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnector : BinaryRoutine WorkCount

Move the rolling output reference back by one read-formula block and emit the next conjunction connector.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseChoiceConnector : BinaryRoutine WorkCount

Move from the state-member output to the preceding choice-member output and emit the final conjunction connector.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnectors : ℕ → BinaryRoutine WorkCount

Emit a fixed number of equal-width predecessor-member connectors.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousCaseReadConnectors 0 = Complexity.BinaryRoutine.identity

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) : BinaryRoutine WorkCount

Emit one complete fixed transition-case schedule. The sole lasting effect under CaseFormulaClean is the advance of available.

Equations

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