Fusion covers of circuit gates

A family of predicates on semantic values supplies candidate invariants. If every input satisfies an invariant and some output violates it, some evaluated gate fails to preserve it. Thus the semantic gate configurations form a static cover of all candidate invariants. The cover has exactly the program's weighted cost, including unused gates and nullary operations; sharing and repeated outputs incur no additional cost.

This algebra-generic obstruction requires neither a Boolean structure nor an order on values. The reference-to-observation implication used in Fusion models is one possible predicate. Program.trace_induction supplies the direct preservation argument, without selecting a failing atom. Extracting a failing atom from a cover may use classical logic.

Main definitions

• Cslib.Circuits.Fusion.Atom: an operation with its semantic arguments.
• Cslib.Circuits.Fusion.Cover: a finite family defeating every candidate invariant.
• Cslib.Circuits.Fusion.coverComplexity: minimum weighted cover cost, or infinity.

Main results

• Cslib.Circuits.Fusion.programAtoms_isCover: the gates cover failed invariants.
• Cslib.Circuits.Fusion.Cover.cost_ofProgram: extraction preserves arbitrary operation costs.
• Cslib.Circuits.Fusion.coverComplexity_le_ecomplexityFrom: transfer to native source complexity.

References

• Adapted from LowerBound/Fusion/Framework.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

structure Cslib.Circuits.Fusion.Atom (σ : Signature) (U : Type v) : Type (max u v)

One semantic gate configuration, without any constraint on where its arguments came from.

• op : σ.Op

  The operation at the gate.

• arguments : Fin (σ.Arity self.op) → U

  The value supplied to each argument.

def Cslib.Circuits.Fusion.Atom.Preserves {σ : Signature} {U : Type v} (a : Atom σ U) (I : Interpretation σ U) (P : U → Prop) : Prop

An atom preserves a predicate if it holds on the result whenever it holds on all arguments.

def Cslib.Circuits.Fusion.IsCover {σ : Signature} {U : Type v} {W : Type w} (I : Interpretation σ U) (P : W → U → Prop) {k : ℕ} (atoms : Fin k → Atom σ U) : Prop

No candidate invariant is preserved by every atom in a cover.

structure Cslib.Circuits.Fusion.Cover {σ : Signature} {U : Type v} {W : Type w} (I : Interpretation σ U) (P : W → U → Prop) : Type (max u v)

A finite fusion cover. Repeated atoms are allowed and charged separately.

• size : ℕ

  Number of atoms, including repetitions.

• atoms : Fin self.size → Atom σ U

  Semantic gate configurations in the cover.

• isCover : IsCover I P self.atoms

  Every candidate invariant fails at some atom.

def Cslib.Circuits.Fusion.Cover.cost {σ : Signature} {U : Type v} {W : Type w} {I : Interpretation σ U} {P : W → U → Prop} (c : Cover I P) (weight : σ.Op → ℕ) : ℕ

Total operation weight of a cover.

noncomputable def Cslib.Circuits.Fusion.coverComplexity {σ : Signature} {U : Type v} {W : Type w} (I : Interpretation σ U) (P : W → U → Prop) (weight : σ.Op → ℕ) : ℕ∞

The least weighted cost of any finite cover; infinity if there is no cover.

theorem Cslib.Circuits.Fusion.coverComplexity_le {σ : Signature} {U : Type v} {W : Type w} {I : Interpretation σ U} {P : W → U → Prop} (c : Cover I P) (weight : σ.Op → ℕ) : coverComplexity I P weight ≤ ↑(c.cost weight)

Every cover bounds the minimum cover cost from above.

theorem Cslib.Circuits.Fusion.le_coverComplexity_iff {σ : Signature} {U : Type v} {W : Type w} {I : Interpretation σ U} {P : W → U → Prop} {weight : σ.Op → ℕ} {k : ℕ∞} : k ≤ coverComplexity I P weight ↔ ∀ (c : Cover I P), k ≤ ↑(c.cost weight)

A lower bound on minimum cover complexity is exactly a bound for every finite cover.

def Cslib.Circuits.Fusion.programAtoms {σ : Signature} {U : Type v} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (input : Fin n → U) (k : Fin g) : Atom σ U

Semantic atoms of a native program, indexed by its gates in program order.

theorem Cslib.Circuits.Fusion.programAtoms_gate {σ : Signature} {U : Type v} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) (I : Interpretation σ U) (input : Fin n → U) : programAtoms (p.gate line) I input = Fin.snoc (programAtoms p I input) { op := line.op, arguments := p.trace I input ∘ line.wires }

Adding a gate appends its evaluated atom, preserving every earlier atom.

theorem Cslib.Circuits.Fusion.programAtoms_isCover {σ : Signature} {U : Type v} {W : Type w} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (P : W → U → Prop) (input : Fin n → U) (hin : ∀ (t : W) (i : Fin n), P t (input i)) (hfail : ∀ (t : W), ∃ (w : Wire n g), ¬P t (p.trace I input w)) : IsCover I P (programAtoms p I input)

Gates cover every invariant that holds on the inputs and fails on some wire.

def Cslib.Circuits.Fusion.Cover.ofProgram {σ : Signature} {U : Type v} {W : Type w} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (P : W → U → Prop) (input : Fin n → U) (hin : ∀ (t : W) (i : Fin n), P t (input i)) (hfail : ∀ (t : W), ∃ (w : Wire n g), ¬P t (p.trace I input w)) : Cover I P

Extract all gates as a cover; no failing atom needs to be selected.

@[simp]

theorem Cslib.Circuits.Fusion.Cover.cost_ofProgram {σ : Signature} {U : Type v} {W : Type w} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (P : W → U → Prop) (input : Fin n → U) (hin : ∀ (t : W) (i : Fin n), P t (input i)) (hfail : ∀ (t : W), ∃ (w : Wire n g), ¬P t (p.trace I input w)) (weight : σ.Op → ℕ) : (ofProgram p I P input hin hfail).cost weight = p.cost weight

Extracting a program's cover preserves its exact weighted cost.

theorem Cslib.Circuits.Fusion.coverComplexity_le_program_cost {σ : Signature} {U : Type v} {W : Type w} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (P : W → U → Prop) (input : Fin n → U) (hin : ∀ (t : W) (i : Fin n), P t (input i)) (hfail : ∀ (t : W), ∃ (w : Wire n g), ¬P t (p.trace I input w)) (weight : σ.Op → ℕ) : coverComplexity I P weight ≤ ↑(p.cost weight)

Every program violating all candidate invariants pays at least the minimum cover cost.

theorem Cslib.Circuits.Fusion.coverComplexity_le_circuit_cost {σ : Signature} {U : Type v} {W : Type w} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (P : W → U → Prop) (input : Fin n → U) (hin : ∀ (t : W) (i : Fin n), P t (input i)) (hfail : ∀ (t : W), ∃ (o : Fin m), ¬P t (c.eval I input o)) (weight : σ.Op → ℕ) : coverComplexity I P weight ≤ ↑(c.program.cost weight)

Failure on any designated output suffices. Different witnesses may use different outputs.

theorem Cslib.Circuits.Fusion.coverComplexity_le_ecomplexityFrom {σ : Signature} {U : Type v} {W : Type w} {n m : ℕ} {X : Type z} (I : Interpretation σ U) (P : W → U → Prop) (weight : σ.Op → ℕ) (target : X → Fin m → U) (sources : X → Fin n → U) (x : X) (hin : ∀ (t : W) (i : Fin n), P t (sources x i)) (hfail : ∀ (t : W), ∃ (o : Fin m), ¬P t (target x o)) : coverComplexity I P weight ≤ ecomplexityFrom I weight target sources

A single source assignment separating inputs from target outputs bounds source complexity. The common source domain remains arbitrary; its chosen assignment must actually exist.