循环是最常见的编程结构之一，但在形式化验证中对它们进行推理仍然极具挑战性。虽然 Solidity 或任何其他编程语言中的循环看起来很简单——只是重复某个动作直到满足条件——但其验证的复杂性却是呈指数级增长的。形式化验证引擎（如 Certora Prover）必须对所有可能的循环迭代次数进行推理，这会导致所谓的路径爆炸问题（path explosion problem）：随着循环迭代或条件分支数量的增加，Prover 必须探索的可能执行路径呈指数级增长。
为了管理这种复杂性，Certora Prover 及其他形式化验证工具使用了一种称为有界循环展开（bounded loop unrolling）的技术。该技术限制了在验证期间对循环进行符号化探索的次数，使得 Prover 能够避免由未知和无界循环迭代引起的原本不可行的搜索空间。
在本章中，我们将：
- 解释为什么循环难以验证以及路径爆炸问题是如何产生的。
- 展示 Prover 如何使用有界循环展开来缓解此问题。
- 介绍两个配置标志
--loop_iter和--optimistic_loop，它们用于控制循环的探索方式。 - 讨论这些方法的优势和局限性，以及为什么它们无法为未知且无界的循环提供完整且可靠（sound）的证明。
为什么循环难以验证
为了理解为什么循环难以验证，请考虑以下 Solidity 合约，该合约用于跟踪添加到集合数组中的最大数字：
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract MaxInCollection {
uint256[] collection;
uint256 public maxInCollection = 0;
function addToCollection(uint256 x) public {
if (x > maxInCollection) {
maxInCollection = x;
}
collection.push(x);
}
function returnMax() public view returns (uint256) {
uint256 maxTmp = 0;
for (uint256 i = 0; i < collection.length; i++) {
if (collection[i] > maxTmp) {
maxTmp = collection[i];
}
}
return maxTmp;
}
}
在上述合约中，addToCollection() 函数将一个新元素附加到 collection 数组中。每当新元素超过当前最大值时，它还会更新 maxInCollection 状态变量。该合约还包含 returnMax()，它遍历数组以计算并返回最大值。
该合约应该维护的核心属性（不变量）很简单：maxInCollection 应始终等于 returnMax() 返回的值。
让我们在 CVL 中将其表示为**不变量（invariant）**来对其进行形式化验证：
methods {
function maxInCollection() external returns(uint256) envfree;
function returnMax() external returns(uint256) envfree;
}
invariant maxEqReturnMax()
maxInCollection() == returnMax();
乍一看，这个声明似乎是有效的，我们也期望 Prover 能够成功验证它。然而，当我们通过 Certora Prover 运行它时，验证却失败了，如下所示：
看到验证结果后，你可能会感到困惑：如果这两个函数在返回值上逻辑等价，为什么 Prover 仍然无法建立这种等价关系？
答案在于 EVM 执行程序的方式与 Prover 对程序进行推理的方式之间存在根本差异：EVM 使用具体输入执行特定的一条路径，而 Prover 则使用符号输入探索所有可能的路径。
为了理解这种差异，让我们首先研究在合约执行期间发生的事情，然后将其与 Prover 进行符号推理的方式进行对比。
程序遵循一条具体的路径
当我们在实践中使用具体输入（特定的实际值）执行该合约时，程序遵循由这些输入和函数调用顺序决定的单一具体路径。
例如：
- 假设我们按顺序调用
addToCollection(7)、addToCollection(5)和addToCollection(9)。 - 数组
collection变为[7, 5, 9]，并且maxInCollection更新为 9。 - 当我们随后调用
returnMax()时，该函数遍历数组三次并计算出最大值 9。 - 因此
maxInCollection和returnMax()返回相同的结果，证实了最大值被正确追踪。
因此，在具体执行中，程序遵循由给定输入和数组内容定义的单一确定性路径，并且两个函数返回相同的值。
Prover 同时对所有输入进行推理
Certora Prover 是一个符号执行引擎（symbolic execution engine），这意味着它不会一次只使用一个输入来测试程序。相反，它会同时对所有可能的执行进行推理。
为了实现这一点，Prover 逐步进行符号化模拟程序的行为，通过对逻辑约束进行推理，而不是使用具体值。
以下是 Prover 逐步处理不变量 maxEqReturnMax() 的过程：
- **初始状态检查（基本情况）：**第一步是检查在合约的构造函数完成执行后，不变量是否立即成立。
- 在此状态下，
collection数组为空，因此collection.length为0。 maxInCollection状态变量被初始化为0。- 然后，Prover 会符号化地执行
returnMax()函数。它将maxTmp初始化为 0，并遇到该循环：
- 在此状态下，
for (uint256 i = 0; i < collection.length; i++)
由于 collection.length 在初始状态下为 0，因此循环体永远不会运行，函数直接返回 maxTmp，其值保持为 0。
因此，不变量在初始状态下成立，这意味着基本情况已成功验证，如下所示：
-
归纳步骤：在确认不变量在初始状态下成立之后，Prover 进入下一阶段——归纳步骤（inductive step）。此步骤旨在确保在合约发生任何状态更改后，不变量继续成立。
简而言之，Prover 会检查以下内容：
“如果不变量在当前状态 S 下成立，那么它也必须在由任何有效的函数调用产生的下一个状态 S′ 下成立。”
为了对此进行推理，Prover 在概念上遵循三个阶段：
a. 调用前假设：Prover 首先考虑一个任意的、有效的状态
S，在该状态下不变量已经成立。这构成了归纳假设（inductive hypothesis），这是归纳推理中的标准步骤。Prover 不需要知道collection数组的实际内容或maxInCollection的值；它假设——作为证明方法本身的一部分——在这种状态S下，属性maxInCollection() == returnMax()为真。b. 符号执行：接下来，Prover 会模拟一个可能更改合约状态的函数调用。在我们的例子中，它选择了
addToCollection()。至关重要的是，它并没有选择像5或10这样的具体值作为输入传递给addToCollection()。相反，它使用了一个符号变量（symbolic variable） x，它代表该函数可能接收到的任何可能的uint256值。随后，Prover 对
addToCollection(x)的主体进行符号化执行：-
它遇到了
if语句：if (x > maxInCollection)。由于x和maxInCollection都是符号变量，Prover 会进行分支，同时考虑两种可能性：情况 1：
x > maxInCollection。新状态S'中会将maxInCollection更新为x。情况 2：
x <= maxInCollection。新状态S'中maxInCollection将保持不变。
在这两种情况下，它都会符号化执行
collection.push(x)。这意味着在状态S'中，collection数组现在是状态S中的collection加上新元素x，并且collection.length增加了 1。Prover 现在利用旧状态
S和符号输入x获得了关于新状态S'的完整符号化描述。c. 调用后验证：在最后一步中，Prover 必须证明在新的状态
S'下该不变量仍然成立。它会提出疑问：在状态 S’ 下的maxInCollection()是否等于 状态 S’ 下的returnMax()？为了完成此步骤，Prover 会分析此等式的两侧：
-
**等式左侧（
maxInCollection()）：**非常直接。Prover 通过符号化方式已经知晓了maxInCollection的新值（它要么是旧值，要么是x）。 -
等式右侧（
returnMax()）：接下来，它将符号化执行returnMax()函数。这也是验证变得极具挑战性的关键所在，因为returnMax()包含一个循环（loop）：
-
for (uint256 i = 0; i < collection.length; i++) {...}
为什么循环是个问题？
当 Prover 执行到 returnMax() 函数时，它需要符号化执行该循环：
for (uint256 i = 0; i < collection.length; i++) {...}
在具体执行中，循环会运行特定次数——即对数组中的每个元素运行一次。
但对于 Certora Prover 而言，数组长度是符号化的，因此迭代次数是未知的。
这正是问题的关键：Prover 必须同时考虑所有可能的数组长度，从空数组到最大可表示尺寸。单单这一项就已经产生了一个庞大的搜索空间。
在循环内部，还有一个条件语句：
if (collection[i] > maxTmp)
对于符号输入，每次迭代时这个条件可能是 true 或 false。
因此，每次迭代都会使得 Prover 必须考虑的符号路径数量翻倍。
如果数组长度为 n，Prover 大约将面临 2ⁿ 条路径。
例如：
- 2 个元素 ⇒ 4 条路径 (2²)
- 3 个元素 ⇒ 8 条路径 (2³)
- 10 个元素 ⇒ 1024 条路径 (2¹⁰)
- 对于符号化（无界）长度 → 实际上是无法管理的
这种指数级增长使得 Prover 在实际中根本不可能在合理的时间或资源内探索所有路径。
Prover 解决路径爆炸问题的方法
如前所述，Certora Prover 使用有界循环展开来处理此问题。这项技术限制了验证过程中探索循环的次数，默认的边界被设置为一次迭代。一旦达到该限制，Prover 就会停止进一步的探索，因为每次额外的迭代都会使其必须分析的符号路径数翻倍。因此，其余的路径将被处于未证明状态。
在形式化验证中，证明一个不变量要求说明它对于每一个可能的状态转换都成立，包括任何循环的所有迭代。哪怕只有一条潜在的路径没有被检查，证明的归纳步骤也会变得不完整。这就是为什么 Prover 会将不变量 maxEqReturnMax() 标记为失败（failed）：
非常重要的一点是要明白，任何步数无界的计算对 Prover 来说都很难进行符号化推理。而且这种困难并不仅限于你 Solidity 代码中的 for/while 循环。即使在没有可见的显式循环的地方也会出现相同的问题。让我们来考察一个这类隐藏循环的具体例子：Solidity 中的 strings。
Solidity string：隐藏循环的经典案例
为了理解字符串为何会导致“unwinding condition in a loop”（循环展开条件）错误，请考虑下面的智能合约。它将一个字符串存储在状态变量 txt 中，并允许任何人通过 setTxt() 对其进行更新：
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Example {
string public txt;
function setTxt(string memory _txt) external {
txt = _txt;
}
}
现在，考虑以下试图证明存储的字符串始终等于输入值的规范（specification）：
methods{
function setTxt(string) external envfree;
function txt() external returns(string) envfree;
}
rule storedStringShouldEqualToInput() {
string _txt;
//call
setTxt(_txt);
//assertions
assert _txt == txt();
}
如果你用该规范运行 Prover，规则会执行失败：
并且你将看到熟悉的 “Unwinding condition in a loop” 错误，就像之前涉及显式循环的例子一样。
你可能会想，为什么代码中不包含任何显式循环，却出现了这个错误。
原因很简单：存在隐藏循环。
在 Solidity 中，字符串不是单个值，而是一个动态的字节数组。然而，受限于 EVM 的 256 位字长架构，当处理动态数组时，编译器和 EVM 会通过每次复制 **32 字节的块（chunks）**来处理它们。
这种重复的、基于字的复制构成了 Prover 在编译后的字节码中遇到的隐藏循环。
在我们的规范中，在字符串处理期间会触发四个隐藏循环：
-
从
calldata复制到memory（入口点）- **发生了什么：**当你调用
setTxt(_txt)时，输入字符串会到达一个临时的、只读的存储区calldata。为了在函数内实际使用或处理该字符串，EVM 必须首先将其移动到函数的工作区memory中。 - 循环本质：这种传输是每次 32 字节完成的。EVM 循环运行，直到整个字符串被从
calldata移到了memory中。
- **发生了什么：**当你调用
-
从
memory复制到storage（赋值操作）- **发生了什么：**赋值操作
txt = _txt;永久保存了该字符串。它将数据从临时的memory工作区移动到合约的storage中，这是你的合约状态在区块链上的存留之处。 - **循环本质：由于这是永久性写入，EVM 运行一个循环，将字符串逐字（每次 32 字节）**复制到合约指定的存储槽（storage slots）中。这是验证失败的主要环节。
- **发生了什么：**赋值操作
-
从
storage读回到memory（读取操作）- **发生了什么：**当你调用公共 getter 函数
txt()时，合约必须获取存储的字符串数据。它将字符串从其永久的storage位置加载回临时的memory中，以便将其返回。 - **循环本质：**又一个内部循环运行，逐个读取存储中的字符串 32 字节块。
- **发生了什么：**当你调用公共 getter 函数
-
比较字符串（断言操作）
- **发生了什么：**在你的断言
assert _txt == txt();中，Prover 必须检查两个符号字符串是否相等。 - 循环本质：检查两个动态数组是否相等的唯一方法是自始至终逐字进行比较，这就是最后这一个隐藏循环的由来。
- **发生了什么：**在你的断言
对于具体执行（使用特定输入运行代码，例如字符串 "Hello"），这个隐藏循环很简单。字符串的长度是一个已知的、固定的数字，因此循环运行一定的次数。一切都是可预测的。
然而，对于像 Certora Prover 这样的符号执行引擎，输入 _txt 不是一个固定的字符串。它是一个符号值，这意味着它同时代表所有可能的字符串——从空字符串到最大长度的字符串。
Prover 现在被迫要推理一个无界的执行族（unbounded family of executions）。它必须检查属性是否成立，无论字符串的长度是多少或它包含哪些字节。这产生了两个巨大的问题：
问题 1：未知的循环大小（无界搜索）
第一个挑战的出现是因为字符串的长度是符号化的（未知）。这意味着控制 32 字节复制过程的循环计数器也是符号化的。
- 对于某个特定的字符串，循环运行设定的次数（例如，正好 3 次）。
- 对于 Prover 来说，循环可能会运行 任意 次数（例如，0、1、10 或 100 次）。
因此，Prover 不仅必须检查一条执行路径，而是要检查整个路径族，其中每一条路径都对应于字符串可以采用的每一个可能长度。虽然仅这一点就已经造成了庞大的且在技术上是无界的搜索空间，但第二个问题的存在使这个问题呈现出指数级的恶化：循环内部分支。
问题 2：指数级分支（翻倍效应）
因为隐藏循环会频繁遇到条件检查（例如比较当前的 32 字节的字），路径的总数会发生爆炸。由于 Prover 不知道符号化字符串的内容，它无法确定检查的结果。
为了保证正确性，Prover 必须同时探索两种可能性。这就迫使执行路径发生分叉，要求 Prover 探索条件为 true 和条件为 false 的后果。这种探索实际上在循环的每一次单次迭代中都使执行路径的数量翻倍。
举例说明：
- 如果隐藏循环仅运行 3 次，且每次迭代包含一个条件检查，Prover 必须分析
2 x 2 x 2 = 8条独立的路径。 - 如果符号化字符串的长度足以触发 10 次循环迭代，Prover 必须分析
2^10 = 1,024条路径。
这种无界长度和指数级分支的结合就是产生路径爆炸问题的根源，它迅速使验证过程在计算上变得不再可能。
Prover 会被极其庞大且快速增长的可能执行路径数量所压垮，被迫使用有界循环展开在固定数量的迭代后停止探索该循环。
由于 Prover 无法检查所有可能的路径（即它无法为所有符号长度完全展开循环），因此该证明被认为是不完整的（incomplete）。由此，它无法证明该属性对所有可能的字符串都成立，这就是规则 storedStringShouldEqualToInput() 无法成功通过验证的原因。
重新审视其“原因”
我们可以看到，Prover 未能验证 maxEqReturnMax() 和 storedStringShouldEqualToInput() 这两个规则，并不是因为这些属性为假，而是因为 Prover 无法完成对它们的推理。
- 在
maxEqReturnMax()的例子中，returnMax()内部的循环原则上最多可以运行2²⁵⁶−1次 —— 对数组中每一个可能的元素运行一次。如果我们将数组长度表示为n，Prover 必须尝试为n的每一个可能值展开循环，这在计算上是不可行的。 - 在
storedStringShouldEqualToInput()的例子中，txt = _txt内部的隐藏循环可能会对字符串中的每 32 字节运行一次。由于输入长度是符号化的，Prover 必须考虑所有可能的字符串长度，这再次导致了无界探索。
在这两种情况下，根本原因是相同的：Prover 无法符号化地探索无界数量的循环迭代。
这给我们留下了一个问题：对于处理这些情况，我们有哪些选择？
“解决方案”：配置标志
Certora Prover 提供了两个配置选项来帮助处理循环。虽然它们不能提供正确性的完整证明，但它们是控制 Prover 行为的有用工具。
1. 使用 loop_iter 增加展开边界
第一种也是最直接的选项是使用 --loop_iter 标志告诉 Prover 展开循环更多次。这可以从终端或通过配置文件来完成。
从终端执行：
certoraRun confs/<your-config-file>.conf --loop_iter <N>
或在配置文件内部：
{
"files": [
"contracts/<YourContract>.sol:<ContractName>"
],
"verify": "<ContractName>:specs/<your-spec-file>.spec",
"loop_iter": "<N>"
}
在上述终端命令和配置文件的例子中，<N> 指定了 Prover 在停止前将要探索的最大循环迭代次数。
在我们的规则中使用 loop_iter 标志
为了了解 --loop_iter 标志在实际中是如何运作的，让我们将其应用于我们的字符串示例，并使用以下命令运行 Prover：
certoraRun confs/example.conf --loop_iter 3
当我们在使用上述命令运行 Prover 时，在实际中将会发生以下情况：
- Prover 现在将展开隐藏循环的最前 3 次迭代（
txt = _txt内部的字节复制循环）。 - 由于每次迭代复制一个 32 字节的字，这意味着 Prover 可以成功验证最大长度不超过 96 字节（3 × 32 = 96）的字符串的属性。
- 然而，对于长于 96 字节的字符串，Prover 会达到其展开边界。此时，那些路径仍然处于未证明的状态。
- 因此，规则
storedStringShouldEqualToInput()在一般情况下仍然会执行失败，因为 Prover 无法对所有字符串长度证明其正确性。
无论你把界限提高多少，结果都是一样的：任何有限的 --loop_iter 仅仅能证明字符串长度在该数量乘以 32 字节块范围内的属性。更大的字符串仍然未被证明，且增加边界值会迅速减慢 Prover 的速度。
2. 使用 optimistic_loop 跳过边界以外的部分
第二种选项采取了一种截然不同的方法。它不是去增加边界，而是告诉 Prover 去假设边界以外的一切都正常运行。这就是 --optimistic_loop 的作用。
从终端执行：
certoraRun confs/<your-config-file>.conf --optimistic_loop
或在配置文件内部：
{
"files": [
"contracts/<YourContract>.sol:<ContractName>"
],
"verify": "<ContractName>:specs/<your-spec-file>.spec",
"optimistic_loop": true
}
通常情况下，当 Prover 达到其循环边界并看到循环仍可以继续时，它会将该路径标记为未证明。
使用 --optimistic_loop 时，Prover 改变了策略：
- 对于边界以内的迭代，它表现正常并检查每一种情况。
- 对于边界以外的迭代，它会假设该属性继续成立，而不会实际去探索那些路径。
在我们的规则中使用 optimistic_loop 标志
为了了解 --optimistic_loop 标志在实际中是如何运作的，让我们将其应用于我们的字符串示例，并使用以下命令运行 Prover：
certoraRun confs/example.conf --optimistic_loop
当我们使用上述命令运行 Prover 时，在实际中将会发生以下情况：
- Prover 仍会对循环进行少量迭代的探索（它的默认展开边界）。
- 一旦达到该边界，它不会再报告 “unwinding condition in a loop”（循环展开条件）错误，而是假设对所有剩余的情况该属性继续成立。
- 结果就是，即使更长的字符串长度从未得到全面检查，规则
storedStringShouldEqualToInput()现在也能通过验证了。
这种方法之所以被称为“乐观的（optimistic）”，是因为 Prover 本质上是在希望它在最初几次迭代中看到的东西对所有未来的迭代也会保持为真。我们可以看到，使用 --loop_iter，Prover 只会探索到边界值（在我们的例子中是 3 次迭代）。任何更长的路径均处于未证明状态，因此验证失败。然而，使用 --optimistic_loop，Prover 采取了一条捷径：它假设如果该属性在探索到的边界内成立，那么在边界外它也同样成立。这就消除了循环展开带来的失败并使得规则能够通过。
虽然这些标志对于调试和管理验证非常有用，但它们都不能为未知和无界的循环提供完整、可靠（sound）的证明。
--loop_iter是不完整的（incomplete）。--optimistic_loop是不可靠的（unsound）（因为它做出了假设）。
总结
在本章中，我们看到了为什么显式和隐藏循环在形式化验证中都会构成如此重大的挑战。在这两种情况下，Prover 都无法符号化地探索未知且无界数量的迭代。为了取得进展，它依赖于两个配置标志：--loop_iter 和 --optimistic_loop
--loop_iter 标志增加了所探索的迭代次数，但这仅能证明小输入的正确性，因此仍然是不完整的。--optimistic_loop 标志允许 Prover 通过假设其正确来跳过边界之外的部分，但该假设可能是错误的，从而使其变得不可靠（unsound）。
这些变通方法对于调试、快速检查或捕获浅层错误很有帮助。但是，在处理无界循环时，它们无法提供完整的证明。
本文是关于 使用 Certora Prover 进行形式化验证 系列文章的一部分