技術的概要：拡張定数配列に関する充足可能性

問題定義

ハードウェアおよびソフトウェア検証において、特に機械整数と組み合わせた配列データ構造に関する推論は、基本的な要件である。SMT-LIB で定義され、マッカーシーによって公理化された標準的な充足可能性理論（SMT）の拡張配列理論は、select（読み取り）およびstore（書き込み）演算子と拡張性公理を提供する。多くの検証タスクに対しては十分であるが、この理論はデフォルト値（例：ゼロ初期化されたメモリ）で初期化された配列をモデル化する際に、簡潔性に欠ける。

標準理論では、そのような初期化は、デフォルト値をすべての関連インデックスに書き込む、深くネストされたstore 式を通じて表現されなければならない。これにより、モデル化の不正確さ（インデックスは明示的に上書きされる場合に限られる）および、ストアチェーンの深さに起因する解決手順における深刻な非効率性が生じる。

定数配列（すべてのインデックスで単一の要素を格納する配列）による理論の拡張は、簡潔な解決策を提供する。しかし、既存の拡張定数配列の決定手続きは、無限インデックス領域に制限されている。有限インデックス領域の場合、既存の SMT ソルバーは非拡張的なフラグメントのみをサポートするか、あるいは一部のソルバーの場合、有限インデックスを持つ定数配列における拡張性に関する推論において誤った答えを出力する。核心的な課題は、異なる定数配列に対するストア操作のシーケンスが、インデックスを十分に更新することで等しくなり得るかどうかを決定することであり、これは無限の場合には生じない問題である。

手法

著者らは、有限のものを含む任意のインデックス領域をサポートする、拡張定数配列の理論（$T_{\langle A \rangle}$）に対する新規の決定手続きを提示する。この手続きは、CAEXTという抽象計算として形式化され、先行研究で提示された拡張配列に対する要求に基づく補題（LOD）手続き（DPA）を一般化し、拡張する。

計算 CAEXT

この計算は、$\langle A, I, \pi \rangle$という構成上で動作する。ここで、$A$は平坦なリテラルの集合、$I$は空理論（$T_E$）における解釈、$\pi$は伝播ステップのマップである。この手続きは、すべてのインデックスに対する仮想読み取りの導入（無限領域では非現実的であり、大規模な有限領域では計算コストが高いため）を回避し、代わりにデフォルト値を伝播させ、更新されたインデックスを追跡する。

計算の主要な構成要素は以下の通りである：

1. 基本計算（AEXT）: 固定サイズのビットベクトルを持つ拡張配列に対する LOD 手続きを、任意のインデックスおよび要素ソートに一般化し、特定の理論の組み合わせから切り離す。これはマッカーシーの読み書き公理（row-eq、row-ne）および拡張性公理（ext）に基づいて読み取り情報を伝播させる。
2. 定数配列の拡張:
   • デフォルト値の伝播: すべてのインデックスに対する読み取りを生成する代わりに、この計算は定数配列$\langle v \rangle$のデフォルト値$v$を他の配列に伝播させる。伝播経路に沿って配列$a$がデフォルト値$\langle v \rangle$と異なるインデックスを表す更新されたインデックスの集合$I(a, \langle v \rangle)$を維持する。
   • 矛盾検出（CongC）: 異なるデフォルト値$v$と$w$が同じ配列$a$に伝播された場合、更新されたインデックスの集合$I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$がインデックス領域全体をカバーするかどうかを確認する。領域が有限であり、更新されたインデックスがすべての可能なインデックスをカバーしない場合、$v \approx w$でない限り矛盾が生じる。
   • DistinctN エンコーディング: 未更新のインデックスが存在するかどうかを確認する量化式$\exists i : \sigma. \bigwedge_{k \in I} i \neq k$を効率的に処理するために、実装はこの式を特殊なdistinctN 制約としてエンコードする。これは、更新されたインデックスの集合が、インデックス領域のサイズ$n$以上の少なくとも$n$個の異なる値を含んでいるかどうかを確認する。

実装

この決定手続きは、最先端の SMT ソルバーBitwuzlaに実装されている。ビットベクトルソルバーが解釈$I$を提供する Bitwuzla の既存の LOD アーキテクチャとシームレスに統合されている。実装には、distinctN 制約の遅延展開や、メモリオーバーヘッドを最小化するための伝播経路の幅優先探索などの最適化が含まれている。

主要な貢献

1. LOD の一般化: 著者らは、固定サイズのビットベクトルを持つ拡張配列に対する LOD 手続きを、任意のインデックスおよび要素ソートに一般化した。
2. 抽象計算 AEXT: 彼らは、LOD 解決パラダイムに依存しない、拡張配列の理論のための切り離された抽象計算として AEXT を提示した。
3. 定数配列への拡張（CAEXT）: 彼らは AEXT を拡張して拡張定数配列を処理できるようにし、反証的健全性（unsat が報告された場合、入力は充足不可能である）および充足可能性健全性（unsat なく飽和構成に到達した場合、入力は充足可能である）を証明した。
4. 実装と評価: この手続きは Bitwuzla に実装され、多様なベンチマークで評価された。その結果、ベースラインの Bitwuzla および他の主要なソルバー（Z3、cvc5、MathSAT5）と比較して、大幅なパフォーマンスの向上が示された。

結果

評価は、5 つのベンチマークセットで行われた：smtlib（量化論理）、mbqi（モデルベースの量化子インスタンス化からの部分クエリ）、k-ind（インクリメンタルハードウェアモデル検査）、hevm（Ethereum 仮想マシン）、およびcrafted（有限定数配列の拡張性をテストするために特別に設計された合成ベンチマーク）。

• パフォーマンス: 新しい手続きを備えた Bitwuzla（Bitwuzla⟨A⟩）は、すべての他のソルバーを大幅に上回った。smtlib セットでは、ベースラインの Bitwuzla と比較して解決されたベンチマーク数が 5 倍に増加した（3,545 対 717）。mbqi セットでは、Bitwuzla⟨A⟩は 4,147 件のクエリすべてを解決したが、ベースラインは 4 件しか解決しなかった。
• 正しさ: 異なるデフォルト値を持つ有限定数配列上の等式をエンコードしたcrafted⟨A⟩ セットにおいて、Bitwuzla⟨A⟩はすべてのインスタンスに対して正しい答えを提供した唯一のソルバーであった。Z3 および MathSAT5 は入力を受理したが、多くのベンチマークで誤った答えを報告した。cvc5 およびベースラインの Bitwuzla は、サポート不足により入力を完全に拒否した。
• 健全性の検証: 著者らは、crafted⟨A⟩ セット上でソルバーが生成したモデルを検証した。Bitwuzla⟨A⟩のみが、自身の充足可能性の主張と一貫したモデルを生成した。Z3 および MathSAT5 は、元の式に戻して主張すると矛盾を引き起こすモデルを生成した。

重要性

本論文は、提案された決定手続きが Bitwuzla の解決能力を大幅に拡大し、以前は他のツールでは解決不可能であったか、誤って処理されていた有限インデックス領域を持つ拡張定数配列に関する問題を処理可能にしたと主張している。

この研究は、SMT 解決における重要なギャップに対処している。定数配列はメモリ初期化の標準的なモデル化パターンであるが、既存のソルバーは有限領域におけるそれらのサポートを欠いているか、あるいは健全でない結果を提供している。有限および無限の両方を含む拡張定数配列の完全な理論に対する健全かつ完全な決定手続きを提供することで、この研究は、ハードウェアモデル検査やスマートコントラクト検証（特に Ethereum 仮想マシン向け）などのアプリケーションにおいて、より正確かつ効率的な検証を可能にする。著者らは、評価が有限領域に焦点を当てていたものの、この手続きは基盤となるソルバーアーキテクチャに依存せず、無限領域の場合も完全にサポートしていると指摘している。