双向条件运算符

Certora 的形式化验证

双条件运算符

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

最后更新于 2026 年 2 月 13 日

介绍

双条件运算符使我们能够断言布尔值之间的当且仅当关系。蕴含（$P => Q$）表示如果条件 $P$ 满足，则观察到 $Q$。双条件运算符增加了反向要求：如果观察到 $Q$，则条件 $P$ 也必须满足。换句话说，$P <=> Q$ 等同于断言 $P => Q$ 和 $Q => P$。

注意：假定读者已阅读“蕴含运算符”一章，该章为本章奠定了基础。

setX() 函数

让我们从一个基本的 setter 函数开始。它接受一个 uint256 输入并更新存储变量 $x$，但仅当新值严格大于当前值时才更新。此限制通过 require 语句强制执行，如果条件不满足，它将回滚交易：

Copy/// Solidity

uint252 public x;

function setX(uint256 _x) external {
    require(_x > x, "x must be greater than the previous value"); // x 必须大于前一个值
    x = _x;
}

为了使用蕴含运算符对该函数进行形式化验证，我们可以将交易成功与由此产生的状态变化之间的关系表达为两个断言蕴含语句：

Copyrule setX_usingImplication() {
    uint256 _x;

    mathint xBefore = x();

    setX@withrevert(_x);
    bool success = !lastReverted;

    mathint xAfter = x();

    assert success => xAfter > xBefore; // 如果调用成功，则 x 增加 (P => Q)
    assert xAfter > xBefore => success; // 如果 x 增加，则调用必须成功 (Q => P)
}

Prover 运行：链接

虽然逻辑上正确，但编写两个单向蕴含（$P => Q$ 和 $Q => P$）是不必要的冗长。

CVL 中的双条件运算符（<=>）

这里的目的是表达一个精确的规则：“当且仅当输入值大于 $x$ 的当前值时，交易成功。”

这可以更清晰地写成：

Copyrule setX_TxSucceeds_iff_XIncreases() {
    uint256 _x;

    mathint xBefore = x();

    setX@withrevert(_x);
    bool success = !lastReverted;

    mathint xAfter = x();
    assert success <=> xAfter > xBefore;
}

这个单一的断言双条件语句更简洁，并直接表达了调用成功与状态 $x$ 变化（增加）之间的双向关系。换句话说，函数只有在 $x$ 增加时才成功，而 $x$ 只有在调用成功时才增加。

正如预期，这条规则得到了验证：

Prover 运行：链接

隐含地，我们也可以推断：如果调用失败，那么 $x$ 没有增加：

Copyassert !success <=> !(xAfter > xBefore);

或者

Copyassert !success <=> xAfter <= xBefore;

这已经由双条件运算符隐含，无需单独编写。

形式化验证 Solmate 的 mulDivUp()

在上一章（蕴含运算符）中，我们讨论了 Solmate 的 mulDivUp() 函数的行为、其溢出检查和舍入逻辑。以下是快速回顾：

• 如果 denominator == 0（除以零）或 $x * y > MAX_UINT256$（溢出），它将回滚。
• mulDivUp(x, y, denominator) 将 $x$ 和 $y$ 相乘，将结果除以 denominator，如果有余数则向上舍入；否则，它返回精确的商。

现在让我们使用双条件运算符形式化验证这些行为。

回滚行为

让我们从回滚行为开始。我们首先编写最简单的回滚条件 denominator == 0，然后逐步构建一个完整的规则。

这将失败，正如我们所知，因为它没有捕获所有回滚场景，但它是一个很好的起点：

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

    mulDivUp@withrevert(x, y, denominator);
    assert denominator == 0 <=> lastReverted;
}

由于 $x$ 和 $y$ 的乘积超过 max_uint256 的反例，该规则失败。我们需要将其作为附加回滚条件包含在内：

这是更正后的 CVL 规则：

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

    mulDivUp@withrevert(x, y, denominator);
    assert denominator == 0 || x * y > max_uint256 <=> lastReverted;
}

Prover 运行：链接

请注意，双条件运算符是可逆的（与蕴含不同），因此我们可以将断言重写为：

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

    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted <=> denominator == 0 || x * y > max_uint256;
}

Prover 运行：链接

此外，由于双条件运算符是组合的双向蕴含（$P => Q$ 和 $Q => P$），两者在逻辑上绑定在一起；因此，通过 <=> 推理的表达式是不可分割的。

舍入行为

下面的规则指定了 mulDivUp() 函数的舍入行为。它断言当且仅当存在余数时，函数返回一个向上舍入的值。双条件运算符保证余数是触发向上舍入的唯一条件，并且没有其他条件可以影响返回值：

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

Prover 运行：链接

下面的规则涵盖了“另一种”情况。它断言当且仅当没有余数时，函数返回精确的商。双条件运算符保证返回未舍入结果的唯一原因是缺少余数：

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

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

Prover 运行：链接

何时使用双条件运算符而非蕴含运算符

排除不确定性

上面的规则，正如我们在上一章中看到的，可以用 => 来编写，因为被验证的属性碰巧只有一个条件导致该结果。在这种情况下，=> 可以替换为 <=>。这种替换更可取，因为 <=> 表示除了指定条件之外，没有任何其他条件可以导致该结果。蕴含运算符不提供此保证，因此在这种情况下，最好使用双条件运算符来明确该保证。

在前面的例子（max 函数）中，我们考虑了所有回滚条件，因为我们正在验证函数的整体正确性。然而，在处理一个调用多个内部函数、每个函数都可能导致不同回滚条件的函数时，使用蕴含运算符可能更实用。这种方法只关注回滚的必要条件，而无需详尽地处理每种可能的失败场景。

验证相互依赖

当两个变量相互依赖时，就会发生相互依赖，这意味着其中一个变量的变化会触发另一个变量的相应变化，反之亦然。

以 AMM WETH/USDC 资金池为例：在掉期交易期间，WETH 余额增加当且仅当 USDC 余额减少，反之亦然。这产生了双向依赖，其中一个代币的余额必须响应另一个代币的变化而调整，表明两个余额都不能独立变化。

总结

• 双条件运算符（<=>）明确保证双向蕴含。如果条件 $P$ 满足，则 $Q$ 成立，并且如果 $Q$ 成立，则条件 $P$ 也必须满足。
• 蕴含运算符（=>）在条件导致结果时起作用，但它不保证结果只能由该条件引起。
• 当有许多可能导致结果的条件时，使用双条件运算符可能不切实际。

供读者练习

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

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

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