在上一章中，我们了解到规范（specification）是一段用 CVL 编写的代码，用于描述智能合约的预期行为。规范主要由以下部分组成：
- 规则（Rules）
- 方法块（The Methods Block）
这些规则的主体和方法块由 CVL 语句（statements）组成。
在本章中，我们将学习 CVL 语句。
CVL 语句简介
根据 Certora 的官方文档，“语句描述了 Prover 在评估规则时所模拟的步骤。” 换句话说，语句定义了条件和操作，用于指导 Certora Prover 如何根据规则测试智能合约。
CVL 提供了多种用于编写规则的语句，但目前我们将重点关注以下几种：
require– 用于指定在运行规则之前必须成立的条件。assert– 用于指定在所有执行路径中都必须成立的条件，以便将规则评估为已验证（verified）。satisfy– 用于断言至少存在一条有效的执行路径。
“Execution Path”（执行路径）是什么意思？
在验证智能合约时，Prover 会探索各种可能的状态和转换，以检查规则在所有场景下是否都成立。执行路径（execution path）指的是合约在验证过程中经历的特定函数调用和状态变更序列。
理解 assert 的用法
CVL 中的 assert 语句用于验证合约执行期间必须为真的条件。每条规则都必须以 assert 或 satisfy 语句结束。
如果规则没有以 assert 或 satisfy 语句结束，Prover 就无法确定应该检查什么条件，从而导致错误。例如，考虑运行上一章中的以下规范，并将 assert 语句注释掉：
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;
}
由于上述两条规则都没有在末尾包含 assert 语句，Prover 无法确定要验证哪个属性。这会导致如下所示的错误 “last statement of the rule …… is not an assert or satisfy command (but must be)”。
assert 语句以表达式的形式包含合约的预期状态，并带有一个可选的用于描述该表达式的消息字符串，如下所示：
assert Expression, "An Optional Message String";
//OR
assert Expression;
在验证期间，如果所有执行路径都满足其 assert 语句中表达的条件，则规则通过验证。然而，如果在任何执行路径中任何 assert 语句的评估结果为假（false），则该规则被视为遭到违反（violated）。
为 Counter 合约定义验证基准
为了更好地理解 assert 语句的工作原理，让我们回顾一下之前的 Counter 示例，并更详细地探讨其功能。
//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {
uint256 public count;
function increment() external {
count++;
}
}
如果上述合约在测试期间满足以下条件，则可以认为它运行正确：
- 合约部署后，
count变量应该正确初始化。 - 调用
increment()时，count的值应该增加 1。
将预期转化为断言检查
现在，假设我们想要对 Counter 合约的预期进行形式化验证。为此，我们定义一个名为 checkCountValidity() 的规则，它确保 count 变量从零开始，并在每次函数调用时正确递增。
rule checkCountValidity(.......)
以下是该规则逐步执行的过程：
- 捕获初始状态： 我们首先使用
count()getter 获取 count 的当前值，并将其存储在一个名为PrecallCountValue的变量中。这为我们提供了一个发生任何修改之前的参考点。
rule checkCountValidity() {
// Grabbing the initial state of the count variable
uint256 PrecallCountValue = count();
}
- 执行递增操作： 然后我们调用
increment()函数三次以增加计数器。
rule checkCountValidity() {
// Grabbing the initial state of the count variable
uint256 PrecallCountValue = count();
// Call to increment()
increment();
increment();
increment();
}
- 获取更新后的状态： 执行完
increment()调用后，我们获取count的新值并将其存储在PostcallCountValue中。这允许我们比较函数执行前后的状态。
rule checkCountValidity() {
// Grabbing the initial state of the count variable
uint256 PrecallCountValue = count();
// Call to increment()
increment();
increment();
increment();
// Grabbing the state of count after the increment() calls
uint256 PostcallCountValue = count();
}
- 验证初始状态： 为了确保正确性，我们使用
assert语句来验证 count 最初是否为 0——确认合约从一个已知的、预期的状态开始。
rule checkCountValidity() {
// Grabbing the initial state of the count variable
uint256 PrecallCountValue = count();
// Call to increment()
increment();
increment();
increment();
// Grabbing the state of count after the increment() calls
uint256 PostcallCountValue = count();
// Assertions
assert PrecallCountValue == 0;
}
- 验证递增行为： 最后，我们断言
count准确增加了 3，确认每次对increment()的调用都成功为其值加了 1。
rule checkCountValidity() {
// Grabbing the initial state of the count variable
uint256 PrecallCountValue = count();
// Call to increment()
increment();
increment();
increment();
// Grabbing the state of count after the increment() calls
uint256 PostcallCountValue = count();
// Assertions
assert PrecallCountValue == 0;
assert PostcallCountValue == PrecallCountValue + 3;
}
我们可以看到如何使用 assert 语句来强制执行我们对合约行为的预期。
预期结果是什么？
乍一看，您可能会认为 checkCountValidity 能够通过验证，因为：
- 默认初始化：
Counter合约没有显式初始化count状态变量，所以 Solidity 自动将其设置为 0。因此，当规则使用count()检索初始值时，它应该返回 0，使得断言PrecallCountValue == 0对任何执行路径都有效。 - 递增行为： 每次调用
increment()都会使count变量增加 1。由于规则调用了increment()三次，count的预期最终值应该是PrecallCountValue + 3。因此，断言PostcallCountValue == PrecallCountValue + 3有望在任何执行路径上都成立。
运行验证
然而，在您运行验证过程时，会遇到一个意外的结果，如下所示。
在上面的结果中，我们可以清楚地看到 Prover 未能验证 checkCountValidity() 规则。这表明以下条件中至少有一个评估为假，导致违反了规则：
assert PrecallCountValue == 0assert PostcallCountValue == PrecallCountValue + 3
当发生违规时，Prover 会生成一份详细说明该违规的报告，包含关于哪个断言失败、相关变量值以及导致失败的执行步骤等信息。
通过反例解读验证失败
为了理解该违规，Certora Prover 提供了反例（counterexamples）。简单来说，反例（counterexample）就是一条特定的执行路径，在该路径上规则的验证失败。
要查看被违反规则的反例，请在报告页面上点击被违反的规则名称（checkCountValidity），以获得类似于下方的视图。
这样做之后，它会显示该规则的参数和变量的值（在右侧），以及一个调用追踪（在中间），如下所示。
在调查违规情况时，调用追踪（call trace）非常有用，因为它提供了关于规则执行开始时状态变量的详细信息，并在整个执行过程中跟踪这些变量的更新情况，如下所示：
在 Certora Prover 提供的反例中，我们可以清楚地看到我们的规则验证失败，因为规则期望 count 从 0 开始，但实际上它却从 10 开始，这导致了 assert PrecallCountValue == 0 失败。
这提出了一个重要问题：为什么 count 被设置成了 10，而不是预期的默认值 0？ 要理解这一点，我们需要了解 Solidity 和 CVL 在处理未初始化变量时的不同方式。
为什么 count 的值被设置为 10 而不是 0？
众所周知，如果 Solidity 智能合约没有显式地初始化状态变量，系统会根据它的类型自动赋予一个默认值。例如：
- 对于
uint256，默认值是0。 - 对于
bool，默认值是false。 - 对于
address，默认值是零地址。
与 Solidity 不同，CVL 不会自动为变量分配默认值。相反，CVL 中未初始化的变量保持不受约束（unconstrained）状态，这意味着在验证期间，它们可以呈现其定义范围内的任何可能值。这牵涉到一个至关重要的概念：CVL 规则不会从合约特定的初始部署状态（如 Solidity 执行通常假设的那样）开始验证，而是从一个任意（arbitrary）状态开始。 这是一个关键的区别，也是形式化验证的一个基本层面。
由于这种行为，count 的初始值在验证期间被设置为了 10，这导致了规则失败，因为我们期望 count 从 0 开始。
理解 require 的用法
如上所述，Prover 在验证过程中会为状态变量分配任意值，如果规则假定使用 Solidity 的默认值，这可能会导致出现意外的初始值并引起断言失败。
在这种情况下，我们可能希望在我们的验证设置中显式定义对状态变量的约束，确保在执行规则之前它们以预期的值开始。这就是 CVL 中 require 语句发挥作用的地方。
CVL 中的 require 语句用于为规则指定前提条件，确保在将规则视为有效之前满足某些条件。
当规则中包含 require 语句时，它会充当一个过滤器，告诉 Prover 忽略任何不满足指定条件的执行路径。这意味着 Prover 只会考虑 require 表达式评估为真的场景，从而有效地将所有其他场景排除在分析之外。
例如，我们可以在 checkCountValidity 规则中使用 require 语句，将 count 的初始值约束为零，如下所示：
rule checkCountValidity() {
// We just added this
require count() == 0;
// Grabbing the initial state of the count variable
uint256 PrecallCountValue = count();
//Call to increment()
increment();
increment();
increment();
//Grabbing the state of count after the increment() calls
uint256 PostcallCountValue = count();
// Asserting that the initial value of count is 0
assert PrecallCountValue == 0;
assert PostcallCountValue == PrecallCountValue + 3;
}
如果您在进行上述更改后重新运行 Prover，并打开终端中打印的验证链接，您将得到一条已验证通过的规则，如下所示。
这一次，我们可以看到 Prover 已经成功验证了我们的规则。这是因为，有了 require 约束，Prover 会忽略任何 count 初始值不为零的执行路径。
默认情况下，Prover 不会为已验证通过的规则提供调用追踪，因为满足规则条件的有效执行追踪数量可能极为庞大。既然已验证的规则确认了不存在反例，那么生成并显示所有可能的有效追踪就既无必要也不切实际。
理解 satisfy 的用法
如前所述，当规则成功验证时，Prover 不会生成调用追踪。然而，CVL 提供了 satisfy 语句，它允许您生成一条满足 require 和 assert 语句所强制执行的所有条件的执行追踪。这在您想要确认特定场景是否能在合约逻辑内发生时特别有用。
例如，我们可以编写一条使用 satisfy 语句的规则来验证：
- 至少存在一条执行路径，让用户在存入流动性并铸造 LP 代币后，可以完全提取其流动性。
- 至少存在一条执行路径，如果借款人的抵押品价值跌破指定阈值，其头寸就会被清算。
当规则包含 satisfy 语句时，Prover 会检查是否至少存在一条有效执行路径满足该条件。虽然可能存在多条这样的路径，但如果找到了，只会生成一条满足条件的追踪。根据结果，该规则的分类如下：
- Verified Rule（验证通过的规则）： 如果至少有一条有效的执行满足 satisfy 语句，Prover 将该规则报告为 verified。
- Violated Rule（违规的规则）： 如果没有任何执行路径满足 satisfy 语句，Prover 将该规则报告为 violated。
在规则中使用 satisfy
为了理解 satisfy 语句的工作原理，请考虑下面的规范，它包含了一条以 satisfy 语句结尾的 searchValidExecution() 规则。
methods {
function count() external returns(uint256) envfree;
function increment() external envfree;
}
rule searchValidExecution {
increment();
increment();
increment();
satisfy count() == 8;
}
由于规则 searchValidExecution 以 satisfy 语句结束，它指示 Prover 探索可能的执行路径，并确定是否存在连续三次 increment() 调用使得 count() 的值达到 8 的序列。如果找到了这样的路径，Prover 将报告该规则被验证通过（verified）。否则，它将报告该规则被违反（violated）。
要检查规则 searchValidExecution 是否成立，请运行 Prover 并在浏览器中打开验证链接以查看结果。
上述结果表明 Certora Prover 已成功验证了该规则。这意味着它找到了至少一条满足 satisfy 语句的执行路径。具体来说，Prover 识别出了一种在连续调用三次 increment() 后 count() 达到 8 的状态。
这一结果符合预期，因为在理想情况下，如果初始值为 5（假设每次调用使计数加 1），那么 count() 的值可以在连续三次 increment() 调用后达到 8。既然规则是在寻找一条有效的执行路径，Prover 确认了其存在，从而实现了成功的验证。
使用 Prover 求解并验证线性方程组
因为 Prover 在处理包含 satisfy 语句的规则时仅评估单一执行路径，所以它充当了求解器的角色，能够确定满足给定约束的输入值。为了演示这种能力，让我们使用 satisfy 来寻找方程组的解。
例如，考虑以下方程：
现在，假设我们想找到满足这两个方程的 和 的整数值。为了实现这一点，我们首先需要定义一个 Solidity 函数来对该方程组进行编码**：**
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Math {
function eqn(uint256 x, uint256 y) external pure returns (bool) {
return (2 * x + 3 * y == 22) && (4 * x - y == 2);
}
}
定义好 Solidity 函数后，我们可以创建一条规则来指示 Prover 搜索满足约束的 和 的有效值，如下所示：
methods {
function eqn(uint256, uint256) external returns (bool) envfree;
}
rule checkEqn() {
uint256 x;
uint256 y;
satisfy eqn(x, y) == true;
}
或者，可以将变量直接定义在规则声明中，而不是在规则主体内声明，如下所示：
rule checkEqn(uint256 x, uint256 y) {
satisfy eqn(x, y) == true;
}
当规则执行时，Prover 会尝试寻找使得函数返回 true 的 和 的值。在这个例子中，正确的整数解是 且 。
此外，如果以某种方式修改方程使其变得不一致——例如定义了平行线——Prover 会检测出不存在解。考虑修改后的方程组：
由于第二个方程只是第一个方程的倍数，但具有不同的常数，该方程组没有解，因为这两条线现在是平行的且永远不会相交。等效的 Solidity 函数为：
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Math {
function eqn(uint256 x, uint256 y) external pure returns (bool) {
return (2 * x + 3 * y == 22) && (4 * x + 6 * y == 50);
}
}
当我们针对这个修改后的函数重新运行 checkEqn() 规则时，验证结果表明 Prover 正确地识别出了不存在有效解。
上述结果凸显了 Prover 的能力：不仅能在有效解存在时找到它们，还能检测并确认一组约束何时本质上不可满足，例如在方程不一致或平行的情况下。
使用 satisfy 语句时的主要注意事项
在任何规则中使用 satisfy 语句时，都有一些重要的细微差别需要牢记：
- 如果一条规则包含多个
satisfy语句，Prover 只有在所有执行到的 satisfy 语句都在至少一条执行路径上成立时，才会将其报告为已验证（verified）；否则，该规则将被视为遭到违反（violated）（在默认的 Prover 模式下），如下所示：
- 位于未执行的条件分支上的
satisfy语句不需要成立，因为它在验证期间永远不会被访问到。Prover 会独立验证每条执行路径，并报告已执行路径的结果，如下所示。
assert 和 satisfy 之间的区别
乍一看，assert 和 satisfy 语句在功能上似乎很相似，因为它们都用于验证规则中的条件。然而，它们的目的和用途却大不相同，如下所示：
assert 语句（Statement） |
satisfy 语句（Statement） |
|---|---|
| 确保一个条件在所有可能的执行中始终成立（always holds）。 | 检查是否至少存在一条有效执行路径使得条件成立。 |
| 如果条件一旦失败，该规则被标记为遭到违反（violated）。 | 如果没有有效执行满足条件，该规则被认定为遭到违反（violated）。 |
| 寻找反例（counterexamples）（规则失败的场景）。 | 寻找见证（witnesses）（规则成功的场景）。 |
结论
在本章中，我们探讨了 CVL 语句如何在验证期间指导 Certora Prover。我们学习了 assert 如何跨所有执行路径强制执行属性，require 如何约束 Prover 考虑的状态，以及 satisfy 如何证明有效执行路径的存在。理解这些语句以及 Prover 如何对任意状态进行推理，对于编写正确而有效的 CVL 规则至关重要。
本文是使用 Certora Prover 进行形式化验证系列文章的一部分