众所周知，zkRollup是L2中安全等级最高的Rollup方案，但是zkRollup目前没有可编程性，更无从谈起可组合性。zkEVM是用zk-SNARK技术将EVM的执行进行证明。zkRollup支持了zkEVM，在L2就能支持兼容EVM的智能合约。目前有几个团队都在研究zkEVM的实现。除了AppliedZKP公开了一些电路设计的思路和细节外，其他团队都没有详细的资料。AppliedZKP有关zkEVM的设计资料如下：

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

https://hackmd.io/Hy_nqH4yTOmjjS9nbOArgw

本文详细分析AppliedZKP构想的zkEVM设计。本文中提到的zkEVM专指AppliedZKP提出的zkEVM方案。

以太坊的每一个节点为了确保交易的正确性，需要针对每一个区块中的每一笔交易执行。也就是说，每一个节点需要验证以太坊的整个交易历史，并且要一笔笔的进行执行验证。zkEVM利用零知识证明技术（zk-SNARK）证明：

• 针对智能合约的交易执行，生成交易证明。在L2实现zkRollup支持可编程性。

• 针对以太坊的每一个区块，生成区块证明。

这些证明都由两部分组成：State proof（状态证明）和EVM proof（EVM执行证明）。在一条交易执行过程中，State包括Storage，Memory以及Stack的状态。

Bus-mapping是设计的基础思想。一般的PC体系结构中，CPU通过总线访问存储（内存/硬盘），也就是计算和存储分开。zkEVM采用的同样的架构思想，状态的变化和指令的执行分开，并且分别由State proof和EVM proof进行证明。

State proof负责Bus Mapping信息的一致性和正确性。一致性指的Bus Mapping和State之间的读写一致。正确性指的是Bus Mapping中的读写状态正确。EVM proof负责EVM的op code的执行正确（如果涉及到State的op code，保证存储相关的操作正确）。

EVM Execution和存储之间好像有一条存储访问的总线一样：EVM Execution通过Bus Mapping获取或者存储执行需要的相关状态。采用Bus Mapping的方式，需要证明Bus Mapping和State以及EVM Execution之间的“总线”操作的正确性。逻辑上分成如下的几步：读取状态，EVM执行（修改状态），写回状态。Bus Mapping包括了读取以及写回状态。

Bus Mapping包括了两种状态，一种是读取老的状态，一种是写回生成新的状态。无论是老的状态和新的状态，Bus Mapping都是“包含”关系。这种“包含”的mapping关系可以通过Plookup算法证明。

存储状态（Storage/Memory/Stack），采用key-value的格式进行表示。key-value对的绑定关系可以实现为一个序列：

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)

想证明某个key-value对在一些key-value中，可以通过三个Plookup证明实现：

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和values是State相关的key-value对。mappings是所有key-value对行程的mapping数组。通过三个Plookup证明：

1/ 某个mapping的key在keys中

2/ 某个mapping的value在values中

3/ 某个mapping在mappings中

并且mapping和key-value满足build_mapping建立的关系。如上的这些证明，能够证明某个key-value对是keys和values的mapping中的部分。

在如上的基础上，可以定义出bus_mapping的数据结构：

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是slot的编号。slot是一个证明逻辑的最小单元。一个交易的证明由多条指令组成，每个指令可能由多个slot组成。op是操作类型，逻辑上由读和写组成。prog_counter是pc。所有的bus_mapping中的读取操作可以通过plookup确定是不是“属于”当前的State。读取状态需要和老的存储状态一致，写入状态需要和更新后的存储状态一致。

在Bus mapping的基础上，采用State Proof和EVM Proof证明数据的读写正确以及和opcode的语义一致。

State Proof证明了和“存储”相关的读写和Bus Mapping的数据一致。也就是在“总线”上的读写数据的一致性。State Proof根据存储类型分成三种证明。

Storage

和Storage相关的op code罗列如下：

相关的op code分为两种，一种是Storage读，一种是Storage写。比如SLOAD就是从Storage读取数据到Stack中。Storage相关的op code对应的读写数据在Bus mapping中。注意，State Proof中的Storage证明只单纯证明Storage相关的读写操作是否在bus mapping中。至于读写数据的语义信息是通过EVM proof进行证明的。

Memory

从State Proof证明的角度看，所有的内存操作按照index进行排序。index是内存地址。举个例子：

地址0和地址1的相关内存操作罗列在一起。每个内存地址在程序开始执行时会初始化为0。也就是global_counter为零时，index 0/1初始为0。从Bus Mapping的角度看，这些内存操作如下：

对于每个地址上的读写数据都需要保持一致性。这些一致性由如下的约束检查：

蓝色部分限制内存只有读写操作，褐色部分限制每个地址内存初始为零，并且读写数据一致，橘黄色部分限制相关的内存操作在bus mapping中。

Stack

Stack的操作主要分为三类：Push/Pop，Dup和Swap。用1024大小的数组模拟Stack实现。Stack的位置信息的检查由EVM proof完成。Stack的数据和bus mapping的关系由Stack proof完成。基本思路和Memory一致。

EVM Proof是EVM执行相关约束的核心。EVM proof需要证明如下的一些逻辑：

1/ EVM执行的代码是指定的transaction的代码逻辑

2/ 和存储相关的语义是否正确，比如Stack的位置管理，SLoad数据和Stack的数据是否一致等等

3/ 和计算相关的语义是否正确，比如算术计算等等

4/ 跳转逻辑是否正确，比如Call指令

5/ Gas消耗计算正确

6/ 程序终止是否正确

Slot是电路的基本单元。多个Slot可以组合在一起实现一个op code的语义。

算术计算

以加法为例，通过Plookup可以证明8bit整数的计算。通过多个8bit的加法以及进位，可以实现任意长度的加法。

两个数的比较的实现原理和加法类似。

跳转逻辑

call_id记录一个执行环境。为了绑定和跳转逻辑的关系，call_id采用如下的计算逻辑：

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是random linear combination。

EVM proof的逻辑相对来说比较复杂。当前公布的文档没有展开描述设计的细节。zkEVM给出了大致的设计思路，细节的部分还需要进一步细化。

总结：

AppliedZKP公开了zkEVM的设计思路。zkEVM采用数据总线（Bus Mapping）的思路，将存储和计算分开。在Bus Mapping抽取了正确的存储数据的基础上，State proof证明数据的一致性，EVM proof证明计算逻辑的正确性。