Layered arithmetic circuits and the GKR identity

A layered arithmetic circuit of fan-in two (Cslib.Interactive.GKR.LayeredCircuit) has its gates arranged in layers, with the gates of layer i labelled by the bit strings of length width i. Layer 0 is the input. Every gate of layer i + 1 is an addition or a multiplication of two gates of layer i, its left and right in-neighbours. Evaluating the layers in turn gives the gate values value x i on an input x (Cslib.Interactive.GKR.LayeredCircuit.value). We number the layers from the input, while Thaler, §4.6 numbers them from the output.

The wiring predicates add_i (a, b, c) and mult_i (a, b, c) of layer i + 1 are 1 exactly when gate a of layer i + 1 is an addition, respectively a multiplication, with in-neighbours b and c (addPred, multPred). The identity at the heart of the GKR protocol expresses the multilinear extension of the gate values of a layer through the multilinear extensions of the wiring predicates and the gate values of the layer below (Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_step) Thaler, Lemma 4.7, Goldwasser, Kalai, Rothblum: W̃_{i+1}(z) = ∑_{b, c} ãdd_i(z, b, c) (W_i(b) + W_i(c)) + m̃ult_i(z, b, c) W_i(b) W_i(c).

Main definitions

• Cslib.Interactive.GKR.LayeredCircuit: a layered arithmetic circuit of fan-in two.
• Cslib.Interactive.GKR.LayeredCircuit.step, Cslib.Interactive.GKR.LayeredCircuit.value: evaluation of one layer and of the circuit.
• Cslib.Interactive.GKR.LayeredCircuit.addPred, Cslib.Interactive.GKR.LayeredCircuit.multPred: the wiring predicates.

Main results

• Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_wiringPred: the closed form of the multilinear extensions of the wiring predicates (addPred and multPred are its two cases).
• Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_step: the GKR identity.

References

• S. Goldwasser, Y. T. Kalai, G. N. Rothblum, Delegating computation: interactive proofs for muggles
• J. Thaler, Proofs, Arguments, and Zero-Knowledge, Section 4.6

inductive Cslib.Interactive.GKR.Gate : Type

The two kinds of gates of an arithmetic circuit of fan-in two.

• add : Gate

  An addition gate.

• mul : Gate

  A multiplication gate.

@[instance_reducible]

instance Cslib.Interactive.GKR.instDecidableEqGate : DecidableEq Gate

structure Cslib.Interactive.GKR.LayeredCircuit : Type

A layered arithmetic circuit of fan-in two. The gates of layer i are labelled by bit strings of length width i; layer 0 is the input, and each gate of layer i + 1 combines two gates of layer i.

• depth : ℕ

  The number of layers above the input.

• width : ℕ → ℕ

  Layer i has 2 ^ width i gates.

• gate (i : ℕ) : (Fin (self.width (i + 1)) → Bool) → Gate

  The kind of each gate of layer i + 1.

• left (i : ℕ) : (Fin (self.width (i + 1)) → Bool) → Fin (self.width i) → Bool

  The left in-neighbour, in layer i, of each gate of layer i + 1.

• right (i : ℕ) : (Fin (self.width (i + 1)) → Bool) → Fin (self.width i) → Bool

  The right in-neighbour, in layer i, of each gate of layer i + 1.

def Cslib.Interactive.GKR.LayeredCircuit.step (C : LayeredCircuit) {R : Type u_1} [CommRing R] (i : ℕ) (W : (Fin (C.width i) → Bool) → R) (a : Fin (C.width (i + 1)) → Bool) : R

The values of layer i + 1, given the values W of layer i.

def Cslib.Interactive.GKR.LayeredCircuit.value (C : LayeredCircuit) {R : Type u_1} [CommRing R] (x : (Fin (C.width 0) → Bool) → R) (i : ℕ) : (Fin (C.width i) → Bool) → R

The gate values of layer i on the input x.

def Cslib.Interactive.GKR.LayeredCircuit.output (C : LayeredCircuit) {R : Type u_1} [CommRing R] (x : (Fin (C.width 0) → Bool) → R) : (Fin (C.width C.depth) → Bool) → R

The output values of the circuit.

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.WiringVar (C : LayeredCircuit) (i : ℕ) : Type

The variables of a wiring predicate of layer i + 1: a gate a of layer i + 1 and two gates b, c of layer i.

def Cslib.Interactive.GKR.LayeredCircuit.wiringPred (C : LayeredCircuit) {R : Type u_1} [CommRing R] (g : Gate) (i : ℕ) (v : C.WiringVar i → Bool) : R

The wiring predicate of a gate kind: 1 exactly when gate a of layer i + 1 has that kind and in-neighbours b and c.

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.addPred (C : LayeredCircuit) {R : Type u_1} [CommRing R] (i : ℕ) : (C.WiringVar i → Bool) → R

The addition predicate add_i.

@[reducible, inline]

abbrev Cslib.Interactive.GKR.LayeredCircuit.multPred (C : LayeredCircuit) {R : Type u_1} [CommRing R] (i : ℕ) : (C.WiringVar i → Bool) → R

The multiplication predicate mult_i.

theorem Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_wiringPred (C : LayeredCircuit) {R : Type u_1} [CommRing R] (g : Gate) (i : ℕ) (z : Fin (C.width (i + 1)) → R) (y w : Fin (C.width i) → R) : (MvPolynomial.eval (Sum.elim z (Sum.elim y w))) (BitString.multilinearExtension (C.wiringPred g i)) = ∑ a : Fin (C.width (i + 1)) → Bool, if C.gate i a = g then (MvPolynomial.eval z) (BitString.indicatorPoly a) * (MvPolynomial.eval y) (BitString.indicatorPoly (C.left i a)) * (MvPolynomial.eval w) (BitString.indicatorPoly (C.right i a)) else 0

The multilinear extension of a wiring predicate at (z, y, w) is the sum, over the gates a of that kind, of the product of the basis polynomials of a, its left and its right in-neighbour.

theorem Cslib.Interactive.GKR.LayeredCircuit.eval_multilinearExtension_step (C : LayeredCircuit) {R : Type u_1} [CommRing R] (i : ℕ) (W : (Fin (C.width i) → Bool) → R) (z : Fin (C.width (i + 1)) → R) : (MvPolynomial.eval z) (BitString.multilinearExtension (C.step i W)) = ∑ b : Fin (C.width i) → Bool, ∑ c : Fin (C.width i) → Bool, ((MvPolynomial.eval (Sum.elim z (Sum.elim (BitString.bitPoint b) (BitString.bitPoint c)))) (BitString.multilinearExtension (C.addPred i)) * (W b + W c) + (MvPolynomial.eval (Sum.elim z (Sum.elim (BitString.bitPoint b) (BitString.bitPoint c)))) (BitString.multilinearExtension (C.multPred i)) * (W b * W c))

The GKR identity Thaler, Lemma 4.7. The multilinear extension of the values of layer i + 1 is a sum over the pairs of gates b, c of layer i of the multilinear extensions of the wiring predicates times the sum, respectively the product, of the values of b and c.