简介

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

本章是 OpenZeppelin’s ERC-721 CVL specification 代码走查系列的第 (2/5) 部分，重点关注不变式属性。它验证了以下五个 ERC-721 不变式：

• balanceOfConsistency

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

• ownerHasBalance

  代币所有者始终具有大于零的余额。

• ownedTotalIsSumOfBalances

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

• notMintedUnset

  未铸造的代币未设置授权地址。

• zeroAddressHasNoApprovedOperator

  未铸造的代币没有授权操作员。

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

balanceOfConsistency 不变式

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

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

这三个数量必须相等，因为它们都代表同一个基本事实：用户拥有多少代币。任何差异都表明余额与所有权跟踪之间的记账不一致。

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

Copy
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 variable），它通过 Sload 钩子（hook）读取并镜像了私有存储映射变量 _balances。

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

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

如果没有此初始化，Prover 会假设余额有任意的初始值（基础情况），这可能导致初始状态下的记账错误。这会使跟踪逻辑失效，并在验证期间导致出现误报的违规结果。

初始化后，规范必须使用 Sload 钩子将存储的读取反映到幽灵状态中。Sload 钩子从实际的 _balances 存储槽中读取值，并将这些值与幽灵变量同步（幽灵变量与存储变量同名，但不会发生冲突）：

Copy
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 钩子返回的存储值约束为等于幽灵变量时，就会发生同步。这种同步是必要的，因为幽灵变量在读取存储时不会自动更新。

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

_ownedByUser[user] 是一个幽灵变量，表示满足 ownerOf(tokenId) == user 的所有 tokenId 的数量：

Copy
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）。

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

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

• 铸造：oldOwner == address(0) 且 newOwner != address(0)
• 销毁：oldOwner != address(0) 且 newOwner == address(0)
• 转移：oldOwner 和 newOwner 都是非零地址

该钩子会更新幽灵映射 _ownedByUser 以反映这些所有权变化：

Copy
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);
}

注意：我们故意注释掉了 _ownedTotal = ... 这行代码，因为在这一步它并不是必须的。我们现在不跟踪已拥有代币的总数；我们只跟踪每个单独用户拥有的代币。

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

Copy
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);

• 如果 newOwner != 0，则 newOwner 的代币计数加 1。这适用于：
  • 铸造（Mint）：当代币被创建并分配给用户时（从 address(0) 变为 newOwner）
  • 转移（Transfer）：当代币从一个用户转移到另一个用户时（从 oldOwner 变为 newOwner）
• 如果 newOwner == 0，这表示销毁（burn），因此没有 newOwner 接收代币。三元表达式的计算结果为 0，因此不进行加法。然而，代币的减少（销毁）仍需要被记录，这由第二行处理。

Sstore 钩子 _owners 中的第二行处理代币减量，这意味着发生了销毁和（同样发生）转移：

Copy
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);

• 如果 oldOwner != 0，以前的（非零）所有者持有了代币现在失去了它，因此我们减去 1。这同时适用于转移和销毁操作。
• 如果 oldOwner == 0，这表示铸造（mint），即代币是新创建的，没有前任所有者。三元表达式的计算结果为 0，因此不进行减法。相应的所有权计数实际上在第一行——即处理代币增量的那一行中入账。

既然我们已经讨论了不变式的表达式以及如何推导用户代币余额的三种表示法，规范中还剩下最后一部分需要完成：处理来自安全铸造（safe mint）和安全转移（safe transfer）操作的外部回调。

在验证期间，不变式会自动调用所有改变状态的函数，这意味着 Prover 会调用 safeMint() 和 safeTransferFrom() —— 这两者都会触发对接收者合约中 onERC721Received() 的外部回调。我们需要配置 Prover 如何处理此外部调用。否则，Prover 会将这些外部调用视为未解决（unresolved），这将导致幽灵变量和存储产生 havoc，从而引发不变式属性的误报违规。

DISPATCHER —— 解析 onERC721Received 回调

为了解析此回调，规范将 onERC721Received() 调用分发（dispatch）给一个模拟接收者合约（mock receiver contract），该合约返回 bytes4 选择器 0x150b7a02 以表明支持 ERC-721。要实现这种分发，我们需要：

• 创建一个简单的 ERC721 接收者合约（模拟合约），
• 将其包含在验证的场景 (scene)中，
• 在 methods 块中添加一个分发指令。

ERC721 模拟接收者合约：
下面是接收者合约，实现为一个 Harness，它返回 bytes4 选择器 0x150b7a02：

Copy
// 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 接收者规范。

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

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

Copy
// .conf

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

至此，模拟接收者已成为验证场景的一部分，可作为分发目标。

添加 DISPATCH 指令：

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

Copy
// .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）——例如，通过返回不正确的回调值——不变式也不受影响，因为回退不会导致任何状态改变。然而，我们在后面的章节中正式验证安全铸造和安全转移函数时则不是这样，那时发生回退的回调会导致断言失败。

在这个 CVL 不变式规范中，DISPATCHER 的作用仅仅是解析外部调用。如果没有它，safeMint() 和 safeTransferFrom()——包括它们的变体——会调用未解析的外部调用，这会产生 havoc 并导致不变式的误报失败。

balanceOfConsistency 不变式的完整规范及 Prover 运行结果

这是 balanceOfConsistency 不变式的完整 CVL 规范，其中包含了 methods 块、幽灵变量声明以及钩子实现：

Copy
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 存在（所有者非零），那么该所有者的余额必须大于零：

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

在后面验证转移（transfer）的章节中，该不变式被用作前置条件，发送者应当具有正数余额。我们可以将 unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 直接硬编码到规则中，但将其作为不变式进行证明可提供更强的安全性保证。

这里需要一个 preserved 块，以便在 ownerHasBalance 运行之前 require balanceOfConsistency(ownerOf(tokenId))。这告诉 Prover：“在检查所有者是否有余额之前，先确认 balanceOf 与幽灵变量追踪的所有权计数相匹配。” 它可以防止 Prover 由于 havoc 进入一种不一致的状态：所有者存在，但看起来余额为零。

这是该 CVL 不变式：

Copy
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 块、幽灵变量、钩子以及 preserved 中的 balanceOfConsistency 不变式：

Copy
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 v8.3.1 版本中通过验证。

这是 Prover 的运行链接。

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

在此不变式规范中，拥有代币的总数和总供应量是被推导出来的，因为核心的 ERC-721 标准并没有暴露出任何关于总供应量的概念——只有 ERC-721 Enumerable 才定义了 totalSupply()。由于此不变式无法直接针对标准函数进行验证，因此这些值是使用幽灵变量（_ownedTotal 和 _supply）和钩子重新构建的。

_ownedTotal 通过对存储变量 _owners 使用 Sstore 钩子观察所有权变化，计算当前存在多少代币。_supply 是所有用户余额的总和，同样作为幽灵变量进行跟踪。

当这两个值被重构并作为幽灵变量进行跟踪时，不变式验证 _ownedTotal 等于 _supply。这确保了一致的余额记账。如果拥有的代币超过了供应量，意味着余额被低估了（代币存在但未在余额中反映出来）。如果供应量超过了拥有的代币数量，意味着余额被高估了（余额声称的代币数量多于实际存在的数量）。

因此，这种等价关系保证了每个被拥有的代币在余额总数中恰好被计算一次：

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

_supply 和 _ownedTotal 都是幽灵映射变量，用于通过 Sstore 钩子跟踪代币的总供应量，只是从不同视角出发：

• _supply 通过在每次写入 _balances 存储时，减去旧余额并加上新余额来跟踪总供应量：

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

  通过在存储层面观察余额，即可推导出了 _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 钩子跟踪所拥有的代币数量，当所有权被清除时减去 1，当向非零地址分配代币时加上 1：

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

  让我们根据所有权的变化来模拟一下，但首先，为清晰起见，我们将代码重新整理：

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

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

    • newOwner 为非零，所以三元表达式的计算结果为 1，加 1。
    • oldOwner 为非零，所以三元表达式的计算结果为 1，减 1。

    最终净影响是对 _ownedTotal 无任何改变，因为既加了 1 又减了 1。从原理上讲，转移操作不影响总的所有权计数。

  • 如果 oldOwner 为零且 newOwner 为非零，则发生铸造（mint）：

    • newOwner 为非零，所以三元表达式的计算结果为 1，加 1。
    • oldOwner 为零，所以三元表达式的计算结果为 0，减 0。

    最终净影响是 +1，因为加了 1 且没有减去任何值。从原理上讲，铸造操作会增加总的所有权计数。

  • 如果 oldOwner 为非零且 newOwner 为零，则发生销毁（burn）：

    • 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 子句的不变式：

Copy
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);
        }
    }

注意：即使没有 requireInvariant balanceOfConsistency__，不变式 ownedTotalIsSumOfBalances _也能成功验证。为了讨论方便，我们将其注释掉，以便读者可以看清哪些 preserved 条件是验证不变式所严格必需的。_这并不意味着它毫无用处——既然它已经被证明成立，就可以假定它始终成立。因此，重新加回它是安全的。将其作为 preserved 条件添加通常还能缩短 Prover 的运行时间。

ownedTotalIsSumOfBalances 不变式的完整规范及 Prover 运行结果

这是 ownedTotalIsSumOfBalances 不变式的完整 CVL 规范，其中包含了 methods 块、幽灵变量、钩子以及 preserved 中的 ownerHasBalance 和 balanceOfConsistency 不变式：

Copy
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
    {
        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 运行链接：link

notMintedUnset 不变式 —— 未铸造的代币没有授权

如果一个代币未被铸造（即它没有所有者），那么它也必定没有被授权（approved）的地址：

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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() 函数在遇到未铸造的代币时会发生回退，因此永远不会返回这些零地址值。

使用 ownerOf() 和 getApproved() 会对不变式求值造成问题。不变式必须是求值为 true 或 false 的布尔表达式，但是当 Prover 在评估某个调用了未铸造 tokenId 的 ownerOf(tokenId) 或 getApproved(tokenId) 的不变式时，函数调用会发生回退。回退既不是 true 也不是 false，这会阻止不变式表达式得出布尔值。虽然规则（rules）可以使用 @withrevert 并且检查 lastReverted 标志来处理回退的调用，但不变式属于纯布尔表达式，不支持这种控制流逻辑。

通过使用返回零地址而非引发回退的 Harness 函数 unsafeOwnerOf() 和 unsafeGetApproved()，Prover 就可以针对所有 tokenId 值（包括未铸造的代币）将不变式表达式计算为布尔值。

这个不变式很重要，因为如果通过某种方式为不存在的 tokenId 设置了授权，并且该 tokenId 稍后被铸造到了一个不同的地址，那么之前被授权的地址仍会保留转移的权利。这可能允许在代币刚刚铸造后立即发生未经授权的转移。该不变式保证了所有的代币都以默认状态（无所有者，无授权）开始。

notMintedUnset 不变式的完整规范及 Prover 运行结果

Copy
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 运行链接：link

zeroAddressHasNoApprovedOperator 不变式 —— 未铸造的代币没有授权操作员

isApprovedForAll 是一个公开函数，用于检查某个操作员（某地址）是否被授权管理特定账户拥有的所有代币。该不变式声明，不应有任何地址被授权为 address(0) 的操作员。由于 address(0) 是未铸造代币的隐式所有者，这防止了任何操作员在代币被铸造之前就被预先授权管理代币。

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

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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) 定义）——的情况下，这才会成立：

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

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

通过 preserved 条件确保 msg.sender 是非零的，该不变式保证了 address(0) 永远不会有授权操作员。因此，未铸造的代币不可能有操作员。

zeroAddressHasNoApprovedOperator 不变式的完整规范及 Prover 运行结果

现在这是不变式 zeroAddressHasNoApprovedOperator 的完整规范，它包含了 methods 块和 definition：

Copy
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 运行链接：link

针对所有不变式整合的 CVL 规范

既然我们已经独立地讨论了每个不变式，我们可以将它们整合到单一的一个规范中：

Copy
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 进行形式化验证 系列文章的一部分