💻 computer science

Satisfiability Modulo Extensional Constant Arrays (Extended Version)

本文提出了一种针对支持任意索引域的扩展性数组常数组 SMT 理论的新的、可靠的判定过程，克服了以往仅限于有限或无限情形的局限，并通过在 Bitwuzla 求解器中的实现证明了其有效性。

原作者： Mathias Preiner, Aina Niemetz, Clark Barrett

发布于 2026-05-20

📖 1 分钟阅读☕ 轻松阅读

原作者： Mathias Preiner, Aina Niemetz, Clark Barrett

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你是一名侦探，试图解开一个涉及一座庞大、无限图书馆（一个数组）的谜团。每本书都有一个特定的插槽编号（一个索引），并包含一个故事（一个元素）。

在计算机验证的世界里，我们常常需要提出这样的问题：“如果我更改插槽 5 中的故事，插槽 10 中的故事会改变吗？”或者“这两座图书馆是否完全相同？”

长期以来，用于回答这些问题的工具（称为SMT 求解器）存在一个重大盲点。它们非常擅长处理可以更改单本书籍的图书馆，但当图书馆在开始之前就在每一页上都写好了“默认故事”时，它们就束手无策了。

问题：“空白页”困境

想象你有一座图书馆，其中每一本书都以相同的默认故事开头：“结局”。

旧方法：如果你想告诉计算机“好吧，保持所有地方都是‘结局’，但将插槽 5 改为‘第一章’"，计算机必须写出一份庞大且嵌套的列表：“更改插槽 5，然后更改插槽 6，然后更改插槽 7……"一直延伸到无限。
结果：这使得计算机变得缓慢、困惑且容易出错。这就像试图通过逐个列出每一个白色像素来描述一面白墙。

此外，以前的工具只有在图书馆是无限的情况下才能处理这种“默认故事”的概念。如果图书馆是有限的（比如一个只有 4 个插槽的小书架），旧工具通常会给出错误的答案。它们无法推断出，如果你在小板架上覆盖了每一个插槽，那么“默认故事”就不再重要了。

解决方案：“魔法印章”

本文的作者 Mathias Preiner、Aina Niemetz 和 Clark Barrett 构建了一种新的决策过程（侦探的一套新规则），称为CAEXT。

将他们的解决方案想象成一个魔法印章。
你不再需要列出每一本书，现在你可以说：“整个书架都盖上了‘结局’这个故事。”

创新点：他们的新系统无论书架是无限的还是仅仅是一个微小的有限书架，都能处理这种“魔法印章”。
技巧：他们意识到，对于有限书架，你只需要检查是否覆盖了每一个插槽。如果你覆盖了，那么书架现在就只剩下新故事。如果你没有覆盖，那么“默认故事”仍然适用于空余的插槽。

工作原理（“传递接力棒”游戏）

该论文将他们的方法描述为一场传递接力棒的游戏。

设置：你有一个带有“魔法印章”（常量数组）的书架，以及一些特定的更改（更新）。
追逐：系统试图追踪信息的传递路径。如果你更改了插槽 1，这个更改会影响插槽 2 吗？
冲突：有时，系统会发现矛盾。例如，它可能看到“插槽 1 是‘结局’"，但同时“插槽 1 是‘第一章’"。
解决：新规则允许系统说：“等等，如果书架只有 4 个插槽，而我更改了 4 个不同的插槽，那么‘魔法印章’就完全消失了。书架现在只剩下新故事。”

该论文从数学上证明了这套新规则是可靠的。这意味着：

反驳可靠性：如果系统说“这是不可能的”，那么它是 100% 正确的。它永远不会在矛盾上撒谎。
可满足性可靠性：如果系统说“这是可能的”，那么它是 100% 正确的。它永远不会在解的存在性上撒谎。

现实世界测试

作者们不仅撰写了理论，还构建了一个名为Bitwuzla的工具，并将其与其他顶级侦探工具（如 Z3、cvc5 和 MathSAT5）进行了测试。

结果：他们的新工具解决的谜题比其他工具多得多。
陷阱：他们发现，其他工具在面对这些“有限书架”谜题时，经常给出错误的答案。它们会声称一个谜题可解而实际上不可解，或者反之。而使用新“魔法印章”逻辑的 Bitwuzla 每次都给出了正确答案。
应用场景：他们在现实世界的问题上测试了这一点，例如检查硬件设计以及验证以太坊区块链上的智能合约（数字协议）。

总结

简而言之，这篇论文介绍了一种让计算机更智能地推理具有默认值的数据结构的方法。

以前：当处理小型有限数据集上的“默认值”时，计算机既缓慢又困惑。
现在：新方法将这些默认值视为一个易于追踪和覆盖的“魔法印章”，在无限和有限场景中都能完美工作。
影响：这使得用于验证安全关键软件（如自动驾驶汽车或区块链合约）的计算机工具变得更快速、更准确，并且能够解决以前无法解决的问题。

技术摘要：带扩展性常量数组的可满足性模理论

问题陈述

关于数组数据结构的推理，特别是与机器整数结合时，是硬件和软件验证的一项基本要求。SMT-LIB 中定义并由 McCarthy 公理化的标准可满足性模理论（SMT）扩展性数组理论，提供了 select（读）和 store（写）操作符以及一个扩展性公理。虽然该理论足以应对许多验证任务，但在对以默认值初始化的数组（例如零初始化内存）进行建模时，缺乏简洁性。

在标准理论中，此类初始化必须通过深度嵌套的 store 表达式来表达，将默认值写入每一个相关索引。这导致了建模不准确（索引只能被显式覆盖）以及由于存储链的深度而导致求解过程出现严重低效。

通过引入常量数组（即在每个索引处存储单个元素的数组）来扩展该理论，提供了一种简洁的解决方案。然而，现有的扩展性常量数组判定过程仅限于无限索引域。对于有限索引域，现有的 SMT 求解器要么仅支持非扩展性子片段，要么（在某些求解器的情况下）在对具有有限索引的常量数组进行扩展性推理时产生错误答案。核心挑战在于确定：在具有有限域的不同常量数组上，两个存储操作序列是否可以通过充分更新索引而变得相等；这一问题在无限域情况下并不存在。

方法论

作者提出了一种针对扩展性常量数组理论（ $T_{\langle A \rangle}$ ）的新型判定过程，该过程支持任意索引域，包括有限域。该过程被形式化为一个抽象演算 CAEXT，它概括并扩展了先前工作中提出的用于扩展性数组（DPA）的需求引理（LOD）过程。

演算 CAEXT

该演算在配置 $\langle A, I, \pi \rangle$ 上运行，其中 $A$ 是一组扁平文字， $I$ 是空理论（ $T_E$ ）中的解释， $\pi$ 是传播步骤的映射。该过程避免了为所有索引引入虚拟读取（这对于无限域不可行，对于大型有限域计算代价高昂），而是通过传播默认值并跟踪更新后的索引来实现。

该演算的关键组件包括：

基础演算（AEXT）：将 LOD 过程推广到任意索引和元素排序，使其与特定的理论组合解耦。它基于 McCarthy 的读覆盖写公理（row-eq、row-ne）和扩展性公理（ext）传播读取信息。
常量数组扩展：
- 默认值传播：演算不生成每个索引的读取，而是将常量数组 $\langle v \rangle$ 的默认值 $v$ 传播到其他数组。它维护一组更新后的索引 $I(a, \langle v \rangle)$ ，表示在传播路径上数组 $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 中实现。它与 Bitwuzla 现有的 LOD 架构无缝集成，其中位向量求解器提供解释 $I$ 。实现包括优化措施，例如 distinctN 约束的惰性扩展以及用于传播路径的广度优先搜索，以最小化内存开销。

主要贡献

LOD 的推广：作者将用于固定大小位向量的扩展性数组 LOD 过程推广到任意索引和元素排序。
抽象演算 AEXT：他们提出了 AEXT，作为一个解耦的、抽象的演算，用于扩展性数组理论，独立于 LOD 求解范式。
扩展到常量数组（CAEXT）：他们将 AEXT 扩展以处理扩展性常量数组，证明了反驳可靠性（如果报告 unsat，则输入不可满足）和可满足性可靠性（如果达到饱和配置而未报告 unsat，则输入可满足）。
实现与评估：该过程在 Bitwuzla 中实现，并在多样化的基准测试上进行了评估，显示出比基准 Bitwuzla 和其他领先求解器（Z3、cvc5、MathSAT5）显著的性能提升。

结果

评估在五个基准测试集上进行：smtlib（量化逻辑）、mbqi（基于模型的量化器实例化中的子查询）、k-ind（增量硬件模型检测）、hevm（以太坊虚拟机）和 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 求解中的一个关键差距：虽然常量数组是内存初始化的标准建模模式，但现有求解器要么在有限域中缺乏对其的支持，要么提供不可靠的结果。通过为扩展性常量数组的完整理论（包括有限域和无限域）提供可靠且完备的判定过程，这项工作使得在硬件模型检测和智能合约验证（特别是针对以太坊虚拟机）等应用中能够实现更准确、更高效的验证。作者指出，虽然他们的评估侧重于有限域，但该过程与底层求解器架构无关，并且完全支持无限域情况。