技術要約：表現力豊かなリファインメント・タイピングのための基礎的制約解消

問題提起

SMTベースのプログラム検証器は、2つの根本的な限界に直面している：表現力と信頼性である。

1. 表現力: 予測可能な検証は、SMTの決定可能性の境界内に制限される。量化子、ユーザー定義述語、または複雑な理論（例：ビットベクトル）を含む表現力豊かな仕様の推論は、不完全なヒューリスティックに依存することが多く、「証明の不安定性」や予測不可能な検証時間を引き起こす。
2. 信頼性: SMTソルバーは、大規模で未検証のアーティファクトである（例：Z3やCVC4は数十万行のC++コードを含んでいる）。これらのソルバーにおける健全性のバグは、その上に構築されたあらゆるツールの正当性を密かに損なう可能性があり、大きな信頼できる計算基盤（Trusted Computing Base）を生み出してしまう。

現在のアプローチは、仕様が決定可能なSMTフラグメント内に収まるように制限することが多いが、これは低レベルのシステムコードの複雑な特性を検証する能力を犠牲にしている。

手法：Flex

著者らは、定理証明器であるLean内で完全に実装された、基礎的な制約ホーン節（CHC）ソルバーであるFlexを提案する。Flexは、信頼できる基盤をLeanカーネルのみに縮小し、Leanの証明エコシステム全体を活用して低レベルのシステムコードを検証する。

核心となる洞察は、CHCは基礎的な論理における存在量化された命題であるということである。したがって、CHCの解法は、外部のブラックボックスソルバーに頼るのではなく、これらの命題のカーネルでチェック可能な証明を計算するメタプログラム（タクティクス）として再構築できる。

アーキテクチャ

Flexは、Leanタクティクスとして実装された3段階の解法プロセスを通じて動作する：

1. 分割（Partitioning）: ホーン変数を、**非循環的（acyclic）**な変数（「直線的」なコードに由来するもの）と、**循環的（cyclic）**な変数（ループや再帰に由来するもの）に分割する。
2. 非循環的解法（タクティクス zap）: 非循環的変数に対して、制約構造を走査することで最強の解（strongest solution）（正確な閉形式）を計算する。変数のヘッド出現箇所を $\top$（True）に、ボディ出現箇所を計算された解に置き換える。
3. 循環的解法（タクティクス fix）: 循環的変数に対して、Flexは**述語抽象化（predicate abstraction）**を採用する。ユーザーが提供する「修飾子（qualifiers）」のライブラリから導出された初期候補述語の集合を、オラクル（例：grind や aesop）を用いて反復的に弱体化させ、不動点に到達するまで繰り返す。

証明（Certification）

Flexの重要な構成要素は**証明（certification）**である。基礎的な設定においては、制約を書き換えるだけでは不十分であり、システムはその簡約が健全であることを証明しなければならない。

• zap または fix が制約を簡約する際、それらは明示的な証明項（proof term）（サーティフィケート）を構築する。
• このサーティフィケートは、簡約された $\kappa$-freeな検証条件（VC）の証明が、元のCHCの証明を論理的に含意することを実証する。
• Leanカーネルはこれらのサーティフィケートを再チェックし、カーネルを超えたソルバー内部のロジックを信頼することなく、健全性を保証する。

主な貢献

1. 基礎的な解法 (§4)

著者らは、CHCをLeanの命題として浅い埋め込み（shallow embedding）を行い、既存の解法技術をタクティクスとして再構築する方法を示す。

• 非循環的解法: Fusionアルゴリズムを適応して非循環的変数の最強の解を計算し、存在量化子の除去を正当化する証明書を生成する。
• 循環的解法: 述 Predicate Abstraction を基礎的な設定に適応させ、ユーザー定義の理論上で不変量を合成するための拡張可能なオラクルを可能にする。
• 健全性: タクティクスはカーネルが検証可能な証明項を生成するため、ソルバーの出力は信頼できる。

2. 基礎的な生成 (§5)

論文では、FlexをCHCジェネレータと接続することで、2つのエンドツーエンドの基礎的な検証器を実装している：

• 命令型検証器（Imp）: 命令型言語のためのFloyd-Hoareスタイルの検証器であり、ホーン変数はループ不変量の合成をバックエンドのソルバーに委譲する。
• 関数型検証器 ($\lambda_{RK}$): コア関数型計算に対するアルゴリズム的リファインメント・タイピングの最初のメカニゼーションである。これは、未知のリファインメントを推論するためにホーン変数を使用し、充足可能なCHCがソースプログラムがその型の解釈に含まれる値を返し、かつ停止しないことを証明する。

3. 表現力豊かな検証 (§6)

Flexは、Rustのリファインメント型チェッカーであるFluxのバックエンドとして統合されている。

• SMTからの解放: バックエンドとしてLeanを使用することで、仕様がSMTで決定可能であるという制限を取り除く。これにより、量化子や複雑なユーザー定義不変量を必要とする任意の関数的正当性特性の検証が可能になる。
• ケーススタディ: 著者らは、以下のものを含む低レベルのRustライブラリを検証した：
  • インプレースソートアルゴリズム（普遍量化を通じてソート済みであることを証明）。
  • Tock組み込みカーネルのリングバッファ・バックエンド・デック（メモリ安全性と未初期化メモリの回避を証明）。
  • セキュアなメモリ隔離のためのモジュラー算術とビットベクトル特性。
  • チェイニングを持つハッシュテーブル。

結果と評価

著者らは、Fluxの既存のテストおよび新しいケーススタディから派生した880個のCHCからなるベンチマークスイートを用いてFlexを評価した。

• 自動化: Flexは、CHCの**95.7%**を自動的に解消した。
  • 非循環的変数については、zap タクティクスが100%の制約を簡約した。
  • 循環的変数については、fix タクティクスが82.3%のケースで成功した。失敗の主な原因は、再帰制限、修飾子の不足、またはオラクルが最終的なゴールを閉じることができなかったことによるものである。
• 効率 vs 探索: 決定論的な zap タクティクスは、代替手段として使用される探索ベースのタクティクス（grind および aesop）を大幅に上回った。
  • zap は、平均してgrindよりも18倍速く（ハートビート単位）、ウォールクロック時間で13倍速かった。
  • zap は100%の制約を簡約したが、grind は67%、aesop は90%しか簡約できなかった。
• パフォーマンスコスト: 基礎的なアプローチは、SMTベースのバックエンドよりも低速である。Flexは全スイートの解決に約21.8分を要したが、LiquidFixpoint（SMTベース）のバックエンドは31秒であった。著者らは、これが基礎的な保証のために支払うべき「現在の代償」であることを認め、最適化によってこの差を縮めることを期待している。
• 表現力: Flexは、Fluxにおいて以前は不可能であった仕様（普遍量化されたソート済み特性や、マップとモジュラー算術を含む複雑な不変量など）の検証を可能にした。これらは以前はSMTのタイムアウトを引き起こすか、あるいは表現不可能であった。

意義と主張

論文は、Flexがプログラム検証器の設計におけるパラダイムシフトを提示していると主張している：

1. 信頼: 信頼できる計算基盤をLeanカーネルに縮小し、大規模なSMTエンジンにおける健全性のバグのリスクを排除する。
2. 表現力: 基礎的な論理（Lean）の全能力を活用できるようにすることで、SMTの決定可能性を超えた特性を証明することを可能にし、現在のツールの表現力の限界を事実上「飛び越える」ことができる。
3. ハイブリッド・アプローチ: 自動化が検証の大部分を処理できる一方で、自動化が失敗した場合（複雑な不変量などの場合）、ユーザーは不透明なSMTの失敗によってブロックされるのではなく、同じ信頼できる環境内でインタラクティブな証明へとフォールバックできる、実行可能な道筋を提供する。

著者らは、Flexをあらゆる文脈におけるSMTソルバーの置き換えとしてではなく、SMTの制限が以前は進歩を妨げていた、表現力豊かで低レベルなシステムコードの信頼できる検証を可能にする基礎的なバックエンドとして位置づけている。