Documentation

Complexity.Computability.Circuit.Simulation

Circuit simulation and exact costs #

The cost of a program is the sum of the costs of its lines (Program.cost_eq_sum), so a bound on the cost of every operation bounds the cost of the program by the number of gates (Program.cost_le_mul). Costs add up along the composition of circuits (Circuit.cost_program_comp, Circuit.cost_program_append, Circuit.cost_program_pi). Replacing each gate by a supplied circuit also preserves costs exactly, charging the source operation the entire cost of its replacement (Circuit.cost_program_simulate).

Main definitions #

Main results #

source
theorem Cslib.Circuits.Program.cost_eq_sum {σ : Signature} {n g : ℕ} (p : Program σ n g) (cost : σ.Op → ℕ) :
p.cost cost = ∑ k : Fin g, cost (p.lines k).op

The cost of a program is the sum of the costs of its lines.

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

If every operation costs at most b, a program with g gates costs at most b * g.

source
@[simp]
theorem Cslib.Circuits.Program.cost_append {σ : Signature} {n g k g₂ : ℕ} (p : Program σ n g) (feed : Fin k → Wire n g) (q : Program σ k g₂) (cost : σ.Op → ℕ) :
(p.append feed q).cost cost = p.cost cost + q.cost cost

Continuing a program adds the costs.

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

Weighted simulation cost is exactly the sum of the replacement-circuit costs.

source
def Cslib.Circuits.Circuit.simulate {σ : Signature} {τ : Signature} {n m : ℕ} (c : Circuit σ n m) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) :
Circuit τ n m

The circuit with every gate replaced by the circuit impl op for its operation.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Circuit.size_simulate {σ : Signature} {τ : Signature} {n m : ℕ} (c : Circuit σ n m) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) :
    (c.simulate impl).size = c.program.cost fun (op : σ.Op) => (impl op).size
    source
    theorem Cslib.Circuits.Circuit.eval_simulate {σ : Signature} {τ : Signature} {U : Type u} {n m : ℕ} {I : Interpretation σ U} {J : Interpretation τ U} (c : Circuit σ n m) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) (h : ∀ (op : σ.Op), (impl op).Computes J (single (I op))) :
    (c.simulate impl).eval J = c.eval I

    Replacing the gates by circuits computing their operations computes the same function.

    The costs of circuits built from smaller ones. They are not simp lemmas: simp would first rewrite the number of gates, an implicit argument of Program.cost, by Circuit.size_comp and the like, after which they no longer match. They apply with rw and simp only.

    source
    theorem Cslib.Circuits.Circuit.cost_program_wiring {σ : Signature} {n m : ℕ} (select : Fin m → Fin n) (cost : σ.Op → ℕ) :
    (wiring σ select).program.cost cost = 0
    source
    theorem Cslib.Circuits.Circuit.cost_program_oneGate {σ : Signature} {n : ℕ} (op : σ.Op) (args : Fin (σ.Arity op) → Fin n) (cost : σ.Op → ℕ) :
    (oneGate op args).program.cost cost = cost op
    source
    theorem Cslib.Circuits.Circuit.cost_program_comp {σ : Signature} {n m p : ℕ} (d : Circuit σ m p) (c : Circuit σ n m) (cost : σ.Op → ℕ) :
    (d.comp c).program.cost cost = c.program.cost cost + d.program.cost cost

    Sequential composition adds the costs.

    source
    theorem Cslib.Circuits.Circuit.cost_program_append {σ : Signature} {n m p : ℕ} (c : Circuit σ n m) (d : Circuit σ n p) (cost : σ.Op → ℕ) :
    (c.append d).program.cost cost = c.program.cost cost + d.program.cost cost

    Parallel composition adds the costs.

    source
    theorem Cslib.Circuits.Circuit.cost_program_simulate {σ : Signature} {τ : Signature} {n m : ℕ} (c : Circuit σ n m) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) (cost : τ.Op → ℕ) :
    (c.simulate impl).program.cost cost = c.program.cost fun (op : σ.Op) => (impl op).program.cost cost

    Gate replacement preserves arbitrary weighted costs exactly.

    source
    theorem Cslib.Circuits.Circuit.cost_program_pi {σ : Signature} {n m : ℕ} (cs : Fin m → Circuit σ n 1) (cost : σ.Op → ℕ) :
    (pi cs).program.cost cost = ∑ j : Fin m, (cs j).program.cost cost

    The cost of pi cs is the sum of the costs.