Simulation between circuit bases with gate budgets

J.Simulates I means that every operation of I can be computed by a circuit over J. J.SimulatesWithCost I cost also bounds the number of gates used for each operation. Replacing each gate of a program preserves all input and intermediate wire values, with total gate count at most Program.cost. The interpretations share a carrier, but their signatures and gate arities may differ. A budget may be zero when wiring suffices.

Program.simulate constructs the replacement program and wire map from supplied circuits. Program.simulateProgram and Program.simulateRenaming name these two components. Program.trace_simulate proves that this construction preserves every wire value.

Gate replacement yields equivalent circuits and preserves computation on any support. Simulations compose, multiplying uniform gate budgets, and transfer functional completeness from the simulated basis to the simulating basis.

def Cslib.Circuits.Interpretation.SimulatesWithCost {σ : Signature} {τ : Signature} {U : Type u} (J : Interpretation τ U) (I : Interpretation σ U) (cost : σ.Op → ℕ) : Prop

A simulation with a gate budget for each primitive operation.

def Cslib.Circuits.Interpretation.Simulates {σ : Signature} {τ : Signature} {U : Type u} (J : Interpretation τ U) (I : Interpretation σ U) : Prop

J simulates I if it can compute every primitive operation of I, with some gate budget.

theorem Cslib.Circuits.Interpretation.SimulatesWithCost.simulates {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {cost : σ.Op → ℕ} (h : J.SimulatesWithCost I cost) : J.Simulates I

theorem Cslib.Circuits.Interpretation.simulates_iff {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} : J.Simulates I ↔ ∀ (op : σ.Op), ∃ (c : Circuit τ (σ.Arity op) 1), c.Computes J (single (I op))

def Cslib.Circuits.Program.cost {σ : Signature} {n g : ℕ} (p : Program σ n g) (cost : σ.Op → ℕ) : ℕ

Given a cost per operation, this is the sum of the costs along a straight-line program.

@[simp]

theorem Cslib.Circuits.Program.cost_empty {σ : Signature} {n : ℕ} (cost : σ.Op → ℕ) : empty.cost cost = 0

@[simp]

theorem Cslib.Circuits.Program.cost_gate {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) (cost : σ.Op → ℕ) : (p.gate line).cost cost = p.cost cost + cost line.op

@[simp]

theorem Cslib.Circuits.Program.cost_const {σ : Signature} {n g : ℕ} (p : Program σ n g) (b : ℕ) : (p.cost fun (x : σ.Op) => b) = b * g

theorem Cslib.Circuits.Program.cost_mono {σ : Signature} {n g : ℕ} (p : Program σ n g) {cost cost' : σ.Op → ℕ} (h : ∀ (op : σ.Op), cost op ≤ cost' op) : p.cost cost ≤ p.cost cost'

def Cslib.Circuits.Program.simulate {σ : Signature} {τ : Signature} {n g : ℕ} (p : Program σ n g) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) : Program τ n (p.cost fun (op : σ.Op) => (impl op).size) × Wire.Renaming n g (p.cost fun (op : σ.Op) => (impl op).size)

Replace each operation by its supplied circuit, returning the resulting program and a map from the original wires to their replacements. The gate count is the sum of the sizes of the replacement circuits.

@[reducible, inline]

abbrev Cslib.Circuits.Program.simulateProgram {σ : Signature} {τ : Signature} {n g : ℕ} (p : Program σ n g) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) : Program τ n (p.cost fun (op : σ.Op) => (impl op).size)

The program obtained by replacing each operation by its supplied circuit.

@[reducible, inline]

abbrev Cslib.Circuits.Program.simulateRenaming {σ : Signature} {τ : Signature} {n g : ℕ} (p : Program σ n g) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) : Wire.Renaming n g (p.cost fun (op : σ.Op) => (impl op).size)

The map from original wires to their replacements in Program.simulateProgram.

theorem Cslib.Circuits.Program.trace_simulate {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n g : ℕ} (p : Program σ n g) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) (h : ∀ (op : σ.Op), (impl op).Computes J (single (I op))) (x : Fin n → U) : (p.simulateProgram impl).trace J x ∘ (p.simulateRenaming impl).apply = p.trace I x

Replacing each operation by a circuit computing it preserves every wire value.

theorem Cslib.Circuits.Program.exists_simulationWithCost {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n g : ℕ} (p : Program σ n g) (cost : σ.Op → ℕ) (h : J.SimulatesWithCost I cost) : ∃ (k : ℕ) (q : Program τ n k) (ρ : Wire.Renaming n g k), k ≤ p.cost cost ∧ ∀ (x : Fin n → U), q.trace J x ∘ ρ.apply = p.trace I x

Simulate a program over σ by a program over τ, with a bound on the number of gates.

Assume that each operation op under I is computed by a circuit under J using at most cost op gates. Replacing the gates of p : Program σ n g by these circuits produces a program q : Program τ n k with k ≤ p.cost cost.

The returned map ρ : Wire.Renaming n g k fixes the input wires and maps every gate wire of p to a wire of q carrying the same value. For every input x, the equality q.trace J x ∘ ρ = p.trace I x says that all input and intermediate values are preserved.

theorem Cslib.Circuits.Program.exists_simulation {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n g : ℕ} (p : Program σ n g) (h : J.Simulates I) : ∃ (k : ℕ) (q : Program τ n k) (ρ : Wire.Renaming n g k), ∀ (x : Fin n → U), q.trace J x ∘ ρ.apply = p.trace I x

Replace the gates of a program, preserving every input and intermediate value.

theorem Cslib.Circuits.Circuit.exists_simulationWithCost {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n m : ℕ} (c : Circuit σ n m) (cost : σ.Op → ℕ) (h : J.SimulatesWithCost I cost) : ∃ (d : Circuit τ n m), d.eval J = c.eval I ∧ d.size ≤ c.program.cost cost

The total replacement cost bounds the size of an equivalent circuit.

theorem Cslib.Circuits.Circuit.exists_simulation_le {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n m : ℕ} (c : Circuit σ n m) {b : ℕ} (h : J.SimulatesWithCost I fun (x : σ.Op) => b) : ∃ (d : Circuit τ n m), d.eval J = c.eval I ∧ d.size ≤ b * c.size

A uniform per-gate simulation budget gives a multiplicative circuit-size bound.

theorem Cslib.Circuits.Interpretation.SimulatesWithCost.refl {σ : Signature} {U : Type u} (I : Interpretation σ U) : I.SimulatesWithCost I fun (x : σ.Op) => 1

Every basis simulates itself with a one-gate budget for each operation.

theorem Cslib.Circuits.Interpretation.SimulatesWithCost.trans {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {υ : Signature} {K : Interpretation υ U} {b c : ℕ} (hK : K.SimulatesWithCost J fun (x : τ.Op) => b) (hJ : J.SimulatesWithCost I fun (x : σ.Op) => c) : K.SimulatesWithCost I fun (x : σ.Op) => b * c

Uniform simulation budgets multiply under composition.

theorem Cslib.Circuits.Circuit.exists_simulation {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n m : ℕ} (c : Circuit σ n m) (h : J.Simulates I) : ∃ (d : Circuit τ n m), d.eval J = c.eval I

Gate replacement gives an equivalent circuit over the simulating basis.

theorem Cslib.Circuits.Circuit.ComputesOn.simulation {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n m : ℕ} {c : Circuit σ n m} {S : Set (Fin n → U)} {f : (Fin n → U) → Fin m → U} (hc : c.ComputesOn I S f) (h : J.Simulates I) : ∃ (d : Circuit τ n m), d.ComputesOn J S f

Simulation preserves computation on any support.

theorem Cslib.Circuits.Circuit.Computes.simulation {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {n m : ℕ} {c : Circuit σ n m} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) (h : J.Simulates I) : ∃ (d : Circuit τ n m), d.Computes J f

Simulation preserves computation on all inputs.

theorem Cslib.Circuits.Interpretation.Simulates.refl {σ : Signature} {U : Type u} (I : Interpretation σ U) : I.Simulates I

Every basis simulates itself.

theorem Cslib.Circuits.Interpretation.Simulates.trans {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} {υ : Signature} {K : Interpretation υ U} (hK : K.Simulates J) (hJ : J.Simulates I) : K.Simulates I

Compose simulations by replacing the gates of each implementing circuit.

theorem Cslib.Circuits.Interpretation.Simulates.isComplete {σ : Signature} {τ : Signature} {U : Type u} {I : Interpretation σ U} {J : Interpretation τ U} (h : J.Simulates I) [I.IsComplete] : J.IsComplete

A basis that simulates a complete basis is itself complete.

theorem Cslib.Circuits.Interpretation.IsComplete.simulates {σ : Signature} {τ : Signature} {U : Type u} {J : Interpretation τ U} [J.IsComplete] (I : Interpretation σ U) : J.Simulates I

A complete basis simulates every interpretation on the same carrier.