使用 Ghost 和 Hook 验证不变量

Last updated on Feb 13, 2026

在任何正确的 ERC20 实现中，所有账户余额的总和必须始终等于代币的总供应量。 在任何状态更改过程中，这一属性都应始终保持为真。如果某个调用（无论是直接调用还是序列调用的一部分）违反了这一不变量，则标志着合约的逻辑和设计中存在根本性缺陷。

在本章中，我们将利用前几章中所学的有关 ghost 变量和 hook 的知识，来形式化验证这个关键的不变量。

添加用于验证的智能合约

在本教程中，我们将使用由 Transmission11 开发的 Solmate 库 中的 ERC20 合约。为了将此合约包含到你的项目中，请在你的 Certora 项目目录的 contracts 子目录内创建一个名为 ERC20.sol 的新文件。然后，复制 Solmate 的 ERC20 实现 的代码并将其粘贴到该文件中。

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity 0.8.25;

/// @notice Modern and gas efficient ERC20 + EIP-2612 implementation.
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author Modified from Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev Do not manually set balances without updating totalSupply, as the sum of all user balances must not exceed it.
contract ERC20 {
    /*//////////////////////////////////////////////////////////////
                                 EVENTS
    //////////////////////////////////////////////////////////////*/

    event Transfer(address indexed from, address indexed to, uint256 amount);

    event Approval(address indexed owner, address indexed spender, uint256 amount);

    /*//////////////////////////////////////////////////////////////
                            METADATA STORAGE
    //////////////////////////////////////////////////////////////*/

    string public name;

    string public symbol;

    uint8 public immutable decimals;

    /*//////////////////////////////////////////////////////////////
                              ERC20 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 public totalSupply;

    mapping(address => uint256) public balanceOf;

    mapping(address => mapping(address => uint256)) public allowance;

    /*//////////////////////////////////////////////////////////////
                            EIP-2612 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 internal immutable INITIAL_CHAIN_ID;

    bytes32 internal immutable INITIAL_DOMAIN_SEPARATOR;

    mapping(address => uint256) public nonces;

    /*//////////////////////////////////////////////////////////////
                               CONSTRUCTOR
    //////////////////////////////////////////////////////////////*/

    constructor(
        string memory _name,
        string memory _symbol,
        uint8 _decimals
    ) {
        name = _name;
        symbol = _symbol;
        decimals = _decimals;

        INITIAL_CHAIN_ID = block.chainid;
        INITIAL_DOMAIN_SEPARATOR = computeDomainSeparator();
    }

    /*//////////////////////////////////////////////////////////////
                               ERC20 LOGIC
    //////////////////////////////////////////////////////////////*/

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        allowance[msg.sender][spender] = amount;

        emit Approval(msg.sender, spender, amount);

        return true;
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        balanceOf[msg.sender] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(msg.sender, to, amount);

        return true;
    }

    function transferFrom(
        address from,
        address to,
        uint256 amount
    ) public virtual returns (bool) {
        uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

        if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

        balanceOf[from] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(from, to, amount);

        return true;
    }

    /*//////////////////////////////////////////////////////////////
                             EIP-2612 LOGIC
    //////////////////////////////////////////////////////////////*/

    function permit(
        address owner,
        address spender,
        uint256 value,
        uint256 deadline,
        uint8 v,
        bytes32 r,
        bytes32 s
    ) public virtual {
        require(deadline >= block.timestamp, "PERMIT_DEADLINE_EXPIRED");

        // Unchecked because the only math done is incrementing
        // the owner's nonce which cannot realistically overflow.
        unchecked {
            address recoveredAddress = ecrecover(
                keccak256(
                    abi.encodePacked(
                        "\x19\x01",
                        DOMAIN_SEPARATOR(),
                        keccak256(
                            abi.encode(
                                keccak256(
                                    "Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"
                                ),
                                owner,
                                spender,
                                value,
                                nonces[owner]++,
                                deadline
                            )
                        )
                    )
                ),
                v,
                r,
                s
            );

            require(recoveredAddress != address(0) && recoveredAddress == owner, "INVALID_SIGNER");

            allowance[recoveredAddress][spender] = value;
        }

        emit Approval(owner, spender, value);
    }

    function DOMAIN_SEPARATOR() public view virtual returns (bytes32) {
        return block.chainid == INITIAL_CHAIN_ID ? INITIAL_DOMAIN_SEPARATOR : computeDomainSeparator();
    }

    function computeDomainSeparator() internal view virtual returns (bytes32) {
        return
            keccak256(
                abi.encode(
                    keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"),
                    keccak256(bytes(name)),
                    keccak256("1"),
                    block.chainid,
                    address(this)
                )
            );
    }

    /*//////////////////////////////////////////////////////////////
                        INTERNAL MINT/BURN LOGIC
    //////////////////////////////////////////////////////////////*/

    function _mint(address to, uint256 amount) internal virtual {
        totalSupply += amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(address(0), to, amount);
    }

    function _burn(address from, uint256 amount) internal virtual {
        balanceOf[from] -= amount;

        // Cannot underflow because a user's balance
        // will never be larger than the total supply.
        unchecked {
            totalSupply -= amount;
        }

        emit Transfer(from, address(0), amount);
    }
}

理解挑战

要将我们的不变量表达为 CVL 表达式，我们需要两个值：

代币总供应量
所有账户余额的总和

我们的合约中有一个名为 totalSupply 的公共状态变量，它记录了任意状态下的代币总供应量，并且可以使用名为 totalSupply() 的 getter 函数读取其值。然而，核心挑战在于，合约并没有提供任何内置的方法来获取所有余额的总和。

“解决方案”

为了获取所有账户余额的总和，我们将创建一个名为 sumOfBalances 的 ghost 变量，并使用 init_state 公理将其初始值设置为 0。每次对 balanceOf 映射进行写操作时，ghost 变量 sumOfBalances 都会通过一个 store hook 进行更新。

我们知道，store hook 可以让我们访问正在更新的余额的旧值和新值。我们利用这些值来计算变动，并相应地更新我们的 ghost 变量：

sumOfBalances = sumOfBalances - oldValue + newValue;

例如，如果某个用户的余额从 100 增加到 150，我们的 hook 会从 sumOfBalances 中减去 100 并加上 150，从而正确地将总和增加 50。通过对每次余额更新应用这种增量（delta）计算，我们的 ghost 变量 sumOfBalances 将追踪合约状态的变化，从而映射出所有余额的总和。

一旦 Prover 能够获取这两个值（来自合约的实际 totalSupply 和我们精确维护的 sumOfBalances ghost 变量），我们就可以使用 CVL 中的 invariant 块来正式声明不变量，断言总供应量始终等于所有账户余额的总和。

逐步编写完整的规范

现在让我们把讨论过的所有内容付诸实践，按照以下步骤编写一个完整的规范，以验证所有余额的总和是否与代币总供应量相匹配：

在你的 Certora 项目目录内，导航到 specs 子目录并创建一个名为 erc20.spec 的新文件。
在 erc20.spec 中，定义一个名为 sumOfBalances 的 ghost 变量。

ghost mathint sumOfBalances;

接下来，我们使用 init_state 公理，在 invariant 的 base case 中将 sumOfBalances 的初始值设置为 0。

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

该公理仅在 invariant 的 base case 中约束 ghost 变量，建立一致的构造函数后（post-constructor）状态。如果没有这个基准线，Prover 可能会为 ghost 变量假设任意初始值，从而使得不变量保持（invariant preservation）变得毫无意义。

定义一个 store hook，以追踪 balanceOf 映射的变化并相应地更新我们的 ghost 变量 sumOfBalances。

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

现在我们已经拥有了这两个值——合约的 totalSupply() 和我们的 ghost 变量 sumOfBalances——我们可以如下所示定义核心不变量：

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

最后，添加一个 methods 块，其中将包含 totalSupply() 的函数签名。

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

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}


invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

导航到 confs 子目录，创建一个名为 erc20.conf 的新文件。

{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "msg": "Testing erc20 functionality"
}

运行验证

执行完上述所有步骤后，通过在终端中运行命令 certoraRun confs/erc20.conf 来提交代码进行验证。

在你选择的任何 Web 浏览器中打开由 Prover 提供的 verification result 以查看类似下图的结果：

在我们的验证结果中，可以看到不变量检查在两个地方都失败了：构造函数调用之后和方法执行期间。

当我们点击 “induction base: After the constructor” 违规项时，Prover 会建议在你的配置中添加 optimistic_loop 键并将其值设置为 true，或者将 loop_iter 的值增加到大于 1。

现在，让我们采纳 Prover 的建议，通过将 optimistic_loop 键设为 true 来更新配置文件。我们将在后面名为 “How Strings Lead to Loops?” 的章节中更深入地探讨这个问题。

{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}

完成后，通过在终端中运行命令 certoraRun confs/erc20.conf 重新运行 Prover。在新的验证结果中，我们可以看到我们的不变量在构造函数执行期间成功通过，但在方法执行期间失败了，特别是对于 transfer() 和 transferFrom() 函数。

要了解违规的原因，请点击 transfer() 或 transferFrom() 函数的 call trace。在我们的例子中，我们将分析 transfer() 函数的 call trace。

要查看完整的 call trace，请点击 Call Trace 面板右上角的 “Expand” 按钮。

在 call trace 中，我们可以看到单个账户 0x7 和 0x8200 的初始余额分别被设置为 2^256 − 4 和 0xf000000000000000000000000000000000000000000000000000000000000000。以十进制形式表示，它们分别对应 115792089237316195423570985008687907853269984665640564039457584007913129639932 和 108890810646419256008710686707116392212123736112785533035372916772359555072000。

这两个值都是 Prover 通过 havocing 分配的，并且落在 0 到 2^{256} - 1 的数值范围内。然而，在任何正确实现的 ERC20 合约中，单个账户余额永远不应超过所有余额的总和。在这种情况下，这两个账户的初始余额都远远大于总供应量（0xa）和 sumOfBalances，这创造了一种在实际部署中根本不可能存在的初始状态。
Prover 之所以这样做，是因为它本身并不理解 ERC20 代币的业务逻辑；它仅仅将存储视为原始数据。除非有明确的约束，否则它会假设任何 uint256 值都是有效的起点。

为了避免这种情况，我们特别需要告诉 Prover，初始的单个账户余额不应大于 sumOfBalances。为此，我们将使用 CVL 提供的 require 语句来约束 Prover 应该考虑的值。

使用 `require` 语句约束初始余额

在我们的 erc20.spec 文件中，将下面显示的代码添加到我们的 store hook 中，以限制可以分配给任何账户余额的值的范围。完成后，重新运行 Prover 以查看验证结果：

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    require oldAmount <= sumOfBalances;  //add this line
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

在 new result 中，你会注意到 Prover 不再发现任何违规项。

我们的不变量 totalSupplyEqSumOfBalances 通过了验证，因为在 store hook 中添加了 require oldAmount <= sumOfBalances; 这一行之后，Prover 将只探索该条件为真的执行路径。这有效地排除了依赖单一余额高于总和的反例**（例如，transfer 中发送方或接收方的余额），从而确保 Prover 专注于单个余额保持在总供应量逻辑界限内**的场景。结果就是验证成功了，证实了不变量在所有允许的状态转换下都得以保持。

另一种方法：Load Hook

虽然向 Sstore hook 添加约束是有效的，但还有另一种方法，我们可以在 Load Hook 中对单个余额添加约束。

要实现此方法，请按照以下步骤操作：

在 balanceOf 映射上定义一个 load hook，以拦截每次对 balanceOf 的读取。

hook Sload uint256 balance balanceOf[KEY address addr] {}

在这个 hook 中使用 require sumOfBalances >= to_mathint(balance); 引入一个约束。

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

从 Sstore hook 中移除约束，以便我们完全依赖 load hook 逻辑。

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    require oldAmount <= sumOfBalances;  //remove this line
    sumOfBalances = sumOfBalances - oldAmount + newAmount;   
}

以上述建议的更改之后，更新后的规范如下所示：

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

ghost mathint sumOfBalances {
    // Constraining pre-constructor ghost value through axiom
    init_state axiom sumOfBalances == 0;

}

// Added a load hook on balanceOf mapping
hook Sload uint256 balance balanceOf[KEY address addr] {
    // Introduce a constraint
    require sumOfBalances >= to_mathint(balance);

}

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount)  {
    // Delta Update
    sumOfBalances = sumOfBalances - oldAmount + newAmount;

}


invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

如果使用此更改重新运行验证（从 Sstore hook 中移除 require 并仅将其保留在 Sload hook 中），不变量 totalSupplyEqSumOfBalances 仍将通过。

这之所以有效，是因为 load hook 显式地过滤掉了任何单个账户余额大于所有余额总和的状态。如果 Prover 试图使用这样一个不可能的初始状态来构建反例，它最终会在评估合约逻辑时读取该余额。在该读取发生的瞬间，load hook 内部的 require 语句会检查该余额是否与我们的 ghost 变量一致。由于该余额是不切实际的极大值，该条件检查会失败，于是 Prover 被迫丢弃这整条执行路径。

Sstore vs. Sload：在哪里放置约束？

这两个版本都“有效”，因为它们都排除了会违反我们不变量的不可能状态，但 load hook 方法提供了更可靠、更全面的保护。让我们来拆解一下原因：

Store Hook 实际上保证了什么

当我们将约束放在 store hook 中时：

hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
    require oldAmount <= sumOfBalances;
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

在上面的代码中，我们实际上是在告诉 Prover：“每当你在 balanceOf[account] 写入数据时，请确保之前的值（oldAmount）不大于 sumOfBalances”

这就产生了一个盲区：

如果 Prover 从未写入某个特定的 balanceOf[addr] slot，那么针对该地址的 hook 就永远不会被触发。
这意味着 Prover 仍然可以自由地从一个奇怪的初始值开始（通过 havoc），比如 balanceOf[addr] = 2^{256} - 1，即使 sumOfBalances = 10。
只要合约不尝试向该 slot 写入，Sstore 中的 require 就永远不会被检查，而这种不可能的状态在读取和逻辑推理期间就能一直存在。

简而言之，store hook 仅仅是在说：“如果你通过写入数据触及了这个 slot，那么之前的值必须是合理的。” 它并没有说：“无论你什么时候查看它们，所有余额都总是合理的。”

Load Hook 能够保证什么

现在，来看看 load hook 的版本：

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

它会在 Prover 每次从 balanceOf 读取余额时运行。在这里，我们告诉 Prover：“每当你读取余额时，该余额必须小于或等于 sumOfBalances”

这带来了两个重要效果：

Prover 无法在任何计算中使用不可能的余额。 如果它试图假设 balanceOf[addr] 大于 sumOfBalances 然后去读取它，load hook 中的 require 就会失败，并且该执行路径会立即被丢弃。
即使从未向该 slot 写入过，这一点也同样适用。 Prover 在开始时可能会将 balanceOf[addr] havoc 成某个任意值，但在它读取该值的瞬间，load hook 就会对其进行检查。如果该值是不可能的，整条路径就会被抛弃。

load hook 就像是一个全局完整性检查（sanity check）：“你看到的任何余额，都必须与 ghost 变量 sumOfBalances 保持逻辑上的一致。”

这就是为什么当我们关心保持 sumOfBalances 与实际余额一致并避免不可能的 ERC20 状态时，load hook 方法通常是更好的选择。

结论

在本章中，我们验证了基本的 ERC20 不变量：总供应量 = 所有余额的总和。

我们通过使用 ghost 变量来追踪总和，并使用 hook 将该 ghost 变量与合约的存储进行同步，从而实现了这一目标。至关重要的是，我们演示了为什么将约束放在 Sload hook 中通常比放在 Sstore hook 中更安全。通过在数值被_读取_时进行监督，我们有效地消除了盲区，否则 Prover 在该盲区中可能会假设存在不可能的初始状态。

这些技术允许你在底层存储之上证明高级业务规则，从而确保你的验证仅专注于有效、符合现实的合约行为。

本文是 formal verification using the Certora Prover 系列文章的一部分。