💻 computer science

Automated Reasoning with Nested Datatypes

本文引入了一种嵌套数据类型的理论，该理论通过限制数据类型与数组的组合来防止非标准模型，并为该理论提供了一个经证明正确的判定程序，同时在真实世界和人工构建的基准测试上对该程序的实现进行了评估。

原作者： Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli

发布于 2026-07-01

📖 1 分钟阅读☕ 轻松阅读

原作者： Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, Cesare Tinelli

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

想象一下你正在使用两种不同类型的乐高积木来建造一座复杂的数字城市：数据类型（Datatypes）和数组（Arrays）。

数据类型就像是家谱或组织架构图。它们是层级化的。一个“人”可以有一个“孩子”，而这个“孩子”可以有自己的“孩子”。这里的规则很简单：没有人能成为自己的祖先。 你不能有一个家谱，其中一个人是自己的祖父；这会产生逻辑循环（一个环），从而破坏结构。
数组就像是信箱或储物柜。它们是扁平的，允许你通过编号（索引）立即抓取任何物品。你可以往信箱里放任何东西，包括一整棵家谱。

问题：“无限循环”陷阱

论文首先指出，当你天真地将这两个系统结合在一起时，会发生一种危险的故障。

想象你有一个人（一种数据类型），他有一个名为“家庭”的字段。在正常世界里，“家庭”是一个人的列表。但在这个有故障的世界里，“家庭”是一个数组（一个储物柜）。

你把一个特定的人（我们称他为鲍勃）放入了5号储物柜。
然后，你将鲍勃的“家庭”字段定义为5号储物柜。

现在，看看会发生什么：

为了找到鲍勃的家庭，你打开了5号储物柜。
在5号储物柜内部，你找到了鲍勃。
为了找到鲍勃的家庭，你再次打开了5号储物柜。
你再次找到了鲍勃。

你陷入了一个无限循环。在计算机科学中，这被称为非标准模型（non-standard model）。这就像一条正在吞食自己尾巴的蛇。虽然计算机在技术上可能允许这样做，但这破坏了数据结构应该遵循的直觉规则。它创造了一个本不该存在的“环”。

解决方案：“嵌套数据类型”理论

作者们（Tomer Hakak 及其团队）说：“我们需要一本规则手册，来防止这种‘蛇吞尾’的场景。”

他们引入了一种名为**嵌套数据类型（Nested Datatypes）**的新理论。将其想象为为你数字城市制定的严格建筑规范。

规则： 你可以将一棵家谱放入储物柜，也可以将一个储物柜放入家谱中，但是你不能创建一个让你回到原点的路径。
目标： 如果你追踪一条路径——从一个人出发，经过他的家庭数组，到达另一个人，再通过他的家庭数组返回——你绝不能回到最初的那个人那里。

他们是如何修复它的：“翻译器”机器

难点在于，计算机非常擅长检查家谱是否有效，也非常擅长检查储物柜是否有效。但它们并不擅长检查两者的结合是否会产生循环。

作者们构建了一个翻译器（一个判定程序）。它是这样工作的，让我们用一个比喻来说明：

想象你有一个由两种不同类型的碎片组成的拼图：树形碎片和盒子碎片。计算机不知道如何处理混合在一起的碎片并检查是否存在循环。

翻译： 作者的算法获取这个混合的拼图，并将其翻译成计算机能够理解的一种语言。它将“盒子碎片”转化为特殊的“树形碎片”，这些碎片看起来像盒子，但行为逻辑像树。
安全网： 他们在翻译过程中加入了额外的“护栏”（引理/lemmas）。这些护栏确保，如果原始混合拼图中原本存在循环，那么翻译后的树形版本会立即显示出矛盾（就像试图建造一座违背重力的塔）。
检查： 计算机检查翻译后的拼图。
- 如果翻译后的拼图是不可能的（不可满足/unsatisfiable），这意味着原始的混合拼图包含了一个被禁止的循环。
- 如果翻译后的拼图可行，则原始拼图是安全的。

这为什么重要（根据论文）

作者们不仅仅是写了一个理论；他们在名为 cvc5（一个用于验证软件的工具）的真实世界计算机程序中构建了一个原型。

现实世界测试： 他们在来自 Move Prover 的基准测试上测试了它，这是一个用于验证智能合约（数字货币协议）的工具。这些合约经常使用复杂的嵌套数据。
合成测试： 他们创建了专门设计用来诱捕其他求解器进入无限循环的虚假谜题。
结果： 他们的这种新方法成功捕捉到了其他方法错过的循环。在许多情况下，它比用于类似任务的现有工具（Z3）更快、更准确。

总结

简而言之，这篇论文是关于修复一个关于计算机如何理解复杂数据的漏洞。

漏洞： 将“家谱”与“信箱”混合使用，可能会意外创建无限循环，导致一个人成为自己的祖先。
修复： 一套新的规则（嵌套数据类型理论），严格禁止这些循环。
工具： 一个翻译器，它将这些复杂的混合规则转换为计算机可以轻松检查其安全性的格式，确保你的数字数据结构保持逻辑严密且无循环。

技术摘要：嵌套数据类型的自动化推理

1. 问题陈述

SMT-LIB 的数据类型理论为列表和树等数据结构提供了便捷的编码方式，这对于软件验证至关重要。然而，由于缺乏更新操作（update operators）和随机访问能力，其表达能力受到了限制。为了解决这一问题，人们通常尝试将数据类型与数组理论进行朴素结合。

本研究确定的核心问题是，这种朴素结合引入了非标准模型（non-standard models）。具体而言，当涉及数组时，原本的无环性原则（acyclicity principle）——即规定数据类型值不能包含其自身——会被绕过。一个数据类型值可能会出现在一个数组的元素中，而该数组本身又是该数据类型值的一个字段。这便创建了一个循环，而标准的理论组合（通过 Nelson-Oppen 方法）无法检测到该循环，因为该循环被“拆分”到了数据类型和数组组件之间。这些非-标准模型是不理想的，因为它们不符合用于验证的嵌套数据结构的直观语义。

2. 方法论

作者提出了一种显式排除这些非标准模型的嵌套数据类型理论。该方法论包含两个主要部分：形式化定义该理论以及基于归约（reduction）的判定程序。

2.1. 形式化定义

该理论通过限制数据类型与数组的标准组合来定义。

良基性（Well-foundedness）： 作者引入了一种新的良基排序（well-founded sorts）定义（定义 10），该定义考虑了数组排序的存在。这确保了即使在涉及数组元素时，数据类型的递归结构仍保持良基。
NDT 关系： 为了排除非标准模型，作者在结构上定义了一个关系 $\mathcal{R}_{\mathcal{A}}$ （定义 16）。该关系将项与其子项以及数组与其元素相连。只有当该关系是良基时，一个结构才被视为有效的 NDT 结构。这有效地排除了数据类型值通过数组间接引用自身的循环情况。

2.2. 判定程序

论文提出了一种判定程序，将嵌套数据类型的满足性问题归约为数据类型、数组和未解释函数（EUF）的（朴素）组合。该程序的操作流程如下：

签名翻译（Signature Translation）： 构建一个新的签名 $\Sigma_{\varphi}$ 。
- 数组排序被拆分为两个组件：一个用于循环检查的数据类型排序 ( $\sigma^*$ )，以及一个用于标准数组推理的数组排序 ( $\sigma'$ )。
- 数据类型构造器被复制以操作新的排序。
- 引入特殊构造器将数组表示为有限元组（finite tuples），以捕捉输入公式中存在的索引所访问的元素。
- 添加未解释函数 ( $f_A, g_A$ ) 以将数组排序表示 ( $\sigma'$ ) 与数据类型排序表示 ( $\sigma^*$ ) 联系起来。
公式翻译（Formula Translation）： 输入公式 $\varphi$ 被翻译为 $\text{trFormula}(\varphi)$ 。
- 标准文字（例如 $x = \text{select}(a, i)$ ）被映射到新签名中的对应项。
- 引理（Lemmas）： 至关重要的是，翻译过程通过一组引理 ( $L(\varphi)$ ) 进行增强，这些引理强制要求原公式中的数组操作与新签名中的基于元组的表示之间保持一致。这些引理确保了“隐藏的循环”在翻译后的公式中得以暴露。
求解（Solving）： 使用能够处理数据类型、数组和 EUF 组合的现有 SMT 求解器（例如通过 Nelson-Oppen 方法）对生成的公式 $\text{trFormula}(\varphi)$ 进行满足性检查。

2.3. 正确性与可判定性

论文证明了在数据类型理论相对于共享排序是稳定无限（stably infinite）的假设下，该翻译保持了满足性（定理 31）。因此，嵌套数据类型理论是可判定的（定理 32）。

3. 主要贡献

本文做出了三个主要贡献：

理论定义： 引入了一种精确的嵌套数据类型理论，防止了由数据类型与数组交互产生的非标准循环模型。
判定程序： 提供了一种基于归约的判定程序，将嵌套数据类型问题转化为增强了未解释函数的标准理论组合。
实现与评估： 在 cvc5 SMT 求解器中进行了原型实现，并进行了经验性评估，以展示该方法的有效性。

4. 实验结果

作者在两个基准测试集上评估了其实现：

合成基准测试（Synthetic Benchmarks）： 系统性设计的公式，旨在创建数据类型与数组之间不同规模的循环。
- 在不可满足实例（存在循环）上，cvc5 解决了所有 500 个基准测试，优于 Z3（Z3 平均解决了 299.8 个，尽管表格显示 Z3 解决的总实例较少）。
- 在可满足实例（循环被打破）上，cvc5 解决了 50 个中的 25 个，而 Z3 仅解决了 1 个。
真实世界基准测试（Real-World Benchmarks）： 源自 Move Prover 验证工具的公式，该工具使用嵌套数据类型来建模智能合约中的持久化数据结构。
- 两个求解器都快速解决了所有 Move Prover 基准测试。
- 在可满足实例上，cvc5 与 Z3 相当或略快。

5. 意义与主张

论文声称，所提出的理论和判定程序成功解决了数据类型与数组组合中的非标准模型问题，而现有的求解器（如 Z3）可能在处理此类问题时虽然能隐式处理，但缺乏精确的理论定义或关于无环性的保证正确性。

作者指出其方法是“有前景的”，表明其在处理现实世界基准测试时具有竞争力，并且在专门测试循环检测能力的合成基准测试上表现优异。他们强调，这项工作是受 Move Prover 需求的驱动，因为其中经常出现此类嵌套结构。

论文的结论较为谦逊，指出虽然目前的工作解决了数组的具体情况，但未检测到的循环问题在其他数据结构（如序列、集合等）中同样存在。作者建议，他们针对数组的解决方案可以作为解决朴素理论组合问题的更通用方案的基础。未来的工作方向包括扩展对增量求解（incremental solving）和量词（quantifiers）的支持。