Circuit evaluation with stored gate values

Program.evalVector stores gate values in an array-backed vector as it evaluates the program. The compiler uses this implementation for Program.eval, Program.trace and Circuit.eval; the kernel definitions and their simplification rules remain unchanged. The replacement theorems prove equality for arbitrary signatures and interpretations, without an inhabited carrier.

The vector evaluators compute every gate, including unused gates. Separate calls may recompute the vector; retain Circuit.evalVector explicitly when reading several outputs. Compiler replacements apply to callers compiled with this module imported, not previously compiled callers. This module does not certify a runtime bound.

Main definitions

• Cslib.Circuits.Program.evalVector: evaluate a program into a vector of gate values.
• Cslib.Circuits.Circuit.evalVector: evaluate all circuit outputs using one gate-value vector.

Main results

• Cslib.Circuits.Program.get_evalVector: the stored values agree with Program.eval.
• Cslib.Circuits.Circuit.get_evalVector: the stored outputs agree with Circuit.eval.
• Cslib.Circuits.Circuit.eval_eq_evalImpl: proved compiler replacement for circuit evaluation.

def Cslib.Circuits.Program.evalVector {σ : Signature} {inputCount : ℕ} {U : Type u} {gateCount : ℕ} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Vector U gateCount

Evaluate every gate in program order, storing its value in a vector.

@[simp]

theorem Cslib.Circuits.Program.get_evalVector {σ : Signature} {inputCount : ℕ} {U : Type u} {gateCount : ℕ} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) : (p.evalVector i x).get = p.eval i x

The stored gate values agree with the functional evaluator.

def Cslib.Circuits.Program.evalImpl {σ : Signature} {inputCount : ℕ} {U : Type u} {gateCount : ℕ} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin gateCount → U

Compiler implementation of Program.eval using stored gate values.

@[csimp]

theorem Cslib.Circuits.Program.eval_eq_evalImpl : @eval = @evalImpl

def Cslib.Circuits.Program.traceImpl {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Wire inputCount gateCount → U

Compiler implementation of Program.trace, evaluating gates only for a gate wire.

@[csimp]

theorem Cslib.Circuits.Program.trace_eq_traceImpl : @trace = @traceImpl

def Cslib.Circuits.Circuit.evalVector {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Vector U outputCount

Evaluate all circuit outputs using one vector of stored gate values. Retain the result to read several outputs without reevaluating the program. This also evaluates unused gates.

@[simp]

theorem Cslib.Circuits.Circuit.get_evalVector {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : (c.evalVector i x).get = c.eval i x

The stored output values agree with the functional evaluator.

def Cslib.Circuits.Circuit.evalImpl {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin outputCount → U

Compiler implementation of Circuit.eval using stored gate values.

@[csimp]

theorem Cslib.Circuits.Circuit.eval_eq_evalImpl : @eval = @evalImpl