[Ethena ARM] - Invariant Testing

[clement-ux]

Description

• Add invariant campaign for EthenaARM.
• Add agnostic fuzzer setup for EthenaARM.
• Support Foundry and Medusa Fuzzer.
• Improve CI to support Medusa Fuzzer + split invariant repo runs.
• Increase fuzzing runs + depth when running on CI. Runs/depth prev: 256/500; new 1000/1000.

Invariants

Here is a list of all invariants tested:

// ╔══════════════════════════════════════════════════════════════════════════════╗
// ║                           ✦✦✦ SWAP PROPERTIES ✦✦✦                            ║
// ╚══════════════════════════════════════════════════════════════════════════════╝
// [x] Invariant A: USDe  balance == ∑swapIn - ∑swapOut
//                                   + ∑userDeposit - ∑userWithdraw
//                                   + ∑marketWithdraw - ∑marketDeposit
//                                   + ∑baseRedeem - ∑feesCollected
// [x] 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
//
// ╔══════════════════════════════════════════════════════════════════════════════╗
// ║                         ✦✦✦ LIQUIDITY MANAGEMENT ✦✦✦                         ║
// ╚══════════════════════════════════════════════════════════════════════════════╝
// [x] Invariant L: liquidityAmountInCooldown == ∑unstaker.underlyingAmount
// [x] Invariant M: nextUnstakerIndex < MAX_UNSTAKERS
// [x] Invariant N: ∀ unstaker, usde.balanceOf(unstaker) == 0 && susde.balanceOf(unstaker) == 0
//
// ╔══════════════════════════════════════════════════════════════════════════════╗
// ║                              ✦✦✦ AFTER ALL ✦✦✦                               ║
// ╚══════════════════════════════════════════════════════════════════════════════╝
// [x] sUSDe in ARM == 0
// [x] Morpho shares in ARM == 0
// [x] ∀ user, usde.balanceOf(user) >= totalMinted - 1e1
//
// ╔══════════════════════════════════════════════════════════════════════════════╗
// ║                                   ✦✦✦  ✦✦✦                                   ║
// ╚══════════════════════════════════════════════════════════════════════════════╝

[naddison36]

Awesome work