ZKP — zkEVM

It is well known that zkRollup has the highest security level amongst all Rollup solutions; however, currently zkRollup does not support programmability, not to mention composability. zkEVM utilizes zk-SNARK technology to execute EVM in order to prove. zkRollup supports zkEVM, and it is compatible EVM smart contract at L2. As of now a couple of teams are working on implementation of zkEVM. Besides AppliedZKP who published some details on circuit design, no on ther teams have published related documentations. Here are some public documentations on zkEVM from AppliedZKP:

https://github.com/appliedzkp/zkevm-specs

https://hackmd.io/Hy_nqH4yTOmjjS9nbOArgw

This article will analyze zkEVM design from AppliedZKP team. Therefore, note that the zkEVM mentioned here refers specifically to AppliedZKP’s zkEVM solution.

Background

In order for Etherem to ensure the correctness of every transaction, each block needs to have a corresponding transaction. That is also to say, each node requires proving entire transaction history and executing validation on every transaction. zkEVM uses Zero-Knowledge Proof technology (zk-SNARK) for the validation:

• For each smart contract transaction execution, generate transaction proof. Implementing zkRollup on L2 supports programmability.
• For every block in Etherem, generate block proof.

These proofs are made up with two parts: State proof and EVM proof. During the execution process of each transaction, State includes Storage, Memory, and Stack status.

Bus-mapping is the fondamental methodology of the design. In a normal PC system structure, CPU visits storage (RAM/hard drive) via bus, which separates execution from storage logic. zkEVM builds upon the same structure methodology — the state change and order execution are separated, and proved by State proof and EVM proof accordingly.

State proof is in charge of the consistency and correctness of Bus Mapping. Consistency refers to the consistent Bus Mapping and State read/write. Correctness means the correctness of correct read/write status in Bus Mapping. EVM proof is in charge of the correct execution of EVM op code (if State op code is referred, make sure the executions regarding storage are correct.

It is almost like storage visiting bus exists between EVM Execution and storage: EVM Execution gets/saves related status required for execution through Bus Mapping. Utilizing Bus Mapping, we need to prove the correctness of the “Bus”execution between Bus Mapping State and EVM Execution. It breaks down to following steps in logic: read state, EVM execution(modifying state), write state. Bus Mapping includes both read and write of state.

Bus Mapping

Bus Mapping includes two kinds of state: reading the old state, and writing back the new state. No matter it is old or new, Bus Mapping has a “containment” relationship. This “containment” of mapping relationship can be proved by Plookup algorithm.

Storage state (Storage/Memory/Stack) is represented by key-value pairs. The binding relationship of Key-value pair can be implementd as a sequence:

def build_mapping():
   keys = [1,3,5]
   values = [2,4,6]
   randomness = hash(keys, values)
   
   mappings = []
​
   for key , value in zip(keys,values):
       mappings.append(key + randomness*value)
   return(mappings)

To prove a certain key-value pair exists in a set of key-value pairs, we can implement with 3 Plookup proofs:

def open_mapping(mappings, keys, values):
   randomness = hash(keys,values)
   index = 1
   # Prover can chose any mapping, key , value
   mapping = plookup(mappings)
   key = plookup(keys)
   value = plookup(values)
   # But it has to satisfy this check
   require(mappings[index] == key[index] + randomness*value[index])
   # with overwhelming probability will not find an invalid mapping.

keys and values are State related pairs. mappings is an array of all journey mapping key-value pairs. With 3 Plookup proofs:

1/ there exists one key of mapping in keys

2/ there exists one value of mapping in values

3/ there exists one mapping in mappings

At the same time, mapping and key-value pair should satisfy the relationship established by build_mapping. All of the above would be adequate to prove that certain key-value pair is a part of mapping of keys and values.

Based on these, we can define the bus_mapping data structure:

bus_mapping[global_counter] = {
   mem: [op, key, value], 
   stack: [op, index, value],
   storage: [op, key, value],
   index: opcode,
   call_id: call_id,
   prog_counter: prog_counter
}

global_counter is the index of slot. slot is the smallest unit of a proof logic. One transaction is made up with multiple commands, and each command may be made up with multiple slots. op is operation type, by logic it is composed of reading and writing. prog_counter is pc. All readings of bus_mapping can be checked whether it “belongs” to current through plookup. Reading state requires the consistency with old state, and the write state also needs to be consistent with the saving state post-update.

Based on Bus mapping, we use State Proof and EVM Proof for correctness of read/write of data, and its consistency with opcode semantics.

State Proof

State Proof proves that “saving” related read/write is consistent with Bus Mapping data, which is the consistency with the read/write data on bus. State Proof has 3 types of proofs based on storage type.

Storage

Listed below are Storage related op code:

There are two types of op code: Storage read, and Storage write. For instance, SLOAD reads data to Stack from Storage. Storage related op code corresponds to read/write data in Bus mapping. Note that in State Proof, Storage proof only proves whether Storage related read and write operations exist in bus mapping. As for semantic information, it is proved via EVM proof.

Memory

From the State Proof prespective, all RAM operations are ordered by index. index is the RAM address. As an example:

Address 0 and Address 1 related RAM operations are listed together. Each RAM address initializes to 0 at the beginning of procedure execution. That is to say, when global_counter is eqaul to 0, index 0/1 resets to 0. From Bus Mapping perspective, these RAM operations are listed below:

Read/write data at each address needs to be consistent. Such consistency is checked by the following constraint:

The blue part limits RAM to read/write only, while the brown part limits each address RAM initializes to 0 and be consistent with read/write data. The orange part limits related RAM operations to happen only in bus mapping.

Stack

Stack has 3 functions: Push/Pop, Dup and Swap. It is implemented with an array of 1024 size. Check on ck position info is done by EVM proof, while Stackdata and relationship with bus mapping is done by Stack proof. The fondamental theory follows similar fashion of Memory.

EVM Proof

EVM Proof is the core logic of EVM executing relative constraints. EVM proof requires floowing logic to be proved:

1/ EVM execution code is appointed transaction code logic

2/ correctness of storage related semantics, such as Stack location management, consistency of SLoad data and Stack data, etc.

3/ correctness of calculation related semantics, such as the arithmetic calculation.

4/ correctness of the jump logic, such as the Call command

5/ correctness of Gas consumption calculation

6/ if the procedure is terminated appropriately

Slot is the basic unit of a circuit. Multiple Slots can combine together to implement an op code semantic.

Arithmetic calculation

Take addition as an example, the 8bit integers addition can be proved with Plookup. Through multiple 8bit additions and carry-over, addition of any length can be implemented.

The comparison between two integers has very similar implementation logic.

Jump Logic

call_id records an execution environment. To bind the relationship with jump logic, call_id takes following claculation 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 stands for random linear combination.

EVM proof logic is relatively complicated. Not much documentation available currently on the design details. zkEVM offers documentation of an overall logic yet details can still be refined in the future.

Conclusion:

AppliedZKP published the design document of zkEVM. zkEVM takes advantage of the Bus Mapping methodology, which seperates the Storage and Execution logic. Bus Mapping based on extracting the correct storage data, uses State proof for consistency of data, and EVM proof for correctness of execution logic.