技術概要：Lean におけるビットベクトルと有限体の等価性証明の自動化

問題定義

ゼロ知識証明（ZKP）回路エンコーディングの検証は、ビットベクトル演算（$2^N$ 法での標準的な機械語演算）と有限体演算（大きな素数 $P$ 法での演算）を同時に使用する量化自由な命題の証明という、決定的な課題に直面しています。ZKP システムは、ビットベクトル論理を有限体の多項式としてエンコードする「算術化」を頻繁に必要とします。これらのエンコードが正しいことを保証することは ZKP システムの健全性にとって不可欠ですが、それらの構築は誤りを起こしやすいものです。

既存の検証ワークフローは、主に以下の 2 つの制限に悩まされています：

1. 手動検証: Lean などの対話型定理証明器（ITP）に ZKP システム全体を埋め込むことは強力な保証を提供しますが、多大な人的努力を必要とします。ZKP の最適化が急速に進化するにつれ、これらの手動証明は頻繁に大幅な手直しを必要とします。
2. 自動 SMT 検証: 検証を充足可能性理論（SMT）クエリに還元することはより高い自動化をもたらしますが、以下の 2 つの根本的な問題に直面します：
   • 理論変換: SMT ソルバーは、有限体とビットベクトル間の変換をネイティブにサポートしていません。ビット分割のような回避策は過剰な変数を導入し、範囲チェックはソルバーのパフォーマンスを低下させる複雑な多項式を必要とします。
   • 信頼コードベース（TCB）: SMT ソルバーは ITP よりもはるかに大きな TCB を持っており、見逃されたバグのリスクを高めています。

手法

著者らは、有限体エンコーディングとそれに対応するビットベクトル意味論間の等価性を自動的に証明するために設計された新しい Lean tactic BitModEq を提示します。このアプローチは、ITP の豊かな意味論を活用して直接型変換を行う一方で、専門的なワークフローを通じて SMT 解決の自動化を維持します。

コアワークフロー

BitModEq は、論文の図 1 に示されるように、4 つの明確なフェーズで動作します：

1. 有限体から自然数への変換: 有限体（$FP$）のソートを持つすべての項を自然数（$N$）に変換します。これには、toNat などの変換演算子を算術式の内側へ押し込む処理が含まれます。
2. 範囲分析: 変換中に生成される自然数に関する不等式を、専用の範囲分析アルゴリズムを用いて解決します。
3. 自然数からビットベクトルへの変換: 残った自然数の項をビットベクトル（$BV_N$）に変換します。
4. ビットブラスト: 最終的なビットベクトルの等式目標を、Lean に実装された決定手続きである bv_decide を用いて解決します。

主要な技術的コンポーネント

1. 変換計算論（セクション 4.2）
この tactic は、ドメイン間を移動するための一連の変換規則を採用します：

• $FP \to N$: distNat などの規則は、加算や乗算に対して toNat を分配します。重要なのは、この tactic が、モジュラーな巻き戻し（modular wraparound）を排除できる場合（単純な減算を許可）と、排除できない場合（モジュラス $P$ の加算 followed by モジュロ演算を必要とする）を区別することです。sqrBds などの規則は、ビットエンコーディング（$x^2 = x$ となる場合）を検出し、それらを境界（$x \le 1$）に変換します。
• $N \to BV$: distBV などの規則は、演算に対して toBV を分配します。$FP \to N$ のステップとは異なり、これらの規則はターゲット空間が本質的に $2^N$ 法であるため、モジュロ演算子の追加を必要としません。

2. 範囲分析（セクション 4.3）
標準的な Lean tactic（例：omega、linarith）は、大きな係数と複雑な変数依存性により、ZKP の算術化に対してしばしば失敗します。BitModEq は、構文指向の範囲分析計算論を導入します：

• プレースホルダー変数: このアルゴリズムは、複雑な不等式を分解するために、存在量化されたプレースホルダー変数を導入します。
• 分解と除去: 規則は不等式を分解します（例：$a + b \le w$ を $a \le w_1, b \le w_2, w_1+w_2 \le w$ に変換）。その後、仮説や既知の性質（例：有限体の要素は $P-1$ 以下に制限される）から導かれた境界を用いてプレースホルダーを具体化することで、それらを除去します。
• 依存性の処理: 特殊な規則（ineqCases、ineqXOR）は、ビット（0 または 1）をシミュレートする変数に対してターゲットを絞った場合分けを行い、標準的な算術ソルバーが見逃す依存関係を解決します。

3. 実装
この tactic は Lean 4.23.0 で実装されており、補題には mathlib を、最終的なビットブラスト段階には bv_decide を利用しています。これは証明チェックのために Lean のカーネルに依存しており、最小限の信頼計算ベース（TCB）を確保しています。

主要な貢献

1. BitModEq Tactic: 有限体演算をビットベクトルに変換し、ビットブラストを通じて生成された目標を解決する Lean tactic。これにより、ITP の正しさの保証を維持します。
2. 実世界エンコーディングの限界付き検証: 2 つの実世界の ZKP システム（Jolt と CirC）の概念実証としての検証を行い、以前の手法よりも高いビット幅の境界を達成しました。
3. 専門的な範囲分析: 変換に起因する目標を証明するための新しい Lean tactic。ZKP の算術化に共通する変数依存性や不等式制約を処理するように特別に設計されています。

結果と評価

著者らは、Jolt（zkVM）とCirC（zkVM コンパイラ）から抽出されたベンチマークを用いて、BitModEq を最先端の SMT ソルバー（特に完全および分割グロブナー基底を備えた cvc5）と比較評価しました。

• パフォーマンス: BitModEq は、最高性能の SMT 設定よりも19% 多くのベンチマークを解決しました。
  • Jolt ベンチマーク（8 ビットおよび 32 ビットルックアップテーブル）において、BitModEq は cvc5（弱いエンコーディング）よりも 8 ビットで 3 つ、32 ビットで 7 つ多くのインスタンスを解決しました。
  • CirC ベンチマークにおいて、BitModEq はテストされた 17 のビット幅のうち 13 でより多くのインスタンスを解決しました。
• スケーラビリティ: cvc5 はより小さなビット幅では優れたパフォーマンスを発揮しましたが、ビット分割による変数の爆発により、ビット幅が増加するにつれてパフォーマンスが著しく低下しました。一方、BitModEq は 32 ビット入力まで効果的にスケーリングしました。
• 効率性: 除去実験（ablation study）により、カスタムの範囲分析が重要であることが示されました。場合分けを削除すると、解決されたベンチマーク数が大幅に減少しました（例：CirC で 737 から 720 に、Jolt で 24 から 21 に）。カスタム分析を標準的な Lean tactic（ring_nf、linarith など）に置き換えると、解決されたインスタンス数が劇的に低下しました（例：CirC で 434 対 737）。
• 実行時間: 範囲分析は総実行時間の約 52% を占め、次いで変換（23%）、ビットブラスト（21%）が続きます。
• バグの発見: CirC の評価中、著者らは整数オーバーフローに関連する 32 ビット算術右シフト実装における健全性のバグを特定しました。これはより小さなビット幅では検出されませんでした。

意義と主張

本論文は、BitModEq がITP の健全性と自動推論を組み合わせることで、現在の ZKP 検証ワークフローの特定の制限に対処していると主張しています。有限体の制約をビットベクトルに戻して変換することで、このアプローチは SMT 理論変換のパフォーマンスボトルネックと、SMT ソルバーの大きな TCB を回避します。

著者らは、このアプローチが、現代の ZK システムで一般的なパターンである有限体内でビットレベルの操作をシミュレートする ZKP の算術化に対して特に効果的であることを強調しています。この手法は完全ではありません（特定の複雑な依存関係や逆数などの分野固有の操作に対して「不明」と返す場合があります）が、以前は自動ツールでは扱えなかった実世界のエンコーディングを正常に検証し、これらの重要な暗号コンポーネントの正しさについてカーネルチェックされた証明を提供します。