[Ethena ARM] - Invariant Testing

src/contracts/Interfaces.sol

@@ -357,4 +357,10 @@ interface IStakedUSDe is IERC4626 {
     function unstake(address receiver) external;
 
     function cooldowns(address receiver) external view returns (UserCooldown memory);
+
+    function getUnvestedAmount() external view returns (uint256);
+
+    function lastDistributionTimestamp() external view returns (uint256);
+
+    function transferInRewards(uint256 amount) external;
 }

test/invariants/EthenaARM/Base.sol

@@ -0,0 +1,104 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Contracts
+import {Proxy} from "contracts/Proxy.sol";
+import {EthenaARM} from "contracts/EthenaARM.sol";
+import {MockMorpho} from "test/invariants/EthenaARM/mocks/MockMorpho.sol";
+import {MorphoMarket} from "src/contracts/markets/MorphoMarket.sol";
+import {EthenaUnstaker} from "contracts/EthenaUnstaker.sol";
+
+// Interfaces
+import {IERC20} from "contracts/Interfaces.sol";
+import {IStakedUSDe} from "contracts/Interfaces.sol";
+
+// Tests
+import {Vm} from "./helpers/Vm.sol";
+
+/// @notice This contract should be the common parent for all test contracts.
+///         It should be used to define common variables and that will be
+///         used across all test contracts. This pattern is used to allow different
+///         test contracts to share common variables, and ensure a consistent setup.
+/// @dev This contract should be inherited by "Shared" contracts.
+/// @dev This contract should only be used as storage for common variables.
+/// @dev Helpers and other functions should be defined in a separate contract.
+abstract contract Base_Test_ {
+    //////////////////////////////////////////////////////
+    /// --- CONTRACTS
+    //////////////////////////////////////////////////////
+    // --- Main contracts ---
+    Proxy public armProxy;
+    Proxy public morphoMarketProxy;
+    EthenaARM public arm;
+    MockMorpho public morpho;
+    MorphoMarket public market;
+    EthenaUnstaker[] public unstakers;
+    uint256[] public unstakerIndices;
+
+    // --- Tokens ---
+    IERC20 public usde;
+    IStakedUSDe public susde;
+
+    // --- Utils ---
+    Vm public vm = Vm(address(uint160(uint256(keccak256("hevm cheat code")))));
+
+    //////////////////////////////////////////////////////
+    /// --- USERS
+    //////////////////////////////////////////////////////
+    // --- Users with roles ---
+    address public deployer;
+    address public governor;
+    address public operator;
+    address public treasury;
+
+    // --- Regular users ---
+    address public alice;
+    address public bobby;
+    address public carol;
+    address public david;
+    address public elise;
+    address public frank;
+    address public grace;
+    address public harry;
+    address public dead;
+
+    // --- Group of users ---
+    address[] public makers;
+    address[] public traders;
+    mapping(address => uint256[]) public pendingRequests;
+
+    //////////////////////////////////////////////////////
+    /// --- DEFAULT VALUES
+    //////////////////////////////////////////////////////
+    uint256 public constant MAKERS_COUNT = 3;
+    uint256 public constant TRADERS_COUNT = 3;
+    uint256 public constant UNSTAKERS_COUNT = 42;
+    uint256 public constant DEFAULT_CLAIM_DELAY = 10 minutes;
+    uint256 public constant DEFAULT_MIN_TOTAL_SUPPLY = 1e12;
+    uint256 public constant DEFAULT_ALLOCATE_THRESHOLD = 1e18;
+    uint256 public constant DEFAULT_MIN_SHARES_TO_REDEEM = 1e7;
+
+    /// @notice Indicates if labels have been set in the Vm.
+    function isLabelAvailable() external view virtual returns (bool);
+    function isAssumeAvailable() external view virtual returns (bool);
+    function isConsoleAvailable() external view virtual returns (bool);
+
+    //////////////////////////////////////////////////////
+    /// --- GHOST VALUES
+    //////////////////////////////////////////////////////
+    // --- USDe values ---
+    uint256 public sumUSDeSwapIn;
+    uint256 public sumUSDeSwapOut;
+    uint256 public sumUSDeUserDeposit;
+    uint256 public sumUSDeUserRedeem;
+    uint256 public sumUSDeUserRequest;
+    uint256 public sumUSDeBaseRedeem;
+    uint256 public sumUSDeFeesCollected;
+    uint256 public sumUSDeMarketDeposit;
+    uint256 public sumUSDeMarketWithdraw;
+    // --- sUSDe values ---
+    uint256 public sumSUSDeSwapIn;
+    uint256 public sumSUSDeSwapOut;
+    uint256 public sumSUSDeBaseRedeem;
+}
+

test/invariants/EthenaARM/FoundryFuzzer.sol

@@ -0,0 +1,77 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Test imports
+import {Properties} from "./Properties.sol";
+import {StdInvariant} from "forge-std/StdInvariant.sol";
+import {StdAssertions} from "forge-std/StdAssertions.sol";
+
+/// @title FuzzerFoundry
+/// @notice Concrete fuzzing contract implementing Foundry's invariant testing framework.
+/// @dev    This contract configures and executes property-based testing:
+///         - Inherits from Properties to access handler functions and properties
+///         - Configures fuzzer targeting (contracts, selectors, senders)
+///         - Implements invariant test functions that call property validators
+///         - Each invariant function represents a critical system property to maintain
+///         - Fuzzer will call targeted handlers randomly and check invariants after each call
+contract FuzzerFoundry_EthenaARM is Properties, StdInvariant, StdAssertions {
+    bool public constant override isLabelAvailable = true;
+    bool public constant override isAssumeAvailable = true;
+    bool public constant override isConsoleAvailable = true;
+
+    //////////////////////////////////////////////////////
+    /// --- SETUP
+    //////////////////////////////////////////////////////
+    function setUp() public override {
+        super.setUp();
+
+        // --- Setup Fuzzer target ---
+        // Setup target
+        targetContract(address(this));
+
+        // Add selectors
+        bytes4[] memory selectors = new bytes4[](22);
+        // --- sUSDe ---
+        selectors[0] = this.targetSUSDeDeposit.selector;
+        selectors[1] = this.targetSUSDeCooldownShares.selector;
+        selectors[2] = this.targetSUSDeUnstake.selector;
+        selectors[3] = this.targetSUSDeTransferInRewards.selector;
+        // --- Morpho ---
+        selectors[4] = this.targetMorphoDeposit.selector;
+        selectors[5] = this.targetMorphoWithdraw.selector;
+        selectors[6] = this.targetMorphoTransferInRewards.selector;
+        selectors[7] = this.targetMorphoSetUtilizationRate.selector;
+        // --- ARM ---
+        selectors[8] = this.targetARMDeposit.selector;
+        selectors[9] = this.targetARMRequestRedeem.selector;
+        selectors[10] = this.targetARMClaimRedeem.selector;
+        selectors[11] = this.targetARMSetARMBuffer.selector;
+        selectors[12] = this.targetARMSetActiveMarket.selector;
+        selectors[13] = this.targetARMAllocate.selector;
+        selectors[14] = this.targetARMSetPrices.selector;
+        selectors[15] = this.targetARMSetCrossPrice.selector;
+        selectors[16] = this.targetARMSwapExactTokensForTokens.selector;
+        selectors[17] = this.targetARMSwapTokensForExactTokens.selector;
+        selectors[18] = this.targetARMCollectFees.selector;
+        selectors[19] = this.targetARMSetFees.selector;
+        selectors[20] = this.targetARMRequestBaseWithdrawal.selector;
+        selectors[21] = this.targetARMClaimBaseWithdrawals.selector;
+        // Target selectors
+        targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- INVARIANTS
+    //////////////////////////////////////////////////////
+    function invariantA() public view {
+        assertTrue(propertyA(), "Property A failed");
+        assertTrue(propertyB(), "Property B failed");
+        assertTrue(propertyC(), "Property C failed");
+        assertTrue(propertyD(), "Property D failed");
+        assertTrue(propertyE(), "Property E failed");
+        assertTrue(propertyF(), "Property F failed");
+        assertTrue(propertyG(), "Property G failed");
+        assertTrue(propertyH(), "Property H failed");
+        assertTrue(propertyI(), "Property I failed");
+    }
+}

test/invariants/EthenaARM/Properties.sol

@@ -0,0 +1,138 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Foundry
+import {console} from "forge-std/console.sol";
+
+// Test imports
+import {TargetFunctions} from "./TargetFunctions.sol";
+
+// Helpers
+import {Math} from "./helpers/Math.sol";
+
+/// @title Properties
+/// @notice Abstract contract defining invariant properties for formal verification and fuzzing.
+/// @dev    This contract contains pure property functions that express system invariants:
+///         - Properties must be implemented as view/pure functions returning bool
+///         - Each property should represent a mathematical invariant of the system
+///         - Properties should be stateless and deterministic
+///         - Property names should clearly indicate what invariant they check
+///         Usage: Properties are called by fuzzing contracts to validate system state
+abstract contract Properties is TargetFunctions {
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                           ✦✦✦ SWAP PROPERTIES ✦✦✦                            ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    // [ ] Invariant A: USDe  balance == ∑swapIn - ∑swapOut
+    //                                   + ∑userDeposit - ∑userWithdraw
+    //                                   + ∑marketWithdraw - ∑marketDeposit
+    //                                   + ∑baseRedeem - ∑feesCollected
+    // [ ] Invariant B: sUSDe balance == (∑swapIn - ∑swapOut) - ∑baseRedeem
+    //
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                            ✦✦✦ LP PROPERTIES ✦✦✦                             ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    // [x] Invariant C: ∑shares > 0 due to initial deposit
+    // [x] Invariant D: totalShares == ∑userShares + deadShares
+    // [x] Invariant E: previewRedeem(∑shares) == totalAssets
+    // [x] Invariant F: withdrawsQueued == ∑requestRedeem.amount
+    // [x] Invariant G: withdrawsQueued > withdrawsClaimed
+    // [x] Invariant H: withdrawsQueued == ∑request.assets
+    // [x] Invariant I: withdrawsClaimed == ∑claimRedeem.amount
+    // [x] Invariant J: ∀ requestId, request.queued >= request.assets
+    // [x] Invariant K: ∑feesCollected == feeCollector.balance
+
+    function propertyA() public view returns (bool) {
+        uint256 usdeBalance = usde.balanceOf(address(arm));
+        uint256 inflow = 1e12 + sumUSDeSwapIn + sumUSDeUserDeposit + sumUSDeMarketWithdraw + sumUSDeBaseRedeem;
+        uint256 outflow = sumUSDeSwapOut + sumUSDeUserRedeem + sumUSDeMarketDeposit + sumUSDeFeesCollected;
+        // console.log(">>> Property A:");
+        // console.log("    - USDe balance:         %18e", usdeBalance);
+        // console.log("    - Inflow breakdown:");
+        // console.log("        o Initial buffer:   %18e", uint256(1e12));
+        // console.log("        o Swap In:          %18e", sumUSDeSwapIn);
+        // console.log("        o User Deposit:     %18e", sumUSDeUserDeposit);
+        // console.log("        o Market Withdraw:  %18e", sumUSDeMarketWithdraw);
+        // console.log("        o Base Redeem:      %18e", sumUSDeBaseRedeem);
+        // console.log("    - USDe inflow sum:      %18e", inflow);
+        // console.log("    - Outflow breakdown:");
+        // console.log("        o Swap Out:         %18e", sumUSDeSwapOut);
+        // console.log("        o User Redeem:      %18e", sumUSDeUserRedeem);
+        // console.log("        o Market Deposit:   %18e", sumUSDeMarketDeposit);
+        // console.log("        o Fees Collected:   %18e", sumUSDeFeesCollected);
+        // console.log("    - USDe outflow sum:     %18e", outflow);
+        // console.log("    - Diff:                 %18e", Math.absDiff(inflow, outflow));
+        return Math.eq(usdeBalance, Math.absDiff(inflow, outflow));
+    }
+
+    function propertyB() public view returns (bool) {
+        uint256 susdeBalance = susde.balanceOf(address(arm));
+        uint256 inflow = sumSUSDeSwapIn;
+        uint256 outflow = sumSUSDeSwapOut + sumSUSDeBaseRedeem;
+        // console.log(">>> Property B:");
+        // console.log("    - sUSDe balance:        %18e", susdeBalance);
+        // console.log("    - Inflow breakdown:");
+        // console.log("        o Swap In:          %18e", sumSUSDeSwapIn);
+        // console.log("    - sUSDe inflow sum:     %18e", inflow);
+        // console.log("    - Outflow breakdown:");
+        // console.log("        o Swap Out:         %18e", sumSUSDeSwapOut);
+        // console.log("        o Base Redeem:      %18e", sumSUSDeBaseRedeem);
+        // console.log("    - sUSDe outflow sum:    %18e", outflow);
+        // console.log("    - Diff:                 %18e", Math.absDiff(inflow, outflow));
+        return Math.eq(susdeBalance, Math.absDiff(inflow, outflow));
+    }
+
+    function propertyC() public view returns (bool) {
+        return Math.gt(arm.totalSupply(), 0);
+    }
+
+    function propertyD() public view returns (bool) {
+        uint256 totalUserShares = 0;
+        for (uint256 i = 0; i < MAKERS_COUNT; i++) {
+            totalUserShares += arm.balanceOf(makers[i]);
+        }
+        uint256 deadShares = 1e12;
+        return Math.eq(arm.totalSupply(), totalUserShares + deadShares);
+    }
+
+    function propertyE() public view returns (bool) {
+        return Math.eq(arm.previewRedeem(arm.totalSupply()), arm.totalAssets());
+    }
+
+    function propertyF() public view returns (bool) {
+        return Math.eq(arm.withdrawsQueued(), sumUSDeUserRequest);
+    }
+
+    function propertyG() public view returns (bool) {
+        return Math.gte(arm.withdrawsQueued(), arm.withdrawsClaimed());
+    }
+
+    function propertyH() public view returns (bool) {
+        uint256 sum = 0;
+        uint256 len = arm.nextWithdrawalIndex();
+        for (uint256 i; i < len; i++) {
+            (,,, uint128 amount,) = arm.withdrawalRequests(i);
+            sum += amount;
+        }
+        return Math.eq(arm.withdrawsQueued(), sum);
+    }
+
+    function propertyI() public view returns (bool) {
+        return Math.eq(arm.withdrawsClaimed(), sumUSDeUserRedeem);
+    }
+
+    function propertyJ() public view returns (bool) {
+        uint256 len = arm.nextWithdrawalIndex();
+        for (uint256 i; i < len; i++) {
+            (,,, uint128 amount, uint128 queued) = arm.withdrawalRequests(i);
+            if (queued < amount) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    function propertyK() public view returns (bool) {
+        uint256 feeCollectorBalance = usde.balanceOf(treasury);
+        return Math.eq(sumUSDeFeesCollected, feeCollectorBalance);
+    }
+}