简介

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

• supplyChange

  总供应量只能通过 mint 或 burn 操作发生变化，且每次变化量必须精确为 1。

• balanceChange

  账户余额只能通过 mint、burn 或 transfer 操作发生变化，且每次变化量必须精确为 1。

• ownershipChange

  代币所有权只能通过 mint、burn 或 transfer 操作发生变化。

• approvalChange

  单代币授权只能通过调用 approve()，或作为 burn 或 transfer 操作的副作用发生变化。

• approvedForAllChange

  操作员授权只能通过调用 setApprovalForAll() 发生变化。

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

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

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

有人可能会问，CVL 不变量（invariants）是否可以达到相同的目的。然而，CVL 不变量在这里并不适用，因为它们无法捕获一个值在一次方法调用前后是如何变化的。不变量无法访问调用前的值，也无法将它们与调用后的值进行比较，因此它们无法表达诸如“这种状态只能在调用特定方法时发生改变”或“这种状态的改变恰好是这个数量”等属性。这些是状态转移（state-transition）属性，需要对调用前和调用后的状态进行推理。

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

部分参数化规则

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

“……参数化规则验证在一个属性在以任何有效参数调用任何函数之后都保持为真。”

关键短语是：”在以任何有效参数调用任何函数之后”（after any function is called with any valid arguments），这对应于以下代码模式：

Copy
rule 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

}

这种模式（完全参数化）在相同的前置条件（preconditions）适用于所有方法时非常有效。然而，当不同的方法需要不同的约束时，它就不合适了。

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

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

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

Copy
rule 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 函数中，如下所示：

Copy
rule partiallyParametricExample(env e) {
	method f;
	helperFunction(e, f); // contains all conditional logic
}

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

Copy
/// ERC721.spec  

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

helperSoundFnCall() 中的 “Sound” 是故意为之的。可靠性（Soundness）意味着验证不会遗漏任何真实的错误，而导致不可靠的一个常见来源是通过过于严格的前置条件排除了有效的执行路径。

该辅助函数通过基于调用的方法有选择地（而不是全局地对所有调用）应用前置条件，以一种可靠的方式路由 f(e, args)。对不需要前置条件的方法应用前置条件将排除有效的执行路径。

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

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

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

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

针对 mint 操作 —— 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)。

Copy
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 < 0xffff;
        require balanceLimited(to);
        // requireInvariant notMintedUnset(tokenId);
        safeMint(e, to, tokenId, data);
    }
		...
}

针对 burn 操作 —— burn()

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

• 声明所需参数 uint256 tokenId。

• 应用特定于方法的前置条件 requireInvariant ownerHasBalance(tokenId)，该条件要求在销毁（burn）发生之前代币必须存在（拥有非零的所有者）。

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

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

针对 transfer 操作 —— 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)

Copy
function 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);
		...
}

针对除 mint、burn 和 transfer 之外的所有操作

除 mint、burn 或 transfer 之外的函数通过带有任意参数的完全参数化调用 f(e, args) 来处理：

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

CVL 函数 helperSoundFnCall() 的完整实现

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

Copy
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 < 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。以下是捕获此行为的规则，我们将在稍后详细讨论：

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 运行结果：link

前置条件

• require nonzerosender(e)

  这个前置条件将调用者限制为非零地址。如果没有这个约束，Prover 可以探索转移从 address(0) 发起并将代币移动到非零地址的执行情况，这实际上是一个通过 transfer 操作执行的 mint。

• 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

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

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

ERC-721 不跟踪总供应量，因此我们使用一个 ghost 变量 _supply，通过 Sstore 钩子（hook）来跟踪所有 _balances 的总和：

Copy
ghost 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) 引起：

  Copy
  rule 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
          )
      );
      ...
  }
  

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

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

balanceChange —— 账户余额只能通过 mint、burn 和 transfer 操作发生变化

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

• 每次操作的余额变化量精确为一个代币
• 只有 mint、burn 或 transfer 操作才能改变余额

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 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
    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 运行结果：link

前置条件

requireInvariant balanceOfConsistency(account) 和 require balanceLimited(account) 被注释掉了，因为 helperSoundFnCall() 已经为所有更改余额的方法强制执行了这些前置条件。balanceOfConsistency 是通过在 burn 和 transfer 分支中 ownerHasBalance 不变量的 preserved 块来强制执行的。

调用前与调用后状态

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

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

断言

第一个断言指出，如果在调用 helperSoundFnCall(e, f) 之后账户余额发生了变化（balanceBefore != balanceAfter），那么变化量必须是加一或减一 —— 不能多也不能少。

Copy
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
    balanceAfter == balanceBefore - 1 ||
    balanceAfter == balanceBefore + 1
);

第二个断言指出，只有以下函数才能改变余额：

• mint 函数（mint()、safeMint()、safeMint(bytes)）
• burn 函数（burn()）
• transfer 函数（transferFrom()、safeTransferFrom()、safeTransferFrom(bytes)）

Copy
// 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 将报告违规。

ownershipChange() —— 所有权只能通过 mint、burn 和 transfer 操作发生变化

以下规则验证了代币的所有权（ownerOf(tokenId)）只能通过 mint、burn 或 transfer 操作发生变化。操作的类型取决于所有者地址是如何变化的：

• 从零地址变为非零地址 —— 表示发生了 mint，只有 mint()、safeMint() 或 safeMint(bytes) 才能引起此变化。
• 从非零地址变为零地址 —— 表示发生了 burn，只有 burn() 才能引起此变化。
• 从一个非零地址变为另一个非零地址 —— 表示发生了 transfer，只有 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 运行结果：link

前置条件

• require nonzerosender(e)

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

• requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)
  这个不变量前置条件防止零地址授权给任何操作员。如果没有它，Prover 可以假设 address(0) 授权了一个非零操作员。这将允许 transferFrom(from = address(0), ...) 即使在调用者非零的情况下也能成功，从而产生一个来自零地址的所有权转移，违反了只有 mint 函数才能创建所有权的规则。

调用前与调用后状态

以下代码行记录了 helperSoundFnCall(e, f) 调用前后的代币所有者：

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

使用 unsafeOwnerOf(tokenId) 允许规则推理所有权变化，即使在代币不存在的情况下也是如此（在这种情况下，所有者是 address(0)）。

断言

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

  如果所有权从零地址变为非零地址，意味着发生了 mint，那么只有以下函数可能导致此变化：mint()、safeMint() 或 safeMint(bytes)：

  Copy
  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 => (...)

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

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

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

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

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

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

以下规则验证了特定代币的授权（getApproved(tokenId)）只能以三种方式发生变化：

• 通过直接调用 approve() 函数进行设置
• 作为 transfer 操作的副作用被重置为 address(0)
• 作为 burn 操作的副作用被重置为 address(0)

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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
    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 运行结果：link

调用前与调用后状态

下面的代码记录了部分参数化调用 method f; helperSoundFnCall(e, f) 之前和之后的被授权地址，以确定授权是否由于列表中调用的方法而发生了变化，以及它是否被清空为 address(0)：

Copy
address 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
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
    )
);

在以下情况下，该断言将失败：

• 未在规则中列出的函数清空或修改了被授权地址。
• transferFrom、safeTransferFrom 或 burn 没有将被授权地址清空为 address(0)。

approvedForAllChange —— 全部授权只能通过 setApprovalForAll() 函数发生变化

该规则验证了代币支出者（spender）的全部授权状态（isApprovedForAll(owner, spender)）只能通过显式调用 setApprovalForAll() 函数来改变：

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through 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 运行结果：link

调用前与调用后状态

• bool approvedForAllBefore = isApprovedForAll(owner, spender);

  记录在调用 helperSoundFnCall(e, f) 之前的全部授权状态。

• bool approvedForAllAfter = isApprovedForAll(owner, spender);

  记录在调用 helperSoundFnCall(e, f) 之后的全部授权状态。

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

断言

如果支出者的全部授权状态发生变化，那么唯一的原因是调用了 setApprovalForAll()：

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

与在发生 transfer 或 burn 时会重置的 approve() 不同，isApprovedForAll 在 mint、transfer 或 burn 期间不会发生变化。只有显式调用 setApprovalForAll 才能对其进行修改。如果任何其他函数改变了这种状态，断言将失败，Prover 将报告违规。

完整规范

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

Copy
methods {
    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                                                                                                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count                                                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

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

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

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

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                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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.           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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
    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
    );
}

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly).                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
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
    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
        )
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through 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 运行结果：link

关于使用部分参数化与完全参数化之间区别的说明

这些状态变化属性可以使用单一的部分参数化规则进行验证，也可以使用多个完全参数化规则（每个属性一个规则）进行验证。这两种方法都使用 method f 来推理所有合约方法的状态变化，但它们在如何确定前置条件的作用域方面有所不同。

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

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

它们之间的选择主要是关于代码组织的考虑：部分参数化规则将特定于方法的逻辑集中在一起，而完全参数化规则将关注点分离到独立的规则中。这种组织差异会影响可维护性和清晰度，但在前置条件作用域设置正确的情况下，这两种方法都是同样有效的。

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