Linear-size segmented propagation circuits

Source bits occupy the first input block and links the second. The circuit outputs every prefix value of BitString.propagate: one false constant initializes the computation, and each record adds an AND gate and an OR gate. Earlier values are shared wires, so the gate count is linear even when links connect a long run.

Main definitions

• Cslib.Circuits.Boolean.propagateCircuit: all prefix values in input order.

Main results

• Cslib.Circuits.Boolean.eval_propagateCircuit: agreement with the functional recurrence.
• Cslib.Circuits.Boolean.eval_propagateCircuit_eq_true_iff: a connected true source exists.
• Cslib.Circuits.Boolean.cost_program_propagateCircuit: exact arbitrary weighted cost.
• Cslib.Circuits.Boolean.size_propagateCircuit: one constant and two gates per record.

Weighted cost distinguishes conventions that charge the initial constant from those that make constants free. The zero-record circuit still contains its unused initial constant. The constructor is executable; these gate counts do not certify its running time.

References

• Adapted from MassProduction/Nonuniform/Propagation.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.propagateCircuit (count : ℕ) : Circuit signature (count + count) count

All propagated prefix values, sharing earlier values as circuit wires.

def Cslib.Circuits.Boolean.propagateCircuit.program (count processed : ℕ) : processed ≤ count → Program signature (count + count) (1 + 2 * processed)

Two gates per processed record, after a single false constant.

def Cslib.Circuits.Boolean.propagateCircuit.inputBlock {count : ℕ} (x : BitString count) (i : ℕ) : Bool

Extend a finite input block by false beyond its endpoint.

theorem Cslib.Circuits.Boolean.eval_propagateCircuit_program {count : ℕ} (x : BitString (count + count)) (processed : ℕ) (fits : processed ≤ count) (prefixCount : ℕ) (hle : prefixCount ≤ processed) : (propagateCircuit.program count processed fits).eval interpretation x ⟨2 * prefixCount, ⋯⟩ = BitString.propagate (propagateCircuit.inputBlock (x ∘ Fin.castAdd count)) (propagateCircuit.inputBlock (x ∘ Fin.natAdd count)) prefixCount

Every earlier prefix value is retained at the corresponding even-numbered gate.

theorem Cslib.Circuits.Boolean.eval_propagateCircuit {count : ℕ} (x : BitString (count + count)) (j : Fin count) : (propagateCircuit count).eval interpretation x j = BitString.propagate (propagateCircuit.inputBlock (x ∘ Fin.castAdd count)) (propagateCircuit.inputBlock (x ∘ Fin.natAdd count)) (↑j + 1)

Every output is the recurrence value after processing its record.

theorem Cslib.Circuits.Boolean.eval_propagateCircuit_eq_true_iff {count : ℕ} (source link : BitString count) (j : Fin count) : (propagateCircuit count).eval interpretation (Fin.append source link) j = true ↔ ∃ start ≤ j, source start = true ∧ ∀ (index : Fin count), start < index → index ≤ j → link index = true

A finite-array interface: a true output has an earlier true source connected by links. The link at the source itself need not be true.

theorem Cslib.Circuits.Boolean.cost_propagateCircuit_program (count processed : ℕ) (fits : processed ≤ count) (cost : signature.Op → ℕ) : (propagateCircuit.program count processed fits).cost cost = cost (Op.const false) + processed * (cost Op.and + cost Op.or)

Each prefix contributes one AND and one OR, independently of the input links.

theorem Cslib.Circuits.Boolean.cost_program_propagateCircuit (count : ℕ) (cost : signature.Op → ℕ) : (propagateCircuit count).program.cost cost = cost (Op.const false) + count * (cost Op.and + cost Op.or)

The exact weighted cost includes the initial constant, even for zero records.

@[simp]

theorem Cslib.Circuits.Boolean.size_propagateCircuit (count : ℕ) : (propagateCircuit count).size = 1 + 2 * count

The circuit contains one false constant and two gates per record.