Boolean-formula raw compiler internals

This module proves the structural and semantic invariants of the proof-free formula compiler. Public statements are re-exported by Complexitylib.Circuits.Encoding.Formula.

theorem Complexity.BoolFormula.length_compileRaw_internal (available : ℕ) (formula : BoolFormula) : List.length (compileRaw available formula) = formula.size

Internal exact gate-count theorem for formula compilation.

theorem Complexity.BoolFormula.rawOutputWire_lt_internal (available : ℕ) (formula : BoolFormula) : rawOutputWire available formula < available + formula.size

Internal bound placing the output inside its compiled fragment.

theorem Complexity.BoolFormula.rawOutputWire_eq_internal (available : ℕ) (formula : BoolFormula) : rawOutputWire available formula = available + List.length (compileRaw available formula) - 1

Internal equation identifying the fragment's final wire.

theorem Complexity.BoolFormula.evalAux?_compileRaw_of_agree_internal (available : ℕ) [NeZero available] (formula : BoolFormula) (assignment : ℕ → Bool) (wires : Array Bool) (hsize : wires.size = available) (hvars : ∀ i ∈ formula.vars, i < available) (hagree : ∀ i ∈ formula.vars, wires[i]? = some (assignment i)) : ∃ (result : Array Bool), (compileRaw available formula).evalAux? wires = some result ∧ result.size = wires.size + formula.size ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[rawOutputWire available formula]? = some (eval assignment formula)

theorem Complexity.BoolFormula.evalAux?_compileRaw_internal (available : ℕ) [NeZero available] (formula : BoolFormula) (assignment : ℕ → Bool) (wires : Array Bool) (hsize : wires.size = available) (hinput : ∀ i < available, wires[i]? = some (assignment i)) (hvars : ∀ i ∈ formula.vars, i < available) : ∃ (result : Array Bool), (compileRaw available formula).evalAux? wires = some result ∧ result.size = wires.size + formula.size ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ result[rawOutputWire available formula]? = some (eval assignment formula)

Internal semantic correctness theorem for formula fragments.

theorem Complexity.BoolFormula.topologicallyWellFormed_compileRaw_internal (available : ℕ) [NeZero available] (formula : BoolFormula) (hvars : ∀ i ∈ formula.vars, i < available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (compileRaw available formula)

Internal topological correctness theorem for formula fragments.