AaveV3HorizonProtectionSuite

Git Source

Inherits: LendingProtectionSuiteBase

Title: AaveV3HorizonProtectionSuite

Author: Phylax Systems

Example ILendingProtectionSuite targeting a local Aave v3 Horizon deployment.

This is intentionally aligned with the Aave v3 Horizon pool paths found in ~/Documents/code/solidity/aave-v3-horizon/:

• borrow(...)
• withdraw(...)
• liquidationCall(...)
• setUserUseReserveAsCollateral(asset, false)
• finalizeTransfer(...) for aToken transfers that reduce effective collateral.

Constants

HEALTH_FACTOR_METRIC

bytes32 internal constant HEALTH_FACTOR_METRIC = 0x4845414c54485f464143544f5200000000000000000000000000000000000000

WITHDRAW_CLAIM_CHECK

bytes32 internal constant WITHDRAW_CLAIM_CHECK = "WITHDRAW_CLAIM"

LIQUIDATION_DEBT_CHECK

bytes32 internal constant LIQUIDATION_DEBT_CHECK = "LIQUIDATION_DEBT"

LIQUIDATION_COLLATERAL_CHECK

bytes32 internal constant LIQUIDATION_COLLATERAL_CHECK = "LIQUIDATION_COLLATERAL"

HEALTH_FACTOR_THRESHOLD

uint256 internal constant HEALTH_FACTOR_THRESHOLD = 1e18

HEALTH_FACTOR_THRESHOLD_INT

int256 internal constant HEALTH_FACTOR_THRESHOLD_INT = 1e18

POOL

address internal immutable POOL

ADDRESSES_PROVIDER

address internal immutable ADDRESSES_PROVIDER

Functions

constructor

Creates an Aave v3 Horizon suite bound to a specific pool.

The assertion adopter should also be this pool, since the monitored selectors are all pool entrypoints or pool callbacks.

constructor(address pool_) ;

Parameters

getMonitoredSelectors

Returns the Aave v3 Horizon pool selectors relevant to the shared lending invariants.

These map directly to the protocol paths that Aave v3 Horizon guards with the health factor checks or bounded-consumption checks relevant to the shared lending invariants.

function getMonitoredSelectors() external pure override returns (bytes4[] memory selectors);

Returns

decodeOperation

Decodes an Aave v3 Horizon pool call into the shared lending operation model.

Aave v3 Horizon mixes calldata-owned and caller-owned account semantics:

• borrow(...) checks the onBehalfOf account.
• withdraw(...) and setUserUseReserveAsCollateral(...) act on msg.sender.
• liquidationCall(...) checks the liquidated user, with asset = debtAsset and relatedAsset = collateralAsset.
• finalizeTransfer(...) checks the from account when collateral leaves. Calls that do not reduce risk headroom are returned as neutral operations and filtered later by shouldCheckPostOperationSolvency(...).

function decodeOperation(TriggeredCall calldata triggered)
    external
    pure
    override
    returns (OperationContext memory operation);

Parameters

Returns

shouldCheckPostOperationSolvency

Filters decoded Aave v3 Horizon operations down to the ones that must preserve solvency.

This suite only checks paths that either increase debt or reduce effective collateral for a concrete account. Neutral operations are ignored to keep the assertion cheap and avoid false positives from selectors that are monitored broadly.

function shouldCheckPostOperationSolvency(OperationContext calldata operation)
    external
    pure
    override
    returns (bool shouldCheck);

Parameters

Returns

getConsumptionChecks

Returns the bounded-consumption checks implied by the decoded Aave v3 Horizon operation.

This example exposes two shared resource bounds:

• withdraws cannot consume more aToken claim than the user had before the call
• liquidations cannot move more debt from the liquidator into the debt reserve than the user owed before the call, and cannot move more collateral to the liquidator than the user had before the call Other operation kinds return an empty array.

function getConsumptionChecks(
    TriggeredCall calldata triggered,
    OperationContext calldata operation,
    PhEvm.ForkId calldata beforeFork,
    PhEvm.ForkId calldata afterFork
) external view override returns (ConsumptionCheck[] memory checks);

Parameters

Returns

getAccountSnapshot

Reads the post-call account snapshot needed by the Aave v3 Horizon solvency invariant.

Hot path override: the invariant itself only needs Aave’s aggregate health factor, so the suite skips per-reserve enumeration here. getAccountBalances(...) remains available for richer debugging or derived assertions.

function getAccountSnapshot(address account, PhEvm.ForkId calldata fork)
    external
    view
    virtual
    override
    returns (AccountSnapshot memory snapshot);

Parameters

Returns

getAccountState

Reads Aave v3 Horizon aggregate account metrics from Pool.getUserAccountData(...).

The returned AccountState uses Aave’s base-currency values for total collateral and total debt, and stores the additional health-factor inputs in metadata.

function getAccountState(address account, PhEvm.ForkId calldata fork)
    external
    view
    override
    returns (AccountState memory state);

Parameters

Returns

getAccountBalances

Enumerates Aave v3 reserve balances for the account.

This is not needed on the hot path for the example invariant, but it shows how a suite can still expose per-reserve state for debugging, richer assertions, or protocols whose solvency rule depends on per-asset inspection.

function getAccountBalances(address account, PhEvm.ForkId calldata fork)
    external
    view
    override
    returns (AccountBalance[] memory balances);

Parameters

Returns

evaluateSolvency

Evaluates Aave v3 Horizon solvency from aggregate account state.

The example intentionally ignores per-reserve balances because Aave v3 Horizon’s own post-action checks reduce to health factor over aggregate pool data. Suites for other protocols may need to inspect the balances argument instead.

function evaluateSolvency(
    AccountState calldata state,
    AccountBalance[] calldata balances,
    PhEvm.ForkId calldata fork
) external pure override returns (SolvencyState memory solvency);

Parameters

Returns

_getAccountState

Internal helper that reads and normalizes Aave v3 Horizon aggregate account data.

This is the canonical aggregate-state implementation used by both getAccountState(...) and the optimized getAccountSnapshot(...) hot path.

function _getAccountState(address account, PhEvm.ForkId memory fork)
    internal
    view
    returns (AccountState memory state);

Parameters

Returns

_getAccountBalances

Internal helper that expands the account into reserve-level balances and values.

Reads the reserve list, user collateral bitset, reserve token addresses, and oracle prices, then emits one balance entry per reserve with a non-zero collateral or debt balance. The values are normalized to Aave’s base currency.

function _getAccountBalances(address account, PhEvm.ForkId memory fork)
    internal
    view
    returns (AccountBalance[] memory balances);

Parameters

Returns

_getWithdrawClaimCheck

Builds the withdraw bounded-consumption check from Aave v3 Horizon call output and pre-state.

Pool.withdraw(...) returns the actual amount withdrawn, which already handles the type(uint256).max full-withdraw path. The available pre-operation claim is the user’s aToken balance before the call.

function _getWithdrawClaimCheck(
    TriggeredCall calldata triggered,
    OperationContext calldata operation,
    PhEvm.ForkId calldata beforeFork
) internal view returns (ConsumptionCheck memory check);

Parameters

Returns

_getLiquidationDebtCheck

Builds the liquidation debt-consumption check from actual debt-asset transfers.

Aave v3 Horizon clips liquidation debt to the user’s actual debt or the close-factor cap. The assertion therefore measures the actual debt asset moved from the liquidator to the debt reserve’s aToken during the successful liquidation call.

function _getLiquidationDebtCheck(
    OperationContext calldata operation,
    PhEvm.ForkId calldata beforeFork,
    PhEvm.ForkId calldata afterFork
) internal view returns (ConsumptionCheck memory check);

Parameters

Returns

_getLiquidationCollateralCheck

Builds the liquidation collateral-consumption check from actual collateral transfers.

This measures what the liquidator actually receives:

• underlying collateral when receiveAToken == false
• collateral aTokens when receiveAToken == true The bound is still capped by the user’s pre-call collateral claim.

function _getLiquidationCollateralCheck(
    OperationContext calldata operation,
    PhEvm.ForkId calldata beforeFork,
    PhEvm.ForkId calldata afterFork
) internal view returns (ConsumptionCheck memory check);

Parameters

Returns

_evaluateHealthFactor

Converts Aave v3 Horizon aggregate metrics into the common solvency representation.

This is the protocol-specific core of the invariant for Aave v3 Horizon: an account with debt is solvent iff healthFactor >= 1e18.

function _evaluateHealthFactor(AccountState memory state) internal pure returns (SolvencyState memory solvency);

Parameters

Returns

_buildAccountBalance

Builds a single reserve-level balance entry for the account.

Returns (false, ...) when the account has neither supplied balance nor variable debt in the reserve, allowing the caller to compact the final array. This example intentionally follows the local Horizon borrow surface, which only exposes variable-rate borrowing.

function _buildAccountBalance(
    address asset,
    address account,
    uint256 userConfigData,
    address oracle,
    PhEvm.ForkId memory fork
) internal view returns (bool include, AccountBalance memory balance);

Parameters

Returns

_getReserveData

Reads Aave v3 Horizon reserve metadata for a single asset at the requested snapshot fork.

function _getReserveData(address asset, PhEvm.ForkId memory fork)
    internal
    view
    returns (AaveV3Types.ReserveDataLegacy memory reserveData);

Parameters

Returns

_getUserReserveDebt

Reads the user’s total debt for one reserve from Aave v3 Horizon debt-token balances.

The example sums stable and variable debt token balances to make the liquidation bound robust across reserve configurations.

function _getUserReserveDebt(address asset, address account, PhEvm.ForkId memory fork)
    internal
    view
    returns (uint256 debtBalance);

Parameters

Returns

_readOptionalBalance

Reads a token balance when the token address may be unset.

Some deployments disable one debt-token flavor and leave the corresponding address at zero. This helper treats that case as a zero balance instead of reverting.

function _readOptionalBalance(address token, address account, PhEvm.ForkId memory fork)
    internal
    view
    returns (uint256 balance);

Parameters

Returns

_valueInBase

Converts an asset-denominated balance into Aave base currency.

Uses the Aave v3 Horizon oracle price and token decimals from the snapshot fork. This helper is suitable for example code and debugging, but suites with stricter precision requirements may want protocol-exact valuation logic.

function _valueInBase(address oracle, address asset, uint256 balance, PhEvm.ForkId memory fork)
    internal
    view
    returns (uint256);

Parameters

Returns

_isUsingAsCollateral

Returns whether the reserve is enabled as collateral in Aave v3 Horizon’s user config bitset.

Aave v3 Horizon stores collateral and borrow flags as packed bit pairs keyed by reserve id. This helper reads the collateral bit for the reserve.

function _isUsingAsCollateral(uint256 userConfigData, uint256 reserveId) internal pure returns (bool);

Parameters

Returns

_toInt256

Safely casts a uint256 metric to int256 for SolvencyState.

Solvency metrics use signed integers in the common interface to support protocols with negative liquidity margins. Aave v3 health factor is always non-negative, so values above int256.max are saturated instead of reverting.

function _toInt256(uint256 value) internal pure returns (int256);

Parameters

Returns

Structs

AaveAccountMetrics

Extra aggregate Aave v3 Horizon metrics kept in AccountState.metadata.

The common account shape does not have dedicated fields for these values, but they are useful for debugging and for reconstructing the health-factor-based solvency decision.

struct AaveAccountMetrics {
    uint256 availableBorrowsBase;
    uint256 currentLiquidationThreshold;
    uint256 ltv;
    uint256 healthFactor;
}