Building circuits from available functions

An existing circuit can be inserted into a synthesis construction by wiring its inputs to available functions. Its outputs then become available at a cost of its number of gates, while all previously computed functions remain available. Repeated inputs share their original wires.

Synthesis.Builder accumulates available wires and gate costs through Builder.start and Builder.add. Each appended construction is charged once; selecting and reusing wires is free. Builder.finish selects the outputs and checks the requested bound. These operations compose ordinary Synthesis certificates; they do not search for a cheaper construction.

Main definitions

• Cslib.Circuits.Synthesis.Builder: available wires and their accumulated synthesis bound.

Main results

• Cslib.Circuits.Synthesis.circuit: applying a circuit costs its number of gates.
• Cslib.Circuits.Synthesis.Builder.finish: select outputs within a requested gate budget.

References

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

theorem Cslib.Circuits.Synthesis.circuit {σ : Signature} {U : Type u} {I : Interpretation σ U} {n : ℕ} {s : Set ((Fin n → U) → U)} {m p : ℕ} (c : Circuit σ m p) (g : Fin m → (Fin n → U) → U) (hg : ∀ (i : Fin m), g i ∈ s) : Synthesis I s (Set.range fun (j : Fin p) (x : Fin n → U) => c.eval I (fun (i : Fin m) => g i x) j) c.size

A circuit whose inputs are fed by available functions computes its outputs with as many additional gates as it has. The functions feeding the inputs may repeat.

structure Cslib.Circuits.Synthesis.Builder {σ : Signature} {U : Type u} {n : ℕ} (I : Interpretation σ U) (s : Set ((Fin n → U) → U)) : Type u

A sequence of certified constructions, including every wire available along the way.

• wires : Set ((Fin n → U) → U)

  Original sources and all outputs built so far.

• cost : ℕ

  Sum of the appended constructions' gate budgets.

• bound : Synthesis I s self.wires self.cost

  The accumulated synthesis certificate.

def Cslib.Circuits.Synthesis.Builder.start {σ : Signature} {U : Type u} {n : ℕ} (I : Interpretation σ U) (s : Set ((Fin n → U) → U)) : Builder I s

Begin with the source wires, without adding gates.

def Cslib.Circuits.Synthesis.Builder.add {σ : Signature} {U : Type u} {I : Interpretation σ U} {n : ℕ} {s : Set ((Fin n → U) → U)} (b : Builder I s) {t : Set ((Fin n → U) → U)} {k : ℕ} (h : Synthesis I b.wires t k) : Builder I s

Append a construction whose inputs are available, retaining both old and new wires.

theorem Cslib.Circuits.Synthesis.Builder.finish {σ : Signature} {U : Type u} {I : Interpretation σ U} {n : ℕ} {s : Set ((Fin n → U) → U)} (b : Builder I s) {t : Set ((Fin n → U) → U)} {k : ℕ} (ht : t ⊆ b.wires) (hk : b.cost ≤ k) : Synthesis I s t k

Select outputs from the final wires and enlarge the accumulated budget.