EVM到Valida编译器设计

2024 年 9 月 4 日

目标

本文档是一项头脑风暴练习，深入探讨了在设计和实现编译器以将以太坊虚拟机 (EVM) 字节码转换为 Valida 字节码时遇到的复杂性和挑战。在整个探索过程中，很明显，构建 EVM 到 Valida 的编译器比最初预期的要复杂得多。在不依赖 LLVM Valida 后端的情况下，我们发现自己走上了一条更加细致和复杂的解决方案之路，应对了诸如字长差异、与外部世界的交互模型以及操作码实现等无数考虑因素。

介绍

动机

本文档的动机性问题是：我们如何设计和实现一个将以太坊虚拟机 (EVM) 字节码转换为 Valida 字节码的编译器？我们（即 Lita 基金会）发现这个问题有趣的原因是，我们相信与现有的解决方案相比，Valida 可以提供性能更高的 zk-EVM 解决方案。创建一个直接执行 EVM 字节码的 zk-EVM 并不简单或容易，因为 EVM 字节码语言及其各个指令的复杂性。由此产生的 ZK 约束系统可能具有数百列和数千个约束。目前工作背后的假设是，通过将 EVM 字节码转换为 Valida 字节码，并在 Valida zk-EVM 上执行生成的 Valida 字节码，可以获得性能更高的解决方案（在证明的时间和空间复杂度方面）。

解决批评

这种方法可能受到的批评是，它修改了正在证明的语句。要证明的语句不是“在某些输入上执行的 EVM 程序 p 产生输出 x”，而是“在某些输入上执行的 Valida 程序 p′ 产生输出 x”。如果验证者可以通过在 p 上重新运行 EVM 到 Valida 的编译器来验证 p′ 是将 p 编译为 Valida 的结果（或者只是被硬编码为知道这个事实），则这不是问题。解决批评的另一种方法是在 Valida zk-VM 中运行 EVM 到 Valida 的编译器，以生成“p′ 是在 p 上运行 EVM 到 Valida 的编译器的结果”的简洁证明。然后，验证者可以简洁地验证 p′ 的执行以及 p 到 p′ 的编译。

选择 Rust 的原因

EVM 到 Valida 的编译器应该用 Rust 编写。原因有三：

1. 这是为了便于将 EVM 到 Valida 的编译器编译为 Valida，以便使用 Valida 来简洁地证明 EVM 到 Valida 的编译器的执行。

2. 这是为了便于高效地编写正确的代码（与 C/C++ 相比）。

3. 这是为了使用我们计划在 Valida LLVM 后端中支持的第一批语言之一。

‍

EVM 和 Valida：比较

EVM 特性

EVM 是一种计算模型。以下关键区别使 EVM 作为一种计算模型具有独特性：

1. EVM 使用 256 位字长。

2. EVM 使用哈佛架构，RAM 和程序 ROM 具有单独的地址空间。程序 ROM 是可读和可执行的。

3. EVM 是一种堆栈机器，具有 1024 字的堆栈（与 RAM 分开），EVM 操作码隐式地引用该堆栈。

4. EVM 字节码通过两个状态树与外部世界交互：全局状态树和合约数据存储树。全局状态树由所有以太坊合约共享，每个以太坊合约都有自己的合约数据存储树。

Valida 特性

为了进行比较：

1. Valida 使用 32 位字长。

2. Valida 使用哈佛架构，RAM 和程序 ROM 具有单独的地址空间。程序 ROM 是可执行的但不可读的。

3. Valida 是一种堆栈机器。它的堆栈存在于 RAM 地址空间中。

4. Valida 字节码通过只读输入磁带和只写输出磁带与外部世界交互。

异同

Valida 对于 EVM 编译来说不是一个糟糕的目标。EVM 和 Valida 具有某些相似之处，有助于此过程；它们都是哈佛架构的堆栈机器，其中的代码在密闭环境中运行，只有有限的方式与外部世界交互。但是，由于阻抗不匹配，需要做一些重要的工作来弄清楚如何将 EVM 编译为 Valida：主要是不同的字长以及与外部世界交互的不同模型。

‍

处理字长差异

模拟 256 位算术

可以使用八个 32 位字来表示一个 256 位字，从而在 Valida 中模拟 256 位算术操作码。这是 EVM 到 Valida 编译的必要步骤之一。256 位算术操作码的实现可以内联或分离为子例程，具体取决于哪种方法似乎更有效。如果能够检测到何时未使用完整的 256 位范围并且较小的字长就足够了，那就太好了，但是这种优化超出了当前设计中考虑的复杂程度。

‍

地址空间挑战

性能考虑

需要考虑的挑战之一是，EVM 具有 256 位的地址空间，而 Valida 的地址空间小于 32 位。从性能的角度来看，最好的解决方案是假设输入的 EVM 字节码不使用大于 Valida 地址空间中最大地址的地址。例如，从 RAM 加载数据时，可以仅使用 256 位地址的最低有效 32 位。这将导致 EVM 地址空间中不同地址之间的许多等式。这对于某些 EVM 字节码可能是正确的，但对于其他字节码则不然。

地址映射解决方案

一种更通用、效率较低但仍然相当高效的解决方案是，对于较小地址范围，在 EVM RAM 地址空间和 Valida RAM 地址空间之间使用直接映射，然后在一个数据结构（例如哈希表或二叉搜索树）中保存较大地址的值，该数据结构保存在 Valida RAM 的一个与直接映射到 EVM RAM 地址空间的部分不相交的部分中。这种方法的优点是，对于所有不消耗比 Valida 可用 RAM 更多的 RAM 的 EVM 字节码，它都具有语义保留。它的（缺）优点是对于足够小的地址来说是高效的，而对于较大的地址来说，效率较低但仍然正确。

需要考虑的另一个挑战是，EVM 字节码具有两个可以与之交互的状态树，而 Valida 字节码只有只读输入磁带和只写输出磁带。为了解决这个挑战，我们需要为 Valida 设计一个 EVM ABI（应用程序二进制接口），该接口定义了与 EVM 状态树的交互应如何编码为与 Valida 输入和输出磁带的交互。

‍

与状态树的交互

状态树的语义

从语义上讲，状态树是一个键值映射。状态树支持两种形式的交互：读取键处的值和写入键处的值。设计 Valida ABI 的一种天真的方法是在输入磁带上提供状态树，并让程序将状态树更改的日志写入输出磁带。这种天真的方法行不通，因为通常状态树太大，无法完整提供。

建议的状态树交互 ABI

本设计中提出的 ABI 风格具有以下元素：

1. 主机代码，即调用 zk-VM 证明器的代码，将每个状态树的初始根哈希作为输入磁带中的第一项提供。

2. 主机代码将以下数据作为输入磁带中的下一项提供：

(a) gas 价格（执行交易的）

(b) coinbase（即当前区块矿工的地址）

(c) 网络 ID（即链 ID）

(d) 当前区块时间戳、编号、难度、gas 限制和基本费用

(e) 最近 256 个区块的哈希值

3. 主机代码将 calldata 作为输入磁带中的下一项提供。

4. 客机代码，即 Valida 字节码，从输入磁带复制初始状态树根哈希作为输出磁带中的第一项，后跟 gas 价格、coinbase 和最近 256 个区块的哈希值（或其相关子集）。

5. 主机代码在非 ZK EVM 中运行 EVM 字节码，以获得一个跟踪，该跟踪指定所有读取状态树和写入状态树的操作及其结果，以及获得的最终状态树哈希值。

6. 主机代码将一些关于程序查询的键处的状态树内容的主张写入输入磁带。除了这些主张之外，主机代码还写入打开证明，以证明状态树确实包含这些键/值对。

7. 在跟踪中每次写入状态树时，主机代码都将新的状态树根哈希写入输入磁带。

8. 客机代码验证主机代码在输入磁带上发送的打开证明。

9. 客机代码将其执行的所有 LOGi EVM 操作码的输入写入输出磁带。

10. 客机代码将其对外部合约的所有调用写入输出磁带。

11. 主机代码将客机代码对外部合约的所有调用以及产生的状态树根哈希写入输入磁带。

12. 主机代码将所有 RETURNDATASIZE 和 RETURNDATACOPY 操作码的调用的结果写入输入磁带。客机代码将这些操作码的所有调用的结果从输入磁带复制到输出磁带。

13. 如果源客机代码的执行跟踪包括 SELFDESTRUCT 的调用，则编译后的客机代码会明确地向输出磁带写入一条它已执行此操作的消息。

14. 客机代码通过复制主机代码在其输入磁带上提供的每个状态树的最后一个根哈希，将两个状态树的最终根哈希写入输出磁带。

此 ABI 风格旨在证明以下形式的语句：“程序 p 在具有根哈希 (a0,b0) 的状态树、gas 价格 p、coinbase c、网络 ID N、区块时间戳 t、区块编号 i、区块难度 d、gas 限制 l、基本费用 b、最近区块哈希 h0,...,h255 和一些 calldata 上运行时，会产生具有根哈希 (a1,b1) 和日志输出 L 的状态树。”

‍

代码和内存访问挑战

模拟 CODECOPY

需要考虑的另一个挑战是，EVM 包含 CODECOPY 操作码，可用于将字节从程序 ROM 复制到 RAM 中。为了在 Valida 中模拟此操作码，我们可以向使用此操作码的已编译 EVM 程序添加前导码。前导码会将所有 EVM 字节码（源程序）写入 RAM 中的固定位置。

处理 EXTCODESIZE 和 EXTCODECOPY

另一个需要考虑的挑战是，EVM 包含 EXTCODESIZE 和 EXTCODECOPY 操作码，可用于检查或复制与当前执行的合约不同的合约的程序 ROM 中的字节。为了在 Valida 中模拟这些操作码，我们可以认识到它们是从全局状态树读取的示例，因为全局状态树包含所有合约的哈希值，并且主机代码可以通过展示用于创建这些哈希值的源数据来提供这些哈希值的打开证明。

‍

其他 EVM 操作码

GAS 指令

另一个需要考虑的挑战是，EVM 包含 GAS 指令，该指令输出当前剩余的 gas 限制。对于包含此指令的程序，我们可以初始化一个包含当前剩余 gas 限制的全局变量，最初设置为 gas 限制，并且我们可以在每个操作码的编译之后添加一条或一系列指令，以将剩余 gas 限制减少操作码的 gas 成本。

PC 指令

另一个需要考虑的挑战是 PC 指令，该指令输出程序计数器的当前值。这是相对于程序计数器在 EVM 源字节码中的位置，而不是目标 Valida 字节码。因此，我们无法通过读取“pc”寄存器的值来获得所需的答案。使该指令易于实现的原因是 PC 是一个编译时常量，或者它等于一个编译时常量加上 ROM 中第一条指令的地址（如果 ROM 中第一条指令的地址可能不等于零）。如果 ROM 中第一条指令的地址可能不等于零，那么我想我们可以提供输入磁带上第一条指令的地址。

REVERT 操作码实现

为了实现 REVERT 操作码，EVM 到 Valida 的编译器可以简单地将最终状态根哈希写入输出磁带，指示初始状态根哈希作为最终状态根哈希，然后终止。

与外部合约相关的操作码

合约创建：CREATE 和 CREATE2

另一组需要考虑的挑战是如何处理与外部合约相关的操作码：CREATE、CALL、RETURNDATASIZE、RETURNDATACOPY、RETURN、DELEGATECALL、CREATE2 和 STATICCALL。这些与创建和调用其他以太坊合约有关。当调用另一个合约时，它有自己的 RAM 和 ROM 地址空间，并且它可以向调用堆栈添加自己的调用，每个调用都有自己的 RAM 和 ROM 地址空间。

CREATE 向全局状态添加一个新合约。可以通过考虑这是写入全局状态树的一个实例来在编译器中实现此操作码。在 ABI 中，主机代码将生成的全局状态树根哈希写入输入磁带，客机代码将全局状态树的新元素写入输出磁带。CREATE2 类似，可以类似地实现。

处理外部调用

与外部合约相关的其余操作码与调用其他以太坊合约有关。通过将对其他合约的调用外部化来处理这些操作码似乎最简单。在 ABI 中，主机代码将客机代码进行的调用以及调用的结果写入输入磁带。客机代码读取输入磁带，并检查它想要进行的调用是否按照预期记录在那里。它读取调用的结果。客机代码将它读取的关于调用的相同数据写入输出磁带，以便该数据成为正在证明的语句的一部分。关于调用的数据包括每次调用后产生的状态树。

‍

结论和意义

在存在外部调用的情况下，正在证明的语句并没有断言状态转换的正确性；相反，它有条件地断言状态转换的正确性，这取决于为外部调用声明的状态转换的正确性。为了在存在外部调用的情况下简洁地证明状态转换的正确性，证明聚合器可以将与外部调用相关的执行证明与与这些调用发生的上下文相关的有条件执行证明结合起来。

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