在 CVL 中，mathint 类型表示无界整数，这与 Solidity 中诸如 uint256 等固定大小的类型不同。它在执行算术运算时不会发生溢出或下溢，从而允许基于纯数学进行推理。因此，它能够暴露在 unchecked 块或内联汇编中可能无法被检测到的溢出或下溢问题。

在本章中，你将学到：

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

Unchecked 块

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

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

Copy
/// Solidity

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

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

Copy
/// 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 的运算永远不会发生溢出或下溢。” - source

为了了解溢出是如何被检测到的，让我们快速梳理一下断言两侧的计算过程：

Copy
// 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 != 2^255，导致相等性检查失败。

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

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

require_uint256 是一个内置的 CVL 函数，用于将无界的 mathint 转换为有界的 uint256。根据 Certora 的文档：

“…… require 类型转换将忽略转换值超出范围的反例。” - source

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

以下是 CVL 规则：

Copy
/// CVL

rule average_overflowIgnored() {
    uint256 x;
    uint256 y;

    mathint returnVal = average(x, y);
    
    uint256 numerator = require_uint256(x + y);
    uint256 expectedVal = r
equire_uint256(numerator / 2);


    assert returnVal == expectedVal;
}

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

因此，expectedVal 始终等于 returnVal，从而使规则通过，同时悄悄地忽略了溢出问题：

Prover 运行结果：link

内联汇编

溢出/下溢的另一个来源是内联汇编。尽管它能够编写出对 Gas 高效的代码，但它绕过了 Solidity 的安全检查，包括对溢出和下溢的检查。

为了进行演示，请考虑使用内联汇编实现向上取整除法的 flawedCeilDiv() 函数。它映射了数学公式 (n + d - 1) / d，当存在非零余数时，该公式会将整数除法的结果向上取整。例如，6 / 3 的计算结果为 2，因为除法是精确的；而 5 / 2 的计算结果为 3，因为余数会强制向上取整。

以下是该函数的实现：

Copy
/// 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() 函数的预期行为：

Copy
/// 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 != 0 排除了除以零错误，这仅仅是为了演示目的，因为我们这里的重点是检测溢出行为，而不是除以零的情况。

不出所料，这里出现了一个违例，因为在计算 n + d 时发生了溢出：

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

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

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

Copy
/// 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 运行结果：link

验证 unsafeDivUp 的无溢出行为

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

Copy
/// Solidity

function unsafeDivUp(uint256 x, uint256 y) external pure returns (uint256 z) {
    /// @solidity memory-safe-assembly
    assembly {
        // Add 1 to x * y if x % y > 0. Note this will
        // return 0 instead of reverting if y is zero.
        z := add(gt(mod(x, y), 0), div(x, y))
    }
}

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

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

Copy
/// 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 运行结果：link

注意：前提条件 require d != 0 排除了除以零的情况，因为该规则仅侧重于验证无溢出行为。

作为最后的说明，Certora 提供了以下实用指南：

“一般的经验法则是，只要可能，就应该使用 mathint；仅对于将作为合约函数输入传递的数据使用 uint 或 int 类型。” - source

总结

• mathint 是 CVL 中的一种无界类型，用于对没有溢出或下溢的算术进行建模。
• CVL 中的算术运算默认为 mathint，通过避免意外地将类型转换为有界类型，使规范变得更安全。
• require_uint256 会将 mathint 类型限制在 uint256 范围内，从而忽略超出 max_uint256 的值。因此，它可以隐藏溢出问题。
• 只要可能，请尽量使用 mathint，并将 uint 或 int 仅用于合约函数的参数。

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