Technical Summary: Satisfiability Modulo Extensional Constant Arrays

Problem Statement

Reasoning about array data structures, particularly in combination with machine integers, is a fundamental requirement for hardware and software verification. The standard Satisfiability Modulo Theories (SMT) theory of extensional arrays, as defined in SMT-LIB and axiomatized by McCarthy, provides select (read) and store (write) operators along with an extensionality axiom. While sufficient for many verification tasks, this theory lacks succinctness when modeling arrays initialized with a default value (e.g., zero-initialized memory).

In the standard theory, such initialization must be expressed via deeply nested store expressions writing the default value to every relevant index. This leads to modeling inaccuracies (indices can only be explicitly overwritten) and severe inefficiencies in solving procedures due to the depth of the store chains.

Extending the theory with constant arrays—arrays that store a single element at every index—offers a succinct solution. However, existing decision procedures for extensional constant arrays are restricted to infinite index domains. For finite index domains, existing SMT solvers either support only non-extensional fragments or, in the case of some solvers, produce incorrect answers when reasoning about extensionality over constant arrays with finite indices. The core challenge lies in determining whether two sequences of store operations over different constant arrays with finite domains can be made equal by sufficiently updating the indices, a problem that does not arise in the infinite case.

Methodology

The authors present a novel decision procedure for the theory of extensional constant arrays ($T_{\langle A \rangle}$) that supports arbitrary index domains, including finite ones. The procedure is formalized as an abstract calculus, CAEXT, which generalizes and extends the Lemmas on Demand (LOD) procedure for extensional arrays (DPA) presented in prior work.

The Calculus CAEXT

The calculus operates on configurations $\langle A, I, \pi \rangle$, where $A$ is a set of flat literals, $I$ is an interpretation in the empty theory ($T_E$), and $\pi$ is a map of propagation steps. The procedure avoids the introduction of virtual reads for all indices (which is infeasible for infinite domains and computationally expensive for large finite domains) by propagating default values and tracking updated indices.

Key components of the calculus include:

1. Base Calculus (AEXT): Generalizes the LOD procedure to arbitrary index and element sorts, decoupling it from specific theory combinations. It propagates read information based on McCarthy's read-over-write axioms (row-eq, row-ne) and the extensionality axiom (ext).
2. Constant Array Extension:
   • Propagation of Default Values: Instead of generating reads for every index, the calculus propagates the default value $v$ of a constant array $\langle v \rangle$ to other arrays. It maintains a set of updated indices $I(a, \langle v \rangle)$, representing indices where the array $a$ differs from the default value $\langle v \rangle$ along the propagation path.
   • Conflict Detection (CongC): When two different default values $v$ and $w$ are propagated to the same array $a$, the calculus checks if the set of updated indices $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ covers the entire index domain. If the domain is finite and the updated indices do not cover all possible indices, a conflict arises unless $v \approx w$.
   • DistinctN Encoding: To handle the quantified formula $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (checking if an un-updated index exists) efficiently, the implementation encodes this as a specialized distinctN constraint. This checks if the set of updated indices contains at least $n$ distinct values, where $n$ is the size of the index domain.

Implementation

The decision procedure is implemented in the state-of-the-art SMT solver Bitwuzla. It integrates seamlessly with Bitwuzla's existing LOD architecture, where the bit-vector solver provides the interpretation $I$. The implementation includes optimizations such as lazy expansion of distinctN constraints and breadth-first search for propagation paths to minimize memory overhead.

Key Contributions

1. Generalization of LOD: The authors generalize the LOD procedure for extensional arrays with fixed-size bit-vectors to arbitrary index and element sorts.
2. Abstract Calculus AEXT: They present AEXT as a decoupled, abstract calculus for the extensional theory of arrays, independent of the LOD solving paradigm.
3. Extension to Constant Arrays (CAEXT): They extend AEXT to handle extensional constant arrays, proving refutational soundness (if unsat is reported, the input is unsatisfiable) and satisfiability soundness (if a saturated configuration is reached without unsat, the input is satisfiable).
4. Implementation and Evaluation: The procedure is implemented in Bitwuzla and evaluated on diverse benchmarks, demonstrating significant performance improvements over baseline Bitwuzla and other leading solvers (Z3, cvc5, MathSAT5).

Results

The evaluation was conducted on five benchmark sets: smtlib (quantified logics), mbqi (subqueries from model-based quantifier instantiation), k-ind (incremental hardware model checking), hevm (Ethereum virtual machine), and crafted (synthetic benchmarks specifically designed to test finite constant array extensionality).

• Performance: Bitwuzla with the new procedure (Bitwuzla⟨A⟩) significantly outperformed all other solvers. On the smtlib set, the number of solved benchmarks increased by a factor of 5 compared to the baseline Bitwuzla (3,545 vs. 717). On the mbqi set, Bitwuzla⟨A⟩ solved all 4,147 queries, whereas the baseline solved only 4.
• Correctness: On the crafted⟨A⟩ set, which encodes equalities over finite constant arrays with different default values, Bitwuzla⟨A⟩ was the only solver to provide correct answers for all instances. Z3 and MathSAT5 accepted the inputs but reported wrong answers for a significant number of benchmarks. cvc5 and baseline Bitwuzla rejected the inputs entirely due to lack of support.
• Soundness Verification: The authors verified the models produced by the solvers on the crafted⟨A⟩ set. Only Bitwuzla⟨A⟩ produced models consistent with its own satisfiability claims. Z3 and MathSAT5 produced models that, when asserted back to the original formulas, led to contradictions.

Significance

The paper claims that the proposed decision procedure significantly expands the solving capabilities of Bitwuzla, enabling it to handle problems involving extensional constant arrays with finite index domains that were previously unsolvable or handled incorrectly by other tools.

The work addresses a critical gap in SMT solving: while constant arrays are a standard modeling pattern for memory initialization, existing solvers either lack support for them in finite domains or provide unsound results. By providing a sound and complete decision procedure for the full theory of extensional constant arrays (both finite and infinite), this work enables more accurate and efficient verification in applications such as hardware model checking and smart contract verification (specifically for the Ethereum Virtual Machine). The authors note that while their evaluation focused on finite domains, the procedure is agnostic to the underlying solver architecture and fully supports the infinite domain case as well.