在本章中，我们将学习如何使用 CVL 中的方法标签（@withrevert 和 @norevert）以及特殊变量 lastReverted 来验证智能合约执行中预期的 revert。

为 Add() 函数设置验证场景

考虑以下 Math 合约，它有一个基础的 add() 函数，接收两个无符号整数作为输入，并返回它们的和作为输出。

Copy
//SPDX-License-Identifier : MIT
pragma solidity 0.8.25;

contract Math {

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

add() 函数的行为如下：

1. 当提供有效的输入时，它应该正确地计算 x 和 y 的和，并将其作为 uint256 值返回。例如，add(15, 10) 将返回 25。
2. 由于合约使用的是 0.8.0 或更高版本的 Solidity，如果和超过 uint256 的最大值（2^256 - 1），交易将会 revert。例如，如果 x = 2^256 - 1 且 y = 1，溢出将导致交易发生 revert，而不是返回结果。

验证 add() 函数规范

考虑以下规范（specification），用于验证 Math 合约中 add() 函数的正确性：

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

rule checkAdd() {

    uint256 a;
    uint256 b;
    uint256 c = add(a,b);

    assert a + b == c;
}

要查看上述规范的验证结果，请运行 Prover 并打开验证链接，您将看到类似于下图的结果。

这看起来可能令人惊讶，因为当 x 和 y 的总和超过 uint256 的最大值时，预期 add() 函数应该会 revert。由于 Prover 会探索不同的执行路径来验证正确性，人们自然会认为它也会遇到 revert 的情况。在这种情况下，assert 语句的计算结果应为 false，因此该 rule 应该无法通过验证。

然而，事实并非如此，我们的 rule 依然被 Prover 验证通过了。这是因为，在默认情况下，Prover 会在验证过程中忽略 revert 的情况。

这就提出了一个重要的问题：为什么 Prover 在验证过程中会选择忽略 revert 的情况呢？

为什么 Prover 会忽略 Revert 路径？

原因是 revert 可能是正常操作的一部分——例如，如果合约所有者以外的其他人试图执行特权操作。在这种情况下，revert 不会被视为失败；它就是预期的行为。

通过忽略 revert 路径，Prover 将专注于验证函数无错完成的成功执行场景。不过，我们可以使用 CVL 提供的 @withrevert 方法标签来覆盖这种默认行为。

CVL 方法标签简介

Certora 为我们提供了两个方法标签：@norevert 和 @withrevert。它们可以放置在方法名称之后、方法参数之前，如下所示：

Copy
function_name@norevert();
function_name@withrevert();

当我们对方法调用使用 @norevert 标签时，Prover 会主动忽略任何导致 revert 的执行路径。换句话说，function_name@norevert() 的行为与 function_name() 完全相同。

另一方面，当我们对方法调用使用 @withrevert 标签时，Prover 就不再忽略 revert 的情况了。相反，它会将发生 revert 的任何场景视为一种违规（violation）。例如，请考虑下面带有 @withrevert 标签的 checkAdd() rule：

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

rule checkAdd() {

    uint256 a;
    uint256 b;
    
    uint256 c = add@withrevert(a,b);

    assert a + b == c;
}

当我们使用更新后的规范重新运行 Prover 时，结果发生了变化：该 rule 现在的验证失败了，如下图所示：

由于我们在调用 add() 函数时使用了 @withrevert 标签，Prover 不再忽略 revert 的情况。因此，如果 a 和 b 的总和超过 uint256 的最大值，该 rule 就会将 revert 视为违规。验证器（verifier）检测到了这个问题并报告了一个反例（counterexample）——一个会导致溢出和 revert 的反例，最终导致断言（assertion）失败。当发生 revert 时，没有返回值——c 是不受约束的，可以取任意值。正因为如此，断言 a + b == c 无法成立。

引入 CVL 特殊变量： lastReverted

在 CVL 中，我们可以访问一个名为 lastReverted 的特殊布尔变量，该变量在每次方法调用后都会更新——包括那些没有使用 @withrevert 的调用。这个变量表示最近执行的合约函数是发生了 revert（lastReverted = true）还是执行成功（lastReverted = false）。

然而，在默认情况下，Prover 会忽略任何会导致 revert 的执行路径。这意味着，在不使用 @withrevert 调用函数时——例如默认调用或使用 @norevert 标签——Prover 不会去探索 revert 的场景，且 lastReverted 的值将始终保持为 false。

为了准确跟踪函数是否发生了 revert，我们必须使用 @withrevert 标签明确指示 Prover 考虑 revert 路径。当使用 @withrevert 调用函数时，Prover 不再忽略 revert 场景，一旦发生 revert，lastReverted 就会更新为 true。

示例：检测由溢出导致的 Revert

现在，让我们看看如何在实际的验证 rule 中使用 lastReverted。我们将测试 add() 函数，确保它在发生溢出和不发生溢出的情况下都能表现正常。

情况 1：函数应当在溢出时 Revert

考虑下面的 addShouldRevert() rule，旨在验证当发生溢出时，add() 函数能够正确地 revert。

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

rule addShouldRevert() {

    uint256 a;
    uint256 b;

    require(a + b > max_uint256);

    add@withrevert(a,b);

    assert lastReverted; // This is the same as assert lastReverted == true;
}

addShouldRevert() rule 中的 require(a + b > max_uint256); 语句确保所选取的输入 a 和 b 的总和超过了 uint256 所能存储的最大值，从而引发溢出。Solidity 的算术运算在溢出时会自动发生 revert，进而触发了 add(a, b) 函数调用的 revert。

注意：在 CVL 中，不同整数类型的最大值均可作为变量使用，例如 max_uint8, max_uint16, …, max_uint256 等。

因为函数是通过 @withrevert 调用的，Prover 不会忽略这个 revert 场景，并能正确检测到它。因此，lastReverted 被设置为 true，表示函数执行发生 revert。接着断言 assert lastReverted; 计算结果为 true，因为 lastReverted 符合预期结果。因此，该 rule 应该能顺利通过验证，如下图所示。

情况 2：函数在有效的加法运算时不应 Revert

同理，考虑 addShouldNotRevert() rule，它旨在验证当 a 和 b 的总和保持在有效的 uint256 范围内时，add() 函数不会 revert。

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

rule addShouldNotRevert() {

    uint256 a;
    uint256 b;

    require(a + b <= max_uint256);

    add@withrevert(a,b);

    assert !lastReverted;
}

在上述 rule 中，语句 require(a + b <= max_uint256); 确保所选择的输入 a 和 b 的总和不会引发溢出。由于 Solidity 的算术运算仅在发生溢出或其他明确的失败时才会 revert，所以 add(a, b) 函数将成功执行且不发生 revert。

因为函数是使用 @withrevert 调用的，Prover 会跟踪是否发生了 revert。然而，因为加法并没有超出 uint256 的限制，没有发生 revert，且 lastReverted 仍为 false。断言 assert !lastReverted; 验证了这一点，确保 rule 成功通过验证，如下所示。

避免 lastReverted 被覆盖

由于 lastReverted 在每次函数调用后都会更新，后续调用可能会覆盖其值。这意味着如果某个函数发生了 revert，而紧接着又执行了另一个函数，那么原始的 revert 状态就会丢失。

为了防止验证错误，务必在可能覆盖其值的任何额外调用发生之前，在相关函数调用结束后立即捕获 lastReverted。

为了说明这一点，让我们考虑一个简单的算术合约：

Copy
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract Math {

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

    function divide(uint256 x, uint256 y) public pure returns (uint256) {
        return x / y;
    }
}

上面的合约定义了两个基础函数：

• add(x, y) 只是返回 x 和 y 的和。
• divide(x, y) 执行整数除法运算，由于 Solidity 内置的除零保护，当 y == 0 时会发生 revert。

现在，考虑以下用来验证这两个函数在接收 0 作为第二个参数时表现的 rule：

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

rule checkMath() {

    uint256 a;
    
    divide@withrevert(a,0);
    bool divideCallStatus = lastReverted;

    add@withrevert(a,0);
    bool addCallStatus = lastReverted;

    assert divideCallStatus == true;
    assert addCallStatus == false;
}

如果我们在调用 divide(a, 0) 之后没有立即存储 lastReverted，下一次函数调用（add(a, 0)）将再次更新它，从而完全抹去关于除法操作失败的信息。

这意味着如果 rule 随后去检查 divide(a, 0) 是否 revert，它可能会错误地得出函数执行成功的结论——尽管它实际上失败了。这种错误的验证可能导致合约分析失准，从而在关键逻辑中引发安全漏洞或错误假设。

通过在调用 divide(a, 0) 后立即存储 lastReverted，我们确保能够在进行任何其他调用之前，准确地捕获函数的行为。这可以保留正确的执行历史，防止意外覆盖，并确保可靠的验证。

总结

在对方法进行形式化验证时，测试成功和 revert 两种情况都是至关重要的，因为它提供了更好的覆盖率，并确保该方法在所有可能的输入条件下（包括溢出或无效输入等边缘情况）均能表现正确。

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