Understand StarkNet Zero-Knowledge Recursive Proofs in One Article - STARK

Original Title: “Recursive STARKs”

Author: StarkWare Core Engineer Gidi Kaempfer

Translation: StarkNet Chinese Community

Summary

• Recursive proofs are live on the mainnet, using a single proof to scale StarkEx applications and StarkNet
• Recursive proofs enhance scalability, reduce costs and latency (rarely do scalability and latency develop in sync without trade-offs)
• Recursive proofs create conditions for L3 and other clever applications
• Check out the blog post on recursive proofs, it's super cool ?

Multiplicative Scaling!

Recursive proofs powered by Cairo's general computation are now in production. This marks a significant enhancement in STARK's L2 scalability. The number of transactions written to Ethereum with a single proof can increase rapidly.

So far, STARK proofs have achieved scalability by "aggregating" thousands or even hundreds of thousands of transactions into a single proof written to Ethereum. With recursion, many such proofs can be "aggregated" into a single proof.

This approach is now applied to numerous Cairo-based applications: running on StarkWare's SaaS scaling engine StarkEx and the permissionless Rollup StarkNet.

Development History So Far

Since the first proof was generated on the mainnet in March 2020, STARK proofs have gone through different stages of development.

STARK Scaling

In June 2020, the first STARK scaling solution, StarkEx, was deployed on the Ethereum mainnet. StarkEx has a prover that can perform large computations off-chain, generating a STARK proof representing transaction accuracy, and a verifier that validates the proof's accuracy on-chain. The initial deployment was personally handled from scratch by StarkWare engineers, so StarkEx's functionality was greatly limited. Ultimately, we decided that a programming language supporting proof of general computation was needed. Thus, Cairo was born.

Cairo Programming Language

In the summer of 2020, Cairo made its debut on the Ethereum mainnet. Cairo stands for CPU Algebraic Intermediate Representation (AIR), containing a single AIR for verifying the corresponding "CPU" instruction set. Cairo opens the door to coding proofs for more complex business logic and arbitrary computational statements, faster and more securely. A Cairo program can prove the execution logic of the corresponding application. But a Cairo program can also aggregate multiple such applications, which is SHARP.

SHARP

SHARP stands for SHARed ProSver, which can aggregate transactions from several independent applications and prove them in a single STARK proof. Applications can combine different batch transactions, filling the capacity of the STARK proof faster. Both transaction processing speed and latency are improved. Recursive proofs are the next-generation cutting-edge technology, applicable not only to some hard-coded logic but also to general computation.

To understand all the advantages of recursive proofs, it is necessary to further explore how SHARP has executed (non-recursive) proofs so far. Figure 1 depicts a typical non-recursive process:

In this process, propositions gradually arrive. When the capacity (or time) reaches a certain threshold, a large composite proposition (Train) is generated. This composite proposition can only be proven after receiving all individual propositions. This proof takes a long time (about the total time required to prove each individual proposition).

Proving extremely large propositions will ultimately be limited by available computational resources such as memory. Before recursion, this was actually a major obstacle limiting the scalability of STARK proofs.

What are Recursive Proofs?

With STARK proofs, the time taken to verify a proposition is roughly linearly related to the time taken to execute the proposition. Furthermore, if proving a proposition takes time T, then verifying the proof takes about log(T), which is often referred to as "logarithmic compression." In other words, using STARK allows users to spend much less time verifying propositions than computing them.

Cairo allows expressing general computational propositions, which can be verified by STARK proofs and then validated by the corresponding STARK verifier.

This is where the opportunity for recursion lies: just as one can write a Cairo program to prove the correctness of thousands of transactions, one can also write a Cairo program to verify multiple STARK proofs. A proof can be generated to verify the validity of multiple "upstream" proofs. This is what we call recursive proofs.

Due to logarithmic compression and the roughly linear relationship in proof time, the time required to verify STARK proofs is relatively short (expected to be just a few minutes in the near future).

When implementing recursion, SHARP can verify propositions as soon as they are received. Proofs can be repeatedly combined into recursive proofs in various patterns until, at some point, the generated proof is submitted to the on-chain verifier contract. Figure 2 illustrates a typical recursive proof pattern:

In this example, four propositions are sent to SHARP (possibly originating from four different applications). Each of these propositions is proven in parallel. Then, each pair of proofs is verified by a recursive verifier proposition (a Cairo program that verifies STARK proofs), resulting in a proof. This proposition confirms that two proofs have been verified. Next, these two proofs are merged again through the recursive verifier proposition. This produces a proof that confirms all four original propositions. This proof can ultimately be submitted on-chain, verified by a Solidity verifier smart contract.

Direct Advantages of Recursive Proofs

Lower On-Chain Costs

There is no doubt that we have achieved compressing multiple proofs into one, which means the on-chain verification cost per transaction will be significantly lower (where each proposition may contain many transactions).

Using recursive proofs can eliminate the computational resource barriers that have so far limited proof size (such as memory), as each proposition has limited capacity and can be proven individually. Therefore, when using recursion, the capacity of the effective combined propositions (Train) is nearly infinite, and the cost per transaction can be reduced by several orders of magnitude.

In practical terms, cost reduction depends on acceptable latency (and the speed at which transactions arrive). Additionally, since each proof usually also comes with corresponding on-chain data output, the amount of data written to the chain with a single proof will also be limited. Nevertheless, reducing costs by an order of magnitude, or even continuing to improve performance, can be easily achieved.

Lower Latency

The recursive proof pattern can reduce the latency of proving large composite propositions. Two factors are at play:

1. Received propositions can be proven in parallel (instead of proving a huge composite proposition).
2. There is no need to wait for the last proposition in the Train to arrive to prove it. Instead, new propositions can be combined with the proof at any time. In other words, the latency of the last proposition added to the Train is roughly the time required to prove the last proposition plus the time required to prove the recursive verifier proposition (which proves all propositions that have "joined" this specific Train).

We are actively developing and optimizing the latency issue of proving recursive verifier propositions. It is expected that within a few months, the proving time for recursive verifier propositions will reach the order of minutes. Therefore, an efficient SHARP latency can be controlled within a few minutes to a few hours, depending on the trade-off for on-chain costs per transaction. This is a significant improvement in SHARP latency.

Facilitating L3 Applications

Recursive verifier propositions developed with Cairo also open up the possibility of submitting proofs to StarkNet, as these propositions can be written into StarkNet smart contracts. This allows for the deployment of L3 on the StarkNet L2 public network.

The recursive pattern is also applicable to aggregated proofs from L3, verified by a single proof on L2. Thus, L3 can also achieve massive scalability.

More Clever Applications

Applying Recursion

Recursion opens up more opportunities for platforms and applications looking to further scale their costs and performance.

Each STARK proof verifies the validity of propositions applied to certain "public inputs" (or "program outputs" in Cairo terminology). Conceptually, STARK recursion compresses two proofs with two inputs into a single proof with two inputs. In other words, while the number of proofs decreases, the number of inputs remains unchanged. The inputs are typically used by applications to update certain states on L1 (for example, updating the state root or executing on-chain withdrawals).

If recursive propositions can be perceived at the application layer, i.e., recognizing the semantics of the application itself, then recursive propositions can compress two proofs into one and combine two inputs into one. The final proposition verifies the validity of the input combination based on application semantics, which is what we call applicative recursion (see Figure 3 for an example).

Proposition 1 proves the state update from A to B, while Proposition 2 verifies the further update from B to C. The proofs of Proposition 1 and Proposition 2 can be merged into a third proposition, directly proving the update from A to C. By applying similar recursive logic, the cost of state updates can be significantly reduced, meeting the final latency requirements.

Another important example of applicative recursion is compressing aggregate data from multiple proofs. For instance, in a validity-proof Rollup like StarkNet, each L2 storage update also serves as transfer data for L1 updates, ensuring data availability. However, there is no need to send multiple updates for the same storage unit, as only transactions that have been proven to be verified ultimately satisfy data availability. This optimization has been executed in a single StarkNet block. However, by generating proofs for each block, applicative recursion can compress aggregate data from multiple L2 blocks. This can significantly reduce costs and lower L2 block times without sacrificing L1 update scalability.

It is worth noting that applicative recursion can be combined with the general recursion described earlier. However, these two optimizations are independent of each other.

Reducing Complexity of On-Chain Verifiers

The complexity of STARK verifiers depends on the types of propositions used for verification. Particularly for Cairo propositions, the complexity of the verifier depends on the specific elements allowed in the Cairo language, more specifically, the supported built-ins (if we liken Cairo to a CPU, then built-ins are akin to microcircuits in a CPU: computations are executed too frequently, so optimization is needed).

The Cairo language is continuously evolving and providing more useful built-ins. On the other hand, recursive verifiers only need to use a small subset of built-ins. Therefore, recursive SHARP can successfully support any proposition in Cairo by supporting the complete language in the recursive verifier. Specifically, the Solidity verifier on L1 only needs to verify recursive proofs, so the verifier can be limited to verifying a more stable subset of the Cairo language: L1 verifiers do not need to update with the latest and most stable built-ins. In other words, propositions continuously evolve, and complex verification is handled by L2, while L1 verifiers only need to verify simple, stable propositions.

Reducing Computational Footprint

Before recursion, aggregating multiple propositions into one proof was limited by the size of propositions that could be proven on available computational instances (and the time required to generate such proofs).

With recursion, there is no longer a need to prove such large propositions. Because there are more small and inexpensive computational instances available (although more computational instances may be needed than when using a large monolithic prover). This makes it possible to deploy prover instances in more physical and virtual environments.

Conclusion

General computation recursive proofs are now serving multiple product systems on the Ethereum mainnet, including StarkNet.

As improvements can be continuously made, the advantages of recursion will gradually become apparent. Once the potential of parallel computation is realized, gas fees will decrease, latency will improve, and ultra-high scalability will ultimately be achieved.

The advantages of recursion in terms of cost and latency are exceptionally significant and will also give rise to new opportunities such as L3 and applicative recursion. The recursive verifier will continue to optimize, and performance and cost-effectiveness will gradually improve.

Appendix

Original Article: Recursive STARKs

https://medium.com/starkware/recursive-starks-78f8dd401025

Original Article: Youtube: StarkEx - How Does it Work?

https://www.youtube.com/watch?v=P-qoPVoneQA

Original Article: Hello, Cairo!

https://medium.com/starkware/hello-cairo-3cb43b13b209

Original Article: Hello, Cairo!

https://starkware.co/cairo/

Original Article: Wikipedia Entry: Recursion

https://en.wikipedia.org/wiki/Recursion

Original Article: “Form-Based Scaling: From L2 to L3”

https://mirror.xyz/starknet-zh.eth/-5oiKxwShIOzGUwuQJzIl070wopcPjqBcypVjRvyC1E