Sequential fixed-width step semantics -- proof internals #
theorem
Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.decodedSlot_eq_of_code_internal
{inputWidth gateBound : ℕ}
(description : Description inputWidth gateBound)
(slot : Fin gateBound)
(assignment : ℕ → Bool)
(hcode : ∀ (coordinate : Fin (codeWidth inputWidth gateBound)), assignment ↑coordinate = description.encode coordinate)
:
theorem
Complexity.CircuitCode.FixedWidth.Description.EvaluationLayout.eval_stepFormula_internal
{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, ⋯⟩)