Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Evaluation.Layout.Internal

Sequential fixed-width evaluator wire layout -- proof internals #

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.sizeAt_eq_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
sizeAt inputWidth gateBound ↑slot = GateFormula.gateSize inputWidth gateBound slot
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.prefixSize_succ_internal (inputWidth gateBound count : ℕ) :
prefixSize inputWidth gateBound (count + 1) = prefixSize inputWidth gateBound count + sizeAt inputWidth gateBound count
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.prefixSize_mono_internal (inputWidth gateBound : ℕ) {first second : ℕ} (hbound : first ≤ second) :
prefixSize inputWidth gateBound first ≤ prefixSize inputWidth gateBound second
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.stepEnd_eq_prefix_succ_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
stepAvailable inputWidth gateBound slot + GateFormula.gateSize inputWidth gateBound slot = baseWireCount inputWidth gateBound + prefixSize inputWidth gateBound (↑slot + 1)
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.stepOutputWire_lt_stepEnd_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
stepOutputWire inputWidth gateBound slot < stepAvailable inputWidth gateBound slot + GateFormula.gateSize inputWidth gateBound slot
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.earlier_output_lt_stepAvailable_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (earlier : Fin ↑slot) :
stepOutputWire inputWidth gateBound (earlierSlot slot earlier) < stepAvailable inputWidth gateBound slot
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.size_sourceFormula_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (source : Fin (inputWidth + ↑slot)) :
(sourceFormula inputWidth gateBound slot source).size = 1
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.size_stepFormula_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
(stepFormula inputWidth gateBound slot).size = GateFormula.gateSize inputWidth gateBound slot
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.rawOutputWire_stepFormula_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
BoolFormula.rawOutputWire (stepAvailable inputWidth gateBound slot) (stepFormula inputWidth gateBound slot) = stepOutputWire inputWidth gateBound slot
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.vars_sourceFormula_lt_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (source : Fin (inputWidth + ↑slot)) (wire : ℕ) :
wire ∈ (sourceFormula inputWidth gateBound slot source).vars → wire < stepAvailable inputWidth gateBound slot
source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.vars_stepFormula_lt_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (wire : ℕ) :
wire ∈ (stepFormula inputWidth gateBound slot).vars → wire < stepAvailable inputWidth gateBound slot