ERC-721 中的安全铸造和安全转移规则

本文深入探讨了使用Certora Prover对ERC-721代币中的_safeMint()和safeTransferFrom()功能进行形式化验证。文章详细解释了如何通过模拟合约和CVL（Certora验证语言）的辅助函数来处理外部回调，以确保验证的完整性，并阐述了活性、效果和无副作用断言。

Formal Verification with Certora

ERC-721 中的 SafeMint 和 SafeTransfer 规则

模块 2：不变量、存储Hook、幽灵变量和代币的形式化验证

上次更新于 2026 年 2 月 13 日

介绍

本章是 OpenZeppelin ERC-721 CVL 规范代码演练的第四部分（共五部分），主要关注 safe mint 和 safe transfer 操作的形式化验证，具体包括：

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

_safeMint() 函数通过一项额外检查扩展了 _mint()：如果接收者是一个合约，它会检查该合约是否可以处理 ERC-721 代币。这可以防止 NFT 陷入缺少转移逻辑的合约中。

OpenZeppelin 中的 ERC-721 有两个版本的 safeMint：一个接受 bytes 数据参数，一个不接受。较简单的版本（不带 bytes）会调用带 bytes 的版本，并将一个空字符串作为 data 参数传入：

// 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 地址，然后如果接收者是一个合约，则在其上调用Hook函数 onERC721Received()。带有 bytes 参数的版本还会将 data 转发给接收合约的 onERC721Received Hook，这允许接收者根据提供的数据自定义其行为。例如，游戏合约可以直接将 NFT 铸造到玩家的库存合约中，并包含指定物品类型、稀有度或初始属性的 data 以触发游戏事件。

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

  • 接收者没有实现 onERC721Received()，
  • 回调回滚，或
  • 回调返回的值不是预期的选择器 0x150b7a02。

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

当 _safeMint() 在规则中被调用时，它会调用 checkOnERC721Received()，后者又会对接收合约调用 onERC721Received()。Prover 无法确定 onERC721Received() 将做什么，因此它将此调用视为未解析。未解析的外部调用会导致 Prover 假定存储的任意更改，这意味着存储变量和调用后断言中的 ghost 变量会取非确定性值，从而使断言失去意义。

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

// ERC721ReceiverHarness.sol -- 这是一个模拟合约

import "contracts/interfaces/IERC721Receiver.sol";

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

我们不验证外部接收者合约，因为其实现超出了我们的控制范围。相反，onERC721Received 调用被分派给一个模拟接收者合约，该合约始终返回预期的选择器 0x150b7a02。这意味着该规范不测试回调回滚或返回不正确值的情况。

然而，这并不意味着如果回调在实际执行中失败，_safeMint() 就不会回滚。活跃性断言通过回滚来确保函数在此类情况下的行为正确。

活跃性断言本身不检查回调的返回值；它检查整个调用是成功还是回滚。正如“铸造和销毁”一章中所讨论的，当且仅当 ownerBefore == address(0) 且 to != address(0) 时，铸造才不会回滚（!lastReverted）：

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

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

上面讨论的 safe mint 的相同原理也适用于 safe 代币转账。

safeTransferFrom 也有两个版本：一个接受 bytes 数据参数，一个不接受：

// 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 Hook，以便接收者可以在转移过程中处理额外的数据。如果接收者是一个没有实现 onERC721Received 或返回无效响应的合约，则整个交易会回滚。

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

形式化验证 safe mint

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

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

这是我们将接下来详细介绍的规则：

// 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 的两个版本：

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，它根据函数选择器将调用路由到适当的版本：

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

这个分支仅作为包罗万象的备用，但它在这条规则中是不可达的，因为 filtered 子句已经将 method f 限制为两个 safeMint 变体。Prover 不能提供任何其他函数选择器，因此 else 块只覆盖了在过滤规则下不可能发生的理论情况。

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

将 onERC721Received 分派给模拟接收者

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

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

由于只有模拟接收者实现了此方法，因此回调始终分派给它。如果多个合约实现了 onERC721Received，Prover 将分派给它们每一个并探索所有验证路径。

如果没有这个设置，Prover 会将 onERC721Received 调用视为未解析。结果，Prover 会生成反例，这些反例由于 safeMint 和 safeTransferFrom 规则中未解析的外部调用而违反断言。

Dispatchee — 模拟接收者合约

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

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

这是 IERC721Receiver 接口的最小实现。它接受任何传入的 ERC721 代币并返回预期的选择器 (0x150b7a02) 以表示成功转移。虽然它不执行任何额外的逻辑，但它为 onERC721Received 提供了有效的 dispatchee。

完整规范 — safeMint

这些断言与“铸造和销毁”章节中 mint 规则中的断言相同，其中活跃性、效果和无副作用检查已详细解释。因此，我们在此不再重复讨论，并请读者参阅该章节以获取进一步解释。

以下是 safeMint 的完整 CVL 规范：

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

注意：版本 8.1.0 中引入的新 Prover 功能允许 CVL 函数使用 @withRevert。这改变了函数内部的语法：@withRevert 不再放置在每个方法调用上，而是应用于 CVL 函数。我们更新了语法使其与最新的 Prover 版本兼容。

Prover 运行结果：链接

形式化验证 safe transferFrom

合约函数 safeTransferFrom() 使用 onERC721Received 安全检查扩展了 transferFrom()。因此，safeTransferFrom 规则的前置条件、调用前状态和断言与上一章“转移和批准”中 transferFrom 规则的相同，但它遵循与 safeMint 相同的方法执行模式：

  • 它使用 method f 并通过过滤来测试两种变体，
  • 通过 CVL 辅助函数路由执行，以及
  • 将 onERC721Received() 分派给模拟接收者。

这是规则。与 safeMint 一样，我们专注于如何使用方法过滤、辅助函数路由和外部回调处理来验证 safeTransferFrom 的两种变体：

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()，如下所示：

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 参数的变体。

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

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

这些断言与上一章“转移和批准”中 transferFrom 规则中的断言相同，其中活跃性、效果和无副作用检查已详细解释。

以下是 safeTransferFrom 的完整 CVL 规范：

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

注意：版本 8.1.0 中引入的新 Prover 功能允许 CVL 函数使用 @withRevert。这改变了函数内部的语法：@withRevert 不再放置在每个方法调用上，而是应用于 CVL 函数。我们更新了语法使其与最新的 Prover 版本兼容。

Prover 运行结果：链接。

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

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

0 条评论

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

RareSkills

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