プログラム検証で Rocq が Lean より適している理由

 (joomy.korkutblech.com)
1 ポイント 投稿者 GN⁺ 2 시간 전 | まだコメントはありません。 | WhatsAppで共有
  • 数学の形式化における Lean の成長は明らかだが、実行可能なプログラム検証には、ネイティブな余帰納、多様な抽出経路、蓄積された検証エコシステムを備える Rocq のほうが適している
  • Rocq は CoInductive と CoFixpoint で余データを宣言し、guardedness を検査したうえで遅延実行コードへ抽出するが、Lean ではライブラリエンコーディング、イテレータ、Thunk、partial def のいずれかを選ぶ必要がある
  • Lean のネストした帰納型検査器は、Rocq が許可する一部の検証関係を拒否するため、JSON スキーマの事例では 1 つの Forall₂ 証明を複数の関係に分離し、別途帰納原理を用意する必要がある
  • Rocq は OCaml、Haskell、Rust、C++、WebAssembly などへのプログラム抽出経路と、Iris、CompCert、Interaction Trees のような検証基盤を提供し、実際のゲームの検証済みロジックを実行コードにつなげられる
  • AI エージェントも文書と事例があれば Rocq コードを書ける。Lean へ移行するには定義だけでなく、抽出パイプライン、ライブラリ、規制・制度上の履歴まで置き換える必要があるため、現時点の作業では実益が乏しい

プログラム検証を基準にした比較

  • 比較対象は数学の形式化ではなくプログラム検証であり、数学分野では Lean が実際の成長の原動力を持っている
  • 「より優れている」とは絶対的な優劣ではなく、現在取り組んでいる作業に Rocq のほうがより合っているという意味である
  • AI の数学分野での成果と Lean への関心が高まるにつれ、Rocq を使い続ける理由をよく質問されるようになり、その論旨は LangSec 基調講演のスライドに端を発している

ネイティブな余帰納型と cofixpoint

  • Lean の coinductive が提供する範囲

    • Lean FRO の Wojciech Różowski と Joachim Breitner が開発した余帰納述語サポートは、Lean 4.25の coinductive コマンドに含まれている
    • この機能は bisimulation と余帰納証明には有用だが、Type における実行可能な cofixpoint や抽出可能なプログラムは提供しない
    • Rocq の CoInductive と CoFixpoint は、実行可能な**余データ（codata）**を Type に直接提供する
    • Lean にはこれに対応するカーネル宣言がないため、通常の関数・構造体またはライブラリエンコーディングを使う必要がある

  • QPFTypes の宣言上の制約

    • Alex Keizer の QPFTypes は、一般的な余データのための概念実証パッケージであり、codata 仕様から destructor、corecursor、bisimulation 原理を生成する
    • Rocq の CoInductive とは異なり、カーネル宣言ではなくライブラリエンコーディングである
    • 例は当時の最新対応版である Lean 4.25.0 固定のツールチェーンを使用している
    • Rocq ではごく普通の次の 3 つの宣言が、QPFTypes では動作しない
      • パラメータなしの余データは実装バグにより失敗する
      • tree と forest のような相互余帰納宣言は、Lean の mutual block 制約のためサポートされない
      • 各ステップで clock インデックスが進む istream のようなインデックス付き余帰納ファミリは、QPF 自体の限界によりサポートされない
    • プロトコル、段階、サイズ、状態機械にもインデックス付き余帰納パターンは使われるが、QPFTypes の単純・非相互・非インデックスの範囲を外れると、低レベルの MvQPF.Cofix.corec と bisim API を直接使う必要があるか、実装できない
    • Rocq も guardedness 検査器の扱いは難しいが、上記の事例は別途エンコーディングせずに宣言できる
    • Paco と Damien Pous の coinduction は余帰納述語と関係証明を支援するが、プログラム用の CoFixpoint を置き換えるものではない

  • 抽出されるプログラムの違い

    • Rocq のネイティブ cofixpoint は実際の遅延 OCaml 値として抽出される
    • game tree library の unfold_cotree は、Lazy.t で包まれた木と再帰的な遅延生成関数になる
    • 出力は人が手書きしそうな遅延木構造に近い
    • QPFTypes では生成と観察が MvQPF.Cofix.corec と MvQPF.Cofix.dest を経由し、抽出されたプログラムも一般化された Cofix 表現を維持する
    • BadCoinduction.lean には、Colist・Cotree、生成されたインターフェース、パラメータなし・相互・インデックス付き余データの失敗例、再現用の QPFTypes コミットとコマンドが含まれている

Lean で選べる代替手段

  • ストリームとイテレータ

    • mathlib の Stream' は Nat → α 関数である
    • 位置 n の要素を計算でき、corecursor・外延性・bisimulation・共帰納補題を提供する
    • しかし、尾が別のストリームである遅延コンストラクタではなく、任意の相互・インデックス付き共データまで解決するわけではない
    • 明示的な状態と step 関数を使う状態機械も corecursor の役割を果たせる
    • Lean の Iter は、要求に応じて 1 ステップずつ計算する逐次インターフェイスである
    • イテレータは値の生成または終了を保証する Productive 証明を持つことができ、Iter.repeat にはすでに提供されている
    • ユーザー定義イテレータには、step インターフェイス・不変条件・必要に応じた生産性証明を自分で与える必要がある
    • Rocq の CoFixpoint は再帰呼び出しの guardedness を検査し、状態機械とシーケンスの間の別個の接続作業なしに共帰納値を返す

  • Thunk, partial def, unsafe def

    • Lean の Thunk は、コンパイル済みコードで初めて強制されたときに計算し、結果をキャッシュするが、共帰納を提供しない
    • 論理上は Unit → α に見えるため、定義全体を証明に使えるが、キャッシュは見えない
    • 再帰を許可したり、再帰が最終的にコンストラクタを生成するかを検査したりもしない
    • Rocq の抽出コードも実行時の遅延性を使うが、まず guardedness 検査に合格する
    • partial def は再帰本体を実行できるが、論理には不透明な定数だけが残る
    • 停止性や生産性を検査しないため、自然数の生成器と、ただちに無限再帰する生成器の両方を許容する
    • unsafe def も実行できるが、theorem-safe な宣言からは参照できない
    • Batteries の MLList は、非公開の unsafe な遅延実装、不透明な公開インターフェイス、partial def で書かれた fix・iterate 生成器を組み合わせる
    • このような生成器は、観察された Rocq cofixpoint のように証明内で展開できない
    • partial_fixpoint は方程式を保持するが、コンストラクタと thunk を組み合わせた再帰は受け入れない
    • QPFTypes は corecursor と bisimulation 原理を提供して不透明性を避けるが、一般化された Cofix 表現と宣言上の制約を受け入れる必要がある

効果を持ち停止しないプログラム

  • Interaction Trees は、効果を持ち停止しない可能性のあるプログラムを共帰納的な木として表現する
    • 同じ木でプログラムの記述・解釈・抽出を行い、通常は weak bisimulation まで含む方程式を証明できる
  • Stream' と Iter はシーケンスだけを提供するため、効果に必要な 分岐 continuation を表現できない
  • Thunk と partial def で効果木を実行すると、再帰生成器が証明に対して不透明になり、計算と証明をともに支援するには共データライブラリによるエンコーディングが必要になる
  • MIT PLV の lean4-itree は、Mathlib の PFunctor.M final coalgebra として Interaction Trees を実装している
  • PolyFun は handler・再帰手続き・実行トレース・strong/weak bisimulation と、monad および iteration 法則の証明を追加する
    • Lean で木を計算し証明できるが、それでもライブラリでエンコードされた M-type である
    • ネイティブな共データ宣言はなく、直接的な遅延プログラムの代わりに一般表現が維持される
  • HITrees もこの制約を回避しない
    • Lean にネイティブな共帰納型がないため、ITrees の共帰納的な Delay-monad アプローチを使わない
    • 木は帰納的であり、非停止は高階再帰効果になる
    • 再帰計算は、観察して展開できる無限木ではなく、handler が効果を解釈するときに意味を得る
    • monadic interpretation で実行し、状態機械の解釈で証明できるが、HITree の方程式理論は一般的な再帰展開方程式を提供しない
  • Rocq は共データ宣言、guarded producer、観察に基づく推論、直接的な遅延コード抽出を 1 つの流れとしてサポートする

ネストした帰納型と述語

  • JSON スキーマ検証の事例

    • Lean は複数のネストした帰納的定義を許可するが、Rocq が受け入れる一部の定義を拒否する
    • この違いは A Rose Tree Is Blooming で使われており、より小さな JSON スキーマの事例で再現できる
    • JSON とスキーマ自体は、どちらの言語でも問題なく定義できる
    • オブジェクトスキーマ検証では、フィールド名が一致し、各 JSON 値が対応する下位スキーマに対して妥当かをペアごとに確認する必要がある
    • Rocq は名前の同一性と再帰的検証を、1つの Forall2 導出に保存できる
    • Rocq 9.0 は、再帰出現の周辺にある tuple-pattern lambda を strict positivity 違反として拒否するが、パターンの代わりに projection を使えばコンパイルできる
    • Lean 4.32.1 は、同じオブジェクトコンストラクタ内で再帰出現が Forall₂ と And の両方を通過すると、内側の And を不正なネスト帰納データ型として拒否する
    • Forall₂ ParRed、And・Exists を通る直接再帰、Forall₂ (fun sf jf => Valid sf.2 jf.2) のような近接した形は許可する
    • 関係パラメータがコンストラクタのローカル変数 env をキャプチャする Forall₂ (Eval env) は、Forall₂ の段階で失敗する

  • 回避方法と証明コスト

    • Lean ではオブジェクト検証を2つの Forall₂ 導出に分けられる
      • 1つはフィールド名の同一性を保持する
      • もう1つは対応する値の再帰的検証を保持する
    • 別のインデックスや長さの証明なしにリスト構造を維持し、head の除去も構造的に証明できるが、2つの導出をどちらも分解する必要がある
    • 関係を分離すると、各名前の同一性と再帰的検証が1つのペアとして結び付いた 単一の証明オブジェクト を失う
    • 相互 ValidFields 関係で結合を復元できるが、Lean の induction タクティックは相互帰納型をサポートしておらず、生成された recursor も関係ごとに motive を要求する
    • ユーザー定義の帰納定理を作れば、この設定を隠せる
    • Rocq は標準の Forall2 表現を維持し、相互定義が必要なら Scheme で結合原理を生成できる
    • Lean もインデックスベースのエンコーディングなしで同じ命題を表現できるが、宣言を再配置し、より多くの証明用の仕組みを作る必要がある
    • 比較ファイル全体は Rocq 9.0.0 用の NestedPain.v と Lean 4.32.1 用の NestedPain.lean にあり、Lean の想定される失敗は #guard_msgs でコンパイル時に検査される

  • ネストした引数に対する強い帰納原理

    • Term が list Term を含む場合のように、ネストしたデータの要素ごとの仮定が必要な証明では、どちらのシステムでもより強い recursor が必要だった
    • Rocq 9.2 は nesting type に All 述語と定理を登録すると、ネストした引数の帰納仮定を生成する
    • 標準ライブラリはこれをデフォルトでは登録しないため、Term 宣言の前に Scheme All for list. という1行を追加する必要がある
    • 生成された Term_ind と Term_rect は app ケースで list_all Term P l の仮定を得て、本体は list_all_forall を呼び出す
    • Scheme All for Forall2. を追加すると、ParRed_ind も Forall2 ParRed args args' 前提に対する帰納仮定を提供する
    • 登録しない場合、既存の弱い原理とともに [register-all] 警告が出る
    • Lean では依然として強い recursor を自分で用意する必要がある

プログラム抽出の選択肢

  • Lean の標準ツールチェーンは独自ランタイムを通じてコンパイルし、Lean ライブラリを作り、ランタイム設計が合う場合には利点がある
  • Kim Morrison の検証済み lean-zip は純粋な Rust の miniz_oxide より高速に圧縮できる場合もあり、性能は印象的である
  • しかし Lean は複数の代替抽出バックエンドを提供しておらず、現在のコンパイルパイプラインには エンドツーエンドの正当性証明 がない
    • Kiran Gopinathan が発見した ランタイムバグ のようなまれな問題が発生しうる
    • 生成コードはランタイムに特化しており、人間が読むようには設計されていない
  • Rocq には、信頼基盤と可読性の間で異なるトレードオフを提供する複数の経路がある

検証済みロジックを実行するゲーム

  • Rocq で実行プログラムと同じソースコードの性質を機械検証したうえで、Crane でロジックとイベントループを C++ に抽出し、rocq-crane-sdl2 で SDL2 に接続する

  • Rocqman

    • Rocqman はフレームループが使うゲーム状態遷移を証明する
      • スコアは減少しない
      • ライフと残りの収集物は増加しない
      • 終了状態は tick の固定点である
      • 一時停止と終了画面への遷移を検査する

  • Rocqsweeper

    • Rocqsweeper は Minesweeper のルールと入力レイヤーを証明する
      • 最初のクリックは安全である
      • フラグ付けは地雷と隣接データを保持する
      • flood fill は地雷を保持し、隠れた安全マスを増やさない
      • カーソルは境界を外れない
      • マウスイベントが想定したセルとして解釈される

  • Reversirocq

    • Reversirocq は Charles C. Norton が追加した Reversi ルール と、同じ game tree library の共帰納的 alpha-beta AI を使う
    • 定理は合法手の列挙とゲーム結果を扱い、探索される有限 prefix で alpha-beta と minimax を結び付ける

  • 検証境界

    • 証明境界は Rocq ソース で終わり、SDL・Crane・生成された C++・ネイティブランタイムは含まない
    • 境界内では、実行プログラムと分離したモデルではなく、実際に実行されるロジックの性質を証明する

Rocq のプログラム検証エコシステム

  • プログラム表現の抽象化

    • Interaction Trees: 外部イベントの共帰納的な木として、効果を持ち終了しない可能性のあるプログラムを表現し、非純粋コードに表示的意味論と等式推論を提供する
    • Choice Trees: 内部の非決定的選択を追加し、並行性などの非決定的システムをモデル化する

  • プログラム検証フレームワーク

    • Iris: 状態と並行プログラムのための高階 concurrent separation logic フレームワーク
    • Iris-Lean も急速に発展し、多くの機能をサポートしているが、Rocq Iris ほど広く使われてはいない
    • CFML: OCaml ソースを Rocq に取り込み、characteristic formula を生成し、高階 separation logic 仕様用のタクティックを提供する
    • Perennial: 並行性、クラッシュセーフなストレージ、分散システムを検証する Iris ベースのフレームワークで、Goose により Go のサブセットの実行プログラムと接続する
    • VST: CompCert の意味論を基盤に C プログラムの関数的正しさを証明する Verified Software Toolchain
    • BRiCk: 実際の C++ プログラム向けのプログラム論理とツールチェーン

  • Rocq バックエンドまたは構成要素を備えたツール

    • Frama-C: C 解析・演繹検証プラットフォームで、証明義務を Rocq に渡すことができる
    • Why3: 独自言語のゴールを複数の証明器に送り、Rocq 用の対話的証明義務をエクスポートできる
    • Cerberus: 実用的で大規模な C サブセットの実行可能な形式意味論であり、CHERI C メモリモデルに Rocq 実装がある

  • 実言語の意味論と検証済みコンパイラ

    • CompCert: 形式検証された最適化 C コンパイラ
    • Vellvm: LLVM IR の Rocq 仕様と抽象意味論、それを精緻化するものとして証明された実行インタプリタを提供する
    • Vélus: Lustre から CompCert の Clight への検証済みコンパイラ
    • WasmCert: WebAssembly の機械化された形式意味論
    • JSCert: ECMAScript 5 仕様を追跡する JavaScript 形式意味論

  • 翻訳ベースの軽量検証

    • hs-to-coq: Haskell ソースを Rocq に翻訳する
    • rocq-of-ocaml: OCaml ソースを Rocq に翻訳する
    • rocq-of-python: Python ソースを Rocq に翻訳する
    • rocq-of-rust: Rust ソースを Rocq に翻訳する
    • Aeneas: borrow check を通過した Rust を検証用の純粋関数モデルに変換し、Lean もターゲットとしてサポートする

  • プログラム合成とパース

    • Fiat Crypto: ブラウザや TLS ライブラリで使える高性能な暗号算術を correct-by-construction 方式で導出する
    • Rupicola: 低水準の関数型 Gallina プログラムを命令型の Bedrock2 プログラムに変換する関係コンパイルツール
    • Narcissus: バイナリ形式の correct-by-construction な encoder と decoder を導出する
    • Verbatim: 正規表現ベースの検証済み lexer
    • CoStar: ALL(*) アルゴリズムベースの検証済み parser

  • メンテナンス状況

    • 一部のプロジェクトは活発にメンテナンスされていないが、エージェントに任せて再ビルドし実行することはできた
    • 必要な要素の一つを Lean に短期間で移植できたとしても、エコシステム全体が蓄積してきた機能と利用実績まで自動的に移るわけではない

規制と認証の実績

  • 規制受容に関する直接的な認証経験はなく、特に欧州の作業者にとってより重要になり得る要素である
  • フランスの ANSSI は Common Criteria 評価で Rocq を使用するための 基準 を公開している
  • CompCert は、AbsInt が Airbus の指針を受けて実施した作業を通じ、2026年に ATR 42/72 航空機の MFC_NG コンピュータ向けに qualification に成功したと述べている
  • Lean への移植が同じ環境でどの要件を満たす必要があるのかは分からず、きれいに移植しても既存の 認証実績 を自動的に継承するわけではない

AI エージェントと移行コスト

  • AI エージェントは Lean しかうまく書けないという前提とは異なり、Rocq コードも十分に書ける
  • Rocq は1980年代後半から存在しており、コードと文書が大量に蓄積されている
  • 現在のモデルは文書と例を与えれば馴染みのない言語にもよく適応するため、人気言語しか知らないという理由は proof assistant を変える長期的な根拠にはならない
  • Lean でも mvcgen や Velvet のような本格的なプログラム検証の取り組みが進行中である
  • 現在の作業を Lean に移すには、定義を再構成し、抽出パイプライン、ライブラリ、制度的実績を置き換える必要があるため、現時点では Rocq の方が適している

関連記事

まだコメントはありません。

まだコメントはありません。