In this note, I will try to explicate an idea suggested to us by Joseph Johnston.
In normal FRI-Binius, the prover kicks off the sumcheck by sending the verifier . This information is enough for the verifier to compute ; indeed, the verifer can just compute and compare this thing to the claimed evaluation .
The tricky observation there is that the quantity above is also nothing other than the column representation of , which itself equals
By running a sumcheck on this above thing, over the algebra, the prover and verifier can thus reduce the validity of to that of .
The first nontrivial claim is that the vector above—which, as we already saw, contains just the required data to compute —is itself in turn "equivalent", up to a matrix mult, to the further data . Here, we write for the Frobenius, i.e., the thing that generates . In particular:
Claim 1. We have the matrix identity:
Proof. It's enough to fix arbitrary and and prove that . To this end, we carry out the following calculation:
which is what we want. The second equality above is just the definition of . In the third, we distribute the Frobenius, and also use the fact that each (and is fixed by the Frobenius).
Claim 2. The matrix —i.e., whose entry is —is invertible.
Proof. This nontrivial fact is exactly [LN97, Lem. 3.51].
Now progressing onwards, we see moreover that the left-hand vector above itself can be made to relate to the evaluations of the single polynomal at a number of different places. Indeed, we have:
Moreover, given only the left-hand vector above, the verifier can locally "peel off" the s, in order to obtain the further vector:
The nice thing about this is that it's just evaluated at a number of different points, namely the "componentwise Galois orbit" of . The idea now is that we're going to use [Fig. 3, RR21]-style batching on this set of claims. This will entail a single sumcheck which takes place entirely over .
We will now sketch the end-to-end protocol.
In the eval phase, the parties have a joint evaluation point and a claimed evaluation . The prover has .
The prover and verifier now run an [RR21]-style batched sumcheck on the claims , for . Unwinding what this means, we have:
Assuming the truth of Claim 1, we argue correctness in the following way. If the prover is honest, then will hold; by Claim 1, the verifier will have . We see that the verifier will finally in turn have The rest comes down to the correctness of Rothblum-style batching. In particular, you need to convince yourself that
will hold. The first equality involves interchanging a sum, and is essentially the "content" of [Fig. 3, RR21]'s completeness statement. The second equality holds assuming the prover was honest; this was just calculated above. The third equality is by definition on the verifier's part. Thus if the prover is honest, then its sumcheck claim will be true. The verifier's final step amounts to evaluating ; here, is used as a standin for .
The efficiency of the above protocol is quadratic for the verifier in . Indeed, you can see this already in the verifier's multipliation . Actually, it is interesting to ask whether there is a kind of "Galois NTT", which would allow multiplication by to be carried out in time.
A further question is the verifier's computation of above. It seems that the verifier needs to do "triangularly many" applications of the inverse Frobenius here; i.e., for each , the computation will take inverse Frobeniuses. Up to the issue of forward versus inverse (which shouldn't matter, since we can just "invert the triangle", using cyclicity), this will again take quadratic total work in .
As far as proof cost: the total cost is a FRI-run on something -variate over and then also a sumcheck on something -variate over . So it seems that we are getting 0 embedding overhead whatsoever (for the prover—the verifier needs to do some work).
The fascinating fact is that Claim 2 is necessary for security. As a sketch, we need to argue that if , then will reject. First off, assuming that (i.e. that the prover's claim is false), we immediately get the claim that if then will reject its check 2. above. We may thus assume that . In this case, assuming Claim 2, we have that is injective; we may thus assume further that will hold. Thus we finally get that will hold, since everything Frobenius-related is invertible. This then comes down to the soundness of (tensor-style) Rothblum batching, and the usual arguments of FRI-Binius. Thus the soundness overhead of this protocol over and above normal FRI-Binius is that of the tensor-style batch, which is .
[LN97]: Lidl, Rudolf and Niederreiter, Harald. Finite Fields. 1997.
[RR21]: Ron-Zewi, Noga and Rothblum, Ron. Local Proofs Approaching the Witness Length. Journal of the ACM.