Fixed-width encoded-gate evaluation formulas

This module exposes the exact semantics, tree size, and support of the formula that evaluates one gate slot in a fixed-width circuit description.

@[simp]

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

Conditional formula negation agrees with Boolean XOR.

@[simp]

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

The compact conditional-negation formula has its exact tree size.

@[simp]

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.eval_applyOperation (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

The operation formula follows the fixed-width true-AND, false-OR convention.

@[simp]

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

The compact operation-selection formula has its exact tree size.

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.eval_gate {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, ⋯⟩))

Under the slot's backward-reference invariant, the encoded-gate formula agrees exactly with the raw gate selected by the assignment's code prefix.

@[simp]

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.size_gate {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

Exact encoded-gate formula size for one-node source formulas.

theorem Complexity.CircuitCode.FixedWidth.Description.GateFormula.vars_gate_lt {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

The gate formula only references its code prefix and declared sources.