在上一章中，我们了解到要使用 Certora Prover 进行形式化验证，我们需要向 Prover 提供以下关键项：
- 智能合约（.sol 文件）
- 规范（.spec 文件）
在本章中，我们将讨论规范的确切含义以及如何编写规范。
什么是规范（Specification）？
在 Certora 中，规范是一段使用 Certora Verification Language (CVL) 编写的代码，它定义了一组被验证合约必须保持或遵守的规则。
一个 Certora 规范或 .spec 文件必须至少包含两个组件：
- 一个或多个规则（rules）
- 一个 Methods 块（Methods Block）
还有其他组件，但现在我们将重点关注这些，并在后续使用时再介绍其余部分。
理解规则（Rules）
规则定义了智能合约中函数调用预期的“调用前和调用后”行为。它使用 rule 关键字定义，后跟其名称，如下所示：
rule nameOfRule{}
在 CVL 中，编写规则主要使用以下三个基础概念：
- 前置条件要求（可选）：这指定了 Prover 在何种条件下应该评估某条规则。它是使用
require语句指定的。 - 动作（Action）： 改变合约状态的方法调用。
- 调用后预期： 这部分指定了动作执行后合约的预期状态。它是使用
assert语句指定的。
注意：我们将在下一章详细讨论 require 和 assert 语句。
为了更好地理解上述概念，请查看下方的 Counter 合约。
// 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() 函数进行形式化验证而编写的规则。
rule 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 合约的完整性。
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;
}
然而，我们的规范文件仍然缺少 Methods 块。让我们在将其提交给 Prover 进行验证之前添加它。
Methods 块及其用途
Methods 块包含了验证期间规则将调用的合约方法列表。您可以将其视为类似 Solidity 中的接口或 ABI —— 它告诉 Prover 有哪些函数存在、它们的签名是什么样的，以及如何调用它们。与纯 Solidity 相比，Certora 的版本有时会有一些额外的语法。
Methods 块使用 methods 关键字定义，如下所示：
methods {
// Contract methods entries go here
}
Methods 块中的每个条目应遵循以下语法：
- 每个条目必须以 function 关键字开头来定义方法。
- 指定的方法名称必须与合约中显示的一模一样。
- 在括号内列出输入参数，多个输入之间用逗号分隔。如果该方法不需要任何输入，请保留空括号。
- 添加可见性修饰符，对于我们的目标而言，所有方法都应为
external。更高级的规范可能会对内部函数进行摘要（summarize），我们将在后面介绍。 - 如果方法有返回值，请使用
returns关键字后跟返回类型。如果没有返回值，则不需要这部分。 - 添加一个可选的标签，如
envfree（我们将在使用时讨论其他标签）。 - 每个方法声明以分号（;）结束。
需要着重注意的是，将函数添加到 Methods 块中并不会使验证变得更快或更有效，除非这些函数被标记为 envfree、optional，或者具有 summary（摘要）。如果这些条件都不满足，添加函数将不会产生任何影响，并且验证器很可能会在报告中对此发出警告。
为了保持简单易懂，在本章中我们将只关注 envfree。我们将在单独的章节中探讨 optional 和 summarization。
何时使用 envfree 标签？
当 Methods 块中的某个方法的执行不依赖于 Solidity 的全局变量（例如 msg.sender、block.number 或 tx.origin）时，该方法可被声明为 envfree。
例如，请看下方的 add() 函数：
function add(uint256 x, uint256 y) external returns (uint256) {
return x + y;
}
由于 add() 专门针对其输入参数进行操作，并且在执行时不需要访问任何诸如 block.timestamp、msg.sender、msg.value 或 tx.origin 这样的全局区块链状态，这意味着我们可以在 Methods 块中将其声明为 envfree，如下所示：
methods {
add(uint256, uint256) external returns(uint256) envfree;
}
相反，某些函数在执行时需要访问全局区块链状态，因此无法被声明为 envfree。例如，下方的 balance() 函数用于获取调用者的余额：
function balance() external view returns(uint256) {
return balances[msg.sender];
}
由于 balance() 依赖于 msg.sender，它无法被声明为 envfree。下面是我们应如何在 Methods 块中定义它：
methods {
balance() external returns(uint256);
}
将 Methods 块添加到我们的 spec 中
由于我们的规则（checkIncrementCall 和 checkCounter）调用了 Counter 合约的 count()、increment() 和 decrement() 方法，因此我们的规范的 Methods 块应列出这些函数，如下所示：
methods {
function count() external returns(uint256) envfree;
function increment() external envfree;
function decrement() external envfree;
}
这些函数在执行时都不需要访问 Solidity 的全局变量，因此我们将它们标记为 envfree。如果合约中还有其他在我们的规范中未使用的函数，我们不需要将它们包含在 Methods 块中。
运行验证
要验证上面讨论的规则，请按照以下说明进行操作：
- 打开终端并确保您位于我们在上一章中创建的
certora-counter目录中。 - 在 VS Code 或您选择的任何其他代码编辑器中打开
certora-counter目录。 - 创建两个空文件：在
contracts子目录中创建Counter2.sol，在specs子目录中创建counter-2.spec。 - 将下方的智能合约复制并粘贴到
Counter2.sol中。
// 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中。
methods {
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 虚拟环境：
source certora-env/bin/activate
- 将 Certora 访问密钥作为环境变量加载到您的终端中：
source .profile # For Bash
# OR
source .zshenv # For Zsh
- 运行以下命令以设置正确的 Solidity 编译器版本：
solc-select use 0.8.25
- 最后，运行以下命令将规范和合约提交给 Prover 进行验证：
certoraRun contracts/Counter2.sol:Counter --verify Counter:specs/counter-2.spec
理解验证结果
如果 Prover 成功编译代码且没有报错，它将在您的终端中打印出验证结果的链接。
要查看验证结果，请使用浏览器打开终端中打印的链接。结果应该与下图类似：
在我们的示例中，它显示了三条规则的结果：
checkCounter：这显示了来自我们 spec 的checkCounter规则的验证结果。checkIncrementCall：这显示了来自我们 spec 的checkIncrementCall规则的验证结果。envfreeFuncsStaticCheck：当 Methods 块包含标记为envfree的函数时，Prover 会验证它们是否不依赖于 Solidity 的全局变量。此验证的结果将作为envfreeFuncsStaticCheck发布。
绿色的复选标记（✅）表示 Prover 没有发现任何违规（violations），这意味着我们的规则已成功通过验证。如果发生违规，则会显示红色的叉号（❌）。
尽管所有规则都已通过验证，但这并不意味着整个合约就没有 bug。代码的其他部分可能存在漏洞。也有可能是我们的 spec 并没有涵盖我们所有的预期。例如，我们并没有具体说明当计数器为 0 时调用 decrement() 会发生什么。在后续的章节中，我们将展示如何表达比我们在这里讨论的更复杂的规则。
结论
在本章中，我们探讨了 .spec 文件的剖析结构，重点介绍了用于接口定义的 Methods 块和用于逻辑测试的规则块。我们还了解了像 envfree 这样的标签如何帮助优化验证过程。在下一章中，我们将在此基础上详细研究 require 和 assert 语句。
本文是使用 Certora Prover 进行形式化验证系列文章的一部分