Certora 要求、断言和满足

Certora 形式化验证

Certora require、assert 和 satisfy

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

最后更新于 2026 年 2 月 13 日

在上一章中，我们了解到规范是使用 CVL 编写的一段代码，它描述了智能合约的预期行为。规范主要由以下部分组成：

• 规则
• 方法块（Methods Block）

这些规则的主体和方法块由 CVL 语句构成。

在本章中，我们将学习 CVL 语句。

CVL 语句简介

根据 Certora 的 官方文档，“语句描述了证明器在评估规则时模拟的步骤。” 换句话说，语句定义了指导 Certora 证明器如何根据规则测试智能合约的条件和操作。

CVL 提供了各种语句来编写规则，但目前，我们将重点关注以下内容：

• require – 用于指定在运行规则之前必须满足的条件。
• assert – 用于指定在所有执行路径中都必须满足的条件，规则才能被评估为已验证。
• satisfy – 用于断言至少存在一条有效的执行路径。

“执行路径”是什么意思？

在验证智能合约时，证明器会探索不同的可能状态和转换，以检查规则在所有场景下是否成立。一个执行路径指的是合约在验证期间经历的函数调用和状态变化的特定序列。

理解 assert 的用法

CVL 中的 assert 语句用于验证在合约执行期间必须为真的条件。每条规则都必须以 assert 或 satisfy 语句结束。

如果一条规则不以 assert 或 satisfy 语句结束，证明器将无法确定应该检查哪个条件，从而导致错误。例如，考虑运行上一章中的以下规范，并注释掉 assert 语句：

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;
}

由于上述两条规则都没有以 assert 语句结束，证明器无法确定要验证哪个属性。这会导致错误 "规则的最后一条语句……不是 assert 或 satisfy 命令（但必须是）"，如下图所示。

assert 语句包含合约的预期状态（以表达式的形式），以及一个描述表达式的可选消息字符串，如下图所示：

Copyassert Expression, "An Optional Message String";
//或
assert Expression;

在验证期间，如果所有执行路径都满足其 assert 语句中表达的条件，则规则通过。但是，如果任何执行路径中的任何 assert 语句评估为假，则该规则被视为已违反。

为 Counter 合约定义验证基准

为了更好地理解 assert 语句的工作原理，让我们重新审视早期的 Counter 示例，并更详细地探讨其功能。

Copy//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {

    uint256 public count;

    function increment() external {
        count++;
    }
}

如果上述合约在测试期间满足以下条件，则可以认为它工作正常：

1. 一旦合约部署，count 变量应正确初始化。
2. 当调用 increment() 时，count 的值应增加 1。

将期望转化为断言检查

现在，假设我们想要形式化验证对 Counter 合约的期望。为此，我们定义了一个名为 checkCountValidity() 的规则，它确保 count 变量从零开始，并且每次函数调用都会正确递增。

Copyrule checkCountValidity(.......)

以下是该规则如何逐步工作的：

1. 捕获初始状态：我们首先使用 count() getter 检索 count 的当前值，并将其存储在一个名为 PrecallCountValue 的变量中。这为我们提供了在任何修改发生之前的参考点。

   Copyrule checkCountValidity() {
   
       // Grabbing the initial state of the count variable
       // 获取 count 变量的初始状态
       uint256 PrecallCountValue = count();
   }

2. 执行增量：然后我们调用 increment() 函数三次以增加计数器。

   Copyrule checkCountValidity() {
   
       // Grabbing the initial state of the count variable
       // 获取 count 变量的初始状态
       uint256 PrecallCountValue = count();
   
       // Call to increment()
       // 调用 increment()
       increment();
       increment();
       increment();
   }

3. 检索更新后的状态：执行 increment() 调用后，我们获取 count 的新值并将其存储在 PostcallCountValue 中。这使我们能够比较函数执行前后的状态。

   Copyrule checkCountValidity() {
   
       // Grabbing the initial state of the count variable
       // 获取 count 变量的初始状态
       uint256 PrecallCountValue = count();
   
       // Call to increment()
       // 调用 increment()
       increment();
       increment();
       increment();
   
       // Grabbing the state of count after the increment() calls
       // 获取 increment() 调用后 count 的状态
       uint256 PostcallCountValue = count();
   
   }

4. 验证初始状态：为了确保正确性，我们使用 assert 语句来验证 count 最初为 0——确认合约从一个已知且预期的状态开始。

   Copyrule checkCountValidity() {
   
       // Grabbing the initial state of the count variable
       // 获取 count 变量的初始状态
       uint256 PrecallCountValue = count();
   
       // Call to increment()
       // 调用 increment()
       increment();
       increment();
       increment();
   
       // Grabbing the state of count after the increment() calls
       // 获取 increment() 调用后 count 的状态
       uint256 PostcallCountValue = count();
   
       // Assertions
       // 断言
       assert PrecallCountValue == 0;
   }

5. 验证增量行为：最后，我们断言 count 增加了正好 3，确认每次调用 increment() 都成功地将值增加了 1。

   Copyrule checkCountValidity() {
       // Grabbing the initial state of the count variable
       // 获取 count 变量的初始状态
       uint256 PrecallCountValue = count();
   
       // Call to increment()
       // 调用 increment()
       increment();
       increment();
       increment();
   
       // Grabbing the state of count after the increment() calls
       // 获取 increment() 调用后 count 的状态
       uint256 PostcallCountValue = count();
   
       // Assertions
       // 断言
       assert PrecallCountValue == 0;
       assert PostcallCountValue == PrecallCountValue + 3;
   }

我们可以看到我们如何使用 assert 语句来强制执行我们对合约行为的期望。

预期的结果是什么？

乍一看，你可能会期望 checkCountValidity 通过验证，因为：

1. 默认初始化：Counter 合约没有显式初始化 count 状态变量，因此 Solidity 会自动将其设置为 0。因此，当规则使用 count() 检索初始值时，它应该返回 0，使得断言 PrecallCountValue == 0 对任何执行路径都有效。
2. 增量行为：每次调用 increment() 都会将 count 变量增加 1。由于规则调用 increment() 三次，因此 count 的预期最终值应为 PrecallCountValue + 3。因此，断言 PostcallCountValue == PrecallCountValue + 3 预计对任何执行路径都成立。

运行验证

然而，当你运行验证过程时，你将遇到一个意想不到的结果，如下图所示。

在上面的结果中，我们可以清楚地看到证明器未能验证 checkCountValidity() 规则。这表明以下条件中至少有一个评估为假，导致规则违反：

• assert PrecallCountValue == 0
• assert PostcallCountValue == PrecallCountValue + 3

在违反的情况下，证明器会生成一份详细的报告，概述违反情况，包括哪个断言失败、相关的变量值以及导致失败的执行步骤。

通过反例解释验证失败

为了理解违反，Certora 证明器提供了反例。简单来说，反例是规则验证失败的特定执行路径。

要查看我们违反规则的反例，请单击报告页面上被违反的规则 (checkCountValidity) 名称，以获得类似于下面的视图。

一旦你这样做，它会显示规则参数和变量的值（在右侧），以及一个调用跟踪（在中间），如下图所示。

在调查违反情况时，调用跟踪非常有用，因为它提供了有关规则执行开始时状态变量的详细信息，并跟踪了执行过程中这些变量的更新，如下图所示：

在 Certora 证明器提供的反例中，我们可以清楚地看到我们的规则验证失败，因为规则期望 count 从 0 开始，但它却从 10 开始，这导致 assert PrecallCountValue == 0 失败。

这引出了一个重要问题：为什么 count 的值设置为 10 而不是预期的默认值 0？ 为了理解这一点，我们需要了解 Solidity 和 CVL 如何以不同方式处理未初始化的变量。

为什么 count 的值被设置为 10 而不是 0？

我们知道，如果 Solidity 智能合约没有显式初始化状态变量，它会自动根据其类型分配一个默认值。例如：

• 对于 uint256，默认值为 0。
• 对于 bool，默认值为 false。
• 对于 address，默认值为零地址。

与 Solidity 不同，CVL 不会自动为变量分配默认值。相反，CVL 中未初始化的变量保持无约束，这意味着它们在验证期间可以取其定义范围内的任何可能值。这与一个关键概念相关：CVL 规则并非从合约的特定初始部署状态（如 Solidity 执行通常假设的那样）开始验证，而是从一个 任意 状态开始。 这是形式化验证的一个关键区别和基本方面。

由于这种行为，count 的初始值在验证期间被设置为 10，这导致规则失败，因为我们期望 count 从 0 开始。

理解 require 的用法

如上所述，证明器在验证过程中会为状态变量分配任意值，这可能导致意外的初始值，并导致断言失败，如果规则假定 Solidity 的默认值。

在这种情况下，我们可能希望在验证设置中显式定义状态变量的约束，确保它们在执行规则之前以预期值开始。这就是 CVL 中的 require 语句变得有用的地方。

CVL 中的 require 语句用于为规则指定前置条件，确保在规则被视为有效之前满足某些条件。

当 require 语句包含在规则中时，它充当一个过滤器，告诉证明器忽略任何不满足指定条件的执行路径。这意味着证明器将只考虑 require 表达式评估为真的场景，从而有效地将所有其他场景排除在分析之外。

例如，我们可以在 checkCountValidity 规则中使用 require 语句将 count 的初始值限制为零，如下图所示：

Copyrule checkCountValidity() {

    // We just added this
    // 我们刚刚添加了这一行
    require count() == 0;

    // Grabbing the initial state of the count variable
    // 获取 count 变量的初始状态
    uint256 PrecallCountValue = count();

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

    //Grabbing the state of count after the increment() calls
    // 获取 increment() 调用后 count 的状态
    uint256 PostcallCountValue = count();

    // Asserting that the initial value of count is 0
    // 断言 count 的初始值为 0
    assert PrecallCountValue == 0;
    assert PostcallCountValue == PrecallCountValue + 3;

}

如果你使用上述更改重新运行证明器并打开终端中打印的验证链接，你将获得一个已验证的规则，如下图所示。

这一次，我们可以看到证明器已成功验证了我们的规则。这是因为，通过 require 约束，证明器将忽略任何 count 初始值不为零的执行路径。

默认情况下，证明器不会为已验证的规则提供调用跟踪，因为可能存在数量极其庞大的有效执行跟踪来满足规则的条件。由于已验证的规则确认不存在反例，因此生成和显示所有可能的有效跟踪既不必要也不切实际。

理解 satisfy 的用法

如前所述，当规则成功验证时，证明器不会生成调用跟踪。然而，CVL 提供了 satisfy 语句，它允许你生成一个满足 require 和 assert 语句所强制的所有条件的执行跟踪。当你想要确认特定场景是否可以在合约逻辑中发生时，这特别有用。

例如，我们可以编写一个使用 satisfy 语句的规则来验证：

• 是否存在至少一条执行路径，用户可以在存入并铸造 LP 代币后完全提取其流动性。
• 是否存在至少一条执行路径，借款人的抵押品价值低于指定阈值时其头寸被清算。

当规则包含 satisfy 语句时，证明器会检查至少一条有效执行路径是否满足条件。虽然可能存在多条此类路径，但如果找到，则只生成一条满足跟踪。根据结果，规则分类如下：

• 已验证规则：如果至少一个有效执行满足 satisfy 语句，则证明器将规则报告为已验证。
• 已违反规则：如果没有执行路径满足 satisfy 语句，则证明器将规则报告为已违反。

在规则中使用 satisfy

为了理解 satisfy 语句的工作原理，请考虑以下规范，其中包含一个以 satisfy 语句结尾的规则 searchValidExecution()。

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

rule searchValidExecution {

    increment();
    increment();
    increment();

    satisfy count() == 8;
}

由于规则 searchValidExecution 以 satisfy 语句结束，它指示证明器探索可能的执行路径，并确定是否存在一个三次 increment() 调用序列，可以使 count() 达到 8。如果找到这样的路径，证明器将规则报告为已验证。否则，它将规则报告为已违反。

要检查规则 searchValidExecution 是否成立，请运行证明器并打开浏览器中的验证链接以查看结果。

上述结果表明 Certora 证明器已成功验证了该规则。这意味着它找到了至少一条满足 satisfy 语句的执行路径。具体来说，证明器识别出一种状态，其中 count() 在三次连续调用 increment() 后达到 8。

这个结果符合预期，因为理想情况下，如果初始值为 5（假设每次调用都将计数增加 1），则 count() 的值可以在三次连续 increment() 调用后达到 8。由于规则寻求一个有效的执行路径，证明器确认了它的存在，从而成功验证。

使用证明器求解和验证线性方程组

由于证明器在处理包含 satisfy 语句的规则时只评估单个执行路径，因此它充当求解器，确定满足给定约束的输入值。为了演示此功能，让我们使用 satisfy 来找到方程组的解。

例如，考虑以下方程：

• $2x+3y=22$
• $4x-y=2$

现在，假设我们想找到满足这两个方程的整数值 $x$ 和 $y$。为了实现这一点，我们首先需要定义一个编码方程组的 Solidity 函数：

Copy// 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 函数，我们就可以创建一个规则来指示证明器搜索满足约束的 $x$ 和 $y$ 的有效值，如下图所示：

Copymethods {

    function eqn(uint256, uint256) external returns (bool) envfree;
}

rule checkEqn() {

    uint256 x;
    uint256 y;

    satisfy eqn(x, y) == true;
}

或者，变量可以 直接在规则声明中定义，而不是在规则体内部声明，如下图所示：

Copyrule checkEqn(uint256 x, uint256 y) {
    satisfy eqn(x, y) == true;
}

当执行该规则时，证明器会尝试找到使函数返回 true 的 $x$ 和 $y$ 值。在这种情况下，正确的整数解是 $x=2$ 和 $y=6$。

此外，如果方程以使其不一致的方式修改——例如定义平行线——证明器将检测到没有解。考虑修改后的系统：

• $2x+3y=22$
• $4x+6y=50$

由于第二个方程只是第一个方程的倍数，但常数不同，因此该系统没有解，因为两条线现在是平行的，永不相交。等效的 Solidity 函数是：

Copy// 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() 规则时，验证结果表明证明器正确识别了缺少有效解。

上述结果突出了证明器不仅能够在存在有效解时找到它们，而且能够检测并确认一组约束何时本质上不可满足，例如在不一致或平行方程的情况下。

使用 satisfy 语句时的关键考量

在使用 satisfy 语句的任何规则中，有几个重要的细节需要记住：

• 如果一个规则包含多个 satisfy 语句，只有当所有执行的 satisfy 语句在至少一条执行路径中都成立时，证明器才会将其报告为已验证；否则，该规则将被视为已违反（在默认证明器模式下），如下图所示：

• 条件分支上未执行的 satisfy 语句不需要成立，因为它在验证期间从未被触及。证明器独立验证每个执行路径并报告执行路径的结果，如下图所示。

assert 和 satisfy 之间的区别

乍一看，assert 和 satisfy 语句在功能上可能相似，因为它们都用于验证规则中的条件。然而，它们的目的和用途大相径庭，如下图所示：

结论

在本章中，我们研究了 CVL 语句如何指导 Certora 证明器进行验证。我们学习了 assert 如何在所有执行路径中强制执行属性，require 如何约束证明器考虑的状态，以及 satisfy 如何证明存在有效执行路径。理解这些语句以及证明器如何推理任意状态对于编写正确且有效的 CVL 规则至关重要。

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

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