The GKR summand

For a point z of layer i + 1, the GKR protocol runs sumcheck on the polynomial f_z (y, w) = ãdd_i(z, y, w) (W̃_i(y) + W̃_i(w)) + m̃ult_i(z, y, w) W̃_i(y) W̃_i(w) in the 2 · width i variables (y, w) (Cslib.Interactive.GKR.LayeredCircuit.summand). Its sum over the cube is W̃_{i+1}(z) (sum_eval_summand, from the GKR identity), its value at any point is computed from the wiring extensions and the two values W̃_i(y) and W̃_i(w) (eval_summand), and each variable has degree at most two (degreeOf_summand_le), so each sumcheck round has soundness error 2 / |F| Thaler, §4.6.

Main definitions

• Cslib.Interactive.GKR.LayeredCircuit.summand: the polynomial f_z.

Main results

• Cslib.Interactive.GKR.LayeredCircuit.eval_summand: the value of f_z at (y, w).
• Cslib.Interactive.GKR.LayeredCircuit.sum_eval_summand: the sum of f_z over the cube.
• Cslib.Interactive.GKR.LayeredCircuit.degreeOf_summand_le: every variable has degree at most two.

References

• J. Thaler, Proofs, Arguments, and Zero-Knowledge, Section 4.6

noncomputable def Cslib.Interactive.GKR.indicatorAt {R : Type u_1} [CommRing R] {k n : ℕ} (e : Fin k → Fin n) (a : Fin k → Bool) : MvPolynomial (Fin n) R

The indicator polynomial of the bit string a, in the variables e j.

theorem Cslib.Interactive.GKR.eval_indicatorAt {R : Type u_1} [CommRing R] {k n : ℕ} (e : Fin k → Fin n) (a : Fin k → Bool) (v : Fin n → R) : (MvPolynomial.eval v) (indicatorAt e a) = (MvPolynomial.eval (v ∘ e)) (BitString.indicatorPoly a)

theorem Cslib.Interactive.GKR.degreeOf_indicatorAt_le {R : Type u_1} [CommRing R] {k n : ℕ} [Nontrivial R] (e : Fin k → Fin n) (a : Fin k → Bool) (v : Fin n) : MvPolynomial.degreeOf v (indicatorAt e a) ≤ ∑ j : Fin k, if e j = v then 1 else 0

The degree of a variable v in an indicator polynomial is at most the number of j with e j = v.

theorem Cslib.Interactive.GKR.sum_castAdd_add_sum_natAdd {k : ℕ} (v : Fin (k + k)) : ((∑ j : Fin k, if Fin.castAdd k j = v then 1 else 0) + ∑ j : Fin k, if Fin.natAdd k j = v then 1 else 0) = 1

Every variable of Fin (k + k) lies in exactly one of the two halves.

def Cslib.Interactive.GKR.splitEquiv (k : ℕ) : (Fin (k + k) → Bool) ≃ (Fin k → Bool) × (Fin k → Bool)

A bit string of length k + k is a pair of bit strings of length k.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.wiringPoly (C : LayeredCircuit) {R : Type u_1} [CommRing R] (g : Gate) (i : ℕ) (z : Fin (C.width (i + 1)) → R) : MvPolynomial (Fin (C.width i + C.width i)) R

The wiring extension of the gate kind g, as a polynomial in the in-neighbour variables, with the gate of layer i + 1 fixed to the point z.

noncomputable def Cslib.Interactive.GKR.LayeredCircuit.valuePoly {R : Type u_1} [CommRing R] {k n : ℕ} (e : Fin k → Fin n) (W : (Fin k → Bool) → R) : MvPolynomial (Fin n) R

The multilinear extension of the values W of layer i, in the variables e j.

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

The GKR summand f_z (y, w) = ãdd_i(z, y, w) (W̃(y) + W̃(w)) + m̃ult_i(z, y, w) W̃(y) W̃(w), for the values W of layer i and a point z of layer i + 1.

theorem Cslib.Interactive.GKR.LayeredCircuit.eval_valuePoly_castAdd {R : Type u_1} [CommRing R] {k : ℕ} (W : (Fin k → Bool) → R) (y w : Fin k → R) : (MvPolynomial.eval (Fin.append y w)) (valuePoly (Fin.castAdd k) W) = (MvPolynomial.eval y) (BitString.multilinearExtension W)

theorem Cslib.Interactive.GKR.LayeredCircuit.eval_valuePoly_natAdd {R : Type u_1} [CommRing R] {k : ℕ} (W : (Fin k → Bool) → R) (y w : Fin k → R) : (MvPolynomial.eval (Fin.append y w)) (valuePoly (Fin.natAdd k) W) = (MvPolynomial.eval w) (BitString.multilinearExtension W)

theorem Cslib.Interactive.GKR.LayeredCircuit.eval_wiringPoly (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 (Fin.append y w)) (C.wiringPoly g i z) = (MvPolynomial.eval (Sum.elim z (Sum.elim y w))) (BitString.multilinearExtension (C.wiringPred g i))

The wiring polynomial at (y, w) is the multilinear extension of the wiring predicate at (z, y, w).

theorem Cslib.Interactive.GKR.LayeredCircuit.eval_summand (C : LayeredCircuit) {R : Type u_1} [CommRing R] (i : ℕ) (W : (Fin (C.width i) → Bool) → R) (z : Fin (C.width (i + 1)) → R) (y w : Fin (C.width i) → R) : (MvPolynomial.eval (Fin.append y w)) (C.summand i W z) = (MvPolynomial.eval (Sum.elim z (Sum.elim y w))) (BitString.multilinearExtension (C.addPred i)) * ((MvPolynomial.eval y) (BitString.multilinearExtension W) + (MvPolynomial.eval w) (BitString.multilinearExtension W)) + (MvPolynomial.eval (Sum.elim z (Sum.elim y w))) (BitString.multilinearExtension (C.multPred i)) * ((MvPolynomial.eval y) (BitString.multilinearExtension W) * (MvPolynomial.eval w) (BitString.multilinearExtension W))

The value of the GKR summand at (y, w), from the wiring extensions and the values of the multilinear extension of layer i at y and w.

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

The sum of the GKR summand over the cube is the multilinear extension of layer i + 1 at z.

theorem Cslib.Interactive.GKR.LayeredCircuit.degreeOf_valuePoly_le {R : Type u_1} [CommRing R] [Nontrivial R] {k n : ℕ} (e : Fin k → Fin n) (W : (Fin k → Bool) → R) (v : Fin n) : MvPolynomial.degreeOf v (valuePoly e W) ≤ ∑ j : Fin k, if e j = v then 1 else 0

theorem Cslib.Interactive.GKR.LayeredCircuit.degreeOf_wiringPoly_le (C : LayeredCircuit) {R : Type u_1} [CommRing R] [Nontrivial R] (g : Gate) (i : ℕ) (z : Fin (C.width (i + 1)) → R) (v : Fin (C.width i + C.width i)) : MvPolynomial.degreeOf v (C.wiringPoly g i z) ≤ 1

theorem Cslib.Interactive.GKR.LayeredCircuit.degreeOf_summand_le (C : LayeredCircuit) {R : Type u_1} [CommRing R] [Nontrivial R] (i : ℕ) (W : (Fin (C.width i) → Bool) → R) (z : Fin (C.width (i + 1)) → R) (v : Fin (C.width i + C.width i)) : MvPolynomial.degreeOf v (C.summand i W z) ≤ 2

Every variable of the GKR summand has degree at most two.