# GKR in practice

## Describing the circuit
$$
S_i= \text{# of gates in layer }i
$$

$$
k_i=log(S_i)
$$

$$
W_i:\{0,1\}^{k_i} \rightarrow \mathbb{F} \quad \text{(binary gate label}\rightarrow \text{gate's value at layer}_i)
$$


$$
S_0=2, S_1=4, S_2=4
$$

$$
k_0=1, S_1=2, S_2=2
$$

## Goal

The goal is to reduce the claim of the output values of the circuit to a claim about the lower layer, and repeat the process until we reach the input layer and we can verify claim ourselves.

More specifically:

$P$ starts at the output values and construct $D: \{0,1\}^{k_0} \rightarrow \mathbb{F}$
$P$ sends $D$
$V$ sends $r_0 \in \mathbb{F}^{k_0}$
$P$ sends $D(r_0)$

At this point, $P$ claims that $D(r_0)=\widetilde{W}_0(r_0)$, but $V$ cannot evaluate $\widetilde{W}_0(r_0)$ without help from the prover. So instead $P$ reduces the claim $\widetilde{W}_0(r_0)$ to a claim about $\widetilde{W}_1(r_1)$ for some $r_1 \in \mathbb{F}^{k_1}$ until it gets to the input layer.

## Details about reducing claims

We can express a multilinear extension of $W_i$ as the following:
$$
\widetilde{W}_i(z) = \sum_{b,c\space\in \{0,1\}^{k_{i+1}}} \widetilde{add}_i(z,b,c)(\widetilde{W}_{i+1}(b)+\widetilde{W}_{i+1}(c))+\widetilde{mult}_i(z,b,c)(\widetilde{W}_{i+1}(b)\cdot\widetilde{W}_{i+1}(c))
$$

where
$$
add_i(a,b,c) = mult_i(a,b,c) = \left\{ \begin{array}{rcl}
1 & \mbox{if (b,c)=(in_1(a), in_2(a))}
\\ 0 & \mbox{otherwise}
\end{array}\right.
$$

Then we can apply the sum-check protocol to $\widetilde{W}_i(z)$ for a $r_i \in \mathbb{F}^{k_i}$ using the following polynomial:

$$
f^{(i)}_{r_i}(b,c)=\widetilde{add}_i(r_i,b,c)(\widetilde{W}_{i+1}(b)+\widetilde{W}_{i+1}(c))+\widetilde{mult}_i(r_i,b,c)(\widetilde{W}_{i+1}(b)\cdot\widetilde{W}_{i+1}(c))
$$

## Example

Let's walk through an example of an actual circuit with $|\mathbb{F}|=5$.


### Define $\widetilde{mult}_0(a,b,c): \{0,1\}^{k_0+2k_1} \rightarrow \{0,1\}$
$1 \space \text{if} \space (0, (0,0), (0,1)) \space \text{or} \space (1, (1,0), (1,1))$
=> $\widetilde{mult}_0=(1-x_1)(1-x_2)(1-x_3)(1-x_4)x_5 + x_1x_2(1-x_3)x_4x_5$
### Define $\widetilde{mult}_1(a,b,c): \{0,1\}^{k_1+2k_2} \rightarrow \{0,1\}$
$1 \space \text{if} \space ((0,0), (0,0), (0,0)) \space \text{or} \space ((0,1), (0,1), (0,1)) \space \text{or} \space ((1,0), (0,1), (1,0)) \space \text{or} \space ((1,1), (1,1), (1,1))$
=> ...?

### Define $\widetilde{W_i}$
$W_0(0)=4, W_0(1)=2 \space$
$\Rightarrow \widetilde{W}_0=4(1-x_1)+2x_1=4-2x_i$
$W_1(0,0)=1, W_1(0,1)=4, W_1(1,0)=2, W_1(1,1)=1$
$\Rightarrow \widetilde{W}_1=(1-x_1)(1-x_2)+4(1-x_1)x_2+2x_1(1-x_2)+x_1x_2=1+x_1+3x_2-4x_1x_2$

### Sum-check protocol for $b,c\in \{0,1\}^2$
$r_0=4$