Proposal: Limitless prover for Linea

Hello, I am AlexandreBelling working in the core Linea team on the prover. In this post, I will present an idea that we are pushing forward in the next upgrade of the proof system: removing the execution limits and how this will reduce the transaction fees in the long run.

Execution limits on Linea

Linea imposes execution limits on the transactions it processes. These limits control how much of certain operations a block of transaction can do. For instance, a Linea block can invoke at most 8192 times Keccakf sponge-function. In practice, there are approximately 50 different limits, each related to a particular area of the EVM.

Why limits?

The reason for these limits comes from the proof system: it needs to be pre-configured to prove up to a specific number of operations at once and for each area of the EVM. Increasing the limits means increasing the computations requirements to generate a proof regardless of how many keccaks are proved. Therefore, some trade-offs have to be made.

How are the limits decided?

The limits are designed in such a way that they do not impact the users 99% of the time. To estimate them we perform statistical analysis taking Ethereum’s and Linea’s mainnet activity. We also take into consideration direct feedback from users. For instance, we have increased some of the limits in the past to permit the deployment of ZK-applications on Linea. However, we still occasionally encounter unexecutable transactions, causing noticeable UX issues.

Why do we want to remove them?

On top of having a direct impact of the UX, the fact that Linea currently has 50 different limits is an issue for numerous technical reasons:

  • It means the sequencer of Linea has to count the limit utilizations of every transactions and every blocks. This comes with an important overhead in the sequencing process and corresponds to 90% of the CPU utilization of the sequencer. Currently, this limits the maximal number of TPS that Linea can do to approximately 100TPS (peak reached during Linea Park), thus removing it will directly remove this bottleneck and move it somewhere else.

  • As we deal with 50 different limits, this tends to reduce the efficiency of the system. To simplify, assume that there are 3 limits: one for the number of contract deployment, one for the number of multiplications and one limit of the number of ECPairings. Most of the time, what happens is that one block typically overuse one limit and not the others. As a result, the prover computation resources are used optimally.

  • With the current limits, the prover needs 700GiB of RAM to be able to perform a validity proof. This may seem unrelated to the fact that we have limits but bear with me. A consequence of the heavy memory requirements is that we need more expensive machines to run the prover, impacting the final transaction costs for the user.

The concrete plan

To remove the limits, we plan on relying on a prover distribution scheme. The main idea is that we will split prover jobs in “segments” both horizontally and vertically and we will generate proofs for segments independently before aggregating them. Horizontally splitting means that different areas of the EVM are processed in different segments independently. Vertically splitting means that we generate a varying number of proofs for each modules depending on whether the corresponding area of the EVM is used a lot or not during the execution. The whole system is completely asynchronous, so this means that different prover jobs do not have to synchronize at any point in time.

Handling the lookups and the permutation constraints.

Some types constraints can be cross-segments and they typically represent how modules are connected to each others in practice. This the case for lookup constraints, permutation constraints and projection constraints. The challenge with these constraints is that they will apply over distincts segments at the same time. To handle them we will be generating specific proofs that are specialized in handling these queries and we have designed a shared-randomness process that allows different segments to use the same randomness while keeping the system fully-asynchronous. A consequence of this design is that each segment will be generating two proofs, one for the non-lookup-permutations-projections queries and one for the lookup-permutations-projections.

Aggregating the segment proofs

Before we can output an execution proof, we have to aggregate all the segment proofs togethers. This aggregation is leveraging the recursion techniques that we have already developed to reduce the proof size of Vortex: verifying many Vortex proofs in a Vortex proof. The recursion process is fast (a couple of second per proofs) and it allows aggregating a very large number of proofs at once. The aggregation proof is also tasked to verify the consistency between each segment proofs to ensure that the sum of all the parts is correct and not just all the parts independently.

The benefits

  • Sub-proofs will require much less memory than what is required for the current “all-at-once” proof, meaning we can run it on more cost-effective machines.
  • Since the number of subproof for each module is dynamic, this creates a “pay-for-what-you-use” effect and we expect this will have a positive effect on the performances of the system.
  • We will be able to remove the limit counting logic in the sequencer allowing it to go a lot faster, unlocking much higher TPS on Linea.
8 Likes

don’t know clearly how it work but hope Linea will success!