简介
双条件运算符使我们能够断言布尔值之间的当且仅当（if-and-only-if）关系。蕴含关系（P => Q）表明，如果满足条件 P，则会观察到 Q。双条件在此基础上增加了反向要求：如果观察到 Q，则也必须满足条件 P。换言之，P <=> Q 等同于同时断言 P => Q 和 Q => P。
注：假设读者已经阅读过“蕴含运算符”（Implication Operator）一章，因为它为本章奠定了基础。
setX() 函数
让我们从一个基本的 setter 函数开始。它接收一个 uint256 类型的输入并更新存储变量 x，但前提是新值必须严格大于当前值。此限制通过 require 语句强制执行，如果条件不满足，交易将回滚：
/// Solidity
uint256 public x;
function setX(uint256 _x) external {
require(_x > x, "x must be greater than the previous value");
x = _x;
}
为了使用蕴含运算符对此函数进行形式化验证，我们可以将交易成功与最终状态变化之间的关系表达为两个 assert 蕴含语句：
rule setX_usingImplication() {
uint256 _x;
mathint xBefore = x();
setX@withrevert(_x);
bool success = !lastReverted;
mathint xAfter = x();
assert success => xAfter > xBefore; // If the call succeeds, then x increased (P => Q)
assert xAfter > xBefore => success; // If x increased, then the call must have succeeded (Q => P)
}
证明器运行：链接
虽然在逻辑上是正确的，但编写两个单向蕴含（P => Q 和 Q => P）显得过于冗长。
CVL 中的双条件（<=>）
这里的目的是表达一个精确的规则：“当且仅当输入值大于 x 的当前值时，交易才会成功。”
这可以更简洁地写成：
rule setX_TxSucceeds_iff_XIncreases() {
uint256 _x;
mathint xBefore = x();
setX@withrevert(_x);
bool success = !lastReverted;
mathint xAfter = x();
assert success <=> xAfter > xBefore;
}
这一个 assert 双条件语句更加简洁，直接表达了调用成功与状态 x 的变化（增加）之间的双向关系。换言之，只有当 x 增加时函数才会成功，并且只有当调用成功时 x 才会增加。
正如预期的那样，此规则验证通过：
证明器运行：链接
隐式地，我们还可以推断出：如果调用失败，那么 x 就没有增加：
assert !success <=> !(xAfter > xBefore);
或者
assert !success <=> xAfter <= xBefore;
这已经被双条件所包含，不需要单独编写。
形式化验证 Solmate 的 mulDivUp()
在上一章（蕴含运算符）中，我们讨论了 Solmate 的 mulDivUp() 函数的行为、它的溢出检查和舍入逻辑。这里简要回顾一下：
- 如果
denominator == 0（除以零）或者x * y > MAX_UINT256（溢出），它将回滚。 mulDivUp(x, y, denominator)将x和y相乘，将结果除以denominator，如果有余数则向上舍入；否则，返回精确的商。
现在让我们使用双条件运算符对这些行为进行形式化验证。
回滚行为
让我们从回滚行为开始。我们首先编写最简单的回滚条件 denominator == 0，然后逐步构建出一条完整的规则。
正如我们所知，这将失败，因为它没有捕获所有的回滚场景，但这可以作为一个很好的起点：
rule mulDivUp_denominatorIsZero_revert() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
assert denominator == 0 <=> lastReverted;
}
由于 x 和 y 的乘积超过 max_uint256 的反例，该规则失败。我们需要将其作为额外的回滚条件包含在内：
这是修正后的 CVL 规则：
rule mulDivUp_allConditions_revert() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
assert denominator == 0 || x * y > max_uint256 <=> lastReverted;
}
证明器运行：链接
请注意，双条件是可逆的（不同于蕴含），所以我们可以这样重写断言：
rule mulDivUp_allConditions_revert() {
uint256 x;
uint256 y;
uint256 denominator;
mulDivUp@withrevert(x, y, denominator);
assert lastReverted <=> denominator == 0 || x * y > max_uint256;
}
证明器运行：链接
此外，由于双条件是组合的双向蕴含（P => Q 和 Q => P），两者在逻辑上是绑定在一起的；因此，通过 <=> 推理的表达式是不可分割的。
舍入行为
下面的规则指定了 mulDivUp() 函数的舍入行为。它断言当且仅当存在余数时，该函数返回向上舍入的值。双条件运算符保证存在余数是触发向上舍入的唯一条件，并且没有其他条件可以影响返回值：
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);
}
证明器运行：链接
何时使用双条件而不是蕴含
排除不确定性
如我们在上一章中所见，上面的规则可以使用 => 来编写，因为被验证的属性碰巧只有一个导致该结果的条件。在这种情况下，=> 可以替换为 <=>。这种替换是更好的选择，因为 <=> 表明除了指定的条件之外，没有其他任何东西可以导致该结果。蕴含运算符不提供此保证，因此在类似这些情况下，最好使用双条件来使该保证明确化。
在前面的示例（max 函数）中，我们考虑了所有的回滚条件，因为我们是在验证函数整体的正确性。然而，当处理一个调用多个内部函数的函数时，每个内部函数都可能导致不同的回滚条件，此时使用蕴含可能更加实用。这种方法仅关注导致回滚的必要条件，而无需穷尽处理每种可能的失败场景。
验证相互依赖关系
相互依赖发生于两个变量互相依赖时，意味着其中一个变量的变化会触发另一个变量的相应变化，反之亦然。
以 AMM 的 WETH/USDC 池为例：在交换（swap）期间，当且仅当 USDC 余额减少时 WETH 余额才会增加，反之亦然。这创造了一种双向依赖关系，即一种代币的余额必须响应另一种代币的变化而调整，表明这两种余额都不能独立变化。
总结
- 双条件（
<=>）明确保证了双向的蕴含关系。如果满足条件 P，则 Q 成立，并且如果 Q 成立，则也必须满足条件 P。 - 蕴含运算符（
=>）在条件导致结果时适用，但它不保证该结果只能由该条件引起。 - 当存在大量可能导致该结果的潜在条件时，使用双条件可能是不切实际的。
读者练习
- 形式化验证 Solady min 始终返回最小值（min）。
- 形式化验证 Solady zeroFloorSub 返回
max(0, x - y)。换言之，如果x小于y，它返回0。否则，返回x - y。
本文是使用 Certora Prover 进行形式化验证系列文章的一部分