Boolean synthesis

The generic synthesis rules specialize to the De Morgan basis: constants, negation, conjunction, and disjunction. Finite conjunctions and disjunctions use the generic fold bound, and synthesis_minterm combines literals to test a specified tuple of input bits.

theorem Cslib.Circuits.Synthesis.const {n : ℕ} {s : Set (BooleanFunction n)} (value : Bool) : Synthesis Boolean.interpretation s {fun (x : Fin n → Bool) => value} 1

Constants cost one gate.

theorem Cslib.Circuits.Synthesis.not {n : ℕ} {s : Set (BooleanFunction n)} {a : ℕ} {f : BooleanFunction n} (h : Synthesis Boolean.interpretation s {f} a) : Synthesis Boolean.interpretation s {fun (x : BitString n) => !f x} (a + 1)

Apply negation to a synthesized function.

theorem Cslib.Circuits.Synthesis.and {n : ℕ} {s : Set (BooleanFunction n)} {a b : ℕ} {f g : BooleanFunction n} (hf : Synthesis Boolean.interpretation s {f} a) (hg : Synthesis Boolean.interpretation s {g} b) : Synthesis Boolean.interpretation s {fun (x : BitString n) => f x && g x} (a + b + 1)

Binary conjunction costs one gate beyond its arguments.

theorem Cslib.Circuits.Synthesis.or {n : ℕ} {s : Set (BooleanFunction n)} {a b : ℕ} {f g : BooleanFunction n} (hf : Synthesis Boolean.interpretation s {f} a) (hg : Synthesis Boolean.interpretation s {g} b) : Synthesis Boolean.interpretation s {fun (x : BitString n) => f x || g x} (a + b + 1)

Binary disjunction costs one gate beyond its arguments.

theorem Cslib.Circuits.Synthesis.xor_of_mem {n : ℕ} {s : Set (BooleanFunction n)} {f g : BooleanFunction n} (hf : f ∈ s) (hg : g ∈ s) : Synthesis Boolean.interpretation s {fun (x : BitString n) => f x ^^ g x} 4

XOR costs four gates when its two arguments are already available. The intermediate conjunction and disjunction are shared.

theorem Cslib.Circuits.Synthesis.exists_mem {n : ℕ} {ι : Type u} {s : Set (BooleanFunction n)} (indices : Finset ι) (f : ι → BooleanFunction n) (cost : ι → ℕ) (h : ∀ i ∈ indices, Synthesis Boolean.interpretation s {f i} (cost i)) : Synthesis Boolean.interpretation s {fun (x : BitString n) => decide (∃ i ∈ indices, f i x = true)} (∑ i ∈ indices, (cost i + 1) + 1)

Disjoin a finite family of functions. The extra gate supplies the empty disjunction.

theorem Cslib.Circuits.Synthesis.forall_mem {n : ℕ} {ι : Type u} {s : Set (BooleanFunction n)} (indices : Finset ι) (f : ι → BooleanFunction n) (cost : ι → ℕ) (h : ∀ i ∈ indices, Synthesis Boolean.interpretation s {f i} (cost i)) : Synthesis Boolean.interpretation s {fun (x : BitString n) => decide (∀ i ∈ indices, f i x = true)} (∑ i ∈ indices, (cost i + 1) + 1)

Conjoin a finite family of functions. The extra gate supplies the empty conjunction.

theorem Cslib.Circuits.Boolean.synthesis_minterm {n k : ℕ} (wires : Fin k → Fin n) (value : Fin k → Bool) : Synthesis interpretation (inputs n) {fun (x : Fin n → Bool) => decide ((fun (i : Fin k) => x (wires i)) = value)} (2 * k + 1)

A conjunction testing a specified tuple of input bits.