# ark-bcs Lincheck Writeup

In `lincheck`, we want to prove the following relation: in the RS-IOP with field $\mathbb{F}$ and codeword domain $L$, we have

- domain $H_1$, denoted as **constraint domain**. This domain has size as number of constraints (power of two).
- domain $H_2$, denoted as **variable domain**. This domain has size as number of variables (power of two).
- $f_{Mz}, f_{z} \in RS[L, \rho]$. Its degree bound is $L\rho.$ We extend them to $\hat{f_{Mz}}$ in domain $H_1$, $\hat{f_{z}}$ in domain $H_2$.
- matrix $M \in \mathbb{F}^{H_1\times H_2}$ . Denote $|H_1| = m, |H_2| = n$.

We want to satisfy:
$$
\hat{f_{Mz}}(a) = \sum_{b\in H_2} M_{a,b} \cdot \hat{f_{z}}(b)
$$
In short, we want to show $\hat{f_{Mz}} = M\hat{f_{z}}$.

## Key Ideas

The key idea is to sample a random vector $\vec{r} \in \mathbb{F}^m$ and compute $M\vec{r}$.

If $\hat{f_{Mz}} = M\hat{f_{z}}$, then:
$$
\hat{f_{Mz}}\cdot\vec{r} = M\hat{f_{z}}\cdot \vec{r}\\
\hat{f_{Mz}}\cdot\vec{r} = M(\hat{r^T} \vec{f_z})\\
\vec{r}\cdot\hat{f_{Mz}} = (M^T\vec{r})\cdot \hat{f_{z}}\\
\vec{r}\cdot\hat{f_{Mz}} - (M^T\vec{r})\cdot \hat{f_{z}} = 0
$$
In Aurora paper, we have shown that instead of sampling $\vec{r}$ uniformly at random, with modest increase of soundness error, we can instead sample $\alpha$ such that
$$
\vec{r} = [1, \alpha, \alpha^2, ...]
$$
Now we low-degree extend both $\vec{r}$ and $M\vec{r}$ to $H$ where $H$ is the larger one of $H_1$ and $H_2$. Indeed, we need $H$ to be $H_1 \cup H_2$, but they are all power of two domain, so it's easy to do. Indeed, since constraints are always more than number of variables, $H = H_1$ so $|H| = m$

Because $\vec{r}$ is exactly at the domain point, it's trivial to find an LDE for $\vec{r}$ where
$$
\hat{\vec{r}} = [1, \alpha, \alpha^2, ..., \alpha^{m-1}]\\
$$
To get LDE of $M\vec{r}$, we would need to compute $M\vec{r}$ and low degree extend it to $\hat{M\vec{r}}$ to $H$ using one IFFT.

Note that now $\hat{f_{Mz}}$ and $\hat{f_{z}}$ is on domain $H = H_1$.

Thus, the relation of inner product becomes

$$
\sum_{x\in H_1}\hat{\vec{r}}(x) \cdot \hat{f_{Mz}}(x) - \sum_{y\in H_2} \hat{(M^T\vec{r})} (y)\cdot \hat{f_{z}}(y) = 0
$$

We want to do one sumcheck the relation above. To do so, the summation domain need to be $H_1 \cup H_2$.

$$
\sum_{x\in H_1 \cup H_2}A(x) \cdot \hat{f_{Mz}}(x) - B(x)\cdot \hat{f_{z}}(x) = 0
$$

where $A(x) = \hat{\vec{r}}(x)$ for $x \in H_1$ and $A(x) = 0$ for $x \in H_2 - H_1$. $B(x) = \hat{(M^T\vec{r})} (x)$ for $x \in H_2$ and $B(x) = 0$ for $x \in H_1 - H_2$.

## The protocol

**Verifier Input**:

- Access to oracle $f_{Mz}, f_{z}$ that belongs somewhere in transcript.
- Matrix $M$.
- Constraint domain $H_1$. Variable domain $H_2$.

**Verifier Output:** $TRUE$ if $\hat{f_{Mz}}(a) = \sum_{b\in H_2} M_{a,b} \cdot \hat{f_{z}}(b)$ where $\hat{f_{Mz}}$ is evaluation of $f_{Mz}$ on $H_1$. $\hat{f_{z}}$ in evaluation of $f_{z}$ on $H_2$. $FALSE$ otherwise.

1. Sample $\alpha$.

2. Compute LDEs. (*Requires 3 IFFTs*).

- $\hat{r}(x)$: no need to interpolate
- $\hat{f_{Mz}}$: need to interpolate $f_{Mz}$ to get coefficients.
- $\hat{f_{z}}$: need to interpolate $f_{z}$ to get coefficients.
- $M^T\vec{r}$: First evaluate $M^T\vec{r}$ (treating $\vec{r}$ as a vector on $H_1$). Then, interpolate it to get coefficients.

3. Make virtual oracle $H(x)$:
$$
H(x) = \hat{\vec{r}}(x) \cdot \hat{f_{Mz}}(x) -\hat{M^T\vec{r}} (x)\cdot \hat{f_{z}}(x)
$$

- Degree bound is $|H| + \mbox{degree bound of f1, f2}$ ($f_{Mz}, f_{z}$ have same degree bound).

4. Invoke sumcheck protocol for $H(x)$ with summation domain $H_1$ where claimed sum is $0$. (If $H_2$ is not a subset of $H_1$, then we need to multiply this virtual oracle by vanishing polynomial of $H_2$ to zero out.)

## Something Further

We can run `lincheck` on multiple instances simultaneously, using random linear combination.