Fixed-width encoded-gate evaluation formulas -- proof internals

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.eval_negateIf_internal (flag value : BoolFormula) (assignment : ℕ → Bool) : BoolFormula.eval assignment (negateIf flag value) = (BoolFormula.eval assignment flag ^^ BoolFormula.eval assignment value)

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.size_negateIf_internal (flag value : BoolFormula) : (negateIf flag value).size = 2 * flag.size + 2 * value.size + 4

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.vars_negateIf_lt_internal (flag value : BoolFormula) (available : ℕ) (hflag : ∀ wire ∈ flag.vars, wire < available) (hvalue : ∀ wire ∈ value.vars, wire < available) (wire : ℕ) : wire ∈ (negateIf flag value).vars → wire < available

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.eval_applyOperation_internal (operation left right : BoolFormula) (assignment : ℕ → Bool) : BoolFormula.eval assignment (applyOperation operation left right) = match BoolFormula.eval assignment operation with | true => BoolFormula.eval assignment left && BoolFormula.eval assignment right | false => BoolFormula.eval assignment left || BoolFormula.eval assignment right

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.size_applyOperation_internal (operation left right : BoolFormula) : (applyOperation operation left right).size = operation.size + 2 * left.size + 2 * right.size + 5

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.vars_applyOperation_lt_internal (operation left right : BoolFormula) (available : ℕ) (hoperation : ∀ wire ∈ operation.vars, wire < available) (hleft : ∀ wire ∈ left.vars, wire < available) (hright : ∀ wire ∈ right.vars, wire < available) (wire : ℕ) : wire ∈ (applyOperation operation left right).vars → wire < available

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.eval_gate_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (sources : Fin (inputWidth + ↑slot) → BoolFormula) (assignment : ℕ → Bool) (hslot : (decodedSlot inputWidth gateBound slot assignment).WellFormedAt (inputWidth + ↑slot)) : BoolFormula.eval assignment (gate inputWidth gateBound slot sources) = (decodedSlot inputWidth gateBound slot assignment).toRawGate.eval (BoolFormula.eval assignment (sources ⟨(decodedSlot inputWidth gateBound slot assignment).input0Value, ⋯⟩)) (BoolFormula.eval assignment (sources ⟨(decodedSlot inputWidth gateBound slot assignment).input1Value, ⋯⟩))

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.size_gate_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (sources : Fin (inputWidth + ↑slot) → BoolFormula) (hsources : ∀ (source : Fin (inputWidth + ↑slot)), (sources source).size = 1) : (gate inputWidth gateBound slot sources).size = gateSize inputWidth gateBound slot

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.vars_gate_lt_internal {inputWidth gateBound available : ℕ} (slot : Fin gateBound) (sources : Fin (inputWidth + ↑slot) → BoolFormula) (hcode : codeWidth inputWidth gateBound ≤ available) (hsources : ∀ (source : Fin (inputWidth + ↑slot)), ∀ wire ∈ (sources source).vars, wire < available) (wire : ℕ) : wire ∈ (gate inputWidth gateBound slot sources).vars → wire < available