理解 Certora CVL 中的规范文件

Formal Verification with Certora

理解 Certora CVL 中的 Spec 文件

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

最后更新于 2026 年 2 月 13 日

在上一章中，我们了解到，要使用 Certora Prover 进行形式化验证，我们需要向 Prover 提供以下关键项：

1. 智能合约（.sol 文件）
2. 规范（.spec 文件）

在本章中，我们将讨论规范究竟意味着什么以及如何编写规范。

什么是规范？

在 Certora 中，规范是使用 Certora Verification Language (CVL) 编写的一段代码，它定义了被验证合约必须遵守或遵循的一组规则。

Certora 规范或 .spec 文件必须至少包含两个组件：

1. 一条或多条规则
2. 一个方法块

还有其他组件，但目前，我们将专注于这些，并在使用它们时介绍其余部分。

理解规则

规则定义了智能合约中函数调用预期的“之前和之后”行为。它使用 rule 关键字定义，后跟其名称，如下所示：

Copyrule nameOfRule{}

在 CVL 中，规则是使用以下三个基本概念编写的：

1. 前置条件要求（可选）：这指定了 Prover 应在何种条件下评估规则。它使用 require 语句指定。
2. 操作：一个改变合约状态的方法调用。
3. 调用后预期：这部分指定了操作执行后合约的预期状态。它使用 assert 语句指定。

注意：我们将在下一章中更详细地讨论 require 和 assert 语句。

为了更好地理解上面讨论的概念，请考虑下面的 Counter 合约。

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

contract Counter {
    uint256 public count;

    // Increment the count
    // 增加计数
    function increment() public {
        count += 1;
    }

    // Decrement the count
    // 减少计数
    function decrement() public {
        count -= 1;
    }

}

现在考虑下面编写的规则，用于形式化验证 Counter 合约的 increment() 函数。

Copyrule checkIncrementCall() {

    // Precall Requirement
    // 调用前置要求
    require count() == 0;

    // Call OR Action
    // 调用或操作
    increment();

    // Post-call Expectation
    // 调用后预期
    assert count() == 1;

}

在我们的 checkIncrementCall() 规则中：

• require count() == 0 这行通过指示 Prover 仅在 count 的初始值为零时才考虑此规则，定义了前置条件要求。
• increment() 这行通过调用合约上的 increment() 函数执行状态转换。这代表了正在测试的操作。
• assert count() == 1 这行定义了调用后预期，它指定了操作执行后的预期状态。在这里，它确保在对初始设置为零的计数器调用 increment() 后，计数器的值更新为 1。

我们需要将这三者放在一起，因为：

• 如果没有操作，就没有什么可测试的，因为合约的状态保持不变。
• 如果我们不包含后置条件检查，我们实际上没有验证任何东西。断言（assert 语句）检查确保合约的状态转换符合我们的预期。
• 如果没有前置条件，规则可能适用于意外情况。

重要的是要注意，前置条件是可选的。应谨慎使用它们，因为 它们可能会 排除需要验证的重要场景。

有些规则可以在没有任何前置条件要求的情况下实现。例如，下面的规则通过验证对 increment() 和 decrement() 的顺序调用是否导致 count 值不变来检查我们的 Counter 合约的完整性。

Copyrule checkCounter() {

    //Retrieval of Pre-call value
    // 获取调用前的值
    uint256 precallCountValue = count();

    // Call
    // 调用
    increment();
    decrement();

    //Retrieval of Post-call value
    // 获取调用后的值
    uint256 postcallCountValue = count();

    //Post-call Expectation
    // 调用后预期
    assert postcallCountValue == precallCountValue;
}

然而，我们的规范文件仍然缺少方法块。让我们在提交给 Prover 进行验证之前添加它。

方法块及其用途

方法块包含规则在验证期间将调用的合约方法的列表。你可以将其视为 Solidity 中的接口或 ABI——它告诉 Prover 哪些函数存在、它们是什么样子以及如何调用它们。Certora 的版本有时会比纯 Solidity 有一些额外的语法。

方法块使用 methods 关键字定义，如下所示：

Copymethods {
// Contract methods entries go here
// 合约方法条目在此处
}

方法块中的每个条目应遵循以下语法：

• 每个条目必须以 function 关键字开头来定义方法。
• 准确指定方法名称，使其与合约中出现的一致。
• 在括号内列出输入参数，多个输入用逗号分隔。如果方法不接受任何输入，则将括号留空。
• 添加一个可见性修饰符，对于我们的目的，所有方法都应为 external。更高级的规范可能会总结内部函数，我们将在后面介绍。
• 如果方法返回一个值，使用 returns 关键字后跟返回类型。如果没有返回值，则不需要这部分。
• 添加一个可选标签，如 envfree（我们将在使用其他标签时讨论它们）。
• 每个方法声明以分号 (;) 结尾。

非常重要的一点是，将函数添加到方法块不会使验证更快或更有效，除非这些函数被标记为 envfree、optional 或具有摘要。如果这些条件都不满足，添加该函数将没有影响，并且验证器可能会在报告中发出警告。

为了保持简单易懂，本章我们将只关注 envfree。我们将在单独的章节中探讨 optional 和 summarization。

何时使用 envfree 标签？

方法块中的方法在其执行不依赖于 Solidity 的全局变量（例如 msg.sender、block.number 或 tx.origin）时被声明为 envfree。

例如，考虑下面的 add() 函数：

Copyfunction add(uint256 x, uint256 y) external returns (uint256) {
    return x + y;
}

由于 add() 仅对其输入参数进行操作，并且在其执行过程中不需要访问任何全局区块链状态（如 block.timestamp、msg.sender、msg.value 或 tx.origin），这意味着我们可以在方法块中将其声明为 envfree，如下所示：

Copymethods {
    add(uint256, uint256) external returns(uint256) envfree;
}

相比之下，有些函数在其执行过程中需要访问全局区块链状态，因此不能声明为 envfree。例如，下面的 balance() 函数检索调用者的余额：

Copyfunction balance() external view returns(uint256) {
    return balances[msg.sender];
}

由于 balance() 依赖于 msg.sender，它不能声明为 envfree。下面是我们应该如何在方法块中定义它：

Copymethods {
    balance() external returns(uint256);
}

将方法块添加到我们的 spec

由于我们的规则（checkIncrementCall 和 checkCounter）调用了 Counter 合约的 count()、increment() 和 decrement() 方法，因此我们规范的方法块应列出这些函数，如下所示：

Copymethods {
    function count() external returns(uint256) envfree;
    function increment() external envfree;
    function decrement() external envfree;
}

这些函数在执行时都不需要访问 Solidity 的全局变量，因此我们将其标记为 envfree。如果合约有其他未在我们的规范中使用的函数，我们不需要将它们包含在方法块中。

运行验证

要验证上面讨论的规则，请按照以下说明进行操作：

• 打开终端，确保你位于上一章中创建的 certora-counter 目录中。
• 在 VS Code 或你选择的任何其他代码编辑器中打开 certora-counter 目录。
• 创建两个空文件：contracts 子目录中的 Counter2.sol 和 specs 子目录中的 counter-2.spec。
• 将下面的智能合约复制并粘贴到 Counter2.sol 中。

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

contract Counter {
    uint256 public count;

    // Increment the count
    // 增加计数
    function increment() public {
        count += 1;
    }

    // Decrement the count
    // 减少计数
    function decrement() public {
        count -= 1;
    }

}

• 将下面的规范复制并粘贴到 counter-2.spec 中。

Copymethods {
    function count() external returns(uint256) envfree;
    function increment() external envfree;
    function decrement() external envfree;
}

rule checkIncrementCall() {

    //Precall Requirement
    // 调用前置要求
    require count() == 0;

    // Call OR Action
    // 调用或操作
    increment();

    // Post-call Expectation
    // 调用后预期
    assert count() == 1;

}
rule checkCounter() {

    //Retrieval of Pre-call value
    // 获取调用前的值
    uint256 precallCountValue = count();

    // Call
    // 调用
    increment();
    decrement();

    //Retrieval of Post-call value
    // 获取调用后的值
    uint256  postcallCountValue = count();

    //Post-call Expectation
    // 调用后预期
    assert postcallCountValue == precallCountValue;
}

• 在你的终端中运行以下命令激活 Python 虚拟环境：

Copysource certora-env/bin/activate

• 在你的终端中将 Certora 访问密钥加载为环境变量：

Copysource .profile  # For Bash
## OR
source .zshenv  # For Zsh

• 通过运行以下命令设置正确的 Solidity 编译器版本：

Copysolc-select use 0.8.25

• 最后，通过运行以下命令将规范和合约提交给 Prover 进行验证：

CopycertoraRun contracts/Counter2.sol:Counter --verify Counter:specs/counter-2.spec

理解验证结果

如果 Prover 成功编译代码且没有错误，它将在你的终端中打印验证结果链接。

要查看验证结果，请使用浏览器打开终端中打印的链接。结果应类似于下图：

在我们的例子中，它显示了三条规则的结果：

• checkCounter：这显示了我们 spec 中 checkCounter 规则的验证结果。
• checkIncrementCall：这显示了我们 spec 中 checkIncrementCall 规则的验证结果。
• envfreeFuncsStaticCheck：当方法块包含标记为 envfree 的函数时，Prover 会验证它们是否不依赖于 Solidity 的全局变量。此验证的结果发布为 envfreeFuncsStaticCheck。

绿色勾号 (✅) 表示 Prover 未发现任何违规，这意味着我们的规则已成功验证。如果发生违规，将显示红色叉号 (❌)。

即使所有规则都经过验证，这并不意味着整个合约都没有 bug。代码的其他部分可能存在 bug。也可能是我们的 spec 没有捕捉到我们所有的预期。例如，我们没有指定当计数器为 0 时调用 decrement() 会发生什么。在接下来的章节中，我们将展示如何表达比这里讨论的更复杂的规则。

结论

在本章中，我们探讨了 .spec 文件的结构，重点关注用于接口定义的方法块和用于逻辑测试的规则块。我们还了解了 envfree 等标签如何帮助完善验证过程。在下一章中，我们将在此基础上，详细研究 require 和 assert 语句。

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

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