# Research updates June 12th

## Formal specification and security proof of Spartan-FRI

- For the past week or so, I’ve been writing a formal specification and the security proof of Spartan-FRI. There are several reasons for this:
- It’s easier to implement when there is a detailed specification.
- Rigorous specification is necessary to understand its security.
- Rigorous specification allows us to understand where Spartran-FRI fits in the literature of zero-knowledge proofs.
- To boost the confidence of implementors through security proofs (including myself).

The most challenging part of writing a security proof for Spartan-FRI is the soundness analysis of the FRI protocol. To understand the soundness of FRI, I’ve been learning coding theory and poring papers regarding the soundness of FRI.

**Coding theory**

- [An Introduction to Coding Theory: Lecture Notes](https://pages.mtu.edu/~tonchev/Coding-Theory-Tohoku-June-09.pdf)
- [Algebraic coding theory (playlist)](https://www.youtube.com/watch?v=vfjN7MmSB6g&list=PLkvhuSoxwjI_UudECvFYArvG0cLbFlzSr)

**FRI soundness**

- [The original FRI paper](https://drops.dagstuhl.de/opus/volltexte/2018/9018/pdf/LIPIcs-ICALP-2018-14.pdf)
- [A summary on the FRI low degree test](https://eprint.iacr.org/2022/1216.pdf)
- [Worst-case to average case reductions for the distance to a code](https://www.math.toronto.edu/swastik/fri.pdf)
- [DEEP-FRI](https://sites.math.rutgers.edu/~sk1233/deep-fri.pdf)
- [Proximity Gaps for Reed–Solomon Codes](https://eprint.iacr.org/2020/654.pdf) (The latest update on the analysis of FRI soundness)
- [ethSTARK](https://eprint.iacr.org/2021/582)

## FRI-recursion vs FRI-batching

FRI-recursion and FRI-batching achieve the same goal: reduce the problem of verifying multiple FRI proofs into verifying a single FRI proof.

- FRI-recursion allows incrementally verifiable computation, hence is appealing for proving the integrity of sequential computations, such as a VM execution. And there’s no limit to the number of steps FRI-recursion can prove.
- On the other hand, FRI-batching is limited to the memory of the prover.
- [More on batching and recursion](https://medium.com/zklend/notes-on-stark-recursion-b83c390644b).

So in general, FRI-recursion enables better prover performance than FRI-batching. However, given that FIR-recursion is more complicated to implement than FRI-batching, it might be valuable to think about a way to scale the **batching of non-sequential statements (e.g. membership proof).** Recursion has been hyped because it’s suited for proving VM execution, but there might be some difference in scalability and complexity when it comes to proving non-sequential statements.

## On circuit frontends

Even though Spartan-FRI will initially only support R1CS compiled by Circom, it can be modified to support other arithmetization methods (PLONKish, CCS, AIR, etc) and hence other DSLs. Although Circom is a popular DSL, many developers will prefer other DSLs (e.g. Noir, Cairo).

**Noir**

After doing the hello world of Noir, I got the impression that it’s more feature rich than Circom but less mature; Noir compiles to an intermediate representation of a constraint system that can encode any statement, so it’s compatible with R1CS, Plonkish, etc, and it also comes with nice debugging tools but it’s still not well-documented and there’s no public specification of the intermediate representation.

**Cairo**

I tried Cairo a while ago so I need to update my knowledge about it, but I have an impression that Cairo is a really popular DSL and has a really strong developer ecosystem for both the language itself and the applications that are written in it.

## FRI and Validiums work well with each other

- One hypothesis that motivates the use of FRI is: for zk apps that don’t involve asset transfers, on-chain proof verification doesn’t require L1 data availability. In other words, verifying proofs on Validiums is sufficient.
- FRI (and STARK) has been portrayed as a proof system whose advantage is its fast prover and its “flexibility” (batchable/recursible, backward-compatible), and its disadvantage is its large proofs. Due to the large proofs of FRI, some developers have opted for SNARKs which provide much smaller proofs. However, for zk apps that don’t involve asset transfers, it’s sufficient to verify proofs on Validiums where storage is really cheap. Therefore, the large proof size of FRI isn’t a problem. Therefore with its superior proving time and flexibility, FRI becomes a more attractive proof system than SNARKs in our setting (zk apps without asset transfers).
- afaik there are no Validiums that support general computations as of now, but there are teams working on them. [zkPorter](https://blog.matter-labs.io/zkporter-a-breakthrough-in-l2-scaling-ed5e48842fbf) from Matters Labs and [Starknet](https://twitter.com/Starknet/status/1666351045155627008).

## What I’ve been reading

- [Reed-Solomon codes over the circle group](https://eprint.iacr.org/2023/824.pdf)
- This is a new technique developed by the Ploygon R&D team. And it might become a part of Plonky3.
- Since this is about FRI, we might be able to apply some findings in the paper in our proof systems.
- [Anatomy of STARK](https://aszepieniec.github.io/stark-anatomy/)
- This is a great series of blog posts that goes deep into STARK and its implementation. There are several mentions of tricks/hints for speed-up the proving of FRI-based proof systems.