Fixed-width evaluator output selection -- definitions

The complete bounded evaluator emits one value for every gate slot. The active gate count is therefore used as a one-based lookup index: zero selects a dummy false source, while count k + 1 selects the output of slot k.

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.fullAvailable (inputWidth gateBound : ℕ) : ℕ

Number of wires available after evaluating every bounded gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.countWord (inputWidth gateBound : ℕ) : Fin (gateCountWidth gateBound) → BoolFormula

Formula word naming the encoded active-gate count.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.countWord inputWidth gateBound = Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.countBit inputWidth gateBound

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.sources (inputWidth gateBound : ℕ) : Fin (gateBound + 1) → BoolFormula

One-based output table: zero is a dummy value and k + 1 names slot k.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.formula (inputWidth gateBound : ℕ) : BoolFormula

Formula selecting the last active gate from the complete bounded sequence.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.selectorSize (gateBound : ℕ) : ℕ

Exact tree size of the output-selector formula.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.compileRaw (inputWidth gateBound : ℕ) : RawCircuit

Compile the output selector after the complete bounded gate sequence.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.outputWire (inputWidth gateBound : ℕ) : ℕ

Absolute wire carrying the compiled selector result.

Equations

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

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

Complete fixed-width evaluator: every bounded gate slot followed by active output selection.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.memoAssignment (wires : Array Bool) : ℕ → Bool

Total Boolean assignment read from an evaluated memo array.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.memoAssignment wires wire = wires[wire]?.getD false

def Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.lastActiveSlot {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (hpositive : description.Positive) : Fin gateBound

Slot immediately preceding a positive active-gate count.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.lastActiveSlot description hpositive = ⟨description.gateCountNat - 1, ⋯⟩

structure Complexity.CircuitCode.FixedWidth.Description.EvaluationOutput.Result {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (input : BitString inputWidth) : Type

Successful complete evaluation of a valid fixed-width description on one sample input.

• wires : Array Bool

  Memo after the gate sequence and active-output selector.

• circuitEval : (circuit inputWidth gateBound).evalAux? (EvaluationSequence.inputWires description input) = some self.wires

  Successful execution of the complete evaluator fragment.

• size : self.wires.size = fullAvailable inputWidth gateBound + selectorSize gateBound

  Exact final memo size.

• output : self.wires[outputWire inputWidth gateBound]? = description.toRawCircuit.eval? input.toList

  The designated evaluator output is exactly direct raw-circuit evaluation.