溢出和Mathint

使用 Certora 进行形式化验证

溢出和 Mathint

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

上次更新于 2026 年 2 月 13 日

在 CVL 中，mathint 类型表示无界整数，与 Solidity 的 uint256 等固定大小类型不同。它在没有溢出或下溢的情况下执行算术运算，这允许基于纯数学进行推理。因此，它会暴露出在 unchecked blocks 或 inline assembly 中可能未被检测到的溢出或下溢。

在本章中，你将学习：

• mathint 是什么以及为什么它是默认类型
• 如何从 mathint 转换为 uint256 以及这样做的危险
• 我们如何将优化的汇编代码与“预期”公式进行比较，并查看假设是否成立

Unchecked Block

在 Solidity 中，unchecked 块会禁用溢出/下溢检查。因此，在 CVL 中，我们应该使用 mathint 进行推理，以暴露这些溢出/下溢情况。

为了演示，考虑 average() 函数，它接受两个无符号整数并计算它们的平均值：

/// Solidity

function average(uint256 x, uint256 y) external pure returns (uint256) {
    unchecked {
        return (x + y) / 2;
    }
}

让我们通过编写以下规则来形式化验证该函数是否正确返回两个无符号整数的平均值：

/// CVL

rule average_overflow() {
    uint256 x;
    uint256 y;

mathint returnVal = average(x, y);

    assert returnVal == (x + y) / 2;
}

此规则失败，表明在求值 $x + y$ 期间发生了溢出。我们将在接下来解释原因。

CVL 算术默认求值为 mathint

检测到溢出是因为 CVL 断言 $(x + y) / 2$ 的右侧默认类型为 mathint。Certora 将 mathint 定义为：“……一种可以表示任意大小整数的类型；对 mathint 的操作永远不会溢出或下溢。” - 来源

为了了解溢出是如何被检测到的，让我们快速计算断言两边的值：

// assert `left-hand side` == `right-hand-side`
assert returnVal == (x + y) / 2;

让我们使用 Prover 使用的相同值（$2^{256} - 3$ 和 $3$，如图像所示）来计算平均值，并了解规则失败的原因。

由于右侧 $(x + y) / 2$ 默认求值为 mathint，它正确计算出平均值为 $2^{255}$：

• $x + y = 2^{256}$ （$x = 2^{256} - 3$ 且 $y = 0x3$）
• $2^{256} / 2 = 2^{255}$

左侧，即 Solidity 调用的 average() 函数的返回值 (returnVal)，求值为 $0$：

• $x + y = 0$ （当 $x = 2^{256} - 3$ 且 $y = 0x3$ 时）由于溢出
• $0 / 2 = 0$

虽然右侧由于无界的 mathint 而正确计算了平均值，但左侧 returnVal（Solidity 函数返回值）在执行 $x + y$ 期间溢出并回绕到零。这导致计算不匹配。因此，$0 \neq 2^{255}$，导致相等性检查失败。

由于 CVL 算术默认使用 mathint，编写规范更安全，因为它消除了将算术运算意外转换为有界类型的可能性。然而，它并不能阻止我们转换为 uint256，这可能是危险的，我们将在下一节中看到。

将 mathint 向下转型为 uint256 可能会危险地掩盖溢出/下溢问题

require_uint256 是一个内置的 CVL 函数，它将无界的 mathint 向下转型为有界的 uint256。根据 Certora：

“……require 转型将忽略 转型值超出范围的反例。” - 来源

为了演示，我们将重新审视之前的规则并重写它，以便 CVL 运算通过 require_uint256 “故意”使用 uint256。因此，重要的规则违规将被忽略。

这是 CVL 规则：

/// CVL

rule average_overflowIgnored() {
    uint256 x;
    uint256 y;

    mathint returnVal = average(x, y);

    uint256 numerator = require_uint256(x + y);
    uint256 expectedVal = require_uint256(numerator / 2);

    assert returnVal == expectedVal;
}

在上述规则中，断言的右侧 (expectedVal) 通过 require_uint256 限制在 uint256 范围内，这本质上排除了任何会导致溢出的输入。

因此，expectedVal 总是等于 returnVal，导致规则通过，同时悄无声息地忽略了溢出：

Prover 运行：链接

内联汇编

溢出/下溢的另一个来源是内联汇编。尽管它能实现省油的代码，但它绕过了 Solidity 的安全检查，包括溢出和下溢检查。

为了演示，考虑 flawedCeilDiv() 函数，它使用内联汇编实现向上取整除法。它模拟了数学公式 $(n + d - 1) / d$，当有非零余数时，该公式会向上舍入整数除法的结果。例如，$6 / 3$ 求值为 $2$，因为除法是精确的，而 $5 / 2$ 求值为 $3$，因为余数强制向上舍入。

以下是函数实现：

/// Solidity

function flawedCeilDiv(uint256 n, uint256 d) external pure returns (uint256 z) {
    assembly {
        z := div(sub(add(n, d), 1), d)
    }
}

以下是汇编的工作方式：

• add(n, d) → 计算 $n + d$
• sub(..., 1) → 减去 $1$ → $n + d - 1$
• div(..., d) → 执行除法

现在，让我们形式化验证公式 $(n + d - 1) / d$ 是否等同于 flawedCeilDiv() 函数的预期行为：

/// CVL

rule flawedCeilDiv_overflow() {
    uint256 n;
    uint256 d;

    require d != 0;

    mathint returnVal = flawedCeilDiv(n, d);
    mathint expectedVal = (n + d - 1) / d;

    assert returnVal == expectedVal;
}

注意：前置条件 require $d \neq 0$ 排除了除以零的错误，这里主要关注检测溢出行为，而不是除以零。

正如预期，由于在求值 $n + d$ 时发生溢出，存在违规：

我们特别想检查 flawedCeilDiv() 是否与 $(n + d - 1) / d$ 等效，但我们也意外地发现发生了溢出。这突显了为什么 CVL 算术运算默认使用 mathint。

强调将 mathint 向下转型可能掩盖溢出/下溢

为了强调为什么要避免将 CVL 算术运算向下转型为 uint256，我们有意将 expectedVal（默认是 mathint）限制在 uint256 范围内：

/// CVL

rule flawedCeilDiv_overflowIgnored() {
    uint256 n;
    uint256 d;

    require d != 0;
    mathint returnVal = flawedCeilDiv(n, d);

    uint256 numerator = require_uint256(n + d - 1);
    uint256 expectedVal = require_uint256(numerator / d);

    assert returnVal == expectedVal;
}

结果，超出了 uint256 范围的反例被忽略；因此，规则通过，隐藏了溢出行为：

Prover 运行：链接

验证 unsafeDivUp 的非溢出行为

让我们将 Solidity 函数 flawedCeilDiv() 替换为不会溢出的替代方案。其中一个实现是 Solmate 的 unsafeDivUp() 函数，如下所示：

/// Solidity

function unsafeDivUp(uint256 x, uint256 y) external pure returns (uint256 z) {
    /// @solidity memory-safe-assembly
    assembly {
        // 如果 x % y > 0，则将 x * y 加 1。
        // 注意，如果 y 为零，这将返回 0 而不是回滚。
        z := add(gt(mod(x, y), 0), div(x, y))
    }
}

注意：我们更改了函数的可见性为 external，以避免使用 harness，这超出了本文的范围。

现在，让我们形式化验证 $(n + d - 1) / d$ 是否等于 unsafeDivUp() 的预期行为：

/// CVL

rule unsafeDivUp_noOverflow() {
    uint256 n;
    uint256 d;

    require d != 0;
    mathint result = unsafeDivUp(n, d);

    mathint expected = (n + d - 1) / d;
    assert result == expected;
}

正如我们所见，该函数在它等同于 $(n + d - 1) / d$ 的假设下成立。由于 CVL 运算自然默认使用 mathint，我们可以观察到没有发生溢出（即使没有主动考虑）。

Prover 运行：链接

注意：前置条件 require $d \neq 0$ 排除了除以零的情况，因为此规则仅专注于验证非溢出行为。

最后一点，Certora 提供了以下实用指南：

“一般的经验法则是，尽可能使用 mathint；仅将 uint 或 int 类型用于将作为输入传递给合约函数的数据。” - 来源

总结

• mathint 是 CVL 中的一种无界类型，它在没有溢出或下溢的情况下建模算术运算。
• CVL 中的算术运算默认使用 mathint，通过避免意外地将算术运算转型为有界类型，使规范更安全。
• require_uint256 将 mathint 类型限制在 uint256 范围内，因此会忽略超出 $max\_uint256$ 的值。因此，它可能会隐藏溢出。
• 尽可能使用 mathint，并将 uint 或 int 用于合约函数参数。

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

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