摘要:众所周知,zkRollup是L2中安全等级最高的Rollup方案,但是zkRollup目前没有可编程性,更无从谈起可组合性。zkEVM是用zk-SNARK技术将EVM的执行进行证明。zkRollup支持了zkEVM,在L2就能支持兼容EVM的智能合约。目前有几个团队都在研究zkEVM的实现。除了Ap ...

众所周知,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方案。


01
背景


以太坊的每一个节点为了确保交易的正确性,需要针对每一个区块中的每一笔交易执行。也就是说,每一个节点需要验证以太坊的整个交易历史,并且要一笔笔的进行执行验证。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包括了读取以及写回状态。


02
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的语义一致。


03
State Proof


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一致。


04
EVM Proof


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证明计算逻辑的正确性。


更新日期:
文章标签: ,
文章链接: [Star Li]零知识证明 – zkEVM解读  [复制链接]
站方声明: 比推所有文章都只代表作者观点,不构成投资建议。投资有风险,后果自负。