为了证明某个属性或不变量（invariant）成立，通常需要检查特定存储位置的更改，特别是当存储无法从外部访问，或者合约没有显式计算或暴露我们关心的值时。

例如，假设我们想在一个 ERC-20 实现中验证：totalSupply 的值始终等于所有独立账户余额的总和。 乍一看，这似乎很简单：我们可以使用 assert totalSupply() == sumOfBalances()。

然而，困难在于合约实际上从未维护过这个累加和；它只是将每个账户的余额存储在一个 mapping 中。与显式存储且可以直接查询的 totalSupply 不同，“余额总和 (sum of balances)” 并不存在于合约的状态中。相反，这些信息分布在多个存储槽（storage slots）中，如果不观察这些槽是如何被访问和更新的，就无法验证这种关系。当其中一些变量是 private 时，挑战就更大了。

为了应对这一挑战，CVL 提供了 hooks 和 ghost 变量。Hooks 允许我们观察底层事件（例如对存储的读写），而 ghost 变量则允许我们 捕获、聚合和共享 这些观察结果，以便在规范（specification）的其他地方引用它们。它们共同弥合了合约内部行为与高级验证规则之间的鸿沟，使我们能够推导依赖于隐藏或隐式状态更改的属性。

在本章中，你将了解 hooks 的工作原理、可用的不同类型以及与它们相关的限制。我们还将向你介绍 ghost 变量，这是 CVL 的一个核心特性，它实现了 hooks 和 rules 之间的通信，使你能够验证隐藏在合约内部存储中的丰富正确性属性。

理解“需求”

为了更好地理解我们所讨论的问题，请看下面的智能合约，它保留了一个 private 的 count 和在部署时设置的 owner。increment() 和 resetCounter() 都受到 onlyOwner modifier 的保护：increment() 将 private 的 count 加一，resetCounter() 将其重置为零，并且只有存储在合约中的 owner 地址才能调用这两个函数。

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


contract Counter {

    // State variables
    address private owner;
    uint256 private count;



    /// @notice Initializes the contract and sets the deployer as the owner
    constructor() {
        owner = msg.sender;
    }


    /// @notice Restricts function calls to the contract owner only
    modifier onlyOwner() {
        require(msg.sender == owner, "Counter: caller is not the owner");
        _;
    }

    // External functions

    /// @notice Increments the counter by 1
    /// @dev Only callable by the owner
    function increment() external onlyOwner {
        count++;
    }

    /// @notice Resets the counter to 0
    /// @dev Only callable by the owner
    function resetCounter() external onlyOwner {
        count = 0;
    }
}

现在假设我们想形式化验证以下属性：

1. owner 一旦在 constructor 中设置，就绝不能更改。
2. 对 increment() 的调用应使 count 准确增加 1。

乍一看，这两个属性都很简单。然而，以 CVL rules 的形式表达它们会带来一些挑战。将第一个属性表达为 CVL rule 的问题在于，owner 变量被标记为 private，而且合约没有提供 getter 来暴露它的值。如果无法从 rule 中访问它，我们就无法断言它在 constructor 中设置后保持不变。

第二个属性引入了不同的挑战。虽然我们可以在 rule 中调用 increment()，但变量 count 是 private 的，且合约没有提供 getter 来读取它的值。这意味着 rule 无法直接看到函数运行时 count 发生了什么。

由于 rules 只能观察函数的输入和输出，而不能观察内部存储的更改，因此它们无法在 count 更新时捕获其旧值和新值。如果没有这种可见性，Certora Prover 就无法确认每次对 increment() 的调用是否确实将计数器加一。

简而言之，问题不在于这些属性难以陈述，而在于它们依赖于 底层存储行为 (low-level storage behavior)，并需要直接观察执行期间存储是如何更新的。标准的 CVL rules 仅限于通过公共接口与合约交互，因此它们无法捕获这些内部更改。为了验证如 owner 的不可变性或计数器的精确增量等属性，我们需要一种工具，允许我们窥探合约内部，监控其存储操作，并将这些观察结果带入我们的规范中。

这就是 hooks 发挥作用的地方。

什么是 Hooks？

在 CVL 中，hooks 是一段代码块，当智能合约执行底层 EVM 操作（例如读写存储、执行 opcode 或修改 transient 数据）时，它们会在验证过程中自动运行。

hook 使用 hook 关键字定义，每个 CVL hook 指定以下内容：

1. 它监听的 操作 (operation)（例如 SLOAD、SSTORE 或特定的 EVM opcode）。
2. 当检测到该操作时执行的 CVL 代码块，从而提供对该事件相关数据的访问。

Hooks 的类型

CVL 提供了 3 种不同类型的 hooks，按它们监控的操作类型进行分类。这 3 种类型是：

1. Storage Hooks
2. Opcode Hooks
3. Transient Storage Hooks

对于本章，我们将重点关注 Storage Hooks，因为它们适用范围最广，并构成了理解 hooks 在 CVL 中工作原理的基础。其他类型的 hooks 在特定上下文中同样有用，我们将在后面的章节中介绍它们。

什么是 Storage Hooks？

Storage hooks 是 CVL 中的一种特定类型的 hook，只要合约的存储变量被访问（无论是读取还是写入），它们就会被触发。换句话说，当 EVM 对受监控的存储槽执行读取 (SLOAD) 或写入 (SSTORE) 操作时，它们就会激活，从而允许我们：

• 捕获正在读取或写入的值。
• 在访问或修改变量时强制执行条件。
• 跟踪合约状态在不同执行中的演变过程。

CVL 中主要有两种 storage hooks：

1. The Load Hooks
2. The Store Hooks

1. The Load Hooks

当对受监控的存储变量发生读取操作（SLOAD）时，会触发 load hook，并允许你捕获正在读取的值。

它使用 hook Sload 关键字定义，后跟一个用于保存加载值的 CVL 变量的类型和名称，最后是受监控的合约存储变量的名称。

Copy
hook Sload address contractOwner owner { ... }

每当被验证的合约为了读取操作而访问其类型为 address 的 owner 存储变量时，上述 hook 就会执行。然后，该值将存储在 CVL 变量 contractOwner 中。

2. The Store Hooks

Store hooks 会在对任何特定存储变量进行任何写入操作之前执行。

Store hooks 也使用 hook 关键字定义，后跟 Sstore 关键字。之后，你指定受监控的合约存储变量的名称，以及将保存即将写入该存储位置的值的 CVL 变量的类型和名称。

Copy
hook Sstore owner address newOwner{...}

作为可选项，该模式还可以包含用于存储正在被覆盖的旧值的变量的类型和名称。

Copy
hook Sstore owner address newOwner (address oldOwner) {...}

在我们应用 hooks 来验证 Counter 合约的属性之前，有一个重要的限制需要理解：在 hooks 内部声明的变量是 hook 代码块的局部变量，对 rules 不直接可见。

理解 Hooks 的限制

hook 不仅允许我们监控特定的存储变量，还可以通过将其存储在 CVL 变量中以供使用来提供对其值的访问。然而，一个限制是：在 hooks 内定义的 CVL 变量的作用域仅限于该 hook 本地，这意味着无法从 rules 中直接访问它们。

要理解此限制，请考虑下面的规范，该规范旨在证明 Counter 合约的 owner 在其首次于 constructor 中设置后永远不会改变：

Copy
hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;


}

在上面的 spec 中，Sload hook 使得 private 的 owner 变量在每次被读取时都是可观察的，将其值存储到 contractOwner 中。在 rule 中，spec 将这个观察到的值保存为 prevOwner，对具有任意输入的任何合约函数执行符号调用（symbolic call），然后再次将 owner 观察为 currentOwner。最后，它断言 prevOwner == currentOwner，这意味着在所有可能的调用中，owner 必须保持一致。

然而，当你运行 Certora Prover 时，你将遇到以下错误：

上述错误仅仅突显了这样一个事实：rule checkOwnerConsistency() 无法访问和使用我们在 load hook 中声明的 contractOwner。

这可能会引发一个问题：如果 hooks 的设计是为了捕获和存储数据，为什么我们不能在 rules 中直接使用这些数据呢？

答案在于 hooks 中定义的变量的作用域。

Hooks 的作用域限制

当你在 hook 内定义变量时，其作用域 仅限于该 hook 的本地。这就像在函数内部定义变量一样——它可以在该代码块内使用，但在外部是不可见的。这就是为什么 contractOwner 在 hook 内部是完全有效的，但对于 rule checkOwnerConsistency() 来说却完全未知。

这意味着 CVL rules 和 hooks 并不共享变量——它们在各自独立的作用域中运行。

那么，我们如何利用在 hook 中提取的信息来编写有用的 rules 呢？

答案是 ghost 变量（ghost variables）。

使用 Ghost 突破作用域限制

虽然我们无法在 rules 中直接访问 hook 变量，但我们可以定义称为 ghost 变量（或简称为 ghosts）的特殊变量，以在 hooks 和 rules 之间传递信息。

ghost 是使用 ghost 关键字后跟其类型和名称来声明的，如下所示。

Copy
ghost bool hasVoted;
ghost uint x;
ghost mathint numVoted;
ghost mapping(address => mathint) balances;

ghost 变量可以是任何 CVL 支持的类型或 mapping。在 mapping 的情况下，其键必须是 CVL 支持的类型，其值可以是 CVL 类型或其他 mapping。

验证 Counter 合约中的 Owner 一致性

为了使 checkOwnerConsistency() rule 按照预期工作，在 hook 内部观察到的值需要能在 rule 的作用域内使用。我们可以通过将观察到的值存储在 ghost 变量中来实现这一点。实现这一目标的步骤如下：

1. 声明一个 ghost 来保存 观察到的 owner 值： 在我们规范的顶层，引入一个名为 ghostOwner 的 ghost 变量。每当读取合约的 owner 槽时，这个 ghost 将作为其值的容器。

Copy

/// Top-level ghost variable to mirror the contract's `owner` slot
ghost address ghostOwner;

hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;

}

声明 ghost 变量时，务必加上 ghost 或 ghost_ 前缀（例如 ghostOwner、ghost_owner），以明确将它们与 Solidity 存储变量和 hook 本地 CVL 变量区分开来。

在此阶段，ghost 变量 ghostOwner 已被声明，但尚未与合约的存储进行同步。

2. 在 hook 内部同步 ghost： 接下来，修改 Sload hook，这样无论合约何时对 owner 存储槽执行读取操作，hook 都会捕获该值并 将其写入 ghost。

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    //assign captured value to ghost
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;


}

这就建立了一座桥梁，从合约的 private 存储连接到 hook，然后再从 hook 连接到一个能够在 hook 局部作用域之外持久存在的 ghost 变量。每次合约读取 owner 时，ghost ghostOwner 都会与该存储值进行同步。

3. 在 rule 内部使用 ghost： 最后，更新 checkOwnerConsistency() rule，使其不再使用 hook 本地的 contractOwner，而是引用 ghost ghostOwner。

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

    //Take a snapshot of the ghost before the call
    address prevOwner = ghostOwner;

    //parametric call
    method f;
    calldataarg args;
    f(e,args);
     
    //Take another snapshot after the call
    address currentOwner = ghostOwner;

     
    assert prevOwner == currentOwner;
}

按照上述说明更新规范后，使用 certoraRun 命令 重新运行 Certora Prover。这次 Prover 将毫无错误地编译我们的 rule，并将验证结果打印在终端中。结果将类似于下图：

看到上面的结果后，你可能会感到惊讶，并想知道为什么尽管 Counter 合约从未显式更新其 owner，我们的 rule 仍然失败了。原因不在于 Solidity 代码，而在于 Prover 是如何解释 ghosts 以及在验证运行期间如何执行 hooks 的。

将 Ghosts 与 Storage 同步

Ghost 变量不会自动与合约的存储绑定。在执行开始时，Prover 会为它们分配 havoced 值（即被扰乱的值）——这是任意的占位符，除非显式初始化，否则它们在不同的执行轨迹（traces）中可能会发生变化。在我们的例子中，ghost ghostOwner 仅在读取 owner 槽（通过 Sload）时才会更新。如果在 rule 比较 prevOwner 和 currentOwner 之前没有发生读取操作，则 ghost 将保持未初始化状态，持有一个与实际存储无关的任意值。

实际发生的情况是这样的：owner 的存储槽持有一个地址（例如 0x2712 或 0x2711），但 ghost ghostOwner 包含了一个完全不同的值（例如 0x401）。

由于 ghost 从未与存储对齐，我们的 rule 最终比较了两个毫无意义的值，而 Prover 非常正确地报告了失败。

我们可以看到，主要问题在于 ghost 变量不会自动镜像合约存储。为了修复这个问题，我们需要确保在 rule 中使用 ghost 之前，通过 hook 显式地对其进行更新。在实践中，这意味着强制合约对相关的存储槽执行读取操作，以便 Sload hook 能够触发并将 ghost 与存储中的实际值同步。

为了实现这一点，我们只需进行一次初始调用，使合约读取 owner 槽，这反过来会触发 Sload hook 并更新我们的 ghost。在我们的例子中，我们将通过在 rule 开始处调用 resetCounter(e) 来实现这一点。由于 resetCounter(e) 受 onlyOwner modifier 的保护，EVM 必须读取 owner 存储槽来检查 modifier 的条件。这次读取会自动触发 hook，从而确保 ghostOwner 在被我们捕获到 prevOwner 之前已得到更新。

下面是显示完整修改后 rule 的 更新规范：

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

// Updated rule: now includes an initial sync call
rule checkOwnerConsistency(env e) {

    // NEW: Force an SLOAD of `owner` so the hook fires and syncs `ghostOwner`
    resetCounter(e);
    
    /// Take the first snapshot after synchronization
    address prevOwner = ghostOwner;
    
    //parametric call
    method f;
    calldataarg args;
    f(e, args);

    // Take another snapshot after the call
    address currentOwner = ghostOwner;

    // The owner must not change across any call
    assert prevOwner == currentOwner;
}

rule 内的 第一行（resetCounter(e);）是关键的补充。

现在 ghost 已经正确同步，prevOwner 和 currentOwner 之间的比较变得有意义了，这使得 Prover 能够正确地验证 owner 变量的一致性。

让我们一步一步来分解这里 发生 了什么：

1. 初始同步调用 (resetCounter(e))
   • rule 首先调用 resetCounter(e)。
   • 为了检查 onlyOwner modifier，合约 必须读取 owner 槽（SLOAD）。
   • 这一读取操作 触发了 Sload hook，该 hook 将观察到的值写入 ghost ghostOwner 中。
   • 结果是，在截取任何快照之前，ghostOwner 现在与实际的存储值实现了同步。
2. 第一次快照 (prevOwner)
   • 同步之后，rule 立即执行 address prevOwner = ghostOwner;。
   • 由于步骤 1，prevOwner 也就是合约中存储的 真实的 owner。
3. 任意调用 (method f; calldataarg args; f(e, args);)
   • Prover 现在探索具有符号化输入的 任意外部调用。
   • 在这个合约中，这意味着带有任意参数的 increment(...) 或 resetCounter(...)。
   • 这两个函数都受 onlyOwner 保护，并且 不会写入 owner。
   • 在此调用期间，任何对 owner 的额外读取（因为 onlyOwner）都将 重新触发 Sload hook，但它只是将 相同的值 写入 ghost。
4. 第二次快照 (currentOwner)
   • 任意调用返回后，rule 执行 address currentOwner = ghostOwner;。
   • 由于合约从未改变 owner，且 hook 只镜像读取操作，因此 currentOwner 等于之前捕获的相同存储值。
5. 断言 (Assertion)
   • rule 检查 assert prevOwner == currentOwner;。
   • 由于合约在部署后从未修改 owner，因此不存在这两个快照会产生差异的代码路径。
   • 因此，在所有探索的执行中，prevOwner 和 currentOwner 始终保持相等。
   • 结果是，Prover 没有找到任何反例，并报告该 rule 为 已验证 (verified)。

随着 owner 属性得到验证，我们现在转向前面提到的第二个属性。

验证 Counter 合约中的 Increment() 调用

我们想要证明的第二个属性是：对 increment() 的调用应使 count 准确增加 1。由于 count 是 private 的，单凭 rules 无法观察到 count++ 所执行的实际存储写入。为了证明这个属性，我们将一个 store hook 附加到 count 槽，捕获写入前和写入后的值，将它们持久化到 ghosts 中，最后在 rule 中断言这种算术关系。

完整的规范如下所示：

Copy
methods {
    function increment() external;
}


ghost mathint ghost_prevCount;

ghost mathint ghost_currentCount;

hook Sstore count uint256 postcallValue (uint256 precallValue) {
    ghost_prevCount = precallValue;
    ghost_currentCount = postcallValue;
}

rule checkCounter() {

    env e;

    //call to increment
    increment(e);

    assert ghost_currentCount == ghost_prevCount + 1; 
}

在上面的 spec 中，只要调用 increment() 函数，hook 就会观察 count 存储槽的更新。旧值（precallValue）存储在一个 ghost 变量（ghost_prevCount）中，而新值（postcallValue）存储在另一个 ghost 变量（ghost_currentCount）中。这允许 rule 检查在调用 increment() 函数之后，计数器是否如预期那样准确增加了 1。

当我们在上述 spec 上运行 Prover 时，我们将看到该 rule 已经通过了验证，如下图所示：

让我们一步一步来分解这里发生了什么：

1. 调用前：合约的 private 变量 count 有某个初始值（比方说 X）。
2. 在 increment() 调用期间：
   • EVM 执行 count++ 语句，这转化为对 count 存储槽的先读后写操作。
   • 就在写入发生之前，触发了 Sstore hook。
   • hook 捕获即将被覆盖的值（precallValue）和正在写入的新值（postcallValue）。
   • 这些值存储在 ghost 变量 ghost_prevCount 和 ghost_currentCount 中。
3. rule 检查：
   • 函数调用完成后，rule 断言 ghost_currentCount == ghost_prevCount + 1。
   • 考虑到 ghost_currentCount = X + 1 并且 ghost_prevCount = X，该断言成立。

因此，我们从 Prover 那里得到了已验证的结果。换句话说，任何对 increment() 的调用都会使计数器准确加一，Prover 能够形式化验证此属性，而未发现任何反例。

作为存储扩展的 Ghost 变量

我们可以看到，hooks 用于通过检测对合约存储的特定读或写操作来观察和收集数据。然而，由于在 hooks 内部声明的变量是 hook 局部的，它们的值在 hook 执行完毕后就会消失。为了在整个规范中保留和重用这些信息，CVL 引入了 ghost 变量 —— 这是一种持久的、规范级别的存储，它镜像或扩展了合约的实际状态。正因如此，ghost 变量可以被视为并被处理为合约存储的延伸。

事实上，Certora Prover 对待 ghost 变量的方式与常规存储非常相似：

• 如果进行中的交易随后发生 revert，任何对 ghost 的更新都会自动 revert，就像存储一样。
• 在验证运行开始时，ghosts（与其他 CVL 变量一样）代表任意的（havoced）值，除非在规范中显式设置它们，这反映了 Prover 对存储的符号化视角。

我们将在后面的章节中更详细地探讨这些行为，在那里我们还将学习如何显式地初始化 ghost 变量，以避免意外的 havoc（扰动），并确保更可预测的验证结果。

结论

Certora hooks 对存储和 EVM 操作提供了强大的可观测性。然而，它们的变量被限制在每个 hook 的局部作用域内。Ghost 变量通过捕获来自 hooks 的数据并使其可供 rules 访问来解决此问题，从而在验证期间实现对合约内部状态的有效且全面的推理。

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