Ledgers for gates of unbounded fan-in

The frontier method charges each gate for its fan-in, so it cannot afford gates of unbounded fan-in. A few of them can nevertheless be absorbed, when they aggregate: when their outputs are determined by a product, in a commutative monoid, of contributions of the wires.

Mark a set of gates as special. A ledger for them in a commutative monoid M (Frontier.Ledger) assigns to each wire and each of its values a contribution in M, and reads off the value of every special gate from the product of the contributions of all wires. The defining identity holds for every assignment of values to the wires, not only for runs of the circuit. For example, k gates computing AND, OR, parity, or counts modulo m of their arguments have a ledger in a product of k small monoids.

Guess and check. Replace each special gate by a constant placeholder (Frontier.erase): the result has fan-in bounded by that of the other gates. To run it, guess the final product m ∈ M and let each placeholder read its value from m (Frontier.Ledger.run). The guess is consistent when the run reproduces it: when the product of the contributions of the run is m.

• A consistent guess yields the true run (Frontier.Ledger.run_eq_trace): the placeholders hold the values that the special gates would compute from the run.
• The product of the contributions of the true run is a consistent guess (Frontier.Ledger.run_total_trace).

So a circuit with special gates is an ordinary circuit, of bounded fan-in, together with one global register in M: the guess, checked against an accumulated product. A sweep carries the guess and the product accumulated so far in its messages, at a cost of 2 log |M|.

Main definitions

• Frontier.guessSignature σ: the signature σ with a placeholder constant for every natural.
• Frontier.erase special p: the program p with its special gates replaced by placeholders.
• Frontier.Ledger p I special M: a ledger for the special gates of p in M.

Main results

• Frontier.Ledger.run_eq_trace, Frontier.Ledger.run_total_trace: guess and check.

@[reducible, inline]

abbrev Complexity.Frontier.guessSignature (σ : Cslib.Circuits.Signature) : Cslib.Circuits.Signature

The signature σ with a placeholder constant for every natural number.

Equations

• Complexity.Frontier.guessSignature σ = { Op := σ.Op ⊕ ℕ, Arity := Sum.elim σ.Arity fun (x : ℕ) => 0 }

def Complexity.Frontier.guessInterpretation {σ : Cslib.Circuits.Signature} {U : Type u_1} (I : Cslib.Circuits.Interpretation σ U) (γ : ℕ → U) : Cslib.Circuits.Interpretation (guessSignature σ) U

The interpretation I, with the placeholder k holding the value γ k.

Equations

• Complexity.Frontier.guessInterpretation I γ (Sum.inl o) x_2 = I o x_2
• Complexity.Frontier.guessInterpretation I γ (Sum.inr k) x_2 = γ k

def Complexity.Frontier.placeholderLine {σ : Cslib.Circuits.Signature} (g : ℕ) {n s : ℕ} : Cslib.Circuits.Line (guessSignature σ) n s

The line of the placeholder for gate g.

Equations

• Complexity.Frontier.placeholderLine g = { op := Sum.inr g, wires := Fin.elim0 }

def Complexity.Frontier.liftLine {σ : Cslib.Circuits.Signature} {n s : ℕ} (line : Cslib.Circuits.Line σ n s) : Cslib.Circuits.Line (guessSignature σ) n s

An ordinary line, over the signature with placeholders.

Equations

• Complexity.Frontier.liftLine line = { op := Sum.inl line.op, wires := line.wires }

noncomputable def Complexity.Frontier.erase {σ : Cslib.Circuits.Signature} {n : ℕ} (special : ℕ → Prop) {s : ℕ} : Cslib.Circuits.Program σ n s → Cslib.Circuits.Program (guessSignature σ) n s

Erasing the special gates. The gate numbered g becomes the placeholder g when special g, and is unchanged otherwise.

Equations

• Complexity.Frontier.erase special Cslib.Circuits.Program.empty = Cslib.Circuits.Program.empty
• Complexity.Frontier.erase special (p.gate line) = (Complexity.Frontier.erase special p).gate (if special s then Complexity.Frontier.placeholderLine s else Complexity.Frontier.liftLine line)

theorem Complexity.Frontier.erase_gate {σ : Cslib.Circuits.Signature} {n s : ℕ} (special : ℕ → Prop) (p : Cslib.Circuits.Program σ n s) (line : Cslib.Circuits.Line σ n s) : erase special (p.gate line) = (erase special p).gate (if special s then placeholderLine s else liftLine line)

theorem Complexity.Frontier.placeholderLine_mapWires {σ : Cslib.Circuits.Signature} {n s n' s' : ℕ} (g : ℕ) (f : Cslib.Circuits.Wire n s → Cslib.Circuits.Wire n' s') : (placeholderLine g).mapWires f = placeholderLine g

theorem Complexity.Frontier.liftLine_mapWires {σ : Cslib.Circuits.Signature} {n s n' s' : ℕ} (line : Cslib.Circuits.Line σ n s) (f : Cslib.Circuits.Wire n s → Cslib.Circuits.Wire n' s') : (liftLine line).mapWires f = liftLine (line.mapWires f)

theorem Complexity.Frontier.lines_erase {σ : Cslib.Circuits.Signature} {n s : ℕ} (special : ℕ → Prop) (p : Cslib.Circuits.Program σ n s) (g : Fin s) : (erase special p).lines g = if special ↑g then placeholderLine ↑g else liftLine (p.lines g)

The lines of an erased program.

theorem Complexity.Frontier.lines_erase_of_special {σ : Cslib.Circuits.Signature} {n s : ℕ} {special : ℕ → Prop} (p : Cslib.Circuits.Program σ n s) {g : Fin s} (hg : special ↑g) : (erase special p).lines g = placeholderLine ↑g

theorem Complexity.Frontier.lines_erase_of_not_special {σ : Cslib.Circuits.Signature} {n s : ℕ} {special : ℕ → Prop} (p : Cslib.Circuits.Program σ n s) {g : Fin s} (hg : ¬special ↑g) : (erase special p).lines g = liftLine (p.lines g)

theorem Complexity.Frontier.fanInAtMost_erase {σ : Cslib.Circuits.Signature} {n s : ℕ} (special : ℕ → Prop) (p : Cslib.Circuits.Program σ n s) {r : ℕ} (h : ∀ (g : Fin s), ¬special ↑g → σ.Arity (p.lines g).op ≤ r) : (erase special p).FanInAtMost r

Erasing the special gates leaves the fan-in of the others.

structure Complexity.Frontier.Ledger {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} (p : Cslib.Circuits.Program σ n s) (I : Cslib.Circuits.Interpretation σ U) (special : ℕ → Prop) (M : Type u_2) [CommMonoid M] : Type (max u_1 u_2)

A ledger for the special gates of a program, in a commutative monoid M: a contribution of each wire for each of its values, and a readout of the value of each special gate from the product of all contributions. The identity holds for every assignment of values to the wires.

• contribution : Cslib.Circuits.Wire n s → U → M

  The contribution of a wire carrying a value.

• readout : M → ℕ → U

  The value of each special gate, read off the product of the contributions.

• readout_prod (v : Cslib.Circuits.Wire n s → U) (g : Fin s) : special ↑g → self.readout (∏ w : Cslib.Circuits.Wire n s, self.contribution w (v w)) ↑g = I (p.lines g).op fun (a : Fin (σ.Arity (p.lines g).op)) => v ((p.lines g).wires a)

  The readout of a special gate is the gate applied to the values of its arguments.

def Complexity.Frontier.Ledger.total {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) (v : Cslib.Circuits.Wire n s → U) : M

The product of the contributions of an assignment of values to the wires.

Equations

• L.total v = ∏ w : Cslib.Circuits.Wire n s, L.contribution w (v w)

noncomputable def Complexity.Frontier.Ledger.run {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) (m : M) (x : Fin n → U) : Cslib.Circuits.Wire n s → U

The run of the erased program, with the placeholders reading their values from the guess m.

Equations

• L.run m x = (Complexity.Frontier.erase special p).trace (Complexity.Frontier.guessInterpretation I (L.readout m)) x

theorem Complexity.Frontier.Ledger.run_gate_of_special {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) (m : M) (x : Fin n → U) {g : Fin s} (hg : special ↑g) : L.run m x (Cslib.Circuits.Wire.gate g) = L.readout m ↑g

The value of a special gate in the run with guess m is its readout.

theorem Complexity.Frontier.Ledger.run_gate_of_not_special {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) (m : M) (x : Fin n → U) {g : Fin s} (hg : ¬special ↑g) : L.run m x (Cslib.Circuits.Wire.gate g) = I (p.lines g).op fun (a : Fin (σ.Arity (p.lines g).op)) => L.run m x ((p.lines g).wires a)

The value of an ordinary gate in the run with guess m is the gate applied to its arguments.

theorem Complexity.Frontier.Ledger.run_eq_trace {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) {m : M} {x : Fin n → U} (h : L.total (L.run m x) = m) : L.run m x = p.trace I x

Guess and check, soundness. If the run with guess m reproduces m, it is the true run.

theorem Complexity.Frontier.Ledger.run_total_trace {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) (x : Fin n → U) : L.run (L.total (p.trace I x)) x = p.trace I x

Guess and check, completeness. The product of the contributions of the true run is a guess whose run is the true run.

theorem Complexity.Frontier.Ledger.total_run_eq_iff {σ : Cslib.Circuits.Signature} {n s : ℕ} {U : Type u_1} {p : Cslib.Circuits.Program σ n s} {I : Cslib.Circuits.Interpretation σ U} {special : ℕ → Prop} {M : Type u_2} [CommMonoid M] (L : Ledger p I special M) (m : M) (x : Fin n → U) : L.total (L.run m x) = m ↔ m = L.total (p.trace I x)

A guessed ledger is consistent exactly when it is the ledger of the unique true run. This is the uniqueness needed when summing counts over ledger guesses.