aszepieniec
commented
4 months ago Is this alternative construction sound? Here goes an argument in support of "yes".
Suppose there exists a malicious prover who convinces the new verifier of a falsehood, meaning that
- the FRI verifier accepts;
- all inner product checks succeed;
- even though at least one of the batched trace columns is $\delta$-far from the code of low-degree polynomials.
The batched codeword is well defined because the malicious prover commits to it. This batched codeword either (a) corresponds to a low-degree polynomial, or (b) is $\delta$-far from any codeword that does. (We ignore the middle.)
The probability that FRI accepts a far from low degree codeword is captured by the soundness analysis of FRI. This quantity is already present in the soundness error of the current construction and thus does not constitute soundess degredation.
The probability that batching generates a codeword that is closer than relative Hamming distance $\delta$ from the code of low-degree polynomials, even though at least one of the inputs to the batch is $\delta$-far from this code, is bounded by $\epsilon$ from the $(\delta, \epsilon)$ proximity gap used to prove the soundness of FRI. It follows that the soundness degradation is bounded by $\epsilon$.
A discussion with @ulrich-haboeck highlights a discrepancy between TritonVM's workflow and the workflow of (to wit) every other STARK construction. Other STARK systems separate the batch verification from the first folding step of FRI. In Triton VM, these steps are merged into one, and the first FRI codeword is never explicitly committed to. In exchange for introducing a new Merkle tree and the workloads of having to build and open it, and verify its paths, this alternative STARK construction reduces by half the number of rows of the low-degree-extended trace that must be opened and verified. This affects both the zero-knowledge calculus (fewer zerofiers required) and the verifier work (fewer inner products).