Sequential fixed-width evaluator wire layout -- definitions

The evaluator receives a description code followed by one sample input. It then compiles one formula fragment per bounded gate slot. This module assigns absolute wires to primary inputs and earlier gate results without yet building or executing the concatenated raw circuit.

The numeric prefix schedule depends only on the public exact gate-formula size, so later compilation and streaming constructions share one wire layout.

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.baseWireCount (inputWidth gateBound : ℕ) : ℕ

Number of incoming wires: description code followed by one sample input.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.baseWireCount inputWidth gateBound = Complexity.CircuitCode.FixedWidth.codeWidth inputWidth gateBound + inputWidth

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.sizeAt (inputWidth gateBound index : ℕ) : ℕ

Gate-formula size at a natural slot index, with zero outside the bound.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.prefixSize (inputWidth gateBound : ℕ) : ℕ → ℕ

Total gate-formula size of the first count slots.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.prefixSize inputWidth gateBound 0 = 0

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.stepAvailable (inputWidth gateBound : ℕ) (slot : Fin gateBound) : ℕ

Number of wires available before compiling one gate-slot formula.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.stepOutputWire (inputWidth gateBound : ℕ) (slot : Fin gateBound) : ℕ

Absolute output wire assigned to one compiled gate-slot formula.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.earlierSlot {gateBound : ℕ} (slot : Fin gateBound) (earlier : Fin ↑slot) : Fin gateBound

Lift a prior local gate index to the global bounded slot type.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.earlierSlot slot earlier = ⟨↑earlier, ⋯⟩

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.sourceFormula (inputWidth gateBound : ℕ) (slot : Fin gateBound) : Fin (inputWidth + ↑slot) → BoolFormula

One-node formulas naming the primary inputs and earlier gate results available to a particular gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.stepFormula (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula computing one sequentially laid-out encoded gate slot.

Equations

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