简介

ERC-721 是以太坊非同质化代币（NFT）的标准，广泛用于表示数字资产。与任何形式的资产一样，它围绕着供应量创建、供应量移除以及所有权转移而展开。

本章重点介绍对铸造（mint）和销毁（burn）操作进行形式化验证。这是 OpenZeppelin’s ERC-721 CVL specification 代码解读的第一部分（1/5）。

在整个规范中，OpenZeppelin 使用了一种将三种类型的断言结合到单个 rule（规则）中的模式，分类如下：

1. Liveness（活性）—— 指定函数不发生 revert（回退）的条件。
2. Effect（效果）—— 指定当函数未发生 revert 时所发生的状态变更。
3. No side-effect（无副作用）—— 指定除了 Effect 断言中的状态变更外，不发生任何意外的状态变更。

暴露内部函数 _mint() 和 _burn() 以进行验证

_mint() 和 _burn() 是 internal（内部）函数，旨在供开发者继承并构建用于创建和销毁 NFT 的自定义逻辑。在本规范中，harness 合约继承并将它们暴露为 external（外部）函数，这使得 Prover 可以在验证期间调用 _mint() 和 _burn()。

以下是 OpenZeppelin implementations 对以下内容的实现：

• _mint()
• _burn()
• 暴露它们的 harness 合约

Copy
// ERC721.sol

function _mint(address to, uint256 tokenId) internal {
    if (to == address(0)) {
        revert ERC721InvalidReceiver(address(0));
    }
    address previousOwner = _update(to, tokenId, address(0));
    if (previousOwner != address(0)) {
        revert ERC721InvalidSender(address(0));
    }
}
...

function _burn(uint256 tokenId) internal {
    address previousOwner = _update(address(0), tokenId, address(0));
    if (previousOwner == address(0)) {
        revert ERC721NonexistentToken(tokenId);
    }
}

Copy
// ERC721Harness.sol

function mint(address account, uint256 tokenId) external {
    _mint(account, tokenId);
}
...

function burn(uint256 tokenId) external {
    _burn(tokenId);
}

形式化验证 mint

mint() 操作创建一个新的代币并将其分配给接收者。我们对其进行形式化验证以确保：

• 当且仅当代币未被铸造且接收者有效时，它不会发生 revert
• 如果它未发生 revert，总供应量（total supply）和接收者的余额（balance）均增加一
• 接收者成为所有者（owner）
• 没有其他账户的余额或代币所有权发生改变

以下是证明这些属性的 CVL 规则：

Copy
// ERC721.spec -- mint (explanation follows)


rule mint(env e, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	// requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);
    
	// pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
		
	// method call
    mint@withrevert(e, 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;
}

我们将按如下方式讨论上述规则的各个部分：

• 前置条件（Preconditions）
• 调用前状态（Pre-call state）
• Mint 调用（Mint call）
• 断言（Assertions）
  • liveness（活性）
  • effect（效果）
  • no side-effect（无副作用）

前置条件（Preconditions）

前置条件是规则中的一个约束，用于指定在 Prover 执行 mint() 方法之前必须为真的条件。在调用“之后”它是否仍然成立，取决于该方法引发的状态变更。

以下是 mint 规则的前置条件：

Copy
require nonpayable(e);
// requireInvariant notMintedUnset(tokenId); // intentionally commented out
...

require balanceLimited(to);

注意：为了便于讨论，invariant（不变式）前置条件 notMintedUnset(tokenId) 被注释掉了，因为即使没有它， mint 规则也能成功验证。我们将在下一章介绍 ERC-721 代码库的 CVL invariants。

• require nonpayable(e)

  这要求在不发送任何 ETH 的情况下进行调用，因为 mint() 是不可支付（non-payable）的。nonpayable(e) 表示为一个 definition，如果 e.msg.value == 0，则返回 true，否则返回 false：

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

  它通过将 e.msg.value == 0 条件绑定到名为 nonpayable(e) 的可重用表达式，封装了检查调用不携带 ETH 的逻辑。这个 definition 允许我们在整个规范中引用该条件，而不是每次调用不可支付函数时都重复编写 e.msg.value == 0。

  注意： definition 是 CVL 中的一个宽泛主题。要了解更多信息，请查阅 Certora documentation。在本系列中，definition 仅被直接用作可重用表达式，以提高代码的可读性。

• require balanceLimited(to)

  这要求接收者的余额小于 max_uint256。它同样表示为一个 definition，如果 balanceOf(account) < max_uint256 则返回 true：

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

  OpenZeppelin 的 ERC-721 实现为了节省 Gas，特意在 unchecked 块内增加余额。溢出在理论上是可能的，但在实际中是不可能的，因为达到 max_uint256 需要铸造比现实中可能存在的更多的 NFT。因此，前置条件 require balanceLimited(to) 是合理的。

  如果没有前置条件 balanceLimited(to)，Prover 将会考虑溢出情况，因为 mint() 调用了 _update() 函数，而余额的增加发生在 unchecked 块内：

  Copy
  // ERC721.sol
  
  function _mint(address to, uint256 tokenId) internal {
      ...
      address previousOwner = _update(to, tokenId, address(0));
      ...
  }
  

  Copy
  /// ERC721.sol
  
  function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
      ...
  
      if (to != address(0)) {
          unchecked {
              _balances[to] += 1;
          }
      }
  	  ...
  }
  

记录调用前状态 —— mint 调用前的总供应量、余额和所有权

在调用 mint() 函数之前，会记录以下状态。随后会在断言部分将这些值与调用后的值进行比较：

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

• mathint supplyBefore = _supply

  这记录了 mint 调用前的总供应量，以便将其与 mint 后的供应量进行比较，确认其增加了 1。

  _supply 是一个 ghost 变量，用于跟踪总供应量，并且在添加新余额和减去旧余额时通过 Sstore hook 进行更新。

  ghost 变量 _supply 被声明为 mathint，因此 supplyBefore 也必须是 mathint。如果 supplyBefore 被声明为 uint256，Prover 将报告类型错误。出现此错误是因为 mathint 表示无界的数学整数，而 uint256 表示有界的整数。将 mathint 值分配给 uint256 会假设该值在 256 位内，而 Prover 无法安全地做出这种假设。

  以下是更新 ghost 变量 _supply 的 Sstore hook 实现：

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

• uint256 balanceOfToBefore = balanceOf(to)

  这记录了接收者在 mint 调用前的余额，以便将其与 mint 后的余额进行比较，确认其也增加了 1。

• uint256 balanceOfOtherBefore = balanceOf(otherAccount)

  这记录了任何其他账户在 mint 调用前的余额，以便将其与 mint 后的余额进行比较，确认其未发生改变，从而证明无副作用。

• address ownerBefore = unsafeOwnerOf(tokenId)

  这记录了代币在 mint 调用前的所有者。为了使 mint 成功，此值必须为零，这是 liveness 的条件之一（ownerBefore == 0 且 to != 0）。

  unsafeOwnerOf() 是一个 harness 函数，即使对于没有有效所有者的代币，它也会暴露所有权。对于未铸造的代币，它返回零地址，这与在这些情况下会发生 revert 的 ownerOf() 不同。这使得该规则能够比较铸造前后的所有权，因为这些所有权转换涉及从零地址（未铸造状态）到有效所有者地址的过渡。

• address otherOwnerBefore = unsafeOwnerOf(otherTokenId)

  这记录了任意代币（非正在铸造的代币）在 mint 调用前的所有者，以便我们可以确认它在 mint 后未发生改变，从而证明无副作用。

Mint 调用（Mint call）

@withrevert 标签允许 Prover 探索发生 revert 和不发生 revert 的两条路径。!lastReverted 条件捕获了调用是否未发生 revert，并将其存储为 success：

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

断言（Assertions）—— liveness、effect 以及 no side effect

如前所述，在整个规范中使用的规则模式将 liveness、effect 和 no side-effect 组合到一个单独的规则中。以下是稍后我们将详细解释的代码块：

Copy
// 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;

Liveness（活性）:

下面的断言表明，当且仅当代币未被铸造（ownerBefore == 0）且接收者有效（to != 0）时，_mint() 才不会发生 revert：

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

我们在前两章中使用了 revert 结合析取（逻辑或）的模式。如果我们把上面的断言转换成那种模式，它就变成了：

当且仅当代币已经被铸造（ownerBefore != 0）或接收者无效（to == 0）时，_mint() 会发生 revert。

Copy
// reverts
assert !success <=> (
    ownerBefore != 0 ||
    to == 0
);

虽然“success + 合取”（liveness）模式列出了函数成功的所有条件，但“revert + 析取”模式列出了函数 revert 的所有条件。它们在逻辑上是等价的。

Effect（效果）:

如果 mint() 函数没有发生 revert，那么随之产生的状态变更如下：

• 总供应量刚好增加一（_supply == supplyBefore + 1）
• 接收者的余额刚好增加一（balanceOf(to) == balanceOfToBefore + 1）
• 代币现在归接收者所有（unsafeOwnerOf(tokenId) == to）

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

No side effect（无副作用）:

以下断言检查 mint() 函数是否没有引起意料之外的副作用：

• assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to

  这会检查是否只有目标接收者的余额发生了变化，而所有其他账户均不受影响。如果在 mint 调用之后某个账户的余额发生了变化，那么该账户必定是接收者（to）。如果某个账户的余额没有变化，则该账户不是接收者，因此不受 mint 调用的影响。

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

  这会检查是否只有被铸造代币的所有权发生变更，而所有其他代币均不受影响。如果在 mint 调用之后某个代币的所有者发生了变化，那么该代币必定是新铸造的代币。如果某个代币的所有者没有改变，那么该代币不是新铸造的代币，因此其所有权不受 mint 调用的影响。

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

现在，以下是完整的规范，其中包含了 mint 规则、definition、ghost 和 hook：

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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: mint behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule mint(env e, address to, uint256 tokenId) {
    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);

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

这里是 Prover 的运行结果。

形式化验证 burn

burn（销毁）操作执行与 mint 相反的状态变更。

在进行铸造（minting）时，状态变更如下：

• _supply 增加 1
• balanceOf(to) 增加 1
• ownerOf(tokenId) 从先前的值 address(0) 更改为非零地址

在进行销毁（burning）时，情况正好相反：

• _supply 减少 1
• balanceOf(from) 减少 1
• ownerOf(tokenId) 从先前的非零地址变回 address(0)

与 mint 期间代币被新创建且不存在授权（approvals）的情况不同，burn 操作必须清除任何现存的授权，作为重置代币状态的一部分。

考虑到这些行为，我们对其进行形式化验证以确保：

• 当且仅当代币存在时（即所有者不是 address(0)），它不会发生 revert
• 如果调用成功，总供应量减少一，前任所有者的余额减少一
• 所有者被设置为 address(0)，这意味着该代币没有所有者
• 代币的授权被清除
• 没有其他账户的余额、代币所有权或授权发生改变

以下是证明这些属性的 CVL 规则：

Copy
// ERC721.spec -- burn (explanation follows) 

rule burn(env e, uint256 tokenId) {
	// preconditions
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);
    
    // pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    burn@withrevert(e, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

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

前置条件（Preconditions）

与 mint 规则一样，该规则是不可支付的（non-payable）。因此，require nonpayable(e) 是必不可少的：

Copy
require nonpayable(e);
...

记录调用前状态 —— burn 调用前的总供应量、余额、所有权和授权

在 mint 规则中记录的所有调用前状态也出现在 burn 规则中，除了以下内容：

• uint256 balanceOfFromBefore = balanceOf(from)

  burn 规则不记录 mint 接收者的调用前状态（balanceOf(to)），而是记录所有者的余额（balanceOf(from)），以验证在 burn 调用结束时，余额是否减少了 1。

• address otherApprovalBefore = unsafeGetApproved(otherTokenId)

  在 burn 函数中处理授权是必要的；因此，它记录了任意其他代币的授权状态，以验证其保持不变。

Burn 调用（Burn call）

与之前的规则一样，该调用使用了 @withrevert 标签。布尔值 success 捕获了调用是否未发生 revert (!lastReverted)，该值用于验证调用前状态与调用后状态之间的预期变更：

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

断言（Assertions）—— liveness、effect 以及 no side effect

此处检索的所有值都是要与调用前状态进行比较的调用后状态：

Copy
// liveness
assert success <=> (
    ownerBefore != 0
);

// effect
assert success => (
    unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
    to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
    unsafeOwnerOf(tokenId)      == 0 &&
    unsafeGetApproved(tokenId)  == 0
);

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

Liveness（活性）:

它断言当且仅当被销毁的 tokenId 有一个所有者时，burn 调用才不会发生 revert。

Effect（效果）:

如果 burn 调用没有发生 revert，这意味着以下所有的状态变更一定发生了：

• unsafeOwnerOf(tokenId) != 0 => (_supply == supplyBefore - 1)

  如果代币被铸造（有一个非零所有者），那么供应量刚好减少 1。这意味着仅当至少存在一个已铸造的代币时，才会检查供应量的减少情况。

• to_mathint(balanceOf(from)) == balanceOfFromBefore - 1

  from 地址（代币所有者）的余额减少了 1。

• unsafeOwnerOf(tokenId) == 0

  该代币的所有权已被清除，因此 unsafeOwnerOf(tokenId) 返回 0。

• unsafeGetApproved(tokenId) == 0

  该代币的所有现存授权均已被移除，因此 unsafeGetApproved(tokenId) 返回 0。

No side effect（无副作用）:

• assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == from

  这会检查是否只有销毁前所有者的余额发生了变化，而所有其他账户均不受影响。如果在 burn 调用之后某个账户的余额发生了变化，那么该账户必定是销毁前所有者。

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

  这会检查是否只有被销毁代币的所有权发生变更，而所有其他代币均不受影响。如果在 burn 调用之后某个代币的所有者发生了变化，那么该代币必定是被销毁的代币。

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

  这会检查是否只有被销毁代币的授权被清除，而所有其他代币的授权均不受影响。如果在 burn 调用之后某个代币的授权发生了变化，那么该代币必定是被销毁的代币。

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

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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: burn behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule burn(env e, uint256 tokenId) {
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);

    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

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

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

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

注意：代码行 requireInvariant ownerHasBalance(tokenId) 被注释掉了，因为 Prover 8.3.1 报告违反了该 invariant，因此它不能应用于本规范中。这就导致需要将“effect”断言从 _supply == supplyBefore - 1 调整为 unsafeOwnerOf(tokenId) != 0 => (_supply == supplyBefore - 1)。所有的 invariants（包括 ownerHasBalance(tokenId)），都将在下一章中讨论。

这里是 burn 规则的 Prover 运行结果。

mint 和 burn 的完整规范

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

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