方法属性介绍

Formal Verification with Certora

Method Properties 介绍

模块 1：规则和基本 CVL 语法规则和基本 CVL 语法

上次更新于 2026 年 2 月 13 日

介绍

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

• 任何合约的 owner 都应该保持不变，除非 owner 调用 changeOwner 或 renounceOwnership。
• ERC-20 代币的总供应量应该保持不变，除非代币正在铸造或销毁。

我们如何处理这类属性通常成立但根据函数有已知例外的情况？或者如果你只是想完全从一般不变量检查中排除某些管理方法呢？

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

什么是方法属性？

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

Copyrule someParametricRule() {
    env e;

    method f;
    calldataarg args;
    f(e, args);

    assert property_1;
}

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

在 CVL 中，方法属性是可以通过 method 变量（例如 f）使用类似字段的语法（例如 f.propertyName）访问的属性。这些属性提供了关于 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 行为的规则时，例如可支付要求或对低级调用的特殊处理，这很有帮助。
• 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，使用参数化设置调用任意方法，然后根据调用的函数强制执行预期行为：

Copyrule totalSupplyIntegrityCheck() {

    env e;

    // 步骤 1：记录初始状态
    mathint supplyBefore = totalSupply(e);

    // 步骤 2：执行任意函数
    method f;
    calldataarg args;
    f(e, args);

    // 步骤 3：记录更新状态
    mathint supplyAfter = totalSupply(e);

    // 步骤 4：函数特定的断言
    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，这意味着它们只从区块链状态读取并且不修改任何内容。因此，对这些函数运行状态更改规则并没有多大意义，也无助于我们捕获有意义的 bug。

尽管验证它们在技术上没有错，但它会增加额外的计算工作并减慢过程。这就是为什么在不相关时将不影响合约状态的函数排除在验证之外很重要。这时 filtered 块就派上用场了。

filter 块允许我们根据 isView、isPure 等方法属性选择性地包含或排除方法不被参数化规则分析。

使用 filtered 块排除视图函数

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

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

    // 步骤 1：记录初始状态
    mathint supplyBefore = totalSupply(e);

    // 步骤 2：执行任意函数
    f(e, args);

    // 步骤 3：记录更新状态
    mathint supplyAfter = totalSupply(e);

    // 步骤 4：函数特定的断言
    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";
    }
}

在上述规则中，filtered {} 块内的 f -> !f.isView 行充当过滤器，它告诉证明器：“只对 f.isView 为假的函数运行此规则。”换句话说，它将所有标记为 view 的函数排除在验证之外。

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

在参数化规则中使用 filter 块有助于我们实现两件事：

1. 它通过跳过保证不会更改合约状态的不相关函数来减少计算开销。
2. 它简化了验证输出，使我们能够只关注状态更改函数的结果。

总结

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

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

• 原文链接： rareskills.io/post/certo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～