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, either to functions that are already available or to functions synthesized in turn. Composition keeps everything built along the way available to later steps. The fold rules accept a bound for combining two arguments, which may itself use several gates. Ordered families allow each member to use all preceding members, with the total budget given by the sum of the step budgets. Synthesis.exists_circuit_outputs selects any tuple 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 : Wire 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.of_mem {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {f : (Fin n → U) → U} (hf : f ∈ s) : Synthesis I s {f} 0

An available function requires 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 ∪ t₁) (a + b)

Successive constructions add their gate budgets. The second construction may use the targets of the first, and both target families remain available.

theorem Cslib.Circuits.Synthesis.trans {σ : 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, keeping only the final targets.

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

A synthesis retains its sources alongside its targets.

theorem Cslib.Circuits.Synthesis.sequence {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {k : ℕ} (stages : Fin (k + 1) → Set ((Fin n → U) → U)) (cost : Fin k → ℕ) (step : ∀ (j : Fin k), Synthesis I (stages j.castSucc) (stages j.succ) (cost j)) : Synthesis I (stages 0) (stages (Fin.last k)) (∑ j : Fin k, cost j)

Compose an indexed sequence of syntheses, adding their gate budgets.

theorem Cslib.Circuits.Synthesis.ordered_family {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {s : Set ((Fin n → U) → U)} {k : ℕ} (f : Fin k → (Fin n → U) → U) (cost : Fin k → ℕ) (step : ∀ (j : Fin k), Synthesis I (s ∪ f '' {i : Fin k | i < j}) {f j} (cost j)) : Synthesis I s (Set.range f) (∑ j : Fin k, cost j)

Synthesize a family in order, allowing each function to use all preceding ones.

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_outputs {σ : 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) : ∃ (c : Circuit σ n m), (c.Computes I fun (x : Fin n → U) (j : Fin m) => f j x) ∧ c.size ≤ cost

Select a tuple of outputs from a synthesis bound. Selecting outputs, including repeated outputs or none at all, 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) : ∃ (c : Circuit σ n 1), (c.Computes I fun (x : Fin n → U) (x_1 : Fin 1) => f x) ∧ c.size ≤ cost

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

theorem Cslib.Circuits.Program.wireFunction_mem_before {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) (j : Fin g) (wire : Wire n g) (hwire : ↑wire.index < n + ↑j) : p.wireFunction I wire ∈ inputs n ∪ p.gateFunction I '' {i : Fin g | i < j}

A preceding wire is either an input or a preceding gate function.

theorem Cslib.Circuits.Program.synthesis_step {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) (j : Fin g) : Synthesis I (inputs n ∪ p.gateFunction I '' {i : Fin g | i < j}) {p.gateFunction I j} 1

Each program gate can be synthesized from the inputs and preceding gates.

theorem Cslib.Circuits.Program.synthesis_of_steps {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {g : ℕ} (p : Program σ n g) (cost : Fin g → ℕ) (step : ∀ (j : Fin g), Synthesis I (inputs n ∪ p.gateFunction I '' {i : Fin g | i < j}) {p.gateFunction I j} (cost j)) : Synthesis I (inputs n) (available I p) (∑ j : Fin g, cost j)

Rebuild a program from gatewise synthesis bounds, retaining every wire function.