约束规则中的幽灵变量

使用 Certora 进行形式化验证

在规则中约束 Ghost 值

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

最后更新于 2026 年 2 月 13 日

在上一章中，我们学习了 ghost 变量如何允许信息从Hook流向规则。我们还了解到：

1. 在验证运行开始时，Prover 为 ghost 变量选择任意（havoced）值。
2. Ghost 变量被视为合约存储的扩展。如果在符号执行期间事务回滚，Prover 也会回滚该路径上的任何 ghost 更新，使其与合约的存储状态保持一致。

第二种情况通常不是问题，因为在事务期间回滚 ghost 值反映了正常的存储行为。然而，第一种情况可能导致不正确或误导性的验证结果。

在本章中，我们将演示这个问题如何影响验证，并解释如何通过使用 require 语句在 ghost 变量和合约状态之间建立一致性来解决它。

理解无约束 Ghost 的危险

为了了解无约束 ghost 变量如何影响验证，让我们回顾一下前面章节中使用的 Counter 合约。

Copy//SPDX-许可证标识符：MIT
pragma solidity 0.8.24;
contract Counter {

    uint256 public count;

    function increment() external {
        count++;
    }
}

考虑下面的规范，它旨在验证每次对 increment() 函数的调用都能正确地增加 count 变量。它确保 count 的总变化量与函数被调用的次数（由 ghost 变量 countIncrementCall 跟踪）相匹配。

Copymethods {
    function increment() external envfree;
    function count() external returns (uint) envfree;
}

// Ghost 变量，用于跟踪 `count` 变量更新了多少次
ghost mathint countIncrementCall;

// 在 `count` 即将通过 SSTORE 更新之前触发的Hook
hook Sstore count uint256 updatedValue (uint256 prevValue) {
    // 每次 `count` 即将被修改时，增加 ghost
    countIncrementCall = countIncrementCall + 1;
}

/*
*规则，用于验证 count 增加的次数恰好是调用 increment() 的次数
*/

rule checkCounterIncrements() {

    // 在任何更新之前捕获 `count` 的值
    mathint precallCountValue = count();

    // 执行三次增量操作
    increment();
    increment();
    increment();

    // 在更新之后捕获 `count` 的值
    mathint postCallCountValue = count();

    // 断言 `count` 的增加量与 ghost 跟踪的量相同
    assert postCallCountValue == precallCountValue + countIncrementCall;
}

上述规范执行以下操作：

1. 我们声明一个类型为 mathint 的 ghost 变量 countIncrementCall，作为我们的独立计数器。
2. 我们使用一个 Sstore Hook来监视 count 变量。每当合约向 count 写入新值时，此Hook就会被触发，并增加 countIncrementCall ghost。
3. checkCounterIncrements 规则建立了一个测试场景。它读取 count 的初始值，调用 increment() 三次，然后读取最终值。
4. 最后，它断言最终计数必须等于初始计数加上我们的 ghost 跟踪的增量次数。由于我们调用了 increment() 三次，countIncrementCall 应该为 3，因此断言预期成立。

乍一看，这个规范在逻辑上是合理的。然而，当它通过 Certora Prover 运行时，未能验证 checkCounterIncrements 规则，如下图所示：

为了理解断言失败的原因，让我们深入研究 Prover 提供的调用跟踪。

为什么验证失败了

我们对调用跟踪的分析表明，规则失败并非由于逻辑缺陷，而是因为 ghost 变量 countIncrementCall 开始时有一个 Prover 对抗性选择的值，在本例中为 -0x2（或 -2）。重要的是，这个值并非错误选择。相反，它是通过一种称为 havocing 的系统过程有意分配的。

Havocing 是 Prover 为状态或 ghost 变量分配任意（无约束）初始值的机制。这里的“任意”意味着该变量可以在其类型范围内自由取任何值。通过这样做，Prover 可以系统地检查可能导致验证失败的边缘情况和极端场景。这项技术使验证过程穷尽，允许 Prover 推理合约可能达到的所有可能状态。

在这个特定案例中，存储变量 count 开始于 0xA（十进制 10），而 countIncrementCall 开始于 -2。在调用 increment() 三次之后，count 达到 0xD（十进制 13），ghost 变量从 -2 增加到 1。然而，断言预期：

CopypostCallCountValue == precallCountValue + countIncrementCall;

代入实际值后，变为：

Copy13 == 10 + 1

这显然是假的，因此验证失败。

需要记住的“教训”

这次失败突出了 Prover 操作方式的一个重要概念。在验证期间，Prover 不假设合约存储或 ghost 变量有任何默认或构造函数定义的初始值。相反，它 havocs 它们——在允许的范围内分配任意符号值。这种行为允许 Prover 推理合约的所有可能的起始状态，确保属性普遍成立，而不仅仅针对特定的初始配置。

虽然这种方法使验证穷尽，但它也可能引入不切实际的初始条件。如果规则依赖于合约存储和 ghost 变量之间的有意义的关系，havocing 可能会通过从不相关的值开始来破坏这种关系。例如，表示 increment() 调用次数的 ghost 可能会以 -2 或 5 开始，即使还没有发生对 increment() 函数的任何调用。

当这种情况发生时，规则可能会失败——不是因为其逻辑有缺陷，而是因为验证从在实践中永远不会存在的状态开始。这种失败是误报：它们突出的是符号初始化和语义意图之间的不匹配，而不是合约中的真实问题。

“解决方案”是什么

避免这些错误失败的关键是确保在验证开始之前，ghost 变量和合约存储之间的初始关系是逻辑正确的。这并不意味着固定它们的精确值，而是约束它们，使它们以有意义的状态开始。

例如，在我们的规则中，ghost 变量 countIncrementCall 旨在表示 increment() 被调用的次数。在规则开始时，在任何调用发生之前，这个数字必须是零。合约的 count 变量可能以任何值开始——0、10 或 100——但 ghost 应该始终以 0 开始，因为还没有发生任何增量。

为了强制执行这种逻辑一致性，我们在 CVL 中使用 require 语句。在 CVL 中，require 语句充当逻辑前置条件，告诉 Prover _只_从满足指定关系的初始状态探索所有可能的行为。通过添加一个简单的约束，例如：

Copyrequire countIncrementCall == 0;

我们有效地过滤掉了 ghost 初始值与其预期含义相矛盾的无意义配置。

有了这个约束，Prover 仍然执行对抗性探索，但它现在从语义有效的状态开始。这确保了在应用约束后发生的任何验证失败都对应于规则或合约逻辑中的一个_真正_问题——而不是任意初始化的人为副作用。

使用 require 语句约束 Ghost

如前所述，在我们的例子中，ghost 变量 countIncrementCall 旨在表示 increment() 函数被调用的次数。在规则执行开始时，尚未发生此类调用——这意味着此 ghost 的正确初始值应为零。

我们可以通过在规则开头简单地添加 require countIncrementCall == 0; 来将此约束直接编码到我们的规则中。

Copy// 规则，用于验证 `increment()` 增加 `count` 的次数恰好是调用它的次数
rule checkCounterIncrements() {

    // 添加 require 语句以约束 ghost
    require countIncrementCall == 0;

    // 在任何更新之前捕获 `count` 的值
    mathint precallCountValue = count();

    // 执行三次增量操作
    increment();
    increment();
    increment();

    // 在更新之后捕获 `count` 的值
    mathint postCallCountValue = count();

    // 断言 `count` 的增加量与 ghost 跟踪的量相同
    assert postCallCountValue == precallCountValue + countIncrementCall;
}

通过包含这个前置条件，我们确保 Prover 以逻辑上有意义的状态开始规则执行，其中合约的存储和 ghost 的语义是对齐的。Prover 仍然执行完整的符号和对抗性探索，但它现在避免探索不可能的状态，例如 ghost 变量 countIncrementCall 从 -2 或 5 开始。

当重新运行验证时，count 和 countIncrementCall 都以逻辑上一致的状态开始。它们的值可能不同——例如，count 可能从 10 开始，而 countIncrementCall 从 0 开始——但它们的关系仍然是健全的。

从现在开始，每次调用 increment() 都会完美同步地更新合约的存储和 ghost。三次调用后，count 增加三，countIncrementCall 也记录了三次更新。结果，断言

Copyassert postCallCountValue == precallCountValue + countIncrementCall;

在所有有效执行路径中都成立，确认该规则现在成功通过验证。

这表明一行 require countIncrementCall == 0 如何通过将 Prover 的分析固定到逻辑上合理的起点来消除错误的验证失败。它不限制验证范围；相反，它确保探索空间在语义上是有效的，并且任何规则失败都反映了真正的逻辑问题，而不是任意初始化的人为产物。

然而，这个规范中有一个重要的假设值得更深入的思考。

在这里，ghost countIncrementCall 在写入 count 存储槽时增加，这之所以有效，是因为 count 目前仅在 increment() 内部修改。但是，如果另一个函数——比如 reset() 或 setCount()——也修改了 count 怎么办？即使没有调用 increment()，ghost 仍然会增加。

这强调了一个重要的设计考虑：选择要钩取的内容决定了 ghost 实际跟踪的内容。在这种情况下，我们跟踪的是存储写入，而不是函数调用。对于简单的合约，这些可能等价——但随着合约变得更复杂，这种等价性可能会失效。我们将在后续章节中探讨解决此限制的替代钩取策略。

结论

无约束的 ghost 变量可能导致 Prover 探索不切实际的状态，从而导致误导性的验证失败。通过使用 require 语句约束它们的初始值，我们可以确保 ghost 以逻辑上与合约存储对齐的状态开始。这个虽小但关键的一步使验证既穷尽又语义有效，允许 Prover 仅报告真正的逻辑问题。

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

• 原文链接： rareskills.io/post/certo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～