Shannon synthesis with a shared column library

Split the inputs into a short address block and a data block. Build both tables of minterms, then every Boolean function of the address block. For each data assignment, select its column of the supplied truth table, conjoin it with that assignment's minterm, and disjoin the rows.

The construction uses native CSLib circuits and the existing balanced Boolean formulas. Its finite gate bound counts constants and negations, as well as binary gates. The companion ShannonSynthesis module chooses the address width to obtain a uniform 27 * 2 ^ n / n bound.

Main definitions

• Cslib.Circuits.Boolean.ShannonSynthesis.columnFormula, Cslib.Circuits.Boolean.ShannonSynthesis.columnLibrary: disjunction formula for a bit pattern and circuit computing all disjunctions of an address minterm table.
• Cslib.Circuits.Boolean.ShannonSynthesis.column, Cslib.Circuits.Boolean.ShannonSynthesis.rowFormula, Cslib.Circuits.Boolean.ShannonSynthesis.outputFormula: truth-table column index, single-row conjunction formula, and final disjunction of rows.
• Cslib.Circuits.Boolean.ShannonSynthesis.splitMinterms, Cslib.Circuits.Boolean.ShannonSynthesis.libraryAndData, Cslib.Circuits.Boolean.ShannonSynthesis.circuit: block minterm tables, address library paired with data minterms, and synthesized circuit on split inputs.
• Cslib.Circuits.Boolean.ShannonSynthesis.bound: the finite construction budget.

Main results

• Cslib.Circuits.Boolean.ShannonSynthesis.eval_circuit: correctness of the synthesized circuit.
• Cslib.Circuits.Boolean.ShannonSynthesis.size_circuit_le: the complete finite gate ledger.

References

• C. E. Shannon, The Synthesis of Two-Terminal Switching Circuits.
• Adapted from MassProduction/ShannonCircuit.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.ShannonSynthesis.columnFormula {n : ℕ} (pattern : BitString n) : Formula signature n

Disjoin exactly the input coordinates selected by a bit vector.

@[simp]

theorem Cslib.Circuits.Boolean.ShannonSynthesis.eval_columnFormula {n : ℕ} (pattern x : BitString n) : (columnFormula pattern).eval interpretation x = decide (∃ (i : Fin n), pattern i = true ∧ x i = true)

columnFormula pattern evaluates to true on x if and only if some coordinate i has both pattern i = true and x i = true.

theorem Cslib.Circuits.Boolean.ShannonSynthesis.size_columnFormula_le {n : ℕ} (hn : 0 < n) (pattern : BitString n) : (columnFormula pattern).size ≤ n

A nonempty ambient table bounds even the empty disjunction's constant gate.

def Cslib.Circuits.Boolean.ShannonSynthesis.columnLibrary (k : ℕ) : Circuit signature (2 ^ k) (2 ^ 2 ^ k)

Every pattern of a table of address minterms is computed once and shared by all data rows.

@[simp]

theorem Cslib.Circuits.Boolean.ShannonSynthesis.eval_columnLibrary_minterms {k : ℕ} (x : BitString k) (p : Fin (2 ^ 2 ^ k)) : (columnLibrary k).eval interpretation ((mintermCircuit k).eval interpretation x) p = (BitString.equivFin (2 ^ k)).symm p ((BitString.equivFin k) x)

Evaluating columnLibrary k on the minterm indicators of x yields at output p the value of the pth Boolean function at the index of x.

theorem Cslib.Circuits.Boolean.ShannonSynthesis.size_columnLibrary_le (k : ℕ) : (columnLibrary k).size ≤ 2 ^ 2 ^ k * 2 ^ k

columnLibrary k has size at most 2 ^ (2 ^ k) * 2 ^ k.

def Cslib.Circuits.Boolean.ShannonSynthesis.column {k d : ℕ} (f : BooleanFunction (k + d)) (y : Fin (2 ^ d)) : Fin (2 ^ 2 ^ k)

The truth-table column at one data assignment, indexed as an address-value bit string.

def Cslib.Circuits.Boolean.ShannonSynthesis.rowFormula {k d : ℕ} (f : BooleanFunction (k + d)) (y : Fin (2 ^ d)) : Formula signature (2 ^ 2 ^ k + 2 ^ d)

One row uses the selected column and the corresponding data minterm.

def Cslib.Circuits.Boolean.ShannonSynthesis.outputFormula {k d : ℕ} (f : BooleanFunction (k + d)) : Formula signature (2 ^ 2 ^ k + 2 ^ d)

The final disjunction of rows.

theorem Cslib.Circuits.Boolean.ShannonSynthesis.size_outputFormula_le {k d : ℕ} (f : BooleanFunction (k + d)) : (outputFormula f).size ≤ 2 * 2 ^ d

outputFormula f has size at most 2 * 2 ^ d.

def Cslib.Circuits.Boolean.ShannonSynthesis.splitMinterms (k d : ℕ) : Circuit signature (k + d) (2 ^ k + 2 ^ d)

The two minterm tables read disjoint coordinate blocks.

def Cslib.Circuits.Boolean.ShannonSynthesis.libraryAndData (k d : ℕ) : Circuit signature (2 ^ k + 2 ^ d) (2 ^ 2 ^ k + 2 ^ d)

Compute the address library while retaining the data minterms as free wires.

def Cslib.Circuits.Boolean.ShannonSynthesis.circuit {k d : ℕ} (f : BooleanFunction (k + d)) : Circuit signature (k + d) 1

Synthesize a Boolean function from shared minterms, address columns and row selection.

@[simp]

theorem Cslib.Circuits.Boolean.ShannonSynthesis.eval_circuit {k d : ℕ} (f : BooleanFunction (k + d)) (x : BitString (k + d)) (i : Fin 1) : (circuit f).eval interpretation x i = f x

The selected row and address column reconstruct the original input.

def Cslib.Circuits.Boolean.ShannonSynthesis.bound (k d : ℕ) : ℕ

The complete gate budget, before choosing the split.

theorem Cslib.Circuits.Boolean.ShannonSynthesis.size_circuit_le {k d : ℕ} (f : BooleanFunction (k + d)) : (circuit f).size ≤ bound k d

Shared minterms, shared columns and the final row disjunction account for every gate.