Circuit simulation with shared context

An operation gadget can read a shared block of ambient inputs as well as its ordinary arguments. This permits a nullary dictionary term to depend on ambient variables, as in Waring decompositions. All gadgets read the same input block; no context gates are added.

Compilation first adds context arguments to each line, then uses Program.simulate through Circuit.simulate. Thus the existing wire-renaming and gate-replacement machinery handles sharing and output wiring. Costs count every gadget gate, including gates unused by outputs.

Main definitions

• Cslib.Circuits.Signature.withContext: prepend ambient inputs to every operation's arguments.
• Cslib.Circuits.Circuit.withContext: pass the same ambient inputs to every gate.
• Cslib.Circuits.Circuit.simulateWithContext: replace each operation by a contextual gadget.

Main results

• Cslib.Circuits.Circuit.eval_simulateWithContext: exact semantics for every output.
• Cslib.Circuits.Circuit.cost_program_simulateWithContext: exact arbitrary weighted cost.

References

• Ported from Translation/Contextual.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib, using native circuit simulation.

@[reducible, inline]

abbrev Cslib.Circuits.Signature.withContext (σ : Signature) (q : ℕ) : Signature

Add a q-input context before each operation's ordinary arguments.

def Cslib.Circuits.Line.withContext {σ : Signature} {n g : ℕ} (q : ℕ) (line : Line σ (q + n) g) : Line (σ.withContext q) (q + n) g

Prepend references to the ambient input block to a line's arguments.

def Cslib.Circuits.Circuit.withContext {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) : Circuit (σ.withContext q) (q + n) m

Every gate receives the shared context, followed by its original arguments.

theorem Cslib.Circuits.Circuit.cost_program_withContext {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (cost : σ.Op → ℕ) : (c.withContext q).program.cost cost = c.program.cost cost

Adding context does not add gates or change their costs.

@[simp]

theorem Cslib.Circuits.Circuit.size_withContext {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) : (c.withContext q).size = c.size

Adding context keeps the number of gates.

theorem Cslib.Circuits.Circuit.eval_withContext {σ : Signature} {U : Type u} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (J : Interpretation (σ.withContext q) U) (context : Fin q → U) (x : Fin n → U) : (c.withContext q).eval J (Fin.append context x) = c.eval (fun (op : σ.Op) (args : Fin (σ.Arity op) → U) => J op (Fin.append context args)) x

Evaluating a context-bearing circuit fixes the same context in every operation.

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

Replace every gate by a gadget receiving shared ambient inputs and its local arguments.

theorem Cslib.Circuits.Circuit.eval_simulateWithContext {σ : Signature} {τ : Signature} {U : Type u} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (impl : (op : σ.Op) → Circuit τ (q + σ.Arity op) 1) (J : Interpretation τ U) (context : Fin q → U) (x : Fin n → U) : (c.simulateWithContext q impl).eval J (Fin.append context x) = c.eval (fun (op : σ.Op) (args : Fin (σ.Arity op) → U) => (impl op).eval J (Fin.append context args) 0) x

Contextual simulation computes every output with the supplied gadget semantics.

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

Contextual simulation charges exactly the weighted cost of each operation gadget.

@[simp]

theorem Cslib.Circuits.Circuit.size_simulateWithContext {σ : Signature} {τ : Signature} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (impl : (op : σ.Op) → Circuit τ (q + σ.Arity op) 1) : (c.simulateWithContext q impl).size = c.program.cost fun (op : σ.Op) => (impl op).size

The compiled gate count is exactly the sum of the gadget sizes.

theorem Cslib.Circuits.Circuit.size_simulateWithContext_le {σ : Signature} {τ : Signature} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (impl : (op : σ.Op) → Circuit τ (q + σ.Arity op) 1) {b : ℕ} (h : ∀ (op : σ.Op), (impl op).size ≤ b) : (c.simulateWithContext q impl).size ≤ b * c.size

A uniform gadget-size bound gives a uniform factor on circuit size.