From f8f348d25d79cdffe0d74a0010720ca7733dd78a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Mon, 17 Nov 2025 17:44:50 +0100
Subject: [PATCH 01/28] Add mock for sUSDe contract.

---
 test/invariants/EthenaARM/mocks/MockSUSDE.sol | 145 ++++++++++++++++++
 1 file changed, 145 insertions(+)
 create mode 100644 test/invariants/EthenaARM/mocks/MockSUSDE.sol

diff --git a/test/invariants/EthenaARM/mocks/MockSUSDE.sol b/test/invariants/EthenaARM/mocks/MockSUSDE.sol
new file mode 100644
index 00000000..b768ab01
--- /dev/null
+++ b/test/invariants/EthenaARM/mocks/MockSUSDE.sol
@@ -0,0 +1,145 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Solmate
+import {Owned} from "@solmate/auth/Owned.sol";
+import {ERC20} from "@solmate/tokens/ERC20.sol";
+import {ERC4626} from "@solmate/mixins/ERC4626.sol";
+
+// Interfaces
+import {UserCooldown} from "contracts/Interfaces.sol";
+
+contract MockSUSDE is ERC4626, Owned {
+    //////////////////////////////////////////////////////
+    /// --- CONSTANTS & IMMUTABLES
+    //////////////////////////////////////////////////////
+    address public immutable SILO;
+    uint256 public immutable VESTING_DURATION;
+
+    //////////////////////////////////////////////////////
+    /// --- STATE VARIABLES
+    //////////////////////////////////////////////////////
+    uint256 public vestingAmount;
+    uint256 public lastDistribution;
+    uint256 public cooldownDuration;
+    mapping(address => UserCooldown) public cooldowns;
+
+    //////////////////////////////////////////////////////
+    /// --- EVENTS
+    //////////////////////////////////////////////////////
+    event CooldownSet(uint256 oldDuration, uint256 newDuration);
+    event RewardReceived(uint256 amount);
+
+    //////////////////////////////////////////////////////
+    /// --- CONSTRUCTOR
+    //////////////////////////////////////////////////////
+    constructor(address _underlying, address _governor)
+        ERC4626(ERC20(_underlying), "Staked USDe", "sUSDe")
+        Owned(_governor)
+    {
+        SILO = address(new MockSilo(asset));
+        VESTING_DURATION = 8 hours;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- VIEWS
+    //////////////////////////////////////////////////////
+    function totalAssets() public view override returns (uint256) {
+        return asset.balanceOf(address(this)) - getUnvestedAmount();
+    }
+
+    function getUnvestedAmount() public view returns (uint256) {
+        uint256 timeSinceLastDistribution = block.timestamp - lastDistribution;
+
+        if (timeSinceLastDistribution >= VESTING_DURATION) {
+            return 0;
+        }
+
+        uint256 deltaT;
+        unchecked {
+            deltaT = VESTING_DURATION - timeSinceLastDistribution;
+        }
+        return (vestingAmount * deltaT) / VESTING_DURATION;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- MUTATIVE FUNCTIONS
+    //////////////////////////////////////////////////////
+    function unstake(address receiver) external {
+        UserCooldown storage cooldown = cooldowns[msg.sender];
+        uint256 assets = cooldown.underlyingAmount;
+
+        if (block.timestamp >= cooldown.cooldownEnd) {
+            delete cooldowns[msg.sender];
+
+            MockSilo(SILO).withdraw(receiver, assets);
+        } else {
+            revert("SUSDE: Invalid cooldown");
+        }
+    }
+
+    function cooldownAssets(uint256 assets) external returns (uint256 shares) {
+        if (assets > maxWithdraw(msg.sender)) revert("SUSDE: Excessive withdraw amount");
+
+        shares = previewWithdraw(assets);
+
+        cooldowns[msg.sender].cooldownEnd = uint104(block.timestamp + cooldownDuration);
+        cooldowns[msg.sender].underlyingAmount += uint152(assets);
+
+        withdraw(assets, SILO, msg.sender);
+    }
+
+    function cooldownShares(uint256 shares) external returns (uint256 assets) {
+        if (shares > maxRedeem(msg.sender)) revert("SUSDE: Excessive redeem amount");
+
+        assets = previewRedeem(shares);
+
+        cooldowns[msg.sender].cooldownEnd = uint104(block.timestamp + cooldownDuration);
+        cooldowns[msg.sender].underlyingAmount += uint152(assets);
+
+        withdraw(assets, SILO, msg.sender);
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- ADMIN FUNCTIONS
+    //////////////////////////////////////////////////////
+    function setCooldownDuration(uint256 _cooldownDuration) external onlyOwner {
+        require(_cooldownDuration <= 30 days, "SUSDE: cooldown too long");
+        emit CooldownSet(cooldownDuration, _cooldownDuration);
+        cooldownDuration = _cooldownDuration;
+    }
+
+    function transferInRewards(uint256 amount) external onlyOwner {
+        require(amount != 0, "SUSDE: amount zero");
+
+        // Ensure previous vesting period is complete before starting a new one
+        // _updateVestingAmount(amount) in original contract
+        require(getUnvestedAmount() == 0, "SUSDE: previous vesting not complete");
+        vestingAmount += amount;
+        lastDistribution = block.timestamp;
+
+        asset.transferFrom(msg.sender, address(this), amount);
+        emit RewardReceived(amount);
+    }
+}
+
+contract MockSilo is Owned {
+    //////////////////////////////////////////////////////
+    /// --- IMMUTABLES
+    //////////////////////////////////////////////////////
+    ERC20 public immutable _USDE;
+
+    /////////////////////////////////////////////////////
+    /// --- CONSTRUCTOR
+    //////////////////////////////////////////////////////
+    constructor(ERC20 _usde) Owned(msg.sender) {
+        _USDE = _usde;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- MUTATIVE FUNCTIONS
+    //////////////////////////////////////////////////////
+    function withdraw(address to, uint256 amount) external onlyOwner {
+        _USDE.transfer(to, amount);
+    }
+}

From 5144d32785c5c3eeaf7f8835ad12fb70a57c4ae7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Mon, 17 Nov 2025 17:45:02 +0100
Subject: [PATCH 02/28] Add Medusa VM interface.

---
 test/invariants/EthenaARM/helpers/Vm.sol | 93 ++++++++++++++++++++++++
 1 file changed, 93 insertions(+)
 create mode 100644 test/invariants/EthenaARM/helpers/Vm.sol

diff --git a/test/invariants/EthenaARM/helpers/Vm.sol b/test/invariants/EthenaARM/helpers/Vm.sol
new file mode 100644
index 00000000..fc29d5f5
--- /dev/null
+++ b/test/invariants/EthenaARM/helpers/Vm.sol
@@ -0,0 +1,93 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.23;
+
+/// @notice Medusa StdCheats interface
+interface Vm {
+    // Set block.timestamp
+    function warp(uint256) external;
+
+    // Set block.number
+    function roll(uint256) external;
+
+    // Set block.basefee
+    function fee(uint256) external;
+
+    // Set block.difficulty (deprecated in `medusa`)
+    function difficulty(uint256) external;
+
+    // Set block.prevrandao
+    function prevrandao(bytes32) external;
+
+    // Set block.chainid
+    function chainId(uint256) external;
+
+    // Sets the block.coinbase
+    function coinbase(address) external;
+
+    // Loads a storage slot from an address
+    function load(address account, bytes32 slot) external returns (bytes32);
+
+    // Stores a value to an address' storage slot
+    function store(address account, bytes32 slot, bytes32 value) external;
+
+    // Sets the *next* call's msg.sender to be the input address
+    function prank(address) external;
+
+    // Sets all subsequent call's msg.sender (until stopPrank is called) to be the input address
+    function startPrank(address) external;
+
+    // Stops a previously called startPrank
+    function stopPrank() external;
+
+    // Set msg.sender to the input address until the current call exits
+    function prankHere(address) external;
+
+    // Sets an address' balance
+    function deal(address who, uint256 newBalance) external;
+
+    // Sets an address' code
+    function etch(address who, bytes calldata code) external;
+
+    // Signs data
+    function sign(uint256 privateKey, bytes32 digest) external returns (uint8 v, bytes32 r, bytes32 s);
+
+    // Computes address for a given private key
+    function addr(uint256 privateKey) external returns (address);
+
+    // Gets the creation bytecode of a contract
+    function getCode(string calldata) external returns (bytes memory);
+
+    // Gets the nonce of an account
+    function getNonce(address account) external returns (uint64);
+
+    // Sets the nonce of an account
+    // The new nonce must be higher than the current nonce of the account
+    function setNonce(address account, uint64 nonce) external;
+
+    // Performs a foreign function call via terminal
+    function ffi(string[] calldata) external returns (bytes memory);
+
+    // Take a snapshot of the current state of the EVM
+    function snapshot() external returns (uint256);
+
+    // Revert state back to a snapshot
+    function revertTo(uint256) external returns (bool);
+
+    // Convert Solidity types to strings
+    function toString(address) external returns (string memory);
+    function toString(bytes calldata) external returns (string memory);
+    function toString(bytes32) external returns (string memory);
+    function toString(bool) external returns (string memory);
+    function toString(uint256) external returns (string memory);
+    function toString(int256) external returns (string memory);
+
+    // Convert strings into Solidity types
+    function parseBytes(string memory) external returns (bytes memory);
+    function parseBytes32(string memory) external returns (bytes32);
+    function parseAddress(string memory) external returns (address);
+    function parseUint(string memory) external returns (uint256);
+    function parseInt(string memory) external returns (int256);
+    function parseBool(string memory) external returns (bool);
+
+    function label(address account, string calldata newLabel) external;
+}

From e94d1f64088ea67bdc9d1ef9cdb53d7941a4a0c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Mon, 17 Nov 2025 17:45:11 +0100
Subject: [PATCH 03/28] Add base contracts and setup for EthenaARM invariant
 tests

---
 test/invariants/EthenaARM/Base.sol            |  76 +++++++
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  19 ++
 test/invariants/EthenaARM/Properties.sol      |  15 ++
 test/invariants/EthenaARM/Setup.sol           | 194 ++++++++++++++++++
 test/invariants/EthenaARM/TargetFunctions.sol |  10 +
 5 files changed, 314 insertions(+)
 create mode 100644 test/invariants/EthenaARM/Base.sol
 create mode 100644 test/invariants/EthenaARM/FoundryFuzzer.sol
 create mode 100644 test/invariants/EthenaARM/Properties.sol
 create mode 100644 test/invariants/EthenaARM/Setup.sol
 create mode 100644 test/invariants/EthenaARM/TargetFunctions.sol

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
new file mode 100644
index 00000000..96ec575a
--- /dev/null
+++ b/test/invariants/EthenaARM/Base.sol
@@ -0,0 +1,76 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Contracts
+import {Proxy} from "contracts/Proxy.sol";
+import {EthenaARM} from "contracts/EthenaARM.sol";
+import {MorphoMarket} from "src/contracts/markets/MorphoMarket.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;
+    address public morpho;
+    EthenaARM public arm;
+    MorphoMarket public market;
+
+    // --- 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 dead;
+
+    // --- Group of users ---
+    address[] public makers;
+    address[] public traders;
+
+    //////////////////////////////////////////////////////
+    /// --- DEFAULT VALUES
+    //////////////////////////////////////////////////////
+    uint256 public constant MAKERS_COUNT = 3;
+    uint256 public constant TRADERS_COUNT = 3;
+    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);
+}
+
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
new file mode 100644
index 00000000..a86c9103
--- /dev/null
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Test imports
+import {Properties} from "./Properties.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 {
+    bool public constant override isLabelAvailable = true;
+
+    function test() public {}
+}
diff --git a/test/invariants/EthenaARM/Properties.sol b/test/invariants/EthenaARM/Properties.sol
new file mode 100644
index 00000000..84d39122
--- /dev/null
+++ b/test/invariants/EthenaARM/Properties.sol
@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Test imports
+import {TargetFunctions} from "./TargetFunctions.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 {}
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
new file mode 100644
index 00000000..4732c74e
--- /dev/null
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -0,0 +1,194 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Test imports
+import {Base_Test_} from "./Base.sol";
+
+// Contracts
+import {Proxy} from "contracts/Proxy.sol";
+import {EthenaARM} from "contracts/EthenaARM.sol";
+import {MorphoMarket} from "src/contracts/markets/MorphoMarket.sol";
+import {Abstract4626MarketWrapper} from "contracts/markets/Abstract4626MarketWrapper.sol";
+
+// Mocks
+import {ERC20} from "@solmate/tokens/ERC20.sol";
+import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
+import {MockSUSDE} from "test/invariants/EthenaARM/mocks/MockSUSDE.sol";
+import {MockERC4626} from "@solmate/test/utils/mocks/MockERC4626.sol";
+
+// Interfaces
+import {IERC20} from "contracts/Interfaces.sol";
+import {IStakedUSDe} from "contracts/Interfaces.sol";
+
+/// @notice Shared invariant test contract.
+/// @dev This contract should be used for deploying all contracts and mocks needed for the test.
+abstract contract Setup is Base_Test_ {
+    //////////////////////////////////////////////////////
+    /// --- SETUP
+    //////////////////////////////////////////////////////
+    function setUp() public virtual {
+        // 1. Setup a realistic test environnement.
+        _setUpRealisticEnvironnement();
+
+        // 2. Create user.
+        _createUsers();
+
+        // 3. Deploy mocks.
+        _deployMocks();
+
+        // 4. Deploy contracts.
+        _deployContracts();
+
+        // 5. Label addresses
+        _labelAll();
+
+        // 6. Ignite contracts
+        _ignite();
+    }
+
+    function _setUpRealisticEnvironnement() internal virtual {
+        vm.warp(1_800_000_000); // Warp to a future timestamp
+        vm.roll(24_000_000); // Warp to a future block number
+    }
+
+    function _createUsers() internal virtual {
+        // --- Users with roles ---
+        deployer = generateAddr("deployer");
+        governor = generateAddr("governor");
+        operator = generateAddr("operator");
+        treasury = generateAddr("treasury");
+
+        // --- Regular users ---
+        alice = generateAddr("alice");
+        bobby = generateAddr("bobby");
+        carol = generateAddr("carol");
+        david = generateAddr("david");
+        elise = generateAddr("elise");
+        frank = generateAddr("frank");
+        dead = generateAddr("dead");
+
+        // --- Group of users ---
+        makers = new address[](MAKERS_COUNT);
+        makers[0] = alice;
+        makers[1] = bobby;
+        makers[2] = carol;
+
+        traders = new address[](TRADERS_COUNT);
+        traders[0] = david;
+        traders[1] = elise;
+        traders[2] = frank;
+    }
+
+    function _deployMocks() internal virtual {
+        // Deploy mock USDe.
+        usde = IERC20(address(new MockERC20("USDe", "USDe", 18)));
+
+        // Deploy mock sUSDe.
+        susde = IStakedUSDe(address(new MockSUSDE(address(usde), governor)));
+
+        // Deploy mock Morpho Market.
+        morpho = address(new MockERC4626(ERC20(address(usde)), "Morpho USDe Market", "morpho-USDe"));
+    }
+
+    function _deployContracts() internal virtual {
+        vm.startPrank(deployer);
+
+        // Deploy Ethena ARM proxy.
+        armProxy = new Proxy();
+
+        // Deploy Ethena ARM implementation.
+        arm = new EthenaARM({
+            _usde: address(usde),
+            _susde: address(susde),
+            _claimDelay: DEFAULT_CLAIM_DELAY,
+            _minSharesToRedeem: DEFAULT_MIN_SHARES_TO_REDEEM,
+            _allocateThreshold: int256(DEFAULT_ALLOCATE_THRESHOLD)
+        });
+
+        // Initialization requires to transfer some USDe to the proxy from the deployer.
+        MockERC20(address(usde)).mint(deployer, DEFAULT_MIN_TOTAL_SUPPLY);
+        usde.approve(address(armProxy), DEFAULT_MIN_TOTAL_SUPPLY);
+
+        // Initialize Ethena ARM proxy.
+        bytes memory data = abi.encodeWithSelector(
+            EthenaARM.initialize.selector,
+            "Ethena ARM",
+            "ARM-USDe-sUSDe",
+            operator,
+            2000, // 20% performance fee
+            treasury,
+            address(0) // CapManager address
+        );
+        armProxy.initialize(address(arm), governor, data);
+
+        // Cast proxy address to EthenaARM type for easier interaction.
+        arm = EthenaARM(address(armProxy));
+
+        // Deploy Morpho Market Proxy.
+        morphoMarketProxy = new Proxy();
+
+        // Deploy Morpho Market implementation.
+        market = new MorphoMarket(address(arm), morpho);
+
+        // Initialize Morpho Market proxy.
+        data = abi.encodeWithSelector(Abstract4626MarketWrapper.initialize.selector, address(0x1), address(0x1));
+        morphoMarketProxy.initialize(address(market), governor, data);
+
+        // Cast proxy address to MorphoMarket type for easier interaction.
+        market = MorphoMarket(address(morphoMarketProxy));
+
+        vm.stopPrank();
+    }
+
+    function _labelAll() internal virtual {
+        // This only works with Foundry's Vm.label feature.
+        if (!this.isLabelAvailable()) return;
+
+        // --- Proxies ---
+        vm.label(address(armProxy), "Proxy EthenaARM");
+        vm.label(address(morphoMarketProxy), "Proxy MorphoMarket");
+
+        // --- Implementations ---
+        vm.label(address(arm), "Ethena ARM");
+        vm.label(address(market), "Morpho Market");
+        vm.label(address(morpho), "Morpho Blue");
+
+        // --- Tokens ---
+        vm.label(address(usde), "USDe");
+        vm.label(address(susde), "sUSDe");
+
+        // --- Users with roles ---
+        vm.label(deployer, "Deployer");
+        vm.label(governor, "Governor");
+        vm.label(operator, "Operator");
+        vm.label(treasury, "Treasury");
+
+        // --- Regular users ---
+        vm.label(alice, "Alice");
+        vm.label(bobby, "Bobby");
+        vm.label(carol, "Carol");
+        vm.label(david, "David");
+        vm.label(elise, "Elise");
+        vm.label(frank, "Frank");
+        vm.label(dead, "Dead");
+    }
+
+    function _ignite() internal virtual {
+        // As sUSDe is an ERC4626, we want to avoid small total supply issues.
+        // So we mint some sUSDe to the dead address, to replicate a realistic scenario.
+        MockERC20(address(usde)).mint(address(dead), 2_000_000 ether);
+
+        vm.startPrank(dead);
+        usde.approve(address(susde), 1_000_000 ether);
+        susde.deposit(1_000_000 ether, dead);
+
+        // Same for morpho contract.
+        usde.approve(morpho, 1_000_000 ether);
+        MockERC4626(morpho).deposit(1_000_000 ether, dead);
+        vm.stopPrank();
+    }
+
+    function generateAddr(string memory name) internal returns (address) {
+        return vm.addr(uint256(keccak256(abi.encodePacked(name))));
+    }
+}
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
new file mode 100644
index 00000000..71f84532
--- /dev/null
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Test imports
+import {Setup} from "./Setup.sol";
+
+/// @title TargetFunctions
+/// @notice TargetFunctions contract for tests, containing the target functions that should be tested.
+///         This is the entry point with the contract we are testing. Ideally, it should never revert.
+abstract contract TargetFunctions is Setup {}

From 4b28780cc8dd03b84470c6b748efde0f60514124 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 09:10:54 +0100
Subject: [PATCH 04/28] Simplify MockSUSDE

---
 test/invariants/EthenaARM/mocks/MockSUSDE.sol | 25 +++++++++++--------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/test/invariants/EthenaARM/mocks/MockSUSDE.sol b/test/invariants/EthenaARM/mocks/MockSUSDE.sol
index b768ab01..d849674e 100644
--- a/test/invariants/EthenaARM/mocks/MockSUSDE.sol
+++ b/test/invariants/EthenaARM/mocks/MockSUSDE.sol
@@ -15,13 +15,13 @@ contract MockSUSDE is ERC4626, Owned {
     //////////////////////////////////////////////////////
     address public immutable SILO;
     uint256 public immutable VESTING_DURATION;
+    uint256 public immutable COOLDOWN_DURATION;
 
     //////////////////////////////////////////////////////
     /// --- STATE VARIABLES
     //////////////////////////////////////////////////////
     uint256 public vestingAmount;
     uint256 public lastDistribution;
-    uint256 public cooldownDuration;
     mapping(address => UserCooldown) public cooldowns;
 
     //////////////////////////////////////////////////////
@@ -39,6 +39,7 @@ contract MockSUSDE is ERC4626, Owned {
     {
         SILO = address(new MockSilo(asset));
         VESTING_DURATION = 8 hours;
+        COOLDOWN_DURATION = 7 days;
     }
 
     //////////////////////////////////////////////////////
@@ -83,10 +84,10 @@ contract MockSUSDE is ERC4626, Owned {
 
         shares = previewWithdraw(assets);
 
-        cooldowns[msg.sender].cooldownEnd = uint104(block.timestamp + cooldownDuration);
+        cooldowns[msg.sender].cooldownEnd = uint104(block.timestamp + COOLDOWN_DURATION);
         cooldowns[msg.sender].underlyingAmount += uint152(assets);
 
-        withdraw(assets, SILO, msg.sender);
+        super.withdraw(assets, SILO, msg.sender);
     }
 
     function cooldownShares(uint256 shares) external returns (uint256 assets) {
@@ -94,21 +95,23 @@ contract MockSUSDE is ERC4626, Owned {
 
         assets = previewRedeem(shares);
 
-        cooldowns[msg.sender].cooldownEnd = uint104(block.timestamp + cooldownDuration);
+        cooldowns[msg.sender].cooldownEnd = uint104(block.timestamp + COOLDOWN_DURATION);
         cooldowns[msg.sender].underlyingAmount += uint152(assets);
 
-        withdraw(assets, SILO, msg.sender);
+        super.withdraw(assets, SILO, msg.sender);
+    }
+
+    function withdraw(uint256, address, address) public pure override returns (uint256) {
+        revert("SUSDE: Use cooldown functions");
+    }
+
+    function redeem(uint256, address, address) public pure override returns (uint256) {
+        revert("SUSDE: Use cooldown functions");
     }
 
     //////////////////////////////////////////////////////
     /// --- ADMIN FUNCTIONS
     //////////////////////////////////////////////////////
-    function setCooldownDuration(uint256 _cooldownDuration) external onlyOwner {
-        require(_cooldownDuration <= 30 days, "SUSDE: cooldown too long");
-        emit CooldownSet(cooldownDuration, _cooldownDuration);
-        cooldownDuration = _cooldownDuration;
-    }
-
     function transferInRewards(uint256 amount) external onlyOwner {
         require(amount != 0, "SUSDE: amount zero");
 

From 5ff7e4139a5df8d15580823d2f5fc8dcd1b7b78e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 09:11:43 +0100
Subject: [PATCH 05/28] Add unstakers

---
 test/invariants/EthenaARM/Base.sol  |  8 ++-
 test/invariants/EthenaARM/Setup.sol | 80 +++++++++++++++++++++++++++--
 2 files changed, 82 insertions(+), 6 deletions(-)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index 96ec575a..03402322 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -3,8 +3,10 @@ pragma solidity 0.8.23;
 
 // Contracts
 import {Proxy} from "contracts/Proxy.sol";
+import {ERC4626} from "@solmate/mixins/ERC4626.sol";
 import {EthenaARM} from "contracts/EthenaARM.sol";
 import {MorphoMarket} from "src/contracts/markets/MorphoMarket.sol";
+import {EthenaUnstaker} from "contracts/EthenaUnstaker.sol";
 
 // Interfaces
 import {IERC20} from "contracts/Interfaces.sol";
@@ -27,9 +29,10 @@ abstract contract Base_Test_ {
     // --- Main contracts ---
     Proxy public armProxy;
     Proxy public morphoMarketProxy;
-    address public morpho;
+    ERC4626 public morpho;
     EthenaARM public arm;
     MorphoMarket public market;
+    EthenaUnstaker[] public unstakers;
 
     // --- Tokens ---
     IERC20 public usde;
@@ -54,6 +57,8 @@ abstract contract Base_Test_ {
     address public david;
     address public elise;
     address public frank;
+    address public grace;
+    address public harry;
     address public dead;
 
     // --- Group of users ---
@@ -65,6 +70,7 @@ abstract contract Base_Test_ {
     //////////////////////////////////////////////////////
     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;
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
index 4732c74e..d1a270cd 100644
--- a/test/invariants/EthenaARM/Setup.sol
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -6,8 +6,10 @@ import {Base_Test_} from "./Base.sol";
 
 // Contracts
 import {Proxy} from "contracts/Proxy.sol";
+import {ERC4626} from "@solmate/mixins/ERC4626.sol";
 import {EthenaARM} from "contracts/EthenaARM.sol";
 import {MorphoMarket} from "src/contracts/markets/MorphoMarket.sol";
+import {EthenaUnstaker} from "contracts/EthenaUnstaker.sol";
 import {Abstract4626MarketWrapper} from "contracts/markets/Abstract4626MarketWrapper.sol";
 
 // Mocks
@@ -65,6 +67,8 @@ abstract contract Setup is Base_Test_ {
         david = generateAddr("david");
         elise = generateAddr("elise");
         frank = generateAddr("frank");
+        grace = generateAddr("grace");
+        harry = generateAddr("harry");
         dead = generateAddr("dead");
 
         // --- Group of users ---
@@ -87,12 +91,13 @@ abstract contract Setup is Base_Test_ {
         susde = IStakedUSDe(address(new MockSUSDE(address(usde), governor)));
 
         // Deploy mock Morpho Market.
-        morpho = address(new MockERC4626(ERC20(address(usde)), "Morpho USDe Market", "morpho-USDe"));
+        morpho = ERC4626(address(new MockERC4626(ERC20(address(usde)), "Morpho USDe Market", "morpho-USDe")));
     }
 
     function _deployContracts() internal virtual {
         vm.startPrank(deployer);
 
+        // --- Ethena ARM ---
         // Deploy Ethena ARM proxy.
         armProxy = new Proxy();
 
@@ -119,16 +124,30 @@ abstract contract Setup is Base_Test_ {
             treasury,
             address(0) // CapManager address
         );
-        armProxy.initialize(address(arm), governor, data);
+        armProxy.initialize(address(arm), deployer, data);
 
         // Cast proxy address to EthenaARM type for easier interaction.
         arm = EthenaARM(address(armProxy));
 
+        // --- Ethena Unstakers ---
+        // Deploy 42 Ethena Unstaker contracts
+        address[UNSTAKERS_COUNT] memory _unstakers;
+        for (uint256 i; i < UNSTAKERS_COUNT; i++) {
+            unstakers.push(new EthenaUnstaker(address(arm), susde));
+            _unstakers[i] = address(unstakers[i]);
+        }
+        // Set unstakers in the ARM
+        arm.setUnstakers(_unstakers);
+
+        // Transfer ownership of the ARM to the governor.
+        arm.setOwner(governor);
+
+        // --- Morpho Market ---
         // Deploy Morpho Market Proxy.
         morphoMarketProxy = new Proxy();
 
         // Deploy Morpho Market implementation.
-        market = new MorphoMarket(address(arm), morpho);
+        market = new MorphoMarket(address(arm), address(morpho));
 
         // Initialize Morpho Market proxy.
         data = abi.encodeWithSelector(Abstract4626MarketWrapper.initialize.selector, address(0x1), address(0x1));
@@ -152,6 +171,49 @@ abstract contract Setup is Base_Test_ {
         vm.label(address(arm), "Ethena ARM");
         vm.label(address(market), "Morpho Market");
         vm.label(address(morpho), "Morpho Blue");
+        vm.label(address(unstakers[0]), "Ethena Unstaker 0");
+        vm.label(address(unstakers[1]), "Ethena Unstaker 1");
+        vm.label(address(unstakers[2]), "Ethena Unstaker 2");
+        vm.label(address(unstakers[3]), "Ethena Unstaker 3");
+        vm.label(address(unstakers[4]), "Ethena Unstaker 4");
+        vm.label(address(unstakers[5]), "Ethena Unstaker 5");
+        vm.label(address(unstakers[6]), "Ethena Unstaker 6");
+        vm.label(address(unstakers[7]), "Ethena Unstaker 7");
+        vm.label(address(unstakers[8]), "Ethena Unstaker 8");
+        vm.label(address(unstakers[9]), "Ethena Unstaker 9");
+        vm.label(address(unstakers[10]), "Ethena Unstaker 10");
+        vm.label(address(unstakers[11]), "Ethena Unstaker 11");
+        vm.label(address(unstakers[12]), "Ethena Unstaker 12");
+        vm.label(address(unstakers[13]), "Ethena Unstaker 13");
+        vm.label(address(unstakers[14]), "Ethena Unstaker 14");
+        vm.label(address(unstakers[15]), "Ethena Unstaker 15");
+        vm.label(address(unstakers[16]), "Ethena Unstaker 16");
+        vm.label(address(unstakers[17]), "Ethena Unstaker 17");
+        vm.label(address(unstakers[18]), "Ethena Unstaker 18");
+        vm.label(address(unstakers[19]), "Ethena Unstaker 19");
+        vm.label(address(unstakers[20]), "Ethena Unstaker 20");
+        vm.label(address(unstakers[21]), "Ethena Unstaker 21");
+        vm.label(address(unstakers[22]), "Ethena Unstaker 22");
+        vm.label(address(unstakers[23]), "Ethena Unstaker 23");
+        vm.label(address(unstakers[24]), "Ethena Unstaker 24");
+        vm.label(address(unstakers[25]), "Ethena Unstaker 25");
+        vm.label(address(unstakers[26]), "Ethena Unstaker 26");
+        vm.label(address(unstakers[27]), "Ethena Unstaker 27");
+        vm.label(address(unstakers[28]), "Ethena Unstaker 28");
+        vm.label(address(unstakers[29]), "Ethena Unstaker 29");
+        vm.label(address(unstakers[30]), "Ethena Unstaker 30");
+        vm.label(address(unstakers[31]), "Ethena Unstaker 31");
+        vm.label(address(unstakers[32]), "Ethena Unstaker 32");
+        vm.label(address(unstakers[33]), "Ethena Unstaker 33");
+        vm.label(address(unstakers[34]), "Ethena Unstaker 34");
+        vm.label(address(unstakers[35]), "Ethena Unstaker 35");
+        vm.label(address(unstakers[36]), "Ethena Unstaker 36");
+        vm.label(address(unstakers[37]), "Ethena Unstaker 37");
+        vm.label(address(unstakers[38]), "Ethena Unstaker 38");
+        vm.label(address(unstakers[39]), "Ethena Unstaker 39");
+        vm.label(address(unstakers[40]), "Ethena Unstaker 40");
+        vm.label(address(unstakers[41]), "Ethena Unstaker 41");
+        // Using a loop here would be cleaner, but Vm.label doesn't support dynamic strings.
 
         // --- Tokens ---
         vm.label(address(usde), "USDe");
@@ -170,6 +232,8 @@ abstract contract Setup is Base_Test_ {
         vm.label(david, "David");
         vm.label(elise, "Elise");
         vm.label(frank, "Frank");
+        vm.label(grace, "Grace");
+        vm.label(harry, "Harry");
         vm.label(dead, "Dead");
     }
 
@@ -183,9 +247,15 @@ abstract contract Setup is Base_Test_ {
         susde.deposit(1_000_000 ether, dead);
 
         // Same for morpho contract.
-        usde.approve(morpho, 1_000_000 ether);
-        MockERC4626(morpho).deposit(1_000_000 ether, dead);
+        usde.approve(address(morpho), 1_000_000 ether);
+        ERC4626(morpho).deposit(1_000_000 ether, dead);
         vm.stopPrank();
+
+        // Set initial prices in the ARM.
+        vm.prank(governor);
+        arm.setCrossPrice(0.9998e36);
+        vm.prank(operator);
+        arm.setPrices(0.9992e36, 0.9999e36);
     }
 
     function generateAddr(string memory name) internal returns (address) {

From 2f90f7a4878f3be477bd77d7a6f5d279b57d363d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 09:12:05 +0100
Subject: [PATCH 06/28] Prepare list for target functions

---
 test/invariants/EthenaARM/TargetFunctions.sol | 37 ++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 71f84532..df525e9b 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -7,4 +7,39 @@ import {Setup} from "./Setup.sol";
 /// @title TargetFunctions
 /// @notice TargetFunctions contract for tests, containing the target functions that should be tested.
 ///         This is the entry point with the contract we are testing. Ideally, it should never revert.
-abstract contract TargetFunctions is Setup {}
+abstract contract TargetFunctions is Setup {
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                              ✦✦✦ ETHENA ARM ✦✦✦                              ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    // [ ] SwapExactTokensForTokens
+    // [ ] SwapTokensForExactTokens
+    // [ ] Deposit
+    // [ ] Allocate
+    // [ ] CollectFees
+    // [ ] RequestRedeem
+    // [ ] ClaimRedeem
+    // [ ] RequestBaseWithdrawal
+    // [ ] ClaimBaseWithdrawals
+    // --- Admin functions
+    // [ ] SetPrices
+    // [ ] SetCrossPrice
+    // [ ] SetFee
+    // [ ] SetActiveMarket
+    // [ ] SetARMBuffer
+    //
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    // [ ] Deposit
+    // [ ] CoolDownShares
+    // [ ] Unstake
+    // [ ] TransferInRewards
+    //
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                                ✦✦✦ MORPHO ✦✦✦                                ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    // [ ] Deposit
+    // [ ] Withdraw
+    // [ ] TransferInRewards
+
+    }

From fb18073acc1c3897c9e8aa5c6bb3e5e879a8bb25 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 11:56:03 +0100
Subject: [PATCH 07/28] Fix rewards calculation

---
 test/invariants/EthenaARM/mocks/MockSUSDE.sol | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/invariants/EthenaARM/mocks/MockSUSDE.sol b/test/invariants/EthenaARM/mocks/MockSUSDE.sol
index d849674e..b71cd1f5 100644
--- a/test/invariants/EthenaARM/mocks/MockSUSDE.sol
+++ b/test/invariants/EthenaARM/mocks/MockSUSDE.sol
@@ -21,7 +21,7 @@ contract MockSUSDE is ERC4626, Owned {
     /// --- STATE VARIABLES
     //////////////////////////////////////////////////////
     uint256 public vestingAmount;
-    uint256 public lastDistribution;
+    uint256 public lastDistributionTimestamp;
     mapping(address => UserCooldown) public cooldowns;
 
     //////////////////////////////////////////////////////
@@ -50,7 +50,7 @@ contract MockSUSDE is ERC4626, Owned {
     }
 
     function getUnvestedAmount() public view returns (uint256) {
-        uint256 timeSinceLastDistribution = block.timestamp - lastDistribution;
+        uint256 timeSinceLastDistribution = block.timestamp - lastDistributionTimestamp;
 
         if (timeSinceLastDistribution >= VESTING_DURATION) {
             return 0;
@@ -118,8 +118,8 @@ contract MockSUSDE is ERC4626, Owned {
         // Ensure previous vesting period is complete before starting a new one
         // _updateVestingAmount(amount) in original contract
         require(getUnvestedAmount() == 0, "SUSDE: previous vesting not complete");
-        vestingAmount += amount;
-        lastDistribution = block.timestamp;
+        vestingAmount = amount;
+        lastDistributionTimestamp = block.timestamp;
 
         asset.transferFrom(msg.sender, address(this), amount);
         emit RewardReceived(amount);

From d42cd55d763f444de7a87c3435ff979a494997d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 11:56:12 +0100
Subject: [PATCH 08/28] Add label and assume functions to Vm interface

---
 test/invariants/EthenaARM/helpers/Vm.sol | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/invariants/EthenaARM/helpers/Vm.sol b/test/invariants/EthenaARM/helpers/Vm.sol
index fc29d5f5..1535210e 100644
--- a/test/invariants/EthenaARM/helpers/Vm.sol
+++ b/test/invariants/EthenaARM/helpers/Vm.sol
@@ -89,5 +89,7 @@ interface Vm {
     function parseInt(string memory) external returns (int256);
     function parseBool(string memory) external returns (bool);
 
+    // Only works with Foundry
     function label(address account, string calldata newLabel) external;
+    function assume(bool condition) external;
 }

From ab309aed3887abde4d0fbce1e4c07381a529eea9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 11:56:34 +0100
Subject: [PATCH 09/28] Improve invariant setup

---
 test/invariants/EthenaARM/Base.sol  |  1 +
 test/invariants/EthenaARM/Setup.sol | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index 03402322..1eab02b9 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -78,5 +78,6 @@ abstract contract Base_Test_ {
 
     /// @notice Indicates if labels have been set in the Vm.
     function isLabelAvailable() external view virtual returns (bool);
+    function isAssumeAvailable() external view virtual returns (bool);
 }
 
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
index d1a270cd..68a6d65c 100644
--- a/test/invariants/EthenaARM/Setup.sol
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -256,9 +256,28 @@ abstract contract Setup is Base_Test_ {
         arm.setCrossPrice(0.9998e36);
         vm.prank(operator);
         arm.setPrices(0.9992e36, 0.9999e36);
+
+        // Grace will only deposit/withdraw USDe from/to sUSDe.
+        vm.prank(grace);
+        usde.approve(address(susde), type(uint256).max);
+
+        // Harry will only deposit/withdraw USDe from/to Morpho.
+        vm.prank(harry);
+        usde.approve(address(morpho), type(uint256).max);
+
+        // Governor will deposit usde rewards into sUSDe.
+        vm.prank(governor);
+        usde.approve(address(susde), type(uint256).max);
     }
 
     function generateAddr(string memory name) internal returns (address) {
         return vm.addr(uint256(keccak256(abi.encodePacked(name))));
     }
+
+    function assume(bool condition) internal returns (bool returnEarly) {
+        if (!condition) {
+            if (this.isAssumeAvailable()) vm.assume(false);
+            else returnEarly = true;
+        }
+    }
 }

From 20cf9aabc271e7d10fbe6b45f52b9ca285f2fc6f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 11:56:57 +0100
Subject: [PATCH 10/28] wip add targets for susde contract

---
 src/contracts/Interfaces.sol                  |  6 ++
 test/invariants/EthenaARM/FoundryFuzzer.sol   | 30 ++++++-
 test/invariants/EthenaARM/TargetFunctions.sol | 80 ++++++++++++++++++-
 3 files changed, 113 insertions(+), 3 deletions(-)

diff --git a/src/contracts/Interfaces.sol b/src/contracts/Interfaces.sol
index d013642c..13c75b7a 100644
--- a/src/contracts/Interfaces.sol
+++ b/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;
 }
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index a86c9103..91eb135e 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -3,6 +3,7 @@ pragma solidity 0.8.23;
 
 // Test imports
 import {Properties} from "./Properties.sol";
+import {StdInvariant} from "forge-std/StdInvariant.sol";
 
 /// @title FuzzerFoundry
 /// @notice Concrete fuzzing contract implementing Foundry's invariant testing framework.
@@ -12,8 +13,33 @@ import {Properties} from "./Properties.sol";
 ///         - 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 {
+contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
     bool public constant override isLabelAvailable = true;
+    bool public constant override isAssumeAvailable = true;
 
-    function test() public {}
+    //////////////////////////////////////////////////////
+    /// --- SETUP
+    //////////////////////////////////////////////////////
+    function setUp() public override {
+        super.setUp();
+
+        // --- Setup Fuzzer target ---
+        // Setup target
+        targetContract(address(this));
+
+        // Add selectors
+        bytes4[] memory selectors = new bytes4[](4);
+        selectors[0] = this.targetSUSDeDeposit.selector;
+        selectors[1] = this.targetSUSDeCooldownShares.selector;
+        selectors[2] = this.targetSUSDeUnstake.selector;
+        selectors[3] = this.targetSUSDeTransferInRewards.selector;
+
+        // Target selectors
+        targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- INVARIANTS
+    //////////////////////////////////////////////////////
+    function invariantA() public {}
 }
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index df525e9b..8c441c85 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -3,11 +3,18 @@ pragma solidity 0.8.23;
 
 // Test imports
 import {Setup} from "./Setup.sol";
+import {StdUtils} from "forge-std/StdUtils.sol";
+
+// Solmate
+import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
+
+// Contracts
+import {UserCooldown} from "contracts/Interfaces.sol";
 
 /// @title TargetFunctions
 /// @notice TargetFunctions contract for tests, containing the target functions that should be tested.
 ///         This is the entry point with the contract we are testing. Ideally, it should never revert.
-abstract contract TargetFunctions is Setup {
+abstract contract TargetFunctions is Setup, StdUtils {
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                              ✦✦✦ ETHENA ARM ✦✦✦                              ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
@@ -33,6 +40,7 @@ abstract contract TargetFunctions is Setup {
     // [ ] Deposit
     // [ ] CoolDownShares
     // [ ] Unstake
+    // --- Admin functions
     // [ ] TransferInRewards
     //
     // ╔══════════════════════════════════════════════════════════════════════════════╗
@@ -41,5 +49,75 @@ abstract contract TargetFunctions is Setup {
     // [ ] Deposit
     // [ ] Withdraw
     // [ ] TransferInRewards
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                                   ✦✦✦  ✦✦✦                                   ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    function targetSUSDeDeposit(uint88 amount) external {
+        // Ensure we don't mint 0 shares.
+        uint256 totalAssets = susde.totalAssets();
+        uint256 totalSupply = susde.totalSupply();
+        uint256 minAmount = totalAssets / totalSupply + 1;
+        // Prevent zero deposits
+        amount = uint88(_bound(amount, minAmount, type(uint88).max));
+
+        // Mint amount to grace
+        MockERC20(address(usde)).mint(grace, amount);
+
+        // Deposit as grace
+        vm.prank(grace);
+        susde.deposit(amount, grace);
+    }
+
+    function targetSUSDeCooldownShares(uint88 shareAmount) external {
+        // Cache balance
+        uint256 balance = susde.balanceOf(grace);
+
+        // Assume balance not zero
+        if (assume(balance > 1)) return;
+
+        // Bound shareAmount to [1, balance]
+        shareAmount = uint88(_bound(shareAmount, 1, balance));
+
+        // Cooldown shares as grace
+        vm.prank(grace);
+        susde.cooldownShares(shareAmount);
+    }
+
+    function targetSUSDeUnstake() external {
+        // Check grace's cooldown
+        UserCooldown memory cooldown = susde.cooldowns(grace);
+
+        // Ensure grace has a valid cooldown
+        if (assume(cooldown.cooldownEnd != 0)) return;
+
+        // Fast forward to after cooldown end
+        vm.warp(cooldown.cooldownEnd + 1);
+
+        // Unstake as grace
+        vm.prank(grace);
+        susde.unstake(grace);
+
+        MockERC20(address(usde)).burn(grace, cooldown.underlyingAmount);
+    }
+
+    function targetSUSDeTransferInRewards(uint8 bps) external {
+        // Ensure enough time has passed since last distribution
+        uint256 lastDistribution = susde.lastDistributionTimestamp();
+        if (block.timestamp - lastDistribution < 8 hours) {
+            // Fast forward time to allow rewards distribution
+            vm.warp(lastDistribution + 8 hours + 1);
+        }
 
+        uint256 balance = usde.balanceOf(address(susde));
+        // Rewards can be distributed 3/days max. 1bps at every distribution -> 10 APR.
+        bps = uint8(_bound(bps, 1, 10));
+        uint256 rewards = (balance * bps) / 10_000;
+        MockERC20(address(usde)).mint(governor, rewards);
+        vm.prank(governor);
+        susde.transferInRewards(rewards);
     }
+}

From a0afd617dc74680754b1804e144ed61500e95860 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 15:22:28 +0100
Subject: [PATCH 11/28] add logs

---
 test/invariants/EthenaARM/Base.sol            |  1 +
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  1 +
 test/invariants/EthenaARM/TargetFunctions.sol | 62 +++++++++++++++++--
 3 files changed, 60 insertions(+), 4 deletions(-)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index 1eab02b9..45c00df5 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -79,5 +79,6 @@ abstract contract Base_Test_ {
     /// @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);
 }
 
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 91eb135e..39a9a887 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -16,6 +16,7 @@ import {StdInvariant} from "forge-std/StdInvariant.sol";
 contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
     bool public constant override isLabelAvailable = true;
     bool public constant override isAssumeAvailable = true;
+    bool public constant override isConsoleAvailable = true;
 
     //////////////////////////////////////////////////////
     /// --- SETUP
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 8c441c85..1abd83f9 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -3,7 +3,9 @@ pragma solidity 0.8.23;
 
 // Test imports
 import {Setup} from "./Setup.sol";
+import {console} from "forge-std/console.sol";
 import {StdUtils} from "forge-std/StdUtils.sol";
+import {StdStyle} from "forge-std/StdStyle.sol";
 
 // Solmate
 import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
@@ -69,7 +71,13 @@ abstract contract TargetFunctions is Setup, StdUtils {
 
         // Deposit as grace
         vm.prank(grace);
-        susde.deposit(amount, grace);
+        uint256 shares = susde.deposit(amount, grace);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> sUSDe Deposit:\t Grace deposited %18e USDe\t and received %18e sUSDe shares", amount, shares
+            );
+        }
     }
 
     function targetSUSDeCooldownShares(uint88 shareAmount) external {
@@ -84,7 +92,14 @@ abstract contract TargetFunctions is Setup, StdUtils {
 
         // Cooldown shares as grace
         vm.prank(grace);
-        susde.cooldownShares(shareAmount);
+        uint256 amount = susde.cooldownShares(shareAmount);
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> sUSDe Cooldown:\t Grace cooled down %18e sUSDe shares\t for %18e USDe underlying",
+                shareAmount,
+                amount
+            );
+        }
     }
 
     function targetSUSDeUnstake() external {
@@ -95,12 +110,32 @@ abstract contract TargetFunctions is Setup, StdUtils {
         if (assume(cooldown.cooldownEnd != 0)) return;
 
         // Fast forward to after cooldown end
-        vm.warp(cooldown.cooldownEnd + 1);
+        if (this.isConsoleAvailable()) {
+            console.log(
+                StdStyle.yellow(
+                    string(
+                        abi.encodePacked(
+                            ">>> Time jump:\t Fast forwarded to: ",
+                            vm.toString(cooldown.cooldownEnd),
+                            "  (+ ",
+                            vm.toString(cooldown.cooldownEnd - block.timestamp),
+                            "s)"
+                        )
+                    )
+                )
+            );
+        }
+        vm.warp(cooldown.cooldownEnd);
 
         // Unstake as grace
         vm.prank(grace);
         susde.unstake(grace);
 
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> sUSDe Unstake:\t Grace unstaked %18e USDe underlying after cooldown", cooldown.underlyingAmount
+            );
+        }
         MockERC20(address(usde)).burn(grace, cooldown.underlyingAmount);
     }
 
@@ -109,7 +144,22 @@ abstract contract TargetFunctions is Setup, StdUtils {
         uint256 lastDistribution = susde.lastDistributionTimestamp();
         if (block.timestamp - lastDistribution < 8 hours) {
             // Fast forward time to allow rewards distribution
-            vm.warp(lastDistribution + 8 hours + 1);
+            if (this.isConsoleAvailable()) {
+                console.log(
+                    StdStyle.yellow(
+                        string(
+                            abi.encodePacked(
+                                ">>> Time jump:\t Fast forwarded to: ",
+                                vm.toString(lastDistribution + 8 hours),
+                                "  (+ ",
+                                vm.toString((lastDistribution + 8 hours) - block.timestamp),
+                                "s)"
+                            )
+                        )
+                    )
+                );
+                vm.warp(lastDistribution + 8 hours);
+            }
         }
 
         uint256 balance = usde.balanceOf(address(susde));
@@ -119,5 +169,9 @@ abstract contract TargetFunctions is Setup, StdUtils {
         MockERC20(address(usde)).mint(governor, rewards);
         vm.prank(governor);
         susde.transferInRewards(rewards);
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> sUSDe Rewards:\t Governor transferred in %18e USDe as rewards, bps: %d", rewards, bps);
+        }
     }
 }

From 31b456984052166743a88cb670a80fa7a3fa1517 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 15:23:31 +0100
Subject: [PATCH 12/28] Update SUSDE target functions to reflect completed
 implementations

---
 test/invariants/EthenaARM/TargetFunctions.sol | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 1abd83f9..7099d41e 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -39,11 +39,11 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
-    // [ ] Deposit
-    // [ ] CoolDownShares
-    // [ ] Unstake
+    // [x] Deposit
+    // [x] CoolDownShares
+    // [x] Unstake
     // --- Admin functions
-    // [ ] TransferInRewards
+    // [x] TransferInRewards
     //
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ MORPHO ✦✦✦                                ║

From 43bafdd03eb5b910715514a47d648883af0832eb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Tue, 18 Nov 2025 16:38:59 +0100
Subject: [PATCH 13/28] Add Morpho target functions

---
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  7 +-
 test/invariants/EthenaARM/TargetFunctions.sol | 64 ++++++++++++++++++-
 2 files changed, 67 insertions(+), 4 deletions(-)

diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 39a9a887..0f4d8245 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,11 +29,16 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](4);
+        bytes4[] memory selectors = new bytes4[](7);
+        // --- 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;
 
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 7099d41e..9762014d 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -48,9 +48,9 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ MORPHO ✦✦✦                                ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
-    // [ ] Deposit
-    // [ ] Withdraw
-    // [ ] TransferInRewards
+    // [x] Deposit
+    // [x] Withdraw
+    // [x] TransferInRewards
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                   ✦✦✦  ✦✦✦                                   ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
@@ -174,4 +174,62 @@ abstract contract TargetFunctions is Setup, StdUtils {
             console.log(">>> sUSDe Rewards:\t Governor transferred in %18e USDe as rewards, bps: %d", rewards, bps);
         }
     }
+
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                                ✦✦✦ MORPHO ✦✦✦                                ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    function targetMorphoDeposit(uint88 amount) external {
+        // Ensure we don't mint 0 shares.
+        uint256 totalAssets = morpho.totalAssets();
+        uint256 totalSupply = morpho.totalSupply();
+        uint256 minAmount = totalAssets / totalSupply + 1;
+        // Prevent zero deposits
+        amount = uint88(_bound(amount, minAmount, type(uint88).max));
+
+        // Mint amount to harry
+        MockERC20(address(usde)).mint(harry, amount);
+
+        // Deposit as harry
+        vm.prank(harry);
+        uint256 shares = morpho.deposit(amount, harry);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> Morpho Deposit:\t Harry deposited %18e USDe\t and received %18e Morpho shares", amount, shares
+            );
+        }
+    }
+
+    function targetMorphoWithdraw(uint88 amount) external {
+        // Check harry's balance
+        uint256 balance = morpho.balanceOf(harry);
+
+        // Assume balance not zero
+        if (assume(balance > 1)) return;
+
+        // Bound shareAmount to [1, balance]
+        amount = uint88(_bound(amount, 1, balance));
+
+        // Withdraw as harry
+        vm.prank(harry);
+        uint256 shares = morpho.withdraw(amount, harry, harry);
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> Morpho Withdraw:\t Harry withdrew %18e Morpho shares\t for %18e USDe underlying", shares, amount
+            );
+        }
+
+        MockERC20(address(usde)).burn(harry, amount);
+    }
+
+    function targetMorphoTransferInRewards(uint8 bps) external {
+        uint256 balance = usde.balanceOf(address(morpho));
+        bps = uint8(_bound(bps, 1, 10));
+        uint256 rewards = (balance * bps) / 10_000;
+        MockERC20(address(usde)).mint(address(morpho), rewards);
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> Morpho Rewards:\t Transferred in %18e USDe as rewards, bps: %d", rewards, bps);
+        }
+    }
 }

From 58c92c79ce2fd2a3ca1f6fa24f3bb4bb402ffa73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 12:37:48 +0100
Subject: [PATCH 14/28] Add Find library for user request retrieval in testing

---
 test/invariants/EthenaARM/helpers/Find.sol | 43 ++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 test/invariants/EthenaARM/helpers/Find.sol

diff --git a/test/invariants/EthenaARM/helpers/Find.sol b/test/invariants/EthenaARM/helpers/Find.sol
new file mode 100644
index 00000000..20b25623
--- /dev/null
+++ b/test/invariants/EthenaARM/helpers/Find.sol
@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+import {AbstractARM} from "contracts/AbstractARM.sol";
+
+/// @notice Library used to find specific data in storage for testing purposes.
+///         Most of the time to find a specific user/request that meets certain criteria.
+library Find {
+    struct GetUserRequestWithAmountStruct {
+        address arm;
+        uint248 randomAddressIndex;
+        uint248 randomArrayIndex;
+        address[] users;
+        uint256 targetAmount;
+    }
+
+    function getUserRequestWithAmount(
+        GetUserRequestWithAmountStruct memory $,
+        mapping(address => uint256[]) storage pendingRequests
+    ) internal returns (address user, uint256 requestId, uint40 claimTimestamp) {
+        uint256 usersLen = $.users.length;
+        for (uint256 i; i < usersLen; i++) {
+            // Take a random user
+            address _user = $.users[($.randomAddressIndex + i) % usersLen];
+            // Find a request that can be claimed
+            for (uint256 j; j < pendingRequests[_user].length; j++) {
+                // Take a random request from that user
+                uint256 _requestId = pendingRequests[_user][($.randomArrayIndex + j) % pendingRequests[_user].length];
+                // Check request data
+                (,, uint40 _claimTimestamp, uint128 _amount,) = AbstractARM($.arm).withdrawalRequests(_requestId);
+                // Check if this is claimable
+                if (_amount <= $.targetAmount) {
+                    (user, requestId, claimTimestamp) = (_user, _requestId, _claimTimestamp);
+                    // Remove pendingRequests
+                    pendingRequests[_user][($.randomArrayIndex + j) % pendingRequests[_user].length] =
+                        pendingRequests[_user][pendingRequests[_user].length - 1];
+                    pendingRequests[_user].pop();
+                    break;
+                }
+            }
+        }
+    }
+}

From f38d005dd5a524d3a99ef4ae35bb07cf929a3d59 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 12:38:14 +0100
Subject: [PATCH 15/28] Add ARM deposit/request/claim target functions

---
 test/invariants/EthenaARM/Base.sol            |   1 +
 test/invariants/EthenaARM/FoundryFuzzer.sol   |   6 +-
 test/invariants/EthenaARM/Setup.sol           |  19 ++
 test/invariants/EthenaARM/TargetFunctions.sol | 172 ++++++++++++++++--
 test/invariants/EthenaARM/helpers/Vm.sol      |   1 +
 5 files changed, 178 insertions(+), 21 deletions(-)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index 45c00df5..c60e1c87 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -64,6 +64,7 @@ abstract contract Base_Test_ {
     // --- Group of users ---
     address[] public makers;
     address[] public traders;
+    mapping(address => uint256[]) public pendingRequests;
 
     //////////////////////////////////////////////////////
     /// --- DEFAULT VALUES
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 0f4d8245..ee9be96c 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](7);
+        bytes4[] memory selectors = new bytes4[](10);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -39,6 +39,10 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         selectors[4] = this.targetMorphoDeposit.selector;
         selectors[5] = this.targetMorphoWithdraw.selector;
         selectors[6] = this.targetMorphoTransferInRewards.selector;
+        // --- ARM ---
+        selectors[7] = this.targetARMDeposit.selector;
+        selectors[8] = this.targetARMRequestRedeem.selector;
+        selectors[9] = this.targetARMClaimRedeem.selector;
 
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
index 68a6d65c..d9320a30 100644
--- a/test/invariants/EthenaARM/Setup.sol
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -268,6 +268,19 @@ abstract contract Setup is Base_Test_ {
         // Governor will deposit usde rewards into sUSDe.
         vm.prank(governor);
         usde.approve(address(susde), type(uint256).max);
+
+        // Makers and traders approve ARM to spend their USDe.
+        for (uint256 i; i < MAKERS_COUNT; i++) {
+            vm.prank(makers[i]);
+            usde.approve(address(arm), type(uint256).max);
+        }
+
+        for (uint256 i; i < TRADERS_COUNT; i++) {
+            vm.startPrank(traders[i]);
+            usde.approve(address(arm), type(uint256).max);
+            susde.approve(address(arm), type(uint256).max);
+            vm.stopPrank();
+        }
     }
 
     function generateAddr(string memory name) internal returns (address) {
@@ -280,4 +293,10 @@ abstract contract Setup is Base_Test_ {
             else returnEarly = true;
         }
     }
+
+    modifier ensureTimeIncrease() {
+        uint256 oldTimestamp = block.timestamp;
+        _;
+        require(block.timestamp >= oldTimestamp, "TIME_DECREASED");
+    }
 }
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 9762014d..24057522 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -13,6 +13,9 @@ import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
 // Contracts
 import {UserCooldown} from "contracts/Interfaces.sol";
 
+// Helpers
+import {Find} from "./helpers/Find.sol";
+
 /// @title TargetFunctions
 /// @notice TargetFunctions contract for tests, containing the target functions that should be tested.
 ///         This is the entry point with the contract we are testing. Ideally, it should never revert.
@@ -22,11 +25,11 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // ╚══════════════════════════════════════════════════════════════════════════════╝
     // [ ] SwapExactTokensForTokens
     // [ ] SwapTokensForExactTokens
-    // [ ] Deposit
+    // [x] Deposit
     // [ ] Allocate
     // [ ] CollectFees
-    // [ ] RequestRedeem
-    // [ ] ClaimRedeem
+    // [x] RequestRedeem
+    // [x] ClaimRedeem
     // [ ] RequestBaseWithdrawal
     // [ ] ClaimBaseWithdrawals
     // --- Admin functions
@@ -55,6 +58,133 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // ║                                   ✦✦✦  ✦✦✦                                   ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
 
+    // ╔══════════════════════════════════════════════════════════════════════════════╗
+    // ║                              ✦✦✦ ETHENA ARM ✦✦✦                              ║
+    // ╚══════════════════════════════════════════════════════════════════════════════╝
+    function targetARMDeposit(uint88 amount, uint256 randomAddressIndex) external {
+        // Select a random user from makers
+        address user = makers[randomAddressIndex % MAKERS_COUNT];
+
+        uint256 totalSupply = arm.totalSupply();
+        uint256 totalAssets = arm.totalAssets();
+        // Min amount to avoid 0 shares minting
+        uint256 minAmount = totalAssets / totalSupply + 1;
+        amount = uint88(_bound(amount, minAmount, type(uint88).max));
+
+        // Mint amount to user
+        MockERC20(address(usde)).mint(user, amount);
+        // Deposit as user
+        vm.prank(user);
+        uint256 shares = arm.deposit(amount, user);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> ARM Deposit:\t %s deposited %18e USDe\t and received %18e ARM shares",
+                vm.getLabel(user),
+                amount,
+                shares
+            );
+        }
+    }
+
+    function targetARMRequestRedeem(uint88 shareAmount, uint248 randomAddressIndex) external {
+        address user;
+        uint256 balance;
+        // Todo: mirgate it to Find library
+        for (uint256 i; i < MAKERS_COUNT; i++) {
+            address _user = makers[(randomAddressIndex + i) % MAKERS_COUNT];
+            uint256 _balance = arm.balanceOf(_user);
+            // Found a user with non-zero balance
+            if (_balance > 1) {
+                (user, balance) = (_user, _balance);
+                break;
+            }
+        }
+        if (assume(user != address(0))) return;
+        // Bound shareAmount to [1, balance]
+        shareAmount = uint88(_bound(shareAmount, 1, balance));
+
+        // Request redeem as user
+        vm.prank(user);
+        (uint256 requestId, uint256 amount) = arm.requestRedeem(shareAmount);
+        pendingRequests[user].push(requestId);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                string(
+                    abi.encodePacked(
+                        ">>> ARM Request:\t ",
+                        vm.getLabel(user),
+                        " requested redeem of %18e ARM shares\t for %18e USDe underlying\t Request ID: %d"
+                    )
+                ),
+                shareAmount,
+                amount,
+                requestId
+            );
+        }
+    }
+
+    function targetARMClaimRedeem(uint248 randomAddressIndex, uint248 randomArrayIndex) external ensureTimeIncrease {
+        address user;
+        uint256 requestId;
+        uint256 claimTimestamp;
+        uint256 claimable = arm.claimable();
+        if (assume(claimable != 0)) return;
+        // Find a user with a pending request, where the amount is <= claimable
+        {
+            (user, requestId, claimTimestamp) = Find.getUserRequestWithAmount(
+                Find.GetUserRequestWithAmountStruct({
+                    arm: address(arm),
+                    randomAddressIndex: randomAddressIndex,
+                    randomArrayIndex: randomArrayIndex,
+                    users: makers,
+                    targetAmount: claimable
+                }),
+                pendingRequests
+            );
+            if (assume(user != address(0))) return;
+        }
+
+        // Fast forward time if needed
+        if (block.timestamp < claimTimestamp) {
+            if (this.isConsoleAvailable()) {
+                console.log(
+                    StdStyle.yellow(
+                        string(
+                            abi.encodePacked(
+                                ">>> Time jump:\t Fast forwarded to: ",
+                                vm.toString(claimTimestamp),
+                                "  (+ ",
+                                vm.toString(claimTimestamp - block.timestamp),
+                                "s)"
+                            )
+                        )
+                    )
+                );
+            }
+            vm.warp(claimTimestamp);
+        }
+
+        // Claim redeem as user
+        vm.prank(user);
+        uint256 amount = arm.claimRedeem(requestId);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                string(
+                    abi.encodePacked(
+                        ">>> ARM Claim:\t ",
+                        vm.getLabel(user),
+                        " claimed redeem request ID %d\t and received %18e USDe underlying"
+                    )
+                ),
+                requestId,
+                amount
+            );
+        }
+    }
+
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
@@ -102,30 +232,32 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
-    function targetSUSDeUnstake() external {
+    function targetSUSDeUnstake() external ensureTimeIncrease {
         // Check grace's cooldown
         UserCooldown memory cooldown = susde.cooldowns(grace);
 
         // Ensure grace has a valid cooldown
         if (assume(cooldown.cooldownEnd != 0)) return;
 
-        // Fast forward to after cooldown end
-        if (this.isConsoleAvailable()) {
-            console.log(
-                StdStyle.yellow(
-                    string(
-                        abi.encodePacked(
-                            ">>> Time jump:\t Fast forwarded to: ",
-                            vm.toString(cooldown.cooldownEnd),
-                            "  (+ ",
-                            vm.toString(cooldown.cooldownEnd - block.timestamp),
-                            "s)"
+        // Fast forward to after cooldown end if needed
+        if (block.timestamp < cooldown.cooldownEnd) {
+            if (this.isConsoleAvailable()) {
+                console.log(
+                    StdStyle.yellow(
+                        string(
+                            abi.encodePacked(
+                                ">>> Time jump:\t Fast forwarded to: ",
+                                vm.toString(cooldown.cooldownEnd),
+                                "  (+ ",
+                                vm.toString(cooldown.cooldownEnd - block.timestamp),
+                                "s)"
+                            )
                         )
                     )
-                )
-            );
+                );
+            }
+            vm.warp(cooldown.cooldownEnd);
         }
-        vm.warp(cooldown.cooldownEnd);
 
         // Unstake as grace
         vm.prank(grace);
@@ -139,10 +271,10 @@ abstract contract TargetFunctions is Setup, StdUtils {
         MockERC20(address(usde)).burn(grace, cooldown.underlyingAmount);
     }
 
-    function targetSUSDeTransferInRewards(uint8 bps) external {
+    function targetSUSDeTransferInRewards(uint8 bps) external ensureTimeIncrease {
         // Ensure enough time has passed since last distribution
         uint256 lastDistribution = susde.lastDistributionTimestamp();
-        if (block.timestamp - lastDistribution < 8 hours) {
+        if (block.timestamp < 8 hours + lastDistribution) {
             // Fast forward time to allow rewards distribution
             if (this.isConsoleAvailable()) {
                 console.log(
diff --git a/test/invariants/EthenaARM/helpers/Vm.sol b/test/invariants/EthenaARM/helpers/Vm.sol
index 1535210e..ba1ddc99 100644
--- a/test/invariants/EthenaARM/helpers/Vm.sol
+++ b/test/invariants/EthenaARM/helpers/Vm.sol
@@ -91,5 +91,6 @@ interface Vm {
 
     // Only works with Foundry
     function label(address account, string calldata newLabel) external;
+    function getLabel(address account) external returns (string memory);
     function assume(bool condition) external;
 }

From bb34132ca8c505e85124f56b5b4803b6df5ad993 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 15:11:10 +0100
Subject: [PATCH 16/28] Add MockMorpho contract and update tests for
 utilization rate functionality

---
 test/invariants/EthenaARM/Base.sol            |  4 +-
 test/invariants/EthenaARM/FoundryFuzzer.sol   | 10 ++---
 test/invariants/EthenaARM/Setup.sol           |  8 ++--
 test/invariants/EthenaARM/TargetFunctions.sol | 12 +++++
 .../invariants/EthenaARM/mocks/MockMorpho.sol | 44 +++++++++++++++++++
 5 files changed, 66 insertions(+), 12 deletions(-)
 create mode 100644 test/invariants/EthenaARM/mocks/MockMorpho.sol

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index c60e1c87..2eb4ba40 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -3,8 +3,8 @@ pragma solidity 0.8.23;
 
 // Contracts
 import {Proxy} from "contracts/Proxy.sol";
-import {ERC4626} from "@solmate/mixins/ERC4626.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";
 
@@ -29,8 +29,8 @@ abstract contract Base_Test_ {
     // --- Main contracts ---
     Proxy public armProxy;
     Proxy public morphoMarketProxy;
-    ERC4626 public morpho;
     EthenaARM public arm;
+    MockMorpho public morpho;
     MorphoMarket public market;
     EthenaUnstaker[] public unstakers;
 
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index ee9be96c..0b45e932 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](10);
+        bytes4[] memory selectors = new bytes4[](11);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -39,11 +39,11 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         selectors[4] = this.targetMorphoDeposit.selector;
         selectors[5] = this.targetMorphoWithdraw.selector;
         selectors[6] = this.targetMorphoTransferInRewards.selector;
+        selectors[7] = this.targetMorphoSetUtilizationRate.selector;
         // --- ARM ---
-        selectors[7] = this.targetARMDeposit.selector;
-        selectors[8] = this.targetARMRequestRedeem.selector;
-        selectors[9] = this.targetARMClaimRedeem.selector;
-
+        selectors[8] = this.targetARMDeposit.selector;
+        selectors[9] = this.targetARMRequestRedeem.selector;
+        selectors[10] = this.targetARMClaimRedeem.selector;
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
     }
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
index d9320a30..17f8668d 100644
--- a/test/invariants/EthenaARM/Setup.sol
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -6,17 +6,15 @@ import {Base_Test_} from "./Base.sol";
 
 // Contracts
 import {Proxy} from "contracts/Proxy.sol";
-import {ERC4626} from "@solmate/mixins/ERC4626.sol";
 import {EthenaARM} from "contracts/EthenaARM.sol";
 import {MorphoMarket} from "src/contracts/markets/MorphoMarket.sol";
 import {EthenaUnstaker} from "contracts/EthenaUnstaker.sol";
 import {Abstract4626MarketWrapper} from "contracts/markets/Abstract4626MarketWrapper.sol";
 
 // Mocks
-import {ERC20} from "@solmate/tokens/ERC20.sol";
 import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
 import {MockSUSDE} from "test/invariants/EthenaARM/mocks/MockSUSDE.sol";
-import {MockERC4626} from "@solmate/test/utils/mocks/MockERC4626.sol";
+import {MockMorpho} from "test/invariants/EthenaARM/mocks/MockMorpho.sol";
 
 // Interfaces
 import {IERC20} from "contracts/Interfaces.sol";
@@ -91,7 +89,7 @@ abstract contract Setup is Base_Test_ {
         susde = IStakedUSDe(address(new MockSUSDE(address(usde), governor)));
 
         // Deploy mock Morpho Market.
-        morpho = ERC4626(address(new MockERC4626(ERC20(address(usde)), "Morpho USDe Market", "morpho-USDe")));
+        morpho = new MockMorpho(address(usde));
     }
 
     function _deployContracts() internal virtual {
@@ -248,7 +246,7 @@ abstract contract Setup is Base_Test_ {
 
         // Same for morpho contract.
         usde.approve(address(morpho), 1_000_000 ether);
-        ERC4626(morpho).deposit(1_000_000 ether, dead);
+        morpho.deposit(1_000_000 ether, dead);
         vm.stopPrank();
 
         // Set initial prices in the ARM.
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 24057522..a39df477 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -54,6 +54,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [x] Deposit
     // [x] Withdraw
     // [x] TransferInRewards
+    // [x] SetUtilizationRate
+    //
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                   ✦✦✦  ✦✦✦                                   ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
@@ -364,4 +366,14 @@ abstract contract TargetFunctions is Setup, StdUtils {
             console.log(">>> Morpho Rewards:\t Transferred in %18e USDe as rewards, bps: %d", rewards, bps);
         }
     }
+
+    function targetMorphoSetUtilizationRate(uint256 utilizationRatePct) external {
+        utilizationRatePct = _bound(utilizationRatePct, 0, 100);
+
+        morpho.setUtilizationRate(utilizationRatePct * 1e16);
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> Morpho UseRate:\t Governor set utilization rate to %s%", utilizationRatePct);
+        }
+    }
 }
diff --git a/test/invariants/EthenaARM/mocks/MockMorpho.sol b/test/invariants/EthenaARM/mocks/MockMorpho.sol
new file mode 100644
index 00000000..38ce877a
--- /dev/null
+++ b/test/invariants/EthenaARM/mocks/MockMorpho.sol
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+// Solmate
+import {ERC20} from "@solmate/tokens/ERC20.sol";
+import {ERC4626} from "@solmate/mixins/ERC4626.sol";
+
+contract MockMorpho is ERC4626 {
+    //////////////////////////////////////////////////////
+    /// --- STATE VARIABLES
+    //////////////////////////////////////////////////////
+    uint256 public utilizationRate;
+
+    //////////////////////////////////////////////////////
+    /// --- EVENTS
+    //////////////////////////////////////////////////////
+    event UtilizationRateChanged(uint256 oldUtilizationRate, uint256 newUtilizationRate);
+
+    //////////////////////////////////////////////////////
+    /// --- CONSTRUCTOR
+    //////////////////////////////////////////////////////
+    constructor(address _underlying) ERC4626(ERC20(_underlying), "Mock Morpho Blue", "Mock Morpho Blue") {}
+
+    //////////////////////////////////////////////////////
+    /// --- VIEW FUNCTIONS
+    //////////////////////////////////////////////////////
+    function totalAssets() public view override returns (uint256) {
+        return asset.balanceOf(address(this));
+    }
+
+    function maxWithdraw(address owner) public view override returns (uint256) {
+        uint256 remainingLiquidity = totalAssets() * (1e18 - utilizationRate) / 1e18;
+        uint256 userLiquidity = convertToAssets(balanceOf[owner]);
+        return userLiquidity > remainingLiquidity ? remainingLiquidity : userLiquidity;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- MUTATIVE FUNCTIONS
+    //////////////////////////////////////////////////////
+    function setUtilizationRate(uint256 _utilizationRate) external {
+        emit UtilizationRateChanged(utilizationRate, _utilizationRate);
+        utilizationRate = _utilizationRate;
+    }
+}

From 926716ea1946f642ca1f3ee182be1542f6da5aba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 16:15:03 +0100
Subject: [PATCH 17/28] Fix claimable request check in Find library by updating
 variable usage

---
 test/invariants/EthenaARM/helpers/Find.sol | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/invariants/EthenaARM/helpers/Find.sol b/test/invariants/EthenaARM/helpers/Find.sol
index 20b25623..8730206d 100644
--- a/test/invariants/EthenaARM/helpers/Find.sol
+++ b/test/invariants/EthenaARM/helpers/Find.sol
@@ -27,9 +27,9 @@ library Find {
                 // Take a random request from that user
                 uint256 _requestId = pendingRequests[_user][($.randomArrayIndex + j) % pendingRequests[_user].length];
                 // Check request data
-                (,, uint40 _claimTimestamp, uint128 _amount,) = AbstractARM($.arm).withdrawalRequests(_requestId);
+                (,, uint40 _claimTimestamp,, uint128 _queued) = AbstractARM($.arm).withdrawalRequests(_requestId);
                 // Check if this is claimable
-                if (_amount <= $.targetAmount) {
+                if (_queued <= $.targetAmount) {
                     (user, requestId, claimTimestamp) = (_user, _requestId, _claimTimestamp);
                     // Remove pendingRequests
                     pendingRequests[_user][($.randomArrayIndex + j) % pendingRequests[_user].length] =

From 05a6ffed3a77195bfcfd203526c64005173a826f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 16:15:26 +0100
Subject: [PATCH 18/28] Make MockMorpho more realistic

---
 test/invariants/EthenaARM/mocks/MockMorpho.sol | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/test/invariants/EthenaARM/mocks/MockMorpho.sol b/test/invariants/EthenaARM/mocks/MockMorpho.sol
index 38ce877a..e15f762a 100644
--- a/test/invariants/EthenaARM/mocks/MockMorpho.sol
+++ b/test/invariants/EthenaARM/mocks/MockMorpho.sol
@@ -29,11 +29,19 @@ contract MockMorpho is ERC4626 {
     }
 
     function maxWithdraw(address owner) public view override returns (uint256) {
-        uint256 remainingLiquidity = totalAssets() * (1e18 - utilizationRate) / 1e18;
+        uint256 remainingLiquidity = availableLiquidity();
         uint256 userLiquidity = convertToAssets(balanceOf[owner]);
         return userLiquidity > remainingLiquidity ? remainingLiquidity : userLiquidity;
     }
 
+    function beforeWithdraw(uint256 assets, uint256) internal view override {
+        require(assets <= availableLiquidity(), "INSUFFICIENT_LIQUIDITY");
+    }
+
+    function availableLiquidity() public view returns (uint256) {
+        return totalAssets() * (1e18 - utilizationRate) / 1e18;
+    }
+
     //////////////////////////////////////////////////////
     /// --- MUTATIVE FUNCTIONS
     //////////////////////////////////////////////////////

From 90c0d215ac629bfde1a8b24f99d0ef28b2104fd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 16:49:00 +0100
Subject: [PATCH 19/28] Add target functions for allocate liquidity on ARM.

---
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  5 +-
 test/invariants/EthenaARM/Setup.sol           |  8 ++
 test/invariants/EthenaARM/TargetFunctions.sol | 77 +++++++++++++++++--
 .../invariants/EthenaARM/mocks/MockMorpho.sol |  6 ++
 4 files changed, 88 insertions(+), 8 deletions(-)

diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 0b45e932..b0705ff3 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](11);
+        bytes4[] memory selectors = new bytes4[](14);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -44,6 +44,9 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         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;
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
     }
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
index 17f8668d..6803659e 100644
--- a/test/invariants/EthenaARM/Setup.sol
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -254,6 +254,10 @@ abstract contract Setup is Base_Test_ {
         arm.setCrossPrice(0.9998e36);
         vm.prank(operator);
         arm.setPrices(0.9992e36, 0.9999e36);
+        address[] memory markets = new address[](1);
+        markets[0] = address(market);
+        vm.prank(governor);
+        arm.addMarkets(markets);
 
         // Grace will only deposit/withdraw USDe from/to sUSDe.
         vm.prank(grace);
@@ -292,6 +296,10 @@ abstract contract Setup is Base_Test_ {
         }
     }
 
+    function abs(int256 x) internal pure returns (uint256) {
+        return uint256(x >= 0 ? x : -x);
+    }
+
     modifier ensureTimeIncrease() {
         uint256 oldTimestamp = block.timestamp;
         _;
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index a39df477..4f3d6777 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -26,7 +26,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [ ] SwapExactTokensForTokens
     // [ ] SwapTokensForExactTokens
     // [x] Deposit
-    // [ ] Allocate
+    // [x] Allocate
     // [ ] CollectFees
     // [x] RequestRedeem
     // [x] ClaimRedeem
@@ -36,8 +36,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [ ] SetPrices
     // [ ] SetCrossPrice
     // [ ] SetFee
-    // [ ] SetActiveMarket
-    // [ ] SetARMBuffer
+    // [x] SetActiveMarket
+    // [x] SetARMBuffer
     //
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
@@ -187,6 +187,65 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
+    function targetARMSetARMBuffer(uint256 pct) external {
+        pct = _bound(pct, 0, 100);
+
+        vm.prank(operator);
+        arm.setARMBuffer(pct * 1e16);
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> ARM Buffer:\t Governor set ARM buffer to %s%", pct);
+        }
+    }
+
+    function targetARMSetActiveMarket(bool isActive) external {
+        // If isActive is true it will `setActiveMarket` with MorphoMarket
+        // else it will set it to address(0)
+        address currentMarket = arm.activeMarket();
+        address targetMarket = isActive ? address(market) : address(0);
+
+        // If the current market is the morpho market and we want to deactivate it
+        // ensure the is enough liquidity in Morpho to cover the ARM's assets withdrawals
+        if (currentMarket == address(market) && !isActive) {
+            uint256 shares = market.balanceOf(address(arm));
+            uint256 assets = market.convertToAssets(shares);
+            uint256 availableLiquidity = morpho.availableLiquidity();
+            if (assume(assets < availableLiquidity)) return;
+        }
+
+        vm.prank(operator);
+        arm.setActiveMarket(targetMarket);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> ARM SetMarket:\t Governor set active market to %s", isActive ? "Morpho Market" : "No active market"
+            );
+        }
+    }
+
+    function targetARMAllocate() external {
+        address currentMarket = arm.activeMarket();
+        if (assume(currentMarket != address(0))) return;
+
+        (int256 targetLiquidityDelta, int256 actualLiquidityDelta) = arm.allocate();
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                string(
+                    abi.encodePacked(
+                        ">>> ARM Allocate:\t ARM allocated liquidity to active market. Target delta: ",
+                        targetLiquidityDelta < 0 ? "-" : "",
+                        "%18e USDe\t Actual delta: ",
+                        actualLiquidityDelta < 0 ? "-" : "",
+                        "%18e USDe"
+                    )
+                ),
+                abs(targetLiquidityDelta),
+                abs(actualLiquidityDelta)
+            );
+        }
+    }
+
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
@@ -344,6 +403,10 @@ abstract contract TargetFunctions is Setup, StdUtils {
         // Bound shareAmount to [1, balance]
         amount = uint88(_bound(amount, 1, balance));
 
+        // Ensure there is enough liquidity to withdraw the amount
+        uint256 maxWithdrawable = morpho.maxWithdraw(harry);
+        if (assume(amount <= maxWithdrawable)) return;
+
         // Withdraw as harry
         vm.prank(harry);
         uint256 shares = morpho.withdraw(amount, harry, harry);
@@ -367,13 +430,13 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
-    function targetMorphoSetUtilizationRate(uint256 utilizationRatePct) external {
-        utilizationRatePct = _bound(utilizationRatePct, 0, 100);
+    function targetMorphoSetUtilizationRate(uint256 pct) external {
+        pct = _bound(pct, 0, 100);
 
-        morpho.setUtilizationRate(utilizationRatePct * 1e16);
+        morpho.setUtilizationRate(pct * 1e16);
 
         if (this.isConsoleAvailable()) {
-            console.log(">>> Morpho UseRate:\t Governor set utilization rate to %s%", utilizationRatePct);
+            console.log(">>> Morpho UseRate:\t Governor set utilization rate to %s%", pct);
         }
     }
 }
diff --git a/test/invariants/EthenaARM/mocks/MockMorpho.sol b/test/invariants/EthenaARM/mocks/MockMorpho.sol
index e15f762a..32a5dc17 100644
--- a/test/invariants/EthenaARM/mocks/MockMorpho.sol
+++ b/test/invariants/EthenaARM/mocks/MockMorpho.sol
@@ -34,6 +34,12 @@ contract MockMorpho is ERC4626 {
         return userLiquidity > remainingLiquidity ? remainingLiquidity : userLiquidity;
     }
 
+    function maxRedeem(address owner) public view override returns (uint256) {
+        uint256 maxRedeemableShares = convertToShares(availableLiquidity());
+        uint256 userShares = balanceOf[owner];
+        return userShares > maxRedeemableShares ? maxRedeemableShares : userShares;
+    }
+
     function beforeWithdraw(uint256 assets, uint256) internal view override {
         require(assets <= availableLiquidity(), "INSUFFICIENT_LIQUIDITY");
     }

From 65201c362a7105ba22cf082f7d96060e0555e8f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Wed, 19 Nov 2025 17:18:50 +0100
Subject: [PATCH 20/28] Add target function for setting prices in
 TargetFunctions contract

---
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  3 ++-
 test/invariants/EthenaARM/TargetFunctions.sol | 22 ++++++++++++++++++-
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index b0705ff3..42b61a6a 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](14);
+        bytes4[] memory selectors = new bytes4[](15);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -47,6 +47,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         selectors[11] = this.targetARMSetARMBuffer.selector;
         selectors[12] = this.targetARMSetActiveMarket.selector;
         selectors[13] = this.targetARMAllocate.selector;
+        selectors[14] = this.targetARMSetPrices.selector;
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
     }
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index 4f3d6777..f1b9e262 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -33,7 +33,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [ ] RequestBaseWithdrawal
     // [ ] ClaimBaseWithdrawals
     // --- Admin functions
-    // [ ] SetPrices
+    // [x] SetPrices
     // [ ] SetCrossPrice
     // [ ] SetFee
     // [x] SetActiveMarket
@@ -246,6 +246,26 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
+    function targetARMSetPrices(uint256 buyPrice, uint256 sellPrice) external {
+        uint256 crossPrice = arm.crossPrice();
+        // Bound sellPrice
+        sellPrice = uint120(_bound(sellPrice, crossPrice, (1e37 - 1) / 9)); // -> min traderate0 -> 0.9e36
+        // Bound buyPrice
+        buyPrice = uint120(_bound(buyPrice, 0.9e36, crossPrice - 1)); // -> min traderate1 -> 0.9e36
+
+        vm.prank(operator);
+        arm.setPrices(buyPrice, sellPrice);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> ARM SetPrices:\t Governor set buy price to %36e\t sell price to %36e\t cross price to %36e",
+                buyPrice,
+                1e72 / sellPrice,
+                arm.crossPrice()
+            );
+        }
+    }
+
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝

From 325373fbd0e83e78409044c9327dea5950a56ce9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Thu, 20 Nov 2025 16:17:08 +0100
Subject: [PATCH 21/28] add target functions for swaps

---
 test/invariants/EthenaARM/FoundryFuzzer.sol   |   5 +-
 test/invariants/EthenaARM/Setup.sol           |   9 +
 test/invariants/EthenaARM/TargetFunctions.sol | 160 +++++++++++++++++-
 3 files changed, 170 insertions(+), 4 deletions(-)

diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 42b61a6a..f8ac843b 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](15);
+        bytes4[] memory selectors = new bytes4[](18);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -48,6 +48,9 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         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;
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
     }
diff --git a/test/invariants/EthenaARM/Setup.sol b/test/invariants/EthenaARM/Setup.sol
index 6803659e..584fffa3 100644
--- a/test/invariants/EthenaARM/Setup.sol
+++ b/test/invariants/EthenaARM/Setup.sol
@@ -280,6 +280,7 @@ abstract contract Setup is Base_Test_ {
         for (uint256 i; i < TRADERS_COUNT; i++) {
             vm.startPrank(traders[i]);
             usde.approve(address(arm), type(uint256).max);
+            usde.approve(address(susde), type(uint256).max);
             susde.approve(address(arm), type(uint256).max);
             vm.stopPrank();
         }
@@ -300,6 +301,14 @@ abstract contract Setup is Base_Test_ {
         return uint256(x >= 0 ? x : -x);
     }
 
+    function max(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a >= b ? a : b;
+    }
+
+    function min(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a <= b ? a : b;
+    }
+
     modifier ensureTimeIncrease() {
         uint256 oldTimestamp = block.timestamp;
         _;
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index f1b9e262..c8c7dcb6 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -11,6 +11,7 @@ import {StdStyle} from "forge-std/StdStyle.sol";
 import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
 
 // Contracts
+import {IERC20} from "contracts/Interfaces.sol";
 import {UserCooldown} from "contracts/Interfaces.sol";
 
 // Helpers
@@ -23,8 +24,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                              ✦✦✦ ETHENA ARM ✦✦✦                              ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
-    // [ ] SwapExactTokensForTokens
-    // [ ] SwapTokensForExactTokens
+    // [x] SwapExactTokensForTokens
+    // [x] SwapTokensForExactTokens
     // [x] Deposit
     // [x] Allocate
     // [ ] CollectFees
@@ -34,7 +35,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [ ] ClaimBaseWithdrawals
     // --- Admin functions
     // [x] SetPrices
-    // [ ] SetCrossPrice
+    // [x] SetCrossPrice
     // [ ] SetFee
     // [x] SetActiveMarket
     // [x] SetARMBuffer
@@ -266,6 +267,159 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
+    function targetARMSetCrossPrice(uint256 crossPrice) external {
+        uint256 maxCrossPrice = 1e36;
+        uint256 minCrossPrice = 1e36 - 20e32;
+        uint256 sellT1 = 1e72 / (arm.traderate0());
+        uint256 buyT1 = arm.traderate1() + 1;
+        minCrossPrice = max(minCrossPrice, buyT1);
+        maxCrossPrice = min(maxCrossPrice, sellT1);
+        if (assume(maxCrossPrice >= minCrossPrice)) return;
+        crossPrice = _bound(crossPrice, minCrossPrice, maxCrossPrice);
+
+        if (arm.crossPrice() > crossPrice) {
+            if (assume(susde.balanceOf(address(arm)) < 1e12)) return;
+        }
+
+        vm.prank(governor);
+        arm.setCrossPrice(crossPrice);
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> ARM SetCPrice:\t Governor set cross price to %36e", crossPrice);
+        }
+    }
+
+    function targetARMSwapExactTokensForTokens(bool token0ForToken1, uint88 amountIn, uint256 randomAddressIndex)
+        external
+    {
+        (IERC20 tokenIn, IERC20 tokenOut) = token0ForToken1
+            ? (IERC20(address(usde)), IERC20(address(susde)))
+            : (IERC20(address(susde)), IERC20(address(usde)));
+
+        // What's the maximum amountOut we can obtain?
+        uint256 maxAmountOut;
+        if (address(tokenOut) == address(usde)) {
+            uint256 balance = usde.balanceOf(address(arm));
+            uint256 outstandingWithdrawals = arm.withdrawsQueued() - arm.withdrawsClaimed();
+            maxAmountOut = outstandingWithdrawals >= balance ? 0 : balance - outstandingWithdrawals;
+        } else {
+            maxAmountOut = susde.balanceOf(address(arm));
+        }
+        // Ensure there is liquidity available in ARM
+        if (assume(maxAmountOut > 1)) return;
+
+        // What's the maximum amountIn we can provide to not exceed maxAmountOut?
+        uint256 maxAmountIn = token0ForToken1
+            ? (maxAmountOut * 1e36 / arm.traderate0()) * susde.totalAssets() / susde.totalSupply()
+            : (maxAmountOut * 1e36 / arm.traderate1()) * susde.totalSupply() / susde.totalAssets();
+        if (assume(maxAmountIn > 0)) return;
+
+        // Bound amountIn
+        amountIn = uint88(_bound(amountIn, 1, maxAmountIn));
+        // Select a random user from makers
+        address user = traders[randomAddressIndex % TRADERS_COUNT];
+
+        vm.startPrank(user);
+        // Mint amountIn to user
+        if (token0ForToken1) {
+            MockERC20(address(usde)).mint(user, amountIn);
+        } else {
+            // Mint too much USDe to user to be able to mint enough sUSDe
+            MockERC20(address(usde)).mint(user, uint256(amountIn) * 10);
+            // Mint sUSDe to user
+            susde.mint(amountIn, user);
+            // Burn excess USDe
+            MockERC20(address(usde)).burn(user, usde.balanceOf(user));
+        }
+        // Perform swap
+        uint256[] memory obtained = arm.swapExactTokensForTokens(tokenIn, tokenOut, amountIn, 0, user);
+        vm.stopPrank();
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                string(
+                    abi.encodePacked(
+                        ">>> ARM SwapEF:\t ",
+                        vm.getLabel(user),
+                        " swapped %18e ",
+                        token0ForToken1 ? "USDe" : "sUSDe",
+                        "\t for %18e ",
+                        token0ForToken1 ? "sUSDe" : "USDe"
+                    )
+                ),
+                amountIn,
+                obtained[1]
+            );
+        }
+    }
+
+    function targetARMSwapTokensForExactTokens(bool token0ForToken1, uint88 amountOut, uint256 randomAddressIndex)
+        external
+    {
+        (IERC20 tokenIn, IERC20 tokenOut) = token0ForToken1
+            ? (IERC20(address(usde)), IERC20(address(susde)))
+            : (IERC20(address(susde)), IERC20(address(usde)));
+
+        // What's the maximum amountOut we can obtain?
+        uint256 maxAmountOut;
+        if (address(tokenOut) == address(usde)) {
+            uint256 balance = usde.balanceOf(address(arm));
+            uint256 outstandingWithdrawals = arm.withdrawsQueued() - arm.withdrawsClaimed();
+            maxAmountOut = outstandingWithdrawals >= balance ? 0 : balance - outstandingWithdrawals;
+        } else {
+            maxAmountOut = susde.balanceOf(address(arm));
+        }
+        // Ensure there is liquidity available in ARM
+        if (assume(maxAmountOut > 1)) return;
+
+        amountOut = uint88(_bound(amountOut, 1, maxAmountOut));
+
+        // What's the maximum amountIn we can provide to not exceed maxAmountOut?
+        uint256 convertedAmountOut;
+        if (token0ForToken1) {
+            convertedAmountOut = (amountOut * susde.totalAssets()) / susde.totalSupply();
+        } else {
+            convertedAmountOut = (amountOut * susde.totalSupply()) / susde.totalAssets();
+        }
+        uint256 price = token0ForToken1 ? arm.traderate0() : arm.traderate1();
+        uint256 amountIn = ((uint256(convertedAmountOut) * 1e36) / price) + 3 + 10; // slippage + rounding buffer
+
+        // Select a random user from makers
+        address user = traders[randomAddressIndex % TRADERS_COUNT];
+        vm.startPrank(user);
+        // Mint amountIn to user
+        if (token0ForToken1) {
+            MockERC20(address(usde)).mint(user, amountIn);
+        } else {
+            // Mint too much USDe to user to be able to mint enough sUSDe
+            MockERC20(address(usde)).mint(user, amountIn * 2);
+            // Mint sUSDe to user
+            susde.mint(amountIn, user);
+            // Burn excess USDe
+            MockERC20(address(usde)).burn(user, usde.balanceOf(user));
+        }
+        // Perform swap
+        uint256[] memory spent = arm.swapTokensForExactTokens(tokenIn, tokenOut, amountOut, type(uint256).max, user);
+        vm.stopPrank();
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                string(
+                    abi.encodePacked(
+                        ">>> ARM SwapFT:\t ",
+                        vm.getLabel(user),
+                        " swapped %18e ",
+                        token0ForToken1 ? "USDe" : "sUSDe",
+                        "\t for %18e ",
+                        token0ForToken1 ? "sUSDe" : "USDe"
+                    )
+                ),
+                spent[0],
+                amountOut
+            );
+        }
+    }
+
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝

From 5b7e924866ceee7cf8c369bd5dcac5c93fc11e1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Thu, 20 Nov 2025 17:40:42 +0100
Subject: [PATCH 22/28] Fix ClaimRequest checks

---
 test/invariants/EthenaARM/helpers/Find.sol | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/test/invariants/EthenaARM/helpers/Find.sol b/test/invariants/EthenaARM/helpers/Find.sol
index 8730206d..385b2bdc 100644
--- a/test/invariants/EthenaARM/helpers/Find.sol
+++ b/test/invariants/EthenaARM/helpers/Find.sol
@@ -11,25 +11,26 @@ library Find {
         uint248 randomAddressIndex;
         uint248 randomArrayIndex;
         address[] users;
-        uint256 targetAmount;
+        uint128 claimable;
+        uint128 availableLiquidity;
     }
 
     function getUserRequestWithAmount(
         GetUserRequestWithAmountStruct memory $,
         mapping(address => uint256[]) storage pendingRequests
     ) internal returns (address user, uint256 requestId, uint40 claimTimestamp) {
-        uint256 usersLen = $.users.length;
-        for (uint256 i; i < usersLen; i++) {
+        for (uint256 i; i < $.users.length; i++) {
             // Take a random user
-            address _user = $.users[($.randomAddressIndex + i) % usersLen];
+            address _user = $.users[($.randomAddressIndex + i) % $.users.length];
             // Find a request that can be claimed
             for (uint256 j; j < pendingRequests[_user].length; j++) {
                 // Take a random request from that user
                 uint256 _requestId = pendingRequests[_user][($.randomArrayIndex + j) % pendingRequests[_user].length];
                 // Check request data
-                (,, uint40 _claimTimestamp,, uint128 _queued) = AbstractARM($.arm).withdrawalRequests(_requestId);
+                (,, uint40 _claimTimestamp, uint128 _amount, uint128 _queued) =
+                    AbstractARM($.arm).withdrawalRequests(_requestId);
                 // Check if this is claimable
-                if (_queued <= $.targetAmount) {
+                if (_queued <= $.claimable && _amount <= $.availableLiquidity) {
                     (user, requestId, claimTimestamp) = (_user, _requestId, _claimTimestamp);
                     // Remove pendingRequests
                     pendingRequests[_user][($.randomArrayIndex + j) % pendingRequests[_user].length] =

From a69a91c5ee3625f6d6fc18b55e1c79a56cbaa0db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Thu, 20 Nov 2025 17:40:50 +0100
Subject: [PATCH 23/28] Add target for fees management

---
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  4 +-
 test/invariants/EthenaARM/TargetFunctions.sol | 47 +++++++++++++++++--
 2 files changed, 47 insertions(+), 4 deletions(-)

diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index f8ac843b..d1f50acd 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](18);
+        bytes4[] memory selectors = new bytes4[](20);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -51,6 +51,8 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         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;
         // Target selectors
         targetSelector(FuzzSelector({addr: address(this), selectors: selectors}));
     }
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index c8c7dcb6..ef365ba2 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -12,6 +12,7 @@ import {MockERC20} from "@solmate/test/utils/mocks/MockERC20.sol";
 
 // Contracts
 import {IERC20} from "contracts/Interfaces.sol";
+import {IERC4626} from "contracts/Interfaces.sol";
 import {UserCooldown} from "contracts/Interfaces.sol";
 
 // Helpers
@@ -28,7 +29,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [x] SwapTokensForExactTokens
     // [x] Deposit
     // [x] Allocate
-    // [ ] CollectFees
+    // [x] CollectFees
     // [x] RequestRedeem
     // [x] ClaimRedeem
     // [ ] RequestBaseWithdrawal
@@ -36,7 +37,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // --- Admin functions
     // [x] SetPrices
     // [x] SetCrossPrice
-    // [ ] SetFee
+    // [x] SetFee
     // [x] SetActiveMarket
     // [x] SetARMBuffer
     //
@@ -133,6 +134,11 @@ abstract contract TargetFunctions is Setup, StdUtils {
         uint256 requestId;
         uint256 claimTimestamp;
         uint256 claimable = arm.claimable();
+        uint256 availableLiquidity = usde.balanceOf(address(arm));
+        address market = arm.activeMarket();
+        if (market != address(0)) {
+            availableLiquidity += IERC4626(market).maxWithdraw(address(arm));
+        }
         if (assume(claimable != 0)) return;
         // Find a user with a pending request, where the amount is <= claimable
         {
@@ -142,7 +148,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
                     randomAddressIndex: randomAddressIndex,
                     randomArrayIndex: randomArrayIndex,
                     users: makers,
-                    targetAmount: claimable
+                    claimable: uint128(claimable),
+                    availableLiquidity: uint128(availableLiquidity)
                 }),
                 pendingRequests
             );
@@ -420,6 +427,40 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
+    function targetARMCollectFees() external {
+        uint256 fees = arm.feesAccrued();
+        uint256 balance = usde.balanceOf(address(arm));
+        uint256 outstandingWithdrawals = arm.withdrawsQueued() - arm.withdrawsClaimed();
+        if (assume(balance >= fees + outstandingWithdrawals)) return;
+
+        uint256 feesCollected = arm.collectFees();
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> ARM Collect:\t Governor collected %18e USDe in fees", feesCollected);
+        }
+        require(feesCollected == fees, "Fees collected mismatch");
+    }
+
+    function targetARMSetFees(uint256 fee) external {
+        // Ensure current fee can be collected
+        uint256 fees = arm.feesAccrued();
+        if (fees != 0) {
+            uint256 balance = usde.balanceOf(address(arm));
+            uint256 outstandingWithdrawals = arm.withdrawsQueued() - arm.withdrawsClaimed();
+            if (assume(balance >= fees + outstandingWithdrawals)) return;
+        }
+
+        uint256 oldFee = arm.fee();
+        // Bound fee to [0, 50%]
+        fee = _bound(fee, 0, 50);
+        vm.prank(governor);
+        arm.setFee(fee * 100);
+
+        if (this.isConsoleAvailable()) {
+            console.log(">>> ARM SetFees:\t Governor set ARM fee from %s% to %s%", oldFee / 100, fee);
+        }
+    }
+
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝

From e20d72bd2c55d78baabd4ace772b567eb745e23c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Fri, 21 Nov 2025 10:25:40 +0100
Subject: [PATCH 24/28] Add target functions for base request/claim withdraw

---
 test/invariants/EthenaARM/Base.sol            |   1 +
 test/invariants/EthenaARM/FoundryFuzzer.sol   |   4 +-
 test/invariants/EthenaARM/TargetFunctions.sol | 100 +++++++++++++++++-
 3 files changed, 102 insertions(+), 3 deletions(-)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index 2eb4ba40..f661e8f9 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -33,6 +33,7 @@ abstract contract Base_Test_ {
     MockMorpho public morpho;
     MorphoMarket public market;
     EthenaUnstaker[] public unstakers;
+    uint256[] public unstakerIndices;
 
     // --- Tokens ---
     IERC20 public usde;
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index d1f50acd..1b685903 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -29,7 +29,7 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         targetContract(address(this));
 
         // Add selectors
-        bytes4[] memory selectors = new bytes4[](20);
+        bytes4[] memory selectors = new bytes4[](22);
         // --- sUSDe ---
         selectors[0] = this.targetSUSDeDeposit.selector;
         selectors[1] = this.targetSUSDeCooldownShares.selector;
@@ -53,6 +53,8 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
         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}));
     }
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index ef365ba2..f4037a34 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -32,8 +32,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
     // [x] CollectFees
     // [x] RequestRedeem
     // [x] ClaimRedeem
-    // [ ] RequestBaseWithdrawal
-    // [ ] ClaimBaseWithdrawals
+    // [x] RequestBaseWithdrawal
+    // [x] ClaimBaseWithdrawals
     // --- Admin functions
     // [x] SetPrices
     // [x] SetCrossPrice
@@ -461,6 +461,102 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
     }
 
+    function targetARMRequestBaseWithdrawal(uint88 amount) external {
+        uint256 balance = susde.balanceOf(address(arm));
+        if (assume(balance > 1)) return;
+        amount = uint88(_bound(amount, 1, balance));
+
+        // Ensure there is an unstaker available
+        uint256 nextIndex = arm.nextUnstakerIndex();
+        address unstaker = arm.unstakers(nextIndex);
+        UserCooldown memory cooldown = susde.cooldowns(unstaker);
+        // If next unstaker has an active cooldown, this means all unstakers are in cooldown
+        // -> no unstaker available
+        if (assume(cooldown.underlyingAmount == 0)) return;
+
+        // Ensure time delay has passed
+        uint32 lastRequestTimestamp = arm.lastRequestTimestamp();
+        if (block.timestamp < lastRequestTimestamp + 3 hours) {
+            if (this.isConsoleAvailable()) {
+                console.log(
+                    StdStyle.yellow(
+                        string(
+                            abi.encodePacked(
+                                ">>> Time jump:\t Fast forwarded to: ",
+                                vm.toString(lastRequestTimestamp + 3 hours),
+                                "  (+ ",
+                                vm.toString((lastRequestTimestamp + 3 hours) - block.timestamp),
+                                "s)"
+                            )
+                        )
+                    )
+                );
+            }
+            vm.warp(lastRequestTimestamp + 3 hours);
+        }
+
+        vm.prank(operator);
+        arm.requestBaseWithdrawal(amount);
+
+        unstakerIndices.push(nextIndex);
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                ">>> ARM ReqBaseW:\t Operator requested base withdrawal of %18e sUSDe underlying, using unstakers #%s",
+                amount,
+                nextIndex
+            );
+        }
+    }
+
+    function targetARMClaimBaseWithdrawals(uint256 randomAddressIndex) external ensureTimeIncrease {
+        if (assume(unstakerIndices.length != 0)) return;
+        // Select a random unstaker index from used unstakers
+        uint256 selectedIndex = unstakerIndices[randomAddressIndex % unstakerIndices.length];
+        address unstaker = arm.unstakers(uint8(selectedIndex));
+        UserCooldown memory cooldown = susde.cooldowns(address(unstaker));
+        uint256 endTimestamp = cooldown.cooldownEnd;
+
+        // Fast forward time if needed
+        if (block.timestamp < endTimestamp) {
+            if (this.isConsoleAvailable()) {
+                console.log(
+                    StdStyle.yellow(
+                        string(
+                            abi.encodePacked(
+                                ">>> Time jump:\t Fast forwarded to: ",
+                                vm.toString(endTimestamp),
+                                "  (+ ",
+                                vm.toString(endTimestamp - block.timestamp),
+                                "s)"
+                            )
+                        )
+                    )
+                );
+            }
+            vm.warp(endTimestamp);
+        }
+
+        vm.prank(operator);
+        arm.claimBaseWithdrawals(unstaker);
+
+        // Remove selectedIndex from unstakerIndices, without preserving order
+        unstakerIndices[randomAddressIndex % unstakerIndices.length] = unstakerIndices[unstakerIndices.length - 1];
+        unstakerIndices.pop();
+
+        if (this.isConsoleAvailable()) {
+            console.log(
+                string(
+                    abi.encodePacked(
+                        ">>> ARM ClaimBaseW:\t Operator claimed base withdrawals using %s\t ", "who unstaked %18e USDe"
+                    )
+                ),
+                vm.getLabel(unstaker),
+                cooldown.underlyingAmount
+            );
+        }
+    }
+
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                                ✦✦✦ SUSDE ✦✦✦                                 ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝

From 010dbee89f88566acee1985a14b2ae959e4090c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Fri, 21 Nov 2025 15:42:11 +0100
Subject: [PATCH 25/28] Add Math library with utility functions for absolute
 values, min/max, and comparisons

---
 test/invariants/EthenaARM/helpers/Math.sol | 127 +++++++++++++++++++++
 1 file changed, 127 insertions(+)
 create mode 100644 test/invariants/EthenaARM/helpers/Math.sol

diff --git a/test/invariants/EthenaARM/helpers/Math.sol b/test/invariants/EthenaARM/helpers/Math.sol
new file mode 100644
index 00000000..18c1676d
--- /dev/null
+++ b/test/invariants/EthenaARM/helpers/Math.sol
@@ -0,0 +1,127 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.23;
+
+library Math {
+    //////////////////////////////////////////////////////
+    /// --- ABS
+    //////////////////////////////////////////////////////
+    /// @notice Returns the absolute value of an int256 as uint256
+    /// @param a The integer to get the absolute value of
+    /// @return The absolute value as uint256
+    function abs(int256 a) internal pure returns (uint256) {
+        return uint256(a >= 0 ? a : -a);
+    }
+
+    /// @notice Returns the absolute difference between two uint256 values
+    /// @param a The first value
+    /// @param b The second value
+    /// @return The absolute difference
+    function absDiff(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a >= b ? a - b : b - a;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- MIN & MAX
+    //////////////////////////////////////////////////////
+    /// @notice Returns the maximum of two uint256 values
+    /// @param a The first value
+    /// @param b The second value
+    /// @return The maximum value
+    function max(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a >= b ? a : b;
+    }
+
+    /// @notice Returns the minimum of two uint256 values
+    /// @param a The first value
+    /// @param b The second value
+    /// @return The minimum value
+    function min(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a <= b ? a : b;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- EQUALITY STRICT AND APPROXIMATE
+    //////////////////////////////////////////////////////
+    /// @notice Checks if two uint256 values are equal
+    /// @param a The first value
+    /// @param b The second value
+    /// @return True if equal, false otherwise
+    function eq(uint256 a, uint256 b) internal pure returns (bool) {
+        return a == b;
+    }
+
+    /// @notice Checks if two uint256 values are approximately equal within a maximum absolute difference
+    /// @param a The first value
+    /// @param b The second value
+    /// @param maxDelta The maximum allowed absolute difference
+    /// @return True if approximately equal, false otherwise
+    function approxEqAbs(uint256 a, uint256 b, uint256 maxDelta) internal pure returns (bool) {
+        if (a >= b) {
+            return (a - b) <= maxDelta;
+        } else {
+            return (b - a) <= maxDelta;
+        }
+    }
+
+    /// @notice Checks if two uint256 values are approximately equal within a maximum relative difference (in WAD)
+    /// @param a The first value
+    /// @param b The second value
+    /// @param maxRelDeltaWAD The maximum allowed relative difference in WAD (1e18 = 100%)
+    /// @return True if approximately equal, false otherwise
+    function approxEqRel(uint256 a, uint256 b, uint256 maxRelDeltaWAD) internal pure returns (bool) {
+        if (a == b) {
+            return true;
+        }
+        uint256 _absDiff = a >= b ? a - b : b - a;
+        uint256 relDiffWAD = (_absDiff * 1 ether) / Math.max(a, b);
+        return relDiffWAD <= maxRelDeltaWAD;
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- GREATER THAN
+    //////////////////////////////////////////////////////
+    /// @notice Checks if a is greater than b
+    /// @param a The first value
+    /// @param b The second value
+    /// @return True if a > b, false otherwise
+    function gt(uint256 a, uint256 b) internal pure returns (bool) {
+        return a > b;
+    }
+
+    /// @notice Checks if a is greater than or equal to b
+    function gte(uint256 a, uint256 b) internal pure returns (bool) {
+        return a >= b;
+    }
+
+    /// @notice Checks if a is approximately greater than or equal to b within a maximum absolute difference
+    /// @param a The first value
+    /// @param b The second value
+    /// @param maxDelta The maximum allowed absolute difference
+    /// @return True if a is approximately greater than or equal to b, false otherwise
+    function approxGteAbs(uint256 a, uint256 b, uint256 maxDelta) internal pure returns (bool) {
+        if (a >= b) {
+            return true;
+        } else {
+            return (b - a) <= maxDelta;
+        }
+    }
+
+    //////////////////////////////////////////////////////
+    /// --- LESS THAN
+    //////////////////////////////////////////////////////
+    /// @notice Checks if a is less than b
+    /// @param a The first value
+    /// @param b The second value
+    /// @return True if a < b, false otherwise
+    function lt(uint256 a, uint256 b) internal pure returns (bool) {
+        return a < b;
+    }
+
+    /// @notice Checks if a is less than or equal to b
+    /// @param a The first value
+    /// @param b The second value
+    /// @return True if a <= b, false otherwise
+    function lte(uint256 a, uint256 b) internal pure returns (bool) {
+        return a <= b;
+    }
+}

From 972162cc8c7ebeb7fdc032c7c8ec8bb5e060eaae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Fri, 21 Nov 2025 15:42:32 +0100
Subject: [PATCH 26/28] Add ghost values

---
 test/invariants/EthenaARM/Base.sol            | 17 ++++++
 test/invariants/EthenaARM/TargetFunctions.sol | 60 +++++++++++++++++--
 2 files changed, 72 insertions(+), 5 deletions(-)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index f661e8f9..4c0b1e6d 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -82,5 +82,22 @@ abstract contract Base_Test_ {
     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 sumUSDeBaseRedeem;
+    uint256 public sumUSDeFeesCollected;
+    uint256 public sumUSDeMarketDeposit;
+    uint256 public sumUSDeMarketWithdraw;
+    // --- sUSDe values ---
+    uint256 public sumSUSDeSwapIn;
+    uint256 public sumSUSDeSwapOut;
+    uint256 public sumSUSDeBaseRedeem;
 }
 
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index f4037a34..f0aba047 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -89,6 +89,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 shares
             );
         }
+
+        sumUSDeUserDeposit += amount;
     }
 
     function targetARMRequestRedeem(uint88 shareAmount, uint248 randomAddressIndex) external {
@@ -177,6 +179,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
         }
 
         // Claim redeem as user
+        uint256 balanceBefore = usde.balanceOf(address(arm));
         vm.prank(user);
         uint256 amount = arm.claimRedeem(requestId);
 
@@ -193,6 +196,12 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 amount
             );
         }
+
+        sumUSDeUserRedeem += amount;
+        if (balanceBefore < amount) {
+            // This means we had to withdraw from market
+            sumUSDeMarketWithdraw += amount - balanceBefore;
+        }
     }
 
     function targetARMSetARMBuffer(uint256 pct) external {
@@ -221,14 +230,23 @@ abstract contract TargetFunctions is Setup, StdUtils {
             if (assume(assets < availableLiquidity)) return;
         }
 
+        uint256 balanceBefore = usde.balanceOf(address(arm));
         vm.prank(operator);
         arm.setActiveMarket(targetMarket);
+        uint256 balanceAfter = usde.balanceOf(address(arm));
 
         if (this.isConsoleAvailable()) {
             console.log(
                 ">>> ARM SetMarket:\t Governor set active market to %s", isActive ? "Morpho Market" : "No active market"
             );
         }
+
+        int256 diff = int256(balanceAfter) - int256(balanceBefore);
+        if (diff > 0) {
+            sumUSDeMarketWithdraw += uint256(diff);
+        } else {
+            sumUSDeMarketDeposit += uint256(-diff);
+        }
     }
 
     function targetARMAllocate() external {
@@ -252,6 +270,12 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 abs(actualLiquidityDelta)
             );
         }
+
+        if (actualLiquidityDelta > 0) {
+            sumUSDeMarketDeposit += uint256(actualLiquidityDelta);
+        } else {
+            sumUSDeMarketWithdraw += uint256(-actualLiquidityDelta);
+        }
     }
 
     function targetARMSetPrices(uint256 buyPrice, uint256 sellPrice) external {
@@ -358,6 +382,15 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 obtained[1]
             );
         }
+
+        require(obtained[0] == amountIn, "Amount in mismatch");
+        if (token0ForToken1) {
+            sumUSDeSwapIn += obtained[0];
+            sumSUSDeSwapOut += obtained[1];
+        } else {
+            sumSUSDeSwapIn += obtained[0];
+            sumUSDeSwapOut += obtained[1];
+        }
     }
 
     function targetARMSwapTokensForExactTokens(bool token0ForToken1, uint88 amountOut, uint256 randomAddressIndex)
@@ -406,7 +439,7 @@ abstract contract TargetFunctions is Setup, StdUtils {
             MockERC20(address(usde)).burn(user, usde.balanceOf(user));
         }
         // Perform swap
-        uint256[] memory spent = arm.swapTokensForExactTokens(tokenIn, tokenOut, amountOut, type(uint256).max, user);
+        uint256[] memory obtained = arm.swapTokensForExactTokens(tokenIn, tokenOut, amountOut, type(uint256).max, user);
         vm.stopPrank();
 
         if (this.isConsoleAvailable()) {
@@ -421,10 +454,19 @@ abstract contract TargetFunctions is Setup, StdUtils {
                         token0ForToken1 ? "sUSDe" : "USDe"
                     )
                 ),
-                spent[0],
+                obtained[0],
                 amountOut
             );
         }
+
+        require(obtained[1] == amountOut, "Amount out mismatch");
+        if (token0ForToken1) {
+            sumUSDeSwapIn += obtained[0];
+            sumSUSDeSwapOut += obtained[1];
+        } else {
+            sumSUSDeSwapIn += obtained[0];
+            sumUSDeSwapOut += obtained[1];
+        }
     }
 
     function targetARMCollectFees() external {
@@ -439,15 +481,17 @@ abstract contract TargetFunctions is Setup, StdUtils {
             console.log(">>> ARM Collect:\t Governor collected %18e USDe in fees", feesCollected);
         }
         require(feesCollected == fees, "Fees collected mismatch");
+
+        sumUSDeFeesCollected += feesCollected;
     }
 
     function targetARMSetFees(uint256 fee) external {
         // Ensure current fee can be collected
-        uint256 fees = arm.feesAccrued();
-        if (fees != 0) {
+        uint256 feesAccrued = arm.feesAccrued();
+        if (feesAccrued != 0) {
             uint256 balance = usde.balanceOf(address(arm));
             uint256 outstandingWithdrawals = arm.withdrawsQueued() - arm.withdrawsClaimed();
-            if (assume(balance >= fees + outstandingWithdrawals)) return;
+            if (assume(balance >= feesAccrued + outstandingWithdrawals)) return;
         }
 
         uint256 oldFee = arm.fee();
@@ -459,6 +503,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
         if (this.isConsoleAvailable()) {
             console.log(">>> ARM SetFees:\t Governor set ARM fee from %s% to %s%", oldFee / 100, fee);
         }
+
+        sumUSDeFeesCollected += feesAccrued;
     }
 
     function targetARMRequestBaseWithdrawal(uint88 amount) external {
@@ -507,6 +553,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 nextIndex
             );
         }
+
+        sumSUSDeBaseRedeem += amount;
     }
 
     function targetARMClaimBaseWithdrawals(uint256 randomAddressIndex) external ensureTimeIncrease {
@@ -555,6 +603,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 cooldown.underlyingAmount
             );
         }
+
+        sumUSDeBaseRedeem += cooldown.underlyingAmount;
     }
 
     // ╔══════════════════════════════════════════════════════════════════════════════╗

From 4376cac30c39dfcd5afe32a322a4d71df34b074d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Fri, 21 Nov 2025 15:42:47 +0100
Subject: [PATCH 27/28] Add initial swaps invariant

---
 test/invariants/EthenaARM/FoundryFuzzer.sol |  8 ++-
 test/invariants/EthenaARM/Properties.sol    | 57 ++++++++++++++++++++-
 2 files changed, 62 insertions(+), 3 deletions(-)

diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 1b685903..631c27e8 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -4,6 +4,7 @@ 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.
@@ -13,7 +14,7 @@ import {StdInvariant} from "forge-std/StdInvariant.sol";
 ///         - 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 {
+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;
@@ -62,5 +63,8 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant {
     //////////////////////////////////////////////////////
     /// --- INVARIANTS
     //////////////////////////////////////////////////////
-    function invariantA() public {}
+    function invariantA() public view {
+        assertTrue(propertyA());
+        assertTrue(propertyB());
+    }
 }
diff --git a/test/invariants/EthenaARM/Properties.sol b/test/invariants/EthenaARM/Properties.sol
index 84d39122..bfe48fed 100644
--- a/test/invariants/EthenaARM/Properties.sol
+++ b/test/invariants/EthenaARM/Properties.sol
@@ -1,9 +1,15 @@
 // 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:
@@ -12,4 +18,53 @@ import {TargetFunctions} from "./TargetFunctions.sol";
 ///         - 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 {}
+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
+    // [ ]
+    //
+    //
+
+    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));
+    }
+}

From cf1096720b668f2b88c9845636352a096f23a903 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clemmoller@gmail.com>
Date: Fri, 21 Nov 2025 17:39:16 +0100
Subject: [PATCH 28/28] implement properties

---
 test/invariants/EthenaARM/Base.sol            |   1 +
 test/invariants/EthenaARM/FoundryFuzzer.sol   |  11 +-
 test/invariants/EthenaARM/Properties.sol      | 126 ++++++++++++++----
 test/invariants/EthenaARM/TargetFunctions.sol |   8 +-
 4 files changed, 112 insertions(+), 34 deletions(-)

diff --git a/test/invariants/EthenaARM/Base.sol b/test/invariants/EthenaARM/Base.sol
index 4c0b1e6d..3612dc39 100644
--- a/test/invariants/EthenaARM/Base.sol
+++ b/test/invariants/EthenaARM/Base.sol
@@ -91,6 +91,7 @@ abstract contract Base_Test_ {
     uint256 public sumUSDeSwapOut;
     uint256 public sumUSDeUserDeposit;
     uint256 public sumUSDeUserRedeem;
+    uint256 public sumUSDeUserRequest;
     uint256 public sumUSDeBaseRedeem;
     uint256 public sumUSDeFeesCollected;
     uint256 public sumUSDeMarketDeposit;
diff --git a/test/invariants/EthenaARM/FoundryFuzzer.sol b/test/invariants/EthenaARM/FoundryFuzzer.sol
index 631c27e8..b9968794 100644
--- a/test/invariants/EthenaARM/FoundryFuzzer.sol
+++ b/test/invariants/EthenaARM/FoundryFuzzer.sol
@@ -64,7 +64,14 @@ contract FuzzerFoundry_EthenaARM is Properties, StdInvariant, StdAssertions {
     /// --- INVARIANTS
     //////////////////////////////////////////////////////
     function invariantA() public view {
-        assertTrue(propertyA());
-        assertTrue(propertyB());
+        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");
     }
 }
diff --git a/test/invariants/EthenaARM/Properties.sol b/test/invariants/EthenaARM/Properties.sol
index bfe48fed..89f4eea9 100644
--- a/test/invariants/EthenaARM/Properties.sol
+++ b/test/invariants/EthenaARM/Properties.sol
@@ -22,32 +22,45 @@ abstract contract Properties is TargetFunctions {
     // ╔══════════════════════════════════════════════════════════════════════════════╗
     // ║                           ✦✦✦ SWAP PROPERTIES ✦✦✦                            ║
     // ╚══════════════════════════════════════════════════════════════════════════════╝
-    // [ ] Invariant A: USDe  balance == (∑swapIn - ∑swapOut) + (∑userDeposit - ∑userWithdraw) + (∑marketWithdraw - ∑marketDeposit) + ∑baseRedeem - ∑feesCollected
+    // [ ] 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));
+        // 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));
     }
 
@@ -55,16 +68,71 @@ abstract contract Properties is TargetFunctions {
         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));
+        // 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);
+    }
 }
diff --git a/test/invariants/EthenaARM/TargetFunctions.sol b/test/invariants/EthenaARM/TargetFunctions.sol
index f0aba047..cd725b27 100644
--- a/test/invariants/EthenaARM/TargetFunctions.sol
+++ b/test/invariants/EthenaARM/TargetFunctions.sol
@@ -129,6 +129,8 @@ abstract contract TargetFunctions is Setup, StdUtils {
                 requestId
             );
         }
+
+        sumUSDeUserRequest += amount;
     }
 
     function targetARMClaimRedeem(uint248 randomAddressIndex, uint248 randomArrayIndex) external ensureTimeIncrease {
@@ -470,17 +472,17 @@ abstract contract TargetFunctions is Setup, StdUtils {
     }
 
     function targetARMCollectFees() external {
-        uint256 fees = arm.feesAccrued();
+        uint256 feesAccrued = arm.feesAccrued();
         uint256 balance = usde.balanceOf(address(arm));
         uint256 outstandingWithdrawals = arm.withdrawsQueued() - arm.withdrawsClaimed();
-        if (assume(balance >= fees + outstandingWithdrawals)) return;
+        if (assume(balance >= feesAccrued + outstandingWithdrawals)) return;
 
         uint256 feesCollected = arm.collectFees();
 
         if (this.isConsoleAvailable()) {
             console.log(">>> ARM Collect:\t Governor collected %18e USDe in fees", feesCollected);
         }
-        require(feesCollected == fees, "Fees collected mismatch");
+        require(feesCollected == feesAccrued, "Fees collected mismatch");
 
         sumUSDeFeesCollected += feesCollected;
     }