Local Fusion properties with shared context #
Every gate of Circuit.withContext receives the same supplied context. Therefore a local
property of contextual gadgets transfers to every atom of the compiled circuit, with gadget
assumptions needed only at this fixed context. The rest of each gadget's arguments may be
arbitrary. Compilation and cost accounting remain those of native contextual simulation.
Main results #
Cslib.Circuits.Fusion.forall_programAtoms_withContext: all source atoms receive the context.Cslib.Circuits.Fusion.forall_programAtoms_simulateWithContext: transfer gadget properties to the compiled circuit at a fixed context.
References #
- Adapted from LowerBound/Fusion/Contextual.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
theorem Cslib.Circuits.Fusion.forall_programAtoms_withContext {σ : Signature} {U : Type w} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (I : Interpretation (σ.withContext q) U) (context : Fin q → U) (input : Fin n → U) (P : Atom (σ.withContext q) U → Prop) (h : ∀ (op : (σ.withContext q).Op) (args : Fin (σ.Arity op) → U), P { op := op, arguments := Fin.append context args }) (k : Fin (c.withContext q).size) :
P (programAtoms (c.withContext q).program I (Fin.append context input) k)
Every atom of a context-bearing circuit receives the same context prefix.
theorem Cslib.Circuits.Fusion.forall_programAtoms_simulateWithContext {σ : Signature} {τ : Signature} {U : Type w} {n m : ℕ} (c : Circuit σ n m) (q : ℕ) (impl : (op : σ.Op) → Circuit τ (q + σ.Arity op) 1) (J : Interpretation τ U) (context : Fin q → U) (input : Fin n → U) (P : Atom τ U → Prop) (hlocal :
∀ (op : σ.Op) (args : Fin (σ.Arity op) → U) (j : Fin (impl op).size),
P (programAtoms (impl op).program J (Fin.append context args) j)) (j : Fin (c.simulateWithContext q impl).size) :
P (programAtoms (c.simulateWithContext q impl).program J (Fin.append context input) j)
A property of every gadget atom at the supplied context holds throughout compilation. No assumption is made about the same gadget at a different context.