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 program. 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 (Frontier.Ledger.ofAggregates).

Guess and check. Replace each special gate by a constant (Cslib.Circuits.Program.eraseGates): the result has fan-in bounded by that of the other gates. To run it, guess the final product m ∈ M and let each constant 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 constants hold the values that the special gates compute from the run.
• The product of the contributions of the true run is a consistent guess (Frontier.Ledger.run_total_trace).

So a program with special gates is an ordinary program, 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

• Cslib.Circuits.Frontier.Ledger special p I M: a ledger for the special gates of p in M.
• Cslib.Circuits.Frontier.Ledger.total, Cslib.Circuits.Frontier.Ledger.totalOn: the product of the contributions of all wires, and of the wires of a set.
• Cslib.Circuits.Frontier.Ledger.run: the run of the erased program on a guess.

Main results

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

structure Cslib.Circuits.Frontier.Ledger {σ : Signature} {n s : ℕ} {U : Type u_1} (special : Fin s → Prop) (p : Program σ n s) (I : Interpretation σ U) (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 : Wire n s → U → M

  The contribution of a wire carrying a value.

• readout : M → { g : Fin s // special g } → U

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

• readout_prod (v : Wire n s → U) (g : { g : Fin s // special g }) : self.readout (∏ w : 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 Cslib.Circuits.Frontier.Ledger.total {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (v : Wire n s → U) : M

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

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

The product of the contributions of the wires in Q.

theorem Cslib.Circuits.Frontier.Ledger.total_eq_mul {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) (Q : Set (Wire n s)) (v : Wire n s → U) : L.total v = L.totalOn Q v * L.totalOn Qᶜ v

The total is the product on Q times the product on its complement.

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

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

@[simp]

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

theorem Cslib.Circuits.Frontier.Ledger.run_gate {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) [DecidablePred special] (m : M) (x : Fin n → U) (g : Fin s) : L.run m x (Wire.gate g) = if h : special g then L.readout m ⟨g, h⟩ else 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 a gate in the run with guess m: the readout for a special gate, and the gate applied to the values of its arguments otherwise.

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

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

theorem Cslib.Circuits.Frontier.Ledger.run_gate_of_not_special {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) [DecidablePred special] (m : M) (x : Fin n → U) {g : Fin s} (hg : ¬special g) : L.run m x (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 Cslib.Circuits.Frontier.Ledger.run_eq_trace {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) [DecidablePred special] {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 Cslib.Circuits.Frontier.Ledger.run_total_trace {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) [DecidablePred special] (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 Cslib.Circuits.Frontier.Ledger.total_run_eq_iff {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} {p : Program σ n s} {I : Interpretation σ U} {M : Type u_2} [CommMonoid M] (L : Ledger special p I M) [DecidablePred special] (m : M) (x : Fin n → U) : L.total (L.run m x) = m ↔ m = L.total (p.trace I x)

The consistent guess is unique. A guess reproduces itself exactly when it is the product of the contributions of the true run.