简介

在上一章中，我们学习了参数化规则（parametric rules），它允许我们对那些无论调用哪个函数都预期成立的属性进行形式化验证。这在验证通用不变量时特别有用。但是，如果期望的行为不是通用的，而是取决于所调用的具体函数呢？例如，考虑以下场景：

• 任何合约的 owner 都应保持不变，除非 owner 调用了 changeOwner 或 renounceOwnership。
• ERC-20 代币的总体供应量（total supply）应保持不变，除非代币正在被铸造（minted）或销毁（burned）。

当某个属性通常成立，但根据函数有已知例外情况时，我们该如何处理？或者，如果您只是想将某些管理方法完全排除在通用不变量检查之外呢？

在本章中，我们将学习如何使用方法属性（method properties）在参数化规则中执行特定于函数的断言。我们还将了解当这些规则不适用时，如何将某些函数排除在验证之外。

什么是方法属性？

下面的代码展示了一个参数化规则——一个适用于所有函数的规则。

Copy
rule someParametricRule() {  
    env e;
      
    method f;  
    calldataarg args;  
    f(e, args);  

    assert property_1;  
}

无论您是需要执行特定于函数的断言，还是从规则中排除某些函数，您都需要一种区分不同函数的方法。这就是方法属性发挥作用的地方。

在 CVL 中，方法属性是可以通过类似字段的语法（例如 f.propertyName）在 method 变量（如 f）上访问的属性。这些属性提供了关于 f 在运行时所指向的函数的信息，允许您的规则逻辑根据被调用的具体方法进行自适应。

可用的方法属性包括：

• f.selector：返回 4 字节的函数选择器（函数签名的哈希值，例如 0xa9059cbb），可用于识别特定的具名函数（例如 f.selector == sig:transfer(address,uint256).selector），从而在参数化规则中应用特定于函数的断言。
• f.isPure：如果函数 f 在 Solidity 中声明为 pure 关键字，则返回 true。这对于将纯计算函数排除在仅对状态修改逻辑有意义的规则之外非常有用。
• f.isView：如果函数 f 声明为 view 关键字，则返回 true。在编写与状态更改相关的规则时，这可用于跳过只读函数。我们将在后面的小节中探讨这样做的优势。
• f.isFallback：如果 f 代表 fallback() 或 receive() 函数，则返回 true。当您需要编写管理回退行为（fallback behavior）的规则时（例如 payable 要求或底层调用的特殊处理），这会很有帮助。
• f.numberOfArguments：返回函数 f 预期的参数数量。
• f.contract：返回定义该函数的合约。这在您同时验证多个合约或处理继承时非常有用——比如两个合约拥有同名且参数相同的函数。我们将在后面的章节中探讨这一点，因为当前的示例仅涉及单个合约。

在所有这些属性中，最常用的方法属性是 f.selector、f.isView 和 f.isPure。它们涵盖了最典型的用例——比如在编写关注状态变化的规则时，识别特定函数（使用选择器）或跳过只读和计算函数（isView 和 isPure）。为了保持实用性，我们将在接下来的示例中重点关注这些属性，并展示它们如何帮助编写更精确、更高效的参数化规则。

在参数化规则中执行依赖于函数的断言

为了理解如何使用方法属性在参数化规则中执行依赖于函数的断言，请看下面展示的 ERC-20 实现 RareToken，它同时包含了 mint 和 burn 功能：

Copy
//SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract RareToken {
    uint256 public totalSupply;
    address public owner;
    
    mapping(address => uint256) public balanceOf;
    mapping(address => mapping(address => uint256)) public allowance;

    event Transfer(address indexed from, address indexed to, uint256 value);
    event Approval(address indexed owner, address indexed spender, uint256 value);

    modifier onlyOwner() {
        require(msg.sender == owner, "Unauthorized");
        _;
    }

    constructor(uint256 _initialSupply) {
        owner = msg.sender;
        if (_initialSupply > 0) {
            _mint(msg.sender, _initialSupply);
        }
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        _transfer(msg.sender, to, amount);
        return true;
    }

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        _approve(msg.sender, spender, amount);
        return true;
    }

    function transferFrom(address from, address to, uint256 amount) public virtual returns (bool) {
        address spender = msg.sender;
        uint256 currentAllowance = allowance[from][spender];
        require(currentAllowance >= amount, "Allowance exceeded");
        
        if (currentAllowance != type(uint256).max) {
            _approve(from, spender, currentAllowance - amount);
        }
        
        _transfer(from, to, amount);
        return true;
    }

    function mint(address account, uint256 amount) public onlyOwner {
        _mint(account, amount);
    }

    function burn(uint256 amount) public virtual {
        _burn(msg.sender, amount);
    }

    function _transfer(address from, address to, uint256 amount) internal virtual {
        require(from != address(0), "Invalid sender");
        require(to != address(0), "Invalid recipient");
        
        uint256 fromBalance = balanceOf[from];
        require(fromBalance >= amount, "Insufficient balance");
        
        balanceOf[from] = fromBalance - amount;
        balanceOf[to] += amount;
        emit Transfer(from, to, amount);
    }

    function _mint(address account, uint256 amount) internal virtual {
        require(account != address(0), "Invalid recipient");
        
        totalSupply += amount;
        balanceOf[account] += amount;
        emit Transfer(address(0), account, amount);
    }

    function _burn(address account, uint256 amount) internal virtual {
        require(account != address(0), "Invalid burner");
        
        uint256 accountBalance = balanceOf[account];
        require(accountBalance >= amount, "Burn exceeds balance");
        
        balanceOf[account] = accountBalance - amount;
        totalSupply -= amount;
        emit Transfer(account, address(0), amount);
    }

    function _approve(address ownerAccount, address spender, uint256 amount) internal virtual {
        require(ownerAccount != address(0), "Invalid owner");
        require(spender != address(0), "Invalid spender");
        
        allowance[ownerAccount][spender] = amount;
        emit Approval(ownerAccount, spender, amount);
    }
}

由于上述 ERC-20 实现包含了 mint() 和 burn()，因此在调用这些函数期间，totalSupply 的值预计会发生变化——这与我们在上一章中使用的 ERC-20 实现不同，当时不允许任何函数更改供应量。

现在，假设我们想为 RareToken 合约编写一个参数化规则，以强制执行以下行为：

• 当调用 mint() 函数时，totalSupply 绝对不能减少（它可以增加，或者如果数量为零则保持不变）。
• 当调用 burn() 函数时，totalSupply 绝对不能增加（它可以减少，或者如果数量为零则保持不变）。
• 对于任何其他函数（如 transfer、approve、transferFrom），totalSupply 必须保持不变。

要定义一个强制执行上述行为的参数化规则，该规则必须确保以下几点：

1. 该规则应首先在任何函数执行之前记录 totalSupply 变量的初始值，以为状态比较建立参考点。
2. 为了评估多个函数对 totalSupply 状态的影响，规则应采用参数化框架，一次一个地执行每个目标函数。
3. 在每个函数完成执行后，规则必须记录 totalSupply 的更新值，以跟踪状态的修改。
4. 最后，规则应基于所执行的函数强制执行三个关键的断言。

下面的规则 totalSupplyIntegrityCheck 实现了所有这些步骤。它在每次函数执行前后捕获 totalSupply，使用参数化设置调用任意方法，然后根据调用的具体函数强制执行预期的行为：

Copy
rule totalSupplyIntegrityCheck() {

    env e;

    // Step 1: Record initial state
    mathint supplyBefore = totalSupply(e);

    // Step 2: Execute an arbitrary function
    method f;
    calldataarg args;
    f(e, args);

    // Step 3: Record updated state
    mathint supplyAfter = totalSupply(e);

    // Step 4: Function-specific assertions
    if (f.selector == sig:mint(address,uint256).selector) {
        assert supplyAfter >= supplyBefore, "Total supply should not decrease after mint()";
    } 
    else if (f.selector == sig:burn(uint256).selector) {
        assert supplyAfter <= supplyBefore, "Total supply should not increase after burn()";
    } 
    else {
        assert supplyAfter == supplyBefore, "Total supply must remain unchanged for other function calls";
    }
}

在上述规则中，我们使用 f.selector 访问了任意函数（f）的函数选择器，并使用 sig:functionName(...).selector 符号派生了已知函数的函数选择器。然后，我们用它来比较已执行的函数 f 是否对应于诸如 mint() 或 burn() 等特定的具名函数，从而在我们的参数化规则中执行特定于函数的断言。

上述规则简单地强制执行了以下行为：

1. 如果执行了 mint() 函数（通过 f.selector == sig:mint(address,uint256).selector 识别），则与其初始值相比，totalSupply 的值绝对不能减少。
2. 如果执行了 burn() 函数（通过 f.selector == sig:burn(uint256).selector 识别），则与其初始值相比，totalSupply 的值绝对不能增加。
3. 对于所有其他函数调用，规则强制要求 totalSupply 的值必须保持不变，以确保没有非预期的函数修改 totalSupply 变量。

要查看参数化规则的结果，请将 RareToken 合约及其规范文件放置在相应的目录中以设置 Certora Prover 环境。然后，运行验证过程。如果合约满足规则的条件，证明器将确认验证成功，未检测到任何违规，如下方的结果所示。

验证结果确认 totalSupplyIntegrityCheck 规则已成功执行，所有九项检查均通过，未检测到任何违规。这验证了 RareToken 合约中 mint()、burn() 及其他函数的行为符合规则的预期——totalSupply 在 mint() 之后增加，在 burn() 之后减少，并在所有其他函数中保持不变。

上述规则成功使用了基于 f.selector 的条件逻辑，在执行每个函数 f _之后_应用了正确的断言。这确保了每个与规则参数兼容的函数，都会根据其标识对照适当的预期进行检查。

使用 filtered 块优化参数化规则

在查看验证报告时，我们注意到 Certora Prover 已将我们的断言检查应用于合约中的每个函数——包括如 totalSupply()、balanceOf() 和 owner() 这样的只读函数。这些函数在 Solidity 中被标记为 view，这意味着它们只从区块链状态中读取数据，而不修改任何内容。因此，在这些函数上运行状态变更规则并没有太大意义，也无法帮助我们捕获有意义的漏洞。

尽管验证它们在技术上并没有错，但这会引起额外的计算工作并拖慢流程。因此，当不影响合约状态的函数与正在测试的规则无关时，将它们排除在外非常重要。这就是 filter 块派上用场的地方。

filter 块允许我们基于方法属性（如 isView、isPure 等）_选择性地包含或排除_某些方法，决定其是否被参数化规则分析。

使用 filtered 块排除 View 函数

为了理解 filter 块的功能，请考虑下面包含带有 filter 块规则的规范。

Copy
rule totalSupplyIntegrityCheck(env e, method f, calldataarg args) filtered {
    f -> !f.isView
} {

    // Step 1: Record initial state
    mathint supplyBefore = totalSupply(e);

    // Step 2: Execute an arbitrary function
    f(e, args);

    // Step 3: Record updated state
    mathint supplyAfter = totalSupply(e);

    // Step 4: Function-specific assertions
    if (f.selector == sig:mint(address,uint256).selector) {
        assert supplyAfter >= supplyBefore, "Total supply should not decrease after mint()";
    } 
    else if (f.selector == sig:burn(uint256).selector) {
        assert supplyAfter <= supplyBefore, "Total supply should not increase after burn()";
    } 
    else {
        assert supplyAfter == supplyBefore, "Total supply must remain unchanged for other function calls";
    }
}

在上述规则中，filter 块 filtered {} 内的代码行 f -> !f.isView 起到了过滤器的作用，它告诉证明器：“仅在 f.isView 为 false 的函数上运行此规则。” 换句话说，它将所有标记为 view 的函数排除在了验证之外。

如果我们使用上述规范重新运行证明器，我们可以看到 像 totalSupply()、 balanceOf() 和 owner() 这样的 view 函数不再被包含在该规则的验证中，如下图所示：

在参数化规则内使用 filter 块可以帮助我们实现两点：

1. 通过跳过那些保证不会改变合约状态的无关函数，它降低了计算开销。
2. 它简化了验证输出，使我们能够只专注于状态变更函数的结果。

总结

这就是我们如何利用方法属性来强制执行特定于函数的断言，并使用 filtered 块将不相关的函数排除在验证之外。

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