CVL 中的条件语句以及形式化验证 Solady 和 Solmate 的部分

本文介绍了如何在 Certora Verification Language (CVL) 中使用 if/else 语句和三元运算符进行形式化验证。通过实例展示了对 Solidity 合约中条件行为（如溢出处理、max 函数）的验证，并强调了优化 CVL 规则以提高验证效率的重要性。文章还讨论了 if/else 的局限性及三元运算符的适用场景。

Certora 形式化验证

CVL 中的条件语句以及 Solady 和 Solmate 部分内容的形式化验证

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

最后更新于 2026 年 2 月 13 日

引言

有些合约行为（属性）本身就是条件性的，在 CVL 中使用 if/else 等结构是形式化捕获条件行为的一种方式。

CVL 中的 if/else 语句与其他语言中的工作方式相同。我们将在此处提供形式化验证具有条件功能代码的示例。

断言和方法调用

我们首先形式化验证一个简单的函数，该函数接受两个无符号整数（uint256）并返回它们的和（uint256）。预期的结果是条件性的：如果加法溢出，函数将回滚；否则，它将返回和。

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

/// Solidity

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

这是 CVL 规范（sum 是自 P__rover 版本 7.25.2 以来的保留关键字，所以我们使用 _sum 代替。）：

/// 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) { // 非回滚情况
        mathint result = add@withrevert(x, y);
        assert !lastReverted;
        assert result == _sum;
    }
    else { // 回滚情况
        add@withrevert(x, y);
        assert lastReverted;
    }
}

让我们分解上面规范代码中发生的事情。在以下几行中，

uint256 x;
uint256 y;

mathint _sum = x + y;

变量 _sum 被声明为 mathint 类型，该类型没有溢出限制，允许它准确表示 $x + y$，即使它超过 $max\_uint256$。这使我们能够通过将 $\_sum$ 与 $max\_uint256$ 进行比较来检测溢出，并确定函数是否应该回滚。

现在在以下几行中，

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

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

正如预期的那样，CVL 规则已验证：

image

Prover 运行：链接

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

if 语句中的变量赋值

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

下面是 Solady max 函数的实现。即使它可能不那么明显，它也返回 $x$ 和 $y$ 中较大的一个。如果 $x$ 等于 $y$，函数只返回 $x$。

/// 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，以消除对辅助文件的需要，这超出了本章的范围。

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

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

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

/// 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$ 时，$max$ 值是 $x$，或者如果 $x = y$，它只是返回 $x$，因为两个值是相同的。else 块涵盖了剩余的情况，即 $x < y$，使 $y$ 成为最大值。无论哪种情况，我们都不允许回滚，因为函数不应该回滚。

正如预期的那样，此规则已验证：

image

Prover 运行：链接

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

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

image

Prover 运行：链接

将函数调用移到 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 来稍微修改了代码，以避免使用辅助文件。

以下是 Solmate mulDivUp() 函数：

/// Solidity

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

function mulDivUp(
    uint256 x,
    uint256 y,
    uint256 denominator
) external pure returns (uint256 z) {
    assembly {
        // 等同于 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 对 denominator 的模严格大于 0，
        // 则加 1 以向上舍入 x * y 除以 denominator 的结果。
        z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))
    }
}

汇编代码的解释超出了本章的范围，但注释描述了每行的功能。

在以下几行中，

// 等同于 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$，如果超过则触发回滚。

在最后一行，它定义了舍入行为：

// 如果 x * y 对 denominator 的模严格大于 0，
// 则加 1 以向上舍入 x * y 除以 denominator 的结果。
z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))

如果 $x * y$ 除以 $denominator$ 的余数大于 $0$，则将 $1$ 添加到结果中以向上取整；否则，结果保持不变。

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

为 mulDivUp 开发规范

以下是一个捕获 Solmate mulDivUp() 函数行为的初始规范，解释紧随其后：

/// CVL

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

    if (denominator == 0) { // 捕获回滚条件：如果除数为零
        mulDivUp@withrevert(x, y, denominator);
        assert lastReverted;
    }
    else if (x * y > max_uint256) { // 捕获回滚条件：乘法溢出 max_uint256 值
        mulDivUp@withrevert(x, y, denominator);
        assert lastReverted;
    }
    else { // 捕获所有非回滚条件
        if (x * y % denominator == 0) { // 如果 x * y 和 denominator 除法后没有余数
            mathint result = mulDivUp@withrevert(x, y, denominator);

            assert !lastReverted;
            assert result == x * y / denominator;
        }
        else { // 如果 x * y 和 denominator 除法后有余数
            mathint result = mulDivUp@withrevert(x, y, denominator);

            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

当我们运行 Certora Prover 时，Solmate mulDivUp() 被验证为正确：

image

Prover 运行：链接

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

以下几行处理回滚条件：

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$ 的乘积在对 $denominator$ 取模后是否余数为 $0$。在这种情况下，不需要向上取整，因此返回值是 $x * y / denominator$。然而，在 else 分支中，当模运算导致余数大于零时，通过将 $1$ 添加到 $x * y / denominator$ 来执行向上取整。

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 规则

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

/// 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 运行时基准

下面是低效代码和优化代码之间的执行时间比较：

image

Prover 运行：链接

从上面的 Prover 报告来看，if/else 的低效使用会显著减慢规则执行。比较低效版本和优化版本，低效代码的执行时间是优化代码的四倍。这个问题在为具有复杂智能合约的真实项目开发规范时只会变得更糟。

注意：为了比较两条规则的执行时间，我们必须同时运行它们，并确保通过在 CLI 命令中添加 --cache none 来关闭缓存。

必须处理所有条件

if/else 结构本质上要求所有条件都必须考虑到。if 块处理特定情况，而 else 块充当捕获所有未在 if 中明确提及的情况的全包。

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

例如，让我们故意省略一个回滚情况：$x * y > max\_uint256$，Prover 将显示 $x * y$ 超过 $max\_uint256$ 的反例。

/// CVL

rule mulDivUp_roundOrRevert_omittedARevertCase() {
    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;
        }
    }
}

image

如果我们只对回滚条件 $denominator == 0$ 感兴趣，我们不能仅使用 if/else 结构来考虑它（技术上可以，但很hacky，最好避免）。我们必须考虑所有其他回滚情况。

处理此问题的惯用方式是使用蕴含运算符，这将在下一章中介绍。

三元运算符

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

我们之前的示例 max() 函数可以使用三元表达式直接翻译，如下所示：

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

image

Prover 运行：链接

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

/// 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; // 有选择的
}

image

Prover 运行：链接

我们无法考虑其他条件的原因是三元运算中的返回表达式必须是相同类型。因此，像这样断言它：_sum <= max_uint256 ? _sum : lastReverted 是不可能的，因为 $\_sum$ 是 mathint 类型，而 $lastReverted$ 是 boolean 类型。

最后，对于 mulDivUp()，我们也无法直接翻译；我们必须像处理 add() 那样，逐一选择属性并对其应用三元运算符。

总结

  • if/else 由于熟悉其他编程语言而直观易懂。
  • 过多的条件分支会减慢 Prover 的速度，但优化可以提高效率。
  • if/else 要求处理所有条件，使其不适用于孤立案例验证。
  • 三元运算符提供了一种简洁的替代方案，但当返回类型不同时不起作用。

读者练习

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

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

  • 原文链接： rareskills.io/post/certo...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
RareSkills
RareSkills
https://www.rareskills.io/

RareSkills

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！