Sequential fixed-width evaluation semantics -- definitions

This module defines the paired result invariant used to compare a compiled encoded-evaluation prefix with direct evaluation of the same padded raw-gate prefix. The compiled memo includes the description code and formula-internal wires; the raw memo contains only sample inputs and one value per gate slot.

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.prefixSlot {gateBound count : ℕ} (hcount : count ≤ gateBound) (slot : Fin count) : Fin gateBound

Lift an index in a bounded prefix to the full fixed slot array.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.prefixSlot hcount slot = ⟨↑slot, ⋯⟩

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.combinedInput {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (input : BitString inputWidth) : BitString (EvaluationLayout.baseWireCount inputWidth gateBound)

Description code followed by one sample input.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.combinedInput description input = Fin.append description.encode input

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.inputWires {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (input : BitString inputWidth) : Array Bool

Initial memo array for encoded evaluation.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.rawPrefix {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (count : ℕ) : RawCircuit

First count gates of the padded direct-semantics circuit.

Equations

• Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.rawPrefix description count = List.take count description.toPaddedRawCircuit

structure Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.PrefixResult {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (input : BitString inputWidth) (count : ℕ) (hcount : count ≤ gateBound) : Type

Paired successful evaluation of one compiled prefix and its direct raw semantics, including the memo correspondence at every emitted slot output.

• circuitWires : Array Bool

  Memo after the compiled encoded-evaluation prefix.

• rawWires : Array Bool

  Memo after the direct padded raw-gate prefix.

• circuitEval : (prefixCircuit inputWidth gateBound count).evalAux? (inputWires description input) = some self.circuitWires

  Successful compiled-prefix evaluation.

• rawEval : (rawPrefix description count).evalAux? (Array.ofFn input) = some self.rawWires

  Successful direct raw-prefix evaluation.

• circuitSize : self.circuitWires.size = EvaluationLayout.baseWireCount inputWidth gateBound + EvaluationLayout.prefixSize inputWidth gateBound count

  Exact compiled memo size.

• rawSize : self.rawWires.size = inputWidth + count

  Exact direct raw memo size.

• inputPreserved (wire : ℕ) : wire < EvaluationLayout.baseWireCount inputWidth gateBound → self.circuitWires[wire]? = (inputWires description input)[wire]?

  The compiled evaluator preserves its description-and-input prefix.

• outputs (slot : Fin count) : self.circuitWires[EvaluationLayout.stepOutputWire inputWidth gateBound (prefixSlot hcount slot)]? = self.rawWires[inputWidth + ↑slot]?

  Every compiled slot output equals the corresponding direct raw memo.