Plookup with zkEVM: A Brief Introduction to How zkEVM Works

The zkEVM project is both great and huge, which cannot be actualized correctly by any single team. It requires the collaboration and hard work of multiple great teams in this industry. Since there is no mature design for reference, all are exploring ways to realize it. The related articles published by Sin7Y Labs only represent our understanding of the zkEVM design, which is not guaranteed to be completely correct. We sincerely hope and desire to communicate with those professionals, learn from each other and get improvement to move forward together.

In the article Exploring Popular zkEVM Solutions, we have a preliminary analysis and comparison of the frameworks of zkEVM designs by Hermez, MatterLabs, AppliedZKP, and Sin7Y. One thing they have in common is to deal with the execution process of EVM separately, including logic calculation, state reading, etc. The following figure shows the general procedure of zkEVM:

As shown in Figure 1, when an overall process is separated and processed separately, it is necessary to ensure:

1. The data between each part is consistent. For example, the data involved in the logic calculation is the same as the data in the state read/write;
2. The order of the executed op is completely consistent with the logic of the contract to ensure the correctness of the program executed;
3. The logic calculation is correct, including Add, Mul, Sub, etc.

Because in the current Rollups scheme (which has specific circuits and is not compatible with EVM), the logic of the contract is written in the circuit, there is no need for PROVER to prove the correctness of the executed contract logic; while in zkEVM, the circuit contains only one op, and the logic of the contract often has multiple ops, which are executed in a certain order. We need to confirm that the order of this execution is consistent with the contract.

For better understanding, we call the functions described in 1) and 2) state proof and in 3) EVM proof:

1. State Proof proves that the implementation procedure is correct;
2. State Proof proves that the operations of stack, memory, and storage are correct;
3. EVM Proof proves that the input, output, and operational logic are correct.

All of the above three requirements can be achieved by using Plookup technology (as shown in Figure 1). For the introduction of the principle of Plookup technology, please refer to the previous article Plookup: An Algorithm Widely Used in zkEVM. Simply put, it is to prove that the set f € t, and the element in f appears at least once in t.

State Proof - 1: Ensure Execution of Right Procedures

When a contract is deployed in the layer 2 EVM, the bytecode will be stored in the Storage (for simplicity, we first consider the scenario of one contract, and multiple contracts can be distinguished according to the contract address); then the user initiates a transaction and calls a method in the contract (as shown in 1 and 2 in Figure 1), and the EVM will match the method when the contract is deployed according to the method signature. Once matched, the EVM will execute the corresponding logic according to the method matched and the parameters passed in by the user, and form the final execution trace (The entire execution traces).

However, there may be a problem. As mentioned earlier in the article, the specific circuit corresponds to a specific function in the rollup scheme of a specific circuit, so the correctness of the function has been guaranteed by the circuit and has been audited and disclosed by security companies. Therefore, Verifier only needs to hold the corresponding input and output to verify whether the data meets the circuit function; however, in the zkEVM design, the circuit only restricts the correct execution of the single-layer base opcode, but the order among opcodes cannot be guaranteed. For example, zkEVM's circuit can only guarantee the correctness of Add Op and Mul Op, but "from Add Op to Mul Op" and "from Mul Op to Add Op" can lead to completely different results. We need to ensure that their order is consistent with the contract itself.

Therefore, we should use Plookup technology to ensure that the op sequence executed by the prover is consistent with that in the contract. This part refers to the principles and ideas of Hermez. Importantly, if the calculation logic of the contract is very complicated, then the Table may take up a lot of memory space. Thus some means should be used to optimize the number of these instructions, such as replacing the Stack operation with Register, but this will increase modifications to the compiler.

Another way to achieve this is to use the Merkel Tree to prove it. As shown in Figure 2 below (Please note that extra fees may incur if you choose this scheme.):

A ZK-friendly hash is needed to implement this process to minimize the scale of this part of the circuit. (It can also be verified by Accumulator based on Class group. Compared with the Merkel tree, it can judge the existence of elements faster, and it can also realize batch verification.)

State Proof - 2: Ensure Usage of Right Data

As described previously, when the EVM matches the corresponding function based on the function signature, a real execute trace is formed according to the parameters input by the user. As shown in the middle part of Figure 1, the complete Trace includes stack operations, memory operations, storage operations, and some Arithmetic calculation operations. If one circuit is used to prove, then this circuit needs to prove:

1. The validity of the Stack operation, the scope limitations of the sp (stack pointer) value, the operation type limit (write/read), etc.
2. The validity of the Memory operation, the pc value limit of the same address (monotonically increasing), the operation type limit (write/read), etc.
3. The validity of the Storage operation.
4. The accuracy of the Arithmetic operation.

…

This will be a complex and huge circuit. Therefore, we need to make a functional segmentation. The function of one circuit is to ensure the validity of data read/write operations. State circuits can be divided into stack circuits, memory circuits, and storage circuits based on the type of Memory operation. The other circuit guarantees that these read/write values are correctly calculated (Add, Mul, Sub…), and ensures that the value involved in the mathematical calculation is consistent with the first circuit, as shown in Figure 1.

Therefore, a cache is needed, namely Busmapping, where valid stack data, memory data, and storage data are stored. When performing mathematical calculations, we need to verify that the value involved in the calculation is stored in Busmapping. For example, when performing the Add operation (a + b = c), we need to verify that a, b, and c are all stored in bus mapping (the plookup technology is still used here) and then verify whether they satisfy the addition relationship (we can use addition circuit + Lookup table, or we can also use Lookup table alone. The lookup table of the first method is used to verify the validity of the data, and the lookup table of the second method is used to verify the validity of the data and the correctness of the calculation. Two options can be selected according to the actual calculation type.)

It should be noted that after the transaction is executed, the storage value of the corresponding location has been updated, but the new state root has not. We need to write this value into bus mapping after calculating the new state root and generate the corresponding circuit to prove the correctness of the new state root update.

EVM Proof: Ensure Execution of Correct Calculations

In the process of State proof, the data needed for the EVM circuit has been stored in the shared bus mapping cache. As mentioned above, the EVM proof needs to ensure

1. the validity of the inputs, i.e., the data for its operation comes from bus mapping;
2. the correctness of the calculation of the arithmetic op, i.e., the input data satisfies the operational logic of Add, Mul, Sub, etc.

Take Add as an example. The pseudo-code is shown below, where va, vb, and vc refer to the addend, the augend, and the sum.

Before checking whether va, vb, and vc satisfy the operational logic of addition, we need to make sure that they are from bus mapping and satisfy the 8-bit rang proof to ensure the data is valid.

Summary

As shown in Figure 1, we have designed several circuits. If the proof of each circuit is placed in L1 for verification, the cost of verification will be very high. However, we can use Aggregative proof to aggregate multiple Proofs together. Only one pairing is required on the chain to verify the validity of all proofs.

This article describes how zkEVM works. Meanwhile, there are still details that are not involved, which require further research. As our design of zkEVM is in an early stage, we sincerely hope to receive suggestions/opinions from industry professionals to accomplish this task.