通过上一篇,我们知道zkEVM包含多个电路,如EVM circuit, MPT circuit,Keccak256 circuit等。本节继续介绍EVM circuit部分,这一部分是典型的业务电路,用于约束EVM执行状态,因为其他例如 Keccak256 circuit 是通用型的电路,不仅可以用在ZKEVM工程中,也可以用在其他使用Keccak256做哈希的应用中,也就是独立于业务逻辑本身的电路组件。
通过上一篇,我们知道zkEVM包含多个电路,如EVM circuit, MPT circuit,Keccak256 circuit等。本节继续介绍EVM circuit部分,这一部分是典型的业务电路,用于约束EVM执行状态,因为其他例如 Keccak256 circuit 是通用型的电路,不仅可以用在ZKEVM工程中,也可以用在其他使用Keccak256做哈希的应用中,也就是独立于业务逻辑本身的电路组件。
EVM circuit遍历block证明中包含的交易,以验证交易的每个执行步骤是否有效。基本上,一个步骤的规模与EVM中的规模相似(可以理解为大部分op code 电路约束可以具有相同的上限复杂度),因此通常我们每个步骤处理一个操作码(EVM中的op code),除了像SHA3或CALLDATACOPY/Log这样的操作码,它们具有可变大小的输入上,这需要多个“虚拟”步骤(virtual step:辅助的操作码,并不是evm真正存在的op code)。
为了验证一个步骤执行是否有效,首先需要在EVM中枚举一个步骤的所有可能执行结果,包括成功和错误情况,然后构建一个自定义约束来验证每个执行结果的转换是否正确。
对于每个步骤,我们使用其中一个执行结果来约束它,特别地,约束第一步是BEGIN_TX(这就是上面提到到virtual step
的一种,标记一个交易开始执行),然后进入交易内部的step,以验证完整的执行。此外,每一步都可以访问下一步,通过设置诸如assert next之类的约束来传播跟踪信息。例如程序计数器执行一个步骤后就要加1:next.program_counter == curr.program_counter + 1
.
对于如何定义执行结果,直观的的做法是将每个操作码作为一个步骤的一个分可能的分支。然而,EVM有非常多的操作码(op ocode),其中一些非常相似,比如{ADD,SUB},{PUSH},{DUP}和 {SWAP*},它们似乎完全是是通过相同的约束来处理的,只需稍加调整(交换一个值或线性变动),我们可以只实现一次来批量处理这些非常相似的op codes,这样就可以在单个执行结果(分支)中处理多个操作码。
此外,EVM状态转换还可能包含多种错误情况,我们还需要实现这些约束。每个操作码分支都要处理自己的错误情况,这很麻烦,因为它需要停止步骤并将执行上下文返回给调用者。虽然说EVM的error 对于EVM执行来说是异常的情况(比如OutOfGas,NotSufficientBalance,ExceedMaxCodeSize 等等),但这些是业务层面来看的, 对于从电路角度来说,它和正常执行结果一样重要,电路只知道有什么情况就要去约束,保证其反映真实的业务过程!
幸运的是,大多数错误情况都容易通过一些预先构建的Lookup talbe进行验证,即使它们可能发生在许多操作码上,但也有一些棘手的错误需要逐一验证,例如Gas不足,stack溢出等。因此,我们进一步将各种错误请阔也做为执行结果来看待。
因此,我们可以列举所有可能的执行结果,并将EVM电路转化为有限状态机,如:
GethExecStep
和 opcodes
一一对应,把单个op code(Call, CREATE2)作为一个step使用GethExecStep的N-1映射,即多个op code共用一个step 。例如{ADD,SUB},{PUSH},{DUP}和{SWAP*}。就是前面提到的非常相似的op codes,但只实现一次
ExecSubStep: 需要使用多个Step表示一个op code, 通常需要处理变长输入的情况,如:
ExplicitReturn: 无异常执行情况下返回
在EVM中,解释器(interpreter)能够对数据块上下文、帐户余额、堆栈和当前范围内的内存等进行任意随机访问。访问可以是读写的,也可以是只读的。 在EVM电路中,我们使用Lookup工具,将这些随机数据访问复制到不同布局中的其他电路,并验证它们的一致性和有效性。在验证了这些随机数据访问之后,我们可以像使用表一样使用它们。上一篇列出了各个电路中使用的table。
对于读写访问数据,EVM电路使用顺序rw_counter(读写计数器)查找状态电路(state circuit),以确保读写访问按时间顺序进行。它还使用一个标志is_write
来检查不同写访问之间的数据一致性。
对于只读访问数据,EVM电路直接查找 Bytecode circuit, Tx circuit and Call circuit.
在EVM中,如果任何调用失败,写入state中的数据会被回滚。
在EVM电路中,每个调用都附加一个标志(is_persistent
),以标志它是否成功。有两类可回滚的数据写入:
因此,理想情况下,我们只需要对第一种情况进行回滚约束检查,如下列类型数据:
第二种情况,它们不会影响未来执行,我们只在is_persistent
为1时写入它们:
为了实现写数据的回滚,同时需要一些额外的调用的信息:
is_persistent
——标记是否成功。
rw_counter_end_of_reversion
——标记应该在未来的哪一点回滚。
reversible_write_counter
--标记到目前为止我们已经进行了多少次可回滚写入。
然后在每次可回滚写入时,我们首先检查is_persistent
是否为0,如果是,我们在rw_counter_end_of_reversion
进行额外的可逆写入rw_counter_end_of_reversion - reversible_write_counter
处的旧值,以相反的顺序还原可逆回滚
在EVM电路中,有3种操作码源头:
如果查询的索引不在给定有效范围内,它会遵循当前EVM的行为隐式返回0, 例如字节码序列有100长度,查询102处字节,会返回0,0对应了STOP
op code.
EVM可以通过op code(Call, CREATE等)执行内部调用。在EVM电路中,触发内部调用的操作码(如CALL或CREATE)将:
需要注意的是,对于操作码(如RETURN或REVERT)的错误情况将恢复到上一个Caller的状态,并将其设置回下一步上下文。
简单调用示例(隐藏了许多细节)如下:
本文主要是开源的社区文档的翻译,略作修改。文中很多annotation来自EVM源代码。尤其是与EVM call及回滚相关的复杂逻辑,熟悉以太坊源代码会增进理解。
原文:https://appliedzkp.github.io/zkevm-docs/architecture/evm-circuit.html#introduction
感谢关注, 欢迎讨论!!!
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!