在规则和不变式中使用 “requireInvariant”

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

本文详细介绍了 Certora 形式化验证工具中 requireInvariant 语句的用法。它通过在规则和不变式中引入已证明的不变式作为假设，避免了在不切实际的合约状态下进行验证，从而提高了验证的效率和准确性。文章以 ERC20 代币的 transfer 函数为例进行了实践演示。

使用 Certora 进行形式化验证

## 在规则和不变量中使用“requireInvariant”

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

最后更新于 2026 年 2 月 13 日

到目前为止，我们已经编写了**规则**来验证特定行为，或者编写了**不变量**来验证在合约整个生命周期中必须始终成立的属性。然而，在验证新属性时，我们通常希望假设我们已经证明的其他属性仍然成立。

例如，在验证代币转账的规则时，我们可能希望假设总供应量仍然等于所有余额的总和——这是一个已经通过单独的不变量证明的属性。使用已证明的不变量作为假设可以防止规则因不切实际的合约状态（违反我们已证明永远不会发生的属性的状态）而失败。

这就是 CVL 的 `requireInvariant` 语句的用武之地。`requireInvariant` 语句允许我们采用一个已证明的不变量，并在验证新规则或不变量时将其用作假设。

在本章中，我们将探讨 `requireInvariant` 是什么、为什么它有用，以及如何在 CVL 中编写规则和不变量时有效应用它。

## 理解 `requireInvariant` 语句

`requireInvariant` 语句是 CVL 的一个构造，允许我们将一个已证明的不变量作为附加条件注入到规则或另一个不变量中。

### `requireInvariant` 如何工作

当 `requireInvariant` 语句包含在规则或另一个不变量中时，Prover 会自动假设所引用的不变量在验证期间已经为真。因此，它只探索满足此条件的合约状态。

### **在** **`requireInvariant`** **规则和不变量中使用**

要在**规则**中使用 `requireInvariant`，只需在规则的开头按名称引用不变量：

```solidity
Copyrule ruleName(env e, ...) {

requireInvariant invariantName();

// rule logic here
}
```

当在**不变量**中（而不是规则中）使用 `requireInvariant` 时，语法是不同的。该语句放置在保留块中，如下所示：

```solidity
Copyinvariant invariantName()
    conditionExpression;

{
    preserved with (env e) {
        requireInvariant otherInvariantName();
    }
}
```

现在我们了解了 `requireInvariant` 语句的目的以及它如何帮助我们重用已证明的不变量，接下来让我们看看它在实践中是如何工作的。

## 回顾 `totalSupplyEqSumOfBalances()` 不变量

在使用 ERC20 代币时，最基本的安全检查之一是确保**所有余额的总和始终等于代币的总供应量**。这个不变量，通常被称为**代币完整性**，保证代币不会被无意中创建或销毁，并且所有个人余额的总和等于总供应量。

在题为《**使用幽灵变量和Hook验证不变量**》的章节中，我们使用以下规范形式化验证了 [Transmission11](https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol) 的 Solmate 库中 ERC20 实现的这一关键安全属性：

```solidity
Copymethods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;
```

让我们看看如何将已证明的 `totalSupplyEqSumOfBalances()` 不变量用作另一个规则或不变量中的假设。

## 在规则中应用 `requireInvariant`

假设我们要定义一个规则 `checkTransferSuccess()` 来验证 ERC20 合约中 `transfer()` 函数的正确性。具体来说，我们希望确保成功的转账正确更新发送方和接收方的余额，同时保持总供应量不变。

为了表达这样一个规则，我们遵循以下步骤：

1.  理解 `transfer()` 函数的预期行为。
2.  编写 CVL 规则来验证此行为。
3.  运行验证并观察结果。

正如我们将看到的，最初的验证会失败——不是因为合约中的 bug，而是因为 Prover 探索了不切实际的状态。这将引导我们引入 `requireInvariant` 作为解决方案。

让我们将这些步骤付诸实践。

### 理解 `transfer()` 函数的期望

为了定义 `transfer()` 成功调用的规范，我们首先检查 Solmate 的 ERC20 合约中该函数的实现：

```solidity
Copyfunction transfer(address to, uint256 amount) public virtual returns (bool) {

balanceOf[msg.sender] -= amount;

unchecked {
        balanceOf[to] += amount;
    }

emit Transfer(msg.sender, to, amount);

return true;
}
```

从上述代码中，我们可以看到 `transfer()` 函数将指定数量的代币（$amount$）从发送方账户转移到接收方账户（$to$）。该函数遵循以下逻辑：

-   **如果发送方有足够的代币：** 发送方的余额减少 $amount$，接收方的余额增加相同数量。
-   **如果发送方没有足够的代币：** 由于算术下溢，操作会自动 revert，并且不会发生状态变化。

### 在 CVL 中表达我们的 `transfer()` 调用期望

现在我们对 `transfer()` 函数的预期行为有了清晰的理解，我们可以通过以下步骤将其转换为 CVL 代码：

1.  **打开规范文件：** 在 Certora 项目目录中，导航到 `specs` 子目录并打开我们为验证 `totalSupplyEqSumOfBalances()` 不变量而创建的 `erc20.spec` 文件。该文件应包含以下规范：

```solidity
Copymethods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;
```

2.  **添加规则：** 通过添加名为 `checkTransferCall()` 的新规则块来扩展 `erc20.spec` 文件。

```solidity
Copyrule checkTransferSuccess() {
    // we’ll fill this step by step
}
```

3.  **包含环境参数：** 由于我们的 `transfer()` 调用需要访问交易环境（如 `msg.sender` 和其他 EVM 上下文变量），我们将其作为 `env e` 类型的参数传递。

```solidity
Copyrule checkTransferSuccess(env e) {
    // we’ll fill this step by step
}
```

4.  **声明输入：** `transfer()` 函数需要两个输入：**一个接收方地址**和一个**代币数量**来转移。我们在规则中将它们声明为局部变量。

```solidity
Copyrule checkTransferSuccess(env e){

// NEWLY ADDED //
    address to;
    uint256 amount;

}
```

5.  **添加对环境的最小约束：** 并非每个输入组合都代表有效的验证场景。例如，我们不希望调用者（`msg.sender`）是合约本身，并且我们不希望允许发送方和接收方是同一账户的转账。我们添加 `require` 语句来排除这些无效场景。

```solidity
Copyrule checkTransferSuccess(env e){

address to;
    uint256 amount;

// NEWLY ADDED //
    require e.msg.sender != currentContract;
    require e.msg.sender != to;
}
```

6.  **捕获调用前状态：** 在进行 `transfer()` 调用之前，我们记录发送方的余额、接收方的余额和总供应量。这些值作为基准，用于验证调用后的更改。

```solidity
Copyrule checkTransferSuccess(env e){

address to;
    uint256 amount;

require e.msg.sender != currentContract;
    require e.msg.sender != to;

// NEWLY ADDED //
    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();
}
```

7.  **调用** `transfer()` **函数：** 我们现在使用环境 $e$ 以及接收方地址 $to$ 和转账金额 $amount$ 来调用 `transfer()` 函数。

```solidity
Copyrule checkTransferSuccess(env e){

address to;
    uint256 amount;

require e.msg.sender != currentContract;
    require e.msg.sender != to;

mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

// NEWLY ADDED //
    transfer(e,to,amount);

}
```

**注意：** 我们调用 `transfer()` 时没有使用 `@withrevert` 修饰符——这意味着规则只验证转账成功的执行。如果转账会 revert（例如，由于余额不足），Prover 只会从验证中排除该路径。

8.  **捕获调用后状态：** 在转账执行后，我们再次捕获发送方的余额、接收方的余额和总供应量，以便我们可以将它们与我们的期望进行比较。

```solidity
Copyrule checkTransferSuccess(env e) {

address to;
    uint256 amount;

require e.msg.sender != currentContract;
    require e.msg.sender != to;

mathint precallSenderBalance = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

transfer@withrevert(e,to,amount);
    bool transferCallStatus = lastReverted;

// NEWLY ADDED //
    mathint postcallSenderBalance = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();

}
```

9.  **断言结果的正确性：** 接下来，我们将期望编码为断言：

-   发送方的余额应正好减少 $amount$。
-   接收方的余额应正好增加 $amount$。
-   总供应量应保持不变（转账只移动代币，不创建或销毁它们）。

```solidity
Copyrule checkTransferSuccess(env e){

address to;
    uint256 amount;

require e.msg.sender != currentContract;
    require e.msg.sender != to;

mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

transfer(e, to, amount);

mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();

// NEWLY ADDED //
    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;
}
```

10. **更新方法块：** 以前，我们的方法块只包含 `totalSupply()` 函数，因为它是在规范中唯一明确调用的函数。现在，我们还需要包含 `balanceOf()` 函数，因为我们的规则引用它来读取账户余额。

```solidity
Copymethods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree; // Add this
}
```

与 `totalSupply()` 类似，`balanceOf()` 函数不依赖于交易环境（例如，它不使用 `msg.sender` 或 `msg.value`）。因此，我们将其声明为 `envfree`。

**注意：** 如果你想知道我们是如何使用 `balanceOf()` 函数的，即使它没有出现在合约源代码中，答案在于 Solidity 处理**公共状态变量**的方式。当你声明一个变量，例如 `mapping(address => uint256) public balanceOf;` 时，编译器会自动生成一个签名如下的 getter 函数：

```solidity
Copyfunction balanceOf(address) external view returns (uint256);
```

即使它没有明确写入源代码中，这个 getter 也是编译后的合约接口的一部分。

可选地，我们还可以将 `transfer()` 函数的签名包含在 `methods` 块中。然而，这样做并不会提高验证性能，因为此函数不是 `envfree`。

```solidity
Copymethods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree;
    function transfer(address,uint256) external returns(bool);
}
```

### 运行初始验证

现在我们的规则 `checkTransferSuccess()` 已经完成，让我们运行 Prover 看看它是否通过验证。

要运行验证，请遵循以下说明：

1.  确保你的 `.conf` 文件与以下配置匹配：

```solidity
Copy{
    "files": [\
        "contracts/ERC20.sol:ERC20"\
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}
```

2.  接下来，在你的终端中执行以下命令：

```solidity
CopycertoraRun confs/erc20.conf
```

这将把你的规范和合约发送给 Certora Prover 进行验证。

3.  一旦 Prover 完成运行（可能需要几分钟），它将在你的终端中输出一个唯一的验证报告链接。在浏览器中打开该链接以查看类似于以下图片的結果：

![图片](https://img.learnblockchain.cn/2026/02/28/ec1cd784bfe5b888-image1.png)

结果显示 `checkTransferSuccess()` **失败**了验证。

### 理解失败原因

要理解规则为何失败，让我们检查调用跟踪。在**存储状态**部分下的**`全局状态 #1`**中，我们可以看到 Prover 选择的初始值：

![图片](https://img.learnblockchain.cn/2026/02/28/945d0c94e0bd2b08-image2.png)

Prover 从具有以下值的状态开始：

**存储状态（ERC20）：**

-   `balanceOf[0x2712]` = `0x7`（$7$ 个代币）
-   `balanceOf[0x25fc]` = $2^{256} - 5$（一个天文数字）
-   `totalSupply` = `0x6`（只有 $5$ 个代币）
-   `sumOfBalances` = $2^{256} + 8$（**幽灵状态**）

请注意每个值右侧的 **`HAVOC`** 标签。这表明这些值是由 Prover 任意选择的。

这种不一致性非常引人注目：一个账户持有 $2^{256} - 5$ 个代币，但总供应量只有 $6$。另一个账户持有 $7$ 个代币——比总供应量还多一个。同时，幽灵变量 `sumOfBalances` 被设置为 $2^{256} + 8$，这与单个余额或总供应量都没有任何关系。

发生这种情况是因为 Prover 在验证新规则时不会自动假定我们之前证明的不变量 `totalSupplyEqSumOfBalances()` 成立。每个规则都从一个新的符号状态开始，其中存储变量和幽灵变量被赋予任意值，除非我们明确约束它们。结果，Prover 探索了在真实的 ERC-20 执行中永远不会发生的状态——即余额、幽灵变量和总供应量之间的会计关系完全被破坏的状态。

当 `transfer()` 在这些不切实际的条件下执行时，我们对余额变化的断言失败了，即使合约逻辑是正确的。

### 使用 `requireInvariant` 修复失败

为了排除这种不一致的状态，我们需要告诉 Prover，`checkTransferCall()` 应该只在 `totalSupplyEqSumOfBalances()` 已经成立的假设下进行检查。

我们通过在规则的**最开始**插入以下行来完成此操作：

```solidity
CopyrequireInvariant totalSupplyEqSumOfBalances();
```

这行代码告诉 Prover 从我们的早期不变量已经为真的状态开始验证。简单来说，Prover 只会在总供应量已经等于所有余额之和的情况下检查该规则。

以下是添加了 `requireInvariant` 的完整规则：

```solidity
Copy// Our Rule
rule checkTransferSuccess(env e){

requireInvariant totalSupplyEqSumOfBalances();

address to;
    uint256 amount;

require e.msg.sender != currentContract;
    require e.msg.sender != to;

mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

transfer(e,to,amount);

mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();

assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;

}
```

### 重新运行验证

现在，让我们再次运行 Prover，并将 `requireInvariant` 语句放在合适的位置：

```solidity
CopycertoraRun confs/erc20.conf
```

打开验证链接以查看结果：

![图片](https://img.learnblockchain.cn/2026/02/28/25073679fd123260-image3.png)

我们的验证结果清楚地表明 Prover 已经验证了该规则。这意味着 `transfer()` 函数正确更新了余额并保持了总供应量不变量。

![图片](https://img.learnblockchain.cn/2026/02/28/c2c46d45f581a4b0-image4.png)

上面讨论的例子清楚地表明，添加 `requireInvariant` 确保 Prover 只考虑符合已证明的全局属性的真实合约状态。在下一节中，我们将看到如何在另一个不变量定义中使用 `requireInvariant`。

## 在不变量中使用 `requireInvariant`

为了理解如何在 CVL 的不变量构造中使用 `requireInvariant`，让我们在 `erc20.spec` 文件中（紧接在 `totalSupplyEqSumOfBalances()` 不变量之下）定义另一个名为 `indBalanceCap()` 的不变量。

```solidity
Copy///..
invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

// Our new Invariant
invariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) <= to_mathint(totalSupply());
//.....
```

这个新不变量编码了一个基本的 ERC-20 安全属性：**任何账户的余额都不应超过总供应量**。

### 验证我们的新不变量

现在让我们运行 Prover，然后打开 Prover 提供的验证链接以查看类似于以下图片的結果：

![图片](https://img.learnblockchain.cn/2026/02/28/38d24303937c8ad9-image5.png)

上图结果显示我们的不变量 `indBalanceCap()` 未通过验证过程。

对 Prover 报告的进一步分析表明，该不变量未能通过归纳检查。具体来说，Prover 通过 `transfer()` 和 `transferFrom()` 函数调用发现了不变量的违规行为，如下图所示：

![图片](https://img.learnblockchain.cn/2026/02/28/863674fbc9fdc8b0-image6.png)

为了理解违规的原因，让我们分析 `transfer()` 的调用跟踪。（**注意：**`transferFrom()` 因同样的原因失败，因此分析 `transfer()` 涵盖了两种情况）

### 理解违规原因

让我们从 Prover 报告的**存储状态**部分开始分析。此部分显示了合约存储变量在验证初始点的实际值。

![图片](https://img.learnblockchain.cn/2026/02/28/01906a718311f34a-image7.png)

在存储状态中，我们可以看到单个账户余额如下：

-   $balanceOf[0x2711] = 0x5$（账户 `0x2711` 持有 5 个代币）
-   $balanceOf[0x2713] = 0x4$（账户 `0x2713` 持有 4 个代币）

而代币的 `totalSupply` 仅记录为 $0x4$（即 4 个代币）。

由于我们已经证明了 `totalSupplyEqSumOfBalances()` 不变量，像这样的状态在合约的实际执行中永远不应该出现。该不变量表示在每个有效状态下，总供应量必须始终等于所有余额的总和。但在上面的跟踪中，余额总和为 $9$，而总供应量仅为 $4$。这种不匹配表明 Prover 从一个在我们的 ERC-20 实现中实际无法到达的状态开始。

发生这种情况是因为 Prover 在开始验证新属性时，不会自动假定之前证明的不变量应该成立。每个新规则或不变量都从一个全新的符号状态开始，除非我们明确将其与早期结果连接起来。因此，Prover 可能会选择一个违反我们之前证明的不变量的初始配置，即使这种配置在实际合约执行期间是不可能的。

### 使用 `requireInvariant` 语句修复失败

为了排除这种不一致的状态，我们需要告诉 Prover，`indBalanceCap()` 应该只在 `totalSupplyEqSumOfBalances()` 已经成立的假设下进行检查。

为了强制执行此操作，我们使用 `requireInvariant` 明确导入该不变量，如下所示：

```solidity
Copyinvariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) <= to_mathint(totalSupply())
{
    preserved with (env e) {
        // Require that our earlier invariant holds
        requireInvariant totalSupplyEqSumOfBalances();
    }
}
```

通过这种方式，Prover 从一个已经满足我们之前证明的代币守恒规则的世界开始，并防止搜索空间漂移到不可能的 ERC-20 状态。

### 验证加强后的不变量

现在，如果我们使用以下命令重新运行 Prover：

```solidity
CopycertoraRun confs/erc20.conf
```

并打开验证链接，我们将看到类似于以下图片的結果：

![图片](https://img.learnblockchain.cn/2026/02/28/3f7b7ad0589f7335-image8.png)

我们可以看到，正如预期的那样，`indBalanceCap()` 现在已成功验证。由于 Prover 被限制在已经满足 `totalSupplyEqSumOfBalances()` 的状态，它不再遇到导致早期失败的不可能配置。

## **`require`** **与** **`requireInvariant`：相同的过滤器，不同的保证**

有趣的是，如果使用常规的 `require` 语句而不是 `requireInvariant`，`indBalanceCap()` 不变量也会通过验证，如下图所示：

![图片](https://img.learnblockchain.cn/2026/02/28/f819d7a48232d181-image9.png)

发生这种情况是因为，在保留块内部，`require` 和 `requireInvariant` 都服务于相同的操作目的：它们**过滤归纳步骤的 pre-state**。实际上，这两个语句都指示 Prover：

_**“只探索从满足此条件的状态开始的转换。”**_

因此，以下两行对搜索空间施加了**相同的功能限制**：

```solidity
CopyrequireInvariant totalSupplyEqSumOfBalances();
```

和

```solidity
Copyrequire to_mathint(totalSupply()) == sumOfBalances;
```

两者都阻止 Prover 考虑我们之前观察到的不一致的初始状态，从而使 `indBalanceCap()` 不变量得以通过。

### 为什么 `requireInvariant` 仍然更可取

尽管两种形式都以相似的方式限制了搜索空间，但它们在结果规范的**可靠性和原则性**方面有所不同。

`requireInvariant` 更安全，因为它导入了一个 Prover 已经确定在所有可达状态中都为真的属性。而普通的 `require` 完全依赖于规范编写者来陈述一个正确的条件。例如：

```solidity
Copyrequire to_mathint(totalSupply()) == sumOfBalances;
```

强制 Prover 接受这个相等性，而不检查它是否实际为真。如果条件哪怕是稍微不正确或不完整，Prover 可能会悄悄地忽略真实的**反例**，从而给出具有误导性的成功验证。

因此，关键的区别很简单：

-   `require` 强制执行我们编写的条件。
-   `requireInvariant` 强制执行一个已被证明普遍为真的条件。

因此，`requireInvariant` 提供了一种更安全、更具原则性的方式来重用假设，而普通的 `require` 如果条件不正确或不完整，可能会无意中隐藏真正的违规行为。

## 结论

这就是我们如何使用 `requireInvariant` 使我们的规范更强大、更模块化、更高效。

-   在**规则**中，它允许我们将已证明的不变量作为先决条件重复使用，确保在真实条件下检查每个执行路径。
-   在**不变量**中，它允许我们通过假设早期不变量来证明新属性，避免来自不一致状态的无意义**反例**。

关键原则简单而强大：**首先证明全局不变量，然后在验证特定行为或附加不变量时将它们作为构建块重复使用**。

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

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

使用 Certora 进行形式化验证

在规则和不变量中使用“requireInvariant”

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

最后更新于 2026 年 2 月 13 日

到目前为止，我们已经编写了规则来验证特定行为，或者编写了不变量来验证在合约整个生命周期中必须始终成立的属性。然而，在验证新属性时，我们通常希望假设我们已经证明的其他属性仍然成立。

这就是 CVL 的 requireInvariant 语句的用武之地。requireInvariant 语句允许我们采用一个已证明的不变量，并在验证新规则或不变量时将其用作假设。

在本章中，我们将探讨 requireInvariant 是什么、为什么它有用，以及如何在 CVL 中编写规则和不变量时有效应用它。

理解 `requireInvariant` 语句

requireInvariant 语句是 CVL 的一个构造，允许我们将一个已证明的不变量作为附加条件注入到规则或另一个不变量中。

`requireInvariant` 如何工作

当 requireInvariant 语句包含在规则或另一个不变量中时，Prover 会自动假设所引用的不变量在验证期间已经为真。因此，它只探索满足此条件的合约状态。

在 `requireInvariant` 规则和不变量中使用

要在规则中使用 requireInvariant，只需在规则的开头按名称引用不变量：

Copyrule ruleName(env e, ...) {

    requireInvariant invariantName();

    // rule logic here
}

当在不变量中（而不是规则中）使用 requireInvariant 时，语法是不同的。该语句放置在保留块中，如下所示：

Copyinvariant invariantName()
    conditionExpression;

{
    preserved with (env e) {
        requireInvariant otherInvariantName();
    }
}

现在我们了解了 requireInvariant 语句的目的以及它如何帮助我们重用已证明的不变量，接下来让我们看看它在实践中是如何工作的。

回顾 `totalSupplyEqSumOfBalances()` 不变量

在使用 ERC20 代币时，最基本的安全检查之一是确保所有余额的总和始终等于代币的总供应量。这个不变量，通常被称为代币完整性，保证代币不会被无意中创建或销毁，并且所有个人余额的总和等于总供应量。

在题为《使用幽灵变量和Hook验证不变量》的章节中，我们使用以下规范形式化验证了 Transmission11 的 Solmate 库中 ERC20 实现的这一关键安全属性：

Copymethods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

让我们看看如何将已证明的 totalSupplyEqSumOfBalances() 不变量用作另一个规则或不变量中的假设。

在规则中应用 `requireInvariant`

假设我们要定义一个规则 checkTransferSuccess() 来验证 ERC20 合约中 transfer() 函数的正确性。具体来说，我们希望确保成功的转账正确更新发送方和接收方的余额，同时保持总供应量不变。

为了表达这样一个规则，我们遵循以下步骤：

理解 transfer() 函数的预期行为。
编写 CVL 规则来验证此行为。
运行验证并观察结果。

正如我们将看到的，最初的验证会失败——不是因为合约中的 bug，而是因为 Prover 探索了不切实际的状态。这将引导我们引入 requireInvariant 作为解决方案。

让我们将这些步骤付诸实践。

理解 `transfer()` 函数的期望

为了定义 transfer() 成功调用的规范，我们首先检查 Solmate 的 ERC20 合约中该函数的实现：

Copyfunction transfer(address to, uint256 amount) public virtual returns (bool) {

    balanceOf[msg.sender] -= amount;

    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

从上述代码中，我们可以看到 transfer() 函数将指定数量的代币（$amount$）从发送方账户转移到接收方账户（$to$）。该函数遵循以下逻辑：

如果发送方有足够的代币： 发送方的余额减少 $amount$，接收方的余额增加相同数量。
如果发送方没有足够的代币： 由于算术下溢，操作会自动 revert，并且不会发生状态变化。

在 CVL 中表达我们的 `transfer()` 调用期望

现在我们对 transfer() 函数的预期行为有了清晰的理解，我们可以通过以下步骤将其转换为 CVL 代码：

打开规范文件： 在 Certora 项目目录中，导航到 specs 子目录并打开我们为验证 totalSupplyEqSumOfBalances() 不变量而创建的 erc20.spec 文件。该文件应包含以下规范：

Copymethods {
    function totalSupply() external returns(uint256) envfree;
}

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

添加规则： 通过添加名为 checkTransferCall() 的新规则块来扩展 erc20.spec 文件。

Copyrule checkTransferSuccess() {
    // we’ll fill this step by step
}

包含环境参数： 由于我们的 transfer() 调用需要访问交易环境（如 msg.sender 和其他 EVM 上下文变量），我们将其作为 env e 类型的参数传递。

Copyrule checkTransferSuccess(env e) {
    // we’ll fill this step by step
}

声明输入： transfer() 函数需要两个输入：一个接收方地址和一个代币数量来转移。我们在规则中将它们声明为局部变量。

Copyrule checkTransferSuccess(env e){

    // NEWLY ADDED //
    address to;
    uint256 amount;

}

添加对环境的最小约束： 并非每个输入组合都代表有效的验证场景。例如，我们不希望调用者（msg.sender）是合约本身，并且我们不希望允许发送方和接收方是同一账户的转账。我们添加 require 语句来排除这些无效场景。

Copyrule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    // NEWLY ADDED //
    require e.msg.sender != currentContract;
    require e.msg.sender != to;
}

捕获调用前状态： 在进行 transfer() 调用之前，我们记录发送方的余额、接收方的余额和总供应量。这些值作为基准，用于验证调用后的更改。

Copyrule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    // NEWLY ADDED //
    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();
}

调用 transfer() 函数： 我们现在使用环境 $e$ 以及接收方地址 $to$ 和转账金额 $amount$ 来调用 transfer() 函数。

Copyrule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    // NEWLY ADDED //
    transfer(e,to,amount);

}

注意： 我们调用 transfer() 时没有使用 @withrevert 修饰符——这意味着规则只验证转账成功的执行。如果转账会 revert（例如，由于余额不足），Prover 只会从验证中排除该路径。

捕获调用后状态： 在转账执行后，我们再次捕获发送方的余额、接收方的余额和总供应量，以便我们可以将它们与我们的期望进行比较。

Copyrule checkTransferSuccess(env e) {

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer@withrevert(e,to,amount);
    bool transferCallStatus = lastReverted;

    // NEWLY ADDED //
    mathint postcallSenderBalance = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();

}

断言结果的正确性： 接下来，我们将期望编码为断言：

发送方的余额应正好减少 $amount$。
接收方的余额应正好增加 $amount$。
总供应量应保持不变（转账只移动代币，不创建或销毁它们）。

Copyrule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer(e, to, amount);

    mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();

    // NEWLY ADDED //
    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;
}

更新方法块： 以前，我们的方法块只包含 totalSupply() 函数，因为它是在规范中唯一明确调用的函数。现在，我们还需要包含 balanceOf() 函数，因为我们的规则引用它来读取账户余额。

Copymethods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree; // Add this
}

与 totalSupply() 类似，balanceOf() 函数不依赖于交易环境（例如，它不使用 msg.sender 或 msg.value）。因此，我们将其声明为 envfree。

注意： 如果你想知道我们是如何使用 balanceOf() 函数的，即使它没有出现在合约源代码中，答案在于 Solidity 处理公共状态变量的方式。当你声明一个变量，例如 mapping(address => uint256) public balanceOf; 时，编译器会自动生成一个签名如下的 getter 函数：

Copyfunction balanceOf(address) external view returns (uint256);

即使它没有明确写入源代码中，这个 getter 也是编译后的合约接口的一部分。

可选地，我们还可以将 transfer() 函数的签名包含在 methods 块中。然而，这样做并不会提高验证性能，因为此函数不是 envfree。

Copymethods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree;
    function transfer(address,uint256) external returns(bool);
}

运行初始验证

现在我们的规则 checkTransferSuccess() 已经完成，让我们运行 Prover 看看它是否通过验证。

要运行验证，请遵循以下说明：

确保你的 .conf 文件与以下配置匹配：

Copy{
    "files": [\
        "contracts/ERC20.sol:ERC20"\
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}

接下来，在你的终端中执行以下命令：

CopycertoraRun confs/erc20.conf

这将把你的规范和合约发送给 Certora Prover 进行验证。

一旦 Prover 完成运行（可能需要几分钟），它将在你的终端中输出一个唯一的验证报告链接。在浏览器中打开该链接以查看类似于以下图片的結果：

结果显示 checkTransferSuccess() 失败了验证。

理解失败原因

要理解规则为何失败，让我们检查调用跟踪。在存储状态部分下的全局状态 #1中，我们可以看到 Prover 选择的初始值：

Prover 从具有以下值的状态开始：

存储状态（ERC20）：

balanceOf[0x2712] = 0x7（$7$ 个代币）
balanceOf[0x25fc] = $2^{256} - 5$（一个天文数字）
totalSupply = 0x6（只有 $5$ 个代币）
sumOfBalances = $2^{256} + 8$（幽灵状态）

请注意每个值右侧的 HAVOC 标签。这表明这些值是由 Prover 任意选择的。

这种不一致性非常引人注目：一个账户持有 $2^{256} - 5$ 个代币，但总供应量只有 $6$。另一个账户持有 $7$ 个代币——比总供应量还多一个。同时，幽灵变量 sumOfBalances 被设置为 $2^{256} + 8$，这与单个余额或总供应量都没有任何关系。

发生这种情况是因为 Prover 在验证新规则时不会自动假定我们之前证明的不变量 totalSupplyEqSumOfBalances() 成立。每个规则都从一个新的符号状态开始，其中存储变量和幽灵变量被赋予任意值，除非我们明确约束它们。结果，Prover 探索了在真实的 ERC-20 执行中永远不会发生的状态——即余额、幽灵变量和总供应量之间的会计关系完全被破坏的状态。

当 transfer() 在这些不切实际的条件下执行时，我们对余额变化的断言失败了，即使合约逻辑是正确的。

使用 `requireInvariant` 修复失败

为了排除这种不一致的状态，我们需要告诉 Prover，checkTransferCall() 应该只在 totalSupplyEqSumOfBalances() 已经成立的假设下进行检查。

我们通过在规则的最开始插入以下行来完成此操作：

CopyrequireInvariant totalSupplyEqSumOfBalances();

这行代码告诉 Prover 从我们的早期不变量已经为真的状态开始验证。简单来说，Prover 只会在总供应量已经等于所有余额之和的情况下检查该规则。

以下是添加了 requireInvariant 的完整规则：

Copy// Our Rule
rule checkTransferSuccess(env e){

   requireInvariant totalSupplyEqSumOfBalances();

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer(e,to,amount);

    mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();

    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;

}

重新运行验证

现在，让我们再次运行 Prover，并将 requireInvariant 语句放在合适的位置：

CopycertoraRun confs/erc20.conf

打开验证链接以查看结果：

我们的验证结果清楚地表明 Prover 已经验证了该规则。这意味着 transfer() 函数正确更新了余额并保持了总供应量不变量。

上面讨论的例子清楚地表明，添加 requireInvariant 确保 Prover 只考虑符合已证明的全局属性的真实合约状态。在下一节中，我们将看到如何在另一个不变量定义中使用 requireInvariant。

在不变量中使用 `requireInvariant`

为了理解如何在 CVL 的不变量构造中使用 requireInvariant，让我们在 erc20.spec 文件中（紧接在 totalSupplyEqSumOfBalances() 不变量之下）定义另一个名为 indBalanceCap() 的不变量。

Copy///..
invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

// Our new Invariant
invariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) &lt;= to_mathint(totalSupply());
//.....

这个新不变量编码了一个基本的 ERC-20 安全属性：任何账户的余额都不应超过总供应量。

验证我们的新不变量

现在让我们运行 Prover，然后打开 Prover 提供的验证链接以查看类似于以下图片的結果：

上图结果显示我们的不变量 indBalanceCap() 未通过验证过程。

对 Prover 报告的进一步分析表明，该不变量未能通过归纳检查。具体来说，Prover 通过 transfer() 和 transferFrom() 函数调用发现了不变量的违规行为，如下图所示：

为了理解违规的原因，让我们分析 transfer() 的调用跟踪。（注意：transferFrom() 因同样的原因失败，因此分析 transfer() 涵盖了两种情况）

理解违规原因

让我们从 Prover 报告的存储状态部分开始分析。此部分显示了合约存储变量在验证初始点的实际值。

在存储状态中，我们可以看到单个账户余额如下：

$balanceOf[0x2711] = 0x5$（账户 0x2711 持有 5 个代币）
$balanceOf[0x2713] = 0x4$（账户 0x2713 持有 4 个代币）

而代币的 totalSupply 仅记录为 $0x4$（即 4 个代币）。

由于我们已经证明了 totalSupplyEqSumOfBalances() 不变量，像这样的状态在合约的实际执行中永远不应该出现。该不变量表示在每个有效状态下，总供应量必须始终等于所有余额的总和。但在上面的跟踪中，余额总和为 $9$，而总供应量仅为 $4$。这种不匹配表明 Prover 从一个在我们的 ERC-20 实现中实际无法到达的状态开始。

使用 `requireInvariant` 语句修复失败

为了排除这种不一致的状态，我们需要告诉 Prover，indBalanceCap() 应该只在 totalSupplyEqSumOfBalances() 已经成立的假设下进行检查。

为了强制执行此操作，我们使用 requireInvariant 明确导入该不变量，如下所示：

Copyinvariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) &lt;= to_mathint(totalSupply())
{
    preserved with (env e) {
        // Require that our earlier invariant holds
        requireInvariant totalSupplyEqSumOfBalances();
    }
}

通过这种方式，Prover 从一个已经满足我们之前证明的代币守恒规则的世界开始，并防止搜索空间漂移到不可能的 ERC-20 状态。

验证加强后的不变量

现在，如果我们使用以下命令重新运行 Prover：

CopycertoraRun confs/erc20.conf

并打开验证链接，我们将看到类似于以下图片的結果：

我们可以看到，正如预期的那样，indBalanceCap() 现在已成功验证。由于 Prover 被限制在已经满足 totalSupplyEqSumOfBalances() 的状态，它不再遇到导致早期失败的不可能配置。

`require` 与 `requireInvariant`：相同的过滤器，不同的保证

有趣的是，如果使用常规的 require 语句而不是 requireInvariant，indBalanceCap() 不变量也会通过验证，如下图所示：

发生这种情况是因为，在保留块内部，require 和 requireInvariant 都服务于相同的操作目的：它们过滤归纳步骤的 pre-state。实际上，这两个语句都指示 Prover：

“只探索从满足此条件的状态开始的转换。”

因此，以下两行对搜索空间施加了相同的功能限制：

CopyrequireInvariant totalSupplyEqSumOfBalances();

和

Copyrequire to_mathint(totalSupply()) == sumOfBalances;

两者都阻止 Prover 考虑我们之前观察到的不一致的初始状态，从而使 indBalanceCap() 不变量得以通过。

为什么 `requireInvariant` 仍然更可取

尽管两种形式都以相似的方式限制了搜索空间，但它们在结果规范的可靠性和原则性方面有所不同。

requireInvariant 更安全，因为它导入了一个 Prover 已经确定在所有可达状态中都为真的属性。而普通的 require 完全依赖于规范编写者来陈述一个正确的条件。例如：

Copyrequire to_mathint(totalSupply()) == sumOfBalances;

强制 Prover 接受这个相等性，而不检查它是否实际为真。如果条件哪怕是稍微不正确或不完整，Prover 可能会悄悄地忽略真实的反例，从而给出具有误导性的成功验证。

因此，关键的区别很简单：

require 强制执行我们编写的条件。
requireInvariant 强制执行一个已被证明普遍为真的条件。

因此，requireInvariant 提供了一种更安全、更具原则性的方式来重用假设，而普通的 require 如果条件不正确或不完整，可能会无意中隐藏真正的违规行为。

结论

这就是我们如何使用 requireInvariant 使我们的规范更强大、更模块化、更高效。

在规则中，它允许我们将已证明的不变量作为先决条件重复使用，确保在真实条件下检查每个执行路径。
在不变量中，它允许我们通过假设早期不变量来证明新属性，避免来自不一致状态的无意义反例。

关键原则简单而强大：首先证明全局不变量，然后在验证特定行为或附加不变量时将它们作为构建块重复使用。

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

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

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

翻译
学分: 0
分类: 安全
标签: 形式化验证 Certora requireInvariant 不变式智能合约 ERC20

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

在规则和不变式中使用 “requireInvariant”

在规则和不变量中使用“requireInvariant”

理解 `requireInvariant` 语句

`requireInvariant` 如何工作

在 `requireInvariant` 规则和不变量中使用

回顾 `totalSupplyEqSumOfBalances()` 不变量

在规则中应用 `requireInvariant`

理解 `transfer()` 函数的期望

在 CVL 中表达我们的 `transfer()` 调用期望

运行初始验证

理解失败原因

使用 `requireInvariant` 修复失败

重新运行验证

在不变量中使用 `requireInvariant`

验证我们的新不变量

理解违规原因

使用 `requireInvariant` 语句修复失败

验证加强后的不变量

`require` 与 `requireInvariant`：相同的过滤器，不同的保证

为什么 `requireInvariant` 仍然更可取

结论

0 条评论

文章目录

在规则和不变式中使用 “requireInvariant”

在规则和不变量中使用“requireInvariant”

理解 requireInvariant 语句

requireInvariant 如何工作

在 requireInvariant 规则和不变量中使用

回顾 totalSupplyEqSumOfBalances() 不变量

在规则中应用 requireInvariant

理解 transfer() 函数的期望

在 CVL 中表达我们的 transfer() 调用期望

运行初始验证

理解失败原因

使用 requireInvariant 修复失败

重新运行验证

在不变量中使用 requireInvariant

验证我们的新不变量

理解违规原因

使用 requireInvariant 语句修复失败

验证加强后的不变量

require 与 requireInvariant：相同的过滤器，不同的保证

为什么 requireInvariant 仍然更可取

结论

0 条评论

文章目录

理解 `requireInvariant` 语句

`requireInvariant` 如何工作

在 `requireInvariant` 规则和不变量中使用

回顾 `totalSupplyEqSumOfBalances()` 不变量

在规则中应用 `requireInvariant`

理解 `transfer()` 函数的期望

在 CVL 中表达我们的 `transfer()` 调用期望

使用 `requireInvariant` 修复失败

在不变量中使用 `requireInvariant`

使用 `requireInvariant` 语句修复失败

`require` 与 `requireInvariant`：相同的过滤器，不同的保证

为什么 `requireInvariant` 仍然更可取