使用 Halmos 进行现代不变性测试

本文介绍了使用 Halmos 工具进行智能合约状态不变性测试的演变过程。首先通过在无状态测试中模拟状态变化来实现，然后利用 Halmos 提供的 cheatcode 简化了测试代码，并加入了快照状态的机制以优化性能。最后展示了 Halmos v0.3.0 版本如何原生支持状态不变性测试，极大地简化了测试流程，并提供了升级和使用 Halmos 的方法。

halmos 的最初重点，我们的开源智能合约符号测试工具，一直是使 SMT 求解适用于无状态属性测试。这些是一个好的起点，并且是从无状态模糊测试的简单过渡，但它们不是智能合约测试的黄金标准。事实上，迄今为止最受欢迎的功能是对有状态不变性测试的支持。

在这篇文章中，我们将介绍不变性测试的模拟技巧，如何使用新的 cheatcode 来改进它，以及最后如何在 halmos v0.3.x 中完全摆脱它。

回顾：在无状态测试中模拟不变性测试

早在 2024 年，Antonio 就写了关于使用一些巧妙的技巧在 halmos 中模拟有状态不变性测试的文章。核心思想是，在单个无状态测试中，你可以将多个调用链接在一起，并在它们之间保留状态。让我们回顾一下 Antonio 在 MiniVat 示例 中的技术：

import "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";

import {MiniVat} from "src/MiniVat.sol";

contract MiniVatTest is Test, SymTest {
    MiniVat public minivat;

    function setUp() public {
        minivat = new MiniVat();
    }

    function check_minivat_n_full_symbolic(bytes4[] memory selectors) public {
        for (uint256 i = 0; i < selectors.length; ++i) {
            assumeValidSelector(selectors[i]);
            assumeSuccessfulCall(address(minivat), calldataFor(selectors[i]));
        }

        assertEq(
            minivat.debt(),
            minivat.Art() * minivat.rate(),
            "The Fundamental Equation of DAI"
        );
    }

    function calldataFor(bytes4 selector) internal view returns (bytes memory) {
        if (selector == minivat.init.selector) {
            return abi.encodeWithSelector(selector);
        } else if (selector == minivat.move.selector) {
            return
                abi.encodeWithSelector(
                    selector,
                    svm.createAddress("dst"),
                    svm.createInt256("wad")
                );
         } else if (selector == minivat.frob.selector) {
            return abi.encodeWithSelector(selector, svm.createInt256("dart"));
        } else if (selector == minivat.fold.selector) {
            return abi.encodeWithSelector(selector, svm.createInt256("delta"));
        } else {
            revert();
        }
    }
}

让我们详细看看发生了什么：

  1. halmos 看到 check_minivat_n_full_symbolic(bytes4[] memory selectors) 函数，它将其识别为无状态测试
  2. 因为 MiniVatTest 中有要运行的测试，所以 halmos 会部署它并运行 setUp()，从而将结果状态保留为 初始测试状态
  3. 然后就到了运行 check_minivat_n_full_symbolic 的时候了。因为它有 bytes4[] memory selectors 作为一个参数，halmos 将把它实例化为一个具体的符号 bytes4 值数组
  4. 然后，测试循环遍历 selector 数组以生成调用序列
  5. 调用 calldataFor 是样板代码，以确保我们为 调用 序列中的每个调用生成有效的符号数据
  6. 调用 assumeValidSelector 是一种表达我们感兴趣的 目标函数 的方式
  7. 然后测试对 address(minivat) (目标合约) 进行调用
  8. assumeSuccessfulCall 拒绝恢复的调用，这是一种在 状态空间探索 期间修剪路径的方式。
  9. 最后我们可以断言协议 不变性

这个过程也包含了不变性测试的必要要素：

  • 初始测试状态
  • 目标合约
  • 目标函数
  • 调用序列生成
  • 状态空间探索
  • 不变性断言

运行此测试会在 2.8 秒内产生结果（请注意，在原始文章中，它过去需要 12.6 秒）：

halmos --function check_minivat_n_full_symbolic
 [⠒] Compiling...
No files changed, compilation skipped

Running 1 tests for test/MiniVat.t.sol:MiniVatTest
Counterexample:
    halmos_dart_int256_ce68fb9_01 = 0x400000000000000000000000000000000000000000
    p_selectors[0]_bytes4_1801362_00 = 0x380dc3ca00000000000000000000000000000000000000000000000000000000
    p_selectors[1]_bytes4_616eaf4_00 = 0xe1c7392a00000000000000000000000000000000000000000000000000000000
    p_selectors_length_baece6c_00 = 0x02

[FAIL] check_minivat_n_full_symbolic(bytes4[]) (paths: 70, time: 2.75s, bounds: [selectors=[0, 1, 2]])
Symbolic test result: 0 passed; 1 failed; time: 2.77s

这在 MiniVat 上运行良好，它是 完整 Vat 合约 的简化版本，只有 4 个目标函数。MiniVat 有意地简单；真正的挑战是打破完整 Vat 合约的不变性。完整的 Vat 合约有 16 个目标函数，这意味着如果我们想支持它，我们将需要编写大量的样板代码，并且性能会受到很大的影响。

下面，我们将展示如何改进手动编写的有状态测试框架，以及如何使用最新版本的 halmos 对其进行简化。

💻 如果你想跟上，这个例子的完整代码可以在这里找到：https://github.com/0xkarmacoma/halmos-invariants-sandbox

支持完整的 Vat 合约，手动编写的方法

使用 svm.createCalldata(address)

Halmos 现在支持一些方便的 cheatcode (请参见 a16z/halmos-cheatcodes)：

// Create arbitrary symbolic calldata for the given contract address, name, or interface name.
// By default, view and pure functions are excluded.
// An optional boolean flag can be set to include view and pure functions.

// 为给定的合约地址、名称或接口名称创建任意符号 calldata。
// 默认情况下，视图和纯函数被排除。
// 可以设置一个可选的布尔标志来包含视图和纯函数。
function createCalldata(
    address contractAddress
) external pure returns (bytes memory);

function createCalldata(
    string memory contractOrInterfaceName
) external pure returns (bytes memory);

function createCalldata(
    string memory filename,
    string memory contractOrInterfaceName
) external pure returns (bytes memory);

这意味着我们可以完全摆脱 calldataFor 和 assumeValidSelector 辅助函数！

完整 Vat 测试的代码现在看起来像这样：

import {Test, console} from "forge-std/Test.sol";
import {SymTest} from "halmos-cheatcodes/SymTest.sol";
import {Vat} from "src/Vat.sol";

contract VatTest is Test, SymTest {
    Vat public vat;
    bytes32 public ilk = "gems";

    function setUp() public {
        vat = new Vat();
        vat.init(ilk);
    }

    function check_vat_n_full_symbolic() public {
        uint256  depth = vm.envOr("INVARIANT_DEPTH", uint256(2));
        console.log("generating call sequences with depth", depth);

        for (uint256 i = 0; i < depth; ++i) {
            assumeSuccessfulCall(
                address(vat),
                svm.createCalldata(address(vat)) // using the new cheatcode
            );
        }

        assertEq(
            vat.debt(),
            vat.vice() + vat.Art(ilk) * vat.rate(ilk),
            "The Fundamental Equation of DAI"
        );
    }

    function assumeSuccessfulCall(address target, bytes memory data) public {
        (bool success, ) = target.call(data);
        vm.assume(success);
    }
}

这会在 1-2 分钟内找到一个反例：

INVARIANT_DEPTH=2 halmos --function check_vat_n_full_symbolic --early-exit
[⠒] Compiling...
No files changed, compilation skipped

Running 1 tests for test/Vat.t.sol:VatTest
[console.log] generating call sequences with depth 2
Counterexample:
    p_dart_int256_45a168c_124 = 0x200000000000000000000000000000000000000000
    p_dink_int256_0cd2e65_123 = 0x00
    p_i_bytes32_ead0d7f_119 = 0x00
    p_ilk_bytes32_718b270_81 = 0x00
    p_rad_uint256_54a455e_46 = 0x8000000000000000000000000000000000000000000000000000000000000000
    p_selectors[0]_bytes4_1eee7ca_00 = 0x00
    p_selectors[1]_bytes4_018ac94_00 = 0x00
    p_selectors_length_14577c1_00 = 0x02
    p_u_address_b307c2b_44 = 0x00
    p_u_address_b5d362f_120 = 0x00
    p_v_address_2f08456_45 = 0x00
    p_v_address_3bc206a_121 = 0x00
    p_w_address_e6be6d6_122 = 0x00

[FAIL] check_vat_n_full_symbolic(bytes4[]) (paths:  455, time:  61.55s, bounds: [selectors=[0, 1, 2]])
Symbolic test result:  0 passed;  1 failed; time:  61.59s

让我们花点时间来解释一下 svm.createCalldata(address(vat)) 做了什么：

  • 它根据部署代码将地址映射回合约名称
  • 它查找合约的 ABI
  • 它为所有公共状态修改函数生成带有适当符号参数的 calldata，以及用于回退函数的空字节和字节

💡在 assumeSuccessfulCall 中添加 console.logBytes(data) 以检查自动生成的 calldata 字节。null

使用 vm.snapshotState()

在 AssumeSuccessfulCall 中，我们执行 (bool success, ) = target.call(data); 然后执行 vm.assume(success)，这使我们可以忽略已恢复的调用。

因为 revert 会撤消所有更改，所以拒绝已恢复的调用使我们可以跳过我们知道不会影响状态的路径。但是你可能有其他未恢复的调用，并且也不会更改状态！理想情况下，我们也会想要忽略这些。由于 v0.2.3 我们支持快照 cheatcode，因此我们可以执行以下操作：

mapping(uint256 => bool) public visited;

function check_vat_n_full_symbolic() public {
    uint256 depth = vm.envOr("INVARIANT_DEPTH", uint256(2));
    console.log("generating call sequences with depth", depth);

    // record the initial state snapshot
    // 记录初始状态快照
    visited[vm.snapshotState()] = true;

    for (uint256 i =  0; i < depth; ++i) {
        assumeSuccessfulCall(
            address(vat),
            svm.createCalldata(address(vat))
        );

        uint256 snapshot = vm.snapshotState();

        // skip if the snapshot has already been visited
        // 如果快照已经被访问过，则跳过
        vm.assume(!visited[snapshot]);

        // keep track of new snapshots
        // 跟踪新的快照
        visited[snapshot] = true;
    }

    assertEq(
        vat.debt(),
        vat.vice() + vat.Art(ilk) * vat.rate(ilk),
        "The Fundamental Equation of DAI"
    );
}

在 halmos 中，snapshotState() 返回网络状态（存储、余额、帐户代码）的哈希值，这意味着我们可以比较快照。如果网络状态根本没有改变，那么快照也应该保持不变。

不幸的是，由于在 Solidity 中接触存储的开销，这并没有导致实际的加速，但这个想法本身是合理的。我们只需要 halmos 本身的一些帮助。最后一节介绍了 halmos v0.3 如何提供帮助。

启用任意时间戳、值和发送者

我们当前的方法仍然存在一些问题，限制了它的通用性：

  • 发送者是固定的，每个调用都来自测试地址 (address(this))
  • 区块时间戳永远不会改变
  • 我们从不发送任何值，因此无法正确探索目标合约中的 payable 函数

我们可以通过修改 assumeSuccessfulCall 来解决这些问题：

function assumeSuccessfulCall(address target, bytes memory data) public {
    // allow any sender and value for this call
    // 允许此调用的任何发送者和值
    address sender = svm.createAddress("sender");
    uint256 value = svm.createUint256("value");
    vm.deal(sender, value);

    // also allow any block timestamp to simulate calls in different blocks
    // 还允许任何区块时间戳来模拟不同区块中的调用
    uint256 timestamp = svm.createUint256("timestamp");
    vm.assume(timestamp >= block.timestamp);
    vm.warp(timestamp);

    vm.prank(sender);
    (bool success, ) = target.call{value: value}(data);
    vm.assume(success);
}

通过这些新的修改，我们更通用但仍然是手动编写的有状态测试 “框架” 现在可以在 3 分钟内打破 DAI 不变性：

halmos --function check_vat_n_full_symbolic --early-exit
 [⠒] Compiling...
 [⠃] Compiling 1 files with Solc 0.8.28
 [⠊] Solc 0.8.28 finished in 776.31ms
Compiler run successful!

Running 1 tests for test/Vat.t.sol:VatTest
[console.log] generating call sequences with depth 2
Counterexample:
    halmos_sender_address_80cde3f_47 = 0x7fa9385be102ac3eac297483dd6233d62b3e1496
    halmos_sender_address_97bc225_96 = 0x7fa9385be102ac3eac297483dd6233d62b3e1496
    halmos_timestamp_uint256_afd7084_49 = 0x8000000000000000000000000000000000000000000000000000000000000000
    halmos_timestamp_uint256_e79e87f_98 = 0x8000000000000000000000000000000000000000000000000000000000000000
    halmos_value_uint256_1dc9b21_48 = 0x00
    halmos_value_uint256_6e7e9ac_97 = 0x00
    p_dart_int256_749817d_32 = 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
    p_dink_int256_a5650cc_31 = 0x00
    p_i_bytes32_30b6237_27 = 0x00
    p_i_bytes32_8de9b03_62 = 0x00
    p_rate__int256_9900444_64 = 0x01
    p_u_address_482aaa5_28 = 0x00
    p_u_address_e8dc543_63 = 0x00
    p_v_address_74d52aa_29 = 0x00
    p_w_address_c739174_30 = 0x00

[FAIL] check_vat_n_full_symbolic() (paths: 1091, time: 179.83s, bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 179.89s

在 halmos v0.3.0 发布之前，这可能是模拟有状态不变性测试的最佳方式。

将所有内容与现代 halmos 结合在一起

由于 halmos v0.3.0 支持开箱即用的不变性测试，我们可以按如下方式重写测试：

import "forge-std/Test.sol";

import {Vat} from "../src/Vat.sol";

/// @custom:halmos --early-exit --invariant-depth 2
contract VatTest is Test {
    Vat public vat;
    bytes32 ilk;

    function setUp() public {
        vat = new Vat();
        ilk = "gems";

        vat.init(ilk);
    }

    function invariant_dai() public view {
        assertEq(
            vat.debt(),
            vat.vice() + vat.Art(ilk) * vat.rate(ilk),
            "The Fundamental Equation of DAI"
        );
    }
}

所有的辅助函数和样板代码都消失了！另请注意，不需要边界或钳制。我们只是用完全无界的值探索状态空间，并让符号引擎发现约束。

在底层，halmos 实现了我们以前必须手动推出的所有功能：

  • 目标合约选择（在本例中仅为 Vat，因为它是在 setUp() 期间部署的

  • 目标函数选择 (所有 Vat 的公共函数)

  • 每个目标函数的符号 calldata 生成

  • 访问过的状态快照

  • 任意发送者、值和区块时间戳

  • 用于设置最大调用序列长度的命令行选项 (--invariant-depth)

    • *

要试用它，请升级到最新版本：

  1. 安装 uv
  2. 如果你尚未安装 halmos，请运行 uv tool install --python 3.13 halmos
  3. 如果你已经有 uv 安装的 halmos，运行 uv tool upgrade halmos

然后查看 不变性测试示例。要运行这篇文章中的最后一个例子： git clone git@github.com:a16z/halmos.git halmos --root halmos/examples/invariants --function invariant_dai 感谢 aviggiano and igorganich 为这篇文章的早期版本提供了反馈。

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

0 条评论

请先 登录 后评论
a16z Crypto
a16z Crypto
https://a16zcrypto.com/

a16z Crypto

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