Aggregate gates

An operation of arity k aggregates in a commutative monoid T when its value is read off a product of contributions of its arguments: f x = ψ (∏ i, φ i (x i)). Unbounded AND, OR, and parity aggregate in a monoid with two elements, and counting modulo m aggregates in ZMod m.

If every special gate of a program aggregates in T, the special gates have a ledger in the monoid T ^ k of functions from the k special gates to T (Frontier.exists_ledger_of_aggregates): the contribution of a wire to a special gate is the product of its contributions to the slots of that gate that read it. So k aggregate gates cost k log |T| in the frontier lower bound.

Main definitions

• Frontier.Aggregates f T: the operation f aggregates in T.

Main results

• Frontier.exists_ledger_of_aggregates: aggregate gates have a ledger.
• Frontier.aggregates_and, aggregates_or, aggregates_xor, aggregates_countMod: examples.

def Complexity.Frontier.Aggregates {U : Type u_1} {k : ℕ} (f : (Fin k → U) → U) (T : Type) [CommMonoid T] : Prop

An operation of arity k aggregates in a commutative monoid T when its value is read off a product of contributions of its arguments.

Equations

• Complexity.Frontier.Aggregates f T = ∃ (φ : Fin k → U → T) (ψ : T → U), ∀ (x : Fin k → U), f x = ψ (∏ i : Fin k, φ i (x i))

theorem Complexity.Frontier.exists_ledger_of_aggregates {U : Type u_1} [Nonempty U] {σ : Cslib.Circuits.Signature} {n s : ℕ} (p : Cslib.Circuits.Program σ n s) (I : Cslib.Circuits.Interpretation σ U) (special : ℕ → Prop) (T : Type) [CommMonoid T] (h : ∀ (g : Fin s), special ↑g → Aggregates (I (p.lines g).op) T) : Nonempty (Ledger p I special ({ g : Fin s // special ↑g } → T))

Aggregate gates have a ledger. If every special gate of a program aggregates in T, the special gates have a ledger in the monoid of functions from the special gates to T.

theorem Complexity.Frontier.aggregates_and (k : ℕ) : Aggregates (fun (x : Fin k → Bool) => decide (∀ (i : Fin k), x i = true)) (ZMod 2)

Unbounded AND aggregates in ZMod 2 under multiplication.

theorem Complexity.Frontier.aggregates_or (k : ℕ) : Aggregates (fun (x : Fin k → Bool) => decide (∃ (i : Fin k), x i = true)) (ZMod 2)

Unbounded OR aggregates in ZMod 2 under multiplication.

theorem Complexity.Frontier.aggregates_xor (k : ℕ) : Aggregates (fun (x : Fin k → Bool) => decide ((∑ i : Fin k, if x i = true then 1 else 0) = 1)) (Multiplicative (ZMod 2))

Unbounded parity aggregates in ZMod 2 under addition.

theorem Complexity.Frontier.aggregates_countMod (k m : ℕ) (R : Set (ZMod m)) [DecidablePred fun (x : ZMod m) => x ∈ R] : Aggregates (fun (x : Fin k → Bool) => decide ((∑ i : Fin k, if x i = true then 1 else 0) ∈ R)) (Multiplicative (ZMod m))

Unbounded counting modulo m aggregates in ZMod m under addition: here the gate tests whether the number of true arguments lies in a set R of residues.