蕴含操作符

Last updated on Feb 13, 2026

简介

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

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

该函数的 Solidity 实现如下：

/// Solidity

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

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

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

ERROR
: 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)

为了解决这个问题，一种变通方法是在最后添加一个无意义的断言：

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

rule mod_ifXLessThanY_resultIsX_usingIf() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

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

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

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

rule 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 语句所带来的控制流复杂性。

因此，我们可以等价地使用 assert P => Q，而不是写成 if (P) assert Q（这无法编译）：

rule 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，以避免对构建 harness 的需求（这超出了本章的范围）：

/// 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 中将其表达为：

rule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

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

在这条规则中，条件（x > y）和预期结果（result == x）构成了蕴含 P => Q。不出所料，该属性已验证（VERIFIED）。

Prover 运行：链接

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

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

现在让我们考虑反向的蕴含命题：“如果 max(x, y) 的返回值是 x，那么 x > y”，即 result == x => x > y。起初这似乎是成立的；然而，当 x == y 时，函数仍然返回 x。这与 x > y 的断言相矛盾，使得该蕴含在那种情况下为假。

以下是验证失败的规则：

rule 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。

这是修改后的规则，其中 || 是 OR（逻辑或）运算符：

rule max_ifResultIsX_thenXGreaterOrEqualToY() {
    uint256 x;
    uint256 y;

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

或者，更简单的写法：

rule max_ifResultIsX_thenXGreaterOrEqualToY_simplified() {
    uint256 x;
    uint256 y;

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

现在它验证通过（VERIFIED）了：

Prover 运行：链接

现在，为了完成验证，我们还要验证一个属性：当 y 大于或等于 x 时，max(x, y) 返回 y。以下是该规则：

rule max_ifResultIsY_thenYGreaterOrEqualToX() {
    uint256 x;
    uint256 y;

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

不出所料，它验证通过（VERIFIED）了：

Prover 运行：链接

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

将蕴含 P => Q 重写为其逆否命题形式 !Q => !P，为我们提供了一种思考规范（specification）的替代方法。

让我们回顾之前包含断言 x > y => result == x 的规则：

rule 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）：

rule 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 时，不管 Q 是什么， `P => Q` 均为 TRUE（空洞为真）

当条件（P）不可达（始终为假）时，即不存在 P 成立的可能状态，蕴含式就会出现“空洞为真（vacuously true）”。在这种情况下，整个语句 P => Q 会自动被认为是真，无论结果（Q）是什么。

这是因为如果 P 永远不可能为真，那么就不存在该蕴含被违反的实例。因此，也就不存在反例。

让我们以这个为例：“如果 x < 0，那么 result == y。”由于 x 是 uint256 类型，它永远不可能是负数。这使得 x < 0 成为一个不可达的状态。无论我们在右侧（Q）断言什么，该蕴含始终会验证通过。

以下是 CVL 中空洞为真的规则：

rule max_unreachableCondition_vacuouslyTrue() {
    uint256 x;
    uint256 y;

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

这条规则验证通过（VERIFIED），但并不是因为 x < 0 导致了 result == y。它能通过验证仅仅是因为 x < 0 在任何有效的执行路径中都是不可达的，使得蕴含出现了空洞为真的情况。由于条件永远不会发生，这就确认了不存在反例：

Prover 运行：链接

既然条件（P）永远不会发生，结果（Q）就可以是任何东西——哪怕是像 1 == 2 这样荒谬的东西，如下所示：

rule max_unreachableCondition_vacuouslyTrueObvious() {
    uint256 x;
    uint256 y;

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

Prover 运行：链接

当 Q 始终为 TRUE_ 时，不管 P 是什么，_ `P => Q` 均为 TRUE（恒真式）

当结果（Q）始终为真，而不管条件（P）是什么时，蕴含式就会变成恒真式（tautology）。在这种情况下，整个语句 P => Q 会自动被认为是真，即使条件是无关的或具误导性的。

这是因为如果 Q 始终为真，结果就得到了保证；因此，蕴含命题永远不可能为假。

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

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

以下是 CVL 中的恒真式规则：

rule max_outcomeIsAlwaysTrue_tautology() {
    uint256 x;
    uint256 y;

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

该规则验证通过（VERIFIED），并非因为 x > y 导致 result >= 0，而是因为按类型定义 result >= 0 始终为真，这使得该蕴含成为了恒真式：

Prover 运行：链接

形式化验证 Solmate 的 `mulDivUp()`

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

我们将要形式化验证的属性分为两类：舍入行为（rounding behavior）和回退行为（revert behavior）。但在开始之前，我们将对原始的 mulDivUp() 代码做一个小调整。

Solmate 的 mulDivUp() 函数的可见性是 internal，为了方便起见，我们将把它更改为 external。否则，就有必要设置一个 harness 合约，这超出了本章的范围，并可能会在现阶段引入不必要的认知负担。

以下是 mulDivUp() 函数：

/// 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))
    }
}

对汇编代码的解释超出了本章的范围。然而，注释有助于我们理解代码的功能。

下面这几行，

// 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)
}

正如注释所暗示的，代表了一个 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，则函数发生 revert。
如果 x * y > MAX_UINT256，则函数发生 revert。

在接下来的一行中，

// 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，则在 x * y / denominator 的基础上加上 1，以补偿 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 且没有余数时，直接返回原结果。

不出所料，这些规则验证通过（VERIFIED）：

rule 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 运行：链接

现在，让我们进入该函数属性的下一个类别：回退（revert）行为。

回退行为

如前所述，有两种情况会导致 mulDivUp() 发生 revert：

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

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

以下是 CVL 规则规范：

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

不出所料，这些规则验证通过（VERIFIED）：

Prover 运行：链接

这里有一个更有趣的方法。到目前为止，我们使用的是 P => Q 结构，这意味着条件（P）导致结果（Q）。但是如果我们将其反转为 Q => P，这意味着结果（Q）是由条件（P）引起的；因此，我们必须考虑导致 Q 的所有 P 的可能情况。

下面是具体实现，在第一条规则中，我们故意遗漏了一个 revert 情况，而在第二条规则中，我们涵盖了所有情况。结果，第一条规则导致了违反（VIOLATION），而第二条规则验证通过（VERIFIED）：

rule 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 运行：链接

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

非回退行为（可选）

如果我们可以形式化验证发生 revert 的路径，我们同样可以验证不发生 revert 的路径。为此，我们需要将语句重新构建为：

denominator != 0
x * y <= MAX_UINT256

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

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

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

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

不出所料，规则验证通过（VERIFIED）：

Prover 运行：链接

总结

蕴含语句由条件 P、结果 Q 以及蕴含运算符（=>）组成。
蕴含运算符定义了一种单向的条件关系，这意味着 P => Q 并不意味着 Q => P。
P => Q 及其逆否命题 !Q => !P 在逻辑上是等价的，但提供了不同的视角，将焦点从条件成立时转移到条件不成立时。
要使一个蕴含具有意义（既非空洞为真，也非恒真式），Q（结果）必须依赖于 P（条件）为真。
当 P 不可达（始终为假）时，就会出现空洞为真（vacuous truth），由于缺乏反例，无论 Q 是什么，P => Q 都为真。
当 Q 始终为真时，就会出现恒真式（tautology），无论 P 是什么，P => Q 都为真。
虚假求真（空洞为真）和恒真式会在形式化验证中造成误导性的保证。

给读者的练习

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

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

Last updated on Feb 13, 2026

简介

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

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

该函数的 Solidity 实现如下：

/// Solidity

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

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

ERROR
: 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)

为了解决这个问题，一种变通方法是在最后添加一个无意义的断言：

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

rule mod_ifXLessThanY_resultIsX_usingIf() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

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

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

rule 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 语句所带来的控制流复杂性。

因此，我们可以等价地使用 assert P => Q，而不是写成 if (P) assert Q（这无法编译）：

rule 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，以避免对构建 harness 的需求（这超出了本章的范围）：

/// 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 中将其表达为：

rule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

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

在这条规则中，条件（x > y）和预期结果（result == x）构成了蕴含 P => Q。不出所料，该属性已验证（VERIFIED）。

Prover 运行：链接

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

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

以下是验证失败的规则：

rule 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。

这是修改后的规则，其中 || 是 OR（逻辑或）运算符：

rule max_ifResultIsX_thenXGreaterOrEqualToY() {
    uint256 x;
    uint256 y;

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

或者，更简单的写法：

rule max_ifResultIsX_thenXGreaterOrEqualToY_simplified() {
    uint256 x;
    uint256 y;

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

现在它验证通过（VERIFIED）了：

Prover 运行：链接

现在，为了完成验证，我们还要验证一个属性：当 y 大于或等于 x 时，max(x, y) 返回 y。以下是该规则：

rule max_ifResultIsY_thenYGreaterOrEqualToX() {
    uint256 x;
    uint256 y;

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

不出所料，它验证通过（VERIFIED）了：

Prover 运行：链接

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

将蕴含 P => Q 重写为其逆否命题形式 !Q => !P，为我们提供了一种思考规范（specification）的替代方法。

让我们回顾之前包含断言 x > y => result == x 的规则：

rule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

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

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

rule 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 时，不管 Q 是什么， `P => Q` 均为 TRUE（空洞为真）

这是因为如果 P 永远不可能为真，那么就不存在该蕴含被违反的实例。因此，也就不存在反例。

以下是 CVL 中空洞为真的规则：

rule max_unreachableCondition_vacuouslyTrue() {
    uint256 x;
    uint256 y;

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

Prover 运行：链接

既然条件（P）永远不会发生，结果（Q）就可以是任何东西——哪怕是像 1 == 2 这样荒谬的东西，如下所示：

rule max_unreachableCondition_vacuouslyTrueObvious() {
    uint256 x;
    uint256 y;

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

Prover 运行：链接

当 Q 始终为 TRUE_ 时，不管 P 是什么，_ `P => Q` 均为 TRUE（恒真式）

这是因为如果 Q 始终为真，结果就得到了保证；因此，蕴含命题永远不可能为假。

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

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

以下是 CVL 中的恒真式规则：

rule max_outcomeIsAlwaysTrue_tautology() {
    uint256 x;
    uint256 y;

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

该规则验证通过（VERIFIED），并非因为 x > y 导致 result >= 0，而是因为按类型定义 result >= 0 始终为真，这使得该蕴含成为了恒真式：

Prover 运行：链接

形式化验证 Solmate 的 `mulDivUp()`

以下是 mulDivUp() 函数：

/// 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))
    }
}

对汇编代码的解释超出了本章的范围。然而，注释有助于我们理解代码的功能。

下面这几行，

// 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)
}

正如注释所暗示的，代表了一个 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，则函数发生 revert。
如果 x * y > MAX_UINT256，则函数发生 revert。

在接下来的一行中，

// 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，则在 x * y / denominator 的基础上加上 1，以补偿 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 且没有余数时，直接返回原结果。

不出所料，这些规则验证通过（VERIFIED）：

rule 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 运行：链接

现在，让我们进入该函数属性的下一个类别：回退（revert）行为。

回退行为

如前所述，有两种情况会导致 mulDivUp() 发生 revert：

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

以下是 CVL 规则规范：

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

不出所料，这些规则验证通过（VERIFIED）：

Prover 运行：链接

rule 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 运行：链接

非回退行为（可选）

如果我们可以形式化验证发生 revert 的路径，我们同样可以验证不发生 revert 的路径。为此，我们需要将语句重新构建为：

denominator != 0
x * y <= MAX_UINT256

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

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

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

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

不出所料，规则验证通过（VERIFIED）：

Prover 运行：链接

总结

蕴含语句由条件 P、结果 Q 以及蕴含运算符（=>）组成。
蕴含运算符定义了一种单向的条件关系，这意味着 P => Q 并不意味着 Q => P。
P => Q 及其逆否命题 !Q => !P 在逻辑上是等价的，但提供了不同的视角，将焦点从条件成立时转移到条件不成立时。
要使一个蕴含具有意义（既非空洞为真，也非恒真式），Q（结果）必须依赖于 P（条件）为真。
当 P 不可达（始终为假）时，就会出现空洞为真（vacuous truth），由于缺乏反例，无论 Q 是什么，P => Q 都为真。
当 Q 始终为真时，就会出现恒真式（tautology），无论 P 是什么，P => Q 都为真。
虚假求真（空洞为真）和恒真式会在形式化验证中造成误导性的保证。

给读者的练习

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

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

简介

CVL 中的蕴含运算符 (=>)

P 蕴含 Q P => Q

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

反例

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

蕴含中的空洞为真与恒真式

当 P 始终为 FALSE 时，不管 Q 是什么， P => Q 均为 TRUE（空洞为真）

当 Q 始终为 TRUE_ 时，不管 P 是什么，_ P => Q 均为 TRUE（恒真式）

形式化验证 Solmate 的 mulDivUp()

舍入行为

回退行为

非回退行为（可选）

总结

给读者的练习