蕴涵运算符

Certora 形式化验证

蕴含运算符

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

上次更新时间：2026 年 2 月 13 日

引言

蕴含运算符常被用作 if 语句的替代，因为它更简洁。

考虑以下示例：一个函数 mod(x, y)，它接受两个无符号整数作为参数，并返回 x 对 y 的模。模运算计算 x 除以 y 的余数。

该函数的 Solidity 实现如下：

Copy/// Solidity

function mod(uint256 x, uint256 y) external pure returns (uint256) {
    return x % y;
}

假设我们想形式化验证这个属性：“如果 x < y，那么模必须等于 x。” 在 CVL 中使用 if 语句来表达这一点会导致编译错误，因为规则中的最后一条语句必须是 assert 或 satisfy：

Copy/// this rule will not compile
rule mod_ifXLessThanY_resultIsX_usingIf() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

    if (x < y) {
        assert result == x;
    }
}

CopyERROR
: Failed to run Certora Prover locally. Please check the errors below for problems in the specifications (.spec files) or the prover_args defined in the .conf file.

CRITICAL
: [main] ERROR ALWAYS - Found errors in certora/specs/ImplicationOperator.spec:

CRITICAL
: [main] ERROR ALWAYS - Error in spec file (ImplicationOperator.spec:15:5): last statement of the rule mod_ifXLessThanY_resultIsX_usingIf is not an assert or satisfy command (but must be)

为了解决这个问题，一个变通方法是在末尾添加一个无关紧要的断言：

Copyif (P) {
    assert Q;
}
assert true;

Copyrule mod_ifXLessThanY_resultIsX_usingIf() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

    if (x < y) {
    assert result == x;
    }
    assert true; // trivially TRUE
}

然而，这个解决方案引入了一个无意义的断言，使得规范变得混乱。另一个变通方法是使用 if-else 语句，其中 else 分支执行有意义的断言：

Copyif (P) {
    assert Q;
} else {
    assert (something_else);
}

Copyrule mod_ifXLessThanY_resultIsX_usingIfElse() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

    if (x < y) {
    assert result == x;
    } else {
    assert result != x;
    }
}

然而，我们最初并不想断言：“如果 x >= y，那么 result != x。” 在许多情况下，像上面所示的那样，我们不希望为每个可能的分支创建断言。

CVL 中的蕴含 (=>)

为了优雅地处理这个问题，我们使用蕴含运算符 (=>)。通过蕴含，我们可以简洁地表达条件，同时避免 if-else 语句的控制流复杂性。

因此，与其编写 if (P) assert Q（这无法编译），我们可以等效地使用 assert P => Q：

Copyrule mod_ifXLessThanY_thenResultIsX() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);
    assert x < y => result == x;
}

Prover 运行：链接

形式 P => Q 读作“如果 P，那么 Q”，或者简称为“P 蕴含 Q”。请注意，Q => P 不一定等价，我们将在下一节中看到。

P 蕴含 Q P => Q

我们再举一个例子：Solady 的 gas 优化 max 函数。正如上一章所讨论的，它返回两个输入 x 和 y 中较大的一个，如果它们相等则默认为 x。

下面是实现，和上一章一样，我们将可见性从 internal 更改为 external，以避免需要进行连接（这超出了本章的范围）：

Copy/// Solidity

function max(uint256 x, uint256 y) external pure returns (uint256 z) {
    assembly {
        z := xor(x, mul(xor(x, y), gt(y, x)))
    }
}

现在我们形式化验证以下属性：“如果 x 大于 y，则 max(x, y) 的返回值必须是 x。” 我们可以在 CVL 中表达为：

Copyrule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x > y => result == x;
}

在此规则中，条件 (x > y) 和预期结果 (result == x) 构成了蕴含 P => Q。正如预期的那样，该属性得到 验证。

Prover 运行：链接

注意：max 函数的验证尚未完成。我们将在下一节中讨论。

P => Q 不等价于 Q => P

现在让我们考虑反向蕴含：“如果 max(x, y) 的返回值是 x，那么 x > y” 或 result == x => x > y。这乍一看可能看似有效；然而，当 x == y 时，函数仍然返回 x。这与 x > y 的断言相矛盾，使得在这种情况下蕴含为假。

以下是失败的规则：

Copyrule max_ifResultIsX_thenXGreaterThanY() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == x => x > y;
}

反例

当规则被违反时，Prover 会显示一个反例。在这种情况下，result == x 不仅在 x > y 时发生，在 x == y 时也会发生。反例具体显示 x = 3 和 y = 3：

为了解决这个问题，我们需要修改条件，以包含 result == x 有效的所有情况：即 x > y 和 x == y。

以下是修改后的规则，其中 || 是或运算符：

Copyrule max_ifResultIsX_thenXGreaterOrEqualToY() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == x => x > y || x == y;
}

或者，更简单地：

Copyrule max_ifResultIsX_thenXGreaterOrEqualToY_simplified() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == x => x >= y;
}

现在它被 验证 了：

Prover 运行：链接

现在，为了完成验证，我们还将验证 max(x, y) 在 y 大于或等于 x 时返回 y 的属性。规则如下：

Copyrule max_ifResultIsY_thenYGreaterOrEqualToX() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == y => y >= x;
}

正如预期的那样，它被 验证 了：

Prover 运行：链接

P => Q 等价于 !Q => !P

将蕴含 P => Q 重写为其逆否命题形式 !Q => !P 提出了一种思考规范的替代方式。

让我们回顾一下我们之前的规则，其断言为：x > y => result == x：

Copyrule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x > y => result == x;
}

在其原始形式中，此规则关注当 x 大于 y 时会发生什么，即 max(x, y) 的返回值是 x。

在其逆否命题形式 assert !(result == x) => !(x > y) 中，我们关注的是如果 max(x, y) 的返回值不是 x 时会发生什么。在这种情况下，我们期望 x 不大于 y（或者简单地说，x <= y）：

Copyrule max_ifResultNotX_thenXNotGreaterThanY() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result != x => x <= y;
}

Prover 运行：链接

两种形式都表达了相同的逻辑真理，但角度不同。

为了更好地理解这一点，我们使用一个常见的类比：

• “如果下雨了，地面是湿的，” 或
• hasRained => isGroundWet

它的逆否命题是：

• “如果地面不湿，那么肯定没下雨，” 或
• !isGroundWet => !hasRained

然而，没有下雨的事实并不能保证地面不湿。可能有人往上面倒了水。因此，!hasRained => !isGroundWet 在逻辑上是无效的。

蕴含中的空泛真理和重言式

现在我们了解了蕴含的工作原理，我们也必须在编写这些语句时保持谨慎。我们可能会在不知不觉中写出带有虚假保证的蕴含，这是我们接下来要探讨的话题。

当 P 始终为 FALSE 时， P => Q 为 TRUE，无论 Q 如何（空泛）

当条件 (P) 无法达到（始终为假）时，蕴含就变成了空泛真理，这意味着不存在 P 成立的可能状态。在这种情况下，整个语句 P => Q 自动被认为是真，无论结果 (Q) 是什么。

发生这种情况是因为如果 P 永远不能为真，那么就不存在可以违反蕴含的情况。因此，不存在反例。

让我们使用这个例子：“如果 x < 0，那么 result == y。” 由于 x 是 uint256，它永远不能是负数。这使得 x < 0 成为一个无法达到的状态。无论我们在右侧 (Q) 断言什么，蕴含都将始终被验证。

以下是 CVL 空泛规则：

Copyrule max_unreachableCondition_vacuouslyTrue() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x < 0 => result == y;
}

这条规则被 验证 了，但并非因为 x < 0 导致 result == y。它验证仅仅是因为 x < 0 在任何有效的执行路径中都是不可达的，使得蕴含是空泛真理。它证实了不存在反例，因为条件永远不会发生：

Prover 运行：链接

由于条件 (P) 永远不会发生，结果 (Q) 可以是任何东西——甚至是一些毫无意义的东西，比如 1 == 2，如下所示：

Copyrule max_unreachableCondition_vacuouslyTrueObvious() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x < 0 => 1 == 2;
}

Prover 运行：链接

当 Q 始终为 TRUE 时， P => Q 为 TRUE，无论 P 如何（重言式）

当结果 (Q) 始终为真时，蕴含就变成了重言式真理，无论条件 (P) 是什么。在这种情况下，整个语句 P => Q 自动被认为是真，即使条件无关或具有误导性。

发生这种情况是因为如果 Q 始终为真，那么结果就是有保证的；因此，蕴含永远不会是假。

让我们使用这个例子：“如果 x > y，那么 result >= 0。”

乍一看，这似乎意味着 x > y 保证了非负结果。但是 result 是 uint256 类型，它总是大于或等于零。所以表达式 result >= 0 总是真的。

以下是 CVL 重言式规则：

Copyrule max_outcomeIsAlwaysTrue_tautology() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x > y => result >= 0;
}

这条规则被 验证 了，并非因为 x > y 导致 result >= 0，而是因为 result >= 0 在类型上总是为真，使得蕴含是重言式真理：

Prover 运行：链接

形式化验证 Solmate 的 mulDivUp()

现在我们了解了基础知识，我们将使用蕴含运算符形式化验证 Solmate 的 mulDivUp()。顾名思义，这个函数将两个无符号整数相乘，将结果除以另一个无符号整数，如果存在余数则向上取整。如果没有余数，它就简单地返回商。

我们将形式化验证的属性分为两类：取整行为和回滚行为。但在我们这样做之前，我们将对原始的 mulDivUp() 代码进行一个小调整。

Solmate 的 mulDivUp() 函数具有 internal 可见性，为了方便起见，我们将其更改为 external。否则，将需要设置一个连接合约，这超出了本章的范围，并且此时可能会引入不必要的思维负担。

以下是 mulDivUp() 函数：

Copy/// Solidity

uint256 internal constant MAX_UINT256 = 2**256 - 1;

function mulDivUp(
    uint256 x,
    uint256 y,
    uint256 denominator
) external pure returns (uint256 z) {
    assembly {
        // Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
        if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
            revert(0, 0)
        }

        // If x * y modulo the denominator is strictly greater than 0,
        // 1 is added to round up the division of x * y by the denominator.
        z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))
    }
}

汇编代码的解释超出了本章的范围。然而，注释帮助我们理解代码的作用。

以下几行代码：

Copy// Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT2256, y)))))) {
    revert(0, 0)
}

正如注释所示，表示一个 require 语句，它强制执行以下条件：

• denominator != 0，这可以防止除以零，因为不允许除以零。

• y == 0 || x <= type(uint256).max / y，这意味着：

  • 如果 y == 0，则条件成立，因为 x * y 自然评估为 0。在这种情况下，不需要溢出检查。
  • 否则，如果 y != 0，x 必须小于或等于 type(uint256).max / y，以确保 x * y 不超过 type(uint256).max，从而防止溢出。

现在我们得出结论，需要形式化验证的属性如下：

• 如果 denominator == 0，则函数回滚。
• 如果 x * y > MAX_UINT256，则函数回滚。

在下一行，

Copy// If x * y modulo the denominator is strictly greater than 0,
// 1 is added to round up the division of x * y by the denominator.
z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))

正如注释所示，该函数按以下方式处理取整：

• 如果 x * y % denominator > 0，则将 1 添加到 x * y / denominator 以弥补 Solidity 在整数除法中的截断。由于 Solidity 向下取整，添加 1 有效地将值向上取整。
• 如果 x * y % denominator == 0，则不需要取整调整，结果按原样返回。

现在我们得出结论，需要形式化验证的属性如下：

• 如果 x * y % denominator > 0，则结果为 x * y / denominator + 1。
• 如果 x * y % denominator == 0，则结果为 x * y / denominator。

既然我们了解了函数的工作原理以及需要形式化验证的属性，我们就可以继续编写规则了。让我们从取整行为的规则开始。

取整行为

以下是取整行为属性的 CVL 规则规范。

mulDivUp_roundUp() 规则的断言表明，当 x 和 y 的乘积被 denominator 除且有余数时，结果会增加 1。

类似地，mulDivUp_noRoundUp() 规则中的断言表明，当 x 和 y 的乘积被 denominator 除且没有余数时，结果按原样返回。

正如预期的那样，这些规则被 验证 了：

Copyrule mulDivUp_roundUp() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mathint result = mulDivUp(x, y, denominator);
    assert ((x * y) % denominator > 0) => (result == (x * y / denominator) + 1);
}

rule mulDivUp_noRoundUp() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mathint result = mulDivUp(x, y, denominator);
    assert ((x * y) % denominator == 0) => (result == x * y / denominator);
}

Prover 运行：链接

现在，让我们转向该函数的下一类属性：回滚行为。

回滚行为

如前所述，mulDivUp() 在两种情况下会回滚：

• 如果 denominator == 0
• 如果 x * y > MAX_UINT256

在形式化验证回滚时，我们必须在调用函数时包含 @withrevert 标签。默认情况下，Prover 只执行不回滚的路径，这意味着传递给 mulDivUp(x, y, denominator) 的所有参数都是不回滚的。然而，向函数添加 @withrevert 会指示 Prover 也考虑导致回滚的参数。这允许我们在蕴含语句中考虑回滚情况。

以下是 CVL 规则规范：

Copyrule mulDivUp_ifDenominatorIsZero_revert() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert (denominator == 0) => isReverted;
}

rule mulDivUp_ifXYExceedsMaxUint_revert() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert (x * y > max_uint256) => isReverted;
}

正如预期的那样，这些规则被 验证 了：

Prover 运行：链接

还有一种更有趣的方法。到目前为止，我们使用了 P => Q 结构，这意味着 (P) 条件导致 (Q) 结果。但如果我们将它反转为 Q => P，则意味着 (Q) 结果源自 (P) 条件；因此，我们必须考虑所有可能导致 Q 的 P 情况。

下面是实现，其中在第一条规则中，我们故意省略了一个回滚情况，而在第二条规则中，我们考虑了所有情况。结果是，第一条规则导致 违反，而第二条规则被 验证：

Copyrule mulDivUp_allRevertCases_violated() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert isReverted => (denominator == 0);
}

rule mulDivUp_allRevertCases() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert isReverted => (denominator == 0 || x * y > max_uint256);
}

Prover 运行：链接

在下一小节中，我们将形式化验证非回滚情况，这是一个可选步骤，因为我们已经涵盖了所有回滚情况。但是，我们仍然会这样做，因为它可能在未来有用。

非回滚行为（可选）

如果我们可以形式化验证回滚路径，我们也可以验证非回滚路径。为此，我们需要将语句重新组织为：

• denominator != 0
• x * y <= MAX_UINT256

并将它们组合起来，如以下 CVL 规则实现所示：

Copyrule mulDivUp_noRevert() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert ((denominator != 0) && (x * y <= max_uint256)) => !isReverted;
}

正如预期的那样，该规则被 验证 了：

Prover 运行：链接

总结

• 蕴含语句由条件 P、结果 Q 和蕴含运算符 (=>) 组成。
• 蕴含运算符定义了单向条件关系，这意味着 P => Q 不蕴含 Q => P。
• P => Q 及其逆否命题 !Q => !P 在逻辑上是等价的，但提供了不同的视角，将焦点从条件何时成立转移到条件何时不成立。
• 为了使蕴含具有意义（既非空泛也非重言），Q（结果）必须依赖于 P（条件）为真。
• 当 P 无法达到（始终为假）时，发生空泛真理，使得 P => Q 为真，无论 Q 如何，因为缺乏反例。
• 当 Q 始终为真时，发生重言式，使得 P => Q 为真，无论 P 如何。
• 空泛真理和重言式在形式化验证中会产生误导性保证。

供读者练习

1. 形式化验证 Solady min 总是返回最小值。
2. 形式化验证 Solady zeroFloorSub 返回 max(0, x - y)。换句话说，如果 x 小于 y，则返回 0。否则，返回 x - y。

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

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