Internals for batch formula compilation

This module proves the structural, topological, and iterative-evaluator laws for BoolFormula.compileRawBatch. Public statements are re-exported by Complexitylib.Circuits.Encoding.Formula.Batch.

Formula-list combinators

theorem Complexity.BoolFormula.eval_literal_internal (wire : ℕ) (value : Bool) (assignment : ℕ → Bool) : eval assignment (literal wire value) = decide (assignment wire = value)

theorem Complexity.BoolFormula.size_literal_le_two_internal (wire : ℕ) (value : Bool) : (literal wire value).size ≤ 2

theorem Complexity.BoolFormula.eval_conjs_internal (formulas : List BoolFormula) (assignment : ℕ → Bool) : eval assignment (conjs formulas) = formulas.all fun (formula : BoolFormula) => eval assignment formula

theorem Complexity.BoolFormula.eval_disjs_internal (formulas : List BoolFormula) (assignment : ℕ → Bool) : eval assignment (disjs formulas) = formulas.any fun (formula : BoolFormula) => eval assignment formula

theorem Complexity.BoolFormula.size_conjs_internal (formulas : List BoolFormula) : (conjs formulas).size = 1 + (List.map (fun (formula : BoolFormula) => formula.size + 1) formulas).sum

theorem Complexity.BoolFormula.size_disjs_internal (formulas : List BoolFormula) : (disjs formulas).size = 1 + (List.map (fun (formula : BoolFormula) => formula.size + 1) formulas).sum

Structural accounting

theorem Complexity.BoolFormula.length_compileRawOutputs_circuit_internal (available : ℕ) (formulas : List BoolFormula) : List.length (compileRawOutputs available formulas).circuit = (List.map size formulas).sum

theorem Complexity.BoolFormula.length_compileRawOutputs_outputs_internal (available : ℕ) (formulas : List BoolFormula) : (compileRawOutputs available formulas).outputs.length = formulas.length

theorem Complexity.BoolFormula.length_compileRawBatch_internal (available : ℕ) (formulas : List BoolFormula) : List.length (compileRawBatch available formulas) = (List.map size formulas).sum + formulas.length

Sequential formula evaluation

Contiguous output packing

Batch correctness

theorem Complexity.BoolFormula.evalAux?_compileRawBatch_internal (available : ℕ) [NeZero available] (formulas : List BoolFormula) (assignment : ℕ → Bool) (wires : Array Bool) (hsize : wires.size = available) (hinput : ∀ i < available, wires[i]? = some (assignment i)) (hvars : ∀ formula ∈ formulas, ∀ i ∈ formula.vars, i < available) : ∃ (result : Array Bool), (compileRawBatch available formulas).evalAux? wires = some result ∧ result.size = wires.size + (List.map size formulas).sum + formulas.length ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ ∀ (j : Fin formulas.length), result[rawBatchOutputBase available formulas + ↑j]? = some (eval assignment (formulas.get j))

theorem Complexity.BoolFormula.topologicallyWellFormed_compileRawBatch_internal (available : ℕ) [NeZero available] (formulas : List BoolFormula) (hvars : ∀ formula ∈ formulas, ∀ i ∈ formula.vars, i < available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (compileRawBatch available formulas)