Talos: 用于 Lean 4 形式化推理的开源 WASM 解释器
Talos 是一个使用 Lean 4 开发的开源 WebAssembly (Wasm) 解释器，它允许用户执行 Wasm 程序并对其行为进行形式化证明。通过在执行和形式化验证中使用单一的代码库，Talos 消除了维护单独规范解释器的需求，确保了程序的求值过程及其正确性证明保持完全同步。
用于形式化验证的可执行语义
Talos 为 WebAssembly 提供了一套功能完备的可执行语义，将 Wasm 环境视为一个形式化对象。这种架构允许开发者在同一个系统中执行两个主要操作：
- 程序执行：用户可以在具体输入上运行 Wasm 程序以观察其行为。
- 形式化证明：用户可以针对程序行为陈述并证明定理，例如相对于规范的正确性、两个不同程序之间的等价性，或者在所有可能输入下均成立的属性。
为了优先考虑形式化推理，Talos 在设计上优化了推理的清晰度而非原始执行速度。该项目专注于 Rust 和 C 等高级源语言通常生成的 Wasm 特性子集，从而确保验证所需的关键语义优先于性能优化。
推理基础：最弱前置条件演算 (Weakest Precondition Calculus)
Talos 中的形式化证明是使用 最弱前置条件 (WP) 演算 实现的，这是一种谓词转换语义的形式。这种方法允许开发者从期望的后置条件反向推理，以确定保证该条件成立的前置条件。
通过使用 WP 演算，Talos 为复杂的程序结构（包括循环、分支和函数调用）提供了结构化且具有组合性的证明。这避免了在证明过程的每一步都需要重新展开解释器的状态，使得 Wasm 程序的验证变得更加易于管理。
项目架构与仓库布局
Talos 被组织为一个 monorepo，包含三个具有严格依赖链的 Lake package：
| Package | Path | Purpose |
|---|---|---|
Interpreter |
interpreter/ |
包含 Wasm AST、语义以及 WP tactic 层 |
CodeLib |
codelib/ |
提供提升引理 (lifting lemmas) 和程序推理辅助工具 |
Programs |
programs/ |
包含具体的 Rust-to-Wasm 验证任务 |
对于将 Talos 作为依赖项集成的开发者，Interpreter 包提供了核心的 Wasm 语义和 WP 演算，而 CodeLib 则增加了更高级别的推理辅助工具，并重新导出了解释器所需的必要部分。
入门指南与工具链
Talos 需要 Lean 4 和 wasm-tools（用于解码 .wasm 二进制文件并运行测试套件）。用户可以使用 runner 可执行文件运行 .wat 模块：
cd interpreter
lake exe runner samples/factorial.wat fact 5
为了防止执行过程中出现死循环，Talos 包含了一个燃料限制 (fuel cap) 机制（默认为 1,000,000 步），可以通过 --fuel 标志进行调整。在 Interpreter/Wasm/Examples/Factorial.lean 文件中提供了一个关于阶乘函数正确性证明的完整示例。