到目前为止，在前几章中，我们已经编写了规则来验证特定方法的行为及其对合约状态的影响。例如：

• 在第 2 章中，我们编写了一条规则来验证调用 increment() 会使 count 的值增加一。
• 在第 3 章中，我们编写了一条规则来检查连续调用 increment() 和 decrement() 后，count 的值应该保持不变。

但是，如果我们想要推导那些无论调用哪个函数都应该成立的属性呢？例如，考虑以下属性：

• 在一个简单的投票合约中，总票数应该始终等于赞成票和反对票的总和。
• **在一个 ERC-20 合约中，**用户的余额绝不能超过代币的总供应量。

在本章中，我们将学习如何编写所谓的参数化规则（parametric rules）——这些规则允许我们形式化验证那些无论调用什么函数都预期成立的属性。

参数化规则简介

在 CVL 中，标准规则通常在_特定_函数调用后检查状态转换。你通常会使用如下模式来定义允许的状态转换：

Copy
rule any_general_rule{

  require <setup conditions>;
  
  mySpecificFunction(arg1, arg2);
   
  assert <expected outcome>;     
}

参数化规则的工作原理类似，但将这一概念进行了泛化。参数化规则不再局限于单一的 function(args)，而是验证在_使用任何有效参数调用任何函数_之后，某个属性是否依然成立。

CVL 如何处理“任何函数，任何参数”

为了表达“带有任何有效参数的任何函数”这一概念，CVL 提供了两种特殊类型：

1. method：代表你正在验证的合约中的_任何 public 或 external 函数_。声明一个 method 类型的变量意味着该规则可以动态引用并执行合约中的任何函数。
2. calldataarg：代表函数调用的_参数_。由于不同的函数需要不同的输入，calldataarg 确保为当前正在测试的任何函数（method）自动提供有效的参数。

参数化调用语法

这两个特殊类型允许我们创建所谓的参数化调用（parametric call），它使得规则能够访问并调用被验证合约的每一个 public 或 external 方法，使用的语法如下：

Copy
rule someParametricRule() { 

    env e;
    
    method f;
    calldataarg args;
    
    f(e,args)
    
    //Any assert statement should go here
    assert <property_1>;
    assert <property_2>;
 }

f(e, args) 这一行被称为参数化调用。它允许我们测试合约中的所有 public 或 external 函数，而不是手动挑选某一个。它的工作原理如下：

• f 代表合约中的任何函数。这个变量不需要指定特定的函数，而是确保每一个函数都能被逐一测试。
• args 代表一组有效的输入值。由于不同的函数具有不同的参数，args 确保为每个函数提供正确类型和数量的输入。
• e：为函数调用模拟提供必要的环境上下文（如发送者地址、区块号等）。

本质上，f(e, args); 这一行告诉 Certora Prover：“对于该合约中的每一个函数 f__，请在模拟环境 e 中使用有效参数 args 来执行它。”

通过将 assert 语句放在 f(e, args); 行_之后_，我们定义了在_任何_函数调用完成后必须普遍成立的属性。这使得参数化规则成为验证智能合约核心不变量和一般安全属性的理想选择。

识别 ERC-20 中的不变量

让我们应用所学知识来形式化验证下面展示的 ERC-20 实现中的一个不变量：

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

contract RareToken {
    uint8 public immutable decimals = 18;
    uint256 public immutable totalSupply;

    mapping(address => uint256) private balances;
    mapping(address => mapping(address => uint256)) private allowances;

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

    constructor(uint256 _initialSupply) {
        require(_initialSupply > 0, "Invalid initial supply");
        
        totalSupply = _initialSupply * 10 ** uint256(decimals);
        balances[msg.sender] = totalSupply;
        
        emit Transfer(address(0), msg.sender, totalSupply);
    }

    function balanceOf(address account) public view returns (uint256) {
        return balances[account];
    }

    function transfer(address recipient, uint256 amount) public returns (bool) {
        require(recipient != address(0), "ERC20: transfer to zero address");
        require(balances[msg.sender] >= amount, "Insufficient balance");
        
        balances[msg.sender] -= amount;
        balances[recipient] += amount;
        emit Transfer(msg.sender, recipient, amount);
        return true;
    }

    function approve(address spender, uint256 amount) public returns (bool) {
        require(spender != address(0), "ERC20: approve to zero address");
        
        allowances[msg.sender][spender] = amount;
        emit Approval(msg.sender, spender, amount);
        return true;
    }

    function allowance(address owner_, address spender) public view returns (uint256) {
        return allowances[owner_][spender];
    }

    function transferFrom(
        address sender,
        address recipient,
        uint256 amount
    ) public returns (bool) {
        require(recipient != address(0), "ERC20: transfer to zero address");
        require(balances[sender] >= amount, "Insufficient balance");
        
        uint256 currentAllowance = allowances[sender][msg.sender];
        require(currentAllowance >= amount, "ERC20: insufficient allowance");
        
        if (currentAllowance != type(uint256).max) {
            allowances[sender][msg.sender] = currentAllowance - amount;
        }
        
        balances[sender] -= amount;
        balances[recipient] += amount;
        emit Transfer(sender, recipient, amount);
        return true;
    }
}

正如我们所学到的，编写参数化规则的目的是验证智能合约在不同的函数调用中应始终成立的属性。在我们的 RareToken 合约中，一个关键的不变量是：总供应量稳定性（Total Supply Stability）。

由于该合约不包含 mint 或 burn 功能，因此总供应量在部署时初始化一次，并必须在合约的整个生命周期内保持不变。换句话说，任何函数都不应该修改 totalSupply() 返回的值。

让我们看看如何编写一条参数化规则来验证总供应量的完整性。

形式化验证总供应量一致性

一旦我们确定了想要验证的合约的关键不变量，请按照以下步骤编写参数化规则：

1. 定义规则

使用 rule 关键字，后跟一个具有描述性的规则名称：

Copy
rule totalSupplyIsConstant() { }

2. 声明执行环境

定义一个 env 变量来表示函数的执行环境：

Copy
rule totalSupplyIsConstant() {
    env e;
}

3. 捕获调用前的状态

因为我们需要比较函数执行前后 totalSupply 的值，所以我们存储它的初始状态：

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);
}

4. 模拟函数执行

声明一个 method 变量来表示任何函数调用，并定义可能传递的 arguments（参数）：

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args); // Execute the function call with the given arguments
}

5. 捕获调用后的状态

在执行该函数后，我们将存储更新后的 totalSupply 的值：

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args);

    mathint afterSupply = totalSupply(e);
}

6. 强制约束总供应量一致性

在我们的 RareToken 合约的例子中，我们要确保 totalSupply 变量在任何函数执行后都绝不会改变。我们使用 assert 语句（assert beforeSupply == afterSupply）来显式强制约束这一条件：

Copy
rule totalSupplyIsConstant() {
    env e;

    mathint beforeSupply = totalSupply(e);

    method f;
    calldataarg args;

    f(e, args);

    mathint afterSupply = totalSupply(e);

    assert beforeSupply == afterSupply; 
}

运行验证

要查看我们参数化规则的结果，请应用你在前面章节中学到的知识：将 RareToken 合约及其相应的规范放入 Certora Prover 环境中。

设置完成后，启动验证过程。如果合约满足规则定义的所有条件，Certora Prover 将确认验证运行成功，未检测到任何违规，如下图所示：

验证结果确认了 RareToken 合约中的所有函数都针对 totalSupplyIsConstant() 规则进行了测试。每个函数旁边的绿色勾号（✅）表示该规则在所有可能的执行情况下都成立，从而确保 totalSupply 变量在任何函数调用下都保持不变。

理解参数化规则的作用范围

关于参数化规则，需要理解的一个重要点是，它被设计为每次只分析一个函数调用的效果。这意味着 Prover 并不检查一系列调用之后会发生什么——它只关注对某一个函数的单次调用，以及紧接着的合约状态是什么样子的。

当 Prover 评估一条参数化规则时，会发生以下情况：

1. 它从一个初始合约状态开始——这是没有任何函数被调用之前的状态。
2. 它从合约中选择一个函数并检查——在给定的前置条件下——是否存在任何有效的输入会导致违反规则的断言。
3. 这个过程会对合约中的每一个函数重复进行。
4. 只有当没有任何函数（在任何有效输入下）导致断言失败时，规则才能通过验证（✅）。

为了更清晰地理解参数化规则的评估过程，考虑一下 Counter 合约。它包含两个 external 函数：increment()（用于增加 count）和 transferOwnership()（用于更新 owner 地址）。加入所有权相关的功能仅仅是为了引入额外的函数，这样我们就可以观察当参数化规则应用于多种函数类型时会表现出怎样的行为。

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

contract Counter {
    uint256 public count;
    address public owner;
    
    // Define custom errors
    error Unauthorized();
    error InvalidAddress();
    
    // Emit events for important state changes
    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);
    event CountUpdated(uint256 newCount);

    constructor() {
        owner = msg.sender;
        emit OwnershipTransferred(address(0), msg.sender);
    }
    
  
  modifier onlyOwner() {

        if (msg.sender != owner) revert Unauthorized();
        _;
    }

    function increment() external {
        count += 1;
        emit CountUpdated(count);
    }

    function transferOwnership(address _newOwner) external onlyOwner {
        if (_newOwner == address(0)) revert InvalidAddress();
        emit OwnershipTransferred(owner, _newOwner);
        owner = _newOwner;
    }
}

现在考虑下面的规范，它定义了一条名为 counterParametricCall() 的参数化规则。

Copy
rule counterParametricCall() {
    env e;

    require count(e) == 0;

    method f;
    calldataarg args;

    f(e,args);

    satisfy count(e) == 2 ;
}

由于我们的 counterParametricCall() 规则包含了 satisfy 语句 satisfy count(e) == 2;，我们是在问 Prover：从 count 为 0 的初始状态开始，是否至少有一种可能的方法可以达到 count 为 2 的状态。

但远不止于此——该规则还在 require 和 satisfy 语句之间包含了一个参数化函数调用（f(e, args)）。这就将问题从一般的可达性检查转变为更聚焦的查询：

“合约中**是否存在任何单一函数** f__**，使得当使用某些有效参数** args 执行一次时，它会将状态直接从 count == 0 转换为 count == 2？”

在我们的 Counter 合约的例子中，唯一可用的函数是 increment()，它每次调用会使计数器增加 1。由于没有函数可以在单次执行中使计数器增加 2，因此 Prover 找不到任何能满足 count(e) == 2 条件的函数。

因此，该规则将未通过验证，这是预期的正确结果——如下图所示：

非常关键的一点是，参数化规则仅仅孤立地分析一次 external 函数调用的效果。它不会检查一系列调用或单一交易中的复杂交互。例如，虽然上述规则证明了没有单一的调用可以使 count == 2，但如果另一个智能合约连续两次调用 increment() 函数，在一次交易中_确实_有可能达到 count == 2。该场景涉及在单一交易中发起的多次函数调用，这超出了本章的讨论范围。

然而，即使我们放宽规则去检查 satisfy count(e) == 1 而不是 satisfy count(e) == 2，该规则仍然不会通过，如下所示：

这是因为，在底层，当评估参数化规则时，Prover 会为合约中的每个函数创建一个规则实例。它会针对断言单独测试这些规则实例。当且仅当每个函数实例都满足 assert 和 satisfy 语句指定的所有条件时，该规则才算通过验证。如果哪怕只有一个函数未能符合标准，整个规则就会失败。

在 Counter 合约中，只有 increment() 函数修改 count 变量，使其成为唯一可能满足 satisfy 条件（例如 count == 1）的候选者。相比之下，transferOwnership() 以及 getter 函数 count() 和 owner() 根本不影响 count。当 Prover 评估这些函数的规则时，它发现它们中没有一个能够产生所需的状态改变。结果，它们的规则实例失败了，而且由于必须所有实例都通过才能使整个规则成功，因此整个规则未通过验证。

总结

这就是我们如何使用参数化规则来验证预期在所有函数执行过程中都成立的智能合约属性。然而，在某些情况下，我们可能希望将某些函数从规则中排除或对它们进行不同的处理。在下一章中，我们将学习如何微调参数化规则，以便根据特定的函数调用有选择性地强制执行约束。

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