ZKEVM

[TOC]

链接

• 状态证明探索：https://hackmd.io/Nwd0e5AgTVSBWRQlp-Ving
• 状态电路规范：https://hackmd.io/oJT1kJjvQYWQlKZ1JEtmMQ
• 电路实现：https://github.com/appliedzkp/zkevm-circuits
• 测试向量：https://github.com/appliedzkp/zkevm-testing-vectors

介绍

目前，以太坊上的每个节点都必须验证以太坊虚拟机中的每笔交易。这意味着每笔交易都会增加每个人验证以太坊历史所需的工作量。更糟糕的是，每笔交易都需要由每个新节点验证。这意味着新节点同步网络所需的工作量在不断增长。我们希望为以太坊区块构建有效性证明以避免这种情况。

1. 创建一个支持智能合约的 zkrollup
2. 为每个以太坊区块创建一个有效性证明

这意味着为 EVM + 状态读取/写入 + 签名创建一个有效性证明。

为了简化，我们将证明分为两个部分。

1. 状态证明：状态/内存/堆栈操作已正确执行。这不会检查是否已读取/写入正确的位置。我们允许我们的证明者在此处选择任何位置，并在 EVM 证明中确认它是正确的。
2. EVM 证明：这会检查是否在正确的时间调用了正确的 opcode。它检查这些 opcode 的有效性。它还会确认对于每个这些 opcode，状态证明都执行了正确的操作。

只有在验证了两个证明之后，我们才能确信该以太坊区块已正确执行。

TODO：这两个电路如何连接的高级描述，即它们消耗相同的总线映射 [name=ying tong]

术语

L1 合约 ：是在以太坊主网上部署的合约。

zkevm 验证器 ：是验证 zkevm 证明的 L1 合约。

L2 合约 ：是部署在我们的 zkrollup 内部的合约，即它使用 zkevm 验证器来证明调用该智能合约的交易是正确的。

`l1tx` ：是用户发送的用于与 L1 合约交互的交易。

`l2tx` ：是用户发送的用于部署或与 L2 合约交互的交易

协调者 ：为以太坊区块生成有效性证明的一方。协调者从用户那里接收 `l2tx`，验证它们，生成见证和证明，并将其发送给 zkevm 验证器。他们使用 `l1tx` 向 zkevm 验证器提供这些证明。

用户 ：部署和/或与部署在 l2 上的智能合约交互的一方

Opcodes ：EVM 操作码

[name=barryWhiteHat] 如果我们可以使用自定义约束条件，则可能会删除 slot

Slot (槽) ：这是我们分配的用于证明每个 EVM opcode 有效性的约束数量。例如，我们可以有一个包含 100 个约束的 slot。这意味着我们将使用 100 个约束来证明 Mul opcode，但也包括 Add、Jump、Sload。每个 opcode 的成本为 100 个约束，即使它使用的约束少于 100 个。

自我提醒：“slot”=“行数” [name=ying tong]

[name=barryWhiteHat] 由于每个 opcode 都是多个 slot，因此可能会删除 multislot opcodes 的表示法。

MultiSlot opcodes (多槽操作码) ：某些 opcode 可以使用多个 slot。这意味着我们只是增加 `slot_counter`，而不增加程序计数器。

是否每个 opcode 都使用一个 slot，并且每个 slot 使用可变数量的行？ [name=ying tong] 我认为不是。在我看来，Slot 是一组用于实现固定功能的约束。对于正常的 opcode，一个 Slot 就足够了。对于复杂的 opcode，应该组合更多的 slot。 [name=Star.LI]

Program Counter (程序计数器) ：要在 EVM 中执行的当前 opcode 的位置。这会在每个 opcode 之后更新；在 $\texttt{JUMP}$ 的情况下，它设置为 $\texttt{JUMP}$ 的位置。对于每个新的合约调用，它都初始化为零。

Slot Counter (槽计数器) ：对于 multislot opcode，我们使用 slot 计数器来跟踪已执行了多少次执行。这会在每个 slot 之后递增。此变量用于跟踪 multislot opcode 何时终止。

Global Counter (全局计数器) ：对于每个 opcode 都会递增的计数器。

准确地说，全局计数器是否计算读取和写入的次数？ [name=ying tong] 是的，但它也用于区分你在 multi slot opcode 中的位置。对于调用数据复制，你可以使用全局计数器在该步骤中移动到下一步。 我觉得全局计数器非常重要，并且在许多地方用于保证许多事情。 我们在关于安全性的论证中使用了它 https://hackmd.io/Hy\_nqH4yTOmjjS9nbOArgw#Proof [name=barryWhiteHat]

Bus Mapping (总线映射) ：在传统的计算机中，总线用于将数据从内存和存储传输到 CPU。在这里，我们重用该范例将数据从我们的状态证明传输到我们的 EVM 证明。

变量

TODO：类型 [name=ying tong]

bus_mapping

与传统计算机中的总线类似，`bus_mapping` 用于将信息从存储、内存和堆栈操作传输到 EVM 证明。

global_counter

一个全局计数器，对于 EVM 证明的每个 slot 都会递增。

call_id

我们当前正在执行的交易/单独调用上下文的 ID

program_counter

是要验证的 opcode 的 `program_index` 的值。

program_index

L2 合约的字节码中 opcode 的位置。

mem

一个内存键值映射，从 `global_counter` -> `index` -> `value`

memory_op

定义此内存操作的类型。例如，0 是读取，1 是写入。

Storage (存储)

用于存储读取/写入的键值映射。`global_counter` -> `index` -> `value`

storage_op

定义要执行的存储操作的类型。

Stack (堆栈)

用于每个堆栈操作的键值映射。

stack_op

定义堆栈操作的类型

opcode

这是要执行的当前 opcode。

总线映射

构建用于验证 VM 的 snark 的一个巨大挑战是，你需要能够随时读取随机值/opcode。为此，我们使用键值映射。键值映射基本上是所有元素的随机线性组合

Plookup 键值映射

在 plookup 中，你可以按如下方式构建键值映射

``` python 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) ```

可以以 3 个 plookup 为代价打开它

``` python def open_mapping(mappings, keys, values): randomness = hash(keys,values) index = 1

证明者可以选择任何映射、键、值

mapping = plookup(mappings) key = plookup(keys) value = plookup(values)

但它必须满足此检查

require(mappings[index] == key[index] + randomness*value[index])

以压倒性的概率将找不到无效的映射。

```

总线映射

EVM 证明和状态证明都使用总线映射。

``` 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 } ```

总线映射由证明者见证。在 EVM 证明中，我们必须确保证明者没有包含额外的变量。为此，我们限制其在 L1 EVM 中的度数，然后检查 EVM 证明中的每个元素。

总线映射的承诺是状态证明和 EVM 证明的公共输入。

区块常量

一个区块有一堆常量，我们创建一个映射来支持这些常量。 对于每个这些 opcode，都可以在我们的 EVM 证明中查找此映射。

``` block = [blockhash, coinbase, timestamp, number, difficiulty, gaslimit, chainID] ```

[name=CPerezz] 如果任何区块常量需要在任何证明中用作公共输入，那么我认为它们都应该表示为标量，对吗？除了：`blockhash` 之外，所有元素都可以，因为 IIRC 的 repr 将不适合标量。 有什么想法吗？我们是否应该以不同的方式比较它，但将其保持在此格式中？使用不同的格式来存储该常量？

[name=barryWhiteHat] 不确定应该是哪个 这是由 l1 evm 创建并作为公共输入传递的 要么 这是作为证明者的见证变量传递并在证明中检查的 想要等待一些 gas 成本估算来找出

获取区块常量的 Opcodes

opcode	名称	描述
0x40	BLOCKHASH	获取 256 个最新完整区块之一的哈希 - 20
0x41	COINBASE	获取区块的受益人地址
0x42	TIMESTAMP	获取区块的时间戳
0x43	NUMBER	获取区块的编号
0x44	DIFFICULTY	获取区块的难度
0x45	GASLIMIT	获取区块的 gas 限制
0x46	CHAINID	返回当前链的 EIP-155 唯一标识符 (EIP1344)

区块详细信息

call_id

一个定义我们当前正在执行哪个调用的变量

call_stack_depth

我们的调用堆栈的当前深度，当前最大值为 1024 个调用

msg.sender

此合约的当前调用者

tx.origin

此交易的发起地址

storage_root_before

如果此调用/l2tx 恢复，我们需要能够撤消所有存储写入。我们存储 storage_root_before，以便我们可以轻松地执行此操作。

gas price

用户为 gas 支付的 gas 价格

gas

此程序拥有的 gas 量

状态证明

Slot (槽)

TODO：添加有关构成状态证明中的 slot 的约束的详细信息。

^ 例如，完成条件 [name=ying tong]

Storage (存储)

有各种各样的 opcode 会导致读取和写入存储。它们包括

Flag	Opcode	描述
0x54	SLOAD	读取变量
0x55	SSTORE	写入变量
0xf0	CREATE	部署合约
0x31	BALANCE	获取用户的余额
0xf1	CALL	调用另一个帐户
0xf2	CALLCODE	使用另一个帐户的代码消息呼叫此帐户
0xf4	DELEGATECALL	使用另一个帐户的代码消息呼叫此帐户并保留更改。
0xfa	STATICCALL	类似于调用，但更改不是持久的
0xfd	REVERT	停止执行并恢复存储更改
	获取当前存储根	使用它来强制执行静态调用和恢复

我们使用映射中的标志变量来定义在状态证明中正在检查这些 opcode 中的哪一个。

状态读取 opcode 将一个元素从存储复制到堆栈。

存储操作发生在状态证明中，并在 EVM 证明中验证。证明者能够在状态证明中选择他们想要的任何存储读取/写入。他们必须使用 `global_counter` 变量来提交已完成的读取和写入的顺序。

TODO：添加有关 merkle 证明的详细信息。

内存

内存操作在 EVM 证明和状态证明中以不同的顺序执行。在状态证明中，内存操作按 `index`（内存中的位置）排序，然后按 `global_counter` 排序。在 EVM 证明中，它们按 `global_counter` 排序检查。

我们让我们的证明者提交他们想要的任何内存读取/写入。我们将检查正确的操作是否在正确的 `global_counter` 执行，并将其推迟到我们的 EVM 证明。

内存读取/写入

index	global_counter	value	memory_flag	评论
0	0	0	1	在 0 处初始化
0	12	12	1	写入 12
0	24	12	0	读取 12
1	0	0	1	在 0 处初始化
1	17	32	1	写入 32
1	89	32	0	读取 32

生成的总线映射

注意：这只是部分总线映射。实际上，我们还将在总线映射中包含堆栈、存储和 opcode 详细信息

global_counter	memory_flag	memory_index	memory_value
12	1	0	12
17	1	1	32
24	0	0	12
89	0	1	32

伪代码

``` python

rand 是用于构造 plookup 键值映射的随机数

它是 r、r**2、r**3、r**4 .. r**n 的列表

def memory(rands): bus_mapping = {{}} index = [0,0,0,1,1,1]

value = [0,12,12,0,32,32] memory_flag = [1,1,0,1,1,0] global_counter = [0,12,24,0,27,89]

将 prev index 设置为 legal 内存范围之外的值

prev_index = p-1

检查 10000 个内存操作

for i in range(10000):

检查其余部分

for value, memory_flag, global_counter, index in zip(value, memory_flag, global_counter, index):

二进制约束

require(memory_flag == 1 or memory_flag == 0)

检查值是否正确

如果 memory_flag == 0，则表示它是读取，我们检查

previous_value == 当前读取的值

if index != prev_index:

初始化为零

prev_index = index require(value == 0) require(memory_flag == 1)

if (memory_flag == 0): require(current_value == value)

else (memory_flag == 1):

如果它是写入，我们只需设置 current_value = new_value

current_value = value

检查 global_counter 是否正确排序

require(global_counter > previous_global_counter) previous_global_counter = global_counter

if(global_counter!=0):

添加到总线映射

global_counter = plookup(global_counter, valid_glbal_counters) mapping = plookup(mapping, valid_mappings) memory = "memory" memory_flag = memory_flag index = index value = value

检查键值映射

require(mapping == global_counter + rand[0] * memory + rand[1] * memory_flag + rand[2] * index)

```

堆栈

我们的堆栈有 16 个可以推送、弹出、复制和交换的元素。但它也包含必须存储的 1024 个元素。例如，你可以将 `3` 推送到堆栈 1024 次，然后弹出 1024 次。因此，我们需要能够支持这 1024 个存储元素。

为了证明我们的堆栈的有效性，我们做了与内存相同的事情。我们创建一个包含 $1024$ 个元素的内存表（索引为 0-1023）。我们还创建一个堆栈指针（`stack_pointer`)，它初始化为 1024。这指向堆栈顶部的索引。

推送/弹出

我们的 EVM 证明跟踪 `stack_pointer`，并在每次推送时递减它，并在每次弹出时递增它。

在我们的状态证明中，我们的证明者必须将每个堆栈元素初始化为零。然后，他们可以执行他们想要的任何更新。然后，他们将其提交到我们的总线映射。

在 EVM 证明中，对于检查堆栈的每个 opcode，我们从总线映射中获取与该堆栈关联的堆栈操作。我们检查 push、pop 的索引是否与 `stack_pointer` 匹配。然后，我们根据我们是弹出还是推送来调整 `stack_pointer` (`++`/`--`)。

复制

与推送/弹出的情况类似，我们可以这样做。但是我们必须检查两个索引：目标和源；然后将该值推送到堆栈上。这需要一次读取，然后进行一次推送。

交换

在这里，我们读取两次要交换的两个索引，并对每个索引执行两次写入以获取另一个值

注意：现在不允许在堆栈中的前 16 个元素之外推送弹出复制交换。为避免这种情况，我们必须对 stack_pointer 执行范围证明 - 索引小于 16。

^ 即，我们必须检查 `index` 是否为 4 位值。这肯定可以通过 4 位查找表来实现（无论如何，我们很可能在电路中有更大的查找表用于其他目的）。 [name=ying tong] [name=barryWhiteHat] 嗯，它是 stack_pointer - index 对吗？因为如果我在堆栈上推送 1016 个东西，我只能推送弹出复制和交换元素 1016 到 1000。

TODO：如果你只使用几个元素，则可能不需要在堆栈中包含 1024 个元素。我们可以让证明者调整这些

EVM 证明

[name=barryWhiteHat] 也许我们可以删除 slot，而只支持必须应用的每个约束的列表。

Slot (槽)

可以将 slot 定义为单个自定义约束。此约束可以由 opcode 程序员定义以执行该操作。大多数 opcode 可能会执行的一些操作是

1. 获取我们正在执行的当前 opcode
2. 获取状态证明通过内存总线提供的堆栈和内存/存储变量。
3. 确保仅提供了内存或存储值。如果提供了两个，则失败。
4. 检查是否提供了正确的总线映射变量。例如，对于 add，我们必须有 3 个堆栈元素（两个弹出和一个推送）。所有操作都在索引 0 处执行。
5. 用于算术/二进制运算/比较器的多个 plookup 约束
6. 检查 3 的结果是否与 opcode 要求的匹配。
7. 检查该 opcode 的完成条件。
   • 如果：true 递增 `program_counter`
   • 否则：对此 opcode 使用另一个 slot 并递增 `slot_counter`

我们的 opcode 可以是多个唯一的自定义约束，我们只需要确保我们的选择器使用 slot_counter 来选择正确的自定义约束。

伪代码

``` python

global_counter 输入

program_counter 输入

slot_counter 输入

fin_condition 由 opcode 定义

def slot(): opcode = plookup(t_opcodes) mapping = plookup(t_mappings)

assert global_counter + program_counter * r + opcode * r**2 == mapping

TODO 我们可能必须在此 plookup 中包含​​更多元素

例如堆栈存储和内存

执行我们实际的 opcode 工作

TODO 如果需要，计算 fin_condition

这意味着多个 slot opcode

几个 plookup

订购 100 个 plookup

检查我们是否完成

if slot_counter == fin_condition: slot_counter = 0 program_counter ++

else: slot_counter ++

gas_used += gas_cost

if gas_used > gas_limit:

耗尽 gas

oog = True program_counter = oog_opcode

global_counter ++ ```

slot 变量

slot 使用一堆变量来确保它在总线映射中查找正确的元素。这些变量是从上一个 slot 传递的。我们可以只查看上一个电路的连线，而不是使用复制约束来确保这些是正确的。

这些变量包括

1. 全局计数器
2. 槽计数器
3. 程序计数器
4. call_id
5. 堆栈指针
6. 几个 advice 电线。
7. 中间变量线

这意味着我们的 evm 证明将有 5 根电线进入每个自定义约束，以及几个 advice 电线

流程控制

（TODO？） [name=ying tong] [name=barryWhiteHat] 简而言之：我们使用 jump opcode 将程序计数器调整到它应该是什么，这就是我们处理循环和其他事情的方式。

数据编码

我们的字段元素大小为 253 位。因此，我们无法在单个字段元素中表示 256 位（evm 字大小）的字。所有算术都以 p ~ 253 位为模完成，这也与 evm 不兼容。

为了使两者都与 EVM 兼容，我们将堆栈和内存元素编码为分解为 8 位的字的随机线性组合。

w 是我们的字，w[0:7] 是我们字的前 8 位。

word = w[0:7] + w[7:15]r + w[15:23] r^2 .. + w[247:255]r^31

注意：r 计算为所有可能的 8 位字的哈希值

[name=barryWhiteHat] 这里是否存在一些攻击？看起来有 2^8 个可能的元素，并且当我们将其增加到 32 个元素的总和时，在某个时候会出现一些“冲突” [name=barryWhiteHat] 如果这是一个问题，我们可以将 r 作为该轮中所有元素的列表。 如果这不是问题，那么我们可以将编码后的变量放入存储中。

这使我们通过在查找表中查找每个字来非常容易地进行算术运算，该查找表映射到该运算。

我们的堆栈和内存不需要为了适应这一点而进行调整。但是当我们在获取调用数据并读取或写入存储时，我们需要应用此编码/解码。

算术

回想一下，总线映射的构造如下：

加法

从总线映射中获取三个元素

``` value1 , value2 , value3 = bus_mapping[global_counter][call_id][prog_counter][stack][op_id][index] ```

^ 这里的 `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 } ``` `value1, value2, value3` 是否应该分别具有不同的 `op_id` 和 `index`？

[name=ying tong] 我打算删除 value2、value 3 并将 value 1 重命名为 value。认为我们不需要多个值，我们可以在我们的自定义 opcode 中包含 3 个堆栈操作。 我正在向 Han 询问这件事，因为我认为他对这件事进行了一些思考，所以很想听听他的想法。 如果总线映射的大小不是恒定的，我们会付出什么代价？ [name=barryWhiteHat]

`value1`、 `value2` 和 `value3` 定义为 32 个 8 位字。

``` python carry_bit = 0 for i in range(len(value1)): result, carry_bit = plookup_add(value1[i], value2[i] carry_bit) require(result == value2[i]) ```

二进制运算

比较器

大于

从总线映射中获取两个元素

``` value1 , value2 = bus_mapping[global_counter][call_id][prog_counter][stack][op_id][index] ```

`value1`、 `value2` 定义为 32 个 8 位字。

``` python carry_bit = 0

在这里，我们使用 carry_bit 作为已检查为真的 a。

从最低有效位到最高有效位的反向顺序.

for i in range(len(value1),0):

old_carry_bit = carry_bit result, carry_bit = plookup_greater_than(value1[i], value2[i], carry_bit)

result == value3 ```

调用 / 静态调用

调用应更新 evm 证明中的 `call_id` 。这将允许证明者创建一个新的内存和堆栈，该内存和堆栈在状态证明中没有任何元素，并将其用于此调用上下文。

我们还跟踪 `calldatacallid`、 `calldata_start`、 `calldatasize` 以及 `returndatacallid`、 `returndata_size`、 `returndata_start`。如果使用 calldatacopy 或 return data copy opcode，我们要求证明者使用 callid 进行数据复制或 returndatacopy 将数据复制到 hte 当前 call_id 的内存中。

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 的元素传递。

与调用详细信息相关的 Opcodes

opcode	名称	描述
0x32	ORIGIN	获取执行发起地址
0x33	CALLER	获取调用者地址
0x34	CALLVALUE	使用此 tx 发送了多少 eth
0x36	CALLDATASIZE	多少调用数据
0x35	CALLDATALOAD	什么是调用数据
0x3d	RETURNDATASIZE	多少返回数据
	返回数据	什么是返回数据
	调用堆栈深度
	此调用之前的存储根	使用它来恢复并强制执行静态调用

具有可变工作的 Opcodes

到目前为止，我们已经讨论了具有恒定工作量的 opcode。例如 $\texttt{mul}$ 采用两个数字并将它们相乘。无论在计算时为 $\texttt{mul}$ 提供什么参数，证明 $\texttt{mul}$ 已正确执行的工作量仍然相同。

还有另一类 evm opcode 与它们相关联具有可变的工作量。这些 opcode 倾向于从内存中加载可变长度的项目。例如， `calldatacopy` 将调用数据复制到堆栈上。此调用数据的长度由智能合约程序员定义，并且是可变的。

这提出了一个困难的挑战。如果我们使我们的“opcode slots”足够长以支持每个可能的 `calldatalength` ，这将使我们的 opcode slot 变得非常大，从而使我们的其余 opcode 过于昂贵。相反，我们将这些 opcode 分隔在多个 opcode slots 上，以便我们继续处理它们，直到它们成功完成。

这些 opcode 包括

`calldatacopy`、 `returndatacopy`

calldatacopy / returndatacopy

我们通过定义一个必须满足才能递增 `program_counter` 的条件来对这些 opcode 进行算术化。然后，我们可以为同一 opcode 使用多个 global_counters。例如， `calldatacopy` 在我们递增程序计数器之前，必须将元素从 `call_details.calldata` 复制到堆栈 `calldatalength` 次。

类似的方法可用于 `returndatacopy` 和 `return` 。

安全属性证明

流程控制

预备知识

我们有一个键值映射，它将智能合约字节码中的每个 opcode 映射到其字节偏移量（也称为 `program_index` ）。此 `program_index` 是执行该 opcode 所需的 `program_counter` 值。

我们的证明者能够选择任何 `opcode`:`program_index` 对。我们想要确保证明者只能选择有效的执行分支。更改 opcode 的顺序、添加 opcode 或删除 opcode 等操作会破坏这一点。

假设

IndexUniqueness ：`program_index` 列表仅包含唯一值（无重复）。

GlobalCounterUniqueness ：在 EVM 证明中，Opcodes 以递增的 `global_counter` 值执行，即。global_counter $0,1,2,3$

StartZero ：`call_id` 的第一个 `program_counter` 变量为 0。

StopAtTermination ：`call_id` 的最后一个 `program_counter` 变量为 opcode $\texttt{stop}$ 或 $\texttt{return}$

ProgramCounterTransition ：每个 opcode 根据其规则调整 `program_counter` ：除了执行当前 opcode 之外，没有其他方法可以更新 `program_counter` 。例如，$\texttt{mul}$ 将其递增 1。$\texttt{jump}$ 从堆栈中弹出一个元素并将程序计数器设置为等于该元素。

2.1 Opcode 以正确的顺序执行

TODO：添加有关部署和加载字节码的推理

• $\texttt{StartZero}$ 假设表示我们必须从 `program_counter` = 0 开始，对于每个智能合约，它都是正确的起始位置。
• $\texttt{ProgramCounterTransition}$ 假设表示我们必须基于我们正在执行的 opcode 正确更新我们的程序计数器。
• 因为我们正确地更新了程序计数器，所以我们得到了正确的第二个存储根。
• 通过归纳法，n 有效，n+1 有效，因此我们必须继续这样做直到终止。
• $\texttt{StopAtTermination}$ 假设表示我们继续这样做直到我们达到终止该调用的 opcode 。

2.2：你不能插入额外的 opcode

注意：这更多是关于部署的证明。

• $\texttt{IndexUniqueness}$ 表示对于每个 `program_index` 只有一个值。
• 如果你插入额外的 opcode，则会破坏此假设，因此它是错误的。

2.3：你不能跳过一个 opcode

• 你需要更新你的 `program_counter` 才能移动到下一个 opcode
• 执行此操作的唯一方法是执行当前 opcode
• 如果你跳过一个 opcode，这将违反 $\texttt{ProgramCounterTransition}$ 假设。

总线映射证明

预备知识

我们使用我们的总#### 证明

因为有了 $\texttt{Global_counterUniqueness}$ 假设，我们知道对于每个 global_counter 只能有一个元素。

在 EVM 证明中，我们确认每个元素都是正确的。

opcode 正确性论证 表明，我们以正确的顺序执行 opcode，直到到达存储读取/写入的 opcode。

$\texttt{ProgramCounterTransition}$ 假设对于每个 opcode（包括存储/堆栈/内存），我们正确地更新程序计数器。

我们还需要确认，在我们的状态证明中，我们没有执行任何额外的读取/写入操作，而这些操作没有在我们的 EVM 证明中进行检查。为此，我们使用 $\texttt{DegreeBound}$ 假设，该假设限制了 `bus_mapping` 的大小。然后，我们在 EVM 证明中确保检查每个 global_counter 值，直到达到我们的 degreeBound。

总有可能一个总线映射包含一个内存读取、一个存储写入和一个堆栈推送。这是无效的，因为没有 opcode 需要这 3 个操作。在这里，攻击者试图将存储写入隐藏在内存读取的 opcode 中。我们添加了 $\texttt{OpcodeFidelity}$ 假设，以确保 opcode 仅包含它们关心的变量的映射，其余变量都为零。例如，$\texttt{mul}$ opcode 的总线映射应该只包含堆栈的一个元素。

• 原文链接： hackmd.io/Hy_nqH4yTOmjjS...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～