简介

本章是我们对 OpenZeppelin’s ERC-721 CVL specification 代码解读的第三部分（3/5），重点关注代币的转账与授权规则，具体包括：

• transferFrom()
• approve()
• setApprovalForAll()
• zeroAddressBalanceRevert()

这些规则验证了所有权转移、单代币授权、针对所有代币的操作员授权，以及查询 balanceOf(0) 时会发生 revert（回滚）。

形式化验证 transferFrom()

transferFrom() 函数将 NFT 的所有权更改为另一个地址。它假设该 NFT 已经被铸造（minted），并且只能由所有者、获得该 token ID 授权的地址或获得所有者全部代币授权的操作员（operator）来调用。

以下是 transferFrom 规则，我们将在代码块之后逐节进行解释：

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);
    
    // pre-call state
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

前置条件

这些前置条件指定了在 Prover 执行 transferFrom() 之前必须满足的条件。我们将在后文解释代码块中的每一行：

Copy
require nonpayable(e);
require authSanity(e);
...
requireInvariant ownerHasBalance(tokenId);
require balanceLimited(to);

require nonpayable(e)

这要求在调用 transferFrom() 时不能发送 ETH，因为该函数是 non-payable 的。它被表示为一个定义（definition）：

Copy
definition nonpayable(env e) returns bool = e.msg.value == 0;

它将条件 e.msg.value == 0 定义为一个名为 nonpayable(e) 的可重用表达式，用于检查调用是否未携带 ETH。

尽管 ERC-721 standard 将 transferFrom() 规范为 payable，但 OpenZeppelin 将其实现为 non-payable。在实践中，通常不期望在进行 NFT 转账时附带发送 ETH，因此这已成为一种实际惯例。CVL 规则强制执行 e.msg.value == 0。

require authSanity(e)

这要求调用者不能是零地址。它同样被表示为一个 definition：

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

如果没有这个要求，Prover 会将 address(0) 视为有效的调用者，尽管实际上没有任何调用能够源自 address(0)。合约的授权逻辑绝不允许 address(0) 成为所有者、授权地址或操作员，因此任何因 address(0) 作为调用者而引发的违规行为都是误报（false positives）。

requireInvariant ownerHasBalance(tokenId)

此前置条件要求在规则开始时 ownerHasBalance(tokenId) 不变量（该不变量保证如果代币存在，其所有者的余额必定为正）必须成立。它强制 Prover 从一个任何现有代币都具有有效（非零）所有者的状态开始验证：

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	require authSanity(e);
	...
	requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
	require balanceLimited(to);
	...
}

Copy
// invariant as a precondition

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

ownerHasBalance 不变量通过 preserved 块依赖于另一个不变量 balanceOfConsistency，后者用于验证 balanceOf、_ownedByUser 以及 ghost 变量 _balances 是否相等：

Copy
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    {
        preserved { // invariant as a preserved condition
            requireInvariant balanceOfConsistency(ownerOf(tokenId));  
        }
    }

Copy
// invariant as a preserved condition 

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

通过将不变量 ownerHasBalance(tokenId) 用作前置条件，transferFrom 规则继承了 balanceOfConsistency 的保证：

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	require authSanity(e);
	...
	requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
	require balanceLimited(to);
	...
}

如果移除该前置条件，Prover 可能会从不可能的状态开始执行该规则，即所有权和余额不匹配——例如，某个地址可能被记录为某个代币的所有者，但其余额却为零，因为 ghost 值与存储中的数据不一致。这会导致误报的违规。

require balanceLimited(to)

balanceLimited(to) 限制了接收者（to）地址的余额，使其保持在 max_uint256 以下，正如其定义中所表达的那样：

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

为了提高 Gas 效率，合约在 unchecked 块内对余额进行自增。尽管在实际情况中几乎不可能发生溢出（overflow），但 Prover 仍然会探索溢出的情况，因为 transferFrom() 调用了 _update()，而在其中余额的自增恰好发生在 unchecked 块内：

Copy
// ERC721.sol

function transferFrom(address from, address to, uint256 tokenId) public virtual {
    ...
    address previousOwner = _update(to, tokenId, _msgSender());
    ..
}

Copy
/// ERC721.sol

function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
    ...

    if (to != address(0)) {
        unchecked {
            _balances[to] += 1;
        }
    }
	  ...
}

使用 require balanceLimited(to) 可以排除实际上无法达到的溢出状态，这些状态会导致规则在不符合实际的场景中失败。

调用前状态

在调用 tra``nsferFrom() 方法之前，我们记录下状态变量，以便与调用后的值进行比较：

• balanceOfFromBefore 是转账前发送者（from）的余额。
• balanceOfToBefore 是转账前接收者（to）的余额。
• balanceOfOtherBefore 是转账前某个未参与账户（otherAccount）的余额。
• ownerBefore 是待转账代币的所有者。
• otherOwnerBefore 是某个未参与代币的所有者。
• approvalBefore 是待转账代币的授权状态。
• otherApprovalBefore 是某个未参与代币的授权状态。

Copy
uint256 balanceOfFromBefore  = balanceOf(from);
uint256 balanceOfToBefore    = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore          = unsafeOwnerOf(tokenId);
address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
address approvalBefore       = unsafeGetApproved(tokenId);
address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

请注意，我们使用 unsafeGetApproved()（一个 harness 函数）来读取授权状态，而不是使用合约原生的 getApproved()。harness 版本即使在代币尚未铸造或已被销毁（owner == address(0)）时也能暴露授权值，因为它直接返回 _getApproved(tokenId)，而不检查代币是否存在或是否有所有者。相比之下，实际合约中的 getApproved() 会执行所有权检查，如果代币尚未铸造或已被销毁，则会 revert：

Copy
// ERC721Harness.sol -- returns approval without checking token existence or ownership

function unsafeGetApproved(uint256 tokenId) external view returns (address) {
    return _getApproved(tokenId);
}

Copy
// ERC721.sol -- performs an ownership check and reverts if the token is unminted or burned

function getApproved(uint256 tokenId) public view virtual returns (address) {
    _requireOwned(tokenId); // reverts if `owner == address(0)`

    return _getApproved(tokenId);
}

这防止了查询未铸造或已销毁代币的授权状态，因为 getApproved() 在这些情况下会发生 revert。然而，规则需要在经过零地址状态的状态转换之间比较授权值：

• 代币创建（从未铸造到已铸造）——所有者从 address(0) 转换到非零地址
• 代币销毁（从已铸造到未铸造/已销毁）——所有者从非零地址转换回 address(0)

因此，需要使用 unsafeGetApproved()，以便规则即使在代币处于零地址所有者状态时也能读取授权值。

既然调用前的状态已经记录完毕，我们接着执行 transferFrom()，并在随后的断言中对调用后的值进行推理分析。

转账调用

带有 @withrevert 的 transferFrom() 调用会指示 Prover 同时探索 revert 和非 revert 两种执行路径。!lastReverted 条件捕获了该调用是否未发生 revert，并将其存储在 success 中：

Copy
transferFrom@withrevert(e, from, to, tokenId);
bool success = !lastReverted;

断言 — 活性、效果与无副作用

活性 (Liveness):

当且仅当（<=>）以下所有条件都成立时，转账才不会 revert：

• from == ownerBefore

  from 地址（代币转出的地址）必须是该代币的前任所有者。

• from != 0

  from 地址不能是零地址。

• to != 0

  to 地址（接收者）不能是零地址。

• (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))

  操作员（调用者）必须通过以下至少一种方式获得授权：

  • operator == from — 所有者转移自己的代币
  • operator == approvalBefore — 操作员获得了对该特定代币的授权（通过 approve()）
  • isApprovedForAll(ownerBefore, operator) — 操作员获得了该所有者所有代币的统管授权（通过 setApprovalForAll()）

Copy
// liveness
assert success <=> (
    from == ownerBefore &&
    from != 0 &&
    to   != 0 &&
    (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
);

效果 (Effect):

如果转账没有 revert，则会应用以下状态变化：

• to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0)

  发送者的余额减少 1，但在自我转账（from == to）的情况下保持不变。

• to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1 : 0)

  接收者的余额增加 1，但在自我转账（from == to）的情况下保持不变。

• unsafeOwnerOf(tokenId) == to

  接收者（to）地址成为 tokenId 的新所有者。

• unsafeGetApproved(tokenId) == 0

  对 tokenId 的授权被清除。

Copy
// effect
assert success => (
    to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
    to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
    unsafeOwnerOf(tokenId)                 == to &&
    unsafeGetApproved(tokenId)             == 0
);

无副作用 (No side effect):

在断言了预期的状态变化（效果）之后，我们还要检查是否对余额、所有权或授权状态产生了意外的副作用：

• 关于余额

  balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to)

  如果任何账户的余额发生了变化，这意味着（=>）该账户要么是发送者，要么是接收者。任何未参与账户的余额都不会被修改。

• 关于所有权

  unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId

  如果任何代币的所有权发生了变化，这意味着（=>）该代币就是被转账的代币。任何未参与代币的所有权都不会改变。

• 关于授权

  unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId

  如果任何代币的授权状态发生了变化，这意味着（=>）该代币就是被转账的代币。任何未参与代币的授权状态都不会被修改。

Copy
// no side effect
assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

以下是 transferFrom 规则的完整规范：

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

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

此处为 Prover 运行结果。

既然我们已经验证了 transferFrom()``，现在可以转向探讨为这些转账提供授权的机制了。

回想一下，transferFrom() 仅在调用者具有适当授权时才能成功执行：例如作为代币所有者、作为获得该代币授权的地址，或者作为获得所有者所有代币统管授权的操作员。接下来的两个规则验证了授予这些权限的函数：用于单代币授权的 approve() 和用于操作员级别授权的 setApprovalForAll()。

形式化验证 approve()

approve() 合约函数会赋予某个地址转移特定代币的权限。仅当代币存在且调用者是所有者或操作员（拥有统管授权）时，它才能成功执行。

以下是验证此行为的规则：

Copy
rule approve(env e, address spender, uint256 tokenId) {
	// preconditions
    require nonpayable(e);
    require authSanity(e);
		
	// pre-call state
    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

前置条件

到目前为止，我们已经知道 nonpayable(e) 要求调用时不发送 Ether，而 authSanity(e) 要求 msg.sender 不能是零地址：

Copy
require nonpayable(e);
require authSanity(e);

Approve 调用

作为 OpenZeppelin 的 ERC-721 规则规范中的常见模式，approve 方法带有 @withrevert 被调用，并且 !lastReverted 的结果被存储在 success 变量中，以便对调用成功的情况进行推理：

Copy
approve@withrevert(e, spender, tokenId);
bool success = !lastReverted;

断言 — 活性、效果与无副作用

活性 (Liveness):

这意味着该函数调用“当且仅当”满足以下条件时才不会 revert：

• owner != 0

  代币所有者不能是零地址。这可以防止对不存在或已销毁的代币进行授权。

• (owner == caller || isApprovedForAll(owner, caller))

  这是一项授权检查，要求 caller 必须满足以下其一：

  • 是代币的 owner，或者
  • 是通过 isApprovedForAll(owner, caller) 获得授权的操作员（返回 true）

Copy
// liveness
assert success <=> (
    owner != 0 &&
    (owner == caller || isApprovedForAll(owner, caller))
);

效果 (Effect):

• assert success => unsafeGetApproved(tokenId) == spender

  如果调用成功（success == true），那么现在 tokenId 的被授权地址必须等于 spender。

Copy
// effect
assert success => unsafeGetApproved(tokenId) == spender;

无副作用 (No side effect):

• assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId

  如果 otherTokenId 的被授权地址发生变化，那么 otherTokenId 必定与 tokenId 相同。这意味着只有 tokenId（预期目标）的授权得到了更新，没有其他代币（otherTokenId）受到意外影响。

Copy
// no side effect
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

以下是 approve 规则的完整规范：

Copy
methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

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

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

此处为 Prover 运行结果。

形式化验证 setApprovalForAll()

setApprovalForAll() 函数授权某个地址来管理调用者拥有的所有代币。以下是该规则：

Copy
rule setApprovalForAll(env e, address operator, bool approved) {
	// preconditions
    require nonpayable(e);
		
	// pre-call state
    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

到了这一步，我们已经对前置条件、调用前和调用后的状态以及方法调用的模式非常熟悉了，因此我们将跳过这些内容，直接来看断言。

断言 — 活性、效果与无副作用

活性 (Liveness):

• assert success <=> operator != 0

  当且仅当操作员不是零地址时调用才会成功。ERC-721 禁止将零地址授权为操作员，因此该断言要求当 operator == 0 时调用必须失败：

Copy
// liveness
assert success <=> operator != 0;

效果 (Effect):

• assert success => isApprovedForAll(owner, operator) == approved

  如果调用成功，(owner, operator) 交易对的授权状态必须与 approved 的布尔值相匹配。这意味着授权值（true 或 false）被正确设置了。

  Copy
  // effect
  assert success => isApprovedForAll(owner, operator) == approved;
  

无副作用 (No side effect):

• 如果任何 (otherOwner, otherOperator) 的授权状态发生了变化，这些地址必须与调用者（owner）和指定的操作员（operator）相匹配。任何对其他授权条目的更改都会导致该断言失败。

Copy
// no side effect
assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
    otherOwner    == owner &&
    otherOperator == operator
);

以下是 setApprovalForAll 规则的完整 CVL 规范：

Copy
methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

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

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

此处为 Prover 运行结果。

形式化验证 balanceOf(0) 会发生 revert

以下规则验证了当查询零地址时，balanceOf 函数总是会 revert。

下面是 balanceOf 的合约代码实现。如果 owner == address(0)，它会 revert：

Copy
function balanceOf(address owner) public view virtual returns (uint256) {
    if (owner == address(0)) {
        revert ERC721InvalidOwner(address(0));

    }
    return _balances[owner];
}

这是验证此行为的规则：

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

此处为 Prover 运行结果：

转账与授权的完整规范

以下是完整的规范及 Prover 运行结果。

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

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    transferFrom@withrevert(e, from, to, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from))            == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0) &&
        to_mathint(balanceOf(to))              == balanceOfToBefore   + assert_uint256(from != to ? 1 : 0) &&
        unsafeOwnerOf(tokenId)                 == to &&
        unsafeGetApproved(tokenId)             == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

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