Talos: An Open-Source WASM Interpreter for Formal Reasoning in Lean 4

Talos 是一個使用 Lean 4 開發的開源 WebAssembly (Wasm) 解釋器，允許使用者執行 Wasm 程式並正式證明其行為。透過在執行與正式驗證中使用單一程式碼庫，Talos 消除了維護獨立規範解釋器的需求，確保程式的求值與其正確性的證明保持完美同步。

Executable Semantics for Formal Verification

Talos 為 WebAssembly 提供功能完備的可執行語義，將 Wasm 環境視為一個正式對象。這種架構允許開發者在同一個系統中執行兩個主要操作：

  1. Program Execution: 使用者可以在具體輸入上執行 Wasm 程式以觀察其行為。
  2. Formal Proofs: 使用者可以針對程式行為陳述並證明定理，例如符合規範的正確性、兩個不同程式之間的等價性，或是在所有可能輸入下皆成立的屬性。

為了優先考慮正式推理，Talos 有意將推理的清晰度置於原始執行速度之上進行優化。該專案專注於由 Rust 和 C 等高階原始語言通常產生的 Wasm 功能子集，確保驗證所需的關鍵語義優先於效能優化。

Reasoning Foundation: Weakest Precondition Calculus

Talos 中的正式證明是使用 weakest precondition (WP) calculus（最弱前置條件演算）實作的，這是一種謂詞轉換語義的形式。這種方法允許開發者從期望的後置條件反向推理，以確定保證該條件的前置條件。

透過使用 WP calculus，Talos 為複雜的程式結構（包括迴圈、分支和函式呼叫）提供結構化且具組合性的證明。這可以避免在證明過程的每一步都需要重新展開解釋器的狀態，使 Wasm 程式的驗證變得更加易於管理。

Project Architecture and Repository Layout

Talos 被組織為一個包含三個 Lake package 的 monorepo，具有嚴格的依賴鏈：

Package Path Purpose
Interpreter interpreter/ 包含 Wasm AST、語義和 WP tactic layer
CodeLib codelib/ 提供 lifting lemmas 和程式推理助手
Programs programs/ 包含具體的 Rust-to-Wasm 驗證任務

對於將 Talos 作為依賴項整合的開發者，Interpreter package 提供核心 Wasm 語義和 WP calculus，而 CodeLib 則增加了高階推理助手並重新導出解釋器所需的必要部分。

Getting Started and Tooling

Talos 需要 Lean 4 和 wasm-tools（用於解碼 .wasm 二進位檔並執行測試套件）。使用者可以使用 runner 執行檔來執行 .wat 模組：

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

為了防止執行過程中的無限迴圈，Talos 包含一個燃料限制機制（預設為 1,000,000 步），可以透過 --fuel 旗標進行調整。在 Interpreter/Wasm/Examples/Factorial.lean 檔案中提供了一個階乘函數正確性證明的完整範例。

Sources