简介

在前面的章节中，我们使用了 ghost 变量（通过 Sstore hook）来记录并未在智能合约中显式追踪的存储值和数量——例如，所有余额的总和。它们允许在验证期间观察并推导状态的变化或状态变量之间随时间推移的关系。

然而，在调用合约方法后的 rule 执行期间，ghost 变量可能会：

• 当 Prover 遇到未解析的外部调用时被 havoc，或者
• 当调用 revert 时回滚到它们之前的状态（重置）。

Ghost 在未解析的外部调用期间被 havoc，因为 Prover 无法看到被调用合约的实现。由于外部合约可能回调调用方并修改存储，Prover 无法排除 ghost 变量可能通过其 hook 被更新的情况。为了处理这种不确定性，Prover 会为 ghost 变量分配非确定性的值。

当调用 revert 时，ghost 不会变成非确定性的。相反，它们会回滚（重置）到调用开始前它们所保持的值。根据 Certora docs 的说法，“Ghost 可以被视为正在验证的合约状态的扩展。这意味着在调用 revert 的情况下，ghost 的值将 revert 到它们的前置状态（pre-state）。”

这些是 ghost 的默认行为：它们在未解析的调用中被 havoc，在方法调用 revert 时被重置。然而，有一种特殊用途的 ghost 称为 persistent ghost，它在未解析的外部调用和 revert 中都能保持其值（不会被 havoc）。

在本章中，我们将演示 persistent ghost 是如何工作的，它们与常规 ghost 的区别，以及何时应该使用它们，何时不该使用。

声明 persistent ghost

使用 persistent 关键字声明 persistent ghost，如下所示：

Copy
persistent ghost bool g_flag;
persistent ghost uint256 g_count;

为了提高可读性，我们在本文中对所有 ghost 变量使用前缀 g_，尽管它们可以自由命名。

要使用特定值初始化 persistent ghost，请在 ghost 声明中添加 init_state axiom：

Copy
persistent ghost bool g_flag {
    init_state axiom g_flag == false;
}

persistent ghost uint256 g_count {
    init_state axiom g_count == 0;
}

_注意：_虽然 persistent ghost 在未解析的方法调用期间不会被 havoc，但它们在 rule 的调用前状态（pre-call state）和 invariant 的基础情况（base case）中会被 havoc；常规 ghost 也是如此。因此，仍然必须将它们作为 rule 中的前置条件（通过 require 语句）进行适当的约束，并使用 init_state axiom 为 invariant 的基础情况进行初始化。

persistent ghost 与常规 ghost 的行为对比

下图展示了 persistent ghost 如何在发生 revert 的调用和未解析的外部调用中保持其值。在 rule 执行期间，当 hook 为 ghostVar 赋值时，该值永远不会被 revert（重置）或被 havoc，因此其最终状态始终反映 hook 最后分配的值：

与 persistent ghost 相反，常规 ghost 在未解析的外部调用时会被 havoc，在 revert 时会被重置：

注意：persistent ghost 和常规 ghost 都只在单次 rule 执行内保持它们的值，并且不会在 rule 之间结转（carry over）。不同之处在于，persistent ghost 能在该执行内的未解析调用或发生 revert 的调用中留存，而常规 ghost 则不能。

使用 persistent ghost 追踪 revert

本节将演示 persistent ghost 如何以常规 ghost 无法做到的方式实现对 revert 的追踪。它解释了为什么常规 ghost 在这种用例中会失败，并展示了 persistent ghost 是如何解决该问题的。

常规 ghost 在方法调用 revert 时重置

当方法 revert 时，常规 ghost 的状态也会回滚。这种行为与存储变量在失败调用期间回滚到先前值的机制是一致的。

为了说明这种行为，考虑下面这个名为 SimpleVault 的合约，用户可以在其中存入和提取 ETH：

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

contract SimpleVault {
    mapping(address => uint256) public balanceOf;

    /// deposit ETH into the vault
    function deposit() external payable {
        balanceOf[msg.sender] += msg.value;
    }

    /// withdraw ETH from the vault
    function withdraw(uint256 amount) external {
        require(balanceOf[msg.sender] >= amount, "Insufficient balance");
        balanceOf[msg.sender] -= amount;

        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "ETH transfer failed");
    }
}

目标是验证 withdraw() 当且仅当在以下情况下发生 revert：

• 提取金额超过已存余额（amount > balanceBefore）
• 向这个 non-payable 函数发送了非零的 msg.value（e.msg.value != 0）
• ETH 转账失败，或者底层调用返回 false

本节专门关注第三种情况：追踪 ETH 转账失败。

以下 rule 实现了“Account Balances”（账户余额）一章中的一种断言模式。它使用了双条件运算符（<=>）并以析取（即 ||）的方式列出所有预期的 revert 条件。当且仅当发生这些条件之一时，这就涵盖了所有可能的方法 revert 情况：

Copy
ghost bool g_lowLevelCallSuccess; // regular ghost

rule withdraw_revert(env e) {
    uint256 amount;
   
 	require g_lowLevelCallSuccess; // by requiring it to be true initially, you can detect when it becomes false during execution

    mathint balanceBefore = balanceOf(e.msg.sender);

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

为了追踪 ETH 转账结果，我们使用了一个 CALL hook；这是一个 CVL 特性，可监控底层的 EVM CALL 指令并捕获其返回码。我们将该返回码赋值给 g_lowLevelCallSuccess（0 表示失败，1 表示成功）：

Copy
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

以下是完整的规范：

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

ghost bool g_lowLevelCallSuccess;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

rule withdraw_revert(env e) {
    uint256 amount;
    require g_lowLevelCallSuccess;

    mathint balanceBefore = balanceOf(e.msg.sender);

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

使用常规 ghost 时，验证将失败：

查看失败的 Prover 运行结果：link

让我们检查一下失败发生的原因。

常规 ghost 值重置 — 调用追踪（call trace）

验证失败是因为 g_lowLevelCallSuccess 是一个在 revert 时重置的常规 ghost。CALL hook 捕获了失败（returnCode == 0），但是当 withdraw revert 时，ghost 被重置并丢失了该值。

如下图所示，在调用 withdraw() 方法之前（调用前状态），g_lowLevelCallSuccess 为 true：

当底层 ETH 转账调用失败时，CALL hook 捕获到失败的调用（返回值为 0），这将 g_lowLevelCallSuccess 设置为 false：

当 CALL 操作码（由 CVL CALL hook 捕获）返回零时，这意味着 ETH 转账失败。在 rule 内部，当 withdraw@withrevert(e, amount) 调用 revert 时，ghost 会重置为其 pre-call state。下图显示 ghost 尽管在转账失败的情况下依然恢复为了 true：

使用 persistent ghost 修复规范

简要回顾我们使用常规 ghost 在调用追踪中观察到的情况，执行过程如下展开：

1. ghost g_lowLevelCallSuccess 被初始化为 true（通过 require 语句）。
2. withdraw 函数执行并触发了一个失败的底层 CALL。
3. CALL hook 检测到失败（returnCode == 0）并将 g_lowLevelCallSuccess 设置为 false。
4. 由于当 success 为 false 时 require(success) 失败，withdraw 函数发生 revert。
5. revert 导致 ghost 重置回其 pre-call state，即 true。

根本问题很明显：第 5 步中的 revert 将 ghost 重置回 true，抹除了在第 3 步中记录转账失败的 false 值。

要修复这个问题，将 ghost 声明为 persistent，以便 CALL hook 分配的布尔值能够在 revert 后留存，并在 rule 中保持可访问：

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

persistent ghost bool g_lowLevelCallSuccess;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

rule withdraw_revert(env e) {
    uint256 amount;
    require g_lowLevelCallSuccess;

    mathint balanceBefore = balanceOf(e.msg.sender);

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

正如预期的那样，rule 验证通过：

Prover 运行结果：link

借助 persistent ghost，我们成功追踪了跨越 revert 的底层调用 ETH 转账失败，这对于常规 ghost 来说是不可能的。这个例子展示了 persistent ghost 的一个适当用例：捕获在 revert 期间会丢失的状态信息。

何时不要使用 persistent ghost

在看到了 persistent ghost 的恰当用例之后，理解何时不应使用它们同样重要。

在常规 ghost 上添加 persistent 关键字很容易，这也让它容易被滥用。当你需要观察在 revert 或未解析的执行中发生了什么时，应该有意识地使用 persistent ghost ——而不是当 rule 或 invariant 验证失败时把它当作变通的方法（workaround）。

为了演示滥用的问题，让我们考虑一个类似的金库，不过它接受的是 ERC-20 代币而不是 ETH。它的余额映射是私有的，由于没有 getter 函数可供读取，所以需要一个 ghost 变量来镜像内部的余额：

Copy
/// minimal ERC20 interface
interface IERC20 {
    function transfer(address to, uint256 amount) external returns (bool);
	...
}

contract SimpleVault20 {
    IERC20 public immutable token;
    mapping(address => uint256) private balanceOf;
    
    constructor(address _token) {
        token = IERC20(_token);
    }
    
    function deposit(uint256 amount) external {
        require(amount > 0, "Zero deposit");
        
        balanceOf[msg.sender] += amount;
        require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
    }
    
    ...
}

让我们为 deposit``() 函数编写规范。对于 ghost 和 hook：

• 将 ghost 声明为常规 ghost
• 实现 Sstore hook 来追踪每个账户存款人的余额变化
• 实现 Sload hook 以同步存储的读取和 ghost

Copy
ghost mapping(address => mathint) g_balanceOf;

hook Sstore balanceOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_balanceOf[account] = g_balanceOf[account] + newVal - oldVal;
}

hook Sload uint256 balance balanceOf[KEY address account] {
    require g_balanceOf[account] == balance;
}

至于 rule，我们验证存入一笔金额（depositAmount）是否正确地将其记入了发送者在金库中的余额：

Copy
rule deposit(env e) {
    uint256 depositAmount;

    require currentContract != e.msg.sender;
    require g_balanceOf[e.msg.sender] == 0;
    
    deposit(e, depositAmount);
    assert g_balanceOf[e.msg.sender] == depositAmount;
}

让我们运行验证。由于 deposit 函数调用了一个未知的 ERC-20 实现（这将引发 havoc），我们预期它会失败：

Prover 运行结果：link

为什么验证失败

根本原因在于 SimpleVault20 合约的以下代码行，它调用了一个未知的 ERC-20 实现：

Copy
contract SimpleVault20 {
    ...
    function deposit(uint256 amount) external {
        require(amount > 0, "Zero deposit");
        
        balanceOf[msg.sender] += amount;
        
        // `token` is an unknown ERC-20 implementation
        require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
    }
    ...
}

在下图中，我们看到 Prover 将值 0xa（即 10）分配给了 depositAmount，然后通过 Sstore hook 传递给了 ghost 映射变量 g_balanceOf[address]：

随后，该 ghost 在调用外部合约期间被 havoc，因为其实现是未知的：

看到 havoc 错误后，可能会有人倾向于添加 persistent 关键字来抑制它。虽然这能使验证通过，但它掩盖了真正的问题：我们不知道外部的 ERC-20 合约是如何实现的：

Prover 运行结果：link

Prover 基于错误假设进行的验证

Prover 显示该 rule 已通过验证，但这基于一个错误的假设。通过使用 persistent ghost，该规范假设 ERC-20 实现永远不会 revert 或修改调用方合约的存储。因此，即使转账实际上可能失败，它仍然将金额 0x``a（即 10）记入了 msg.sender：

这演示了为什么在这种情况下使用 persistent ghost 具有误导性：它绕过了外部合约行为的不确定性，从而掩盖了潜在的 bug，而不是揭示它们。

实际的代币实现应该被 link 到金库中

正确的解决方案并不是使用 persistent ghost。相反，我们必须将一个已知的 ERC-20 实现“链接”（link）到 scene 中——无论是协议自身的 ERC20、WETH、DAI，还是任何代码公开可用的 ERC-20 代币。

Link 指示 Prover 在遇到外部调用时，使用 verification scene 中包含的实际合约实现，而不是将这些调用视作 havoc 行为。

对于 SimpleVault20，代币地址是 immutable 的，这意味着要在部署时使用哪个已知的 ERC-20 是确定的，并且在合约的整个生命周期中不会改变。因此，我们可以通过将该 ERC-20 合约添加到 scene 并在规范中对其进行配置，使用 link 将其“绑定”到某个 ERC-20 实现。这允许 Prover 针对实际的代币实现来验证 SimpleVault20 合约。否则，如果没有 link，Prover 无法准确验证金库与代币之间的交互，从而导致上面展示的误报（false positives）。

有关 link 的更多详细信息，请参阅 Certora 文档：[1, 2]

总结

• persistent ghost 能在 havoc 和 revert 中留存，而常规 ghost 在向未知合约发起外部调用期间会被 havoc，并在 revert 时被重置。
• 对未知合约的外部调用会引发 havoc，因为 Prover 无法看到被调用方的实现，所以它会模拟所有可能的返回值和存储影响。
• persistent ghost 的正确用法是用来捕获来自 CVL hook 的信息——比如 CALL 返回码——这些信息必须在失败的执行路径中保留下来，例如追踪失败的底层 ETH 转账。
• 将 persistent 关键字作为快速修复失败 rule 的方法，会忽略未知合约实现或未解析调用的影响，从而造成一种验证成功的假象。

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