Batch compilation of Boolean formulas

This module exposes finite Boolean-formula combinators and a batch compiler that turns a list of formulas into appendable raw circuit syntax. Every source formula is evaluated against the incoming prefix; a final copy phase places all results in one contiguous block starting at rawBatchOutputBase.

Main definitions and results

• BoolFormula.literal, conjs, and disjs: small formula constructors.
• BoolFormula.compileRawOutputs: sequential variable-sized compilation.
• BoolFormula.compileRawBatch: sequential compilation plus output packing.
• BoolFormula.length_compileRawBatch: exact gate count.
• BoolFormula.topologicallyWellFormed_compileRawBatch: backward references.
• BoolFormula.evalAux?_compileRawBatch: exact packed-output semantics.

@[simp]

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

A literal evaluates to whether its source wire has the requested value.

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

A literal requires at most two formula nodes.

@[simp]

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

Finite conjunction evaluates as Boolean List.all.

@[simp]

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

Finite disjunction evaluates as Boolean List.any.

@[simp]

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

Exact tree size of a finite conjunction.

@[simp]

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

Exact tree size of a finite disjunction.

@[simp]

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

Sequential compilation emits the sum of the formula tree sizes.

@[simp]

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

Sequential compilation records exactly one output per formula.

@[simp]

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

A packed batch emits every formula gate and one final copy per formula.

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

If every formula variable names an incoming wire, the entire packed batch is topologically well formed.

theorem Complexity.BoolFormula.evalAux?_compileRawBatch (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))

Batch evaluation preserves the incoming memo array and packs source formula values into a contiguous final block, in source order.