Movementが形式的検証フレームワークを強化
Movementのaptos-coreリポジトリ内の新しいプルリクエスト（PR #308）は、Lean 4を用いたMove標準ライブラリの形式的検証インフラストラクチャを拡張しています。このアップデートでは、`vector::index_of`関数の包括的な正当性証明と、エラーハンドリング、オプション型、署名者操作、固定小数点演算を含む基礎的な標準ライブラリ操作の新しい仕様モジュールが導入されました。
Vector Index_Ofの精密化証明
このアップデートの中核は、`Refinement/Vector.lean`で927行の新規コードを追加する、`vector::index_of`（`stdModuleEnv`のバイトコードインデックス19）に対する包括的な精密化証明です。この証明は完全な実行経路をカバーしています：ループのセットアップ（`evalProg`からループヘッダまでの7ステップ）、見つかったパス（要素マッチが`(true, k)`を返す）、反復パス（マッチしない場合に`k+1`に進む）。主要な証明技術としては、`(List.map MoveValue.u64 xs).length.toUInt64`を使用してVM ステップ計算にマッチさせることで反射性証明を可能にし、オフセットパラメータを正しく追跡する帰納法の証明に対して`suffices`の一般化を採用しています。証明には、トップレベルの定理`vectorIndexOf_returnValues_found`と`vectorIndexOf_returnValues_notFound`が含まれます。
新しい標準ライブラリ仕様モジュール
このプルリクエストでは、コア標準ライブラリ操作をカバーする5つの新しい仕様モジュールが導入されます：
• Error.lean — 正規エラーコードと中止コード算術
• Option.lean — `option::swap_or_fill`仕様とプロパティ
• Signer.lean — 署名者アドレス抽出操作
• FixedPoint32.lean — `create_from_rational`、`floor`、`ceil`、`round`、`min`、`max`操作を含む固定小数点演算
• BitVector.lean — `new`、`set`、`shift_left`、`is_index_set`などのビットベクトル操作
各モジュールには、バイトコードプログラム、ネイティブ関数モデル、およびMove バイトコード インタプリタに接続する精密化証明が含まれています。
テストと検証
この変更は包括的なテストに合格しています：`lake build`は既存の`sorry`警告のみで正常に完了し、`lake build difftest`微分テスト実行ファイルはエラーなくコンパイルされ、完全な微分テストパイプラインはRustコーパス検証、Move VM オラクル生成、Lean評価器検証全体で227個の合格テストとゼロの失敗を達成しています。
Move開発への重要性
この形式的検証拡張は、Move エコシステムのバイトコードレベルで標準ライブラリ関数の正当性を証明する能力を強化しています。精密化証明は高レベルの Move コードを低レベルのバイトコード実行に接続し、開発者と監査者は重大な操作が正確に仕様どおりに動作することを検証できます。