# Research updates May 14th, 2023

In the doc “[zkNARK for R1CS](https://hackmd.io/lbqy8vPnRtK7e9xPjgdVNQ)”, I mentioned that the verification of NARK for R1CS can be batched, hence leading to cheaper on-chain (EVM) verifications. **However, the reality was that even if we can batch multiple proofs and avoid linearly increasing the verification cost, the concrete cost of verifying the batched proofs will be too high.**

Before describing why this was the case, I’ll outline the two approaches to realizing verification of batched proofs: proof composition, and a bespoke zkSNARK for the verification.

## Proof composition

Proof composition means using systems like Halo2 to arithmetize the verification to produce succinct proofs of verification. We want to avoid this for two reasons:

- Proof composition is complex.
- Proof composition requires wrong-field arithmetic which results in high proving cost.

halo2-spartan was an attempt to do this, but for the above reasons I decided to halt the effort ([and made the repo private](https://github.com/personaelabs/halo2-spartan)).

## A bespoke zkSNARK for the verification

A bespoke zkSNARK is something similar to the “zkSNARK for Committed Relaxed R1CS” in [Nova](https://eprint.iacr.org/2021/370.pdf). Nova constructs a zkSNARK for its IVC scheme using techniques from [Spartan](https://eprint.iacr.org/2019/550), and we *can* build something similar for NARK for R1CS. However, there are several issues with this approach as well.

### Unavailability of curve cycles

IVC schemes like Nova use an elliptic curve cycle. In short, every _folding_ in Nova is attached with a proof the attests to the validity of the folding, and the final zkSNARK only needs to verify that the final folded relaxed R1CS instance is valid (Because the validity of the final instance implies the validity of the preceding steps).


On the contrary, the accumulation scheme for NARK for R1CS doesn’t attest to the accumulation at each step and only verifies that the accumulation was done correctly after all proofs are accumulated. This design is appealing from the perspective of backward compatibility since it doesn't require a curve cycle (Not all curves have a curve cycle, so we don’t want this to be a requirement for our proof system. More on this [here](https://www.notion.so/Supercharge-credible-nuance-with-accumulation-without-succinct-arguments-3b68da8e8c3843caab96d338c5e20221)).

However, this incurs much more work to the final zkSNARK, and there likely isn’t a zkSNARK that can efficiently prove and verify the accumulation.


**In other words, a bespoke zkSNARK for the final proof works for Nova, but not for NARK for R1CS because the former verifies the folding at each step, and the latter doesn't. This difference comes from the usage of elliptic curve cycles; Nova can verify folding at each step because it’s *allowed* to use elliptic curve cycles, but NARK for R1CS (in our context) isn’t.**

## A new approach

Switching gears, we turn back to [FRI](https://eccc.weizmann.ac.il/report/2017/134/). FRI-based zero-knowledge proofs have been appealing from the perspective of client-side zk since they can work with all finite fields (by using [ECFFTs](https://www.math.toronto.edu/swastik/ECFFT1.pdf)). **A concern that is often raised about FRI is that the verification complexity is logarithmic to the size of the proven statement. However, recall that the statements proven in client-side zk, is (and have to be) small.**

Therefore we can formulate a hypothesis: T**he concrete cost for FRI verification in the context of client-side zk is small that on-chain (EVM) verification of proofs is economically viable.** To explore this hypothesis, we construct a proof system for based on Spartan: [Spartan-FRI](https://github.com/DanTehrani/spartan-fri).

## Spartan-FRI

### Spartan

Before fleshing out the design of the Spartan-FRI protocol, we recall Spartan. Spartan is a proof system for R1CS relations that consists of (non-exhaustive)

- zero-knowledge sum-check
- polynomial commitment scheme (PCS) for multilinear polynomials

The Spartan paper instantiates the protocol with

- Sigma protocol and Pedersen commitments for the zk sum-check
- Bulletproofs-like PCS for the multilinear PCS

This instantiation requires the verifier to perform a single multi-exponentiation of size N, where N is the number of variables in the R1CS. (which is too expensive for the EVM!)

### Spartan-FRI

In Spartan-FRI, we plan to realize zk sum-check and the multilinear-PCS using different techniques to realize on-chain verification.

- zk sum-check proposed in the [Libra paper](https://eprint.iacr.org/2019/317.pdf) (section 4.1).
- We can’t use the same zk sum-check protocol as in Spartan because it’s _connected_ to the PCS scheme in use.
- FRI-based multilinear-PCS described in the [HyperPlonk paper](https://eprint.iacr.org/2022/1355.pdf) (Appendix B).

The verification consists of the verification of the zk sum-check, and the verification of the FRI-PCS opening (which we hope is feasible on the EVM).

### Is Spartan-FRI accumulable?

The fact that the FRI PCS [can be batched without any linear increase in verification cost](https://aszepieniec.github.io/stark-anatomy/fri#compiling-a-polynomial-iop) gives us a design space for accumulation/batching.

Moreover, sum-checks might also be accumulatable in an efficient manner. ([Gemini](https://eprint.iacr.org/2022/420.pdf) provides relevant techniques).

## Zooming out, the path from here

Firstly, I’ll be focusing on getting the *[MVP of Spartan-FRI](https://github.com/DanTehrani/spartan-fri)* done to get the relevant benchmarks. Upon getting the MVP done I believe we should expose the project to the public. We can do so by integrating with Circom (i.e. Spartan-FRI proof generation using Circom circuit binaries), and letting developers experiment with the new proof stack including the on-chain verifier.

As of the 15th of May, I’ve implemented the sum-check part of Spartan (yet to make zk), and its verifier in Solidity.

High-level todos left for the MVP I currently recognize are

- Implement FRI-based multilinear PCS
- Implement **univariate** FRI-PCS (the univariate FRI-PCS is a sub-protocol of multilinear FRI-PCS)
- Implement the PIOP for the tensor-product relation (which yields the evaluation of the multilinear polynomial at the given point).
- Implement the multilinear-FRI verifier in Solidity
- This will be the moment of truth; will on-chain FRI verification be cheap enough??
- A Circom interface
- The MVP should include an _interface_ to let developers experiment with it. Circom seems like a good starting point.
- As a sub-task for the Circom support, I believe it’s better to implement a witness generator for the Circom R1CS files in Rust (instead of using the WASM witness generator emitted from the Circom compiler).