Sequential fixed-width step semantics #
The laid-out formula for one gate agrees with that description slot's raw-gate semantics whenever the assignment contains the encoded description prefix and the declared source formulas realize the available wire values.
theorem
Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.decodedSlot_eq_of_code
{inputWidth gateBound : ℕ}
(description : Description inputWidth gateBound)
(slot : Fin gateBound)
(assignment : ℕ → Bool)
(hcode : ∀ (coordinate : Fin (codeWidth inputWidth gateBound)), assignment ↑coordinate = description.encode coordinate)
:
The code prefix of an assignment decodes each gate formula's slot exactly.
theorem
Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.eval_stepFormula
{inputWidth gateBound : ℕ}
{description : Description inputWidth gateBound}
(hdescription : description.WellFormed)
(slot : Fin gateBound)
(wireValue : Fin (inputWidth + ↑slot) → Bool)
(assignment : ℕ → Bool)
(hcode : ∀ (coordinate : Fin (codeWidth inputWidth gateBound)), assignment ↑coordinate = description.encode coordinate)
(hsources :
∀ (source : Fin (inputWidth + ↑slot)),
BoolFormula.eval assignment (sourceFormula inputWidth gateBound slot source) = wireValue source)
:
BoolFormula.eval assignment (stepFormula inputWidth gateBound slot) = (description.slots slot).toRawGate.eval (wireValue ⟨(description.slots slot).input0Value, ⋯⟩)
(wireValue ⟨(description.slots slot).input1Value, ⋯⟩)
A sequentially laid-out gate formula realizes the corresponding raw gate on any supplied family of available wire values.