ERC-721 的不变式

本文详细阐述了如何使用Certora Prover对ERC-721代币合约进行形式化验证，重点介绍了5个关键不变式（invariants）的实现与验证。

使用 Certora 进行形式化验证

ERC-721 的不变量

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

上次更新于 2026 年 2 月 13 日

介绍

在前面的章节中，我们探讨了 CVL 不变量的工作原理：它们是必须在所有合约执行过程中保持的属性。不变量可以作为规则中的前置条件，以及其他不变量中的 preserved 条件，这使得验证可以在已证明的保证基础上进行，并消除了错误假设的风险。不变量还会自动在所有改变状态的函数中进行检查。

本章继续作为 OpenZeppelin 的 ERC-721 CVL 规范 代码演练的 $(2/5)$ 部分，重点关注不变量属性。它验证以下五个 ERC-721 不变量：

  • balanceOfConsistency

用户的余额和所有权计数始终相等。

  • ownerHasBalance

代币所有者始终拥有正余额。

  • ownedTotalIsSumOfBalances

拥有的代币总数等于所有用户余额之和。

  • notMintedUnset

未铸造的代币没有设置批准地址。

  • zeroAddressHasNoApprovedOperator

未铸造的代币没有设置批准操作者。

这些不变量保证了余额准确反映所有权，并且批准与所有权状态保持一致。

balanceOfConsistency 不变量

在 ERC-721 中，有三种方法可以确定账户的代币余额：

  • 通过调用公开的 $balanceOf(address)$ 函数
  • 通过读取 $_balances$ 映射
  • 通过读取存储 $_owners$ 映射并计算该地址拥有的代币数量

这三个数量必须相等，因为它们各自代表相同的基础事实：用户拥有多少代币。任何差异都将表明余额和所有权跟踪之间存在不一致的核算。

在不变量 balanceOfConsistency 中，这些数量分别对应 $balanceOf(user)$、$_balances[user]$ 和 $_ownedByUser[user]$，每个都代表用户的代币余额：

invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user]
    ...

每个余额表示是如何推导的

为了验证这个不变量，规范捕获了这些表示的每一个。下面解释了每个表示是如何推导的。

$balanceOf(user)$ — 用户余额的公开视图函数

$balanceOf(user)$ 是一个公开的视图函数，我们可以在 CVL 中直接调用它来检索用户的余额。此函数返回存储在存储映射变量 $_balances$ 中的值。

$_balances[user]$ — 从存储中镜像的代币余额

$_balances[user]$ 是一个 ghost 变量，它通过一个 $Sload$ Hook读取并镜像私有存储映射变量 $_balances$。

它使用一个 $init_state$ 公理并带有一个 forall 量词为所有地址初始化为零，这表明每个地址在初始状态下都以零余额开始，与合约的默认存储状态相匹配：

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}
...

如果没有此初始化，Prover 会假设余额的任意起始值（基本情况），这可能导致初始状态下的核算不正确。这会使跟踪逻辑失效，并在验证过程中导致误报。

初始化后，规范必须使用 $Sload$ Hook反映 ghost 状态中的存储读取。$Sload$ Hook从实际的 $_balances$ 存储槽读取值，并将这些值与 ghost 变量同步（ghost 变量和存储变量共享相同的名称但不会冲突）：

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

当通过 require 约束 $Sload$ Hook返回的存储值等于 ghost 变量时，就会发生同步。这种同步是必要的，因为 ghost 变量不会在存储读取时自动更新。

$_ownedByUser[user]$ — 代币所有权计数 从存储中推导

$_ownedByUser[user]$ 是一个 ghost 变量，它表示所有 $tokenId$s 中 $ownerOf(tokenId) == user$ 的计数：

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}
...

换句话说，如果我们列出所有代币并计算有多少代币由 user 拥有，我们就得到了 $_ownedByUser[user]$。我们不希望出现 $balanceOf(user)$ 报告 $2$ 个，但实际所有权计数为 $3$ 个的情况（例如，如果 $ownerOf(token1) == user$，$ownerOf(token2) == user$，并且 $ownerOf(token3) == user$）。

ghost 变量 $_ownedByUser[user]$ 通过 $Sstore$ Hook存储用户拥有的代币数量。当合约向合约的私有存储映射 $_owners[tokenId]$ 写入新值时，该Hook就会运行，它会观察 $oldOwner$ 和 $newOwner$ 以确定所有权是如何变化的。

通过比较这两个值，我们可以将更新分类为铸造（Mint）、销毁（Burn）或转移（Transfer）：

  • Mint：$oldOwner == address(0)$ 且 $newOwner != address(0)$
  • Burn：$oldOwner != address(0)$ 且 $newOwner == address(0)$
  • Transfer：$oldOwner$ 和 $newOwner$ 都是非零地址

该Hook更新 ghost 映射 $_ownedByUser$ 以反映这些所有权更改：

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
    // _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}

注意：我们故意注释掉了行 $_ownedTotal = ...$ 因为它目前不必要。我们没有跟踪拥有的代币总数；我们只跟踪每个用户拥有的代币。

$Sstore$ Hook $_owners$ 中的第一行处理代币增量，这意味着发生了铸造和转移：

_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
  • 如果 $newOwner != 0$，则 $1$ 被添加到 $newOwner$ 代币计数中。这适用于：
    • Mint：当代币被创建并分配给用户时（$address(0)$ 到 $newOwner$）
    • Transfer：当代币从一个用户转移到另一个用户时（$oldOwner$ 到 $newOwner$）
  • 如果 $newOwner == 0$，这表示销毁，因此没有 $newOwner$ 接收代币。三元表达式求值为 $0$，因此没有发生加法。然而，这种代币损失（销毁）仍需要核算，这由第二行处理。

$Sstore$ Hook $_owners$ 中的第二行处理代币减量，这意味着发生了销毁和转移：

_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
  • 如果 $oldOwner != 0$，则前一个（非零）所有者持有代币，现在失去了它，因此我们减去 $1$。这适用于转移和销毁操作。
  • 如果 $oldOwner == 0$，这表示铸造，代币是新创建的，没有前一个所有者。三元表达式求值为 $0$，因此没有发生减法。所有权计数由第一行（处理代币增量的那一行）核算。

现在我们已经讨论了不变量表达式以及用户代币余额的三种表示是如何推导的，还剩下最后一部分来完成规范：处理来自安全铸造和安全转移操作的外部回调。

不变量在验证期间会自动调用所有状态改变函数，这意味着 Prover 会调用 $safeMint()$ 和 $safeTransferFrom()$——这两个函数都会触发对接收合约的 $onERC721Received()$ 的外部回调。我们需要配置 Prover 如何处理这个外部调用。否则，这些外部调用将被 Prover 视为未解析，这会对 ghost 变量和存储造成严重破坏，并导致不变量属性的误报。

DISPATCHER — 解析 $onERC721Received$ 回调

为了解析此回调，规范将 $onERC721Received()$ 调用分派给一个模拟接收器合约，该合约返回 $bytes4$ 选择器 0x150b7a02 以表示 ERC-721 支持。要实现分派，我们需要：

  • 创建一个简单的 ERC721 接收器合约（mock），
  • 将其包含在验证 场景 中，
  • 在 $methods$ 块中添加分派指令。

ERC721 模拟接收器合约：

这是一个接收器合约，它作为 harness 实现，返回 $bytes4$ 选择器 0x150b7a02：

// SPDX-License-Identifier: MIT

pragma solidity ^0.8.20;

import "contracts/interfaces/IERC721Receiver.sol";

contract ERC721ReceiverHarness is IERC721Receiver {
    function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
        return this.onERC721Received.selector;
    }
}

注意：导入 $IERC721Receiver$ 用作接口检查，确认合约符合预期的 ERC721 接收器规范。

将模拟接收器合约添加到场景中：

接下来，我们通过将其添加到 .conf 配置文件中来将 ERC721ReceiverHarness.sol 包含在场景中：

// .conf

{
  "files": [
    "certora/harness/ERC721Harness.sol",
    "certora/harness/ERC721ReceiverHarness.sol",
  ],
  ...
}

此时，模拟接收器是验证场景的一部分，并且可用作分派目标。

添加 DISPATCH 指令：

然后，在 CVL 规范的 $methods$ 块中，我们添加分派指令：

// .spec

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

分派行：function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true) 指示 Prover 将 $onERC721Received()$ 调用路由到验证场景中所有实现 $onERC721Received()$ 的合约（$_$ 是通配符），并针对 $balanceOfConsistency$ 不变量测试其实现。由于我们只有一个合约实现了 $onERC721Received()$，即模拟接收器，因此 Prover 将只测试该合约。

使用 $DISPATCHER(true)$，只有场景中的合约被选中进行分派，Prover 会尝试每种匹配的实现，以确定是否有任何实现可能导致违规。

此处使用的模拟接收器合约特意设计为最小化。它只实现了 $onERC721Received()$ 函数并返回所需的选择器 0x150b7a02。它不包含任何改变调用合约状态或影响其存储的逻辑。因此，回调不会引入任何不变量违规。

即使模拟接收器导致 $safeMint()$ 或 $safeTransferFrom()$（包括它们的 $bytes$ 变体）revert——例如，通过返回不正确的回归值——不变量仍然不受影响，因为 revert 不会导致任何状态改变。然而，这与我们在后面的章节中形式化验证安全铸造和安全转移函数时的情况不同，那时 revert 的回调会导致断言失败。

在这个 CVL 不变量规范中，$DISPATCHER$ 的作用仅仅是解析外部调用。没有它，$safeMint()$ 和 $safeTransferFrom()$——包括它们的变体——将调用未解析的外部调用，这会造成严重破坏并导致误报的不变量失败。

balanceOfConsistency 不变量的完整规范和 Prover 运行

以下是 balanceOfConsistency 不变量的完整 CVL 规范，其中包括 $methods$ 块、ghost 变量声明和Hook实现：

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
    // _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];
    // {
    //     preserved {
    //         require balanceLimited(user);
    //     }
    // }

注意：preserved 块被故意注释掉，因为不变量在没有它的情况下也能成功验证，这意味着它不是严格必要的。

这是经过验证的 Prover 运行。

ownerHasBalance 不变量 — 代币所有者拥有正余额

这个不变量表明，如果一个 $tokenId$ 存在（所有者非零），那么该所有者的余额必须大于 $0$：

invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    ...

这个不变量在后续章节中验证转移时用作前置条件，其中发送方应该有正余额。我们可以将 $unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0$ 直接硬编码到规则中，但将其证明为不变量提供了更强的安全保证。

这里需要一个 preserved 块来要求 $balanceOfConsistency(ownerOf(tokenId))$ 在 ownerHasBalance 运行之前成立。这告诉 Prover：“在检查所有者是否有余额之前，首先确认 $balanceOf$ 与 ghost 跟踪的所有权计数匹配。”它防止 Prover 进入不一致的状态，即所有者存在但由于 havoc 而显示零余额。

这是 CVL 不变量：

invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
            // require balanceLimited(ownerOf(tokenId));
        }
    }

ownerHasBalance 不变量的完整规范和 Prover 运行

以下是 ownerHasBalance 不变量的完整 CVL 规范，包括 $methods$ 块、ghost 变量、Hook以及 preserved 的 $balanceOfConsistency$ 不变量：

methods {
    function ownerOf(uint256) external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
    // _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];
    // {
    //     preserved {
    //         require balanceLimited(user);
    //     }
    // }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover v8.3.1
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
            // require balanceLimited(ownerOf(tokenId));
        }
    }

注意：原始不变量表达式是 $balanceOf(ownerOf(tokenId)) > 0$，但已更新为 $unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0$ 以适应 Prover $8.3.1$ 版本。

这是 Prover 运行。

ownedTotalIsSumOfBalances 不变量 — 拥有的代币总数等于所有余额之和

在此不变量规范中，拥有的代币总数和总供应量是推导出来的，因为核心 ERC-721 标准没有公开任何 $totalSupply()$ 的概念——只有 ERC-721 Enumerable 定义了 $totalSupply()$。由于此不变量不能直接针对标准函数进行验证，因此这些值是使用 ghost 变量（$_ownedTotal$ 和 $_supply$）和Hook重建的。

$_ownedTotal$ 通过观察 $_owners$ 存储变量上的 $Sstore$ Hook的所有权变化来计算当前存在的代币数量。$_supply$ 是所有用户余额的总和，也作为 ghost 变量进行跟踪。

通过重建这两个值并将其作为 ghost 变量进行跟踪，不变量验证 $_ownedTotal$ 等于 $_supply$。这确保了余额核算的一致性。如果拥有的代币超过供应量，则余额被低估（代币存在但未反映在余额中）。如果供应量超过拥有的代币，则余额被高估（余额声称的代币数量超过实际存在的数量）。

因此，这种相等性保证了每个拥有的代币在余额总数中只被精确计算一次：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
    _ownedTotal == _supply
{
    // preserved blocks will be shown later
}

$_supply$ 和 $_ownedTotal$ 都是 ghost 映射变量，用于通过 $Sstore$ Hook跟踪代币总供应量，但从不同的角度：

  • $_supply$ 通过在每次存储写入 $_balances$ 时减去旧余额并添加新余额来跟踪总供应量：
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
      _supply = _supply - oldValue + newValue;
}

通过在存储级别观察余额，$_supply$ 被推导出来，并且对 $_supply$ 的影响取决于操作类型：

  • 当代币铸造给用户且余额从 $oldValue = 2$ 变为 $newValue = 3$ 时，$_supply$ 计算为 $_supply = \_supply - 2 + 3$，这导致净增加 $1$。
  • 当代币从所有者处销毁且余额从 $oldValue = 3$ 变为 $newValue = 2$ 时，$_supply$ 计算为 $_supply = \_supply - 3 + 2$，这导致净减少 $1$。
  • 当用户将代币转账给另一个用户时，发送方的余额减少 $1$，而接收方的余额增加 $1$。发送方的减少抵消了接收方的增加，因此 $_supply$ 保持不变。
    • $_ownedTotal$ 通过 $Sstore$ Hook跟踪拥有的代币数量，当所有权被清除时减去 $1$，当代币分配给非零地址时加上 $1$：
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
      ...
      _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}

让我们根据所有权变化来模拟这一点，但首先，为了清晰起见，让我们重新安排代码：

_ownedTotal = _ownedTotal
            + to_mathint(newOwner != 0 ? 1 : 0)
            - to_mathint(oldOwner != 0 ? 1 : 0);

  • 如果 $oldOwner$ 和 $newOwner$ 都是非零地址，则发生转移：

    • $newOwner$ 非零，因此三元表达式求值为 $1$，并添加 $1$。
    • $oldOwner$ 非零，因此三元表达式求值为 $1$，并减去 $1$。

净效应是 $_ownedTotal$ 不变，因为 $1$ 被添加，$1$ 被减去。原则上，转移操作不影响总所有权计数。

  • 如果 $oldOwner$ 为零而 $newOwner$ 非零，则发生铸造：

    • $newOwner$ 非零，因此三元表达式求值为 $1$，并添加 $1$。
    • $oldOwner$ 为零，因此三元表达式求值为 $0$，并减去 $0$。

净效应是 $+1$，因为 $1$ 被添加而没有被减去。原则上，铸造操作会增加总所有权计数。

  • 如果 $oldOwner$ 非零而 $newOwner$ 为零，则发生销毁：

    • $newOwner$ 为零，因此三元表达式求值为 $0$，并添加 $0$。
    • $oldOwner$ 非零，因此三元表达式求值为 $1$，并减去 $1$。

净效应是 $-1$，因为没有被添加而 $1$ 被减去。原则上，销毁操作会减少总所有权计数。

Preserved 子句：

不变量包含 preserved 子句。以下总结了其中的每一个：

  • 对于铸造（Mint）：$mint()$、$safeMint()$、$safeMint(bytes)$

    • $require balanceLimited(to)$

    接收者的余额必须保持在 $max_uint256$ 以下，以防止 Prover 探索不切实际的溢出路径。

  • 对于销毁（Burn）：$burn()$

    • $requireInvariant ownerHasBalance(tokenId)$

    代币在销毁前必须有一个拥有正余额的所有者。

  • 对于转移（Transfer）：$transferFrom()$、$safeTransferFrom()$、$safeTransferFrom(bytes)$

    • $require balanceLimited(to)$

    接收者的余额必须保持在 $max_uint256$ 以下。

    • $requireInvariant ownerHasBalance(tokenId)$

    代币必须来自一个拥有非零余额的有效所有者。

这是包含 preserved 子句的不变量：

invariant ownedTotalIsSumOfBalances()
    _ownedTotal == _supply
    {
        preserved mint(address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
        }
        preserved safeMint(address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
        }
        preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
            require balanceLimited(to);
        }
        preserved burn(uint256 tokenId) with (env e) {
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
        preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
        preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
        preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
    }

注意：不变量 $ownedTotalIsSumOfBalances$ 即使没有 $requireInvariant balanceOfConsistency$ 也能成功验证。为了讨论目的，我们将其注释掉，以便读者可以查看验证不变量严格需要的 preserved 条件。这并不意味着它没有用处——既然它已经得到证明，就可以假定它始终成立。因此，它可以安全地恢复。将其添加为 preserved 条件通常会缩短 Prover 运行时间。

ownedTotalIsSumOfBalances 不变量的完整规范和 Prover 运行

以下是 ownedTotalIsSumOfBalances 不变量的完整 CVL 规范，其中包括 $methods$ 块、ghost 变量、Hook以及 preserved 的 $ownerHasBalance$ 和 $balanceOfConsistency$ 不变量：

methods {
    function ownerOf(uint256) external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

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

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
    _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];
    // {
    //     preserved {
    //         require balanceLimited(user);
    //     }
    // }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
            // require balanceLimited(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
    _ownedTotal == _supply
    {
        preserved mint(address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
        }
        preserved safeMint(address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
        }
        preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
            require balanceLimited(to);
        }
        preserved burn(uint256 tokenId) with (env e) {
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
        preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
        preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
        preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
    }

Prover 运行：链接

notMintedUnset 不变量 — 未铸造的代币没有批准

如果一个代币未铸造（即它没有所有者），那么它也必须没有批准的地址：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;

$unsafeOwnerOf()$ 和 $unsafeGetApproved()$ 是 harness 视图函数，当 $tokenId$ 未铸造时，它们返回零地址而不是 revert。相比之下，标准的 $ownerOf()$ 和 $getApproved()$ 函数对于未铸造的代币会 revert，因此永远不会返回这些零地址值。

使用 $ownerOf()$ 和 $getApproved()$ 会给不变量评估带来问题。不变量必须是求值为 true 或 false 的布尔表达式，但当 Prover 评估一个在未铸造的 $tokenId$ 上调用 $ownerOf(tokenId)$ 或 $getApproved(tokenId)$ 的不变量时，函数调用会 revert。revert 既不是 true 也不是 false，这会阻止不变量表达式求值为布尔值。虽然规则可以使用 $@withrevert$ 并检查 $lastReverted$ 标志来处理 revert 的调用，但不变量是纯布尔表达式，不支持此类控制流逻辑。

通过使用 harness 函数 $unsafeOwnerOf()$ 和 $unsafeGetApproved()$，它们返回零地址而不是 revert，Prover 可以为所有 $tokenId$ 值（包括未铸造的代币）评估不变量表达式为布尔值。

这个不变量很重要，因为如果某个不存在的 $tokenId$ 被设置了批准，而该 $tokenId$ 随后被铸造给不同的地址，那么之前批准的地址仍将保留转移权限。这可能会导致铸造后立即发生未经授权的转移。该不变量保证所有代币都以默认状态开始——没有所有者，没有批准。

notMintedUnset 不变量的完整规范和 Prover 运行

methods {
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;

    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;

Prover 运行：链接

zeroAddressHasNoApprovedOperator 不变量 — 未铸造的代币没有批准的 操作者

$isApprovedForAll$ 是一个公共函数，用于检查某个操作者（一个地址）是否被授权管理某个账户拥有的所有代币。这个不变量规定，任何地址都不应该被批准为 $address(0)$ 的操作者。由于 $address(0)$ 是未铸造代币的隐式所有者，这可以防止任何操作者在代币铸造之前就被预授权管理代币。

因此，视图函数 $isApprovedForAll(0, a)$ 必须始终返回 $false$：

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
    !isApprovedForAll(0, a)
    {
        preserved with (env e) {
            require nonzerosender(e);
        }
    }

然而，这仅在 preserved 条件下成立，即调用者（$msg.sender$）不是零地址（$require nonzerosender(e)$），根据定义：

definition nonzerosender(env e) returns bool = e.msg.sender != 0;

这个假设是有道理的，因为 $address(0)$ 没有私钥，因此没有人能从这个地址发起交易，这使得在现实中不可能调用任何函数。然而，由于 $setApprovalForAll()$ 函数没有明确阻止零地址调用它，Prover 将会探索这种可能性，这可能导致误报，即 Prover 报告了实际上不会发生的违规。

通过确保 $msg.sender$ 非零的 preserved 条件，这个不变量保证 $address(0)$ 永远不能拥有批准的操作者。因此，未铸造的代币不能拥有操作者。

zeroAddressHasNoApprovedOperator 不变量的完整规范和 Prover 运行

现在，这是 zeroAddressHasNoApprovedOperator 不变量的完整规范，其中包括 $methods$ 块和 definition：

methods {
    function isApprovedForAll(address,address) external returns (bool) envfree;
    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonzerosender(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
    !isApprovedForAll(0, a)
    {
        preserved with (env e) {
            require nonzerosender(e);
        }
    }

Prover 运行：链接

所有不变量的合并 CVL 规范

现在我们已经独立讨论了每个不变量，我们可以将它们合并到一个单一的规范中：

methods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;

    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;

    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom forall address a. _ownedByUser[a] == 0;
}

hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
    _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
    _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
    _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

ghost mapping(address => mathint) _balances {
    init_state axiom forall address a. _balances[a] == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];
    // {
    //     preserved {
    //         require balanceLimited(user);
    //     }
    // }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
            // require balanceLimited(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
    _ownedTotal == _supply
    {
        preserved mint(address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
        }
        preserved safeMint(address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
        }
        preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
            require balanceLimited(to);
        }
        preserved burn(uint256 tokenId) with (env e) {
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(ownerOf(tokenId));
        }
        preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
        preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
        preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
            require balanceLimited(to);
            requireInvariant ownerHasBalance(tokenId);
            // requireInvariant balanceOfConsistency(from);
            // requireInvariant balanceOfConsistency(to);
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
    !isApprovedForAll(0, a)
    {
        preserved with (env e) {
            require nonzerosender(e);
        }
    }

这是 Prover 运行。

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

  • 原文链接： rareskills.io/post/certo...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
RareSkills
RareSkills
https://www.rareskills.io/

RareSkills

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！