CVL 中的循环：路径爆炸与循环展开

RareSkills
发布于 2026-02-14 22:31
阅读 22

本文探讨了Certora Prover在形式化验证中处理循环（包括显式和隐式循环）时遇到的路径爆炸问题。文章详细解释了Prover如何通过有界循环展开来缓解这一问题，并介绍了--loop_iter和--optimistic_loop两个配置标志，同时指出了这些方法的局限性（不完整性或不健全性）。

Formal Verification with Certora

## CVL 中的循环：路径爆炸与循环展开

[模块 2：不变式、存储Hook、幽灵变量和形式化验证 Token不变式、存储Hook、幽灵变量和形式化验证 Token](https://rareskills.io/tutorials/certora-book)

最后更新于 2026 年 2 月 13 日

循环是最常见的编程构造之一，但在形式化验证中，对其进行推理仍然具有挑战性。虽然 Solidity 或任何其他编程语言中的循环看起来很简单——只是重复执行一个动作直到满足条件——但其验证会变得指数级复杂。像 Certora Prover 这样的形式化验证引擎必须对所有可能的循环迭代次数进行推理，这导致了所谓的**路径爆炸问题**：随着循环迭代次数或条件分支的增加，Prover 必须探索的可能执行路径呈指数级增长。

为了管理这种复杂性，Certora Prover 和其他形式化验证工具使用一种称为**有界循环展开**的技术。该技术限制了在验证过程中符号性探索循环的次数，从而使 Prover 避免了由未知和无界循环迭代引起的**原本不可行的搜索空间**。

在本章中，我们将：

- 解释**为什么循环难以验证**以及**路径爆炸问题**是如何产生的。
- 展示 Prover 如何使用**有界循环展开**来缓解此问题。
- 介绍两个配置标志 `--loop_iter` 和 `--optimistic_loop`，它们控制循环的探索方式。
- 讨论这些方法的**优缺点**，以及为什么它们不能为**未知和无界**循环提供完整且可靠的证明。

## 为什么循环难以验证

为了理解为什么循环难以验证，请考虑以下 Solidity 合约，它跟踪添加到集合数组中的最大数字：

```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);
    }

在上述合约中，`addToCollection()` 函数将一个新元素附加到 `collection` 数组。它还在新元素超过当前最大值时更新 `maxInCollection` 状态变量。该合约还包含 `returnMax()`，它遍历数组以计算并返回最大值。

该合约应维护的核心属性（不变式）很简单：`maxInCollection` 应该始终等于 `returnMax()` 返回的值。

让我们通过将其表示为 CVL 中的一个**不变式**来形式化验证它：

```solidity
methods {
    function maxInCollection() external returns(uint256) envfree;
    function returnMax() external returns(uint256) envfree;
}
invariant maxEqReturnMax()
    maxInCollection() == returnMax();
```

乍一看，这个声明似乎是有效的，我们期望 Prover 成功验证它。然而，当我们通过 Certora Prover 运行它时，验证失败了，如下所示：

![image](https://img.learnblockchain.cn/2026/02/28/0424cd6cb7e6163a-image1.png)

看到验证结果后，你可能会感到困惑：**如果这两个函数在返回值上逻辑等效，为什么 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 是一个**符号执行引擎**，这意味着它不会一次测试一个程序输入。相反，它同时推理**所有可能的执行**。

为了实现这一点，Prover 逐步符号性地模拟程序的行为，对逻辑约束而非具体值进行推理。

以下是 Prover 如何逐步处理不变式 `maxEqReturnMax()`：

1.  **初始状态检查（基本情况）：** 第一步是检查不变式在合约构造函数执行完毕后是否立即成立。

- 在此状态下，`collection` 数组为空，因此 `collection.length` 为 `0`。
    - `maxInCollection` 状态变量被初始化为 `0`。
    - Prover 然后符号性地执行 `returnMax()` 函数。它将 `maxTmp` 初始化为 0，并遇到循环：

```solidity
    for (uint256 i = 0; i < collection.length; i++)
    ```

由于 `collection.length` 在初始状态下为 `0`，循环体从未运行，函数仅返回 `maxTmp`，它仍然是 `0`。

因此，不变式在初始状态下成立，这意味着基本情况已成功验证，如下所示：

![image](https://img.learnblockchain.cn/2026/02/28/1332fa0e7ae1ed77-image2.png)

2.  **归纳步骤：** 在确认不变式在初始状态下成立后，Prover 进入下一阶段——**归纳步骤**。此步骤旨在确保不变式在合约的任何状态更改后**继续成立**。

简单来说，Prover 检查以下内容：

“**如果不变式在当前状态 S 中成立，那么它也必须在任何有效函数调用导致的新状态 S′ 中成立。**”

为了对此进行推理，Prover 概念性地遵循三个阶段：

a. **调用前假设：** Prover 首先考虑一个任意的、有效的状态 `S`，其中不变式**已经成立**。这构成了**归纳假设**，是归纳推理中的标准步骤。Prover 不需要知道 `collection` 数组的实际内容或 `maxInCollection` 的值；它假设——**作为证明方法本身的一部分**——在此状态 `S` 中，属性 `maxInCollection() == returnMax()` 为真。

b. **符号执行：** 接下来，Prover 模拟一个可能改变合约状态的函数调用。在我们的例子中，它选择 `addToCollection()`。关键是，它不选择像 `5` 或 `10` 这样的特定值作为 `addToCollection()` 的输入。相反，它使用一个**符号变量** `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'` 的完整符号描述，该描述是根据旧状态 `S` 和符号输入 `x` 得出的。

c. **调用后验证：** 在最后一步，Prover 现在必须**证明**不变式在新状态 `S'` 中成立。它会问：_**`maxInCollection()`（在状态 S' 中）是否等于 `returnMax()`（在状态 S' 中）？**_

为了完成此步骤，Prover 分析此等式的两边：
    - **LHS (`maxInCollection()`):** 这很简单。Prover 符号性地知道 `maxInCollection` 的新值（它是旧值或 `x`）。

- **RHS (`returnMax()`):** 接下来，它将符号性地执行 `returnMax()` 函数。这是验证变得具有挑战性的一点，因为 `returnMax()` 包含一个**循环**：

```solidity
    for (uint256 i = 0; i < collection.length; i++) {...}
    ```

### 为什么循环是个问题？

当 Prover 达到 `returnMax()` 函数时，它需要符号性地执行循环：

```solidity
for (uint256 i = 0; i < collection.length; i++) {...}
```

在具体执行中，循环运行**特定次数**——数组中每个元素运行一次。

**但对于 Certora Prover 来说，数组长度是符号性的，因此迭代次数是未知的。**

这是关键点：Prover 必须同时考虑**所有可能的数组长度**，从空数组到最大可表示大小。仅此一点就创造了一个巨大的搜索空间。

循环内部还有另一个条件：

```solidity
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()` 标记为**失败**的原因：

![image](https://img.learnblockchain.cn/2026/02/28/3c60ac847343a698-image3.png)

理解任何具有无界步数的计算对于 Prover 进行符号推理都是困难的，这一点非常重要。而且这种困难不仅限于 Solidity 代码中的 `for/while` 循环。即使在没有明确可见循环的地方，也会出现相同的问题。让我们检查一个这种隐藏循环的具体示例：**Solidity 字符串**。

## Solidity `string`：**隐藏循环**的经典案例

要理解字符串如何导致“**循环中的展开条件**”错误，请考虑以下智能合约，它将一个字符串存储在状态变量 `txt` 中，并允许任何人通过 `setTxt()` 更新它：

```solidity
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract Example {
    string public txt;

function setTxt(string memory _txt) external {
        txt = _txt;
    }
}
```

现在，考虑以下规范，它试图证明存储的字符串始终等于输入：

```solidity
methods{
    function setTxt(string) external envfree;
    function txt() external returns(string) envfree;
}

rule storedStringShouldEqualToInput() {

string _txt;

//call
    setTxt(_txt);

//assertions
    assert _txt == txt();

}
```

如果你使用此规范运行 Prover，则规则失败：

![image](https://img.learnblockchain.cn/2026/02/28/e045e54869a67cf3-image4.png)

你将看到熟悉的**“循环中的展开条件”**错误，就像前面涉及显式循环的示例一样。

![image](https://img.learnblockchain.cn/2026/02/28/a680a7db831717a9-image5.png)

你可能想知道为什么在代码不包含任何显式循环的情况下会出现此错误。

**原因很简单：一个隐藏的循环。**

在 Solidity 中，字符串不是单个值，而是字节的动态数组。然而，由于 **EVM 的 256 位字架构**，当你处理动态数组时，编译器和 EVM 通过一次复制**32 字节块**来处理它们。

这种重复的、基于字的复制是 Prover 在编译后的字节码中遇到的**隐藏循环**。

在我们的规范中，在字符串处理过程中触发了**四个隐藏循环**：

1.  **从 `calldata` 复制到 `memory`（入口）**
    - **发生什么：** 当你调用 `setTxt(_txt)` 时，输入字符串会到达一个名为 `calldata` 的临时只读区域。为了实际在函数内部使用或处理该字符串，EVM 必须首先将其移动到函数的**内存（`memory`）**工作区。
    - **循环：** 此传输**每次 32 字节**进行。EVM 循环直到整个字符串从 `calldata` 移动到 `memory`。
2.  **从 `memory` 复制到 `storage`（赋值）**
    - **发生什么：** 赋值 `txt = _txt;` 永久保存字符串。它将数据从临时**内存（`memory`）**工作区移动到合约的**存储（`storage`）**中，这是合约状态在区块链上的存储位置。
    - **循环：** 由于这是永久写入，EVM 会运行一个循环，**逐字（每次 32 字节）**将字符串复制到合约指定的存储槽中。这是验证失败的主要原因。
3.  **从 `storage` 复制回 `memory`（读取）**
    - **发生什么：** 当你调用公共 getter `txt()` 时，合约必须获取存储的字符串数据。它将字符串从其永久**存储（`storage`）**位置加载回临时**内存（`memory`）**中，以便可以返回。
    - **循环：** 另一个内部循环运行，逐个读取字符串的 32 字节字。
4.  **比较字符串（断言）**
    - **发生什么：** 在你的断言 `assert _txt == txt();` 中，Prover 必须检查两个符号字符串是否相等。
    - **循环：** 检查两个动态数组是否相等的唯一方法是**逐字**从头到尾比较它们，这是最后一个隐藏循环的定义。

对于**具体执行**（使用特定输入运行代码，例如字符串 `"Hello"`），这个隐藏循环很简单。字符串的长度是已知的固定数字，因此循环运行确定的次数。一切都是可预测的。

然而，对于像 Certora Prover 这样的**符号执行引擎**，输入 `_txt` 不是一个固定的字符串。它是一个符号值，这意味着它同时代表**所有可能的字符串**——从空字符串到最大大小的字符串。

Prover 现在被迫推理**无限的执行族**。它必须检查属性是否成立，无论字符串的长度或包含的字节是什么。这会产生两个巨大问题：

### **问题 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 无法检查所有可能的路径（即，它无法完全展开所有符号长度的循环），因此证明被认为是**不完整**的。因此，它无法证明该属性适用于**所有**可能的字符串，这就是规则 `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 更多次地展开循环。这可以通过终端或配置文件完成。

从终端：

```bash
certoraRun confs/<your-config-file>.conf --loop_iter <N>
```

或在配置文件中：

```json
{
    "files": [
        "contracts/<YourContract>.sol:<ContractName>"
    ],
    "verify": "<ContractName>:specs/<your-spec-file>.spec",
    "loop_iter": "<N>"
}
```

在上述终端命令和配置文件示例中，`<N>` 指定 Prover 在停止之前将探索的循环迭代的**最大次数**。**结果，剩余的路径未经验证。**

### 在我们的规则中使用 `loop_iter` 标志

为了理解 `--loop_iter` 标志在实践中是如何工作的，让我们将其应用于我们的字符串示例，并使用以下命令运行 Prover：

```solidity
certoraRun confs/example.conf --loop_iter 3
```

当我们使用上述命令运行 Prover 时，实际上会发生以下情况：

- Prover 现在将展开隐藏循环（`txt = _txt` 内部的字节复制循环）最多**3 次迭代**。
- 由于每次迭代复制一个 32 字节的字，这意味着 Prover 可以成功验证长度最多为**96 字节**（3 × 32 = 96）的字符串的属性。
- 然而，对于长度超过 96 字节的字符串，Prover 达到了其展开边界。此时，这些路径仍然**未经验证**。
- 因此，在一般情况下，规则 `storedStringShouldEqualToInput()` 仍将失败，因为 Prover 无法证明所有字符串长度的正确性。

![image](https://img.learnblockchain.cn/2026/02/28/bf4c0173b2b52a7-image6.png)

无论你将边界提高多少，结果都将相同：**任何有限的** `--loop_iter` **只能证明该属性适用于最多该数量的 32 字节字的字符串**。更长的字符串仍**未经验证**，并且增加边界会迅速减慢 Prover 的速度。

### 2. 使用 `optimistic_loop` 跳过边界之外的部分

第二个选项采用了截然不同的方法。Prover 可以被告知**假设**超出边界的一切都运行良好，而不是增加边界。这就是 `--optimistic_loop` 所做的事情。

从终端：

```bash
certoraRun confs/<your-config-file>.conf --optimistic_loop
```

或在配置文件中：

```solidity
{
    "files": [
        "contracts/<YourContract>.sol:<ContractName>"
    ],
    "verify": "<ContractName>:specs/<your-spec-file>.spec",
    "optimistic_loop": true
}
```

通常，当 Prover 达到其循环边界并看到循环可以继续时，它会将该路径标记为**未经验证**。

使用 `--optimistic_loop`，Prover 改变策略：

- 对于**在边界内的**迭代，它正常行为并检查每个案例。
- 对于**超出边界的**迭代，它**假设**属性将继续成立，而无需实际探索这些路径。

### 在我们的规则中使用 `optimistic_loop` 标志

为了理解 `--optimistic_loop` 标志在实践中是如何工作的，让我们将其应用于我们的字符串示例，并使用以下命令运行 Prover：

```solidity
certoraRun confs/example.conf --optimistic_loop
```

**当我们使用上述命令运行 Prover 时，实际上会发生以下情况：**

- Prover 仍然会探索循环少量迭代（其默认的展开边界）。
- 一旦达到该边界，它不会报告“循环中的展开条件”错误，而是**假设**该属性对于所有剩余情况都成立。
- 因此，规则 `storedStringShouldEqualToInput()` 现在通过了验证，即使更长的字符串长度从未完全检查过。

![image](https://img.learnblockchain.cn/2026/02/28/44179df24c5b21-image7.png)

这种方法被称为“**乐观的**”，因为 Prover 实质上**希望**它在最初几次迭代中看到的情况在所有未来的迭代中都保持不变。

我们可以看到，使用 `--loop_iter`，Prover 只探索到边界（在我们的示例中是 3 次迭代）。任何更长的部分都**未经验证**，因此验证失败。然而，使用 `--optimistic_loop`，Prover 采取了捷径：它假设如果属性在探索的边界内成立，那么它在边界之外也成立。这消除了展开失败，并使规则通过。

虽然这些标志对于调试和管理验证很有用，但它们都不能为未知和无界循环提供完整、可靠的证明。

- `--loop_iter` 是**不完整**的。
- `--optimistic_loop` 是**不可靠**的（它做出了假设）。

## 总结

在本章中，我们探讨了显式循环和隐藏循环在形式化验证中为何构成如此重大的挑战。在这两种情况下，Prover 都无法符号性地探索未知且无界的迭代次数。为了取得进展，它依赖于两个配置标志：`--loop_iter` 和 `--optimistic_loop`。

`--loop_iter` 标志增加了探索的迭代次数，但这只证明了小输入的正确性，因此仍然不完整。`--optimistic_loop` 标志允许 Prover 通过假设正确性来跳过边界之外的部分，但该假设可能是错误的，使其不可靠。

这些变通方法对于调试、快速检查或捕获浅层错误很有帮助。然而，在处理无界循环时，它们无法提供完整的证明。

_本文是关于[使用 Certora Prover 进行形式化验证](https://rareskills.io/tutorials/certora-book)系列文章的一部分。_

>- 原文链接： [rareskills.io/post/certo...](https://rareskills.io/post/certora-loops-in-cvl)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

Formal Verification with Certora

CVL 中的循环：路径爆炸与循环展开

模块 2：不变式、存储Hook、幽灵变量和形式化验证 Token不变式、存储Hook、幽灵变量和形式化验证 Token

最后更新于 2026 年 2 月 13 日

循环是最常见的编程构造之一，但在形式化验证中，对其进行推理仍然具有挑战性。虽然 Solidity 或任何其他编程语言中的循环看起来很简单——只是重复执行一个动作直到满足条件——但其验证会变得指数级复杂。像 Certora Prover 这样的形式化验证引擎必须对所有可能的循环迭代次数进行推理，这导致了所谓的路径爆炸问题：随着循环迭代次数或条件分支的增加，Prover 必须探索的可能执行路径呈指数级增长。

为了管理这种复杂性，Certora Prover 和其他形式化验证工具使用一种称为有界循环展开的技术。该技术限制了在验证过程中符号性探索循环的次数，从而使 Prover 避免了由未知和无界循环迭代引起的原本不可行的搜索空间。

在本章中，我们将：

解释为什么循环难以验证以及路径爆炸问题是如何产生的。
展示 Prover 如何使用有界循环展开来缓解此问题。
介绍两个配置标志 --loop_iter 和 --optimistic_loop，它们控制循环的探索方式。
讨论这些方法的优缺点，以及为什么它们不能为未知和无界循环提供完整且可靠的证明。

为什么循环难以验证

为了理解为什么循环难以验证，请考虑以下 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 &lt; collection.length; i++) {
            if (collection[i] > maxTmp) {
                maxTmp = collection[i];
            }
        }
        return maxTmp;
    }
}

在上述合约中，addToCollection() 函数将一个新元素附加到 collection 数组。它还在新元素超过当前最大值时更新 maxInCollection 状态变量。该合约还包含 returnMax()，它遍历数组以计算并返回最大值。

该合约应维护的核心属性（不变式）很简单：maxInCollection 应该始终等于 returnMax() 返回的值。

让我们通过将其表示为 CVL 中的一个不变式来形式化验证它：

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 是一个符号执行引擎，这意味着它不会一次测试一个程序输入。相反，它同时推理所有可能的执行。

为了实现这一点，Prover 逐步符号性地模拟程序的行为，对逻辑约束而非具体值进行推理。

以下是 Prover 如何逐步处理不变式 maxEqReturnMax()：

初始状态检查（基本情况）： 第一步是检查不变式在合约构造函数执行完毕后是否立即成立。
- 在此状态下，collection 数组为空，因此 collection.length 为 0。
- maxInCollection 状态变量被初始化为 0。
- Prover 然后符号性地执行 returnMax() 函数。它将 maxTmp 初始化为 0，并遇到循环：
```
for (uint256 i = 0; i &lt; collection.length; i++)
```
由于 collection.length 在初始状态下为 0，循环体从未运行，函数仅返回 maxTmp，它仍然是 0。

因此，不变式在初始状态下成立，这意味着基本情况已成功验证，如下所示：
归纳步骤： 在确认不变式在初始状态下成立后，Prover 进入下一阶段——归纳步骤。此步骤旨在确保不变式在合约的任何状态更改后继续成立。

简单来说，Prover 检查以下内容：

“如果不变式在当前状态 S 中成立，那么它也必须在任何有效函数调用导致的新状态 S′ 中成立。”

为了对此进行推理，Prover 概念性地遵循三个阶段：

a. 调用前假设： Prover 首先考虑一个任意的、有效的状态 S，其中不变式已经成立。这构成了归纳假设，是归纳推理中的标准步骤。Prover 不需要知道 collection 数组的实际内容或 maxInCollection 的值；它假设——作为证明方法本身的一部分——在此状态 S 中，属性 maxInCollection() == returnMax() 为真。

b. 符号执行： 接下来，Prover 模拟一个可能改变合约状态的函数调用。在我们的例子中，它选择 addToCollection()。关键是，它不选择像 5 或 10 这样的特定值作为 addToCollection() 的输入。相反，它使用一个符号变量 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' 的完整符号描述，该描述是根据旧状态 S 和符号输入 x 得出的。

c. 调用后验证： 在最后一步，Prover 现在必须证明不变式在新状态 S' 中成立。它会问：maxInCollection()（在状态 S' 中）是否等于 returnMax()（在状态 S' 中）？

为了完成此步骤，Prover 分析此等式的两边：
- LHS (maxInCollection()): 这很简单。Prover 符号性地知道 maxInCollection 的新值（它是旧值或 x）。
- RHS (returnMax()): 接下来，它将符号性地执行 returnMax() 函数。这是验证变得具有挑战性的一点，因为 returnMax() 包含一个循环：
```
for (uint256 i = 0; i &lt; collection.length; i++) {...}
```

为什么循环是个问题？

当 Prover 达到 returnMax() 函数时，它需要符号性地执行循环：

for (uint256 i = 0; i &lt; 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() 标记为失败的原因：

理解任何具有无界步数的计算对于 Prover 进行符号推理都是困难的，这一点非常重要。而且这种困难不仅限于 Solidity 代码中的 for/while 循环。即使在没有明确可见循环的地方，也会出现相同的问题。让我们检查一个这种隐藏循环的具体示例：Solidity 字符串。

Solidity `string`：隐藏循环的经典案例

要理解字符串如何导致“循环中的展开条件”错误，请考虑以下智能合约，它将一个字符串存储在状态变量 txt 中，并允许任何人通过 setTxt() 更新它：

// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract Example {
    string public txt;

    function setTxt(string memory _txt) external {
        txt = _txt;
    }
}

现在，考虑以下规范，它试图证明存储的字符串始终等于输入：

methods{
    function setTxt(string) external envfree;
    function txt() external returns(string) envfree;
}

rule storedStringShouldEqualToInput() {

    string _txt;

    //call
    setTxt(_txt);

    //assertions
    assert _txt == txt();

}

如果你使用此规范运行 Prover，则规则失败：

你将看到熟悉的“循环中的展开条件”错误，就像前面涉及显式循环的示例一样。

你可能想知道为什么在代码不包含任何显式循环的情况下会出现此错误。

原因很简单：一个隐藏的循环。

在 Solidity 中，字符串不是单个值，而是字节的动态数组。然而，由于 EVM 的 256 位字架构，当你处理动态数组时，编译器和 EVM 通过一次复制32 字节块来处理它们。

这种重复的、基于字的复制是 Prover 在编译后的字节码中遇到的隐藏循环。

在我们的规范中，在字符串处理过程中触发了四个隐藏循环：

从 calldata 复制到 memory（入口）
- 发生什么： 当你调用 setTxt(_txt) 时，输入字符串会到达一个名为 calldata 的临时只读区域。为了实际在函数内部使用或处理该字符串，EVM 必须首先将其移动到函数的内存（memory）工作区。
- 循环： 此传输每次 32 字节进行。EVM 循环直到整个字符串从 calldata 移动到 memory。
从 memory 复制到 storage（赋值）
- 发生什么： 赋值 txt = _txt; 永久保存字符串。它将数据从临时内存（memory）工作区移动到合约的存储（storage）中，这是合约状态在区块链上的存储位置。
- 循环： 由于这是永久写入，EVM 会运行一个循环，逐字（每次 32 字节）将字符串复制到合约指定的存储槽中。这是验证失败的主要原因。
从 storage 复制回 memory（读取）
- 发生什么： 当你调用公共 getter txt() 时，合约必须获取存储的字符串数据。它将字符串从其永久存储（storage）位置加载回临时内存（memory）中，以便可以返回。
- 循环： 另一个内部循环运行，逐个读取字符串的 32 字节字。
比较字符串（断言）
- 发生什么： 在你的断言 assert _txt == txt(); 中，Prover 必须检查两个符号字符串是否相等。
- 循环： 检查两个动态数组是否相等的唯一方法是逐字从头到尾比较它们，这是最后一个隐藏循环的定义。

对于具体执行（使用特定输入运行代码，例如字符串 "Hello"），这个隐藏循环很简单。字符串的长度是已知的固定数字，因此循环运行确定的次数。一切都是可预测的。

然而，对于像 Certora Prover 这样的符号执行引擎，输入 _txt 不是一个固定的字符串。它是一个符号值，这意味着它同时代表所有可能的字符串——从空字符串到最大大小的字符串。

Prover 现在被迫推理无限的执行族。它必须检查属性是否成立，无论字符串的长度或包含的字节是什么。这会产生两个巨大问题：

问题 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 无法检查所有可能的路径（即，它无法完全展开所有符号长度的循环），因此证明被认为是不完整的。因此，它无法证明该属性适用于所有可能的字符串，这就是规则 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/&lt;your-config-file>.conf --loop_iter &lt;N>

或在配置文件中：

{
    "files": [
        "contracts/&lt;YourContract>.sol:&lt;ContractName>"
    ],
    "verify": "&lt;ContractName>:specs/&lt;your-spec-file>.spec",
    "loop_iter": "&lt;N>"
}

在上述终端命令和配置文件示例中，<N> 指定 Prover 在停止之前将探索的循环迭代的最大次数。结果，剩余的路径未经验证。

在我们的规则中使用 `loop_iter` 标志

为了理解 --loop_iter 标志在实践中是如何工作的，让我们将其应用于我们的字符串示例，并使用以下命令运行 Prover：

certoraRun confs/example.conf --loop_iter 3

当我们使用上述命令运行 Prover 时，实际上会发生以下情况：

Prover 现在将展开隐藏循环（txt = _txt 内部的字节复制循环）最多3 次迭代。
由于每次迭代复制一个 32 字节的字，这意味着 Prover 可以成功验证长度最多为96 字节（3 × 32 = 96）的字符串的属性。
然而，对于长度超过 96 字节的字符串，Prover 达到了其展开边界。此时，这些路径仍然未经验证。
因此，在一般情况下，规则 storedStringShouldEqualToInput() 仍将失败，因为 Prover 无法证明所有字符串长度的正确性。

无论你将边界提高多少，结果都将相同：任何有限的 --loop_iter 只能证明该属性适用于最多该数量的 32 字节字的字符串。更长的字符串仍未经验证，并且增加边界会迅速减慢 Prover 的速度。

2. 使用 `optimistic_loop` 跳过边界之外的部分

第二个选项采用了截然不同的方法。Prover 可以被告知假设超出边界的一切都运行良好，而不是增加边界。这就是 --optimistic_loop 所做的事情。

从终端：

certoraRun confs/&lt;your-config-file>.conf --optimistic_loop

或在配置文件中：

{
    "files": [
        "contracts/&lt;YourContract>.sol:&lt;ContractName>"
    ],
    "verify": "&lt;ContractName>:specs/&lt;your-spec-file>.spec",
    "optimistic_loop": true
}

通常，当 Prover 达到其循环边界并看到循环可以继续时，它会将该路径标记为未经验证。

使用 --optimistic_loop，Prover 改变策略：

对于在边界内的迭代，它正常行为并检查每个案例。
对于超出边界的迭代，它假设属性将继续成立，而无需实际探索这些路径。

在我们的规则中使用 `optimistic_loop` 标志

为了理解 --optimistic_loop 标志在实践中是如何工作的，让我们将其应用于我们的字符串示例，并使用以下命令运行 Prover：

certoraRun confs/example.conf --optimistic_loop

当我们使用上述命令运行 Prover 时，实际上会发生以下情况：

Prover 仍然会探索循环少量迭代（其默认的展开边界）。
一旦达到该边界，它不会报告“循环中的展开条件”错误，而是假设该属性对于所有剩余情况都成立。
因此，规则 storedStringShouldEqualToInput() 现在通过了验证，即使更长的字符串长度从未完全检查过。

这种方法被称为“乐观的”，因为 Prover 实质上希望它在最初几次迭代中看到的情况在所有未来的迭代中都保持不变。

我们可以看到，使用 --loop_iter，Prover 只探索到边界（在我们的示例中是 3 次迭代）。任何更长的部分都未经验证，因此验证失败。然而，使用 --optimistic_loop，Prover 采取了捷径：它假设如果属性在探索的边界内成立，那么它在边界之外也成立。这消除了展开失败，并使规则通过。

虽然这些标志对于调试和管理验证很有用，但它们都不能为未知和无界循环提供完整、可靠的证明。

--loop_iter 是不完整的。
--optimistic_loop 是不可靠的（它做出了假设）。

总结

在本章中，我们探讨了显式循环和隐藏循环在形式化验证中为何构成如此重大的挑战。在这两种情况下，Prover 都无法符号性地探索未知且无界的迭代次数。为了取得进展，它依赖于两个配置标志：--loop_iter 和 --optimistic_loop。

--loop_iter 标志增加了探索的迭代次数，但这只证明了小输入的正确性，因此仍然不完整。--optimistic_loop 标志允许 Prover 通过假设正确性来跳过边界之外的部分，但该假设可能是错误的，使其不可靠。

这些变通方法对于调试、快速检查或捕获浅层错误很有帮助。然而，在处理无界循环时，它们无法提供完整的证明。

本文是关于使用 Certora Prover 进行形式化验证系列文章的一部分。

原文链接： rareskills.io/post/certo...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

翻译
学分: 0
分类: Solidity
标签: 形式化验证 Certora 循环展开路径爆炸 Solidity 符号执行

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

CVL 中的循环：路径爆炸与循环展开

CVL 中的循环：路径爆炸与循环展开

为什么循环难以验证

程序遵循一条具体路径

Prover 同时推理所有输入

为什么循环是个问题？

Prover 应对路径爆炸问题的方法

Solidity `string`：隐藏循环的经典案例

问题 1：未知循环大小（无界搜索）

问题 2：指数级分支（翻倍效应）

重新审视“原因”

“解决方案”：配置标志

1. 使用 `loop_iter` 增加展开边界

在我们的规则中使用 `loop_iter` 标志

2. 使用 `optimistic_loop` 跳过边界之外的部分

在我们的规则中使用 `optimistic_loop` 标志

总结

0 条评论

文章目录

CVL 中的循环：路径爆炸与循环展开

CVL 中的循环：路径爆炸与循环展开

为什么循环难以验证

程序遵循一条具体路径

Prover 同时推理所有输入

为什么循环是个问题？

Prover 应对路径爆炸问题的方法

Solidity string：隐藏循环的经典案例

问题 1：未知循环大小（无界搜索）

问题 2：指数级分支（翻倍效应）

重新审视“原因”

“解决方案”：配置标志

1. 使用 loop_iter 增加展开边界

在我们的规则中使用 loop_iter 标志

2. 使用 optimistic_loop 跳过边界之外的部分

在我们的规则中使用 optimistic_loop 标志

总结

0 条评论

文章目录

Solidity `string`：隐藏循环的经典案例

1. 使用 `loop_iter` 增加展开边界

在我们的规则中使用 `loop_iter` 标志

2. 使用 `optimistic_loop` 跳过边界之外的部分

在我们的规则中使用 `optimistic_loop` 标志