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

aave-dao 发布于 2025-02-13 阅读 1745

本文档是 Aave v3 不变量测试套件的内部文档，介绍了如何运行测试套件、属性格式、如何添加对新函数的支持、如何从 Foundry 迁移测试、如何迁移 Certora 属性以及如何调试broken属性。该套件使用 Echidna 工具来检查 Aave v3 协议的不变量和后置条件，并通过 property mode 和 assertion mode 两种不同的模式执行。

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

### 目录

1. [运行套件](#running-the-suite)

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

2. [属性格式](#property-formats)

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

3. [Handlers: 添加对新函数的支持](#handlers-adding-support-for-new-functions)

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

4. [从 Foundry 迁移测试](#migrating-tests-from-foundry)

- 概述
   - 迁移步骤

5. [迁移 Certora 属性](#migrating-certora-properties)

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

6. [调试损坏的属性](#debugging-broken-properties)

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

### 运行套件

- **前置条件**:

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

```sh
    cp .env.example .env

forge install
    ```

- 确保已安装最新版本的 **Echidna**。 如果未安装，可以按照[此处](https://github.com/crytic/echidna?tab=readme-ov-file#installation)的指南进行安装。

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

- **属性模式**: 检查协议不变量。 运行:
    ```sh
    make echidna
    ```
  - **断言模式**: 检查协议后置条件。 运行:

```sh
    make echidna-assert
    ```

- **额外**: 运行套件而不检查属性，仅增加语料库大小和覆盖率。 运行:
    ```sh
    make echidna-explore
    ```

- **配置**: 套件配置可以在 [echidna_config.yaml](https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/_config/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 线程数以获得最佳性能。

### 属性格式

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

#### 不变量

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

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

```solidity
 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` 文件，如以下代码片段所示:

```solidity
 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`

```solidity
 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 的末尾调用，如以下代码片段所示:

```solidity
    function _checkPostConditions() internal {
      // Implement post conditions here
      ...

// LENDING
 assert_LENDING_GPOST_C(); /// <--- 全局后置条件执行

...
    }
    ```

- **示例 HSPOST**: E_MODE_HSPOST_G

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

```solidity
    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); /// <--- 后置条件
 }
 }
 }
 ```

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

### 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` 参与者选择修饰符。 以下代码是如何实现这两个函数的方法:

```solidity
 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 之间调用，以确保缓存值以正确检查后置条件。

```solidity
 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`。

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

### 从 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. 使用断言模式重新运行测试，以确保新属性在更广泛的状态下成立。

### 迁移 Certora 属性

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

| Certora 属性              | Enigma Suite 属性 |
| --------------------------- | --------------------- |
| `invariant` 函数       | 不变量            |
| `rule` 函数            | HSPOST 后置条件 |
| 参数化 `rule` 函数 | GPOST 后置条件  |

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

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

### 调试损坏的属性

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

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

```solidity
  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...](https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

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

运行套件
- 前置条件
- 启动套件
- 配置
属性格式
- 不变量
- 后置条件
  - 全局后置条件 (GPOST)
  - Handler 特定后置条件 (HSPOST)
Handlers: 添加对新函数的支持
- 概述
- 添加新函数
- 测试新函数
从 Foundry 迁移测试
- 概述
- 迁移步骤
迁移 Certora 属性
- 概述
- 属性映射
- 迁移指南
调试损坏的属性
- 日志 & 输出
- Crytic to Foundry 测试助手
- 在 Foundry 包装器中复现 Echidna 错误的步骤

运行套件

前置条件:
- 确保所有协议依赖项已安装:
```
cp .env.example .env

forge install
```
- 确保已安装最新版本的 Echidna。如果未安装，可以按照此处的指南进行安装。
启动套件: 该套件能够检查 Aave v3 协议的不变量和后置条件。为此，它使用两种不同的模式，即属性模式和断言模式。
- 属性模式: 检查协议不变量。运行:
```
make echidna
```
- 断言模式: 检查协议后置条件。运行:
```
make echidna-assert
```
- 额外: 运行套件而不检查属性，仅增加语料库大小和覆盖率。运行:
```
make echidna-explore
```
配置: 套件配置可以在 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 线程数以获得最佳性能。

属性格式

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

不变量

定义: 不变量是必须在系统的所有状态中都为真的属性。当该工具在属性模式下运行时会检查这些属性，使 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 &lt; 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 &lt; debtTokens.length; ++i) {
    /// &lt;--- 循环遍历所有债务代币，
    /// 由于套件设置使用三个储备金，因此该循环将运行三次。
    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 &lt; 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(); /// &lt;--- 全局后置条件执行

  ...
}

示例 HSPOST: E_MODE_HSPOST_G

规范: 在切换或离开 emode 后，用户的健康因子必须 >= 1。

实现: 在 setUserEMode handler的末尾，检查后置条件。

function setUserEMode(uint8 i) external setup {
  bool success;
  bytes memory returnData;

  ... /// &lt;--- 变量缓存、参与者调用等，为简洁起见进行了总结

  if (success) {
    _after();

    // POST-CONDITIONS
    if (eModeCategory != previousUserEModeCategory) {
      ...
      assertGe(_getUserHealthFactor(address(actor)), 1, E_MODE_HSPOST_G); /// &lt;--- 后置条件
    }
  }
}

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

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); /// &lt;--- 随机基础资产选择

 uint8 categoryId = _getRandomEModeCategory(j); /// &lt;--- 随机 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; /// &lt;--- 变量以存储调用的成功和返回数据
 bytes memory returnData;

 uint8 eModeCategory = _getRandomEModeCategory(i); /// &lt;--- 随机 eMode 类别选择

 uint256 previousUserEModeCategory = pool.getUserEMode(address(actor));

 address target = address(pool);

 address[] memory assetsBorrowing = _getUserBorrowingAssets(
 address(actor)
 ); /// &lt;--- 缓存用于后置条件检查的所需变量

 _before(); /// &lt;--- Before hook
 (success, returnData) = actor.proxy( /// &lt;--- 对协议的代理调用
 target,
 abi.encodeWithSelector(IPool.setUserEMode.selector, eModeCategory)
 );

 if (success) {
 _after(); /// &lt;--- 成功后的 After hook

 // POST-CONDITIONS
 if (eModeCategory != previousUserEModeCategory) {
 /// &lt;--- 后置条件检查
 assertAssetsBorrowableInEmode(
 assetsBorrowing,
 eModeCategory,
 E_MODE_HSPOST_H
 );
 assertGe(_getUserHealthFactor(address(actor)), 1, E_MODE_HSPOST_G);
 }
 }
}
```
- 更新后置条件: 如果新函数引入了对协议状态的更改，请更新后置条件以反映这些更改。例如，如果使用新的 eMode 更新，则用户在切换或离开 emode 后的健康因子必须 >= 1。应如上面的示例所示实现后置条件 E_MODE_HSPOST_G。
测试: 添加新的 handler 函数并更新后置条件后，运行该工具以确保新逻辑被覆盖并正常工作。你可以在 echidna/default/_data/corpus 目录中检查 html 覆盖率报告。

从 Foundry 迁移测试

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

分步迁移:

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

将 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( /// &lt;--- 从 Foundry 迁移的后置条件 BORROWING_HSPOST_I
          IERC20(asset).balanceOf(address(actor)),
          actorAssetBalanceBefore + amount,
          BORROWING_HSPOST_I
      );
      ...
      }
  }
  ```

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

迁移 Certora 属性

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

Certora 属性	Enigma Suite 属性
`invariant` 函数	不变量
`rule` 函数	HSPOST 后置条件
参数化 `rule` 函数	GPOST 后置条件

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

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

调试损坏的属性

日志 & 输出: 在运行时，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 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

0 条评论

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

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

目录

运行套件

属性格式

不变量

后置条件

Handlers: 添加对新函数的支持

从 Foundry 迁移测试

迁移 Certora 属性

调试损坏的属性

相关文章

0 条评论

请输入验证码

登链社区服务条款与隐私政策

登链社区服务条款与隐私政策

登链社区用户服务条款

一、定义

二、服务内容

三、用户权利义务

四、知识产权保护

五、有限保证及服务免责

六、服务变更、中断或终止

七、通知和送达

八、投诉处理

九、法律适用、争议管辖及其他

隐私政策

一、登链社区可能收集的信息内容

二、登链社区收集信息的使用规则

三、登链社区如何共享、转让、公开披露您的个人信息

四、登链社区如何使用 Cookie 和同类技术

五、登链社区如何保护和保存您的个人信息

六、您如何管理个人信息

七、未成年人信息的保护

八、隐私政策的修订和更新

如何联系我们