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

1. 在验证运行开始时，Prover 会为 ghost 变量选择任意（havoc 后的）值。
2. **Ghost 变量被视为合约存储的扩展。**如果在符号执行（symbolic execution）期间交易发生回滚（revert），Prover 也会回滚该路径上的任何 ghost 更新，以保持它们与合约存储状态的一致性。

第二种情况通常不需要担心，因为在交易期间回滚 ghost 值反映了正常的存储行为。然而，第一种情况可能会导致不正确或具误导性的验证结果。

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

理解未约束 Ghost 变量的危险性

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

Copy
//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {

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

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

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

// Ghost variable to track how many times the `count` variable is updated
ghost mathint countIncrementCall;

// Hook triggered before `count` is updated via SSTORE
hook Sstore count uint256 updatedValue (uint256 prevValue) {
    // Increment the ghost each time `count` is about to be modified
    countIncrementCall = countIncrementCall + 1; 
}


/*
*Rule to verify that count increases by exactly the number of times increment()
is called
*/

rule checkCounterIncrements() {

    // Capture the value of `count` before any updates
    mathint precallCountValue = count();

    // Perform three increment operations
    increment();
    increment();
    increment();

    // Capture the value of `count` after updates
    mathint postCallCountValue = count();

    // Assert that `count` increased by the same amount as tracked by the ghost
    assert postCallCountValue == precallCountValue + countIncrementCall;
}

上述规范执行了以下操作：

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

乍一看，这个规范在逻辑上似乎很完善。然而，当它通过 Certora Prover 运行时，未能验证通过 checkCounterIncrements 规则，如下方的输出结果所示：

要理解该断言为何失败，让我们深入研究一下 Prover 提供的调用跟踪（call trace）。

为什么验证失败了

我们对调用跟踪的分析揭示，规则验证失败并非由于逻辑上的任何缺陷，而是因为 ghost 变量 countIncrementCall 的初始值是由 Prover 对抗性地选择的，在这个例子中为 -0x2（即 -2）。重要的是，这个值并非被错误选中。相反，它是通过一个被称为 havocing 的系统化过程被故意赋予的。

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

在这个特定案例中，存储变量 count 以 0xA（十进制为 10）启动，而 countIncrementCall 则以 -2 启动。在调用 increment() 三次后，count 达到了 0xD（十进制为 13），同时 ghost 变量从 -2 增加到了 1。然而，该断言预期的条件是：

Copy
postCallCountValue == precallCountValue + countIncrementCall;

将实际值代入后，它变成了：

Copy
13 == 10 + 1

这显然是错误的，因此验证失败了。

值得铭记的“教训”

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

虽然这种方法使验证详尽无遗，但它也可能引入不切实际的初始条件。如果某个规则依赖于合约存储与 ghost 变量之间存在意义的关联，havocing 可能会通过让它们从无关的值启动来破坏这种关联。例如，一个表示 increment() 调用次数的 ghost 变量可能会以 -2 或 5 启动，即使尚未发生任何对 increment() 函数的调用。

当这种情况发生时，规则可能会失败——不是因为它的逻辑有缺陷，而是因为验证始于一个在实践中永远不可能存在的状态。这类失败属于_假阳性（false positives）_：它们暴露的是符号初始化与语义意图之间的不匹配，而不是合约中存在真正的问题。

“解决方案”是什么

避免这些错误失败的关键在于确保在验证开始之前，ghost 变量和合约存储之间的初始关系在逻辑上是正确的。这并不意味着要固定它们的确切值，而是对它们进行约束，使得它们从一个合理的状态开始。

例如，在我们的规则中，ghost 变量 countIncrementCall 旨在表示 increment() 被调用的次数。在规则开始时，在任何调用发生之前，这个数字必须为 0。合约的 count 变量可以从任意值启动——0、10 甚至 100——但 ghost 应该始终从 0 开始，因为尚未发生任何递增操作。

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

Copy
require countIncrementCall == 0;

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

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

使用 require 语句约束 Ghost 变量

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

我们可以直接在规则中对这个约束进行编码，只需在规则的开头简单地加上 require countIncrementCall == 0; 即可。

Copy
// Rule to verify that `increment()` increases `count` by exactly the number of times it's called
rule checkCounterIncrements() {

    //Add the require statement to constrain the ghost
    require countIncrementCall == 0;

    // Capture the value of `count` before any updates
    mathint precallCountValue = count();

    // Perform three increment operations
    increment();
    increment();
    increment();

    // Capture the value of `count` after updates
    mathint postCallCountValue = count();

    // Assert that `count` increased by the same amount as tracked by the ghost
    assert postCallCountValue == precallCountValue + countIncrementCall;
}

通过包含这个前置条件，我们确保了 Prover 在一个逻辑上有意义的状态下开始执行规则，此时合约的存储与 ghost 的语义是一致的。Prover 依然会执行完整的符号和对抗性探索，但它现在会避免探索那些不可能出现的状态，比如 ghost 变量 countIncrementCall 从 -2 或 5 启动的情况。

当重新运行验证时，count 和 countIncrementCall 都会从逻辑一致的状态开始。它们的值可能会不同——例如，count 可能从 10 开始，而 countIncrementCall 从 0 开始——然而它们之间的关系依然是合理的。

从此时起，每次对 increment() 的调用都会完美同步地更新合约的存储与 ghost 变量。在三次调用后，count 增加了三，countIncrementCall 也记录了三次更新。因此，该断言

Copy
assert postCallCountValue == precallCountValue + countIncrementCall;

在所有有效的执行路径上均能成立，这证实了该规则现在验证成功了。

这演示了仅仅单行 require countIncrementCall == 0 代码就能如何通过将 Prover 的分析锚定在逻辑合理的起跑点上来消除错误的验证失败。它没有限制验证的范围；相反，它确保了探索空间在语义上是有效的，并且任何规则的失败都能反映真正的逻辑问题，而非任意初始化带来的产物。

然而，在这个规范中有一个重要的假设值得我们进一步深入思考。

在这里，ghost 变量 countIncrementCall 在向 count 存储槽写入时发生递增，这种方式目前是有效的，因为 count 当前仅在 increment() 内部被修改。但是如果另一个函数——比如 reset() 或 setCount()——也修改了 count 会怎样？即使 increment() 未被调用，该 ghost 变量依然会递增。

这凸显了一个重要的设计考量因素：**对何种对象使用 hook 决定了 ghost 实际跟踪的内容。**在这个案例中，我们跟踪的是_存储写入_，而不是_函数调用_。对于简单的合约，这两者可能是等效的——但随着合约变得日益复杂，这种等效性可能会被打破。我们将在后面的章节中探索能够解决此限制的替代 hook 策略。

结论

未加约束的 ghost 变量可能会导致 Prover 去探索不切实际的状态，从而引发具误导性的验证失败。通过使用 require 语句约束其初始值，我们可以确保 ghost 变量从与合约存储逻辑一致的状态启动。这个微小但至关重要的步骤让验证既保持详尽无遗，又保证语义有效，使得 Prover 仅报告真正的逻辑问题。

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