Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Evaluation.Layout

Sequential fixed-width evaluator wire layout #

This module exposes the exact formula-size schedule and backward-reference invariants used to concatenate fixed-width encoded-gate formulas.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.sizeAt_eq {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
sizeAt inputWidth gateBound ↑slot = GateFormula.gateSize inputWidth gateBound slot

At an in-range slot, the numeric size oracle is the exact gate-formula size.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.prefixSize_succ (inputWidth gateBound count : ℕ) :
prefixSize inputWidth gateBound (count + 1) = prefixSize inputWidth gateBound count + sizeAt inputWidth gateBound count

The prefix schedule advances by the size of its next slot.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.prefixSize_mono (inputWidth gateBound : ℕ) {first second : ℕ} (hbound : first ≤ second) :
prefixSize inputWidth gateBound first ≤ prefixSize inputWidth gateBound second

Formula-size prefixes are monotone in their slot count.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.stepEnd_eq_prefix_succ {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
stepAvailable inputWidth gateBound slot + GateFormula.gateSize inputWidth gateBound slot = baseWireCount inputWidth gateBound + prefixSize inputWidth gateBound (↑slot + 1)

The end of a step is the global base plus the next size prefix.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.earlier_output_lt_stepAvailable {inputWidth gateBound : ℕ} (slot : Fin gateBound) (earlier : Fin ↑slot) :
stepOutputWire inputWidth gateBound (earlierSlot slot earlier) < stepAvailable inputWidth gateBound slot

Every earlier gate result is available before the current step begins.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.size_sourceFormula {inputWidth gateBound : ℕ} (slot : Fin gateBound) (source : Fin (inputWidth + ↑slot)) :
(sourceFormula inputWidth gateBound slot source).size = 1

Every generated source is represented by one variable leaf.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.size_stepFormula {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
(stepFormula inputWidth gateBound slot).size = GateFormula.gateSize inputWidth gateBound slot

Each laid-out step has exactly its advertised gate-formula size.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.rawOutputWire_stepFormula {inputWidth gateBound : ℕ} (slot : Fin gateBound) :
BoolFormula.rawOutputWire (stepAvailable inputWidth gateBound slot) (stepFormula inputWidth gateBound slot) = stepOutputWire inputWidth gateBound slot

Formula compilation places the step result on its assigned output wire.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.vars_sourceFormula_lt {inputWidth gateBound : ℕ} (slot : Fin gateBound) (source : Fin (inputWidth + ↑slot)) (wire : ℕ) :
wire ∈ (sourceFormula inputWidth gateBound slot source).vars → wire < stepAvailable inputWidth gateBound slot

Every source formula references a wire available at step entry.

source
theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.vars_stepFormula_lt {inputWidth gateBound : ℕ} (slot : Fin gateBound) (wire : ℕ) :
wire ∈ (stepFormula inputWidth gateBound slot).vars → wire < stepAvailable inputWidth gateBound slot

The complete gate-step formula is topologically scoped to the prefix available before its compilation.