Sequential fixed-width gate evaluation -- definitions

Each gate-slot formula is compiled after the exact wire prefix assigned by the layout layer. Prefix circuits concatenate the first count compiled steps; out-of-range natural indices contribute the empty fragment so the builder is total, while the public evaluator uses exactly gateBound steps.

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.stepCircuit (inputWidth gateBound : ℕ) (slot : Fin gateBound) : RawCircuit

Raw formula fragment computing one fixed-width gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.stepCircuitAt (inputWidth gateBound index : ℕ) : RawCircuit

Compiled step at a natural index, empty when the index is out of range.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.prefixCircuit (inputWidth gateBound : ℕ) : ℕ → RawCircuit

Concatenation of the first count sequential gate-slot fragments.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.prefixCircuit inputWidth gateBound 0 = []

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.circuit (inputWidth gateBound : ℕ) : RawCircuit

Raw fragment computing all bounded gate-slot values for one description and sample input.

Equations

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