Show HN: Talos – 基于 Lean 4 的开源 WebAssembly 解释器

背景

在形式化验证和编译器正确性证明的领域，维持“可执行语义”与“形式化规范”之间的一致性一直是一个痛点。传统的做法往往涉及维护两个独立的代码库：一个是用于实际执行代码的解释器或编译器，另一个是用于数学推理的形式化规范。这种分离不仅增加了维护成本，还容易引入两者不同步的风险，导致证明结果无法反映实际行为。

Talos 项目正是为了解决这一矛盾而诞生。它由希腊神话中守护克里特岛的青铜巨人 Talos 命名，寓意其作为“机械守护者”的角色——旨在严格执行规则。Talos 是一个完全使用 Lean 4 编写的 WebAssembly (Wasm) 解释器。其核心理念在于统一：执行 Wasm 程序所使用的定义，正是用于进行逻辑推理的定义。通过让评估（Evaluation）与证明（Proof）共享同一个代码库，Talos 消除了维护独立规范解释器的需求，实现了语义与形式化对象的统一。

核心内容

Talos 目前处于积极开发阶段（Work in progress），其 API 和证明接口可能会发生变化。该项目的目标是构建一个功能完备的 WebAssembly 可执行语义，同时将其作为形式化对象使用。

双重用途：执行与证明

Talos 允许用户在同一套代码基础上进行两种操作：

1. 运行程序：在具体的输入上运行 Wasm 程序。
2. 形式化证明：利用 Lean 的证明工具，对程序的行为进行陈述和证明。这包括验证程序是否符合规范、证明不同程序之间的等价性，以及证明适用于所有输入的属性。

设计哲学：推理优先于速度

Talos 的解释器在架构上刻意优化了“推理的清晰度”，而非“执行速度”。虽然 Talos 旨在覆盖完整的 Wasm 功能，但其当前的重点在于那些自然出现在非优化、高级源代码（如 Rust、C 等）中的 Wasm 子集。这些语义对于验证程序“做什么”至关重要，而对于验证程序“做得有多快”则次要得多。

证明是北极星（North Star）：性能优化工作被置于次要地位，并计划通过一个单独且经过等价性证明的实现来处理。

技术实现：最弱前置条件演算

Talos 中的证明构建基于最弱前置条件（Weakest Precondition, WP）演算。这是一种谓词变换器语义（predicate transformer semantics），允许用户从后置条件反向推导能够保证该后置条件成立的前置条件。

这种机制使得针对循环、分支和函数调用的证明变得结构化且具有组合性（compositional），无需在每一步都重新展开解释器逻辑。

使用示例与构建流程

1. 运行 Wasm 模块 Talos 提供了命令行工具来运行 .wat (WebAssembly Text) 文件。

• 基本运行：

  cd interpreter
  lake exe runner samples/factorial.wat fact 5
  

  输出结果为 120（5 的阶乘）。
• 设置燃料上限： 为了防止无限循环，默认执行步数上限为 1,000,000 步。可以通过 --fuel 参数调整：

  lake exe runner --fuel 10000 samples/factorial.wat fact 5
  

2. 进行形式化证明 在 interpreter/Interpreter/Wasm/Examples/Factorial.lean 文件中，展示了如何使用 WP 战术层（tactic layer）完成完整的正确性证明。

3. 依赖管理与构建 Talos 采用单仓库（monorepo）结构，包含三个 Lake 包，形成严格的依赖链：

• WasmInterpreterLean：仅依赖解释器（Wasm 语义 + WP 演算）。
• CodeLib：在解释器之上添加提升引理（lifting lemmas）和推理辅助工具。
• Programs：具体的程序验证示例。

依赖使用方式：

• 如果只依赖解释器，在 lakefile.toml 中配置：

  [[require]]
  name = "WasmInterpreterLean"
  scope = "your-org" # 如果发布则使用此字段，否则使用 path/git
  path = "path/to/repo/interpreter"
  

• 如果依赖 CodeLib，则配置：

  [[require]]
  name = "CodeLib"
  path = "path/to/repo/codelib"
  

  导入 CodeLib 的代码无需直接导入解释器，因为 CodeLib 会重新导出下游证明所需的部分。

构建命令：

• 按顺序构建所有包：

  just build # 依次构建 interpreter -> codelib -> programs
  

• 单独构建某个包：

  cd interpreter && lake build
  cd codelib && lake build
  cd programs && lake build
  

依赖项：

• Lean 4：工具链版本锁定在 interpreter/lean-toolchain，由 elan 自动获取。
• wasm-tools：用于解码 .wasm 二进制文件并运行 Wasm 测试套件。
  • macOS: brew install wasm-tools
  • Linux: cargo install wasm-tools

测试：

• 运行完整测试套件：just testsuite
• 按文件名过滤测试：just testsuite i32

关键要点

• 统一代码库：Talos 的核心创新在于执行逻辑与形式化证明逻辑共享同一套 Lean 4 代码，消除了维护独立规范解释器的负担和同步风险。
• WP 演算驱动：利用最弱前置条件（WP）演算实现结构化、组合式的证明，有效处理循环、分支和函数调用，避免了解释器的反复展开。
• 语义优先：设计目标是清晰的可推理性而非执行速度，重点关注由 Rust、C 等高级语言编译而来的常见 Wasm 语义子集。
• 模块化依赖：采用单仓库多包结构（Interpreter -> CodeLib -> Programs），通过重新导出机制简化下游项目的依赖管理。
• 活跃开发中：项目目前处于早期阶段，API 和接口可能变动，适用于对形式化验证有需求的开发者进行实验和集成。

意义与影响

Talos 的出现为编译器正确性验证和系统软件形式化验证提供了一种新的范式。通过消除“执行语义”与“形式化规范”之间的鸿沟，它降低了构建可信编译器和验证 Wasm 程序行为的门槛。

对于依赖 WebAssembly 作为安全沙箱或跨平台目标语言的项目而言，Talos 提供了一种在 Lean 生态系统中直接验证 Wasm 程序属性的手段。这不仅有助于发现潜在的安全漏洞，还能在数学上保证程序行为的正确性。虽然目前性能并非其首要目标，但其清晰的推理结构为未来构建高性能且经过形式化验证的 Wasm 执行环境奠定了坚实的基础。