我们很高兴地宣布，Nethermind Security 的形式化验证团队和 Succinct Labs 已经联手，使用 Lean 证明助手来形式化验证 SP1 Hypercube（https://blog.succinct.xyz/sp1-hypercube/）RISC-V zkVM 中所有核心 RV-64 芯片的正确性。我们还要感谢以太坊基金会为此项工作提供的慷慨支持。
特别是，相关的 RISC-V 操作码的行为已根据官方 64 位 RISC-V Sail 规范（https://github.com/opencompl/sail-riscv-lean）进行了验证，该规范作为另一个由以太坊基金会资助的项目的一部分，被提取到 Lean 中。据我们所知，这是该规范首次成功用于大规模验证工作，证明了其在实际应用中的可行性。
在这篇简短的文章中，我们将总结成果，反思技术挑战，并讨论相关的注意事项。一篇深入的技术博客将在不久的将来发布。
设计原则
形式化验证任何系统的第一步是给出预期行为的精确规范。SP1 Hypercube 证明了使用 RISC-V 64 位指令集编码为程序的计算的有效性。因此，对我们来说，预期行为的真理来源必须是 RISC-V 指令集的官方规范，这一点非常重要。
验证结果
我们使用 Lean 证明助手验证了整个 64 位 SP1 Hypercube RISC-V zkVM 核心的正确性，该核心与官方 RISC-V Sail 规范相符。这涵盖了以下 62 个操作码：
- 41 个与 ALU 相关的操作码：ADD, ADDW, ADDI, ADDIW, SUB, SUBW, XOR, XORI, OR, ORI, AND, ANDI, SLL, SLLI, SLLW, SLLIW, SRL, SRLI, SRLW, SRLIW, SRA, SRAI, SRAW, SRAIW, SLT, SLTI, SLTU, SLTIU, MUL, MULH, MULHU, MULHSU, MULW, DIV, DIVU, DIVW, DIVUW, REM, REMU, REMW, REMUW
- 10 个与控制流相关的操作码：JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LUI, AUIPC
- 11 个与内存相关的操作码：SB, SH, SW, SD, LB, LBU, LH, LHU, LW, LWU, LD
技术挑战
该项目提出了几个技术挑战，包括 SP1 工具层面的挑战以及对使用的 Lean 库进行的更改，包括将一些改进 upstream 到 RISC-V 规范。
挑战 1：与 Lean RISC-V 规范的连接
RISC-V 指令集的形式化规范是用 ISA 规范语言 Sail 编写的。Sail 的 Lean 后端提供了 SailM 单子，这是一个组合的错误和状态单子，表示抽象 RISC-V 机器的执行，其中状态包括寄存器和内存中的当前值。在此单子中运行计算会得到一个从初始机器状态到最终机器状态的函数，表示内存和寄存器是如何更改的。
为了验证给定操作码的正确性，我们在此单子中对 SP1 实现进行建模，并将其与 Sail 提供的实际规范进行比较，表明如果所有提取的约束都成立，那么两者对任何有效的初始机器状态都具有相同的效果。这种方法使我们能够独立地推理单子行为和算术约束：我们可以首先使用单子推理来简化为关于寄存器和内存值的具体语句，然后使用约束来建立规范中和 SP1 中值之间的对应关系。有关标准示例，请参见 add 的证明。
在大多数情况下，此处的有效初始状态仅表示状态中的每个寄存器都初始化为某个（未指定/垃圾）值，这大大简化了推理计算所需的案例分析量。但是，对于基于内存的操作码，我们还需要对特定的寄存器值进行一些额外的假设（例如，假定 plat_ram_base 寄存器（用于设置内存寻址的起始索引）为零）。
由于 Sail 的 Lean 后端提取是自动化且是新的，因此在执行验证时，我们发现并帮助解决了验证过程中出现的一些 upstream 问题，例如不明确的类型注释、循环的不透明定义以及许多无法通过 Lean 内核安全展开的操作。
挑战 2：约束提取
为了获得 SP1 约束的准确表示以用于这些证明中，下一个挑战是将约束从源代码提取为 Lean 可以理解的格式。SP1 约束是使用 Air 抽象用 Rust 编写的。幸运的是，由于此抽象与后端无关，如 AirBuilder 特征所编码的那样，我们可以简单地通过创建一个新的 AirBuilder 实现来跟踪约束和交互来提取约束。这种简单的提取会产生每个芯片的方程和交互集合。
在这方面，一个提出了挑战的要求是提取的模块化。原则上，形式化验证极大地受益于模块化，尤其是在证明复杂语句的情况下，因为这意味着不必一遍又一遍地完整编写相同的证明。最初的 Rust 代码本身是模块化的，因为它识别出了许多重要的独立部分，并将其隔离到函数中，然后通过函数调用重新使用，但是最初的提取代码会“忘记”此结构。这些函数捕获了非常特定的行为，理想情况下，它们将用作证明各种芯片约束的主要定理的基本引理。由于这些原因，我们修改了提取代码以反映这种额外的结构，这需要对 Rust 约束 API 进行一些更改。
挑战 3：推理操作码的正确性
在克服了与 Lean RISC-V 规范相关的挑战之后，剩下的就是实际证明与目标操作码关联的约束实际上描述了所需的行为。
首先，这涉及到开发一种基础设施，用于推理对 32 位和 64 位机器整数执行的字节和 16 位级别操作。
其次，我们还需要推理有限域算术，首先是 BabyBear 域，然后是 KoalaBear 域。特别是，由于这些域的大小略低于 2^32，因此有时这很复杂，这意味着必须使用各种特定于域的技术来表达约束和操作，否则就可以直接表达这些约束和操作。幸运的是，Lean 附带 Mathlib，这是一个关于有限域/自然数/整数/位向量的事实的综合库，以及 omega、bv_decide、aesop 和 grind 自动推理过程，我们发现所有这些都非常有帮助。
最后，我们定义芯片操作的模块化方法在验证更复杂的操作码时被证明是无价的。一个典型的例子是 DivRem 芯片，它使用了乘法、加法和比较等操作。由于我们已经单独证明了这些基本操作的规范，因此我们可以简单地在更大的 DivRem 证明中重用这些规范。如果没有这种模块化，我们将不得不在每次使用每个子操作时重复整个逻辑推理，从而创建出臃肿、难以管理的证明，这些证明可能会压垮 Lean。通过依靠模块化，我们不仅节省了巨大的精力，而且还保持了证明的清晰性和可维护性。
假设和注意事项
重要的是要注意，验证受到许多注意事项和假设的约束。
首先，我们对使用的外部和内部工具有假设：
- 我们假设 Lean 内核的正确性
- 我们假设已实现的约束提取机制的正确性：证明其正确性需要对 Rust 代码本身进行形式化推理
- 我们假设 64 位 Lean Sail RISC-V 规范相对于官方 RISC-V 标准的正确性
我们还对 SP1 的约束和交互在 Lean 中的表示以及它们所暗示的语义做了一些假设（有关 Lean 中的假设，请参见此文件）：
- 我们假设从 SP1 查找总线的内容和相关的 air 交互中导出的约束的正确性
- 我们假设 SP1 查找总线的理论和实现以及底层证明系统的正确性
最后，我们有一些希望在未来工作中处理的限制：
- 我们证明了芯片操作和 RISC-V 规范之间的基本连接：将来，应该加强这种连接，以便更高地进入 RISC-V 执行函数的层次结构
- 我们尚未证明任何与内存一致性相关的结果
- 某些常量表查找的语义被假定为正确，而没有经过证明。与 Lean 中更通用的电路表示集成可以允许直接验证其正确性
