Using the univariate sum-check IOP from Aurora to implement final evaluation claim

[Al-Kindi-0]

The following is a proposition for getting rid of the s column which is used to provide an opening proof for the final evaluation claims in GKR.

The main thing that we need to show is that $\Sigma_{i=0}^{n-1} Q(x_i) \cdot L(x_i) = \zeta$ where $Q$ is a random linear combination of main trace columns appearing in the LogUp relation we are trying to prove, and $L$ is the Lagrange kernel at the final evaluation point.
The s column serves to compute the above sum in a cumulative manner and thus make the above equivalent to showing that this cumulative sum has been computed correctly.
There is however another way to achieve the same result and it is called the univariate sum-check protocol as it appears in the Aurora paper.

The univariate sum-check protocol

Let $p(X)$ be a degree $D$ polynomial and let $H$ be the trace evaluation domain such that $|H| = n$. Assume without loss of generality that $D > n$, then we have the following lemma from Thaler's book (Lemma 10.2):

Lemma
$\sum_{x \in H} p(X) = 0$ if and only if there exists polynomials $q$ and $f$ such that $deg(q) \leq D - n$ and $deg(f) \leq n - 2$ such that $p(X) = q(X) \cdot \left(X^n - 1\right) + X \cdot f(X)$

Thus, in order to witness the sum, the prover provides two commitments, one to $q(X)$ and the other to $f(X)$. Subject to the degree bounds in the statement of the lemma being satisfied, the verifier can query the relevant oracles at a random point in order to check the claim.

Opening proof using univariate sum-check

Suppose we have only one trace column that we want to check the GKR final evaluation claim for, call it $Q$. Let $L$, as before, be the Lagrange kernel at the evaluation point. Then, the (STARK) prover would like to convince the verifier that $$\sum_{x \in H} Q(x) \cdot L(x) = \zeta.$$

We can reduce this claim to the one in the lemma as follows:
$$\sum_{x \in H} \left( Q(x) \cdot L(x) - \frac{\zeta}{|H|}\right)= 0 .$$

Hence we can apply the lemma with $p(X) := Q(X) \cdot L(X) - \frac{\zeta}{|H|}$.

Cost analysis

The dominant cost is the cost of computing the $Q(x) \cdot L(x)$. As the product is of degree less than twice that of $Q(X)$ and $L(X)$, we would need to evaluate and then interpolate on a domain of twice the size of the trace domain. This however can be absorbed in the LDE stage at very little extra cost.
Once the product is computed, the subtraction is trivial to do, the division by the $X^n - 1$ polynomial is easy to do using the Ruffini-Horner-Samaw'al-Xian method in linear time.

The prover then commits to $q(X)$ and $f(X)$ as part of the auxiliary trace so as to reduce the commitment cost.
The other costs related to the DEEP composition polynomial should be negligible.

From the verifier perspective, the main additional cost is related to the terms $\frac{q(x) - q(z)}{x - z}$ and $\frac{f(x) - f(z)}{x - z}$ in the DEEP composition polynomial queries. Evaluating the univariate sum-check protocol identity at the OOD point should incur very little overhead.

The following branch includes a POC implementation of the above

[Al-Kindi-0]

We went instead with the cohomological sumcheck argument as presented in the Darlin paper.