Land of Sumcheck

Prerequisite:

• multilinear polynomials
• low degree extension

Multilinear extensions

A multivariate polynomial $g$ is multilinear if the degree of the polynomial in each variable is at most one.

let $f:{\left\{0,1\right\}}^v\to \mathbb{F}$ be any function mapping the v-dimensional hypercube to $\mathbb{F}$, then multilinear extension of $f$ is $g$, a $v$-variate polynomial that agrees with $f$ on all $x\in {\left\{0,1\right\}}^v$.

Why multilinear extensions?

Allows to represent domain of length 2^v into v variable multilinear polynomial, which is way less than univariate polynomials where $v-1$ variable polynomial is needed to represent length $v$ domain.

Using SZ lemma, verifier gains power over prover as if two functions $f,f^{\prime }$ differ at even one point in ${\left\{0,1\right\}}^v$, then their extension $g,g^{\prime }$ disagree almost everywhere, precisely agree at most $\frac{d}{\mid \mathbb{F}\mid }$.

Prove that a function $f:{\left\{0,1\right\}}^v\to \mathbb{F}$ has a unique multilinear extension $\tilde{f}$ over $\mathbb{F}$. a

Lagrange interpolation

$$\begin{array}{c}\tilde{f}(x_1,x_2,\dots ,x_v)=\sum _{w\in {\left\{0,1\right\}}^v}f(w)\cdot \widetilde{eq}(x_1,\dots ,x_v)\end{array}$$

where for any $w=(w_1,\dots ,w_v)$, ${\widetilde{eq}}_w(x)$ is called equality polynomial,

$$\widetilde{eq}(x_1,\dots ,x_v)=\prod _{i=1}^v(x_i{w}_i+(1-x_i)(1-w_i))$$

Sumcheck protocol

To Prove: ${\sum }_{i=0}^{n}f=c$

More precisely, sumcheck protocol is used to prove a v-variate polynomial defined over a Finite field $\mathbb{F}$.

$$\begin{array}{c}H:=\sum _{b_1\in \left\{0,1\right\}}\sum _{b_2\in \left\{0,1\right\}}\cdots \sum _{b_v\in \left\{0,1\right\}}g(b_1,\dots ,b_v)\end{array}$$

Let’s see how the protocol behaves:

• $\mathcal{P}\to \mathcal{V}:C$ claiming $C$ to equal to $H$
• round 1: $\mathcal{P}$ sends a univariate polynomial: $g_1(X_1)={\sum }_{x_2,\dots ,x_v\in {\left\{0,1\right\}}^{v-1}}g(X_1,x_2,\dots ,x_v)$
• $\mathcal{V}$ checks that $C_1=g_1(0)+g_1(1)$, and ${\mathrm{deg}}_1(g)\le \mathrm{deg}(X_1)$
• $r\in \mathbb{F}\leftarrow \mathcal{V}$, and sends to $\mathcal{P}$
• round i:
  • $\mathcal{P}\to \mathcal{V}:g_j(X_j)={\sum }_{x_{j+1},\dots ,x_v\in {\left\{0,1\right\}}^{v-i}}g(r_1,\dots ,r_{i-1},X_j,x_{j+1},\dots ,x_v)\forall i\in [2,v-1]$
  • $\mathcal{V}$ checks $g_j(0)+g_j(1)=g_{j-1}(r_{j-1})$ and sends $r_j\in \mathbb{F}$ to $\mathcal{P}$
• last round: $\mathcal{P}\to \mathcal{V}:g_v(X_v)=g(r_1,\dots ,r_{v-1},X_v)$
  • $\mathcal{V}$ checks $g_v(0)+g_v(1)=g_{v-1}(r_{v-1})$, and $\mathrm{deg}(g_v)\le deg(X_v\in g)$
  • checks with oracle query access to $g$ that $g(r_1,\dots ,r_v)=g_v(r_v)$

Efficiency:

• $P$: for each round i: $\mathcal{O}(1+{\mathrm{deg}}_i(g))\cdot 2^{v-j}$ terms are sent

Univariate sumcheck

Introduced in Aurora Paper, univariate sumcheck proves relation for a univariate polynomial $f(x)$ of degree $d$ and subset $H\subseteq \mathbb{F}$:

$$\sum _{a\in H}f(a)=0$$

Properties of protocol:

1. rounds: $\mathcal{O}(\log d)$
2. proof complexity: $\mathcal{O}(d)$
3. query complexity: $\mathcal{O}(\log d)$
4. prover operations: $\mathcal{O}(d\log |H|)$
5. verifier operations: $\mathcal{O}(\log d+{\log }^2|H|)$

Uses theorem stated by Byott and Chapman BC99 that ${\sum }_{a\in H}f(a)=0$ iff $f$ has degree less than $|H|-1$. Prove this using FRI protocol by BBHR18b which has proof complexity $\mathcal{O}(\log d)$ and proof length $\mathcal{O}(d)$. For case when degree $d>|H|-1$: we observe that we can split any polynomial $f$ into two polynomials $g$ and $h$ such that $f(x)\equiv g(x)+{\prod }_{\alpha \in H}(x-\alpha )\cdot h(x)$ with $deg(g)<|H|$ and $deg(h)<d-|H|$; in particular, $f$ and $g$ agree on $H$, and thus so do their sums on $H$.

$$\begin{array}{rl}\hat{f}& \equiv \hat{g}+{\mathbb{Z}}_H\cdot \hat{h}\\ \sum _{a\in H}\hat{f}(a)& \equiv \sum _{a\in H}(\hat{g}(a)+{\mathbb{Z}}_H\cdot \hat{h}(a))=\beta \sum _{a\in H}{a}^{|H|-1}\end{array}$$

• https://hackmd.io/@kIJ38IbETaGkxGkcxhrNVg/HycoeJUJh?utm_source=preview-mode&utm_medium=rec

GKR

$\mathcal{P}$ and $\mathcal{V}$ agrees to a circuit. $\mathcal{P}$ proves $\mathcal{V}$, the output of the circuit.

Taken from jolt repo:

GKR is a SNARK protocol for binary trees of multiplication / addition gates. The standard form allows combinations of both using a wiring predicate ${\tilde{V}}_i$, and two additional MLEs ${\widetilde{add}}_i$ and ${\widetilde{mult}}_i$.

${\tilde{V}}_i(j)$ evaluates to the value of he circuit at the $i$-th layer in the $j$-th gate. For example ${\tilde{V}}_1(0)$ corresponds to the output gate.

${\widetilde{add}}_i(j)$ evaluates to 1 if the $j$-th gate of the $i$-th layer is an addition gate.

${\widetilde{mult}}_i(j)$ evaluates to 1 if the $j$-th gate of the $i$-th layer is a multiplication gate.

The sumcheck protocol is applied to the following:

$${\tilde{V}}_i(z)=\sum _{(p,{\omega }_1,{\omega }_2)\in \{0,1{\}}^{s_i+2s_{i+1}}}{f}_{i,z}(p,{\omega }_1,{\omega }_2),$$

where

$$f_i(z,p,{\omega }_1,{\omega }_2)={\beta }_{s_i}(z,p)\cdot {\widetilde{add}}_i(p,{\omega }_1,{\omega }_2)({\tilde{V}}_{i+1}({\omega }_1)+{\tilde{V}}_{i+1}({\omega }_2))+{\widetilde{mult}}_i(p,{\omega }_1,{\omega }_2){\tilde{V}}_{i+1}({\omega }_1)\cdot {\tilde{V}}_{i+1}({\omega }_2)$$ $${\beta }_{s_i}(z,p)=\prod _{j=1}^{s_i}((1-z_j)(1-p_j)+z_j{p}_j).$$

Lasso and Jolt implement the Thaler13 version of GKR which is optimized for the far simpler case of a binary tree of multiplication gates. This simplifies each sumcheck to:

$${\tilde{V}}_i(z)=\sum _{p\in \{0,1{\}}^{s_i}}{g}_z^{(i)}(p),$$

where

$$g_z^{(i)}(p)={\beta }_{s_i}(z,p)\cdot {\tilde{V}}_{i+1}(p,0)\cdot {\tilde{V}}_{i+1}(p,1)$$

GKR is utilized in memory-checking for the multi-set permutation check.

Resources

• recmo’s post about sumcheck
• JThaler’s: unreasonable power of sumcheck
• JThaler’s sumcheck notes
• JThaler’s: Proofs, Args, and ZK, Chapter 3, 4
• JThaler’s small sumcheck
• erhant’s notes on Lecture 4 of ZKP MOOC
• NUS CS6230: The power of IPs
• Berkeley’s CS294: Introduction to IP & Sumcheck
• risencrypto’s sumcheck
• zk sumcheck
• sumcheck arguments and their application
• CPerez’s post about sumcheck
• CPerez’s ideas about GKR