Read zkEVM from a code perspective
Zero Knowledge Proof -- Interpretation of zkEVM
Original author: Star Li, Star Idea
As we all know, zkRollup is the Rollup scheme with the highest security level in L2, but zkRollup has no programmability at present, let alone combinability. ZkEVM uses ZK-SNARK technology to prove the EVM execution. ZkRollup supports zkEVM and supports EVM-compatible smart contracts in L2. Several teams are currently working on zkEVM implementations. Other than AppliedZKP, which shared some of the circuit design ideas and details, no other team has detailed information. AppliedZKP design materials for zkEVM are as follows:
https://github.com/appliedzkp/zkevm-specs
https://hackmd.io/Hy_nqH4yTOmjjS9nbOArgw
This paper analyzes the zkEVM design conceived by AppliedZKP in detail. ZkEVM mentioned in this article refers specifically to the zkEVM solution proposed by AppliedZKP.
01 background
Each node in Ethereum needs to execute for each transaction in each block in order to ensure that the transaction is correct. That is, each node needs to validate the entire transaction history of Ethereum, and perform the validation one by one. ZkEVM uses zero-knowledge proof technology (ZK-SNARK) to prove:
· Generate transaction certificates for the execution of smart contracts. Implementation of zkRollup in L2 supports programmability.
· Generate block proof for each ethereum block.
These proofs are made up of two parts: State proof and EVM proof. State includes Storage, Memory, and Stack states during a transaction.
Bus- Mapping is the basic idea of the design. In a typical PC architecture, the CPU accesses storage (memory/hard disk) through the bus, which means computing and storage are separated. ZkEVM adopts the same architectural idea, the change of State is separated from the execution of instructions, and is proved by State proof and EVM proof respectively.
State proof is responsible for the consistency and correctness of Bus Mapping information. Consistency refers to the consistency of read and write between Bus Mapping and State. Correctness indicates that the read and write status of the Bus Mapping is correct. EVM Proof is responsible for the correct execution of EVM's OP code (if State's OP code is involved, ensure that storage-related operations are correct).
EVM Execution and storage are like a Bus for storing access: EVM Execution retrieves or stores the relevant state required for Execution through Bus Mapping. In Bus Mapping, you need to prove the correctness of the "Bus" operation between Bus Mapping and State and EVM Execution. Logically there are several steps: read state, EVM execution (modify state), and write state. Bus Mapping includes reading and writing state.
02 Bus Mapping
Bus Mapping includes two states. One is to read the old state, and the other is to write back to generate the new state. Regardless of the old state or the new state, Bus Mapping is an "contain" relationship. This "contained" mapping can be proved by Plookup algorithm.
Storage status (Storage, Memory, and Stack) is expressed in the key-value format. The key-value pair binding can be implemented as a sequence:
To prove a key-value pair in some key-values, there are three Plookup proofs:
Keys and values are state-related key-value pairs. Mappings are a mapping array of all key-value pairs. Prove by three Plookup:
1/ The key of a mapping is in the keys
2/ The value of a mapping is in values
3/ A mapping is in mappings
And mapping and key-value satisfy the relationship established by build_mapping. These proofs prove that a key-value pair is part of a mapping of keys and values.
Based on the above, you can define the data structure of bus_mapping:
Global_counter is the slot ID. Slot is the smallest unit of proof logic. A proof of a transaction consists of multiple instructions, each of which may consist of multiple slots. Op is an operation type that logically consists of read and write. Prog_counter is PC. All read operations in bus_mapping can be determined by plookup if they "belong" to the current State. The read status must be the same as the old storage status, and the write status must be the same as the updated storage status.
On the basis of Bus Mapping, State Proof and EVM Proof are used to prove that data reading and writing is correct and the semantics are consistent with Opcode.
03 State Proof
State Proof proves that read/write and Bus Mapping data related to "storage" are consistent. This is the consistency of read and write data across the bus. State Proof is divided into three types of Proof based on storage type.
Storage
Op codes related to Storage are listed as follows:
The associated op code is divided into two types, one is Storage read, one is Storage write. For example, SLOAD reads data from the Storage into the Stack. The read/write data of the OP code related to the Storage is displayed in the Bus Mapping. Note that the Storage Proof in State Proof only proves whether storage-related read/write operations are performed in bus Mapping. Semantic information about read and write data is proved by EVM proof.
Memory
From the point of view of State Proof, all memory operations are sorted by index. Index is the memory address. Here's an example:
The memory operations for address 0 and address 1 are listed together. Each memory address is initialized to 0 when the program starts execution. If global_counter is zero, index 0/1 will start as zero. From the Bus Mapping perspective, these memory operations are as follows:
Consistency is required for read and write data at each address. These conformance are checked by the following constraints:
In the blue part, only read/write operations are allowed. In the brown part, the memory for each address is initially zero and the read/write data is consistent. In the orange part, related memory operations are restricted in the bus Mapping.
Stack
Stack operations are divided into three categories: Push/Pop, Dup, and Swap. Simulate the Stack implementation with a 1024 size array. The Stack location information is checked by EVM Proof. The relationship between Stack data and bus mapping is completed by Stack Proof. The basic idea is the same as Memory.
04 EVM Proof
EVM Proof is the core of EVM to enforce relevant constraints. EVM proof needs to prove the following logic:
The code executed by 1/ EVM is the code logic for the specified transaction
2/ Whether the semantics related to storage are correct, such as Stack location management, SLoad data and Stack data consistency, etc
3/ Whether the semantics related to computation are correct, such as arithmetic computation, etc
4/ Whether the jump logic is correct, such as the Call instruction
5/ Gas consumption calculated correctly
6/ Is the program terminated correctly
Slot is the basic unit of a circuit. Multiple slots can be combined to implement the semantics of an OP code.
Arithmetic calculation
Taking addition as an example, it is possible to prove the calculation of 8-bit integers through Plookup. Arbitrary length of addition can be achieved through multiple 8bit addition and carry.
The comparison of two numbers works similarly to addition.
Jump logic
Call_id Records an execution environment. To bind to the jump logic, call_id uses the following calculation logic:
call_id -> rlc(calldata_callid, call_data_start_addr, call_data_size, return_data_callid,return_data_start_addr, return_data_size, origin, caller, call_value, call_stack_depth)
RLC is random Linear combination.
EVM Proof's logic is relatively complex. Currently published documentation does not expand to describe the design in detail. ZkEVM gives the general design idea, and the details need to be further refined.
conclusion
AppliedZKP discloses the design ideas for zkEVM. ZkEVM uses Bus Mapping to separate storage and computing. Based on the correct storage data extracted by Bus Mapping, State proof proves the consistency of data, and EVM proof proves the correctness of calculation logic.
Welcome to join the official BlockBeats community:
Telegram Subscription Group: https://t.me/theblockbeats
Telegram Discussion Group: https://t.me/BlockBeats_App
Official Twitter Account: https://twitter.com/BlockBeatsAsia
Related Articles
