Simultaneous circuit synthesis

Synthesis I sources targets cost bounds the number of additional gates needed to compute targets from sources under an interpretation I. Every function already available in the starting program remains available, so successive constructions can share intermediate results. The signature and its carrier are arbitrary; neither needs to be finite or decidable.

The core rules compose bounds, combine finite families, and apply operations of the signature. The fold rules accept a bound for combining two arguments, which may itself use several gates. Synthesis.exists_circuit_family selects any finite family of outputs without adding gates; Synthesis.exists_circuit specializes this to a single output.

def Cslib.Circuits.inputs {U : Type u} (n : ℕ) : Set ((Fin n → U) → U)

The coordinate projections supplied by the circuit's inputs.

Equations

• Cslib.Circuits.inputs n = Set.range fun (i : Fin n) (x : Fin n → U) => x i

def Cslib.Circuits.available {σ : Signature} {U : Type u} {n : ℕ} (I : Interpretation σ U) {g : ℕ} (p : Program σ n g) : Set ((Fin n → U) → U)

The functions computed by the wires of p, whether input wires or internal gates.

Equations

• Cslib.Circuits.available I p = Set.range (p.wireFunction I)

theorem Cslib.Circuits.mem_available {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} {p : Program σ n g} {f : (Fin n → U) → U} : f ∈ available I p ↔ ∃ (w : Fin (n + g)), ∀ (x : Fin n → U), p.trace I x w = f x

A function is available exactly when some wire computes it pointwise.

theorem Cslib.Circuits.inputs_subset_available {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) : inputs n ⊆ available I p

The input projections are available in every program.

def Cslib.Circuits.Synthesis {σ : Signature} {U : Type u} {n : ℕ} (I : Interpretation σ U) (sources targets : Set ((Fin n → U) → U)) (cost : ℕ) : Prop

Synthesis I sources targets cost says that targets can be computed from sources using at most cost additional gates, without losing anything already computed.

Precisely: for every program p₁ on whose wires every function in sources is available, there is a program p₂ such that

• p₂ has at most cost more gates than p₁,
• every function available in p₁ is still available in p₂, and
• every function in targets is available in p₂.

Quantifying over an arbitrary starting program, rather than the empty one, is what lets constructions share intermediate results: Synthesis.comp adds budgets because the second construction may reuse wires built by the first.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Circuits.Synthesis.of_subset {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s t : Set ((Fin n → U) → U)} (h : t ⊆ s) : Synthesis I s t 0

Available functions require no additional gates.

theorem Cslib.Circuits.Synthesis.mono {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s t : Set ((Fin n → U) → U)} {a b : ℕ} (h : Synthesis I s t a) {s' t' : Set ((Fin n → U) → U)} (hs : s ⊆ s') (ht : t' ⊆ t) (hab : a ≤ b) : Synthesis I s' t' b

Enlarge the source family, narrow the target family, or increase the budget.

theorem Cslib.Circuits.Synthesis.comp {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s t t₁ : Set ((Fin n → U) → U)} {a b : ℕ} (h : Synthesis I s t a) (h' : Synthesis I (s ∪ t) t₁ b) : Synthesis I s t₁ (a + b)

Successive constructions add their gate budgets.

theorem Cslib.Circuits.Synthesis.union {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s t t₁ : Set ((Fin n → U) → U)} {a b : ℕ} (h : Synthesis I s t a) (h' : Synthesis I s t₁ b) : Synthesis I s (t ∪ t₁) (a + b)

Combine two target families, preserving the first while constructing the second.

theorem Cslib.Circuits.Synthesis.gate {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} (op : σ.Op) (args : Fin (σ.Arity op) → (Fin n → U) → U) (hargs : ∀ (i : Fin (σ.Arity op)), args i ∈ s) : Synthesis I s {fun (x : Fin n → U) => I op fun (i : Fin (σ.Arity op)) => args i x} 1

Synthesize an operation whose arguments are already available.

theorem Cslib.Circuits.Synthesis.biUnion {σ : Signature} {U : Type u} {n : ℕ} {ι : Type w} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} (indices : Finset ι) (targets : ι → Set ((Fin n → U) → U)) (cost : ι → ℕ) (h : ∀ i ∈ indices, Synthesis I s (targets i) (cost i)) : Synthesis I s (⋃ i ∈ indices, targets i) (∑ i ∈ indices, cost i)

Combine a finite family of target sets, retaining all earlier results.

theorem Cslib.Circuits.Synthesis.iUnion {σ : Signature} {U : Type u} {n : ℕ} {ι : Type w} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} [Fintype ι] (targets : ι → Set ((Fin n → U) → U)) (cost : ι → ℕ) (h : ∀ (i : ι), Synthesis I s (targets i) (cost i)) : Synthesis I s (⋃ (i : ι), targets i) (∑ i : ι, cost i)

Combine target sets indexed by a finite type.

theorem Cslib.Circuits.Synthesis.family {σ : Signature} {U : Type u} {n : ℕ} {ι : Type w} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} [Fintype ι] (f : ι → (Fin n → U) → U) (cost : ι → ℕ) (h : ∀ (i : ι), Synthesis I s {f i} (cost i)) : Synthesis I s (Set.range f) (∑ i : ι, cost i)

Simultaneously synthesize an indexed finite family of functions.

theorem Cslib.Circuits.Synthesis.gate_of_syntheses {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} (op : σ.Op) (args : Fin (σ.Arity op) → (Fin n → U) → U) (cost : Fin (σ.Arity op) → ℕ) (h : ∀ (i : Fin (σ.Arity op)), Synthesis I s {args i} (cost i)) : Synthesis I s {fun (x : Fin n → U) => I op fun (i : Fin (σ.Arity op)) => args i x} (∑ i : Fin (σ.Arity op), cost i + 1)

Synthesize every argument, then apply an operation with one further gate.

theorem Cslib.Circuits.Synthesis.nullary {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} (op : σ.Op) (arity : σ.Arity op = 0) : Synthesis I s {fun (x : Fin n → U) => I op fun (i : Fin (σ.Arity op)) => (Fin.cast arity i).elim0} 1

A nullary operation supplies its interpreted constant with one gate.

theorem Cslib.Circuits.Synthesis.unary {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {a : ℕ} {f : (Fin n → U) → U} (h : Synthesis I s {f} a) (op : σ.Op) : Synthesis I s {fun (x : Fin n → U) => I op fun (x_1 : Fin (σ.Arity op)) => f x} (a + 1)

Feed a synthesized function to every argument of an operation, using one further gate. In particular, this applies a unary operation.

theorem Cslib.Circuits.Synthesis.binary {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {a b : ℕ} {f g : (Fin n → U) → U} (hf : Synthesis I s {f} a) (hg : Synthesis I s {g} b) (op : σ.Op) : Synthesis I s {fun (x : Fin n → U) => I op fun (i : Fin (σ.Arity op)) => if ↑i = 0 then f x else g x} (a + b + 1)

Feed f to argument zero and g to the remaining arguments, using one further gate. For a binary operation, these are its two arguments.

theorem Cslib.Circuits.Synthesis.combine {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {a b : ℕ} {f g result : (Fin n → U) → U} {c : ℕ} (hf : Synthesis I s {f} a) (hg : Synthesis I s {g} b) (h : Synthesis I {f, g} {result} c) : Synthesis I s {result} (a + b + c)

Apply a synthesis bound to two previously synthesized arguments. The combining construction can use several gates and can reuse either argument.

theorem Cslib.Circuits.Synthesis.foldr {σ : Signature} {U : Type u} {n : ℕ} {ι : Type w} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {a : ℕ} (op : U → U → U) (combineCost : ℕ) (hop : ∀ (f g : (Fin n → U) → U), Synthesis I {f, g} {fun (x : Fin n → U) => op (f x) (g x)} combineCost) (indices : List ι) (f : ι → (Fin n → U) → U) (cost : ι → ℕ) (seed : (Fin n → U) → U) (hseed : Synthesis I s {seed} a) (h : ∀ i ∈ indices, Synthesis I s {f i} (cost i)) : Synthesis I s {fun (x : Fin n → U) => List.foldr (fun (i : ι) (acc : U) => op (f i x) acc) (seed x) indices} ((List.map (fun (i : ι) => cost i + combineCost) indices).sum + a)

Fold an ordered list of synthesized functions. No algebraic laws are needed for the combining operation. The seed and the combining construction have their own gate budgets.

theorem Cslib.Circuits.Synthesis.finset_fold {σ : Signature} {U : Type u} {n : ℕ} {ι : Type w} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {a : ℕ} (op : U → U → U) [Std.Commutative op] [Std.Associative op] (combineCost : ℕ) (hop : ∀ (f g : (Fin n → U) → U), Synthesis I {f, g} {fun (x : Fin n → U) => op (f x) (g x)} combineCost) (indices : Finset ι) (f : ι → (Fin n → U) → U) (cost : ι → ℕ) (seed : (Fin n → U) → U) (hseed : Synthesis I s {seed} a) (h : ∀ i ∈ indices, Synthesis I s {f i} (cost i)) : Synthesis I s {fun (x : Fin n → U) => Finset.fold op (seed x) (fun (i : ι) => f i x) indices} (∑ i ∈ indices, (cost i + combineCost) + a)

Fold a finite set of synthesized functions with a commutative associative operation. The seed need not be an identity or a constant, and the combining construction may use several gates.

theorem Cslib.Circuits.Synthesis.exists_circuit_family {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {m cost : ℕ} {f : Fin m → (Fin n → U) → U} (h : Synthesis I (inputs n) (Set.range f) cost) : ∃ g ≤ cost, ∃ (c : Circuit σ n g m), ∀ (x : Fin n → U) (j : Fin m), c.eval I x j = f j x

Select a finite family of outputs from a synthesis bound. Selecting outputs, including repeated outputs or an empty family, requires no additional gates.

theorem Cslib.Circuits.Synthesis.exists_circuit {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → U} {cost : ℕ} (h : Synthesis I (inputs n) {f} cost) : ∃ g ≤ cost, ∃ (c : Circuit σ n g 1), c.Computes I f

Extract a single-output circuit from a synthesis bound on the input projections.