Direct-unrolling generator primitives -- definitions

This layer turns the serializer's numeric wire formulas into executable BinaryRoutines over the fixed direct-generator work layout. Recent-wire references are prepared by copying available and applying a fixed number of positive predecessors. Configuration-wire references are assembled from the run-time layout values and fixed state/tape counts with framed binary arithmetic.

The arithmetic helpers clear every general-purpose temporary that they use. Their exact effects below therefore make the usual zero-scratch convention explicit instead of pretending that an arbitrary previous temporary value is preserved. All framed copy, addition, multiplication, and emission counters are restored by their underlying leaves.

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference (reference : Fin WorkCount) (offset : ℕ) : BinaryRoutine WorkCount

Copy available into reference and subtract a fixed recent-wire offset. The routine domain honestly requires every predecessor to remain positive.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate (op : AndOrOp) (negated₀ negated₁ : Bool) (offset₀ offset₁ : ℕ) : BinaryRoutine WorkCount

Emit a raw gate whose inputs are fixed offsets behind the current first unused wire, then clear both prepared-reference tapes.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareStateReference (stateIndex : ℕ) : BinaryRoutine WorkCount

Prepare the absolute state-wire reference configBase + stateIndex in reference₀.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference (stateCount : ℕ) : BinaryRoutine WorkCount

Prepare the absolute head-wire reference in reference₀ from the run-time horizon, tape index, and position. temporary₀ is cleared on exit.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReferenceBase (stateCount tapeCount : ℕ) : BinaryRoutine WorkCount

Prepare configBase + stateCount + tapeCount * (horizon + 1) and retain horizon + 1 in temporary₀.

Equations

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

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

Prepare tapeIndex * (horizon + 2) + position in temporary₂, reusing the two values left by prepareCellReferenceBase.

Equations

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

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

Add the four-symbol cell offset and symbol index to reference₀, then clear all three arithmetic temporaries.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference (stateCount tapeCount : ℕ) : BinaryRoutine WorkCount

Prepare the absolute cell-symbol wire reference in reference₀ from the run-time horizon, tape index, position, and symbol index. Temporaries zero through two are cleared on exit.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreparedReference (prepare : BinaryRoutine WorkCount) (negated : Bool := false) : BinaryRoutine WorkCount

Emit a possibly-negated copy of the wire placed in reference₀ by a preparation routine, then clear that reference tape.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference (stateIndex : ℕ) (negated : Bool := false) : BinaryRoutine WorkCount

Prepare and emit one numeric state-wire reference.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference (stateCount : ℕ) (negated : Bool := false) : BinaryRoutine WorkCount

Prepare and emit one numeric head-wire reference.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference (stateCount tapeCount : ℕ) (negated : Bool := false) : BinaryRoutine WorkCount

Prepare and emit one numeric cell-symbol wire reference.

Equations

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