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

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

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

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

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

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

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

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

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

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

• 　　Gas 消耗计算正确

• 　　程序终止是否正确

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