Direct-unrolling generator program -- definitions

The final serializer uses one fixed work-vector layout. Its prefix evaluates the normalized horizon, padded wire frontier, and gate-count header as fixed polynomials of the unary input length. The zero-length family member is a hardwired two-bit word; the positive tableau body remains a compositional BinaryRoutine parameter at this layer.

@[reducible, inline]

abbrev Complexity.CircuitUnrolling.Serializer.DirectGenerator.WorkCount : ℕ

Fixed number of binary work tapes used by the direct serializer.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.WorkCount = 32

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.inputLength : Fin WorkCount

Unary input length in canonical binary.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.inputLength = 0

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.horizon : Fin WorkCount

Normalized tableau horizon.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.horizon = 1

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.gateBound : Fin WorkCount

Closed padded raw-gate bound.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.gateBound = 2

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.frontier : Fin WorkCount

First wire after all padded gates.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.frontier = 3

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.gateCount : Fin WorkCount

Positive member's encoded gate count.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.gateCount = 4

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.available : Fin WorkCount

First currently unused circuit wire.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.available = 5

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.configBase : Fin WorkCount

Base wire of the current tableau configuration.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.configBase = 6

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.reference₀ : Fin WorkCount

First dynamically prepared gate reference.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.reference₀ = 7

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.reference₁ : Fin WorkCount

Second dynamically prepared gate reference.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.reference₁ = 8

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.emitCounter : Fin WorkCount

Reusable zero counter for code emission.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.emitCounter = 9

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.copyCounter : Fin WorkCount

Reusable zero counter for binary copying.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.copyCounter = 10

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.polynomialScratch : Fin WorkCount

Alternate accumulator for polynomial evaluation.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.polynomialScratch = 11

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.multiplyCounter : Fin WorkCount

Reusable multiplication counter.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.multiplyCounter = 12

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.addCounter : Fin WorkCount

Reusable addition counter.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.addCounter = 13

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₀ : Fin WorkCount

Outermost dynamic loop counter.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₀ = 14

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₀ : Fin WorkCount

Outermost dynamic loop limit.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₀ = 15

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₁ : Fin WorkCount

Second dynamic loop counter.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₁ = 16

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₁ : Fin WorkCount

Second dynamic loop limit.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₁ = 17

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₂ : Fin WorkCount

Third dynamic loop counter.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₂ = 18

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₂ : Fin WorkCount

Third dynamic loop limit.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₂ = 19

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₃ : Fin WorkCount

Innermost dynamic loop counter.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.loop₃ = 20

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₃ : Fin WorkCount

Innermost dynamic loop limit.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.limit₃ = 21

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₀ : Fin WorkCount

First general arithmetic temporary.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₀ = 22

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₁ : Fin WorkCount

Second general arithmetic temporary.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₁ = 23

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₂ : Fin WorkCount

Third general arithmetic temporary.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₂ = 24

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₃ : Fin WorkCount

Fourth general arithmetic temporary.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.temporary₃ = 25

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.savedOutput : Fin WorkCount

Original acceptance wire saved before padding.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.savedOutput = 26

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.direction : Fin WorkCount

Numeric movement-direction code.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.direction = 27

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.atomKind : Fin WorkCount

Numeric configuration-atom phase code.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.atomKind = 28

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.tapeIndex : Fin WorkCount

Numeric named-tape index.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.tapeIndex = 29

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.position : Fin WorkCount

Numeric head or cell position.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.position = 30

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.symbolIndex : Fin WorkCount

Numeric four-symbol alphabet index.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.symbolIndex = 31

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.preambleValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (values : BinaryValues WorkCount) : BinaryValues WorkCount

Pure work-vector state after evaluating the positive member's three polynomial counters and initializing both running wire bases to the input length. Scratch values are unchanged because every arithmetic leaf restores them exactly.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : BinaryRoutine WorkCount

Arithmetic and tagged-header prefix of every positive family member.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveMember {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (body : BinaryRoutine WorkCount) : BinaryRoutine WorkCount

Prefix a positive tableau body with its tag and exact padded gate-count header.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveMember tm q body = (Complexity.CircuitUnrolling.Serializer.DirectGenerator.positivePreamble tm q).seq body

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.zeroMember {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : BinaryRoutine WorkCount

Hardwired tagged code of the unique length-zero family member.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.program {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (positiveBody : BinaryRoutine WorkCount) : BinaryRoutine WorkCount

Complete generator skeleton, branching on whether the loaded input length is zero before entering the positive tableau body.

Equations

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