不变量 (invariant) 是智能合约部署后及其整个执行过程中必须始终保持为真的属性。乍看之下，验证不变量似乎很简单：假设在函数调用之前不变量成立，运行该函数，并确认它在之后仍然成立。

在实践中，这个过程很少如此简单。Certora Prover 运行在一个符号化的世界中，它会探索合约的所有可能状态，而不仅仅是那些在已部署系统中实际发生的状态。这种详尽的符号化探索是其设计的基础；这正是 Prover 能够发现开发者可能从未考虑过的场景中的漏洞的原因。

然而，在合约业务逻辑的上下文中，并非 Prover 探索的每一个符号状态都是有效或可达的状态。如果没有额外的指导，Prover 可能会从真实的区块链执行中永远不会出现的“不可能”状态或条件开始，或者对其进行推理。当这种情况发生时，即使合约本身是正确的，Prover 也可能会标记出违例 (violation)，仅仅是因为分析始于一个无效的假设。

为了防止这种误报的违例，CVL 提供了 preserved block，这是一种允许我们为实际的合约行为指定额外假设的机制。这些假设有助于 Prover 专注于有效且相关的执行路径，排除在逻辑上或上下文中不可能出现的状态。

在本章中，我们将探讨 preserved blocks 在形式化验证中的作用。我们将讨论为什么它们是必要的，如何在 CVL 中编写它们，以及它们如何帮助确保仅在现实条件下检查不变量。我们还将把这个概念应用到一个实际例子中，通过验证在 WETH 合约中，合约的 ETH 余额始终等于或大于其代币总供应量。

为了更清楚地理解它们的作用，让我们首先回顾一下 Prover 是如何检查一个函数是否保持不变量的，以及为什么这个过程有时会失败。

为什么不变量需要额外的假设

众所周知，在验证不变量时，Prover 遵循类似于数学归纳法的结构化推理过程：

1. 初始状态检查（基础情况）： Prover 首先验证在合约的构造函数执行完毕后，不变量是否立即成立。这将不变量在起点的状态确立为真。
2. 假设（前置状态）： 对于每个 public 和 external 函数，Prover 假设在函数执行前不变量成立。
3. 符号执行和后置状态检查： 然后，它在所有可能的输入和控制流路径上对函数进行符号执行，并验证不变量在执行后是否仍然成立。

如果不变量满足所有这些检查，它就被认为在所有合约执行中都能得以保持。但困难在于：Prover 并不局限于真实的执行路径。它还会探索极不可能甚至不可能的状态。

例如，在验证 ERC-20 不变量 “所有账户余额的总和必须始终等于代币总供应量” 时，Prover 可能会探索一条执行路径，在该路径中，合约最终调用了自身的函数。在实践中，这种情况永远不会发生，因为像 transfer 这样的 ERC-20 函数原本就是只由外部用户或其他合约来调用的。然而，由于 Prover 会系统地探索所有可能的调用者，它也会考虑合约调用自身函数的执行轨迹。

这种自调用可能会产生荒谬的场景，即余额和代币总供应量看起来不一致，导致 Prover 报告违例，即使没有任何真实的执行可以触发它。这些都是典型的误报违例 (false violations) 示例：不变量看起来被破坏了，仅仅是因为 Prover 对现实中不可能发生的状态进行了推理。

这就是 preserved blocks 发挥作用的地方。Preserved blocks 允许我们在不变量验证期间引入额外的假设，引导 Prover 忽略不可能或不相关的状态，而只专注于真实的状态。

既然我们理解了为什么需要 preserved blocks，接下来让我们看看在 CVL 中如何编写它们。

如何定义一个 Preserved Block？

Preserved block 是 CVL 中的一种特殊结构，它让我们在证明不变量时添加额外假设。可以把它想象成给 Prover 一个关于系统实际行为的小“提示”，这样它就不会把时间浪费在探索不可能的场景上。

我们在不变量表达式之后立即使用 preserved 关键字来定义 preserved block。最简单的形式如下：

Copy
invariant invariant_name()
    invariant_expression
{
    preserved {
        // assumptions about the invariant
    }

}

有时，我们不希望 preserved block 应用于所有地方——只应用于特定函数，或者仅在具有某些环境细节（如 msg.sender 或 msg.value）时应用。在这种情况下，我们可以通过可选的函数签名和可选的 with 子句（以访问交易环境）来扩展语法：

Copy
invariant invariant_name(param_1, param_2,...)
    invariant_expression;
{
    preserved functionName(type arg, ...) with (env e) {
        // additional assumptions applicable only for this particular function
    }

}

通用的 preserved blocks 和特定于函数的 preserved blocks 都在不变量检查的归纳步骤期间应用。它们在假设不变量在预状态下成立之后，但在对应的验证方法被符号执行之前执行，确保 Prover 从一个在数学上有效且在上下文中真实的状态开始每个归纳步骤。

到目前为止，preserved blocks 决定了在分析每个相关函数时的假设条件。然而，在某些情况下，我们可能还想首先限制不变量针对哪些函数进行检查。为此，CVL 提供了一个 filter block，写作 filtered { … }。（您可以在此处阅读有关 filter block 的更多信息）

Copy
invariant invariant_name()
    invariant_expression;
    filtered {
        // restrict which functions are checked
    }
{
    preserved functionName(type arg, ...) with (env e) {
        // assumptions or requireInvariant statements
    }

}

当存在 filter block 时，不变量仅针对过滤器中包含的函数进行检查，且任何 preserved blocks 都在该受限集合内应用。因此，preserved block 写在 filter block 之后。

filter block 限制了不变量针对哪些函数进行检查。然后，一个通用的 preserved block (preserved with (env e) { ... }) 应用于该过滤集合中的每个函数。一个特定于函数的 preserved block (preserved functionName(…) with (env e) { ... }) 仅当 Prover 正在检查该指定函数时适用。如果指定函数未被过滤器包含，则该 preserved block 将不起作用。

简而言之，过滤器缩小了不变量应用的范围，而 preserved blocks 则描述了在执行这些函数时什么条件必须仍然成立。它们一起使用，为 Prover 提供了一条清晰的路径来检查不变量，而不会被不相关或不可能的状态所干扰。

然而，在实践中，当不变量由于不现实的符号执行而失败时，通常优先使用 preserved blocks 而不是 filter blocks。这两种机制都限制了 Prover 的搜索空间，且必须谨慎使用以避免削弱证明，但过滤器风险更高，因为它们会从不变量检查中移除整个函数。

Preserved blocks 通常更安全，因为它们约束的是关于状态或执行环境的假设，而不是完全排除某些行为。因此，它们更适合排除不可能的状态，同时仍确保不变量能够针对所有相关的合约功能进行检查。

既然我们已经介绍了理论和语法，接下来让我们看看 preserved blocks 在实践中是如何工作的，将其应用到一个真实的合约中：Solady’s WETH。

融会贯通：验证 WETH 不变量

为了将所有内容联系起来，让我们验证 Solady WETH 合约的一个不变量——这是一种 ERC-20 实现，它以 1:1 的比例将 Ether (ETH) 表示为 WETH 代币。该合约的一个关键属性是，其 ETH 余额必须始终大于或等于流通中的 WETH 代币总数。

定义我们的 WETH 不变量

要验证此不变量，请按照以下步骤操作：

1. 在你的 Certora 项目目录中，在 contracts 子目录下创建一个名为 ERC20.sol 的新文件，并从 Solady 中复制此代码到该文件中。
2. 在同一个 contracts 子目录中创建另一个名为 WETH.sol 的文件，并将此代码复制进去。
3. 在 specs 子目录中，创建一个名为 weth.spec 的新文件。
4. 在 weth.spec 中，如下定义不变量 tokenIntegrity()：

Copy
invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply();

注意： 在 CVL 中，nativeBalances 是原生代币余额的映射——例如，以太坊上的 ETH。地址 a 的余额可以使用 nativeBalances[a] 来表示。标识符 currentContract 指的是正在验证的主合约。因此，nativeBalances[currentContract] 代表正在被验证的合约的原生代币余额。

5. 添加一个包含 totalSupply() 函数签名的 methods block：

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply();

6. 在 confs 子目录中，创建一个名为 weth.conf 的配置文件：

Copy
{
    "files": [
        "contracts/WETH.sol:WETH"
    ],
    "verify": "WETH:specs/weth.spec",
    "optimistic_loop" : true,
    "msg": "Check WETH contract integrity"
}

运行验证

完成上述所有步骤后，运行 certoraRun confs/weth.conf 命令来验证我们的规范，并查看类似于下图的结果：

上述验证运行的结果表明，tokenIntegrity 不变量失败了，因为 Prover 发现了一种合约的 ETH 余额可能小于其报告的总供应量的场景。

理解违例 (Violation)

我们的详细分析报告发现，我们的不变量 tokenIntegrity 已经通过了 “归纳基础 (Induction base)：构造函数之后” ✅，这意味着该属性在部署后立即成立。然而，它在 “归纳步骤 (Induction step)：执行 external (非 view/pure) 方法之后” ❌ 时失败了，这表明虽然不变量在开始时是有效的，但在某些改变状态的函数调用之后，它不能始终保持成立。

为了理解违例的原因，我们需要分析失败函数的调用追踪 (call traces)。

让我们从 deposit() 函数开始。

理解 deposit() 调用的违例

我们对 deposit() 函数调用追踪的分析揭示了一些不寻常的情况：发送者 (sender) 和接收者 (receiver) 都是合约本身 (WETH)。

这种情况——合约调用其自身的 deposit()——从实际角度来看是一个荒谬的案例，因为 WETH 合约不包含任何可以直接或间接调用 deposit() 的代码路径。尽管 Prover 准确地将此识别为理论上可能的交互，但我们可以通过 preserved block 显式地告诉它忽略这类情况。

理解 receive() 调用的违例

Solidity 合约中的 receive() 函数是一个特殊的函数，当合约接收到带有空 calldata 的 Ether 时会自动执行。一个合约只能定义一个这样的函数，并且它必须具有以下形式：

Copy
receive() external payable { ... }

receive() 函数不能接受参数，不能返回值，并且会在普通的 ETH 转账（例如通过 .send、.transfer 或原始 ETH 转账）时触发。

在 WETH 的实现中，receive() 函数只是简单地将调用转发给 deposit() 函数：

Copy
// @dev Equivalent to `deposit()`.
receive() external payable virtual {
    deposit();
}

正因为如此，任何破坏 deposit() 的不真实执行路径也同样会破坏 receive()。Prover 将 receive() 视为又一个外部入口点，所以它可能会在符号执行时假设合约调用了自身的 receive() 函数。

这正是在失败的追踪中发生的情况：就像在 deposit() 中一样，Prover 挑选了一条发送者和接收者都是合约本身 (WETH) 的路径，导致了一个不可能的自调用场景，这在真实的执行中并不会发生，但在符号执行上却导致了不变量的失败。

理解 withdraw() 调用的违例

withdraw() 的调用追踪揭示了一个由 Prover 测试极其不真实的场景所引发的问题。为了理解它为什么失败，让我们使用 Prover 所用的确切值，逐步分析调用追踪。

前置状态检查（Global State #1）

在前置状态检查期间，Prover 假设在函数运行之前不变量成立。此时——被捕获为 Global State #1——它建立了一个符号环境，以表示 withdraw() 函数被符号执行之前的可能初始条件。

在此状态下，合约的 ETH 余额被设置为 2^256 − 3，而代币总供应量仅为 2。

这意味着合约在一个不可能的状态下开始——它持有巨额的 ETH，但代币总供应量只有 2。现实世界中的任何部署都无法达到这样的条件，但由于我们没有约束初始状态，Prover 就可以自由选择任意的值。

在此时，我们的不变量成立，因为：

Copy
2^256 − 3 ≥ 2  ✅

withdraw() 的符号执行（Global State #2）

接下来，Prover 对 withdraw() 函数进行符号执行：

在这里，调用者 (0x8200) 尝试提取 2^256 − 6。withdraw() 函数调用了内部函数 _burn(from, amount)。在实际执行中，如果 amount > balanceOf(from)，_burn() 会立即回退 (revert)。

然而，Prover 的推理是符号化的。当它运行到 if (amount > balanceOf(from)) 这个检查时，它将 balanceOf(0x8200) 视为一个无界的符号变量。为了探索一条不回退的路径，它必须为这个余额假设一个足够大的值，以便通过检查。

我们可以通过查看 Global State #3 下方的 _burn 操作来找到这个假设值。追踪显示了在单个存储槽（调用者的余额）上经典的“读取-修改-写入 (read-modify-write)”模式：

这告诉了我们以下内容：

• Prover 加载 (loads) 调用者的余额。为了继续执行，它假设该余额为 2^256 - 2。
• 然后它在减法操作之后存储 (stores) 新的余额 (0x4)。

我们可以用简单的数学计算来证实这一点：

Copy
Precall Balance of 0x8200 =  2^256
Withdrawal Amount = 2^256 - 6
Postcall Balance of 0x8200 should be = (2^256 - 2) - (2^256 - 6) = 4

计算结果 4 与 Store 里的值 0x4 完美匹配。

算术下溢 (Arithmetic Underflow)（Global State #3）

一旦 _burn() 更新了调用者的 WETH 余额，它接下来就会更新 WETH 的总供应量。

此时，totalSupply 从 2 变为 8，因为 2 − (2^256 − 6) 在 uint256 中发生下溢，并按模 2^256 环绕。

注意： 在 Solidity ≥0.8.0 版本中，像 totalSupply -= amount 这样的常规算术在下溢时会发生回退。然而，当合约使用 unchecked 块或在内联汇编 (inline assembly) 中执行此操作时，情况就不会如此，因为两者都遵循底层算术语义，其值会按模 2^256 环绕。

未解析的 ETH 转账与 AUTO-Havoc（Global State #5）

在 _burn() 完成后，withdraw() 试图使用底层的 call 将 ETH 转移给调用者：

Copy
call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)

在调用 withdraw() 之前，WETH 合约持有 2^256 − 3 wei。一次成功的 withdraw() 调用将把 2^256 − 6 wei 转移给调用者，并且应当使合约的 ETH 余额从 2^256 − 3 减少到 3。

如果我们查看 Global State #5 的追踪，我们会发现 Prover 起初正确地执行了这一计算：

然而，Prover 并没有就此止步。这个调用是发向一个外部的、未知的地址 (caller())。Prover 无法确定该被调用者的行为（即调用者的 fallback 函数）。

当 Prover 面临这种未解析的外部调用时，它会自动应用 AUTO-havoc 摘要 (summary)。

在 AUTO-havoc 之下，Prover 假设外部调用成功，但可能会随意修改与该调用相关的状态变量。它这样做是因为缺乏被调用者代码的具体模型。

在调用追踪中，我们看到在正确的计算完成后，这种情况立即发生了：

这个 havoc 覆盖了计算得出的余额。在下一个状态（Global State #6）中，合约的余额变为：

这意味着 Prover 忽略了计算结果 (3)，并将一个任意值 (5) 分配为 havoc 摘要的一部分。这个被 havoc 后的值正是后续用于后置状态检查的值。

后置状态与不变量失败（Global State #7）

在 withdraw 函数完成后，Prover 在后置状态下检查不变量：

nativeBalances[currentContract] >= totalSupply()

此时，符号值为：

• WETH.balance = 0x5（由 AUTO-havoc 设置）
• WETH.totalSupply() = 0x8（被下溢破坏）

因此，不变量的评估结果为：

Copy
5 >= 8 ❌ (false)

Prover 由此得出结论，不变量被破坏了。

根本原因

这个违例是一个典型的误报 (false positive)。它的发生并不是因为 WETH 合约 withdraw() 的实现存在逻辑缺陷。相反，它是由于 Prover 约束不足的符号推理 (under-constrained symbolic reasoning) 造成的：

1. 整个执行路径之所以成为可能，只是因为 Prover 假设了一个不可能的前置状态，其中 balanceOf(msg.sender) (2^256 - 2) 远远大于 totalSupply (2)。
2. 这个由无约束符号变量引起的不现实假设，直接触发了 totalSupply 变量的算术下溢，使其从 2 变成了 8。

auto-havoc 步骤也对最终值产生了影响，但是状态早已受到了下溢不可挽回的影响。

使用 Preserved Blocks 修复误报违例

现在已经很清楚了，Prover 标记出违例并不是因为 WETH 合约存在缺陷，而是因为它探索了在真实执行中永远不会发生的符号状态。我们下一步要做的是引导 Prover 回到现实行为中来。

我们通过添加 preserved blocks 来实现这一点，这些代码块在前置状态检查和符号执行之间引入了额外的假设。这些假设可以防止 Prover 进入不可能的执行路径，例如合约自我调用或荒唐的代币余额。

修复 deposit() 和 receive() 的违例

这两个违例都是由于 Prover 假设了自调用 (self-calls)，在这个模型中 WETH 合约成为了自身的调用者。这在实际执行中是不可能的，但在符号执行中如果不加限制就是有效的。

我们通过添加一个 preserved block 来修复此问题，该代码块排除了任何合约调用自身函数的场景：

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with(env e) {
        require e.msg.sender != currentContract;
    }
}

这一个假设就移除了所有的自调用追踪，立刻消除了 deposit() 和 receive()（在 Prover UI 中报告为 receiveOrFallback()）中的误报。

既然 deposit() 和 receive() 的自调用问题已解决，我们现在可以转向导致误报的第二个根源：withdraw() 内部不现实的符号假设。

修复 withdraw() 的违例

withdraw() 中的失败是由其他原因造成的：Prover 假设 balanceOf(msg.sender) 可以任意大，甚至大于总供应量。这迫使 _burn() 沿着一条本该回退的路径执行，触发了下溢并破坏了 totalSupply。

为了防止这种情况，我们专门为 withdraw() 添加了一个 preserved block：

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
    //we also added the signature of balanceOf()
    function balanceOf(address) external returns(uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    // Generic Block
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    // Function-Specific Block
    preserved withdraw(uint256 amount) with (env e) {
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

在上面更新的 spec 中，require balanceOf(e.msg.sender) <= totalSupply(); 这一行指示 Prover 忽略任何用户代币余额超过总供应量的执行路径。

这几个 preserved blocks 一起消除了以前引起误报的每一条不现实的执行路径。有了这些约束条件，我们现在可以重新运行 Prover 以检查不变量在现实假设下是否仍然成立。

重新运行验证

应用这两个修复后，再次运行 Prover，打开验证结果链接，查看类似于下图的输出。

这一次，Prover 确认 tokenIntegrity 不变量在所有验证阶段都成立，通过了归纳基础和归纳步骤。

报告显示所有相关函数——包括 deposit()、withdraw()、transfer() 和 approve()——现在都能保持该不变量。

至此，不变量已经成功验证，规范 (specification) 也是正确的。不过，我们还可以进一步简化它。我们前面添加的两个假设具有相同的结构，并且不依赖于任何函数参数，这意味着我们可以将它们整合到一个单独、更清晰的 preserved block 中。

更清晰、更统一的规范

在我们的案例中，前面添加的两个假设都有一个重要的属性：

“它们仅依赖于交易环境 (env) 和合约的全局状态。它们不依赖于任何特定函数的参数。”

这意味着它们是关于该合约的全局真理：

1. 合约绝不会是它自己的调用者。
2. 调用者的余额绝不会超过总供应量。

由于这两个条件都不依赖于函数的参数，因此都可以安全地放入一个通用的 preserved block 中，如下所示：

Copy
methods {
    function totalSupply() external returns (uint256) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}

invariant tokenIntegrity()
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

当我们使用这个合并后的代码块运行 Prover 时，规范被无错误地接受，不变量在所有验证阶段都保持成立，如下图所示：

Constructor Preserved Blocks（基础步骤假设）

到目前为止，我们已经讨论了 preserved blocks 作为在不变量验证的归纳步骤期间约束 Prover 的一种方法——即，在假设不变量预先成立的情况下，检查 public 和 external 函数是否保持了该不变量。

从 Prover 版本 8.5.1 开始，CVL 还支持应用于不变量验证的基础步骤 (base step) 的 constructor preserved blocks。

在基础步骤中，Prover 对构造函数进行符号执行，以验证不变量在部署后是否立即成立。主合约的存储（currentContract）被初始化为零，但在多合约场景中，验证场景中的其他合约会从任意的符号状态开始。

这是早期 Prover 版本的一个改变，早期版本中所有合约的存储都被假设为清零——相当于一次性重新部署整个系统。当前的行为使得对已部署系统的建模更加逼真，但这也意味着基础步骤验证可能会从实际部署中永远不会出现的状态开始。

当一个不变量依赖于与这些外部合约的关系时，符号环境可能会违反那些在实际中成立的假设，从而导致基础步骤因纯粹的符号化原因而失败。Constructor preserved blocks 允许我们明确地重新引入这些假设，确保基础步骤反映出真实的部署上下文。

其语法与其他 preserved blocks 类似，但作用域被限制在构造函数 (constructor) 内：

Copy
preserved constructor() with (env e) {
    require e.block.timestamp != 0;
}

该代码块仅应用于基础步骤，对归纳步骤或单个函数的验证没有影响。

在本章中，WETH 案例研究中的误报违例出现在归纳步骤，因此通过通用和函数级别的 preserved blocks 解决了这些问题。当一个不变量由于初始符号环境的不现实假设而在部署后立即失败时，constructor preserved blocks 是最有用的。

结论

Preserved blocks 是在 CVL 中完善不变量验证的强大工具。通过将 Prover 约束为符合现实的假设——无论是在函数执行期间，还是在需要时的部署期间——它们可以在保持证明强度的同时消除误报。

通过 WETH 的案例研究，我们看到了精心挑选的 preserved blocks 如何引导 Prover 远离不可能的符号状态并走向有意义的执行，确保不变量在能够准确反映真实世界行为的条件下得到验证。

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