简介

一些合约行为（属性）本质上是条件性的，在 CVL 中使用 if/else 这样的结构是形式化捕获条件行为的一种方法。

CVL 中的 if/else 语句的工作方式与其他语言相同。我们将在这里提供一些包含条件特性的代码的形式化验证示例。

断言与方法调用

让我们从形式化验证一个简单的函数开始，该函数接收两个无符号整数（uint256）并返回它们的和（uint256）。预期结果是条件性的：如果加法溢出，则函数回退（revert）；否则，返回总和。

下面是 add() 函数的 Solidity 实现：

Copy
/// Solidity

function add(uint256 x, uint256 y) external pure returns (uint256) {
    return x + y;
}

这里是 CVL 规范（sum 自 P__rover 版本 7.25.2 _起是一个保留关键字，_因此我们改为使用 _sum 。）：

Copy
/// CVL

methods {
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule add_sumWithOverflowRevert() {
    uint256 x;
    uint256 y;

    mathint _sum = x + y;
    
    if (_sum <= max_uint256) { // non-revert case
        mathint result = add@withrevert(x, y);
        assert !lastReverted;
        assert result == _sum;
    }
    else { // revert case
        add@withrevert(x, y);
        assert lastReverted; 
    }
}

让我们拆解一下上面规范代码中发生的事情。在接下来的几行中，

Copy
uint256 x;
uint256 y;

mathint _sum = x + y;

变量 _sum 被声明为 mathint（一种没有溢出限制的类型），这允许它准确地表示 x + y，即使该值超过了 max_uint256。这使我们能够通过比较 _sum 和 max_uint256 来检测溢出，并确定函数是否应该回退。

现在看接下来的几行，

Copy
if (_sum <= max_uint256) {
    mathint result = add@withrevert(x, y);
    assert !lastReverted;
    assert result == _sum;
}

如果 _sum = x + y 保持在 max_uint256 的边界内，则执行 Solidity 加法操作。

将 @withrevert 标签添加到函数中，以指示 Prover 包含回退路径或导致回退的参数。断言 !lastReverted 意味着如果总和没有溢出，我们绝不应该遇到回退。

最后，如下所示的 else 块通过预期在 _sum 超过 max_uint256 时发生回退，来处理溢出情况。

Copy
else {
    add@withrevert(x, y);
    assert lastReverted; 
}

正如预期的那样，此 CVL 规则的状态为 VERIFIED（已验证）：

Prover 运行结果：link

这个例子表明，可以在条件块或分支中调用 Solidity 函数并执行断言。

if 语句中的变量赋值

接下来，我们将形式化验证 Solady 库中经过 Gas 优化的 max 函数。

下面是 Solady 的 max 函数实现。尽管可能不那么一目了然，但它会返回 x 和 y 中较大的一个。如果 x 等于 y，该函数只需返回 x。

Copy
/// Solidity

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

请注意，我们将可见性从 internal 更改为 external，以消除对 harness 文件（测试桩文件）的需求，这超出了本章的讨论范围。

解释这个汇编实现的内部工作原理也超出了本章的范围。然而，如果你感到好奇，这里有一个在五分钟内涵盖了这些细节的视频：https://www.youtube.com/watch?v=4nDUQIk4oqQ。

现在，让我们继续对 Solady 的 max 函数进行形式化验证。它有两个变体：一个用于无符号整数，另一个用于有符号整数。由于两者遵循相同的基本概念，我们将重点关注无符号整数变体。

这是一个用于验证 Solady max 函数的初始 CVL 规则，但我们很快就会对其进行简化：

Copy
/// CVL

rule max_returnMax() {
    uint256 x;
    uint256 y;

    if (x >= y) {
        mathint max = max@withrevert(x, y);
        assert !lastReverted;
        assert max == x;
    }
    else {
        mathint max = max@withrevert(x, y);
        assert !lastReverted;
        assert max == y;
    }
}

在上述规则中，if 块验证当 x > y 时，最大值为 x，或者当 x = y 时，它直接返回 x，因为这两个值相同。else 块涵盖了剩余情况，即当 x < y 时，y 成为最大值。在任何一种情况下，我们都不允许回退，因为该函数绝不应该回退。

正如预期的那样，此规则的状态为 VERIFIED（已验证）：

Prover 运行结果：link

函数调用和断言不需要放在 if/else 块内。我们可以将函数调用移到 if 块之外，并在 if 块内部计算预期结果：

Copy
/// CVL

rule max_returnMax_modified() {
    uint256 x;
    uint256 y;

    mathint expectedMax;
    
    if (x >= y) {
        expectedMax = x;
    } else {
        expectedMax = y;
    }
    
    mathint resultMax = max@withrevert(x, y);
    assert !lastReverted;
    
    assert resultMax == expectedMax;
}

Prover 运行结果：link

将函数调用移出 if 语句可带来更高效的 CVL 代码，因为函数只被调用一次，而不是在每个条件分支中都被调用。这种影响目前可能还不太明显，但对于更复杂的规则来说，这种方法可能会很有益处，正如下一节将展示的那样。

降低验证器复杂性：以 mulDivUp 为例

mulDivUp() 是一个将两个无符号整数相乘、将乘积除以另一个无符号整数、并在存在余数时向上取整的函数。如果没有余数，它原样返回商。例如，5 / 2 为 2，但 mulDivUp(5, 2) 的结果为 3（由于向上取整）。相反，4 / 2 为 2，而 mulDivUp(4, 2) 的结果也为 2，因为没有余数。

此外，它在两种情况下会发生回退：当除数为零时，或者当分子（x 和 y 的乘积）超过 max_uint256 时。

我们将使用的实现来自 Solmate 的 mulDivUp()，这是一个用汇编编写的具有高 Gas 效率的函数。我们稍微修改了代码，将其可见性从 internal 更改为 external，以避免使用 harness 文件。

以下是 Solmate 的 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_UINT256, y)))))) {
    revert(0, 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 的余数大于零，则在结果中加一以向上取整；否则，结果保持不变。

现在我们知道了这个函数试图做什么，我们就可以继续进行形式化验证了。

为 mulDivUp 开发规范

这里有一个初始规范，它捕获了 Solmate mulDivUp() 函数的行为，随后会给出相关解释：

Copy
/// CVL

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

    if (denominator == 0) { // catches revert condition: if denominator is zero 
        mulDivUp@withrevert(x, y, denominator); 
        assert lastReverted;
    }
    else if (x * y > max_uint256) { // catches revert condition: multiplication overflows a max_uint256 value
        mulDivUp@withrevert(x, y, denominator);
        assert lastReverted;
    } 
    else { // catches all non-revert conditions
        if (x * y % denominator == 0) { // if there's no remainder after x * y and denominator division
            mathint result = mulDivUp@withrevert(x, y, denominator);
            
            assert !lastReverted;
            assert result == x * y / denominator;
        } 
        else { // if there's a remainder after x * y and denominator division
            mathint result = mulDivUp@withrevert(x, y, denominator); 
            
            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

当我们运行 Certora Prover 时，验证了 Solmate mulDivUp() 的正确性：

Prover 运行结果：link

从上面的代码中请注意，我们可以使用带有 else if 的多个条件分支，并且没有什么能阻止我们使用嵌套的 if/else 语句。然而，为了避免嵌套 if 语句（那会使得规则更难阅读），我们可以重新排列这些条件。

以下代码行处理了回退条件：

Copy
if (denominator == 0) {
    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted;
} 
else if (x * y > max_uint256) {
    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted;
}

如果满足这些条件中的任何一个，则该分支会断言 lastReverted，这意味着函数发生回退。虽然我们可以将这两个回退条件合并为一个，但我们稍后在讨论代码优化时再来处理这个问题。

如果未满足这两个回退条件，执行将转移到 else 语句，在该语句中会验证舍入行为。在 else 块中，还有另一组 if/else 语句定义了舍入行为的规范。

在 else 块中，如下所示，if 条件检查 x 和 y 的乘积在对分母取模时，其余数是否为零。在这种情况下，不需要向上取整，因此返回值是 x * y / denominator。然而，在 else 分支中，模运算产生的余数大于零，因此通过将 x * y / denominator 加 1 来执行向上取整。

Copy
else {
    if (x * y % denominator == 0) {
        mathint result = mulDivUp@withrevert(x, y, denominator);
        
        assert !lastReverted;
        assert result == x * y / denominator;
    } 
    else {
        mathint result = mulDivUp@withrevert(x, y, denominator);
        
        assert !lastReverted;
        assert result == (x * y / denominator) + 1;
    }
}

我们了解到 if/else 可以将验证合并在单个规则中，而不是创建多个规则。但是，它也有其缺点。随着被验证函数的复杂性增加，规范的复杂性也会不成比例地增长，我们接下来将对此进行讨论。

路径爆炸

使用 if/else 往往会创建条件分支、调用函数并在条件块本身内执行断言。发生这种情况时，Prover 会测试每个分支中的所有情况，这增加了必须评估的场景数量，并自然而然地减慢了规则的执行速度。

针对 mulDivUp 的优化后 CVL 规则

下面是优化后的规则，我们接下来将解释所做的更改。

Copy
/// CVL

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

    mathint result = mulDivUp@withrevert(x, y, denominator);

    if (denominator == 0 || x * y > max_uint256) {
        assert lastReverted;
    } 
    else {
        if (x * y % denominator == 0) {
            assert !lastReverted;
            assert result == x * y / denominator;
        } 
        else {
            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

我们所做的第一个改变是将回退条件合并到一个单独的 if 语句中：if (denominator == 0 || x * y > max_uint256) { … }。

然后，我们从各个分支中移除了所有的 mulDivUp@withrevert(x, y, denominator) 函数调用，并将它们隔离为一次单独的调用。这通过避免条件块内冗余的函数调用从而提高了效率。

Prover 运行时间基准测试

以下是低效代码与优化后代码之间的执行时间对比：

Prover 运行结果：link

查看上方的 Prover 报告，低效地使用 if/else 会显著拖慢规则的执行速度。比较低效版本和优化版本，低效代码的执行时间是优化代码的四倍。随着我们为包含复杂智能合约的实际项目开发规范时，这个问题只会变得更糟。

注意_：_ 要基于执行时间比较两个规则，我们必须同时运行它们，并通过在 CLI 命令中添加 –cache none 来确保关闭缓存。

必须处理所有条件

if/else 结构本质上要求涵盖所有条件。if 块处理特定的情况，而 else 块则充当对 if 中未明确提及的任何情况的“全捕捉”（catch-all）。

这既是一件好事，也是一件坏事。好处是它能确保考虑到所有的条件，防止遗漏情况。然而，有时我们只对特定条件的结果感兴趣，而不得不兼顾所有的条件可能会阻碍我们的进度并消耗大量时间。

例如，让我们从该规则中显式地省略一个回退情况：x * y > max_uint256，此时 Prover 将显示 x * y 超过 max_uint256 时的反例（counterexample）。

Copy
/// CVL

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

    mathint result = mulDivUp@withrevert(x, y, denominator);

    if (denominator == 0) { // intentionally omitted `x * y > max_uint256`
        assert lastReverted;
    } else {
        if (x * y % denominator == 0) {
            assert !lastReverted;
            assert result == x * y / denominator;
        } else {
            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

如果我们只对回退条件 denominator == 0 感兴趣，我们就无法使用 if/else 结构来专门考虑它（技术上来说，我们可以这样做，但这不够规范，最好避免）。我们还必须考虑所有其他回退的情况。

处理这个问题的惯用方法是使用蕴含操作符（implication operator），这将在下一章中介绍。

三元运算符

对于简单的条件逻辑，三元运算符是 if/else 语句的一种简洁替代方案。它使用语法 condition ? expressionA : expressionB，如果条件为 true，则返回 expressionA；否则，返回 expressionB。

我们前面的示例（max() 函数）可以直接转换为使用三元表达式，如下所示：

Copy
/// CVL

rule max_returnMax_ifElse() {
    uint256 x;
    uint256 y;

    mathint expectedMax;

    if (x >= y) {
        expectedMax = x;
    } else {
        expectedMax = y;
    }
    
    mathint resultMax = max@withrevert(x, y);
    assert !lastReverted;
    
    assert resultMax == expectedMax;
}

rule max_returnMax_ternary() {
    uint256 x;
    uint256 y;

    mathint resultMax = max@withrevert(x, y);
    assert !lastReverted;
    
    uint256 expectedMax = x > y ? x : y;
    assert resultMax == expectedMax;
}

Prover 运行结果：link

然而，在另一个示例 add() 中，我们也可以使用三元表达式，但只能是有选择性地使用。我们不能包含所有潜在的执行路径，如下所示：

Copy
/// CVL

rule add_sumWithOverflowRevert_ifElse() {
    uint256 x;
    uint256 y;

    mathint _sum = x + y;

    if (_sum <= max_uint256) {
        mathint result = add@withrevert(x, y);
        assert !lastReverted;
        assert result == _sum;
    } 
    else {
        add@withrevert(x, y);
        assert lastReverted; 
    }
}

rule add_sumWithOverflowRevert_ternary() {
    uint256 x;
    uint256 y;

    mathint _sum = x + y;
    mathint result = add@withrevert(x, y);

    assert _sum <= max_uint256 ? !lastReverted : lastReverted; // selective
}

Prover 运行结果：link

我们不能考虑到其他条件的原因是，三元运算中的返回表达式必须具有相同的类型。因此，像这样断言它是不可行的：_sum <= max_uint256 ? _sum : lastReverted，因为 _sum 是 mathint 类型，而 lastReverted 是一个布尔值。

最后，对于 mulDivUp()，我们也无法直接对其进行转换；我们必须逐个提取属性，并对每个属性应用三元运算，这类似于我们对 add() 所做的那样。

总结

• 由于熟悉其他编程语言，if/else 非常直观。
• 包含过多的条件分支会减慢 Prover 的速度，但优化可以提高效率。
• if/else 要求处理所有的条件，使得它对于孤立用例的验证来说不够实用。
• 三元运算符提供了一种简洁的替代方案，但在返回类型不同时无法使用。

读者练习

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

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