简介

本章是我们对 OpenZeppelin’s ERC-721 CVL specification 代码走查的第四部分（4/5），重点在于对安全铸造（safe mint）和安全转账（safe transfer）操作进行形式化验证，具体包括：

• _safeMint() 和 _safeMint(bytes)
• safeTransferFrom() 和 safeTransferFrom(bytes)

_safeMint() 函数对 _mint() 进行了扩展，增加了一个额外的检查：如果接收方是一个合约，它会检查该合约是否能够处理 ERC-721 代币。这可以防止 NFT 被困在缺乏转账逻辑的合约中。

OpenZeppelin 中的 ERC-721 有两个版本的 safeMint：一个接受 bytes 类型的 data 参数，另一个则不接受。较简单的版本（不带 bytes）会通过传递空字符串作为 data 参数来调用带 bytes 的版本：

Copy
// ERC721.sol

function _safeMint(address to, uint256 tokenId) internal {
    _safeMint(to, tokenId, "");
}

function _safeMint(address to, uint256 tokenId, bytes memory data) internal virtual {
    _mint(to, tokenId);
    ERC721Utils.checkOnERC721Received(_msgSender(), address(0), to, tokenId, data);
}

注意：库 ERC721Utils 可以在 此处找到。

这两个版本都会将 NFT 铸造到 to 地址，然后如果接收方是合约，则在其上调用钩子函数 onERC721Received()。带有 bytes 参数的版本还会将 data 转发给接收合约的 onERC721Received 钩子，这使得接收方可以根据提供的数据自定义其行为。例如，游戏合约可能会将 NFT 直接铸造到玩家的物品栏合约中，并包含指定物品类型、稀有度或初始属性的 data 以触发游戏事件。

如果出现以下情况，这两个版本都会回退（revert）并撤销铸造：

• 接收方没有实现 onERC721Received()，
• 回调发生回退，或者
• 回调返回了非预期选择器 0x150b7a02 的其他值。

如果不解析其对接收合约的外部调用，就无法对 _safeMint() 进行形式化验证。

当在规则中调用 _safeMint() 时，它会调用 checkOnERC721Received()，后者继而对接收合约发起对 onERC721Received() 的外部调用。Prover 无法确定 onERC721Received() 会执行什么操作，因此它将该调用视为未解析的（unresolved）。未解析的外部调用会导致 Prover 假设存储发生了任意更改，这意味着调用后断言（post-call assertions）中的存储变量和 ghost 变量将获得非确定性的值，从而使断言变得毫无意义。

为了解析该外部调用，我们添加了一个模拟（mock）接收者合约，其 onERC721Received 函数返回 0x150b7a02（即 this.onERC721Received.selector 的值）。

Copy
// ERC721ReceiverHarness.sol -- this is a mock contract

import "contracts/interfaces/IERC721Receiver.sol";

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

我们不对外部接收者合约进行验证，因为它的实现超出了我们的控制范围。相反，我们将 onERC721Received 调用分发（dispatch）给一个总是返回预期选择器 0x150b7a02 的模拟接收者合约。这意味着该规范（specification）不会测试回调回退或返回错误值的情况。

然而，这并不意味着在实际执行中发生回调失败时 _safeMint() 不会回退。活性断言（liveness assertion）可确保函数在这种情况下通过回退来表现出正确的行为。

活性断言不会检查回调返回值本身；它检查的是作为一个整体的调用是成功了还是回退了。正如在“Mint and Burn”一章中所讨论的，当且仅当 ownerBefore == address(0) 且 to != address(0) 时，铸造不会回退（!lastReverted）：

Copy
bool success = !lastReverted;
assert success <=> (ownerBefore == 0 && to != 0);

当接收者回调导致回退时，右侧（ownerBefore == 0 && to != 0）仍然满足，因为这些值是在调用之前捕获的。然而，success 为 false，这违反了双条件（biconditional）断言。Prover 会检测到这一矛盾并报告违规。因此，不需要显式检查回调返回值的额外断言。

上述关于 safe mint 讨论的相同原理也适用于安全的代币转账（safe token transfers）。

safeTransferFrom 同样有两个版本：一个接受 bytes 类型的 data 参数，另一个则不接受：

Copy
// ERC721.sol

function safeTransferFrom(address from, address to, uint256 tokenId) public {
    safeTransferFrom(from, to, tokenId, "");
}

function safeTransferFrom(address from, address to, uint256 tokenId, bytes memory data) public virtual {
    transferFrom(from, to, tokenId);
    ERC721Utils.checkOnERC721Received(_msgSender(), from, to, tokenId, data);
}

在带有 bytes 参数的版本中，data 会被转发到接收合约的 onERC721Received 钩子中，以便接收方能够在转账期间处理额外的数据。如果接收方是一个未实现 onERC721Received 或者返回无效响应的合约，整个交易将会回退。

safeMint() 和 safeTransferFrom() 都遵循相同的外部调用模式，因此规范在验证这些函数时使用了同一个模拟接收者合约。

形式化验证 safe mint

由于 _safeMint() 和 _safeMint(bytes) 是内部函数，OpenZeppelin 通过 harness 函数将它们暴露出来，以便 Prover 可以调用它们：

Copy
// ERC721Harness.sol

function safeMint(address to, uint256 tokenId) external {
    _safeMint(to, tokenId);
}

function safeMint(address to, uint256 tokenId, bytes memory data) external {
    _safeMint(to, tokenId, data);
}

下面的 safeMint 规则使用了 method f（任意函数调用），其方式与参数化规则（parametric rules）相同。在典型的参数化规则中，函数和参数都是任意的（f(e, args)）。在这里，filtered 块将 method f 限制为仅有的两个 safeMint 变体，并且显式声明了参数 to 和 tokenId，而不是使用 args。这种显式声明允许规则应用约束这些参数的前置条件，而这无法在 calldataarg args 构造中直接完成。这意味着函数在允许的集合内是任意的，而参数是受控的，这与完全的参数化模式不同。

下面是该规则，我们接下来会逐步讲解：

Copy
// ERC721.spec -- safeMint

rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
} {
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    helperMintWithRevert@withrevert(e, f, to, tokenId);
    bool success = !lastReverted;

    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

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

将 method f 过滤为 safeMint 变体

method f 参数告诉 Prover 去测试任意函数，但 filtered 子句将测试限制为 safeMint 的仅有两个版本：

Copy
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
} {
	...
    helperMintWithRevert@withrevert(e, f, to, tokenId);
	...
}

为了在单个规则中处理这两种变体，我们使用了一个辅助函数 helperMintWithRevert，它会根据函数选择器将调用路由到适当的版本：

Copy
function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
    if (f.selector == sig:safeMint(address,uint256).selector) {
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff;
        safeMint(e, to, tokenId, params);
    } else {
        require false;
    }
}

辅助函数使得规则能够在单个规则中使用 method f 同时测试 safeMint() 和 safeMint(bytes)，因此无需为每个变体编写单独的规则。它根据函数选择器对调用进行路由，并将执行引导至相应的 if/else 分支。

让我们解释一下每个条件：

• f.selector == sig:safeMint(address,uint256).selector

  如果任意方法调用是双参数的 safeMint(address,uint256)，则 CVL 辅助函数会调用 safeMint(e, to, tokenId)。

• f.selector == sig:safeMint(address,uint256,bytes).selector

  如果任意方法调用是三参数的 safeMint(address, uint256, bytes)，CVL 辅助函数会调用 safeMint(e, to, tokenId, params)，其中 params 通过 require params.length < 0xffff 被限制为小于 0xffff（$2^{16} - 1$ 或 65,535 字节）。

  由于 bytes 是一个动态大小的数组，require params.length < 0xffff 是一个实用的验证限制——它大到足以涵盖 safeMint 数据参数的实际使用场景，但又小到足以防止 Prover 去探索不切实际的过大输入。

• else { require false; }

  包含这个分支仅作为一种兜底（catch-all）处理，但在这条规则中它是不可达的，因为 filtered 子句已经将 method f 限制为两个 safeMint 变体。Prover 无法提供任何其他的函数选择器，因此 else 块仅涵盖了在过滤规则下不可能发生的理论情况。

注意：在原始的 OpenZeppelin 规范中，辅助函数 helperMintWithRevert 还包含一个针对 mint(address,uint256) 的分支，但该情况已经被规则中的 filtered 子句排除了。由于规则只允许 safeMint() 和 safeMint(bytes) ，为了清晰起见，我们移除了未使用的分支。作为参考，这里是原始的 helperMintWithRevert 代码。

将 onERC721Received 分发给模拟接收者

在 methods 块中添加了 DISPATCHER，以指示 Prover 将调用分发（dispatch）给验证场景中实现了指定方法（onERC721Received）的任何合约（用通配符 _ 表示）：

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

由于只有模拟接收者实现了该方法，回调总是被分发给它。如果有多个合约实现了 onERC721Received，Prover 会分发给它们中的每一个，并探索所有的验证路径。

如果没有这个配置，Prover 会将 onERC721Received 调用视为未解析的。这样一来，由于 safeMint 和 safeTransferFrom 规则中存在未解析的外部调用，Prover 就会生成违反断言的反例。

Dispatchee（被分发者）——模拟接收者合约

被分发者（Dispatchee）是场景中作为分发调用目标的合约。场景中必须包含至少一个实现了 onERC721Received 的合约。以下合约为此提供了一个最小的 dispatchee：

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

这是 IERC721Receiver 接口的最小实现。它接受任何传入的 ERC721 代币，并返回预期的选择器（0x150b7a02）以发出转账成功的信号。虽然它不执行额外的逻辑，但它为 Prover 提供了一个用于 onERC721Received 的有效 dispatchee。

完整规范 —— safeMint

这里的断言与“Mint and Burn”一章中 mint 规则的断言完全相同，在那一章中已经详细解释了活性（liveness）、效果（effect）和无副作用（no side-effect）检查。因此，我们在此不再重复这一讨论，建议读者参考该章节以获取进一步的说明。

下面是 safeMint 的完整 CVL 规范：

Copy
methods {
    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 nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

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

function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
    if (f.selector == sig:safeMint(address,uint256).selector) {
        // safeMint@withrevert(e, to, tokenId);
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff;
        // safeMint@withrevert(e, to, tokenId, params);
        safeMint(e, to, tokenId, params);
    } else {
        require false;
    }
}

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: safeMint behavior and side effects                                                                            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
} {
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    helperMintWithRevert@withrevert(e, f, to, tokenId);
    bool success = !lastReverted;
    
		// liveness
    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

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

注意：在 version 8.1.0 中引入的一项 Prover 新功能允许 CVL 函数使用 @withRevert 。这改变了函数内部的语法：无需在每次方法调用上放置 @withRevert ，现在它可以直接应用于 CVL 函数上。我们更新了语法，使其能够与最新版本的 Prover 一起工作。

这里是 Prover 的运行结果：链接

形式化验证 safe transferFrom

合约函数 safeTransferFrom() 通过 onERC721Received 安全检查对 transferFrom() 进行了扩展。因此，safeTransferFrom 规则的前置条件、调用前状态以及断言，与上一章的 transferFrom 规则完全相同，但它遵循与 safeMint 相同的方法执行模式：

• 它通过带过滤的 method f 来测试这两种变体，
• 通过一个 CVL 辅助函数路由执行，并且
• 将 onERC721Received() 分发给模拟接收者。

以下是该规则。与 safeMint 一样，我们将重点关注如何利用方法过滤、辅助函数路由和外部回调处理来验证这两种 safeTransferFrom 变体：

Copy
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
    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);

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

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

将 method f 过滤为 safeTransferFrom 变体

rule safeTransferFrom 将执行约束为两个方法（通过 method f），即：

• safeTransferFrom(address, address, uint256)
• safeTransferFrom(address, address, uint256, bytes)

然后它将调用传递给 CVL 函数 helperTransferWithRevert()，如下所示：

Copy
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
	...
    
    helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
    bool success = !lastReverted;

    ...
}

我们对 safeTransferFrom() 有单独的条件逻辑——一个针对带有 bytes 参数的变体，另一个针对没有该参数的变体。

对于带有 bytes 的变体，我们将字节参数的长度限制为小于 0xffff，以将数组保持在实际边界内，并限制探索空间。除了这一限制之外，这两种 safeTransferFrom() 变体都遵循相同的逻辑并使用相同的规则结构：

Copy
function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
    if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff; 
        safeTransferFrom(e, from, to, tokenId, params);
    } else {
        calldataarg args;
        f(e, args);
    }
}

注意：与 safeMint 规则类似， f.selector == sig:transferFrom(address,address,uint256).selector 条件分支已从此 CVL 函数中移除，因为它是不必要的。该规则已经过滤掉了除 safeTransferFrom() 和 safeTransferFrom(bytes) 以外的所有函数。作为参考，这里是原始的 helperTransferWithRevert 代码： 链接

分发 onERC721Received 回调

在 safeMint 章节中，我们配置了模拟接收者和 DISPATCHER(true) 设置，以便 Prover 能够对外部回调 onERC721Received 进行建模。

这里需要相同的设置，因为 safeMint 和 safeTransferFrom 都会触发对 ERC-721 接收者的外部调用。如果没有这个分发配置，Prover 会将回调视为未解析的外部调用，这会导致严重混乱并使调用后断言变得毫无意义。

完整规范 —— safeTransferFrom

这里的断言与上一章“Transfer and Approval”中 transferFrom 规则的断言完全相同，在那一章中详细解释了活性、效果和无副作用检查。

下面是 safeTransferFrom 的完整 CVL 规范：

Copy
methods {
    function balanceOf(address) external returns (uint256) 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;

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

function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
    if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        // safeTransferFrom@withrevert(e, from, to, tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff; 
        // safeTransferFrom@withrevert(e, from, to, tokenId, params);
        safeTransferFrom(e, from, to, tokenId, params);
    } else {
        calldataarg args;
        f@withrevert(e, args);
    }
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all 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);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: safeTransferFrom behavior and side effects                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
    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);

    helperTransferWithRevert@withrevert(e, f, 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;
}

注意：在 version 8.1.0 中引入的一项 Prover 新功能允许 CVL 函数使用 @withRevert 。这改变了函数内部的语法：无需在每次方法调用上放置 @withRevert ，现在它可以直接应用于 CVL 函数上。我们更新了语法，使其能够与最新版本的 Prover 一起工作。

这里是 Prover 的运行结果。

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