Talos: Lean 4における形式的推論のためのオープンソースWASMインタプリタ
Talosは、Lean 4で開発されたオープンソースのWebAssembly (Wasm) インタプリタであり、ユーザーがWasmプログラムを実行し、その振る舞いを形式的に証明することを可能にします。実行と形式的検証の両方に単一のコードベースを利用することで、Talosは、別途仕様インタプリタを維持する必要性を排除し、プログラムの評価と正当性に関する証明が完全に同期していることを保証します。
形式的検証のための実行可能なセマンティクス
Talosは、Wasm環境を形式的なオブジェクトとして扱うことで、WebAssemblyのための機能的に完全な実行可能なセマンティクスを提供します。このアーキテクチャにより、開発者は同じシステム内で主に2つのアクションを実行できます：
- プログラムの実行: ユーザーは具体的な入力を用いてWasmプログラムを実行し、その振る舞いを観察できます。
- 形式的証明: ユーザーは、仕様に対する正当性、2つの異なるプログラム間の等価性、またはすべての可能な入力に対して保持される特性など、プログラムの振る舞いに関する定理を記述し、証明することができます。
形式的推論を優先するため、Talosは生の実行速度よりも推論の明快さを優先するように意図的に最適化されています。このプロジェクトは、RustやCのような高レベルなソース言語によって通常生成されるWasm機能のサブセットに焦点を当てており、検証に不可欠なセマンティクスがパフォーマンスの最適化よりも優先されるようにしています。
推論の基盤：最弱前置条件（WP）計算
Talosにおける形式的証明は、述語変換セマンティクスの形式である最弱前置条件 (WP) 計算を使用して実装されています。このアプローチにより、開発者は、望ましい事後条件から逆方向に推論を行い、その条件を保証する前置条件を決定することができます。
WP計算を使用することで、Talosは、ループ、分岐、関数呼び出しを含む複雑なプログラム構造に対して、構造化され、合成可能な証明を提供します。これにより、証明プロセスにおける各ステップでインタプリタの状態を再度展開する必要がなくなり、Wasmプログラムの検証がより管理しやすくなります。
プロジェクトのアーキテクチャとリポジトリのレイアウト
Talosは、厳格な依存関係チェーンを持つ3つのLakeパッケージを含むモノリポジトリとして構成されています：
| Package | Path | Purpose |
|---|---|---|
Interpreter |
interpreter/ |
Wasm AST、セマンティクス、およびWPタクティクスのレイヤーを含みます |
CodeLib |
codelib/ |
リフティング補題とプログラム推論ヘルパーを提供します |
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には燃料キャップ（デフォルトで1,000,000ステップ）メカニズムが含まれており、これは--fuelフラグを介して調整可能です。階乗関数の正当性証明の完全な例は、Interpreter/Wasm/Examples/Factorial.leanファイルで確認できます。