Aave v3 不变量测试套件的内部文档

Aave v3 不变量测试套件内部文档

目录

1. 运行套件

   • 前置条件
   • 启动套件
   • 配置

2. 属性格式

   • 不变量
   • 后置条件
     • 全局后置条件 (GPOST)
     • Handler 特定后置条件 (HSPOST)

3. Handlers: 添加对新函数的支持

   • 概述
   • 添加新函数
   • 测试新函数

4. 从 Foundry 迁移测试

   • 概述
   • 迁移步骤

5. 迁移 Certora 属性

   • 概述
   • 属性映射
   • 迁移指南

6. 调试损坏的属性

   • 日志 & 输出
   • Crytic to Foundry 测试助手
   • 在 Foundry 包装器中复现 Echidna 错误的步骤

运行套件

• 前置条件:

  • 确保所有协议依赖项已安装:

  cp .env.example .env
  
  forge install

  • 确保已安装最新版本的 Echidna。 如果未安装，可以按照此处的指南进行安装。

  <br />

• 启动套件: 该套件能够检查 Aave v3 协议的不变量和后置条件。 为此，它使用两种不同的模式，即属性模式和断言模式。

  • 属性模式: 检查协议不变量。 运行:

    make echidna

  • 断言模式: 检查协议后置条件。 运行:

  make echidna-assert

  • 额外: 运行套件而不检查属性，仅增加语料库大小和覆盖率。 运行:

    make echidna-explore

  <br />

• 配置: 套件配置可以在 echidna_config.yaml 文件中找到。 此文件包含 Echidna 测试工具的配置，以下是配置中最重要的参数:

  • seqLen: 定义每个测试序列中的调用次数。
  • maxDepth: 设置要执行的测试序列的总数。
  • coverage: 启用覆盖率跟踪，存储在 corpusDir 指定的目录中。
  • corpusDir: 用于保存覆盖率数据的目录。 在此套件中，覆盖率保存在 tests/invariants/_corpus/echidna/default/_data/corpus 中。
  • deployContracts: 预先部署所需的库，以确保与 Echidna 和底层 hevm 的兼容性，特别是对于依赖于许多库的 Aave v3。 库使用带有 --compile-libraries 标志的 cryticArgs 参数链接。
  • workers: 设置 Echidna 的并行线程数，理想情况下接近机器的 CPU 线程数以获得最佳性能。 <br />

属性格式

正如公共文档中所述，此套件框架围绕两种类型的属性展开，即不变量和后置条件。 以下部分将详细解释每种类型的属性以及如何实现它们。

不变量

• 定义: 不变量是必须在系统的所有状态中都为真的属性。 当该工具在属性模式下运行时会检查这些属性，使 echidna 调用所有以 echidna_ 开头的公共函数，并确保其中的断言不会失败。 这些检查发生在测试序列中每次调用之间。

• 示例: BASE_INVARIANT_A

  • 规范: debtToken totalSupply 应该等于所有用户余额（用户债务）的总和。
  • 实现: BaseInvariants::assert_BASE_INVARIANT_A

  function assert_BASE_INVARIANT_A(IERC20 debtToken) internal {
    uint256 sumOfUserBalances;
    for (uint256 i; i < NUMBER_OF_ACTORS; i++) {
      sumOfUserBalances += debtToken.balanceOf(actorAddresses[i]);
    }
    assertEq(debtToken.totalSupply(), sumOfUserBalances, BASE_INVARIANT_A);
  }

  不变量的每个实现都必须在其包装器 echidna_** 函数中调用 Invariants.sol 文件，如以下代码片段所示:

  function echidna_BASE_INVARIANT_A() public returns (bool) {
    for (uint256 i; i < debtTokens.length; ++i) {
      /// <--- 循环遍历所有债务代币，
      /// 由于套件设置使用三个储备金，因此该循环将运行三次。
      assert_BASE_INVARIANT_A(IERC20(debtTokens[i]));
    }
    return true;
  }

• 实施指南:

  • 定义协议的核心属性（例如，余额约束、流动性检查、内部会计准确性）。
  • 保持断言清晰明了。 如果循环遍历用户、资产或储备金，请力求简单 - 避免过多或复杂的逻辑以保持效率和可读性（检查上面循环遍历套件参与者的示例）。
  • 通过确保不变量彼此之间没有过度重叠来最大程度地减少冗余。 但是，一定程度的重叠可能有利于覆盖更多场景，因此请考虑进行战略性重叠以最大程度地提高检查覆盖率。

后置条件

• 定义: 后置条件是必须在测试序列中特定操作或交互之后成立的属性。 它们有助于确保序列中的每个动作都产生有效的协议状态，从而专注于有针对性的结果而不是整个系统范围内的条件。 与在所有状态中一致检查的不变量不同，后置条件在指定点强制执行。 这些点包括每个 handler 调用的结束处（对于 handler 特定的后置条件）或 _after hook 的结束处（对于全局后置条件），从而验证特定动作的预期结果。

  正如公共文档所述，这些检查是在断言模式下执行的，其中 echidna 在检测到来自失败的 assert 语句的 Panic(1) 错误后会报告失败的警报。

• 类别: 这些后置条件可以分为两类：全局后置条件和 handler 特定后置条件。 全局后置条件 (GPOST) 在每个测试序列结束时使用 _after hook 检查，而 handler 特定的后置条件 (HSPOST) 在特定 handler 调用的结束时检查。

• 示例 GPOST: LENDING_GPOST_C

  • 规范: 如果储备金的 totalSupply 增加，则新的 totalSupply 必须小于或等于供应上限。
  • 实现: DefaultBeforeAfterHooks::assert_LENDING_GPOST_C

  function assert_LENDING_GPOST_C() internal {
    if (targetAsset == address(0)) return;
    uint256 totalSupplyUpdatedTreasury = _getRealTotalSupply(
      targetAsset,
      defaultVarsBefore.scaledTotalSupply,
      defaultVarsAfter.accruedToTreasury
    );
    if (totalSupplyUpdatedTreasury < defaultVarsAfter.totalSupply) {
      if (
        defaultVarsAfter.supplyCap != 0 &&
        msg.sig != IPoolHandler.mintToTreasury.selector
      )
        assertLe(
          defaultVarsAfter.totalSupply,
          defaultVarsAfter.supplyCap,
          LENDING_GPOST_C
        );
    }
  }

  每个全局后置条件都必须在 _checkPostConditions 函数中 _after hook 的末尾调用，如以下代码片段所示:

  function _checkPostConditions() internal {
    // Implement post conditions here
    ...
  
    // LENDING
    assert_LENDING_GPOST_C(); /// <--- 全局后置条件执行
  
    ...
  }

• 示例 HSPOST: E_MODE_HSPOST_G

  • 规范: 在切换或离开 emode 后，用户的健康因子必须 >= 1。
  • 实现: 在 setUserEMode handler的末尾，检查后置条件。

  function setUserEMode(uint8 i) external setup {
    bool success;
    bytes memory returnData;
  
    ... /// <--- 变量缓存、参与者调用等，为简洁起见进行了总结
  
    if (success) {
      _after();
  
      // POST-CONDITIONS
      if (eModeCategory != previousUserEModeCategory) {
        ...
        assertGe(_getUserHealthFactor(address(actor)), 1, E_MODE_HSPOST_G); /// <--- 后置条件
      }
    }
  }

• 实施指南:

  • 确定每个动作应产生的关键结果或状态更改（例如，余额更新、抵押品调整、利息累积）。
  • 旨在通过全局后置条件来补充不变量，确保仍然覆盖了无法实现为不变量的属性。 <br />

Handlers: 添加对新函数的支持

• 概述: 正如公共文档所述，handlers 充当工具和协议之间的一种中间件层。 这就是为什么将新功能添加到协议或升级协议时，必须添加或更新新的 handler 函数以支持新功能。 以下部分将详细说明如何在 handlers 中添加对新函数的支持。

• 添加新函数: 让我们以 Aave v3.2 升级为例，其中引入了 eMode 功能的更精细版本。 新功能允许将资产列在多个 eMode 中，从而删除了 setAssetEModeCategory 函数，转而使用两个更精细的函数 setAssetCollateralInEMode 和 setAssetBorrowableInEMode。 以下步骤展示了通过在 handlers 中添加对这些新函数支持的过程指南:

  • 识别 Handler: 确定哪个 handler 合约将负责新函数。 在本例中，PoolPermissionedHandler handler 负责与协议的所有 permissioned 交互，因此应在此处添加对新函数的支持。

  • 识别参数: 确定动作需要哪些参数，哪些可以随机化，哪些应该被限制，哪些应该从有限的集合（如 helper 存储数组）中获取。

  对于 setAssetCollateralInEMode 和 setAssetBorrowableInEMode 函数，参数如下:

  • asset: 要在 eMode 中设置的资产的地址。
  • eModeCategory: 要将资产设置到的 eMode 类别。
  • allowed: 一个布尔值，用于设置是否允许资产进入 eMode。

  对于 asset 参数，可以使用 _getRandomBaseAsset 函数从 helper 存储数组 baseAssets 中选择一个随机基础资产，对于 eModeCategory 参数，可以使用 _getRandomEModeCategory 函数从 helper 存储数组 ghost_categoryIds 中选择一个随机 eMode 类别。 最后，对于 allowed 参数，可以使用随机布尔参数。

  • 确定该动作是 permissioned 还是 permissionless: 如果该动作是 permissioned，则不需要使用参与者作为代理，因为套件设置为 poolAdmin，因此直接调用 handler 就足够了。 如果该动作是 permissionless，则必须使用参与者代理调用以及 setup 参与者选择修饰符。 以下代码是如何实现这两个函数的方法:

  function setAssetCollateralInEMode(
    bool allowed,
    uint8 i,
    uint8 j
  ) external {
    address asset = _getRandomBaseAsset(i); /// <--- 随机基础资产选择
  
    uint8 categoryId = _getRandomEModeCategory(j); /// <--- 随机 eCategory 选择
  
    // 直接调用 handler，因为套件具有 poolAdmin 角色
    contracts.poolConfiguratorProxy.setAssetCollateralInEMode(
      asset,
      categoryId,
      allowed
    );
  }

  permissionless 动作的外观如下:

  • 动作需要 eModeCategory 参数，因此可以使用 _getRandomEModeCategory 函数从 helper 存储数组 ghost_categoryIds 中选择一个随机 eMode 类别。
  • 函数应由参与者调用，因此使用 setup 修饰符和对协议的代理调用。
  • 函数应在 _before 和 _after hooks 之间调用，以确保缓存值以正确检查后置条件。

  function setUserEMode(uint8 i) external setup {
    bool success; /// <--- 变量以存储调用的成功和返回数据
    bytes memory returnData;
  
    uint8 eModeCategory = _getRandomEModeCategory(i); /// <--- 随机 eMode 类别选择
  
    uint256 previousUserEModeCategory = pool.getUserEMode(address(actor));
  
    address target = address(pool);
  
    address[] memory assetsBorrowing = _getUserBorrowingAssets(
      address(actor)
    ); /// <--- 缓存用于后置条件检查的所需变量
  
    _before(); /// <--- Before hook
    (success, returnData) = actor.proxy( /// <--- 对协议的代理调用
      target,
      abi.encodeWithSelector(IPool.setUserEMode.selector, eModeCategory)
    );
  
    if (success) {
      _after(); /// <--- 成功后的 After hook
  
      // POST-CONDITIONS
      if (eModeCategory != previousUserEModeCategory) {
        /// <--- 后置条件检查
        assertAssetsBorrowableInEmode(
          assetsBorrowing,
          eModeCategory,
          E_MODE_HSPOST_H
        );
        assertGe(_getUserHealthFactor(address(actor)), 1, E_MODE_HSPOST_G);
      }
    }
  }

  • 更新后置条件: 如果新函数引入了对协议状态的更改，请更新后置条件以反映这些更改。 例如，如果使用新的 eMode 更新，则用户在切换或离开 emode 后的健康因子必须 >= 1。 应如上面的示例所示实现后置条件 E_MODE_HSPOST_G。 <br />

• 测试: 添加新的 handler 函数并更新后置条件后，运行该工具以确保新逻辑被覆盖并正常工作。 你可以在 echidna/default/_data/corpus 目录中检查 html 覆盖率报告。 <br />

从 Foundry 迁移测试

• 概述: Foundry 单元和 staless 测试断言与 handler 特定后置条件密切相关，因为两者都执行确定的动作或一组动作，并检查在其执行后保持的关系和属性。 可以将这些测试和断言的大部分迁移到套件中（当前的一些后置条件已经从中获得灵感），从而确保协议仍在测试相同的属性以及变量之间的关系。

• 分步迁移:

  1. 识别两个环境中要迁移的动作。 例如，borrow 函数。

  2. 将 Foundry 断言转换为后置条件甚至不变量。 例如，在测试 test_variable_borrow 中，这个常见的断言 assertEq(balanceAfter, balanceBefore + borrowAmount); 可以转换为以下后置条件: BORROWING_HSPOST_I: 在成功借款后，参与者资产余额应增加借款金额

     这可以在 `borrow` handler 函数的末尾实现，如下所示:
     
     ```solidity
     function borrow(uint256 amount, uint8 i, uint8 j) external setup {
         bool success;
         bytes memory returnData;
     
         ...
         uint256 actorAssetBalanceBefore = IERC20(asset).balanceOf(address(actor));
     
         _before();
         (success, returnData) = actor.proxy(
         address(pool),
         abi.encodeWithSelector(
             IPool.borrow.selector,
             asset,
             amount,
             DataTypes.InterestRateMode.VARIABLE,
             0,
             onBehalfOf
         )
         );
         ...
     
         if (success) {
         _after();
         // POST-CONDITIONS
         assertEq( /// <--- 从 Foundry 迁移的后置条件 BORROWING_HSPOST_I
             IERC20(asset).balanceOf(address(actor)),
             actorAssetBalanceBefore + amount,
             BORROWING_HSPOST_I
         );
         ...
         }
     }
     ```

  3. 使用断言模式重新运行测试，以确保新属性在更广泛的状态下成立。 <br />

迁移 Certora 属性

• 概述: Certora 的框架与套件的方法密切相关，因此许多 Certora 属性可以直接迁移到套件中。 可能需要调整格式和结构，但核心逻辑应该可以很好地转换。 最重要的是，由于该套件基于参与者并使用有限的参与者集，因此可以轻松实现涉及计算用户值总和的属性，例如 BASE_INVARIANT_A。
• 属性类型: 以下是将 Certora 属性类型映射到 Enigma Suite 属性类型，高亮显示了每个属性在套件中如何转换:

• 迁移指南:
  • 不变量: 检查协议范围条件的 Certora invariant 函数通常可以实现为套件的不变量检查。
  • 后置条件:
  • Certora rule 函数通常与套件的 Handler 特定后置条件 (HSPOST) 对齐，该后置条件在单个 handler 调用后检查。
  • Certora 中的参数化 rule 函数（为所有协议动作实现规则）转换为套件中的 全局后置条件 (GPOST)，允许在执行后进行协议范围的检查。

仔细调整每个属性，特别是那些涉及参数化或依赖于特定协议状态的属性。 虽然 Certora 和套件之间的属性框架在概念上相似，但 形式验证 (Certora) 和 覆盖率引导模糊测试 (Enigma Suite) 之间的引擎、执行过程和环境差异很大。 这种差异可能会影响某些假设。 <br />

调试损坏的属性

• 日志 & 输出: 在运行时，Echidna 会显示一个终端 UI，该 UI 报告属性的状态（通过或失败）以及相关的调用堆栈。 当某个属性失败时，某些线程会启动一个“收缩”过程来简化调用堆栈，从而使调试更容易。 可以在 echidna_config.yaml 文件中使用 shrinkLimit 参数调整收缩 effort。 在完成失败属性的收缩后，可以使用 Ctrl+C 停止套件。 语料库和覆盖率数据会自动保存，并且仪表板的信息会输出到命令行，从而允许复制最小化的调用堆栈，以便使用 Foundry 包装器测试进行进一步调试。

• Crytic to foundry test helper: CryticToFoundry 文件充当调用堆栈复现器，可以轻松调试 echidna 输出中的调用堆栈。 以下是如何将 helper 用于失败属性的示例:

  function test_borrow_assertion() public {
  _setUpActorAndDelay(USER1, 453881);
  this.approveDelegation(
    1482526189130252178123437018605205213532554266044322803735452163998541884248,
    226,
    251
  );
  _setUpActorAndDelay(USER1, 42941);
  this.supply(1000000000000000001, 33, 89);
  _setUpActorAndDelay(USER1, 67960);
  this.setEModeCategory(118, 189, 2300, 30039);
  _setUpActorAndDelay(USER2, 287316);
  this.setUserEMode(145);
  _setUpActorAndDelay(USER2, 438639);
  this.borrow(2848252610, 0, 2);
  }

• 在 Foundry 包装器中复现 Echidna 错误的步骤:

  • 从 Echidna 输出中复制调用堆栈。
  • 启动 echidna_parser.py 工具。
  • 将调用堆栈粘贴到工具中。
  • 按 Enter 生成 Foundry 包装器测试。
  • 复制生成的测试并将其粘贴到 CryticToFoundry 文件中。
  • 运行测试并使用 foundry 详细输出 -vvvv 调试失败的属性。

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