foreword

foreword

The Ethereum Virtual Machine is a code operating environment built on the Ethereum blockchain. The contract code can be completely isolated from the outside and run inside the EVM. Its main function is to process smart contracts in the Ethereum system. The reason why Ethereum is Turing complete is that developers can use the Solidity language to create applications that run on the EVM, and all computable problems can be calculated. But Turing completeness is not enough. People also try to encapsulate EVM in the ZK proof system, but the problem is that there will be a lot of redundancy when encapsulating. The "small table mode" zkEVM invented by Fox will not only ensure that native Solidity Ethereum developers can seamlessly migrate to zkEVM, but also greatly reduce the redundant cost of encapsulating EVM into the ZK proof system.

EVM is undergoing an epic ZK transformation since its inception in 2015. This major transformation has two main directions.

The first direction is the so-called zkVM track. This track project is dedicated to improving the performance of the Application to the optimum, and the compatibility with the Ethereum virtual machine is not the primary consideration. There are two sub-directions here. One is to make your own DSL (Domain Specific Language). For example, StarkWare is committed to promoting the Cairo language, which is not easy to promote. The second is that the goal is compatible with existing relatively mature languages, such as RISC Zero is committed to making zkVM compatible with C++/Rust. The difficulty of this track is that the constraints on the final output are more complicated due to the introduction of the instruction set ISA.

The second direction is the so-called zkEVM track. This track project is dedicated to the compatibility of EVM Bytecode, that is, EVM codes at the Bytecode level and above all generate corresponding zero-knowledge proofs through ZkEVM, so that native Solidity Ethereum developers It will be possible to migrate to zkEVM at no cost. The players on this track mainly include Polygon zkEVM, Scroll, Taiko and Fox. The difficulty of this track is that it is compatible with the redundant cost of EVM, which is not suitable for encapsulation in the ZK proof system. After a long period of thinking and argumentation, Fox finally found the key to fundamentally reduce the huge redundancy of the first generation zkEVM: "small table mode" zkEVM.

Data and proof circuits are the two core elements of zkEVM to generate proofs. On the one hand, in zkEVM, the prover needs all the data involved in the transaction to prove that the state transfer brought about by the transaction is correct, while the data in EVM is large and complex. Therefore, how to organize and organize the data required for the proof is a problem that needs to be carefully considered to build an efficient zkEVM. On the other hand, how to efficiently prove (or verify) the validity and correctness of calculation execution through a series of circuit constraints is the basis for ensuring the security of zkEVM.

image description

Figure 1: Two generations of zkEVM solutions for large tables and small tables

For example, we put together each change of elements in the stack, specially write a stack circuit proof, write a set of arithmetic circuits for pure arithmetic operations, and so on. In this way, the situations that each circuit needs to consider become relatively simple. These circuits with different functions have different names in different zkEVMs. Some people call them circuits directly, while others call them (sub)state machines, but the essence of the idea is the same.

In order to explain the meaning of doing this more clearly, let's give an example, assuming that we want to prove the addition operation (take out the upper 2 elements of the stack, and put their sum back to the top of the stack):

Suppose the original stack is [ 1, 3, 5, 4, 2 ]

Then if we do not classify and split, we need to try to prove that after the above operations, the stack becomes [ 1, 3, 5, 6 ]

And if the classification is split, we only need to prove the following things separately:

stack circuit:

C 1 : Prove that [ 1, 3, 5, 4, 2 ] pops 2 and 4 and becomes [ 1, 3, 5 ]

C 2 : Prove that [ 1, 3, 5 ] becomes [ 1, 3, 5, 6 ] after push( 6)

Arithmetic circuit:

C 3 ：a= 2, b= 4,c= 6 , prove that a+b=c

image description

Figure 2: The large table model adopted by the first generation of zkEVM

Once the classification is split, the situation of each part will become relatively simple, so the difficulty of proof will be significantly reduced.

But classification and splitting will also bring about other problems, that is, the data consistency problem of different types of circuits. For example, in the above example, we actually need to prove the following two things:

C 4 : "the number popped in C 1" = "a and b in C 3"

C 5 : "Number of pushes in C 2" = "c in C 3"

In order to solve this problem, we return to the first question, that is, how do we organize the data involved in the transaction, and we will discuss this topic next:

An intuitive method is this: through trace, we can disassemble each step involved in all transactions, know the data involved, and send a request to the node to obtain the part of the data that is not in the trace, and then we will It is arranged into a large table T as follows:

"First step operation" "Data involved in the first step operation"

"Second step operation" "Data involved in the second step operation"

..."operation nth" "data involved in operation nth"

So, in the above example, we would have a line that records

"step k: addition" "a= 2, b= 4, c= 6 "

And the above C 4 can be proved as follows:

C 4(a): The number popped by C 1 is consistent with the kth step in the large table T

C 4(a): a and b of C 3 are consistent with step k in big table T

image description

Figure 3: The "small table mode" zkEVM invented by Fox

We consider the following series of table constructions:

Form Ta:

"first operation of type a" "data involved in the first operation of type a"

"second operation of type a" "data involved in the second operation of type a"

..."the mth operation of type a" "the data involved in the mth operation of type a"

Form Tb:

"first operation of type b" "data involved in the first operation of type b"

"second operation of type b" "data involved in second operation of type b"

..."the mth operation of type b" "the data involved in the nth operation of type b"

…Construct multiple small tables in this way. The advantage of doing so is that we can directly perform lookup in the corresponding small tables according to the type of operation involved in the required data. In this way, the efficiency can be greatly improved.

A simple example (assuming we can only lookup one element at a time) is that if we want to prove that the 8 letters a~h exist in [a, b, c, d, e, f, g, h], we need Perform 8 lookups on a table of size 8, but if we divide the table into [a, b, c, d] and [e, f, g, h], we only need to It is enough to perform 4 lookups on the tables respectively!

in conclusion

in conclusion

The "small table mode" zkEVM invented by Fox not only ensures that native Solidity Ethereum developers can migrate to zkEVM at no cost, but also greatly reduces the redundant cost of encapsulating EVM into the ZK proof system. This is a major change in the structure of zkEVM, which will have a profound impact on Ethereum's expansion plan.