ERC-721 的部分参数化规则

RareSkills
发布于 2026-02-14 22:58
阅读 24

本文详细介绍了如何使用 Certora 的部分参数化规则对 ERC-721 代币的五个关键状态变化（总供应量、账户余额、所有权、单一代币批准和操作员批准）进行形式化验证。文章解释了部分参数化规则的设计模式，通过 helperSoundFnCall() 函数实现方法特定逻辑和前置条件，并对比了其与完全参数化规则的优劣，强调了其在处理不同方法特定约束时的优势。

使用 Certora 进行形式化验证

## ERC-721 的部分参数化规则

[模块 2：不变量、存储Hook、幽灵变量和形式化验证通证不变量、存储Hook、幽灵变量和形式化验证通证](https://rareskills.io/tutorials/certora-book)

最后更新于 2026 年 2 月 13 日

## 引言

本章是 [OpenZeppelin 的 ERC-721 CVL 规范](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/36bf1e46fa811f0f07d38eb9cfbc69a955f300ce/certora/specs/ERC721.spec) 代码演练的最后一部分（5/5），该规范形式化验证了以下规则：

- `supplyChange`

总供应量仅通过铸造（mint）或销毁（burn）操作改变，且每次改变精确为一。

- `balanceChange`

账户余额仅通过铸造、销毁或转移（transfer）操作改变，且每次改变精确为一。

- `ownershipChange`

通证所有权仅通过铸造、销毁或转移操作改变。

- `approvalChange`

单通证授权仅通过 `approve()` 调用或作为销毁或转移操作的副作用而改变。

- `approvedForAllChange`

操作员授权仅通过 `setApprovalForAll()` 调用改变。

这些规则使用了部分参数化规则模式（将在下一节讨论），该模式建立在“参数化规则简介”章节中介绍的参数化规则概念之上。

本章中的属性与前几章中的不同。之前，我们验证了特定的方法行为：`mint()` 是否增加了总供应量？`transferFrom()` 是否按预期更新了余额？这些属性使用普通的（非参数化）规则测试了单个方法。

**这里的属性提出了一个不同的问题：哪些** **方法** **可以改变特定的** **状态** **（例如总供应量或账户余额），我们能否确认没有其他方法可以做到？** 普通规则无法回答这个问题，因为它们一次只测试一个方法。即使每个属性的每个方法都有一个规则，我们也无法验证未列出的方法不会引起变化。

有人可能会问 CVL invariants 是否可以达到相同的目的。然而，CVL invariants 在这里并不适用，因为它们无法捕获值在方法调用前后如何变化。Invariants 无法访问调用前的值或将其与调用后的值进行比较，因此它们无法表达“此状态只能在特定方法被调用时改变”或“此状态精确地改变了这么多量”等属性。这些是状态转换属性，需要推理调用前和调用后的状态。

参数化模式通过在单个规则中测试所有合约方法并推理调用前和调用后的状态来解决这个问题。这使得验证哪些方法被允许改变状态以及没有其他方法可以引起相同的改变成为可能。

## 部分参数化规则

在之前的章节“参数化规则简介”中，我们了解到：

> _“...参数化规则验证了在调用任何函数并传入任何有效参数后，某个属性仍然成立。”_

关键短语是：“_在调用任何函数并传入任何有效参数后_”，这对应于以下代码模式：

```solidity
Copyrule parametricExample(env e, method f, calldataarg args) {
    /// set precondition
    // 设置前置条件

/// record pre-call state
	// 记录调用前状态

/// parametric call: invokes all functions in the scene with arbitrary arguments
    // 参数化调用：以任意参数调用场景中的所有函数
    f(e, args);

/// record post-call state
    // 记录调用后状态

/// assertions
    // 断言

}
```

这种模式（完全参数化）在所有方法都适用相同前置条件时效果良好。然而，当不同方法需要不同约束时，它就不适用了。

我们不使用完全参数化的 `$f(e, args)$`，而是可以使用“部分参数化”模式。这并非 CVL 语法，而是一种规范设计模式。正如 [Certora 文档](https://docs.certora.com/en/latest/docs/user-guide/patterns/partial-apply.html#partially-parametric-rules) 所述：

> _“这种部分参数化规则演示了基于所调用方法的类型的条件逻辑，允许在智能合约中针对不同场景进行特定操作和断言。”_

关键短语是“_针对不同场景的特定操作和断言_”，这对应于以下代码模式：

```solidity
Copyrule partiallyParametricExample(env e) {
	method f;

if (f.selector == sig:exampleMethod1(uint256, address).selector) {
			// method-specific logic
			// 方法特定逻辑
	}
	else if (f.selector == sig:exampleMethod2(address, address).selector) {
			// method-specific logic
			// 方法特定逻辑
	}
	else {
			// method-specific logic
			// 方法特定逻辑
	}
}
```

方法特定逻辑可以是前置条件、方法调用，甚至是断言。为了代码更简洁，这些条件语句可以抽象到一个 CVL 函数中，如下所示：

```solidity
Copyrule partiallyParametricExample(env e) {
	method f;
	helperFunction(e, f); // contains all conditional logic
	// helperFunction(e, f); // 包含所有条件逻辑
}
```

OpenZeppelin 的规范使用辅助函数 `helperSoundFnCall()` 来实现这种模式。以下是 `supplyChange` 规则的一个示例（我们稍后将详细研究）：

```solidity
Copy/// ERC721.spec

rule supplyChange(env e) {
    ...
    method f; helperSoundFnCall(e, f);
    ...

/// assert
    // 断言
    /// assert
    // 断言
}
```

`helperSoundFnCall()` 中的“Sound”是刻意为之的。Soundness 意味着验证不会遗漏任何实际错误，而 unsoundness 的一个常见来源是由于过于严格的前置条件而排除了有效的执行路径。

该辅助函数通过根据所调用的方法选择性地应用前置条件，而不是全局地应用于所有调用，从而以 sound 的方式路由 `$f(e, args)$`。将前置条件应用于不需要它的方法会排除有效的执行路径。

在下一节中，我们将看到任意方法调用 `$f(e, args)$` 如何被路由到适当的方法特定前置条件，从而保持规范的 soundness。

## `helperSoundFnCall()` 将 `$f(e, args)$` 调用路由到正确的方法分支

CVL 函数 `helperSoundFnCall()` 通过匹配函数选择器将任意方法调用 `$f(e, args)$` 路由到正确的方法分支。对于每个匹配的选择器，CVL 辅助函数执行以下操作：

- 声明所需的参数，
- 应用方法特定的前置条件，以及
- 调用相应的具体函数。

### 对于铸造操作 — `mint()`、`safeMint()` 和 `safeMint(bytes)`

当调用的函数是 mint 变体时，辅助函数：

- 声明所需的参数：`address to`、`uint256 tokenId`，对于 bytes 变体，还有 `bytes data`。
- 应用方法特定的前置条件：
  - `require balanceLimited(to)` — 将接收方的余额约束在 `$max\_uint256$` 以下，以防止溢出。
  - `require data.length < 0xffff` — 将数据长度限制在 65,535 字节 `$(0xffff)$` 以下，以避免 Prover 执行期间出现不切实际的大数组。
- 调用相应的函数：`mint(e, to, tokenId)`、`safeMint(e, to, tokenId)` 或 `safeMint(e, to, tokenId, data)`。

### 对于销毁操作 — `burn()`

当调用的函数是 `burn()` 时，辅助函数：

- 声明所需的参数 `uint256 tokenId`。

- 应用方法特定的前置条件 `requireInvariant ownerHasBalance(tokenId)`，要求通证在销毁前存在（具有非零所有者）。

- 调用相应的函数 `burn(e, tokenId)`。

```javascript
Copyfunction helperSoundFnCall(env e, method f) {
      ...
      } else if (f.selector == sig:burn(uint256).selector) {
          uint256 tokenId;
          requireInvariant ownerHasBalance(tokenId);
          // requireInvariant notMintedUnset(tokenId);
          burn(e, tokenId);
      }
  	...
}
```

### 对于转移操作 — `transferFrom()`、`safeTransferFrom()` 和 `safeTransferFrom(bytes)`

当调用的函数是 transfer 变体时，辅助函数：

- 声明所需的参数：`address from`、`address to`、`uint256 tokenId`，对于 bytes 变体，还有 `bytes data`。
- 应用方法特定的前置条件：
  - `require balanceLimited(to)` — 将接收方的余额约束为严格小于 `$max\_uint256$`，以防止 Prover 探索不切实际的接收方余额。
  - `requireInvariant ownerHasBalance(tokenId)` — 确保通证在可以转移之前存在。如果没有这个条件，Prover 将考虑通证从零地址转移的情况。
  - `requireInvariant notMintedUnset(tokenId)` — 排除了对未铸造通证的任何授权。如果没有这个条件，Prover 会将不存在的通证视为拥有已授权的操作员。
  - `require data.length < 0xffff` —（仅限 bytes 变体）将数据长度限制在 65,535 字节 `$(0xffff)$` 以下，以避免 Prover 执行期间出现不切实际的大数组。
- 调用相应的函数：`transferFrom()`、`safeTransferFrom()`、`safeTransferFrom(bytes)`。

```solidity
Copyfunction helperSoundFnCall(env e, method f) {
    ...
    } else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        transferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        address from; address to; uint256 tokenId; bytes data;
        require data.length < 0xffff;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId, data);
		...
}
```

### 对于除铸造、销毁和转移之外的所有操作

除铸造、销毁或转移之外的函数通过带有任意参数的完全参数化调用 `$f(e, args)$` 进行处理：

```solidity
Copyfunction helperSoundFnCall(env e, method f) {
    ...
    } else {
        calldataarg args;
        f(e, args);
    }
}
```

### CVL 函数 `helperSoundFnCall()` 的完整实现

以下是完整的辅助 CVL 函数：

```solidity
Copyfunction helperSoundFnCall(env e, method f) {
    if (f.selector == sig:mint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        mint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        address to; uint256 tokenId; bytes data;
        require data.length < 0xffff;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId, data);
    } else if (f.selector == sig:burn(uint256).selector) {
        uint256 tokenId;
        requireInvariant ownerHasBalance(tokenId);
        // requireInvariant notMintedUnset(tokenId);
        burn(e, tokenId);
    } else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        transferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        address from; address to; uint256 tokenId; bytes data;
        require data.length < 0xffff;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId, data);
    } else {
        calldataarg args;
        f(e, args);
    }
}
```

_注意：在铸造（mint）和销毁（burn）分支中，我们_ _注释掉了_ _`requireInvariant notMintedUnset(tokenId)`_ _，以仅显示每个被调用方法严格必要的前置条件。_ _这并不意味着该不变量无用——因为它在规范中作为单独的不变量被证明，所以可以假设它始终成立并安全地恢复。将其添加为前置条件通常会缩短 Prover 的运行时间。_

通过 `helperSoundFnCall()` 中处理的方法特定前置条件，我们可以进入下一节的规则讨论。

## `supplyChange` — 总供应量只能通过 `mint()`、`safeMint()`、`safeMint(bytes)` 和 `burn()` 改变

此规则验证哪些合约方法可以将总供应量增加或减少 1。以下是捕获此行为的规则，我们将在接下来详细讨论：

```solidity
Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn                                                           │
│ 规则：总供应量只能通过铸造和销毁改变                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

mathint supplyBefore = _supply;
    method f; helperSoundFnCall(e, f);
    mathint supplyAfter = _supply;

assert supplyAfter > supplyBefore => (
        supplyAfter == supplyBefore + 1 &&
        (
            f.selector == sig:mint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256,bytes).selector
        )
    );
    assert supplyAfter < supplyBefore => (
        supplyAfter == supplyBefore - 1 &&
        f.selector == sig:burn(uint256).selector
    );
}
```

Prover 运行：[链接](https://prover.certora.com/output/541734/cf14580f393e40f4ac4d838512c694fc?anonymousKey=405189efeaabcd309a577f256c9011ff757f9e09)

### **前置条件**

- `require nonzerosender(e)`

此**前置条件**限制调用者为非零地址。如果没有此约束，Prover 可以探索从 `address(0)` 发起并将通证转移到非零地址的执行，这实际上是通过转移操作执行的铸造。

- `requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)`

此**不变量前置条件**阻止 `address(0)` 批准操作员。如果没有此约束，Prover 可以探索 `address(0)` 已授予非零地址操作员权限的状态。

### **调用前和调用后状态**

- `supplyBefore = _supply`

记录执行部分参数化调用（`method f; helperSoundFnCall(e, f)`）前的总供应量。

- `method f; helperSoundFnCall(e, f)`

执行前面讨论的部分参数化调用。

- `mathint supplyAfter = _supply`

记录执行部分参数化调用后的总供应量。

```solidity
Copymathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
```

ERC-721 不跟踪总供应量，因此我们使用一个**幽灵变量** `_supply`，它通过 `Sstore` Hook跟踪所有 `_balances` 的总和：

```solidity
Copyghost mathint _supply {
    init_state axiom _supply == 0;
}

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

### **断言**

- 第一个**断言**表明，如果总供应量增加（`$supplyAfter > supplyBefore$`），则增加量必须恰好为 1，并且只能由 `mint()`、`safeMint()` 或 `safeMint(bytes)` 引起：

```solidity
Copyrule supplyChange(env e) {
      ...
      assert $supplyAfter > supplyBefore$ => (
          $supplyAfter == supplyBefore + 1$ &&
          (
              f.selector == sig:mint(address,uint256).selector ||
              f.selector == sig:safeMint(address,uint256).selector ||
              f.selector == sig:safeMint(address,uint256,bytes).selector
          )
      );
      ...
}
```

- 第二个**断言**涵盖了销毁情况。如果总供应量减少（`$supplyAfter < supplyBefore$`），则减少量必须恰好为 1，并且只能由 `burn()` 引起：

```solidity
Copyrule supplyChange(env e) {
      ...
      assert $supplyAfter < supplyBefore$ => (
          $supplyAfter == supplyBefore - 1$ &&
          f.selector == sig:burn(uint256).selector
      );
}
```

## `balanceChange` — 账户余额只能通过铸造、销毁和转移操作改变

以下规则验证了关于余额变化的两个属性：

- 每次操作的余额精确改变一个通证
- 只有铸造、销毁或转移操作才能改变余额

```solidity
Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
│ 规则：balanceOf 只能通过铸造、销毁或转移改变。balanceOf 每次改变不能超过 1。                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {

// requireInvariant balanceOfConsistency(account);
    // require balanceLimited(account);

mathint balanceBefore = balanceOf(account);
    method f; helperSoundFnCall(e, f);
    mathint balanceAfter  = balanceOf(account);

// balance can change by at most 1
    // 余额最多改变 1
    assert balanceBefore != balanceAfter => (
        balanceAfter == balanceBefore - 1 ||
        balanceAfter == balanceBefore + 1
    );

// only selected function can change balances
    // 只有选定的函数可以改变余额
    assert balanceBefore != balanceAfter => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector ||
        f.selector == sig:burn(uint256).selector
    );
}
```

Prover 运行：[链接](https://prover.certora.com/output/541734/9dafe73bd99b4fd5a4aae5d797fe2db2?anonymousKey=92578204ddacb27b80cb4762ddcb75fa49762601)

### 前置条件

`requireInvariant balanceOfConsistency(account)` 和 `require balanceLimited(account)` 被注释掉了，因为 `helperSoundFnCall()` 已经对所有改变余额的方法强制执行了这些**前置条件**。`balanceOfConsistency` 通过销毁和转移分支中 `ownerHasBalance` 不变量的保留块强制执行。

### **调用前和调用后状态**

该规则记录了 `helperSoundFnCall(e, f)` 调用前后账户余额，以比较这些值并确定方法调用是否以及改变了多少余额：

```solidity
Copymathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter  = balanceOf(account);
```

### **断言**

第一个**断言**表明，如果账户余额在 `helperSoundFnCall(e, f)` 调用后发生变化（`$balanceBefore \neq balanceAfter$`），则变化量必须为正负一——不多也不少。

```solidity
Copy// balance can change by at most 1
// 余额最多改变 1
assert $balanceBefore \neq balanceAfter$ => (
    $balanceAfter == balanceBefore - 1$ ||
    $balanceAfter == balanceBefore + 1$
);
```

第二个**断言**表明，只有以下函数可以改变余额：

- 铸造函数（`mint()`、`safeMint()`、`safeMint(bytes)`）
- 销毁（`burn()`）
- 转移函数（`transferFrom()`、`safeTransferFrom()`、`safeTransferFrom(bytes)`）

```solidity
Copy// only selected function can change balances
// 只有选定的函数可以改变余额
assert $balanceBefore \neq balanceAfter$ => (
    f.selector == sig:transferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
    f.selector == sig:mint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector ||
    f.selector == sig:burn(uint256).selector
);
```

如果任何其他未列出的函数导致余额变化，则**断言**将失败，Prover 将报告违规。

## `ownershipChange()` — 所有权只能通过铸造、销毁和转移操作改变

以下规则验证了通证的所有权（`ownerOf(tokenId)`）只能通过铸造、销毁或转移操作改变。操作类型取决于所有者地址如何变化：

- 从零地址到非零地址——表示铸造，只能由 `mint()`、`safeMint()` 或 `safeMint(bytes)` 引起。
- 从非零地址到零地址——表示销毁，只能由 `burn()` 引起。
- 从一个非零地址到另一个非零地址——表示转移，只能由 `transferFrom()`、`safeTransferFrom()` 或 `safeTransferFrom(bytes)` 引起。

```solidity
Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers.                                                   │
│ 规则：所有权只能通过铸造、销毁或转移改变。                                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

address ownerBefore = unsafeOwnerOf(tokenId);
    method f; helperSoundFnCall(e, f);
    address ownerAfter  = unsafeOwnerOf(tokenId);

assert ownerBefore == 0 && ownerAfter != 0 => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector
    );

assert ownerBefore != 0 && ownerAfter == 0 => (
        f.selector == sig:burn(uint256).selector
    );

assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
    );
}
```

Prover 运行：[链接](https://prover.certora.com/output/541734/217a0c2147c34536b99495351133cf56?anonymousKey=4f634a57f4728e3c8a7874f3581400ab56734de2)

### 前置条件

- `require nonzerosender(e)`

此**前置条件**要求调用者（`e.msg.sender`）为非零地址。如果没有它，Prover 可以模拟 `address(0)` 直接调用 `transferFrom` 的执行，这会从 `address(0)` 创建所有权，违反了只有铸造函数才能这样做的规则。

- `requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)`

此**不变量前置条件**阻止零地址批准任何操作员。如果没有它，Prover 可以假设 `address(0)` 批准了一个非零操作员。这允许 `transferFrom(from = address(0), ...)` 即使在调用者是非零地址时也能成功，从而创建从零地址的所有权转移，并违反了只有铸造函数才能创建所有权的规则。

### **调用前和调用后状态**

这些行记录了 `helperSoundFnCall(e, f)` 前后通证的所有者：

```solidity
Copyaddress ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter  = unsafeOwnerOf(tokenId);
```

使用 `unsafeOwnerOf(tokenId)` 允许规则推理所有权变化，即使通证不存在（在这种情况下所有者为 `address(0)`）。

### **断言**

- `assert ownerBefore == 0 && ownerAfter != 0 => (...)`

如果所有权从零地址变为非零地址，意味着发生了铸造，那么只能由以下函数引起：`mint()`、`safeMint()` 或 `safeMint(bytes)`：

```solidity
Copyassert $ownerBefore == 0 \land ownerAfter \neq 0$ => (
  	f.selector == sig:mint(address,uint256).selector ||
  	f.selector == sig:safeMint(address,uint256).selector ||
  	f.selector == sig:safeMint(address,uint256,bytes).selector
);
```

- `assert ownerBefore != 0 && ownerAfter == 0 => (...)`

如果所有权从非零地址变为零地址，意味着发生了销毁，那么只有 `burn()` 函数对此负责：

```solidity
Copyassert $ownerBefore \neq 0 \land ownerAfter == 0$ => (
      f.selector == sig:burn(uint256).selector
);
```

- `assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (...)`

最后，如果变化是从一个非零地址到另一个非零地址，那么发生了转移。只有 `transferFrom()`、`safeTransferFrom()` 和 `safeTransferFrom(bytes)` 对这些变化负责：

```solidity
Copyassert $(ownerBefore \neq ownerAfter \land ownerBefore \neq 0 \land ownerAfter \neq 0)$ => (
      f.selector == sig:transferFrom(address,address,uint256).selector ||
      f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
      f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
);
```

## `approvalChange()` — 授权只能通过 approve、transferFrom 和 burn 函数改变

以下规则验证了特定通证的授权（`getApproved(tokenId)`）只能通过三种方式改变：

- 通过调用 `approve()` 函数直接设置
- 作为转移的副作用重置为 `address(0)`
- 作为销毁的副作用重置为 `address(0)`

```solidity
Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
│ 规则：通证授权只能通过 approve 或转移（隐式）改变。                                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
    address approvalBefore = unsafeGetApproved(tokenId);
    method f; helperSoundFnCall(e, f);
    address approvalAfter  = unsafeGetApproved(tokenId);

// approve can set any value, other functions reset
    // approve 可以设置任何值，其他函数重置
    assert approvalBefore != approvalAfter => (
        f.selector == sig:approve(address,uint256).selector ||
        (
            (
                f.selector == sig:transferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
                f.selector == sig:burn(uint256).selector
            ) && approvalAfter == 0
        )
    );
}
```

Prover 运行：[链接](https://prover.certora.com/output/541734/6b33267777564799a3fe1ebb28ed0626?anonymousKey=ff12144bbac0ee70a140619379a8f7990c092ca7)

### **调用前和调用后状态**

以下行记录了部分参数化调用 `method f; helperSoundFnCall(e, f)` 前后的授权地址，以确定授权是否因列出的被调用方法而改变，以及是否被清除为 `address(0)`：

```solidity
Copyaddress approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter  = unsafeGetApproved(tokenId);
```

### **断言**

此**断言**表明，授权地址的变化只有在以下情况下才能发生：

- 函数调用是 `approve()`，它明确设置了授权地址，或者
- 函数调用是 `transferFrom()`、`safeTransferFrom()`（带或不带 bytes 数据）或 `burn()`，并且授权地址作为副作用被清除为 `address(0)`（`$approvalAfter == 0$`）。

```solidity
Copy// approve can set any value, other functions reset
// approve 可以设置任何值，其他函数重置
assert $approvalBefore \neq approvalAfter$ => (
        f.selector == sig:approve(address,uint256).selector ||
        (
            (
                f.selector == sig:transferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
                f.selector == sig:burn(uint256).selector
            ) && $approvalAfter == 0$
        )
    );
```

如果以下情况发生，则**断言**将失败：

- 未列出的函数清除或修改了授权地址。
- `transferFrom`、`safeTransferFrom` 或 `burn` 未将授权地址清除为 `address(0)`。

## `approvedForAllChange` — 所有通证的授权仅通过 `setApprovalForAll()` 函数改变

此规则验证了**spender**的所有通证授权状态（`isApprovedForAll(owner, spender)`）只能通过显式调用 `setApprovalForAll()` 函数来改变：

```solidity
Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
│ 规则：所有通证的授权只能通过 isApprovedForAll 改变。                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
    bool approvedForAllBefore = isApprovedForAll(owner, spender);
    method f; helperSoundFnCall(e, f);
    bool approvedForAllAfter  = isApprovedForAll(owner, spender);

assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
}
```

Prover 运行：[链接](https://prover.certora.com/output/541734/e4dfd40ef9cf4724b189a084488ee359?anonymousKey=5487cf57e602b3474f064527bceb612654b8e01d)

### **调用前和调用后状态**

- `bool approvedForAllBefore = isApprovedForAll(owner, spender);`

这记录了 `helperSoundFnCall(e, f)` 调用前的所有通证授权状态。

- `bool approvedForAllAfter = isApprovedForAll(owner, spender);`

这记录了 `helperSoundFnCall(e, f)` 调用后的所有通证授权状态。

```solidity
Copybool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter  = isApprovedForAll(owner, spender);
```

### **断言**

如果**spender**的所有通证授权状态发生变化，则唯一的原因是调用了 `setApprovalForAll()`：

```solidity
Copyassert $approvedForAllBefore \neq approvedForAllAfter$ => f.selector == sig:setApprovalForAll(address,bool).selector;
```

与 `approve()` 在转移或销毁时重置不同，`isApprovedForAll` 在铸造、转移或销毁期间不会改变。只有显式调用 `setApprovalForAll` 才能修改它。如果任何其他函数改变此状态，则**断言**失败，Prover 将报告违规。

## 完整规范

以下是部分参数化规则的完整规范：

```solidity
Copymethods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;

function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helper                                                                                                              │
│ 辅助函数                                                                                                            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
│ 幽灵变量与Hook：所有权计数                                                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom _ownedByUser[a] == 0;
}

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
│ 幽灵变量与Hook：余额                                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

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

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

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
│ 不变量：balanceOf 是拥有的通证数量                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];
    // {
    //     preserved {
    //         require balanceLimited(user);
    //     }
    // }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
│ 不变量：通证所有者必须有余额                                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover v8.3.1
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
            // require balanceLimited(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator                                                                    │
│ 不变量：address(0) 没有授权的操作员                                                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
    !isApprovedForAll(0, a)
    {
        preserved with (env e) {
            require nonzerosender(e);
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved                                                  │
│ 不变量：不存在的通证不被拥有且未被授权                                                                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn                                                           │
│ 规则：总供应量只能通过铸造和销毁改变                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

mathint supplyBefore = _supply;
    method f; helperSoundFnCall(e, f);
    mathint supplyAfter = _supply;

assert $supplyAfter > supplyBefore$ => (
        $supplyAfter == supplyBefore + 1$ &&
        (
            f.selector == sig:mint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256,bytes).selector
        )
    );
    assert $supplyAfter < supplyBefore$ => (
        $supplyAfter == supplyBefore - 1$ &&
        f.selector == sig:burn(uint256).selector
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
│ 规则：balanceOf 只能通过铸造、销毁或转移改变。balanceOf 每次改变不能超过 1。                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {
    // requireInvariant balanceOfConsistency(account);
    // require balanceLimited(account);

mathint balanceBefore = balanceOf(account);
    method f; helperSoundFnCall(e, f);
    mathint balanceAfter  = balanceOf(account);

// balance can change by at most 1
    // 余额最多改变 1
    assert $balanceBefore \neq balanceAfter$ => (
        $balanceAfter == balanceBefore - 1$ ||
        $balanceAfter == balanceBefore + 1$
    );

// only selected function can change balances
    // 只有选定的函数可以改变余额
    assert $balanceBefore \neq balanceAfter$ => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector ||
        f.selector == sig:burn(uint256).selector
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers.                                                   │
│ 规则：所有权只能通过铸造、销毁或转移改变。                                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

address ownerBefore = unsafeOwnerOf(tokenId);
    method f; helperSoundFnCall(e, f);
    address ownerAfter  = unsafeOwnerOf(tokenId);

assert $ownerBefore == 0 \land ownerAfter \neq 0$ => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector
    );

assert $ownerBefore \neq 0 \land ownerAfter == 0$ => (
        f.selector == sig:burn(uint256).selector
    );

assert $(ownerBefore \neq ownerAfter \land ownerBefore \neq 0 \land ownerAfter \neq 0)$ => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
│ 规则：通证授权只能通过 approve 或转移（隐式）改变。                                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
    address approvalBefore = unsafeGetApproved(tokenId);
    method f; helperSoundFnCall(e, f);
    address approvalAfter  = unsafeGetApproved(tokenId);

// approve can set any value, other functions reset
    // approve 可以设置任何值，其他函数重置
    assert $approvalBefore \neq approvalAfter$ => (
        f.selector == sig:approve(address,uint256).selector ||
        (
            (
                f.selector == sig:transferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
                f.selector == sig:burn(uint256).selector
            ) && $approvalAfter == 0$
        )
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
│ 规则：所有通证的授权只能通过 isApprovedForAll 改变。                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
    bool approvedForAllBefore = isApprovedForAll(owner, spender);
    method f; helperSoundFnCall(e, f);
    bool approvedForAllAfter  = isApprovedForAll(owner, spender);

assert $approvedForAllBefore \neq approvedForAllAfter$ => f.selector == sig:setApprovalForAll(address,bool).selector;
}
```

Prover 运行：[链接](https://prover.certora.com/output/541734/bd307ec517f248db809a17a626ab9ff7?anonymousKey=752eb5544863170f99831d7d02fc22f144d9463e)

## 关于部分参数化规则与完全参数化规则区别的说明

这些状态变化属性可以通过单个部分参数化规则或多个完全参数化规则（每个属性一个）进行验证。两种方法都使用 `method f` 来推理所有合约方法的状态变化，但它们在前置条件范围界定方式上有所不同。

在完全参数化规则中，所有前置条件都在规则级别应用，因此约束了所有可能的**方法调用**。当验证状态时，所有影响该状态的方法都适用相同的前置条件时，这种方法效果良好。

另一方面，部分参数化规则使用基于被调用方法的条件逻辑。它不是将前置条件应用于所有**方法调用**，而是将任意方法调用路由到方法特定的分支，每个分支都有其自身相关的**前置条件**。前置条件仅在需要时才适用，当规则验证需要不同方法特定约束的多个断言时，这种方法效果良好。

它们之间的选择主要是关于代码组织：部分参数化规则集中了方法特定逻辑，而完全参数化规则将关注点分离到独立的规则中。这种组织差异影响了可维护性和清晰度，但当**前置条件**得到正确限定时，两种方法都同样有效。

_本文是关于 [使用 Certora Prover 进行形式化验证](https://rareskills.io/tutorials/certora-book) 系列文章的一部分。_

>- 原文链接： [rareskills.io/post/certo...](https://rareskills.io/post/certora-partially-parametric-rules-erc-721)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

使用 Certora 进行形式化验证

ERC-721 的部分参数化规则

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

最后更新于 2026 年 2 月 13 日

引言

本章是 OpenZeppelin 的 ERC-721 CVL 规范代码演练的最后一部分（5/5），该规范形式化验证了以下规则：

supplyChange

总供应量仅通过铸造（mint）或销毁（burn）操作改变，且每次改变精确为一。

balanceChange

账户余额仅通过铸造、销毁或转移（transfer）操作改变，且每次改变精确为一。

ownershipChange

通证所有权仅通过铸造、销毁或转移操作改变。

approvalChange

单通证授权仅通过 approve() 调用或作为销毁或转移操作的副作用而改变。

approvedForAllChange

操作员授权仅通过 setApprovalForAll() 调用改变。

这些规则使用了部分参数化规则模式（将在下一节讨论），该模式建立在“参数化规则简介”章节中介绍的参数化规则概念之上。

本章中的属性与前几章中的不同。之前，我们验证了特定的方法行为：mint() 是否增加了总供应量？transferFrom() 是否按预期更新了余额？这些属性使用普通的（非参数化）规则测试了单个方法。

这里的属性提出了一个不同的问题：哪些 方法 可以改变特定的 状态 （例如总供应量或账户余额），我们能否确认没有其他方法可以做到？ 普通规则无法回答这个问题，因为它们一次只测试一个方法。即使每个属性的每个方法都有一个规则，我们也无法验证未列出的方法不会引起变化。

部分参数化规则

在之前的章节“参数化规则简介”中，我们了解到：

“...参数化规则验证了在调用任何函数并传入任何有效参数后，某个属性仍然成立。”

关键短语是：“在调用任何函数并传入任何有效参数后”，这对应于以下代码模式：

Copyrule parametricExample(env e, method f, calldataarg args) {
    /// set precondition
    // 设置前置条件

    /// record pre-call state
    // 记录调用前状态

    /// parametric call: invokes all functions in the scene with arbitrary arguments
    // 参数化调用：以任意参数调用场景中的所有函数
    f(e, args);

    /// record post-call state
    // 记录调用后状态

    /// assertions
    // 断言

}

这种模式（完全参数化）在所有方法都适用相同前置条件时效果良好。然而，当不同方法需要不同约束时，它就不适用了。

我们不使用完全参数化的 $f(e, args)$ ，而是可以使用“部分参数化”模式。这并非 CVL 语法，而是一种规范设计模式。正如 Certora 文档所述：

“这种部分参数化规则演示了基于所调用方法的类型的条件逻辑，允许在智能合约中针对不同场景进行特定操作和断言。”

关键短语是“针对不同场景的特定操作和断言”，这对应于以下代码模式：

Copyrule partiallyParametricExample(env e) {
    method f;

    if (f.selector == sig:exampleMethod1(uint256, address).selector) {
            // method-specific logic
            // 方法特定逻辑
    }
    else if (f.selector == sig:exampleMethod2(address, address).selector) {
            // method-specific logic
            // 方法特定逻辑
    }
    else {
            // method-specific logic
            // 方法特定逻辑
    }
}

方法特定逻辑可以是前置条件、方法调用，甚至是断言。为了代码更简洁，这些条件语句可以抽象到一个 CVL 函数中，如下所示：

Copyrule partiallyParametricExample(env e) {
    method f;
    helperFunction(e, f); // contains all conditional logic
    // helperFunction(e, f); // 包含所有条件逻辑
}

OpenZeppelin 的规范使用辅助函数 helperSoundFnCall() 来实现这种模式。以下是 supplyChange 规则的一个示例（我们稍后将详细研究）：

Copy/// ERC721.spec

rule supplyChange(env e) {
    ...
    method f; helperSoundFnCall(e, f);
    ...

    /// assert
    // 断言
    /// assert
    // 断言
}

helperSoundFnCall() 中的“Sound”是刻意为之的。Soundness 意味着验证不会遗漏任何实际错误，而 unsoundness 的一个常见来源是由于过于严格的前置条件而排除了有效的执行路径。

该辅助函数通过根据所调用的方法选择性地应用前置条件，而不是全局地应用于所有调用，从而以 sound 的方式路由 $f(e, args)$ 。将前置条件应用于不需要它的方法会排除有效的执行路径。

在下一节中，我们将看到任意方法调用 $f(e, args)$ 如何被路由到适当的方法特定前置条件，从而保持规范的 soundness。

`helperSoundFnCall()` 将 $f(e, args)$ 调用路由到正确的方法分支

CVL 函数 helperSoundFnCall() 通过匹配函数选择器将任意方法调用 $f(e, args)$ 路由到正确的方法分支。对于每个匹配的选择器，CVL 辅助函数执行以下操作：

声明所需的参数，
应用方法特定的前置条件，以及
调用相应的具体函数。

对于铸造操作 — `mint()`、`safeMint()` 和 `safeMint(bytes)`

当调用的函数是 mint 变体时，辅助函数：

声明所需的参数：address to、uint256 tokenId，对于 bytes 变体，还有 bytes data。
应用方法特定的前置条件：
- require balanceLimited(to) — 将接收方的余额约束在 $max\_uint256$ 以下，以防止溢出。
- require data.length < 0xffff — 将数据长度限制在 65,535 字节 $(0xffff)$ 以下，以避免 Prover 执行期间出现不切实际的大数组。
调用相应的函数：mint(e, to, tokenId)、safeMint(e, to, tokenId) 或 safeMint(e, to, tokenId, data)。

Copyfunction helperSoundFnCall(env e, method f) {
    if (f.selector == sig:mint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        mint(e, to, tokenId);
    }
    else if (f.selector == sig:safeMint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId);
    }
    else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        address to; uint256 tokenId; bytes data;
        require data.length &lt; 0xffff;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId, data);
    }
        ...
}

对于销毁操作 — `burn()`

当调用的函数是 burn() 时，辅助函数：

声明所需的参数 uint256 tokenId。
应用方法特定的前置条件 requireInvariant ownerHasBalance(tokenId)，要求通证在销毁前存在（具有非零所有者）。
调用相应的函数 burn(e, tokenId)。

Copyfunction helperSoundFnCall(env e, method f) {
      ...
      } else if (f.selector == sig:burn(uint256).selector) {
          uint256 tokenId;
          requireInvariant ownerHasBalance(tokenId);
          // requireInvariant notMintedUnset(tokenId);
          burn(e, tokenId);
      }
    ...
}

对于转移操作 — `transferFrom()`、`safeTransferFrom()` 和 `safeTransferFrom(bytes)`

当调用的函数是 transfer 变体时，辅助函数：

声明所需的参数：address from、address to、uint256 tokenId，对于 bytes 变体，还有 bytes data。
应用方法特定的前置条件：
- require balanceLimited(to) — 将接收方的余额约束为严格小于 $max\_uint256$ ，以防止 Prover 探索不切实际的接收方余额。
- requireInvariant ownerHasBalance(tokenId) — 确保通证在可以转移之前存在。如果没有这个条件，Prover 将考虑通证从零地址转移的情况。
- requireInvariant notMintedUnset(tokenId) — 排除了对未铸造通证的任何授权。如果没有这个条件，Prover 会将不存在的通证视为拥有已授权的操作员。
- require data.length < 0xffff —（仅限 bytes 变体）将数据长度限制在 65,535 字节 $(0xffff)$ 以下，以避免 Prover 执行期间出现不切实际的大数组。
调用相应的函数：transferFrom()、safeTransferFrom()、safeTransferFrom(bytes)。

Copyfunction helperSoundFnCall(env e, method f) {
    ...
    } else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        transferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        address from; address to; uint256 tokenId; bytes data;
        require data.length &lt; 0xffff;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId, data);
        ...
}

对于除铸造、销毁和转移之外的所有操作

除铸造、销毁或转移之外的函数通过带有任意参数的完全参数化调用 $f(e, args)$ 进行处理：

Copyfunction helperSoundFnCall(env e, method f) {
    ...
    } else {
        calldataarg args;
        f(e, args);
    }
}

CVL 函数 `helperSoundFnCall()` 的完整实现

以下是完整的辅助 CVL 函数：

Copyfunction helperSoundFnCall(env e, method f) {
    if (f.selector == sig:mint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        mint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        address to; uint256 tokenId; bytes data;
        require data.length &lt; 0xffff;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId, data);
    } else if (f.selector == sig:burn(uint256).selector) {
        uint256 tokenId;
        requireInvariant ownerHasBalance(tokenId);
        // requireInvariant notMintedUnset(tokenId);
        burn(e, tokenId);
    } else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        transferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        address from; address to; uint256 tokenId; bytes data;
        require data.length &lt; 0xffff;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId, data);
    } else {
        calldataarg args;
        f(e, args);
    }
}

注意：在铸造（mint）和销毁（burn）分支中，我们 注释掉了 requireInvariant notMintedUnset(tokenId) ，以仅显示每个被调用方法严格必要的前置条件。 这并不意味着该不变量无用——因为它在规范中作为单独的不变量被证明，所以可以假设它始终成立并安全地恢复。将其添加为前置条件通常会缩短 Prover 的运行时间。

通过 helperSoundFnCall() 中处理的方法特定前置条件，我们可以进入下一节的规则讨论。

`supplyChange` — 总供应量只能通过 `mint()`、`safeMint()`、`safeMint(bytes)` 和 `burn()` 改变

此规则验证哪些合约方法可以将总供应量增加或减少 1。以下是捕获此行为的规则，我们将在接下来详细讨论：

Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn                                                           │
│ 规则：总供应量只能通过铸造和销毁改变                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

    mathint supplyBefore = _supply;
    method f; helperSoundFnCall(e, f);
    mathint supplyAfter = _supply;

    assert supplyAfter > supplyBefore => (
        supplyAfter == supplyBefore + 1 &&
        (
            f.selector == sig:mint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256,bytes).selector
        )
    );
    assert supplyAfter &lt; supplyBefore => (
        supplyAfter == supplyBefore - 1 &&
        f.selector == sig:burn(uint256).selector
    );
}

Prover 运行：链接

前置条件

require nonzerosender(e)

此前置条件限制调用者为非零地址。如果没有此约束，Prover 可以探索从 address(0) 发起并将通证转移到非零地址的执行，这实际上是通过转移操作执行的铸造。

requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)

此不变量前置条件阻止 address(0) 批准操作员。如果没有此约束，Prover 可以探索 address(0) 已授予非零地址操作员权限的状态。

调用前和调用后状态

supplyBefore = _supply

记录执行部分参数化调用（method f; helperSoundFnCall(e, f)）前的总供应量。

method f; helperSoundFnCall(e, f)

执行前面讨论的部分参数化调用。

mathint supplyAfter = _supply

记录执行部分参数化调用后的总供应量。

Copymathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;

ERC-721 不跟踪总供应量，因此我们使用一个幽灵变量 _supply，它通过 Sstore Hook跟踪所有 _balances 的总和：

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

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

断言

第一个断言表明，如果总供应量增加（ $supplyAfter > supplyBefore$ ），则增加量必须恰好为 1，并且只能由 mint()、safeMint() 或 safeMint(bytes) 引起：

Copyrule supplyChange(env e) {
      ...
      assert $supplyAfter > supplyBefore$ => (
          $supplyAfter == supplyBefore + 1$ &&
          (
              f.selector == sig:mint(address,uint256).selector ||
              f.selector == sig:safeMint(address,uint256).selector ||
              f.selector == sig:safeMint(address,uint256,bytes).selector
          )
      );
      ...
}

第二个断言涵盖了销毁情况。如果总供应量减少（ $supplyAfter < supplyBefore$ ），则减少量必须恰好为 1，并且只能由 burn() 引起：

Copyrule supplyChange(env e) {
      ...
      assert $supplyAfter &lt; supplyBefore$ => (
          $supplyAfter == supplyBefore - 1$ &&
          f.selector == sig:burn(uint256).selector
      );
}

`balanceChange` — 账户余额只能通过铸造、销毁和转移操作改变

以下规则验证了关于余额变化的两个属性：

每次操作的余额精确改变一个通证
只有铸造、销毁或转移操作才能改变余额

Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
│ 规则：balanceOf 只能通过铸造、销毁或转移改变。balanceOf 每次改变不能超过 1。                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {

 // requireInvariant balanceOfConsistency(account);
    // require balanceLimited(account);

    mathint balanceBefore = balanceOf(account);
    method f; helperSoundFnCall(e, f);
    mathint balanceAfter  = balanceOf(account);

    // balance can change by at most 1
    // 余额最多改变 1
    assert balanceBefore != balanceAfter => (
        balanceAfter == balanceBefore - 1 ||
        balanceAfter == balanceBefore + 1
    );

    // only selected function can change balances
    // 只有选定的函数可以改变余额
    assert balanceBefore != balanceAfter => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector ||
        f.selector == sig:burn(uint256).selector
    );
}

Prover 运行：链接

前置条件

requireInvariant balanceOfConsistency(account) 和 require balanceLimited(account) 被注释掉了，因为 helperSoundFnCall() 已经对所有改变余额的方法强制执行了这些前置条件。balanceOfConsistency 通过销毁和转移分支中 ownerHasBalance 不变量的保留块强制执行。

调用前和调用后状态

该规则记录了 helperSoundFnCall(e, f) 调用前后账户余额，以比较这些值并确定方法调用是否以及改变了多少余额：

Copymathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter  = balanceOf(account);

断言

第一个断言表明，如果账户余额在 helperSoundFnCall(e, f) 调用后发生变化（ $balanceBefore \neq balanceAfter$ ），则变化量必须为正负一——不多也不少。

Copy// balance can change by at most 1
// 余额最多改变 1
assert $balanceBefore \neq balanceAfter$ => (
    $balanceAfter == balanceBefore - 1$ ||
    $balanceAfter == balanceBefore + 1$
);

第二个断言表明，只有以下函数可以改变余额：

铸造函数（mint()、safeMint()、safeMint(bytes)）
销毁（burn()）
转移函数（transferFrom()、safeTransferFrom()、safeTransferFrom(bytes)）

Copy// only selected function can change balances
// 只有选定的函数可以改变余额
assert $balanceBefore \neq balanceAfter$ => (
    f.selector == sig:transferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
    f.selector == sig:mint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector ||
    f.selector == sig:burn(uint256).selector
);

如果任何其他未列出的函数导致余额变化，则断言将失败，Prover 将报告违规。

`ownershipChange()` — 所有权只能通过铸造、销毁和转移操作改变

以下规则验证了通证的所有权（ownerOf(tokenId)）只能通过铸造、销毁或转移操作改变。操作类型取决于所有者地址如何变化：

从零地址到非零地址——表示铸造，只能由 mint()、safeMint() 或 safeMint(bytes) 引起。
从非零地址到零地址——表示销毁，只能由 burn() 引起。
从一个非零地址到另一个非零地址——表示转移，只能由 transferFrom()、safeTransferFrom() 或 safeTransferFrom(bytes) 引起。

Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers.                                                   │
│ 规则：所有权只能通过铸造、销毁或转移改变。                                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

    address ownerBefore = unsafeOwnerOf(tokenId);
    method f; helperSoundFnCall(e, f);
    address ownerAfter  = unsafeOwnerOf(tokenId);

    assert ownerBefore == 0 && ownerAfter != 0 => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector
    );

    assert ownerBefore != 0 && ownerAfter == 0 => (
        f.selector == sig:burn(uint256).selector
    );

    assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
    );
}

Prover 运行：链接

前置条件

require nonzerosender(e)

此前置条件要求调用者（e.msg.sender）为非零地址。如果没有它，Prover 可以模拟 address(0) 直接调用 transferFrom 的执行，这会从 address(0) 创建所有权，违反了只有铸造函数才能这样做的规则。

requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)

此不变量前置条件阻止零地址批准任何操作员。如果没有它，Prover 可以假设 address(0) 批准了一个非零操作员。这允许 transferFrom(from = address(0), ...) 即使在调用者是非零地址时也能成功，从而创建从零地址的所有权转移，并违反了只有铸造函数才能创建所有权的规则。

调用前和调用后状态

这些行记录了 helperSoundFnCall(e, f) 前后通证的所有者：

Copyaddress ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter  = unsafeOwnerOf(tokenId);

使用 unsafeOwnerOf(tokenId) 允许规则推理所有权变化，即使通证不存在（在这种情况下所有者为 address(0)）。

断言

assert ownerBefore == 0 && ownerAfter != 0 => (...)

如果所有权从零地址变为非零地址，意味着发生了铸造，那么只能由以下函数引起：mint()、safeMint() 或 safeMint(bytes)：

Copyassert $ownerBefore == 0 \land ownerAfter \neq 0$ => (
    f.selector == sig:mint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
);

assert ownerBefore != 0 && ownerAfter == 0 => (...)

如果所有权从非零地址变为零地址，意味着发生了销毁，那么只有 burn() 函数对此负责：

Copyassert $ownerBefore \neq 0 \land ownerAfter == 0$ => (
      f.selector == sig:burn(uint256).selector
);

assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (...)

最后，如果变化是从一个非零地址到另一个非零地址，那么发生了转移。只有 transferFrom()、safeTransferFrom() 和 safeTransferFrom(bytes) 对这些变化负责：

Copyassert $(ownerBefore \neq ownerAfter \land ownerBefore \neq 0 \land ownerAfter \neq 0)$ => (
      f.selector == sig:transferFrom(address,address,uint256).selector ||
      f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
      f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
);

`approvalChange()` — 授权只能通过 approve、transferFrom 和 burn 函数改变

以下规则验证了特定通证的授权（getApproved(tokenId)）只能通过三种方式改变：

通过调用 approve() 函数直接设置
作为转移的副作用重置为 address(0)
作为销毁的副作用重置为 address(0)

Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
│ 规则：通证授权只能通过 approve 或转移（隐式）改变。                                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
    address approvalBefore = unsafeGetApproved(tokenId);
    method f; helperSoundFnCall(e, f);
    address approvalAfter  = unsafeGetApproved(tokenId);

    // approve can set any value, other functions reset
    // approve 可以设置任何值，其他函数重置
    assert approvalBefore != approvalAfter => (
        f.selector == sig:approve(address,uint256).selector ||
        (
            (
                f.selector == sig:transferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
                f.selector == sig:burn(uint256).selector
            ) && approvalAfter == 0
        )
    );
}

Prover 运行：链接

调用前和调用后状态

以下行记录了部分参数化调用 method f; helperSoundFnCall(e, f) 前后的授权地址，以确定授权是否因列出的被调用方法而改变，以及是否被清除为 address(0)：

Copyaddress approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter  = unsafeGetApproved(tokenId);

断言

此断言表明，授权地址的变化只有在以下情况下才能发生：

函数调用是 approve()，它明确设置了授权地址，或者
函数调用是 transferFrom()、safeTransferFrom()（带或不带 bytes 数据）或 burn()，并且授权地址作为副作用被清除为 address(0)（ $approvalAfter == 0$ ）。

Copy// approve can set any value, other functions reset
// approve 可以设置任何值，其他函数重置
assert $approvalBefore \neq approvalAfter$ => (
        f.selector == sig:approve(address,uint256).selector ||
        (
            (
                f.selector == sig:transferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
                f.selector == sig:burn(uint256).selector
            ) && $approvalAfter == 0$
        )
    );

如果以下情况发生，则断言将失败：

未列出的函数清除或修改了授权地址。
transferFrom、safeTransferFrom 或 burn 未将授权地址清除为 address(0)。

`approvedForAllChange` — 所有通证的授权仅通过 `setApprovalForAll()` 函数改变

此规则验证了spender的所有通证授权状态（isApprovedForAll(owner, spender)）只能通过显式调用 setApprovalForAll() 函数来改变：

Copy/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
│ 规则：所有通证的授权只能通过 isApprovedForAll 改变。                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
    bool approvedForAllBefore = isApprovedForAll(owner, spender);
    method f; helperSoundFnCall(e, f);
    bool approvedForAllAfter  = isApprovedForAll(owner, spender);

    assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
}

Prover 运行：链接

调用前和调用后状态

bool approvedForAllBefore = isApprovedForAll(owner, spender);

这记录了 helperSoundFnCall(e, f) 调用前的所有通证授权状态。

bool approvedForAllAfter = isApprovedForAll(owner, spender);

这记录了 helperSoundFnCall(e, f) 调用后的所有通证授权状态。

Copybool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter  = isApprovedForAll(owner, spender);

断言

如果spender的所有通证授权状态发生变化，则唯一的原因是调用了 setApprovalForAll()：

Copyassert $approvedForAllBefore \neq approvedForAllAfter$ => f.selector == sig:setApprovalForAll(address,bool).selector;

与 approve() 在转移或销毁时重置不同，isApprovedForAll 在铸造、转移或销毁期间不会改变。只有显式调用 setApprovalForAll 才能修改它。如果任何其他函数改变此状态，则断言失败，Prover 将报告违规。

完整规范

以下是部分参数化规则的完整规范：

Copymethods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;

    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;

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

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

definition balanceLimited(address account) returns bool = balanceOf(account) &lt; max_uint256;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helper                                                                                                              │
│ 辅助函数                                                                                                            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

function helperSoundFnCall(env e, method f) {
    if (f.selector == sig:mint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        mint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256).selector) {
        address to; uint256 tokenId;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        address to; uint256 tokenId; bytes data;
        require data.length &lt; 0xffff;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId, data);
    } else if (f.selector == sig:burn(uint256).selector) {
        uint256 tokenId;
        requireInvariant ownerHasBalance(tokenId);
        // requireInvariant notMintedUnset(tokenId);
        burn(e, tokenId);
    } else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        transferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        address from; address to; uint256 tokenId;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        address from; address to; uint256 tokenId; bytes data;
        require data.length &lt; 0xffff;
        require balanceLimited(to);
        requireInvariant ownerHasBalance(tokenId);
        requireInvariant notMintedUnset(tokenId);
        safeTransferFrom(e, from, to, tokenId, data);
    } else {
        calldataarg args;
        f(e, args);
    }
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
│ 幽灵变量与Hook：所有权计数                                                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mapping(address => mathint) _ownedByUser {
    init_state axiom _ownedByUser[a] == 0;
}

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances                                                                                             │
│ 幽灵变量与Hook：余额                                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

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

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

hook Sload uint256 value _balances[KEY address user] {
    require _balances[user] == to_mathint(value);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned                                                                  │
│ 不变量：balanceOf 是拥有的通证数量                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];
    // {
    //     preserved {
    //         require balanceLimited(user);
    //     }
    // }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance                                                                  │
│ 不变量：通证所有者必须有余额                                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover v8.3.1
    {
        preserved {
            requireInvariant balanceOfConsistency(ownerOf(tokenId));
            // require balanceLimited(ownerOf(tokenId));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator                                                                    │
│ 不变量：address(0) 没有授权的操作员                                                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
    !isApprovedForAll(0, a)
    {
        preserved with (env e) {
            require nonzerosender(e);
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved                                                  │
│ 不变量：不存在的通证不被拥有且未被授权                                                                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
    unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn                                                           │
│ 规则：总供应量只能通过铸造和销毁改变                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

    mathint supplyBefore = _supply;
    method f; helperSoundFnCall(e, f);
    mathint supplyAfter = _supply;

    assert $supplyAfter > supplyBefore$ => (
        $supplyAfter == supplyBefore + 1$ &&
        (
            f.selector == sig:mint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256).selector ||
            f.selector == sig:safeMint(address,uint256,bytes).selector
        )
    );
    assert $supplyAfter &lt; supplyBefore$ => (
        $supplyAfter == supplyBefore - 1$ &&
        f.selector == sig:burn(uint256).selector
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1.           │
│ 规则：balanceOf 只能通过铸造、销毁或转移改变。balanceOf 每次改变不能超过 1。                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {
    // requireInvariant balanceOfConsistency(account);
    // require balanceLimited(account);

    mathint balanceBefore = balanceOf(account);
    method f; helperSoundFnCall(e, f);
    mathint balanceAfter  = balanceOf(account);

    // balance can change by at most 1
    // 余额最多改变 1
    assert $balanceBefore \neq balanceAfter$ => (
        $balanceAfter == balanceBefore - 1$ ||
        $balanceAfter == balanceBefore + 1$
    );

    // only selected function can change balances
    // 只有选定的函数可以改变余额
    assert $balanceBefore \neq balanceAfter$ => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector ||
        f.selector == sig:burn(uint256).selector
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers.                                                   │
│ 规则：所有权只能通过铸造、销毁或转移改变。                                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
    require nonzerosender(e);
    requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);

    address ownerBefore = unsafeOwnerOf(tokenId);
    method f; helperSoundFnCall(e, f);
    address ownerAfter  = unsafeOwnerOf(tokenId);

    assert $ownerBefore == 0 \land ownerAfter \neq 0$ => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256).selector ||
        f.selector == sig:safeMint(address,uint256,bytes).selector
    );

    assert $ownerBefore \neq 0 \land ownerAfter == 0$ => (
        f.selector == sig:burn(uint256).selector
    );

    assert $(ownerBefore \neq ownerAfter \land ownerBefore \neq 0 \land ownerAfter \neq 0)$ => (
        f.selector == sig:transferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
        f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
│ 规则：通证授权只能通过 approve 或转移（隐式）改变。                                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
    address approvalBefore = unsafeGetApproved(tokenId);
    method f; helperSoundFnCall(e, f);
    address approvalAfter  = unsafeGetApproved(tokenId);

    // approve can set any value, other functions reset
    // approve 可以设置任何值，其他函数重置
    assert $approvalBefore \neq approvalAfter$ => (
        f.selector == sig:approve(address,uint256).selector ||
        (
            (
                f.selector == sig:transferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
                f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
                f.selector == sig:burn(uint256).selector
            ) && $approvalAfter == 0$
        )
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll.                                            │
│ 规则：所有通证的授权只能通过 isApprovedForAll 改变。                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
    bool approvedForAllBefore = isApprovedForAll(owner, spender);
    method f; helperSoundFnCall(e, f);
    bool approvedForAllAfter  = isApprovedForAll(owner, spender);

    assert $approvedForAllBefore \neq approvedForAllAfter$ => f.selector == sig:setApprovalForAll(address,bool).selector;
}

Prover 运行：链接

关于部分参数化规则与完全参数化规则区别的说明

这些状态变化属性可以通过单个部分参数化规则或多个完全参数化规则（每个属性一个）进行验证。两种方法都使用 method f 来推理所有合约方法的状态变化，但它们在前置条件范围界定方式上有所不同。

在完全参数化规则中，所有前置条件都在规则级别应用，因此约束了所有可能的方法调用。当验证状态时，所有影响该状态的方法都适用相同的前置条件时，这种方法效果良好。

另一方面，部分参数化规则使用基于被调用方法的条件逻辑。它不是将前置条件应用于所有方法调用，而是将任意方法调用路由到方法特定的分支，每个分支都有其自身相关的前置条件。前置条件仅在需要时才适用，当规则验证需要不同方法特定约束的多个断言时，这种方法效果良好。

它们之间的选择主要是关于代码组织：部分参数化规则集中了方法特定逻辑，而完全参数化规则将关注点分离到独立的规则中。这种组织差异影响了可维护性和清晰度，但当前置条件得到正确限定时，两种方法都同样有效。

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

原文链接： rareskills.io/post/certo...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

翻译
学分: 0
分类: 以太坊
标签: 形式化验证 Certora ERC-721 参数化规则 CVL 智能合约

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

ERC-721 的部分参数化规则

ERC-721 的部分参数化规则

引言

部分参数化规则

`helperSoundFnCall()` 将 $f(e, args)$ 调用路由到正确的方法分支

对于铸造操作 — `mint()`、`safeMint()` 和 `safeMint(bytes)`

对于销毁操作 — `burn()`

对于转移操作 — `transferFrom()`、`safeTransferFrom()` 和 `safeTransferFrom(bytes)`

对于除铸造、销毁和转移之外的所有操作

CVL 函数 `helperSoundFnCall()` 的完整实现

`supplyChange` — 总供应量只能通过 `mint()`、`safeMint()`、`safeMint(bytes)` 和 `burn()` 改变

前置条件

调用前和调用后状态

断言

`balanceChange` — 账户余额只能通过铸造、销毁和转移操作改变

前置条件

调用前和调用后状态

断言

`ownershipChange()` — 所有权只能通过铸造、销毁和转移操作改变

前置条件

调用前和调用后状态

断言

`approvalChange()` — 授权只能通过 approve、transferFrom 和 burn 函数改变

调用前和调用后状态

断言

`approvedForAllChange` — 所有通证的授权仅通过 `setApprovalForAll()` 函数改变

调用前和调用后状态

断言

完整规范

关于部分参数化规则与完全参数化规则区别的说明

0 条评论

文章目录

ERC-721 的部分参数化规则

ERC-721 的部分参数化规则

引言

部分参数化规则

helperSoundFnCall() 将 $f(e, args)$ 调用路由到正确的方法分支

对于铸造操作 — mint()、safeMint() 和 safeMint(bytes)

对于销毁操作 — burn()

对于转移操作 — transferFrom()、safeTransferFrom() 和 safeTransferFrom(bytes)

对于除铸造、销毁和转移之外的所有操作

CVL 函数 helperSoundFnCall() 的完整实现

supplyChange — 总供应量只能通过 mint()、safeMint()、safeMint(bytes) 和 burn() 改变

前置条件

调用前和调用后状态

断言

balanceChange — 账户余额只能通过铸造、销毁和转移操作改变

前置条件

调用前和调用后状态

断言

ownershipChange() — 所有权只能通过铸造、销毁和转移操作改变

前置条件

调用前和调用后状态

断言

approvalChange() — 授权只能通过 approve、transferFrom 和 burn 函数改变

调用前和调用后状态

断言

approvedForAllChange — 所有通证的授权仅通过 setApprovalForAll() 函数改变

调用前和调用后状态

断言

完整规范

关于部分参数化规则与完全参数化规则区别的说明

0 条评论

文章目录

`helperSoundFnCall()` 将 $f(e, args)$ 调用路由到正确的方法分支

对于铸造操作 — `mint()`、`safeMint()` 和 `safeMint(bytes)`

对于销毁操作 — `burn()`

对于转移操作 — `transferFrom()`、`safeTransferFrom()` 和 `safeTransferFrom(bytes)`

CVL 函数 `helperSoundFnCall()` 的完整实现

`supplyChange` — 总供应量只能通过 `mint()`、`safeMint()`、`safeMint(bytes)` 和 `burn()` 改变

`balanceChange` — 账户余额只能通过铸造、销毁和转移操作改变

`ownershipChange()` — 所有权只能通过铸造、销毁和转移操作改变

`approvalChange()` — 授权只能通过 approve、transferFrom 和 burn 函数改变

`approvedForAllChange` — 所有通证的授权仅通过 `setApprovalForAll()` 函数改变