From d5ab91263728aad5eee9cf7dcedf403319383f47 Mon Sep 17 00:00:00 2001 From: makemake Date: Mon, 18 May 2026 14:50:03 +0200 Subject: [PATCH] Add protection suite assertion examples --- .../lending/ILendingProtectionSuite.sol | 9 +- .../lending/LendingBaseAssertion.sol | 24 +- .../lending/examples/AaveV3LikeHelpers.sol | 515 ++++++++++++++ .../lending/examples/AaveV3LikeInterfaces.sol | 90 +++ .../examples/AaveV3LikeOperationSafety.sol | 25 + .../examples/AaveV3PostOperationSolvency.sol | 638 +----------------- .../examples/SparkLendV1OperationSafety.sol | 37 + .../UniswapV4PoolManagerAssertion.sol | 243 +++++++ .../examples/UniswapV4PoolManagerHelpers.sol | 182 +++++ .../UniswapV4PoolManagerInterfaces.sol | 71 ++ src/protection/vault/ERC4626BaseAssertion.sol | 13 +- .../examples/MetaMorphoVaultAssertion.sol | 66 ++ .../lending/AaveV3LikeOperationSafety.t.sol | 200 ++++++ .../swaps/UniswapV4PoolManagerAssertion.t.sol | 127 ++++ 14 files changed, 1615 insertions(+), 625 deletions(-) create mode 100644 src/protection/lending/examples/AaveV3LikeHelpers.sol create mode 100644 src/protection/lending/examples/AaveV3LikeInterfaces.sol create mode 100644 src/protection/lending/examples/AaveV3LikeOperationSafety.sol create mode 100644 src/protection/lending/examples/SparkLendV1OperationSafety.sol create mode 100644 src/protection/swaps/examples/UniswapV4PoolManagerAssertion.sol create mode 100644 src/protection/swaps/examples/UniswapV4PoolManagerHelpers.sol create mode 100644 src/protection/swaps/examples/UniswapV4PoolManagerInterfaces.sol create mode 100644 src/protection/vault/examples/MetaMorphoVaultAssertion.sol create mode 100644 test/protection/lending/AaveV3LikeOperationSafety.t.sol create mode 100644 test/protection/swaps/UniswapV4PoolManagerAssertion.t.sol diff --git a/src/protection/lending/ILendingProtectionSuite.sol b/src/protection/lending/ILendingProtectionSuite.sol index 07fb490..e9ffe01 100644 --- a/src/protection/lending/ILendingProtectionSuite.sol +++ b/src/protection/lending/ILendingProtectionSuite.sol @@ -8,8 +8,8 @@ import {PhEvm} from "../../PhEvm.sol"; /// @notice Step-oriented interface for protocol-specific lending protection suites. /// @dev Implementations expose the protocol-specific plumbing needed to assert a shared family of /// lending-protocol invariants: -/// - any successful action that increases debt or reduces effective collateral must leave the -/// affected account solvent under the protocol's own risk metric +/// - any successful action that increases debt or reduces effective collateral must not move a +/// solvent account into insolvency under the protocol's own risk metric /// - successful withdrawals must not consume more claim than the account had before the call /// - successful liquidations must not consume more debt or collateral than existed before the call /// The bounded-consumption portion should be measured from the successful call's actual effect, @@ -24,7 +24,7 @@ import {PhEvm} from "../../PhEvm.sol"; /// `consumed <= availableBefore` for each returned check. /// 5. Filter to solvency-relevant operations with `shouldCheckPostOperationSolvency(...)`. /// 6. Read the account snapshot with `getAccountSnapshot(...)`. -/// 7. Require `snapshot.solvency.isSolvent == true`. +/// 7. Require that a solvent pre-call account remains solvent after the call. /// /// Different protocols can encode different solvency metrics while preserving the same invariant: /// - Aave-like systems can expose `metric = healthFactor`, `threshold = 1e18`, `comparison = Gte`. @@ -54,7 +54,8 @@ interface ILendingProtectionSuite { WithdrawCollateral, DisableCollateral, TransferCollateral, - Liquidation + Liquidation, + SetEMode } /// @notice Comparison rule for the protocol-defined solvency metric. diff --git a/src/protection/lending/LendingBaseAssertion.sol b/src/protection/lending/LendingBaseAssertion.sol index 1005dc8..a737dcb 100644 --- a/src/protection/lending/LendingBaseAssertion.sol +++ b/src/protection/lending/LendingBaseAssertion.sol @@ -3,6 +3,7 @@ pragma solidity ^0.8.13; import {Assertion} from "../../Assertion.sol"; import {PhEvm} from "../../PhEvm.sol"; +import {AssertionSpec} from "../../SpecRecorder.sol"; import {ForkUtils} from "../../utils/ForkUtils.sol"; import {ILendingProtectionSuite} from "./ILendingProtectionSuite.sol"; @@ -64,7 +65,7 @@ abstract contract LendingProtectionSuiteBase is ForkUtils, ILendingProtectionSui /// @dev Inherit this together with a concrete `ILendingProtectionSuite` implementation. The base /// contract handles one decode pass per triggered call, then enforces both: /// - any bounded-consumption checks returned by the suite -/// - post-operation solvency for risk-increasing operations +/// - healthy accounts are not made insolvent by risk-increasing operations abstract contract LendingBaseAssertion is Assertion { error LendingTriggeredCallNotFound(bytes4 selector, uint256 callStart); error LendingOperationAccountMissing(bytes4 selector); @@ -93,6 +94,10 @@ abstract contract LendingBaseAssertion is Assertion { /// @return suite The suite used to decode operations and evaluate solvency. function _suite() internal view virtual returns (ILendingProtectionSuite); + constructor() { + registerAssertionSpec(AssertionSpec.Reshiram); + } + /// @notice Registers one generic lending operation-safety check for every monitored selector. /// @dev This is the only trigger wiring most lending assertions need to implement. The suite /// decides which selectors matter through `getMonitoredSelectors()`, and this base maps all @@ -130,7 +135,7 @@ abstract contract LendingBaseAssertion is Assertion { PhEvm.ForkId memory afterFork = _postCall(triggered.callEnd); _assertConsumptionChecks(suite, triggered, operation, beforeFork, afterFork); - _assertPostOperationSolvency(suite, triggered, operation, afterFork); + _assertPostOperationSolvency(suite, triggered, operation, beforeFork, afterFork); } /// @notice Enforces the suite-provided bounded-consumption checks for the triggered operation. @@ -167,10 +172,10 @@ abstract contract LendingBaseAssertion is Assertion { } } - /// @notice Enforces post-operation solvency for risk-increasing operations. - /// @dev Operations that do not increase debt or reduce effective collateral are skipped. This is - /// the original shared lending invariant, now run as one stage of the broader - /// operation-safety pipeline. + /// @notice Enforces that risk-increasing operations do not newly make an account insolvent. + /// @dev Operations that do not increase debt or reduce effective collateral are skipped. Accounts + /// already insolvent before the call are also skipped so existing bad debt or liquidatable + /// positions do not cause false positives on unrelated account-management actions. /// @param suite The protocol-specific lending suite. /// @param triggered The exact adopter frame that caused the assertion to run. /// @param operation The decoded lending operation. @@ -179,6 +184,7 @@ abstract contract LendingBaseAssertion is Assertion { ILendingProtectionSuite suite, ILendingProtectionSuite.TriggeredCall memory triggered, ILendingProtectionSuite.OperationContext memory operation, + PhEvm.ForkId memory beforeFork, PhEvm.ForkId memory afterFork ) internal view { if (!suite.shouldCheckPostOperationSolvency(operation)) { @@ -189,6 +195,12 @@ abstract contract LendingBaseAssertion is Assertion { revert LendingOperationAccountMissing(triggered.selector); } + ILendingProtectionSuite.AccountSnapshot memory beforeSnapshot = + suite.getAccountSnapshot(operation.account, beforeFork); + if (!beforeSnapshot.solvency.isSolvent) { + return; + } + ILendingProtectionSuite.AccountSnapshot memory snapshot = suite.getAccountSnapshot(operation.account, afterFork); if (!snapshot.solvency.isSolvent) { diff --git a/src/protection/lending/examples/AaveV3LikeHelpers.sol b/src/protection/lending/examples/AaveV3LikeHelpers.sol new file mode 100644 index 0000000..11fb4c9 --- /dev/null +++ b/src/protection/lending/examples/AaveV3LikeHelpers.sol @@ -0,0 +1,515 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {PhEvm} from "../../../PhEvm.sol"; +import {ILendingProtectionSuite} from "../ILendingProtectionSuite.sol"; +import {LendingProtectionSuiteBase} from "../LendingBaseAssertion.sol"; +import { + AaveV3LikeTypes, + IAaveV3LikeAddressesProvider, + IAaveV3LikeOracle, + IAaveV3LikePool, + IERC20MetadataLike +} from "./AaveV3LikeInterfaces.sol"; + +/// @title AaveV3LikeProtectionSuite +/// @author Phylax Systems +/// @notice Shared `ILendingProtectionSuite` implementation for Aave v3-compatible lending forks. +/// @dev This adapter matches the interface and accounting model used by forks such as the local +/// Aave v3 Horizon deployment and SparkLend v1. +/// +/// The suite protects the lending surface that can directly worsen an account: +/// - new borrows and collateral withdrawals must leave the account above Aave's health-factor +/// liquidation threshold; +/// - disabling collateral, transferring aTokens, or changing e-mode must not turn a healthy +/// account into a liquidatable one; +/// - withdrawals and liquidations are bounded by the user's pre-call claim, debt, and collateral +/// so a locally successful call cannot consume more value than the pre-state allowed. +/// +/// These checks intentionally use the pool's own `getUserAccountData` output as the risk source +/// of truth. A failure means the transaction passed protocol execution but left external lending +/// accounting in a state users would experience as bad debt, over-withdrawal, or over-liquidation. +contract AaveV3LikeProtectionSuite is LendingProtectionSuiteBase { + /// @notice Extra aggregate Aave v3-like metrics kept in `AccountState.metadata`. + struct AaveAccountMetrics { + uint256 availableBorrowsBase; + uint256 currentLiquidationThreshold; + uint256 ltv; + uint256 healthFactor; + } + + bytes32 internal constant HEALTH_FACTOR_METRIC = 0x4845414c54485f464143544f5200000000000000000000000000000000000000; + bytes32 internal constant WITHDRAW_CLAIM_CHECK = "WITHDRAW_CLAIM"; + bytes32 internal constant LIQUIDATION_DEBT_CHECK = "LIQUIDATION_DEBT"; + bytes32 internal constant LIQUIDATION_COLLATERAL_CHECK = "LIQUIDATION_COLLATERAL"; + uint256 internal constant HEALTH_FACTOR_THRESHOLD = 1e18; + int256 internal constant HEALTH_FACTOR_THRESHOLD_INT = 1e18; + + address internal immutable POOL; + address internal immutable ADDRESSES_PROVIDER; + + /// @notice Creates an Aave v3-like suite bound to a specific pool. + /// @param pool_ Pool address whose accounting and selectors this suite targets. + /// @param addressesProvider_ The pool's `ADDRESSES_PROVIDER`. Passed in explicitly because + /// assertions are deployed against an empty state where calling the pool would fail. + constructor(address pool_, address addressesProvider_) { + POOL = pool_; + ADDRESSES_PROVIDER = addressesProvider_; + } + + /// @notice Returns the Aave v3-like pool selectors relevant to the shared lending invariants. + /// @dev The list is intentionally limited to operations that can change debt, effective + /// collateral, liquidation settlement, or the user's risk category. Supply, repay, and other + /// risk-improving paths are left out to keep the example focused and low noise. + function getMonitoredSelectors() external pure override returns (bytes4[] memory selectors) { + selectors = new bytes4[](6); + selectors[0] = IAaveV3LikePool.borrow.selector; + selectors[1] = IAaveV3LikePool.withdraw.selector; + selectors[2] = IAaveV3LikePool.liquidationCall.selector; + selectors[3] = IAaveV3LikePool.setUserUseReserveAsCollateral.selector; + selectors[4] = IAaveV3LikePool.finalizeTransfer.selector; + selectors[5] = IAaveV3LikePool.setUserEMode.selector; + } + + /// @notice Decodes an Aave v3-like pool call into the shared lending operation model. + /// @dev The generic lending base only needs a normalized operation: whose risk changed, which + /// asset moved, and whether the call increased debt or reduced effective collateral. Keeping + /// the Aave ABI details here lets the base assertion express protocol-agnostic safety rules. + function decodeOperation(TriggeredCall calldata triggered) + external + pure + override + returns (OperationContext memory operation) + { + operation.selector = triggered.selector; + operation.caller = triggered.caller; + + if (triggered.selector == IAaveV3LikePool.borrow.selector) { + (address asset, uint256 amount,,, address onBehalfOf) = + abi.decode(triggered.input[4:], (address, uint256, uint256, uint16, address)); + + operation.kind = OperationKind.Borrow; + operation.account = onBehalfOf; + operation.asset = asset; + operation.amount = amount; + operation.increasesDebt = amount != 0; + return operation; + } + + if (triggered.selector == IAaveV3LikePool.withdraw.selector) { + (address asset, uint256 amount, address to) = abi.decode(triggered.input[4:], (address, uint256, address)); + + operation.kind = OperationKind.WithdrawCollateral; + operation.account = triggered.caller; + operation.asset = asset; + operation.counterparty = to; + operation.amount = amount; + operation.reducesEffectiveCollateral = amount != 0; + return operation; + } + + if (triggered.selector == IAaveV3LikePool.liquidationCall.selector) { + (address collateralAsset, address debtAsset, address user, uint256 debtToCover, bool receiveAToken) = + abi.decode(triggered.input[4:], (address, address, address, uint256, bool)); + + operation.kind = OperationKind.Liquidation; + operation.account = user; + operation.asset = debtAsset; + operation.relatedAsset = collateralAsset; + operation.counterparty = triggered.caller; + operation.amount = debtToCover; + operation.metadata = abi.encode(receiveAToken); + return operation; + } + + if (triggered.selector == IAaveV3LikePool.setUserUseReserveAsCollateral.selector) { + (address asset, bool useAsCollateral) = abi.decode(triggered.input[4:], (address, bool)); + + if (!useAsCollateral) { + operation.kind = OperationKind.DisableCollateral; + operation.account = triggered.caller; + operation.asset = asset; + operation.reducesEffectiveCollateral = true; + } + + return operation; + } + + if (triggered.selector == IAaveV3LikePool.finalizeTransfer.selector) { + (address asset, address from, address to, uint256 amount,,) = + abi.decode(triggered.input[4:], (address, address, address, uint256, uint256, uint256)); + + operation.kind = OperationKind.TransferCollateral; + operation.account = from; + operation.asset = asset; + operation.counterparty = to; + operation.amount = amount; + operation.reducesEffectiveCollateral = from != to && amount != 0; + return operation; + } + + if (triggered.selector == IAaveV3LikePool.setUserEMode.selector) { + (uint8 categoryId) = abi.decode(triggered.input[4:], (uint8)); + + operation.kind = OperationKind.SetEMode; + operation.account = triggered.caller; + operation.amount = uint256(categoryId); + operation.metadata = abi.encode(categoryId); + return operation; + } + } + + /// @notice Filters decoded Aave v3-like operations down to the ones that must preserve solvency. + /// @dev A post-operation health-factor check is only meaningful for calls that can worsen the + /// account. This avoids tripping on harmless operations and makes each failure actionable: + /// a previously healthy account ended the triggering call below the liquidation threshold. + function shouldCheckPostOperationSolvency(OperationContext calldata operation) + external + pure + override + returns (bool shouldCheck) + { + return operation.account != address(0) + && (operation.increasesDebt + || operation.reducesEffectiveCollateral + || operation.kind == OperationKind.SetEMode); + } + + /// @notice Returns the bounded-consumption checks implied by the decoded Aave v3-like operation. + /// @dev Solvency alone does not catch value extraction bugs. These checks also assert that a + /// withdraw cannot return more assets than the caller's pre-call aToken claim, and that a + /// liquidation cannot repay/seize more debt or collateral than existed immediately before it. + function getConsumptionChecks( + TriggeredCall calldata triggered, + OperationContext calldata operation, + PhEvm.ForkId calldata beforeFork, + PhEvm.ForkId calldata afterFork + ) external view override returns (ConsumptionCheck[] memory checks) { + if (operation.kind == OperationKind.WithdrawCollateral) { + checks = new ConsumptionCheck[](1); + checks[0] = _getWithdrawClaimCheck(triggered, operation, beforeFork); + return checks; + } + + if (operation.kind == OperationKind.Liquidation) { + checks = new ConsumptionCheck[](2); + checks[0] = _getLiquidationDebtCheck(operation, beforeFork, afterFork); + checks[1] = _getLiquidationCollateralCheck(operation, beforeFork, afterFork); + } + } + + /// @notice Reads the post-call snapshot needed by the health-factor solvency invariant. + /// @dev The lending base calls this at precise pre-call and post-call forks. Using the same pool + /// aggregate view that integrators rely on makes the failure easy to interpret: the protocol's + /// own account data says the user is no longer solvent. + function getAccountSnapshot(address account, PhEvm.ForkId calldata fork) + external + view + virtual + override + returns (AccountSnapshot memory snapshot) + { + snapshot.state = _getAccountState(account, fork); + snapshot.solvency = _evaluateHealthFactor(snapshot.state); + } + + /// @notice Reads aggregate account metrics from `Pool.getUserAccountData(...)`. + function getAccountState(address account, PhEvm.ForkId calldata fork) + external + view + override + returns (AccountState memory state) + { + return _getAccountState(account, fork); + } + + /// @notice Enumerates reserve balances for the account. + function getAccountBalances(address account, PhEvm.ForkId calldata fork) + external + view + override + returns (AccountBalance[] memory balances) + { + return _getAccountBalances(account, fork); + } + + /// @notice Evaluates solvency from aggregate account state. + function evaluateSolvency( + AccountState calldata state, + AccountBalance[] calldata balances, + PhEvm.ForkId calldata fork + ) external pure override returns (SolvencyState memory solvency) { + balances; + fork; + return _evaluateHealthFactor(state); + } + + /// @notice Internal helper that reads and normalizes aggregate account data. + function _getAccountState(address account, PhEvm.ForkId memory fork) + internal + view + returns (AccountState memory state) + { + ( + uint256 totalCollateralBase, + uint256 totalDebtBase, + uint256 availableBorrowsBase, + uint256 currentLiquidationThreshold, + uint256 ltv, + uint256 healthFactor + ) = abi.decode( + _viewAt(POOL, abi.encodeCall(IAaveV3LikePool.getUserAccountData, (account)), fork), + (uint256, uint256, uint256, uint256, uint256, uint256) + ); + + state.account = account; + state.totalCollateralValue = totalCollateralBase; + state.totalDebtValue = totalDebtBase; + state.hasDebt = totalDebtBase != 0; + state.metadata = abi.encode( + AaveAccountMetrics({ + availableBorrowsBase: availableBorrowsBase, + currentLiquidationThreshold: currentLiquidationThreshold, + ltv: ltv, + healthFactor: healthFactor + }) + ); + } + + /// @notice Internal helper that expands the account into reserve-level balances and values. + function _getAccountBalances(address account, PhEvm.ForkId memory fork) + internal + view + returns (AccountBalance[] memory balances) + { + address[] memory reserves = + abi.decode(_viewAt(POOL, abi.encodeCall(IAaveV3LikePool.getReservesList, ()), fork), (address[])); + AaveV3LikeTypes.UserConfigurationMap memory userConfig = abi.decode( + _viewAt(POOL, abi.encodeCall(IAaveV3LikePool.getUserConfiguration, (account)), fork), + (AaveV3LikeTypes.UserConfigurationMap) + ); + + address oracle = + _readAddressAt(ADDRESSES_PROVIDER, abi.encodeCall(IAaveV3LikeAddressesProvider.getPriceOracle, ()), fork); + + balances = new AccountBalance[](reserves.length); + uint256 count; + + for (uint256 i; i < reserves.length; ++i) { + (bool include, AccountBalance memory balance) = + _buildAccountBalance(reserves[i], account, userConfig.data, oracle, fork); + + if (!include) { + continue; + } + + balances[count++] = balance; + } + + assembly { + mstore(balances, count) + } + } + + /// @notice Builds the withdraw bounded-consumption check from call output and pre-state. + /// @dev `withdraw` returns the actual asset amount sent. Comparing that return value with the + /// caller's pre-call aToken balance catches accounting bugs where a successful withdrawal + /// consumes more collateral claim than the account had before the call. + function _getWithdrawClaimCheck( + TriggeredCall calldata triggered, + OperationContext calldata operation, + PhEvm.ForkId calldata beforeFork + ) internal view returns (ConsumptionCheck memory check) { + AaveV3LikeTypes.ReserveData memory reserveData = _getReserveData(operation.asset, beforeFork); + uint256 availableBefore = _readBalanceAt(reserveData.aTokenAddress, operation.account, beforeFork); + uint256 consumed = abi.decode(ph.callOutputAt(triggered.callStart), (uint256)); + + check = ConsumptionCheck({ + checkName: WITHDRAW_CLAIM_CHECK, + account: operation.account, + asset: operation.asset, + availableBefore: availableBefore, + consumed: consumed, + metadata: abi.encode(reserveData.aTokenAddress) + }); + } + + /// @notice Builds the liquidation debt-consumption check from actual debt-asset transfers. + /// @dev The liquidation input can request `type(uint256).max`, so the assertion observes the + /// actual debt-asset transfer instead of trusting calldata. A failure means the liquidator + /// repaid more debt than the borrower owed in the pre-call snapshot. + function _getLiquidationDebtCheck( + OperationContext calldata operation, + PhEvm.ForkId calldata beforeFork, + PhEvm.ForkId calldata afterFork + ) internal view returns (ConsumptionCheck memory check) { + AaveV3LikeTypes.ReserveData memory reserveData = _getReserveData(operation.asset, beforeFork); + uint256 debtBefore = _getUserReserveDebt(operation.asset, operation.account, beforeFork); + uint256 repaidEffective = _transferredValueDuringCall( + operation.asset, operation.counterparty, reserveData.aTokenAddress, beforeFork, afterFork + ); + + check = ConsumptionCheck({ + checkName: LIQUIDATION_DEBT_CHECK, + account: operation.account, + asset: operation.asset, + availableBefore: debtBefore, + consumed: repaidEffective, + metadata: abi.encode(reserveData.aTokenAddress, operation.counterparty) + }); + } + + /// @notice Builds the liquidation collateral-consumption check from actual collateral transfers. + /// @dev The seized side differs depending on `receiveAToken`: liquidators can receive aTokens or + /// underlying collateral. The check observes the token that actually moved and bounds it by + /// the borrower's pre-call collateral claim, protecting users from over-seizure. + function _getLiquidationCollateralCheck( + OperationContext calldata operation, + PhEvm.ForkId calldata beforeFork, + PhEvm.ForkId calldata afterFork + ) internal view returns (ConsumptionCheck memory check) { + bool receiveAToken = abi.decode(operation.metadata, (bool)); + AaveV3LikeTypes.ReserveData memory reserveData = _getReserveData(operation.relatedAsset, beforeFork); + uint256 collateralBefore = _readBalanceAt(reserveData.aTokenAddress, operation.account, beforeFork); + address seizedToken = receiveAToken ? reserveData.aTokenAddress : operation.relatedAsset; + address transferSender = receiveAToken ? operation.account : reserveData.aTokenAddress; + uint256 seizedEffective = + _transferredValueDuringCall(seizedToken, transferSender, operation.counterparty, beforeFork, afterFork); + + check = ConsumptionCheck({ + checkName: LIQUIDATION_COLLATERAL_CHECK, + account: operation.account, + asset: operation.relatedAsset, + availableBefore: collateralBefore, + consumed: seizedEffective, + metadata: abi.encode(reserveData.aTokenAddress, seizedToken, transferSender, receiveAToken) + }); + } + + /// @notice Reads token movement for only the triggered call window. + /// @dev ERC20 transfer precompiles return cumulative logs up to the requested fork, so subtract + /// the pre-call amount from the post-call amount to avoid counting earlier same-tx transfers. + function _transferredValueDuringCall( + address token, + address from, + address to, + PhEvm.ForkId calldata beforeFork, + PhEvm.ForkId calldata afterFork + ) internal view returns (uint256 value) { + uint256 beforeValue = _transferredValueAt(token, from, to, beforeFork); + uint256 afterValue = _transferredValueAt(token, from, to, afterFork); + + return afterValue > beforeValue ? afterValue - beforeValue : 0; + } + + /// @notice Converts aggregate metrics into the common solvency representation. + function _evaluateHealthFactor(AccountState memory state) internal pure returns (SolvencyState memory solvency) { + AaveAccountMetrics memory metrics = abi.decode(state.metadata, (AaveAccountMetrics)); + + solvency.isSolvent = !state.hasDebt || metrics.healthFactor >= HEALTH_FACTOR_THRESHOLD; + solvency.isLiquidatable = state.hasDebt && metrics.healthFactor < HEALTH_FACTOR_THRESHOLD; + solvency.metricName = HEALTH_FACTOR_METRIC; + solvency.metric = _toInt256(metrics.healthFactor); + solvency.threshold = HEALTH_FACTOR_THRESHOLD_INT; + solvency.comparison = ComparisonKind.Gte; + solvency.metadata = abi.encode(metrics.availableBorrowsBase, metrics.currentLiquidationThreshold, metrics.ltv); + } + + /// @notice Builds a single reserve-level balance entry for the account. + function _buildAccountBalance( + address asset, + address account, + uint256 userConfigData, + address oracle, + PhEvm.ForkId memory fork + ) internal view returns (bool include, AccountBalance memory balance) { + AaveV3LikeTypes.ReserveData memory reserveData = abi.decode( + _viewAt(POOL, abi.encodeCall(IAaveV3LikePool.getReserveData, (asset)), fork), (AaveV3LikeTypes.ReserveData) + ); + + uint256 collateralBalance = + _readUintAt(reserveData.aTokenAddress, abi.encodeCall(IERC20MetadataLike.balanceOf, (account)), fork); + uint256 debtBalance = _readUintAt( + reserveData.variableDebtTokenAddress, abi.encodeCall(IERC20MetadataLike.balanceOf, (account)), fork + ); + + if (collateralBalance == 0 && debtBalance == 0) { + return (false, balance); + } + + bool countsAsCollateral = collateralBalance != 0 && _isUsingAsCollateral(userConfigData, reserveData.id); + + balance = AccountBalance({ + asset: asset, + collateralBalance: collateralBalance, + debtBalance: debtBalance, + collateralValue: countsAsCollateral ? _valueInBase(oracle, asset, collateralBalance, fork) : 0, + debtValue: debtBalance == 0 ? 0 : _valueInBase(oracle, asset, debtBalance, fork), + countsAsCollateral: countsAsCollateral, + metadata: abi.encode(reserveData.id) + }); + + return (true, balance); + } + + /// @notice Reads reserve metadata for a single asset at the requested snapshot fork. + function _getReserveData(address asset, PhEvm.ForkId memory fork) + internal + view + returns (AaveV3LikeTypes.ReserveData memory reserveData) + { + reserveData = abi.decode( + _viewAt(POOL, abi.encodeCall(IAaveV3LikePool.getReserveData, (asset)), fork), (AaveV3LikeTypes.ReserveData) + ); + } + + /// @notice Reads the user's total debt for one reserve from the debt-token balances. + function _getUserReserveDebt(address asset, address account, PhEvm.ForkId memory fork) + internal + view + returns (uint256 debtBalance) + { + AaveV3LikeTypes.ReserveData memory reserveData = _getReserveData(asset, fork); + debtBalance = _readOptionalBalance(reserveData.stableDebtTokenAddress, account, fork) + + _readOptionalBalance(reserveData.variableDebtTokenAddress, account, fork); + } + + /// @notice Reads a token balance when the token address may be unset. + function _readOptionalBalance(address token, address account, PhEvm.ForkId memory fork) + internal + view + returns (uint256 balance) + { + if (token == address(0)) { + return 0; + } + + return _readBalanceAt(token, account, fork); + } + + /// @notice Converts an asset-denominated balance into the pool base currency. + function _valueInBase(address oracle, address asset, uint256 balance, PhEvm.ForkId memory fork) + internal + view + returns (uint256) + { + uint256 price = _readUintAt(oracle, abi.encodeCall(IAaveV3LikeOracle.getAssetPrice, (asset)), fork); + uint8 decimals = _readUint8At(asset, abi.encodeCall(IERC20MetadataLike.decimals, ()), fork); + return ph.mulDivDown(balance, price, 10 ** uint256(decimals)); + } + + /// @notice Returns whether the reserve is enabled as collateral in the user config bitset. + function _isUsingAsCollateral(uint256 userConfigData, uint256 reserveId) internal pure returns (bool) { + return ((userConfigData >> (reserveId * 2)) & 1) != 0; + } + + /// @notice Safely casts a `uint256` metric to `int256` for `SolvencyState`. + function _toInt256(uint256 value) internal pure returns (int256) { + if (value > uint256(type(int256).max)) { + return type(int256).max; + } + + // forge-lint: disable-next-line(unsafe-typecast) + return int256(value); + } +} diff --git a/src/protection/lending/examples/AaveV3LikeInterfaces.sol b/src/protection/lending/examples/AaveV3LikeInterfaces.sol new file mode 100644 index 0000000..4b6c61d --- /dev/null +++ b/src/protection/lending/examples/AaveV3LikeInterfaces.sol @@ -0,0 +1,90 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/// @notice Minimal ERC20 metadata surface used by the Aave v3-like lending examples. +interface IERC20MetadataLike { + function balanceOf(address account) external view returns (uint256); + function decimals() external view returns (uint8); +} + +/// @notice Minimal reserve and user structs shared by Aave v3-like pool forks. +library AaveV3LikeTypes { + struct UserConfigurationMap { + uint256 data; + } + + struct ReserveData { + uint256 configurationData; + uint128 liquidityIndex; + uint128 currentLiquidityRate; + uint128 variableBorrowIndex; + uint128 currentVariableBorrowRate; + uint128 currentStableBorrowRate; + uint40 lastUpdateTimestamp; + uint16 id; + address aTokenAddress; + address stableDebtTokenAddress; + address variableDebtTokenAddress; + address interestRateStrategyAddress; + uint128 accruedToTreasury; + uint128 unbacked; + uint128 isolationModeTotalDebt; + } +} + +/// @notice Minimal pool surface shared by Aave v3-compatible lending markets. +interface IAaveV3LikePool { + function borrow(address asset, uint256 amount, uint256 interestRateMode, uint16 referralCode, address onBehalfOf) + external; + + function withdraw(address asset, uint256 amount, address to) external returns (uint256); + + function liquidationCall( + address collateralAsset, + address debtAsset, + address user, + uint256 debtToCover, + bool receiveAToken + ) external; + + function setUserUseReserveAsCollateral(address asset, bool useAsCollateral) external; + + function setUserEMode(uint8 categoryId) external; + + function finalizeTransfer( + address asset, + address from, + address to, + uint256 amount, + uint256 balanceFromBefore, + uint256 balanceToBefore + ) external; + + function getUserAccountData(address user) + external + view + returns ( + uint256 totalCollateralBase, + uint256 totalDebtBase, + uint256 availableBorrowsBase, + uint256 currentLiquidationThreshold, + uint256 ltv, + uint256 healthFactor + ); + + function getUserConfiguration(address user) external view returns (AaveV3LikeTypes.UserConfigurationMap memory); + + function getReserveData(address asset) external view returns (AaveV3LikeTypes.ReserveData memory); + + function getReservesList() external view returns (address[] memory); + + function ADDRESSES_PROVIDER() external view returns (address); +} + +interface IAaveV3LikeAddressesProvider { + function getPriceOracle() external view returns (address); +} + +interface IAaveV3LikeOracle { + function getAssetPrice(address asset) external view returns (uint256); +} diff --git a/src/protection/lending/examples/AaveV3LikeOperationSafety.sol b/src/protection/lending/examples/AaveV3LikeOperationSafety.sol new file mode 100644 index 0000000..4748517 --- /dev/null +++ b/src/protection/lending/examples/AaveV3LikeOperationSafety.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {ILendingProtectionSuite} from "../ILendingProtectionSuite.sol"; +import {LendingBaseAssertion} from "../LendingBaseAssertion.sol"; + +/// @title AaveV3LikeOperationSafetyAssertionBase +/// @author Phylax Systems +/// @notice Shared assertion wrapper for Aave v3-like lending suites. +/// @dev The assertion holds the suite as an immutable reference rather than inheriting its bytecode. +/// Concrete bundles construct the protocol-specific suite in their own constructor and pass it +/// in. Keeping the suite in a separate contract preserves the single-`createData` deployment UX +/// while keeping the assertion runtime well below the EIP-170 size limit enforced by CI. +abstract contract AaveV3LikeOperationSafetyAssertionBase is LendingBaseAssertion { + /// @notice Protocol-specific suite deployed alongside the assertion bundle. + ILendingProtectionSuite internal immutable SUITE; + + constructor(ILendingProtectionSuite suite_) { + SUITE = suite_; + } + + function _suite() internal view override returns (ILendingProtectionSuite) { + return SUITE; + } +} diff --git a/src/protection/lending/examples/AaveV3PostOperationSolvency.sol b/src/protection/lending/examples/AaveV3PostOperationSolvency.sol index e7a1ed4..3c5a2b1 100644 --- a/src/protection/lending/examples/AaveV3PostOperationSolvency.sol +++ b/src/protection/lending/examples/AaveV3PostOperationSolvency.sol @@ -1,644 +1,60 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.13; -import {PhEvm} from "../../../PhEvm.sol"; import {ILendingProtectionSuite} from "../ILendingProtectionSuite.sol"; -import {LendingBaseAssertion, LendingProtectionSuiteBase} from "../LendingBaseAssertion.sol"; -import { - AaveV3Types, - IAaveV3AddressesProviderLike, - IAaveV3OracleLike, - IAaveV3PoolLike, - IERC20MetadataLike -} from "./AaveV3Interfaces.sol"; +import {AaveV3LikeProtectionSuite} from "./AaveV3LikeHelpers.sol"; +import {AaveV3LikeOperationSafetyAssertionBase} from "./AaveV3LikeOperationSafety.sol"; /// @title AaveV3HorizonProtectionSuite /// @author Phylax Systems /// @notice Example `ILendingProtectionSuite` targeting a local Aave v3 Horizon deployment. -/// @dev 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. -contract AaveV3HorizonProtectionSuite is LendingProtectionSuiteBase { - /// @notice Extra aggregate Aave v3 Horizon metrics kept in `AccountState.metadata`. - /// @dev 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; - } - - bytes32 internal constant HEALTH_FACTOR_METRIC = 0x4845414c54485f464143544f5200000000000000000000000000000000000000; - bytes32 internal constant WITHDRAW_CLAIM_CHECK = "WITHDRAW_CLAIM"; - bytes32 internal constant LIQUIDATION_DEBT_CHECK = "LIQUIDATION_DEBT"; - bytes32 internal constant LIQUIDATION_COLLATERAL_CHECK = "LIQUIDATION_COLLATERAL"; - uint256 internal constant HEALTH_FACTOR_THRESHOLD = 1e18; - int256 internal constant HEALTH_FACTOR_THRESHOLD_INT = 1e18; - - address internal immutable POOL; - address internal immutable ADDRESSES_PROVIDER; - - /// @notice Creates an Aave v3 Horizon suite bound to a specific pool. - /// @dev The assertion adopter should also be this pool, since the monitored selectors are all - /// pool entrypoints or pool callbacks. - /// @param pool_ Aave v3 Horizon pool address whose accounting and selectors this suite targets. - constructor(address pool_) { - POOL = pool_; - ADDRESSES_PROVIDER = IAaveV3PoolLike(pool_).ADDRESSES_PROVIDER(); - } - - /// @notice Returns the Aave v3 Horizon pool selectors relevant to the shared lending invariants. - /// @dev 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. - /// @return selectors Pool selectors that should trigger the generic lending operation-safety check. - function getMonitoredSelectors() external pure override returns (bytes4[] memory selectors) { - selectors = new bytes4[](5); - selectors[0] = IAaveV3PoolLike.borrow.selector; - selectors[1] = IAaveV3PoolLike.withdraw.selector; - selectors[2] = IAaveV3PoolLike.liquidationCall.selector; - selectors[3] = IAaveV3PoolLike.setUserUseReserveAsCollateral.selector; - selectors[4] = IAaveV3PoolLike.finalizeTransfer.selector; - } - - /// @notice Decodes an Aave v3 Horizon pool call into the shared lending operation model. - /// @dev 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(...)`. - /// @param triggered The exact Aave v3 Horizon pool frame that caused the assertion to run. - /// @return operation Protocol-normalized description of the triggered action. - function decodeOperation(TriggeredCall calldata triggered) - external - pure - override - returns (OperationContext memory operation) - { - operation.selector = triggered.selector; - operation.caller = triggered.caller; - - if (triggered.selector == IAaveV3PoolLike.borrow.selector) { - (address asset, uint256 amount,,, address onBehalfOf) = - abi.decode(triggered.input[4:], (address, uint256, uint256, uint16, address)); - - operation.kind = OperationKind.Borrow; - operation.account = onBehalfOf; - operation.asset = asset; - operation.amount = amount; - operation.increasesDebt = amount != 0; - return operation; - } - - if (triggered.selector == IAaveV3PoolLike.withdraw.selector) { - (address asset, uint256 amount, address to) = abi.decode(triggered.input[4:], (address, uint256, address)); - - operation.kind = OperationKind.WithdrawCollateral; - operation.account = triggered.caller; - operation.asset = asset; - operation.counterparty = to; - operation.amount = amount; - operation.reducesEffectiveCollateral = amount != 0; - return operation; - } - - if (triggered.selector == IAaveV3PoolLike.liquidationCall.selector) { - (address collateralAsset, address debtAsset, address user, uint256 debtToCover, bool receiveAToken) = - abi.decode(triggered.input[4:], (address, address, address, uint256, bool)); - - operation.kind = OperationKind.Liquidation; - operation.account = user; - operation.asset = debtAsset; - operation.relatedAsset = collateralAsset; - operation.counterparty = triggered.caller; - operation.amount = debtToCover; - operation.metadata = abi.encode(receiveAToken); - return operation; - } - - if (triggered.selector == IAaveV3PoolLike.setUserUseReserveAsCollateral.selector) { - (address asset, bool useAsCollateral) = abi.decode(triggered.input[4:], (address, bool)); - - if (!useAsCollateral) { - operation.kind = OperationKind.DisableCollateral; - operation.account = triggered.caller; - operation.asset = asset; - operation.reducesEffectiveCollateral = true; - } - - return operation; - } - - if (triggered.selector == IAaveV3PoolLike.finalizeTransfer.selector) { - (address asset, address from, address to, uint256 amount,,) = - abi.decode(triggered.input[4:], (address, address, address, uint256, uint256, uint256)); - - operation.kind = OperationKind.TransferCollateral; - operation.account = from; - operation.asset = asset; - operation.counterparty = to; - operation.amount = amount; - operation.reducesEffectiveCollateral = from != to && amount != 0; - return operation; - } - } - - /// @notice Filters decoded Aave v3 Horizon operations down to the ones that must preserve solvency. - /// @dev 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. - /// @param operation The decoded operation context. - /// @return shouldCheck True when the generic assertion should read post-call state. - function shouldCheckPostOperationSolvency(OperationContext calldata operation) - external - pure - override - returns (bool shouldCheck) - { - return operation.account != address(0) && (operation.increasesDebt || operation.reducesEffectiveCollateral); - } - - /// @notice Returns the bounded-consumption checks implied by the decoded Aave v3 Horizon operation. - /// @dev 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. - /// @param triggered The exact Aave v3 Horizon pool frame that caused the assertion to run. - /// @param operation The decoded operation context. - /// @param beforeFork The pre-call snapshot fork. - /// @param afterFork The post-call snapshot fork. - /// @return checks Operation-specific bounded-consumption checks for the successful call. - function getConsumptionChecks( - TriggeredCall calldata triggered, - OperationContext calldata operation, - PhEvm.ForkId calldata beforeFork, - PhEvm.ForkId calldata afterFork - ) external view override returns (ConsumptionCheck[] memory checks) { - if (operation.kind == OperationKind.WithdrawCollateral) { - checks = new ConsumptionCheck[](1); - checks[0] = _getWithdrawClaimCheck(triggered, operation, beforeFork); - return checks; - } - - if (operation.kind == OperationKind.Liquidation) { - checks = new ConsumptionCheck[](2); - checks[0] = _getLiquidationDebtCheck(operation, beforeFork, afterFork); - checks[1] = _getLiquidationCollateralCheck(operation, beforeFork, afterFork); - } - } - - /// @notice Reads the post-call account snapshot needed by the Aave v3 Horizon solvency invariant. - /// @dev 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. - /// @param account The account whose health factor should be checked. - /// @param fork The post-call snapshot fork. - /// @return snapshot Snapshot containing aggregate state and the derived health-factor decision. - function getAccountSnapshot(address account, PhEvm.ForkId calldata fork) - external - view - virtual - override - returns (AccountSnapshot memory snapshot) - { - snapshot.state = _getAccountState(account, fork); - snapshot.solvency = _evaluateHealthFactor(snapshot.state); - } - - /// @notice Reads Aave v3 Horizon aggregate account metrics from `Pool.getUserAccountData(...)`. - /// @dev The returned `AccountState` uses Aave's base-currency values for total collateral and - /// total debt, and stores the additional health-factor inputs in `metadata`. - /// @param account The account whose aggregate risk data should be queried. - /// @param fork The snapshot fork to query. - /// @return state Aggregate Aave v3 Horizon account state. - function getAccountState(address account, PhEvm.ForkId calldata fork) - external - view - override - returns (AccountState memory state) - { - return _getAccountState(account, fork); - } - - /// @notice Enumerates Aave v3 reserve balances for the account. - /// @dev 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. - /// @param account The account whose reserve balances should be queried. - /// @param fork The snapshot fork to query. - /// @return balances One entry per non-zero reserve position. - function getAccountBalances(address account, PhEvm.ForkId calldata fork) - external - view - override - returns (AccountBalance[] memory balances) - { - return _getAccountBalances(account, fork); - } - - /// @notice Evaluates Aave v3 Horizon solvency from aggregate account state. - /// @dev 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. - /// @param state Aggregate account state produced by `getAccountState(...)`. - /// @param balances The per-reserve balances, unused in this implementation. - /// @param fork The snapshot fork, unused because all required information is in `state`. - /// @return solvency Health-factor-based solvency result. - function evaluateSolvency( - AccountState calldata state, - AccountBalance[] calldata balances, - PhEvm.ForkId calldata fork - ) external pure override returns (SolvencyState memory solvency) { - balances; - fork; - return _evaluateHealthFactor(state); - } - - /// @notice Internal helper that reads and normalizes Aave v3 Horizon aggregate account data. - /// @dev This is the canonical aggregate-state implementation used by both `getAccountState(...)` - /// and the optimized `getAccountSnapshot(...)` hot path. - /// @param account The account whose risk data should be queried. - /// @param fork The snapshot fork to query. - /// @return state Aggregate state encoded in the common suite format. - function _getAccountState(address account, PhEvm.ForkId memory fork) - internal - view - returns (AccountState memory state) - { - ( - uint256 totalCollateralBase, - uint256 totalDebtBase, - uint256 availableBorrowsBase, - uint256 currentLiquidationThreshold, - uint256 ltv, - uint256 healthFactor - ) = abi.decode( - _viewAt(POOL, abi.encodeCall(IAaveV3PoolLike.getUserAccountData, (account)), fork), - (uint256, uint256, uint256, uint256, uint256, uint256) - ); - - state.account = account; - state.totalCollateralValue = totalCollateralBase; - state.totalDebtValue = totalDebtBase; - state.hasDebt = totalDebtBase != 0; - state.metadata = abi.encode( - AaveAccountMetrics({ - availableBorrowsBase: availableBorrowsBase, - currentLiquidationThreshold: currentLiquidationThreshold, - ltv: ltv, - healthFactor: healthFactor - }) - ); - } - - /// @notice Internal helper that expands the account into reserve-level balances and values. - /// @dev 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. - /// @param account The account whose reserve positions should be queried. - /// @param fork The snapshot fork to query. - /// @return balances One entry per non-zero reserve position. - function _getAccountBalances(address account, PhEvm.ForkId memory fork) - internal - view - returns (AccountBalance[] memory balances) - { - address[] memory reserves = - abi.decode(_viewAt(POOL, abi.encodeCall(IAaveV3PoolLike.getReservesList, ()), fork), (address[])); - AaveV3Types.UserConfigurationMap memory userConfig = abi.decode( - _viewAt(POOL, abi.encodeCall(IAaveV3PoolLike.getUserConfiguration, (account)), fork), - (AaveV3Types.UserConfigurationMap) - ); - - address oracle = - _readAddressAt(ADDRESSES_PROVIDER, abi.encodeCall(IAaveV3AddressesProviderLike.getPriceOracle, ()), fork); - - balances = new AccountBalance[](reserves.length); - uint256 count; - - for (uint256 i; i < reserves.length; ++i) { - (bool include, AccountBalance memory balance) = - _buildAccountBalance(reserves[i], account, userConfig.data, oracle, fork); - - if (!include) { - continue; - } - - balances[count++] = balance; - } - - assembly { - mstore(balances, count) - } - } - - /// @notice Builds the withdraw bounded-consumption check from Aave v3 Horizon call output and pre-state. - /// @dev `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. - /// @param triggered The traced withdraw call. - /// @param operation The decoded withdraw operation. - /// @param beforeFork The pre-call snapshot fork. - /// @return check Bound requiring actual withdrawn amount to be no greater than pre-call supply. - function _getWithdrawClaimCheck( - TriggeredCall calldata triggered, - OperationContext calldata operation, - PhEvm.ForkId calldata beforeFork - ) internal view returns (ConsumptionCheck memory check) { - AaveV3Types.ReserveDataLegacy memory reserveData = _getReserveData(operation.asset, beforeFork); - uint256 availableBefore = _readBalanceAt(reserveData.aTokenAddress, operation.account, beforeFork); - uint256 consumed = abi.decode(ph.callOutputAt(triggered.callStart), (uint256)); - - check = ConsumptionCheck({ - checkName: WITHDRAW_CLAIM_CHECK, - account: operation.account, - asset: operation.asset, - availableBefore: availableBefore, - consumed: consumed, - metadata: abi.encode(reserveData.aTokenAddress) - }); - } - - /// @notice Builds the liquidation debt-consumption check from actual debt-asset transfers. - /// @dev 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. - /// @param operation The decoded liquidation operation. - /// @param beforeFork The pre-call snapshot fork. - /// @param afterFork The post-call snapshot fork. - /// @return check Bound requiring repaid debt to be no greater than pre-call debt. - function _getLiquidationDebtCheck( - OperationContext calldata operation, - PhEvm.ForkId calldata beforeFork, - PhEvm.ForkId calldata afterFork - ) internal view returns (ConsumptionCheck memory check) { - AaveV3Types.ReserveDataLegacy memory reserveData = _getReserveData(operation.asset, beforeFork); - uint256 debtBefore = _getUserReserveDebt(operation.asset, operation.account, beforeFork); - uint256 repaidEffective = - _transferredValueAt(operation.asset, operation.counterparty, reserveData.aTokenAddress, afterFork); - - check = ConsumptionCheck({ - checkName: LIQUIDATION_DEBT_CHECK, - account: operation.account, - asset: operation.asset, - availableBefore: debtBefore, - consumed: repaidEffective, - metadata: abi.encode(reserveData.aTokenAddress, operation.counterparty) - }); - } - - /// @notice Builds the liquidation collateral-consumption check from actual collateral transfers. - /// @dev 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. - /// @param operation The decoded liquidation operation. - /// @param beforeFork The pre-call snapshot fork. - /// @param afterFork The post-call snapshot fork. - /// @return check Bound requiring seized collateral to be no greater than pre-call collateral. - function _getLiquidationCollateralCheck( - OperationContext calldata operation, - PhEvm.ForkId calldata beforeFork, - PhEvm.ForkId calldata afterFork - ) internal view returns (ConsumptionCheck memory check) { - bool receiveAToken = abi.decode(operation.metadata, (bool)); - AaveV3Types.ReserveDataLegacy memory reserveData = _getReserveData(operation.relatedAsset, beforeFork); - uint256 collateralBefore = _readBalanceAt(reserveData.aTokenAddress, operation.account, beforeFork); - address seizedToken = receiveAToken ? reserveData.aTokenAddress : operation.relatedAsset; - address transferSender = receiveAToken ? operation.account : reserveData.aTokenAddress; - uint256 seizedEffective = _transferredValueAt(seizedToken, transferSender, operation.counterparty, afterFork); - - check = ConsumptionCheck({ - checkName: LIQUIDATION_COLLATERAL_CHECK, - account: operation.account, - asset: operation.relatedAsset, - availableBefore: collateralBefore, - consumed: seizedEffective, - metadata: abi.encode(reserveData.aTokenAddress, seizedToken, transferSender, receiveAToken) - }); - } - - /// @notice Converts Aave v3 Horizon aggregate metrics into the common solvency representation. - /// @dev This is the protocol-specific core of the invariant for Aave v3 Horizon: an account with debt is - /// solvent iff `healthFactor >= 1e18`. - /// @param state Aggregate Aave v3 account state whose metadata contains health-factor inputs. - /// @return solvency Common solvency output expressed in terms of health factor. - function _evaluateHealthFactor(AccountState memory state) internal pure returns (SolvencyState memory solvency) { - AaveAccountMetrics memory metrics = abi.decode(state.metadata, (AaveAccountMetrics)); - - solvency.isSolvent = !state.hasDebt || metrics.healthFactor >= HEALTH_FACTOR_THRESHOLD; - solvency.isLiquidatable = state.hasDebt && metrics.healthFactor < HEALTH_FACTOR_THRESHOLD; - solvency.metricName = HEALTH_FACTOR_METRIC; - solvency.metric = _toInt256(metrics.healthFactor); - solvency.threshold = HEALTH_FACTOR_THRESHOLD_INT; - solvency.comparison = ComparisonKind.Gte; - solvency.metadata = abi.encode(metrics.availableBorrowsBase, metrics.currentLiquidationThreshold, metrics.ltv); - } - - /// @notice Builds a single reserve-level balance entry for the account. - /// @dev 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. - /// @param asset The reserve asset being inspected. - /// @param account The account whose reserve position should be read. - /// @param userConfigData Aave v3 user-configuration bitset used to determine collateral usage. - /// @param oracle Price oracle used to value the reserve balances. - /// @param fork The snapshot fork to query. - /// @return include Whether the resulting balance entry should be kept. - /// @return balance Normalized reserve-level balance information. - function _buildAccountBalance( - address asset, - address account, - uint256 userConfigData, - address oracle, - PhEvm.ForkId memory fork - ) internal view returns (bool include, AccountBalance memory balance) { - AaveV3Types.ReserveDataLegacy memory reserveData = abi.decode( - _viewAt(POOL, abi.encodeCall(IAaveV3PoolLike.getReserveData, (asset)), fork), - (AaveV3Types.ReserveDataLegacy) - ); - - uint256 collateralBalance = - _readUintAt(reserveData.aTokenAddress, abi.encodeCall(IERC20MetadataLike.balanceOf, (account)), fork); - uint256 debtBalance = _readUintAt( - reserveData.variableDebtTokenAddress, abi.encodeCall(IERC20MetadataLike.balanceOf, (account)), fork - ); - - if (collateralBalance == 0 && debtBalance == 0) { - return (false, balance); - } - - bool countsAsCollateral = collateralBalance != 0 && _isUsingAsCollateral(userConfigData, reserveData.id); - - balance = AccountBalance({ - asset: asset, - collateralBalance: collateralBalance, - debtBalance: debtBalance, - collateralValue: countsAsCollateral ? _valueInBase(oracle, asset, collateralBalance, fork) : 0, - debtValue: debtBalance == 0 ? 0 : _valueInBase(oracle, asset, debtBalance, fork), - countsAsCollateral: countsAsCollateral, - metadata: abi.encode(reserveData.id) - }); - - return (true, balance); - } - - /// @notice Reads Aave v3 Horizon reserve metadata for a single asset at the requested snapshot fork. - /// @param asset The reserve asset whose metadata should be queried. - /// @param fork The snapshot fork to query. - /// @return reserveData Reserve metadata returned by `Pool.getReserveData(...)`. - function _getReserveData(address asset, PhEvm.ForkId memory fork) - internal - view - returns (AaveV3Types.ReserveDataLegacy memory reserveData) - { - reserveData = abi.decode( - _viewAt(POOL, abi.encodeCall(IAaveV3PoolLike.getReserveData, (asset)), fork), - (AaveV3Types.ReserveDataLegacy) - ); - } - - /// @notice Reads the user's total debt for one reserve from Aave v3 Horizon debt-token balances. - /// @dev The example sums stable and variable debt token balances to make the liquidation bound - /// robust across reserve configurations. - /// @param asset The reserve asset whose debt position should be queried. - /// @param account The user whose debt should be read. - /// @param fork The snapshot fork to query. - /// @return debtBalance Total reserve debt for the user. - function _getUserReserveDebt(address asset, address account, PhEvm.ForkId memory fork) - internal - view - returns (uint256 debtBalance) - { - AaveV3Types.ReserveDataLegacy memory reserveData = _getReserveData(asset, fork); - debtBalance = _readOptionalBalance(reserveData.stableDebtTokenAddress, account, fork) - + _readOptionalBalance(reserveData.variableDebtTokenAddress, account, fork); - } - - /// @notice Reads a token balance when the token address may be unset. - /// @dev 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. - /// @param token The token contract to query, or `address(0)` when absent. - /// @param account The account whose balance should be read. - /// @param fork The snapshot fork to query. - /// @return balance The token balance, or zero when `token == address(0)`. - function _readOptionalBalance(address token, address account, PhEvm.ForkId memory fork) - internal - view - returns (uint256 balance) - { - if (token == address(0)) { - return 0; - } - - return _readBalanceAt(token, account, fork); - } - - /// @notice Converts an asset-denominated balance into Aave base currency. - /// @dev 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. - /// @param oracle Aave v3 price oracle. - /// @param asset Asset whose price and decimals should be read. - /// @param balance Raw token amount to convert. - /// @param fork The snapshot fork to query. - /// @return value Asset value expressed in Aave base currency units. - function _valueInBase(address oracle, address asset, uint256 balance, PhEvm.ForkId memory fork) - internal - view - returns (uint256) - { - uint256 price = _readUintAt(oracle, abi.encodeCall(IAaveV3OracleLike.getAssetPrice, (asset)), fork); - uint8 decimals = _readUint8At(asset, abi.encodeCall(IERC20MetadataLike.decimals, ()), fork); - return ph.mulDivDown(balance, price, 10 ** uint256(decimals)); - } - - /// @notice Returns whether the reserve is enabled as collateral in Aave v3 Horizon's user config bitset. - /// @dev 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. - /// @param userConfigData Packed Aave v3 user configuration. - /// @param reserveId Reserve id from `getReserveData(...)`. - /// @return isCollateral True when the reserve currently counts as collateral. - function _isUsingAsCollateral(uint256 userConfigData, uint256 reserveId) internal pure returns (bool) { - return ((userConfigData >> (reserveId * 2)) & 1) != 0; - } - - /// @notice Safely casts a `uint256` metric to `int256` for `SolvencyState`. - /// @dev 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. - /// @param value Unsigned metric value to convert. - /// @return signedValue Saturated signed representation of `value`. - function _toInt256(uint256 value) internal pure returns (int256) { - if (value > uint256(type(int256).max)) { - return type(int256).max; - } - // forge-lint: disable-next-line(unsafe-typecast) - return int256(value); - } +/// @dev The underlying logic lives in `AaveV3LikeProtectionSuite` so Base Aave, local Horizon +/// deployments, and close forks can reuse the same operation-safety model. The deployment +/// wrapper exists to keep the public example small: pass the pool and addresses provider, then +/// the shared suite supplies health-factor and bounded-consumption checks. +contract AaveV3HorizonProtectionSuite is AaveV3LikeProtectionSuite { + constructor(address pool_, address addressesProvider_) AaveV3LikeProtectionSuite(pool_, addressesProvider_) {} } /// @title AaveV3HorizonOperationSafetyAssertion /// @author Phylax Systems /// @notice Example single-entry assertion bundle for Aave v3 Horizon. /// @dev Usage: -/// `cl.assertion({ adopter: aaveV3HorizonPool, createData: abi.encodePacked(type(AaveV3HorizonOperationSafetyAssertion).creationCode, abi.encode(aaveV3HorizonPool)), fnSelector: AaveV3HorizonOperationSafetyAssertion.assertOperationSafety.selector })` -contract AaveV3HorizonOperationSafetyAssertion is LendingBaseAssertion { - /// @notice Dedicated Horizon suite deployed by this assertion bundle. - /// @dev Keeping the suite in a helper contract preserves the one-create-data UX while keeping - /// the assertion runtime below the EIP-170 size limit enforced by CI. - ILendingProtectionSuite internal immutable SUITE; - - /// @notice Creates an Aave v3 Horizon assertion bundle with an internally deployed suite. - /// @param pool_ Aave v3 Horizon pool used both as the suite data source and assertion adopter. - constructor(address pool_) { - SUITE = ILendingProtectionSuite(address(new AaveV3HorizonProtectionSuite(pool_))); - } - - /// @notice Returns the suite implementation used by the generic lending assertion base. - /// @dev The assertion keeps protocol-specific logic in a dedicated helper suite contract so the - /// assertion runtime stays within CI's contract-size limit. - /// @return suite The internally deployed common lending suite implementation. - function _suite() internal view override returns (ILendingProtectionSuite) { - return SUITE; - } +/// `cl.assertion({ adopter: aaveV3HorizonPool, createData: abi.encodePacked(type(AaveV3HorizonOperationSafetyAssertion).creationCode, abi.encode(aaveV3HorizonPool, addressesProvider)), fnSelector: AaveV3HorizonOperationSafetyAssertion.assertOperationSafety.selector })` +/// +/// The assertion is registered against the pool because the pool is the entry point for borrow, +/// withdraw, liquidation, collateral-flag, aToken transfer-finalization, and e-mode changes. +/// A revert from this bundle means a risk-increasing pool call either made a healthy user +/// liquidatable or consumed more user debt/collateral claim than the pre-call state allowed. +contract AaveV3HorizonOperationSafetyAssertion is AaveV3LikeOperationSafetyAssertionBase { + constructor(address pool_, address addressesProvider_) + AaveV3LikeOperationSafetyAssertionBase(ILendingProtectionSuite( + address(new AaveV3HorizonProtectionSuite(pool_, addressesProvider_)) + )) + {} } /// @title AaveV3ProtectionSuite /// @author Phylax Systems /// @notice Compatibility alias preserving the old generic Aave v3 suite name. -/// @dev The implementation is Horizon-specific and derived from the local Horizon repository. contract AaveV3ProtectionSuite is AaveV3HorizonProtectionSuite { - /// @notice Creates the compatibility alias. - /// @param pool_ Aave v3 Horizon pool used by the underlying suite. - constructor(address pool_) AaveV3HorizonProtectionSuite(pool_) {} + constructor(address pool_, address addressesProvider_) AaveV3HorizonProtectionSuite(pool_, addressesProvider_) {} } /// @title AaveV3OperationSafetyAssertion /// @author Phylax Systems /// @notice Compatibility alias preserving the old generic Aave v3 assertion name. -/// @dev New users should prefer `AaveV3HorizonOperationSafetyAssertion` to make the Horizon scope explicit. contract AaveV3OperationSafetyAssertion is AaveV3HorizonOperationSafetyAssertion { - /// @notice Creates the compatibility alias. - /// @param pool_ Aave v3 Horizon pool used by the underlying assertion bundle. - constructor(address pool_) AaveV3HorizonOperationSafetyAssertion(pool_) {} + constructor(address pool_, address addressesProvider_) + AaveV3HorizonOperationSafetyAssertion(pool_, addressesProvider_) + {} } /// @title AaveV3PostOperationSolvencyAssertion /// @author Phylax Systems /// @notice Deprecated compatibility alias for the pre-operation-safety contract name. -/// @dev New users should prefer `AaveV3HorizonOperationSafetyAssertion`. contract AaveV3PostOperationSolvencyAssertion is AaveV3HorizonOperationSafetyAssertion { - /// @notice Creates the deprecated compatibility alias. - /// @param pool_ Aave v3 Horizon pool used by the underlying assertion bundle. - constructor(address pool_) AaveV3HorizonOperationSafetyAssertion(pool_) {} + constructor(address pool_, address addressesProvider_) + AaveV3HorizonOperationSafetyAssertion(pool_, addressesProvider_) + {} } diff --git a/src/protection/lending/examples/SparkLendV1OperationSafety.sol b/src/protection/lending/examples/SparkLendV1OperationSafety.sol new file mode 100644 index 0000000..4986f2a --- /dev/null +++ b/src/protection/lending/examples/SparkLendV1OperationSafety.sol @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {ILendingProtectionSuite} from "../ILendingProtectionSuite.sol"; +import {AaveV3LikeProtectionSuite} from "./AaveV3LikeHelpers.sol"; +import {AaveV3LikeOperationSafetyAssertionBase} from "./AaveV3LikeOperationSafety.sol"; + +/// @title SparkLendV1ProtectionSuite +/// @author Phylax Systems +/// @notice `ILendingProtectionSuite` implementation for SparkLend v1. +/// @dev SparkLend v1 preserves the Aave v3 pool interface and health-factor accounting closely +/// enough to reuse the shared Aave v3-like lending adapter directly. +contract SparkLendV1ProtectionSuite is AaveV3LikeProtectionSuite { + constructor(address pool_, address addressesProvider_) AaveV3LikeProtectionSuite(pool_, addressesProvider_) {} +} + +/// @title SparkLendV1OperationSafetyAssertion +/// @author Phylax Systems +/// @notice Single-entry assertion bundle for SparkLend v1 pools. +/// @dev Usage: +/// `cl.assertion({ adopter: sparkPool, createData: abi.encodePacked(type(SparkLendV1OperationSafetyAssertion).creationCode, abi.encode(sparkPool, addressesProvider)), fnSelector: SparkLendV1OperationSafetyAssertion.assertOperationSafety.selector })` +contract SparkLendV1OperationSafetyAssertion is AaveV3LikeOperationSafetyAssertionBase { + constructor(address pool_, address addressesProvider_) + AaveV3LikeOperationSafetyAssertionBase(ILendingProtectionSuite( + address(new SparkLendV1ProtectionSuite(pool_, addressesProvider_)) + )) + {} +} + +/// @title SparkLendV1PostOperationSolvencyAssertion +/// @author Phylax Systems +/// @notice Deprecated compatibility alias for the pre-operation-safety contract name. +contract SparkLendV1PostOperationSolvencyAssertion is SparkLendV1OperationSafetyAssertion { + constructor(address pool_, address addressesProvider_) + SparkLendV1OperationSafetyAssertion(pool_, addressesProvider_) + {} +} diff --git a/src/protection/swaps/examples/UniswapV4PoolManagerAssertion.sol b/src/protection/swaps/examples/UniswapV4PoolManagerAssertion.sol new file mode 100644 index 0000000..43b0acb --- /dev/null +++ b/src/protection/swaps/examples/UniswapV4PoolManagerAssertion.sol @@ -0,0 +1,243 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {PhEvm} from "../../../PhEvm.sol"; +import {AssertionSpec} from "../../../SpecRecorder.sol"; + +import {UniswapV4PoolManagerHelpers} from "./UniswapV4PoolManagerHelpers.sol"; +import {IUniswapV4PoolManagerLike} from "./UniswapV4PoolManagerInterfaces.sol"; + +/// @title UniswapV4PoolManagerAssertion +/// @author Phylax Systems +/// @notice Example assertion bundle for a single Uniswap v4 pool sitting inside the singleton +/// PoolManager. +/// @dev Protects the pool's core AMM invariants and the manager-level custody invariants: +/// - swaps move price only in the requested direction and never past the caller's price limit; +/// - modifyLiquidity calls update active liquidity exactly when the position range contains +/// the current tick; +/// - protocol-fee accruals stay backed by the manager's currency balances; +/// - protocol-fee collection does not mutate any of the watched pool's swap-critical state. +/// +/// Because the PoolManager is shared across every v4 pool, each call-scoped trigger must check +/// that the call's PoolKey matches the configured pool before evaluating the per-pool invariants. +/// Calls to other pools no-op silently. +/// +/// The example intentionally combines per-pool state checks with manager-level custody checks: +/// - per-pool checks protect the configured pool's price, tick, liquidity, and fee-growth state; +/// - manager-level checks protect the singleton accounting that backs protocol-fee liabilities for +/// the currencies used by the configured pool; +/// - PoolKey filtering prevents activity in unrelated pools from producing false positives while +/// still letting one assertion deployment monitor a specific pool inside the singleton. +contract UniswapV4PoolManagerAssertion is UniswapV4PoolManagerHelpers { + constructor(address manager_, IUniswapV4PoolManagerLike.PoolKey memory poolKey_) + UniswapV4PoolManagerHelpers(manager_, poolKey_) + { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + /// @notice Registers Uniswap v4 PoolManager selectors against their protection assertions. + /// @dev The PoolManager is the assertion adopter. Call-scoped triggers compare the exact + /// pre-call and post-call snapshots for the matched manager operation. The assertion + /// functions that receive a PoolKey return early when the call targets a different pool. + function triggers() external view override { + registerFnCallTrigger(this.assertSwapPriceMovement.selector, IUniswapV4PoolManagerLike.swap.selector); + registerFnCallTrigger( + this.assertActiveLiquidityAccounting.selector, IUniswapV4PoolManagerLike.modifyLiquidity.selector + ); + _registerProtocolFeeCustodyTriggers(); + registerFnCallTrigger( + this.assertCollectProtocolPreservesPoolState.selector, + IUniswapV4PoolManagerLike.collectProtocolFees.selector + ); + } + + /// @notice Registers the tx-end protocol-fee custody check. + /// @dev Fee custody is global per currency in v4, and swap/donate calls may accrue fees before + /// the surrounding unlock flow settles token custody. Checking at tx end avoids tripping on + /// ordinary mid-flow accounting while still requiring final protocol-fee liabilities to be + /// backed by PoolManager custody for ERC-20 currencies. + function _registerProtocolFeeCustodyTriggers() internal view { + registerTxEndTrigger(this.assertProtocolFeesCoveredByCustody.selector); + } + + /// @notice A successful swap must respect direction and caller-supplied price limits. + /// @dev For zeroForOne swaps `sqrtPriceX96` can only decrease; for oneForZero swaps it can + /// only increase. The post-call price must also stay strictly inside V4's tick-range + /// bounds. A failure means swap execution moved price the wrong way or crossed the + /// explicit limit that bounds user execution. This protects the user-facing swap guarantee + /// rather than duplicating v4's calldata validation. + function assertSwapPriceMovement() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + _requireConfiguredManagerIsAdopter(); + (IUniswapV4PoolManagerLike.PoolKey memory key, IUniswapV4PoolManagerLike.SwapParams memory params,) = + _swapArgs(ph.callinputAt(ctx.callStart)); + if (!_matchesConfiguredPool(key)) { + return; + } + + Slot0Snapshot memory pre = _slot0At(_preCall(ctx.callStart)); + Slot0Snapshot memory post = _slot0At(_postCall(ctx.callEnd)); + + require(post.sqrtPriceX96 > MIN_SQRT_PRICE, "UniswapV4Pool: price below min"); + require(post.sqrtPriceX96 < MAX_SQRT_PRICE, "UniswapV4Pool: price above max"); + + if (params.zeroForOne) { + require(post.sqrtPriceX96 <= pre.sqrtPriceX96, "UniswapV4Pool: zeroForOne price increased"); + require(post.sqrtPriceX96 >= params.sqrtPriceLimitX96, "UniswapV4Pool: zeroForOne crossed limit"); + } else { + require(post.sqrtPriceX96 >= pre.sqrtPriceX96, "UniswapV4Pool: oneForZero price decreased"); + require(post.sqrtPriceX96 <= params.sqrtPriceLimitX96, "UniswapV4Pool: oneForZero crossed limit"); + } + } + + /// @notice modifyLiquidity must update active liquidity exactly for in-range positions. + /// @dev V4's per-pool `liquidity` is only the currently active liquidity. A successful + /// modifyLiquidity whose range excludes the pre-call tick must leave it unchanged; an + /// in-range modifyLiquidity must shift it by `liquidityDelta`. A failure means active + /// liquidity no longer reflects the position range that the swap engine will use. + /// Slot0 (price + tick) must also be unchanged because modifyLiquidity is not allowed to + /// move the pool. This catches accounting corruption that may not be visible until a later + /// swap prices against the wrong active liquidity. + function assertActiveLiquidityAccounting() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + _requireConfiguredManagerIsAdopter(); + (IUniswapV4PoolManagerLike.PoolKey memory key, IUniswapV4PoolManagerLike.ModifyLiquidityParams memory params,) = + _modifyLiquidityArgs(ph.callinputAt(ctx.callStart)); + if (!_matchesConfiguredPool(key)) { + return; + } + + Slot0Snapshot memory preSlot0 = _slot0At(_preCall(ctx.callStart)); + Slot0Snapshot memory postSlot0 = _slot0At(_postCall(ctx.callEnd)); + uint128 preLiquidity = _liquidityAt(_preCall(ctx.callStart)); + uint128 postLiquidity = _liquidityAt(_postCall(ctx.callEnd)); + + if (_inRange(preSlot0.tick, params.tickLower, params.tickUpper)) { + int256 expected = int256(uint256(preLiquidity)) + params.liquidityDelta; + require(expected >= 0, "UniswapV4Pool: liquidityDelta underflows active liquidity"); + require(uint256(expected) == uint256(postLiquidity), "UniswapV4Pool: in-range liquidity mismatch"); + } else { + require(postLiquidity == preLiquidity, "UniswapV4Pool: out-of-range liquidity changed"); + } + + require(postSlot0.sqrtPriceX96 == preSlot0.sqrtPriceX96, "UniswapV4Pool: liquidity op changed price"); + require(postSlot0.tick == preSlot0.tick, "UniswapV4Pool: liquidity op changed tick"); + } + + /// @notice Manager currency balances must keep covering accrued protocol fees. + /// @dev Swaps and donates can accrue protocol fees before the surrounding unlock flow settles + /// token custody, while collectProtocolFees withdraws them. The PoolManager singleton holds + /// tokens for every pool, but `protocolFeesAccrued` is summed per currency across all pools, + /// so the invariant `manager.balanceOf(currency) >= protocolFeesAccrued(currency)` must hold + /// globally at transaction end for ERC-20 currencies used by the configured pool. + function assertProtocolFeesCoveredByCustody() external view { + _requireConfiguredManagerIsAdopter(); + PoolSnapshot memory post = _snapshotAt(_postTx()); + + require(post.managerBalance0 >= post.protocolFeesAccrued0, "UniswapV4Pool: currency0 protocol fees uncovered"); + require(post.managerBalance1 >= post.protocolFeesAccrued1, "UniswapV4Pool: currency1 protocol fees uncovered"); + } + + /// @notice Protocol-fee collection must not mutate swap-critical pool state. + /// @dev `collectProtocolFees` may only reduce `protocolFeesAccrued[currency]` and transfer + /// the matching token custody. A failure means owner fee collection changed the + /// configured pool's price, tick, fee schedule, active liquidity, or fee growth, or + /// the protocol-fee accounting and manager balance change disagreed for the targeted + /// currency. Calls collecting a currency that is not part of the watched pool only + /// assert the per-pool no-mutation invariant. This protects against singleton side effects + /// where a fee withdrawal for one currency unexpectedly contaminates the watched pool. + function assertCollectProtocolPreservesPoolState() external view { + PhEvm.TriggerContext memory ctx = ph.context(); + _requireConfiguredManagerIsAdopter(); + (, address currency, uint256 amount) = _collectProtocolFeesArgs(ph.callinputAt(ctx.callStart)); + + PoolSnapshot memory pre = _snapshotAt(_preCall(ctx.callStart)); + PoolSnapshot memory post = _snapshotAt(_postCall(ctx.callEnd)); + + require(post.slot0.sqrtPriceX96 == pre.slot0.sqrtPriceX96, "UniswapV4Pool: collectProtocol changed price"); + require(post.slot0.tick == pre.slot0.tick, "UniswapV4Pool: collectProtocol changed tick"); + require(post.slot0.protocolFee == pre.slot0.protocolFee, "UniswapV4Pool: collectProtocol changed protocolFee"); + require(post.slot0.lpFee == pre.slot0.lpFee, "UniswapV4Pool: collectProtocol changed lpFee"); + require(post.liquidity == pre.liquidity, "UniswapV4Pool: collectProtocol changed liquidity"); + require( + post.feeGrowthGlobal0X128 == pre.feeGrowthGlobal0X128, "UniswapV4Pool: collectProtocol changed feeGrowth0" + ); + require( + post.feeGrowthGlobal1X128 == pre.feeGrowthGlobal1X128, "UniswapV4Pool: collectProtocol changed feeGrowth1" + ); + + if (currency == CURRENCY0) { + _requireCollectProtocolCustodyMatches( + amount, + pre.protocolFeesAccrued0, + post.protocolFeesAccrued0, + pre.managerBalance0, + post.managerBalance0, + "0", + _isNativeCurrency(CURRENCY0) + ); + require( + post.protocolFeesAccrued1 == pre.protocolFeesAccrued1, + "UniswapV4Pool: collectProtocol touched untargeted currency1 accrual" + ); + } else if (currency == CURRENCY1) { + _requireCollectProtocolCustodyMatches( + amount, + pre.protocolFeesAccrued1, + post.protocolFeesAccrued1, + pre.managerBalance1, + post.managerBalance1, + "1", + _isNativeCurrency(CURRENCY1) + ); + require( + post.protocolFeesAccrued0 == pre.protocolFeesAccrued0, + "UniswapV4Pool: collectProtocol touched untargeted currency0 accrual" + ); + } else { + require( + post.protocolFeesAccrued0 == pre.protocolFeesAccrued0, + "UniswapV4Pool: collectProtocol touched untargeted currency0 accrual" + ); + require( + post.protocolFeesAccrued1 == pre.protocolFeesAccrued1, + "UniswapV4Pool: collectProtocol touched untargeted currency1 accrual" + ); + } + } + + /// @dev When `amount == 0`, V4 collects the full accrued amount for the currency. We treat + /// the actual delta as the amount taken and require the manager's balance to drop by the + /// same amount. + function _requireCollectProtocolCustodyMatches( + uint256 requestedAmount, + uint256 preAccrued, + uint256 postAccrued, + uint256 preBalance, + uint256 postBalance, + string memory currencyTag, + bool isNativeCurrency + ) internal pure { + require(postAccrued <= preAccrued, _msg("UniswapV4Pool: collectProtocol increased accrued", currencyTag)); + + uint256 accruedDelta = preAccrued - postAccrued; + if (!isNativeCurrency) { + require(postBalance <= preBalance, _msg("UniswapV4Pool: collectProtocol increased balance", currencyTag)); + + uint256 balanceDelta = preBalance - postBalance; + require(accruedDelta == balanceDelta, _msg("UniswapV4Pool: collectProtocol custody mismatch", currencyTag)); + } + + if (requestedAmount != 0) { + require( + accruedDelta == requestedAmount, _msg("UniswapV4Pool: collectProtocol amount mismatch", currencyTag) + ); + } else { + require(postAccrued == 0, _msg("UniswapV4Pool: collectProtocol left residual accrual", currencyTag)); + } + } + + function _msg(string memory base, string memory tag) internal pure returns (string memory) { + return string.concat(base, " currency", tag); + } +} diff --git a/src/protection/swaps/examples/UniswapV4PoolManagerHelpers.sol b/src/protection/swaps/examples/UniswapV4PoolManagerHelpers.sol new file mode 100644 index 0000000..a9db1b3 --- /dev/null +++ b/src/protection/swaps/examples/UniswapV4PoolManagerHelpers.sol @@ -0,0 +1,182 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Assertion} from "../../../Assertion.sol"; +import {PhEvm} from "../../../PhEvm.sol"; + +import {IUniswapV4PoolManagerLike} from "./UniswapV4PoolManagerInterfaces.sol"; + +/// @title UniswapV4PoolManagerHelpers +/// @author Phylax Systems +/// @notice Fork-aware Uniswap v4 PoolManager state helpers used by the example assertions. +/// @dev V4 stores every pool's state inside the singleton PoolManager at slot 6 +/// (`mapping(PoolId => Pool.State) _pools`). For each watched pool we compute the per-pool +/// base storage slot once at construction and then read the packed `Slot0`, `liquidity`, and +/// fee growth via the manager's `extsload(bytes32)` precompile. Protocol-fee accruals are +/// tracked globally per currency on the manager, not per pool. +abstract contract UniswapV4PoolManagerHelpers is Assertion { + uint160 internal constant MIN_SQRT_PRICE = 4_295_128_739; + uint160 internal constant MAX_SQRT_PRICE = 1_461_446_703_485_210_103_287_273_052_203_988_822_378_723_970_342; + + /// @dev Storage slot of `mapping(PoolId => Pool.State) _pools` on the PoolManager. Mirrors + /// `StateLibrary.POOLS_SLOT` from v4-core. + uint256 internal constant POOLS_SLOT = 6; + + /// @dev Per-pool offsets inside `Pool.State`. Mirror `StateLibrary` constants in v4-core. + uint256 internal constant FEE_GROWTH_GLOBAL0_OFFSET = 1; + uint256 internal constant FEE_GROWTH_GLOBAL1_OFFSET = 2; + uint256 internal constant LIQUIDITY_OFFSET = 3; + + address internal immutable MANAGER; + address internal immutable CURRENCY0; + address internal immutable CURRENCY1; + bytes32 internal immutable POOL_ID; + bytes32 internal immutable POOL_STATE_BASE_SLOT; + + struct Slot0Snapshot { + uint160 sqrtPriceX96; + int24 tick; + uint24 protocolFee; + uint24 lpFee; + } + + struct PoolSnapshot { + Slot0Snapshot slot0; + uint128 liquidity; + uint256 feeGrowthGlobal0X128; + uint256 feeGrowthGlobal1X128; + uint256 protocolFeesAccrued0; + uint256 protocolFeesAccrued1; + uint256 managerBalance0; + uint256 managerBalance1; + } + + /// @dev Accepts the manager and the full PoolKey explicitly so the constructor never reads + /// from the adopter. The Credible Layer assertion-deploy runtime is isolated from the + /// calling state, so a `manager.extsload(...)` call in the constructor would revert with + /// EXTCODESIZE = 0. + constructor(address manager_, IUniswapV4PoolManagerLike.PoolKey memory poolKey_) { + require(manager_ != address(0), "UniswapV4Pool: manager zero"); + require(poolKey_.currency0 < poolKey_.currency1, "UniswapV4Pool: currencies misordered"); + MANAGER = manager_; + CURRENCY0 = poolKey_.currency0; + CURRENCY1 = poolKey_.currency1; + POOL_ID = keccak256(abi.encode(poolKey_)); + POOL_STATE_BASE_SLOT = keccak256(abi.encode(POOL_ID, POOLS_SLOT)); + } + + function _snapshotAt(PhEvm.ForkId memory fork) internal view returns (PoolSnapshot memory snapshot) { + snapshot.slot0 = _slot0At(fork); + snapshot.liquidity = _liquidityAt(fork); + (snapshot.feeGrowthGlobal0X128, snapshot.feeGrowthGlobal1X128) = _feeGrowthGlobalsAt(fork); + snapshot.protocolFeesAccrued0 = _protocolFeesAccruedAt(CURRENCY0, fork); + snapshot.protocolFeesAccrued1 = _protocolFeesAccruedAt(CURRENCY1, fork); + snapshot.managerBalance0 = _currencyBalanceAt(CURRENCY0, MANAGER, fork); + snapshot.managerBalance1 = _currencyBalanceAt(CURRENCY1, MANAGER, fork); + } + + function _slot0At(PhEvm.ForkId memory fork) internal view returns (Slot0Snapshot memory slot0) { + bytes32 packed = _extsloadAt(POOL_STATE_BASE_SLOT, fork); + slot0.sqrtPriceX96 = uint160(uint256(packed)); + slot0.tick = int24(int256(uint256(packed) >> 160)); + slot0.protocolFee = uint24(uint256(packed) >> 184); + slot0.lpFee = uint24(uint256(packed) >> 208); + } + + function _liquidityAt(PhEvm.ForkId memory fork) internal view returns (uint128 liquidity) { + bytes32 raw = _extsloadAt(_offsetSlot(LIQUIDITY_OFFSET), fork); + liquidity = uint128(uint256(raw)); + } + + function _feeGrowthGlobalsAt(PhEvm.ForkId memory fork) internal view returns (uint256 g0, uint256 g1) { + g0 = uint256(_extsloadAt(_offsetSlot(FEE_GROWTH_GLOBAL0_OFFSET), fork)); + g1 = uint256(_extsloadAt(_offsetSlot(FEE_GROWTH_GLOBAL1_OFFSET), fork)); + } + + function _protocolFeesAccruedAt(address currency, PhEvm.ForkId memory fork) internal view returns (uint256) { + return _readUintAt(MANAGER, abi.encodeCall(IUniswapV4PoolManagerLike.protocolFeesAccrued, (currency)), fork); + } + + function _currencyBalanceAt(address currency, address account, PhEvm.ForkId memory fork) + internal + view + returns (uint256) + { + if (_isNativeCurrency(currency)) { + return type(uint256).max; + } + + return _readBalanceAt(currency, account, fork); + } + + function _isNativeCurrency(address currency) internal pure returns (bool) { + return currency == address(0); + } + + function _extsloadAt(bytes32 slot, PhEvm.ForkId memory fork) internal view returns (bytes32) { + // `extsload(bytes32)` selector — disambiguated from the array overload. + bytes memory raw = _viewAt(MANAGER, abi.encodeWithSelector(bytes4(0x1e2eaeaf), slot), fork); + return abi.decode(raw, (bytes32)); + } + + function _offsetSlot(uint256 offset) internal view returns (bytes32) { + return bytes32(uint256(POOL_STATE_BASE_SLOT) + offset); + } + + function _swapArgs(bytes memory input) + internal + pure + returns ( + IUniswapV4PoolManagerLike.PoolKey memory key, + IUniswapV4PoolManagerLike.SwapParams memory params, + bytes memory hookData + ) + { + return abi.decode( + _args(input), (IUniswapV4PoolManagerLike.PoolKey, IUniswapV4PoolManagerLike.SwapParams, bytes) + ); + } + + function _modifyLiquidityArgs(bytes memory input) + internal + pure + returns ( + IUniswapV4PoolManagerLike.PoolKey memory key, + IUniswapV4PoolManagerLike.ModifyLiquidityParams memory params, + bytes memory hookData + ) + { + return abi.decode( + _args(input), (IUniswapV4PoolManagerLike.PoolKey, IUniswapV4PoolManagerLike.ModifyLiquidityParams, bytes) + ); + } + + function _collectProtocolFeesArgs(bytes memory input) + internal + pure + returns (address recipient, address currency, uint256 amount) + { + return abi.decode(_args(input), (address, address, uint256)); + } + + function _inRange(int24 currentTick, int24 tickLower, int24 tickUpper) internal pure returns (bool) { + return tickLower <= currentTick && currentTick < tickUpper; + } + + function _matchesConfiguredPool(IUniswapV4PoolManagerLike.PoolKey memory key) internal view returns (bool) { + return keccak256(abi.encode(key)) == POOL_ID; + } + + function _requireConfiguredManagerIsAdopter() internal view { + require(ph.getAssertionAdopter() == MANAGER, "UniswapV4Pool: configured manager is not adopter"); + } + + function _args(bytes memory input) internal pure returns (bytes memory args) { + require(input.length >= 4, "UniswapV4Pool: short calldata"); + + args = new bytes(input.length - 4); + for (uint256 i; i < args.length; ++i) { + args[i] = input[i + 4]; + } + } +} diff --git a/src/protection/swaps/examples/UniswapV4PoolManagerInterfaces.sol b/src/protection/swaps/examples/UniswapV4PoolManagerInterfaces.sol new file mode 100644 index 0000000..94bb86d --- /dev/null +++ b/src/protection/swaps/examples/UniswapV4PoolManagerInterfaces.sol @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +/// @title IUniswapV4PoolManagerLike +/// @author Phylax Systems +/// @notice Minimal Uniswap v4 PoolManager surface needed by the example assertion bundle. +/// @dev Currency and IHooks are typed `address` here. The canonical Uniswap v4 ABI encodes +/// both as `address`, so the function selectors derived from these signatures match the +/// production PoolManager exactly. +interface IUniswapV4PoolManagerLike { + struct PoolKey { + address currency0; + address currency1; + uint24 fee; + int24 tickSpacing; + address hooks; + } + + struct SwapParams { + bool zeroForOne; + int256 amountSpecified; + uint160 sqrtPriceLimitX96; + } + + struct ModifyLiquidityParams { + int24 tickLower; + int24 tickUpper; + int256 liquidityDelta; + bytes32 salt; + } + + function initialize(PoolKey calldata key, uint160 sqrtPriceX96) external returns (int24 tick); + + function modifyLiquidity(PoolKey calldata key, ModifyLiquidityParams calldata params, bytes calldata hookData) + external + returns (int256 callerDelta, int256 feesAccrued); + + function swap(PoolKey calldata key, SwapParams calldata params, bytes calldata hookData) + external + returns (int256 swapDelta); + + function donate(PoolKey calldata key, uint256 amount0, uint256 amount1, bytes calldata hookData) + external + returns (int256 delta); + + function take(address currency, address to, uint256 amount) external; + + function settle() external payable returns (uint256); + + function sync(address currency) external; + + function mint(address to, uint256 id, uint256 amount) external; + + function burn(address from, uint256 id, uint256 amount) external; + + function updateDynamicLPFee(PoolKey calldata key, uint24 newDynamicLPFee) external; + + function setProtocolFee(PoolKey calldata key, uint24 newProtocolFee) external; + + function setProtocolFeeController(address controller) external; + + function collectProtocolFees(address recipient, address currency, uint256 amount) external returns (uint256); + + function unlock(bytes calldata data) external returns (bytes memory); + + function protocolFeesAccrued(address currency) external view returns (uint256); + + function extsload(bytes32 slot) external view returns (bytes32); + + function extsload(bytes32 startSlot, uint256 nSlots) external view returns (bytes32[] memory); +} diff --git a/src/protection/vault/ERC4626BaseAssertion.sol b/src/protection/vault/ERC4626BaseAssertion.sol index 4d02fb6..07d565e 100644 --- a/src/protection/vault/ERC4626BaseAssertion.sol +++ b/src/protection/vault/ERC4626BaseAssertion.sol @@ -14,8 +14,8 @@ import {IERC4626} from "./IERC4626.sol"; /// Example – combine share-price, preview, and outflow invariants: /// ```solidity /// contract MyVaultAssertion is ERC4626SharePriceAssertion, ERC4626PreviewAssertion, ERC4626CumulativeOutflowAssertion { -/// constructor(address _vault) -/// ERC4626BaseAssertion(_vault) +/// constructor(address _vault, address _asset) +/// ERC4626BaseAssertion(_vault, _asset) /// ERC4626SharePriceAssertion(50) // 50 bps tolerance /// ERC4626CumulativeOutflowAssertion(1_000, 24 hours) // 10% in 24h /// {} @@ -34,9 +34,14 @@ abstract contract ERC4626BaseAssertion is Assertion { /// @notice The underlying ERC-20 asset of the vault. address internal immutable asset; - constructor(address _vault) { + /// @dev Accepts the asset address explicitly so the constructor never reads from the adopter. + /// The Credible Layer's assertion-deploy runtime is isolated from the calling test state, + /// so a `vault.asset()` call inside the constructor would revert with EXTCODESIZE = 0. + /// @param _vault The ERC-4626 vault being monitored (assertion adopter). + /// @param _asset The vault's underlying ERC-20 asset. + constructor(address _vault, address _asset) { vault = _vault; - asset = IERC4626(_vault).asset(); + asset = _asset; } // --------------------------------------------------------------- diff --git a/src/protection/vault/examples/MetaMorphoVaultAssertion.sol b/src/protection/vault/examples/MetaMorphoVaultAssertion.sol new file mode 100644 index 0000000..51a7a9a --- /dev/null +++ b/src/protection/vault/examples/MetaMorphoVaultAssertion.sol @@ -0,0 +1,66 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {AssertionSpec} from "../../../SpecRecorder.sol"; + +import {ERC4626BaseAssertion} from "../ERC4626BaseAssertion.sol"; +import {ERC4626CumulativeOutflowAssertion} from "../ERC4626CumulativeOutflowAssertion.sol"; +import {ERC4626PreviewAssertion} from "../ERC4626PreviewAssertion.sol"; +import {ERC4626SharePriceAssertion} from "../ERC4626SharePriceAssertion.sol"; + +/// @title MetaMorphoVaultAssertion +/// @author Phylax Systems +/// @notice Example ERC-4626 assertion bundle for MetaMorpho vaults. +/// @dev MetaMorpho vaults typically deploy deposited assets into Morpho Blue markets, so +/// vault-held ERC-20 balance does not need to equal `totalAssets()`. This bundle +/// intentionally omits `ERC4626AssetFlowAssertion` and keeps the ERC-4626 checks +/// that fit computed-asset vaults: share price, preview consistency, and cumulative +/// underlying outflow. +/// +/// The three inherited assertions cover different failure modes: +/// - per-call share price protects existing depositors from dilution during deposit, mint, +/// withdraw, or redeem calls; +/// - preview consistency checks that the pre-call ERC-4626 quote matches the shares/assets +/// actually returned by the triggered call; +/// - cumulative outflow acts as a rolling-window breaker for vault asset exits that are each +/// individually valid but collectively risky. +/// +/// A failure points to an externally visible vault-accounting problem: holders were diluted, +/// users received a result inconsistent with ERC-4626 previews, or the configured outflow +/// budget was breached. +contract MetaMorphoVaultAssertion is + ERC4626SharePriceAssertion, + ERC4626PreviewAssertion, + ERC4626CumulativeOutflowAssertion +{ + /// @param vault_ MetaMorpho vault instance whose selectors this bundle will monitor. + /// @param asset_ Underlying ERC-20 asset of the vault. + /// @param sharePriceToleranceBps_ Max share-price drift tolerated by + /// `ERC4626SharePriceAssertion`, in basis points. + /// @param outflowThresholdBps_ Cumulative net-outflow limit as bps of TVL enforced + /// by `ERC4626CumulativeOutflowAssertion` over the rolling window. + /// @param outflowWindowDuration_ Rolling window, in seconds, used by the outflow assertion. + constructor( + address vault_, + address asset_, + uint256 sharePriceToleranceBps_, + uint256 outflowThresholdBps_, + uint256 outflowWindowDuration_ + ) + ERC4626BaseAssertion(vault_, asset_) + ERC4626SharePriceAssertion(sharePriceToleranceBps_) + ERC4626CumulativeOutflowAssertion(outflowThresholdBps_, outflowWindowDuration_) + { + registerAssertionSpec(AssertionSpec.Reshiram); + } + + /// @notice Registers the ERC-4626 selectors against the MetaMorpho-safe assertion set. + /// @dev The selector set comes from the inherited ERC-4626 protections. We do not register the + /// asset-flow assertion because a healthy MetaMorpho vault can hold less on-hand USDC than + /// `totalAssets()` while its funds are allocated into Morpho markets. + function triggers() external view override { + _registerSharePriceTriggers(); + _registerPreviewTriggers(); + _registerCumulativeOutflowTriggers(); + } +} diff --git a/test/protection/lending/AaveV3LikeOperationSafety.t.sol b/test/protection/lending/AaveV3LikeOperationSafety.t.sol new file mode 100644 index 0000000..33d3700 --- /dev/null +++ b/test/protection/lending/AaveV3LikeOperationSafety.t.sol @@ -0,0 +1,200 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.13; + +import {Test} from "forge-std/Test.sol"; + +import {ILendingProtectionSuite} from "../../../src/protection/lending/ILendingProtectionSuite.sol"; +import {IAaveV3LikePool} from "../../../src/protection/lending/examples/AaveV3LikeInterfaces.sol"; +import {AaveV3HorizonProtectionSuite} from "../../../src/protection/lending/examples/AaveV3PostOperationSolvency.sol"; +import {SparkLendV1ProtectionSuite} from "../../../src/protection/lending/examples/SparkLendV1OperationSafety.sol"; + +contract MockAaveV3LikePool { + address internal immutable PROVIDER; + + constructor(address provider_) { + PROVIDER = provider_; + } + + function ADDRESSES_PROVIDER() external view returns (address) { + return PROVIDER; + } +} + +contract AaveV3LikeOperationSafetyTest is Test { + MockAaveV3LikePool internal pool; + SparkLendV1ProtectionSuite internal sparkSuite; + AaveV3HorizonProtectionSuite internal aaveSuite; + + function setUp() external { + pool = new MockAaveV3LikePool(address(0xBEEF)); + sparkSuite = new SparkLendV1ProtectionSuite(address(pool), address(0xBEEF)); + aaveSuite = new AaveV3HorizonProtectionSuite(address(pool), address(0xBEEF)); + } + + function testMonitoredSelectorsMatchAaveV3LikeSurface() external view { + bytes4[] memory selectors = sparkSuite.getMonitoredSelectors(); + + assertEq(selectors.length, 6); + assertEq(selectors[0], IAaveV3LikePool.borrow.selector); + assertEq(selectors[1], IAaveV3LikePool.withdraw.selector); + assertEq(selectors[2], IAaveV3LikePool.liquidationCall.selector); + assertEq(selectors[3], IAaveV3LikePool.setUserUseReserveAsCollateral.selector); + assertEq(selectors[4], IAaveV3LikePool.finalizeTransfer.selector); + assertEq(selectors[5], IAaveV3LikePool.setUserEMode.selector); + } + + function testSparkBorrowDecodeMarksDebtIncrease() external view { + ILendingProtectionSuite.OperationContext memory operation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.borrow.selector, + address(0xCA11E2), + abi.encodeCall(IAaveV3LikePool.borrow, (address(0xAAA1), 123e18, 2, 0, address(0xB0B0B0))) + ) + ); + + assertEq(operation.selector, IAaveV3LikePool.borrow.selector); + assertEq(uint256(operation.kind), uint256(ILendingProtectionSuite.OperationKind.Borrow)); + assertEq(operation.caller, address(0xCA11E2)); + assertEq(operation.account, address(0xB0B0B0)); + assertEq(operation.asset, address(0xAAA1)); + assertEq(operation.amount, 123e18); + assertTrue(operation.increasesDebt); + assertFalse(operation.reducesEffectiveCollateral); + assertTrue(sparkSuite.shouldCheckPostOperationSolvency(operation)); + } + + function testSparkWithdrawDecodeMarksCollateralReduction() external view { + ILendingProtectionSuite.OperationContext memory operation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.withdraw.selector, + address(0xBEEF12), + abi.encodeCall(IAaveV3LikePool.withdraw, (address(0xAAA2), type(uint256).max, address(0xFEEE))) + ) + ); + + assertEq(uint256(operation.kind), uint256(ILendingProtectionSuite.OperationKind.WithdrawCollateral)); + assertEq(operation.account, address(0xBEEF12)); + assertEq(operation.asset, address(0xAAA2)); + assertEq(operation.counterparty, address(0xFEEE)); + assertEq(operation.amount, type(uint256).max); + assertFalse(operation.increasesDebt); + assertTrue(operation.reducesEffectiveCollateral); + assertTrue(sparkSuite.shouldCheckPostOperationSolvency(operation)); + } + + function testSparkLiquidationDecodeTracksBothAssetsAndMetadata() external view { + ILendingProtectionSuite.OperationContext memory operation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.liquidationCall.selector, + address(0x1100A1), + abi.encodeCall( + IAaveV3LikePool.liquidationCall, (address(0xC011), address(0xDE87), address(0xABCD01), 55e6, true) + ) + ) + ); + + assertEq(uint256(operation.kind), uint256(ILendingProtectionSuite.OperationKind.Liquidation)); + assertEq(operation.account, address(0xABCD01)); + assertEq(operation.asset, address(0xDE87)); + assertEq(operation.relatedAsset, address(0xC011)); + assertEq(operation.counterparty, address(0x1100A1)); + assertEq(operation.amount, 55e6); + assertEq(operation.metadata, abi.encode(true)); + assertFalse(operation.increasesDebt); + assertFalse(operation.reducesEffectiveCollateral); + assertFalse(sparkSuite.shouldCheckPostOperationSolvency(operation)); + } + + function testSparkDisableCollateralOnlyTriggersWhenTurningCollateralOff() external view { + ILendingProtectionSuite.OperationContext memory disableOperation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.setUserUseReserveAsCollateral.selector, + address(0xABCD01), + abi.encodeCall(IAaveV3LikePool.setUserUseReserveAsCollateral, (address(0xC011), false)) + ) + ); + ILendingProtectionSuite.OperationContext memory enableOperation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.setUserUseReserveAsCollateral.selector, + address(0xABCD01), + abi.encodeCall(IAaveV3LikePool.setUserUseReserveAsCollateral, (address(0xC011), true)) + ) + ); + + assertEq(uint256(disableOperation.kind), uint256(ILendingProtectionSuite.OperationKind.DisableCollateral)); + assertEq(disableOperation.account, address(0xABCD01)); + assertTrue(disableOperation.reducesEffectiveCollateral); + assertTrue(sparkSuite.shouldCheckPostOperationSolvency(disableOperation)); + + assertEq(uint256(enableOperation.kind), uint256(ILendingProtectionSuite.OperationKind.Unknown)); + assertEq(enableOperation.account, address(0)); + assertFalse(enableOperation.reducesEffectiveCollateral); + assertFalse(sparkSuite.shouldCheckPostOperationSolvency(enableOperation)); + } + + function testSparkFinalizeTransferIgnoresSelfTransfers() external view { + ILendingProtectionSuite.OperationContext memory transferOperation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.finalizeTransfer.selector, + address(pool), + abi.encodeCall( + IAaveV3LikePool.finalizeTransfer, + (address(0xA710), address(0xF00D01), address(0x7000), 1 ether, 2 ether, 0) + ) + ) + ); + ILendingProtectionSuite.OperationContext memory selfTransferOperation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.finalizeTransfer.selector, + address(pool), + abi.encodeCall( + IAaveV3LikePool.finalizeTransfer, + (address(0xA710), address(0xF00D01), address(0xF00D01), 1 ether, 2 ether, 2 ether) + ) + ) + ); + + assertEq(uint256(transferOperation.kind), uint256(ILendingProtectionSuite.OperationKind.TransferCollateral)); + assertEq(transferOperation.account, address(0xF00D01)); + assertEq(transferOperation.counterparty, address(0x7000)); + assertTrue(transferOperation.reducesEffectiveCollateral); + assertTrue(sparkSuite.shouldCheckPostOperationSolvency(transferOperation)); + + assertEq(selfTransferOperation.account, address(0xF00D01)); + assertFalse(selfTransferOperation.reducesEffectiveCollateral); + assertFalse(sparkSuite.shouldCheckPostOperationSolvency(selfTransferOperation)); + } + + function testSparkSetUserEModeChecksPostOperationSolvency() external view { + ILendingProtectionSuite.OperationContext memory operation = sparkSuite.decodeOperation( + _triggered( + IAaveV3LikePool.setUserEMode.selector, + address(0xABCD01), + abi.encodeCall(IAaveV3LikePool.setUserEMode, (uint8(1))) + ) + ); + + assertEq(uint256(operation.kind), uint256(ILendingProtectionSuite.OperationKind.SetEMode)); + assertEq(operation.account, address(0xABCD01)); + assertEq(operation.amount, 1); + assertEq(operation.metadata, abi.encode(uint8(1))); + assertFalse(operation.increasesDebt); + assertFalse(operation.reducesEffectiveCollateral); + assertTrue(sparkSuite.shouldCheckPostOperationSolvency(operation)); + } + + function testAaveAndSparkSuitesDeploy() external view { + assertTrue(address(aaveSuite) != address(0)); + assertTrue(address(sparkSuite) != address(0)); + } + + function _triggered(bytes4 selector, address caller, bytes memory input) + internal + view + returns (ILendingProtectionSuite.TriggeredCall memory) + { + return ILendingProtectionSuite.TriggeredCall({ + selector: selector, caller: caller, target: address(pool), input: input, callStart: 1, callEnd: 2 + }); + } +} diff --git a/test/protection/swaps/UniswapV4PoolManagerAssertion.t.sol b/test/protection/swaps/UniswapV4PoolManagerAssertion.t.sol new file mode 100644 index 0000000..a1fed2b --- /dev/null +++ b/test/protection/swaps/UniswapV4PoolManagerAssertion.t.sol @@ -0,0 +1,127 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +import {Test} from "forge-std/Test.sol"; + +import {ERC20Mock} from "../../../lib/openzeppelin-contracts/contracts/mocks/token/ERC20Mock.sol"; + +import {UniswapV4PoolManagerHelpers} from "../../../src/protection/swaps/examples/UniswapV4PoolManagerHelpers.sol"; +import {IUniswapV4PoolManagerLike} from "../../../src/protection/swaps/examples/UniswapV4PoolManagerInterfaces.sol"; + +/// @notice Public harness exposing the helpers' internal custody invariant for direct testing. +contract UniswapV4PoolManagerAssertionHarness is UniswapV4PoolManagerHelpers { + constructor(address manager_, IUniswapV4PoolManagerLike.PoolKey memory poolKey_) + UniswapV4PoolManagerHelpers(manager_, poolKey_) + {} + + function triggers() external view override {} + + function poolId() external view returns (bytes32) { + return POOL_ID; + } + + function poolStateBaseSlot() external view returns (bytes32) { + return POOL_STATE_BASE_SLOT; + } + + function isNativeCurrency(address currency) external pure returns (bool) { + return _isNativeCurrency(currency); + } +} + +contract UniswapV4PoolManagerAssertionTest is Test { + ERC20Mock internal token0; + ERC20Mock internal token1; + address internal manager = makeAddr("manager"); + + UniswapV4PoolManagerAssertionHarness internal harness; + + function setUp() public { + token0 = new ERC20Mock(); + token1 = new ERC20Mock(); + (address c0, address c1) = + address(token0) < address(token1) ? (address(token0), address(token1)) : (address(token1), address(token0)); + + IUniswapV4PoolManagerLike.PoolKey memory key = IUniswapV4PoolManagerLike.PoolKey({ + currency0: c0, currency1: c1, fee: 3000, tickSpacing: 60, hooks: address(0) + }); + harness = new UniswapV4PoolManagerAssertionHarness(manager, key); + } + + function testUniswapV4SelectorsMatchExpectedSignatures() external pure { + // Canonical V4 selectors. PoolKey ABI = (address,address,uint24,int24,address); + // SwapParams ABI = (bool,int256,uint160); ModifyLiquidityParams ABI = (int24,int24,int256,bytes32). + assertEq( + IUniswapV4PoolManagerLike.swap.selector, + bytes4(keccak256("swap((address,address,uint24,int24,address),(bool,int256,uint160),bytes)")), + "swap" + ); + assertEq( + IUniswapV4PoolManagerLike.modifyLiquidity.selector, + bytes4( + keccak256("modifyLiquidity((address,address,uint24,int24,address),(int24,int24,int256,bytes32),bytes)") + ), + "modifyLiquidity" + ); + assertEq( + IUniswapV4PoolManagerLike.donate.selector, + bytes4(keccak256("donate((address,address,uint24,int24,address),uint256,uint256,bytes)")), + "donate" + ); + assertEq( + IUniswapV4PoolManagerLike.collectProtocolFees.selector, + bytes4(keccak256("collectProtocolFees(address,address,uint256)")), + "collectProtocolFees" + ); + assertEq( + IUniswapV4PoolManagerLike.initialize.selector, + bytes4(keccak256("initialize((address,address,uint24,int24,address),uint160)")), + "initialize" + ); + } + + function testPoolIdMatchesEncodingOfPoolKey() external view { + IUniswapV4PoolManagerLike.PoolKey memory key = IUniswapV4PoolManagerLike.PoolKey({ + currency0: address(token0) < address(token1) ? address(token0) : address(token1), + currency1: address(token0) < address(token1) ? address(token1) : address(token0), + fee: 3000, + tickSpacing: 60, + hooks: address(0) + }); + assertEq(harness.poolId(), keccak256(abi.encode(key))); + } + + function testPoolStateBaseSlotMatchesStateLibrary() external view { + // base = keccak256(abi.encode(poolId, POOLS_SLOT)) where POOLS_SLOT = 6. + bytes32 expected = keccak256(abi.encode(harness.poolId(), uint256(6))); + assertEq(harness.poolStateBaseSlot(), expected); + } + + function testRejectsMisorderedCurrencies() external { + IUniswapV4PoolManagerLike.PoolKey memory key = IUniswapV4PoolManagerLike.PoolKey({ + currency0: address(0xFFFF), currency1: address(0x1111), fee: 3000, tickSpacing: 60, hooks: address(0) + }); + vm.expectRevert(bytes("UniswapV4Pool: currencies misordered")); + new UniswapV4PoolManagerAssertionHarness(manager, key); + } + + function testRejectsZeroManager() external { + IUniswapV4PoolManagerLike.PoolKey memory key = IUniswapV4PoolManagerLike.PoolKey({ + currency0: address(0x1111), currency1: address(0xFFFF), fee: 3000, tickSpacing: 60, hooks: address(0) + }); + vm.expectRevert(bytes("UniswapV4Pool: manager zero")); + new UniswapV4PoolManagerAssertionHarness(address(0), key); + } + + function testAcceptsNativeCurrencyPool() external { + IUniswapV4PoolManagerLike.PoolKey memory key = IUniswapV4PoolManagerLike.PoolKey({ + currency0: address(0), currency1: address(token0), fee: 3000, tickSpacing: 60, hooks: address(0) + }); + + UniswapV4PoolManagerAssertionHarness nativeHarness = new UniswapV4PoolManagerAssertionHarness(manager, key); + + assertEq(nativeHarness.poolId(), keccak256(abi.encode(key))); + assertTrue(nativeHarness.isNativeCurrency(address(0))); + assertFalse(nativeHarness.isNativeCurrency(address(token0))); + } +}