diff --git a/.github/workflows/run-forge-tests.yaml b/.github/workflows/run-forge-tests.yaml index 0337c84e0..d46bdb6e6 100644 --- a/.github/workflows/run-forge-tests.yaml +++ b/.github/workflows/run-forge-tests.yaml @@ -5,6 +5,9 @@ on: branches: - staging-2.5 - master + # 26Q2 Security Upgrades release branch: run the full suite (including the + # invariant layer) on PRs targeting it, not only when it lands on master. + - pankaj/feat/security-upgrades* workflow_dispatch: @@ -24,7 +27,12 @@ jobs: - name: Install Foundry uses: foundry-rs/foundry-toolchain@v1 with: - version: nightly + # Pinned stable release (matches local dev). `nightly` is a moving + # target and started enforcing the EIP-3860 initcode-size limit in + # tests, which reverts any `new` of a harness inheriting the large + # SecurityUpgradesScript (e.g. ForwardedCallWhitelistRegrant.t.sol) + # with a bare setUp EvmError while the same tests pass on stable. + version: v1.5.1 - name: Run tests run: forge test -vvv diff --git a/certora/config/LiquidityPoolDecomposition.conf b/certora/config/LiquidityPoolDecomposition.conf new file mode 100644 index 000000000..b254c6f04 --- /dev/null +++ b/certora/config/LiquidityPoolDecomposition.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "src/core/LiquidityPool.sol", + "src/core/EETH.sol" + ], + "link": [ + "LiquidityPool:eETH=EETH", + "EETH:liquidityPool=LiquidityPool" + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "@openzeppelin-upgradeable=lib/openzeppelin-contracts-upgradeable", + "@etherfi=src", + "solady=lib/solady/src", + "@eigenlayer-libraries=lib/eigenlayer-libraries" + ], + "verify": "LiquidityPool:certora/specs/LiquidityPoolDecomposition.spec", + "rule_sanity": "none", + "optimistic_loop": true, + "loop_iter": "3", + "msg": "LiquidityPool I9 pooled-ether decomposition lemma (tautological, so rule_sanity is disabled here)" +} diff --git a/certora/config/LiquidityPoolPeg.conf b/certora/config/LiquidityPoolPeg.conf new file mode 100644 index 000000000..ddc3c5d0b --- /dev/null +++ b/certora/config/LiquidityPoolPeg.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "src/core/LiquidityPool.sol", + "src/core/EETH.sol" + ], + "link": [ + "LiquidityPool:eETH=EETH", + "EETH:liquidityPool=LiquidityPool" + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "@openzeppelin-upgradeable=lib/openzeppelin-contracts-upgradeable", + "@etherfi=src", + "solady=lib/solady/src", + "@eigenlayer-libraries=lib/eigenlayer-libraries" + ], + "verify": "LiquidityPool:certora/specs/LiquidityPoolPeg.spec", + "rule_sanity": "basic", + "optimistic_loop": true, + "loop_iter": "3", + "msg": "LiquidityPool peg/solvency invariants I7 rate monotonicity and I8 LP solvency" +} diff --git a/certora/config/RoleRegistryAuthority.conf b/certora/config/RoleRegistryAuthority.conf new file mode 100644 index 000000000..022e803c2 --- /dev/null +++ b/certora/config/RoleRegistryAuthority.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "src/governance/RoleRegistry.sol" + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "@openzeppelin-upgradeable=lib/openzeppelin-contracts-upgradeable", + "solady=lib/solady/src", + "forge-std=lib/forge-std/src" + ], + "verify": "RoleRegistry:certora/specs/RoleRegistryAuthority.spec", + "rule_sanity": "basic", + "optimistic_loop": true, + "loop_iter": "3", + "msg": "RoleRegistry authority invariants I6 owner only role changes and revokeFast guards" +} diff --git a/certora/specs/LiquidityPoolDecomposition.spec b/certora/specs/LiquidityPoolDecomposition.spec new file mode 100644 index 000000000..f13d2974e --- /dev/null +++ b/certora/specs/LiquidityPoolDecomposition.spec @@ -0,0 +1,38 @@ +/* + * Certora CVL spec for ether.fi LiquidityPool — invariant I9 (pooled-ether decomposition). + * + * Split out of LiquidityPoolPeg.spec: I9 is a definitional tautology, so it is + * vacuously true and cannot survive `rule_sanity: basic`. It runs here on its own + * with `rule_sanity: none` (see LiquidityPoolDecomposition.conf) so that the peg + * spec can keep `rule_sanity: basic` for its genuinely non-vacuous rules I7/I8. + * + * I9 — pooled-ether decomposition: getTotalPooledEther() == in + out. + * A definitional helper that I7/I8 lean on. + */ + +using EETH as eeth; + +methods { + function totalValueInLp() external returns (uint128) envfree; + function totalValueOutOfLp() external returns (uint128) envfree; + function getTotalPooledEther() external returns (uint256) envfree; + function eeth.totalShares() external returns (uint256) envfree; + + // Resolve cross-contract totalShares() reads through the linked EETH. + function _.totalShares() external => DISPATCHER(true); +} + +// ---------------------------------------------------------------------------- +// I9 — pooled-ether decomposition lemma: P == in + out. +// +// DEFINITIONAL: getTotalPooledEther() (LiquidityPool.sol:729) literally returns +// `totalValueOutOfLp + totalValueInLp`, so this identity is true in EVERY state +// by construction. It is the cheap lemma I7/I8 lean on. Because the assert is a +// tautology, `rule_sanity` would (correctly) report it as vacuously true — that +// is exactly why this spec runs with `rule_sanity: none` in its own conf, apart +// from LiquidityPoolPeg.spec which keeps `rule_sanity: basic`. The invariant +// still proves the relation holds after every method, which is the assurance we +// want. +// ---------------------------------------------------------------------------- +invariant I9_pooled_ether_decomposition() + to_mathint(getTotalPooledEther()) == to_mathint(totalValueInLp()) + to_mathint(totalValueOutOfLp()); diff --git a/certora/specs/LiquidityPoolPeg.spec b/certora/specs/LiquidityPoolPeg.spec new file mode 100644 index 000000000..1a3dbb8c4 --- /dev/null +++ b/certora/specs/LiquidityPoolPeg.spec @@ -0,0 +1,148 @@ +/* + * Certora CVL spec for ether.fi LiquidityPool — peg/solvency invariants I7, I8. + * (I9, the pooled-ether decomposition lemma, lives in LiquidityPoolDecomposition.spec; + * it is a tautology and runs separately with `rule_sanity: none`.) + * + * Target: the SECURITY-UPGRADE LiquidityPool (carries `nonDecreasingRate` + + * `_checkTotalValueInLp`). These properties hold only OPERATIONALLY on live + * mainnet today; the upgrade codifies them. CVL proves them for ALL inputs + * (vs the stateful fuzzer, which samples). + * + * I7 — the `nonDecreasingRate` guard is correctly wired: on every entry point + * that carries the modifier, the post-rate is >= the pre-rate. Rate = P/S + * where P = getTotalPooledEther() = totalValueInLp + totalValueOutOfLp, + * S = eETH.totalShares(). Checked cross-multiplied (no division): + * P1 * S0 >= P0 * S1 (the `_checkRateNonDec` predicate). This is a + * regression check on the wiring, not a proof that share math can never + * dilute holders — the two by-design unguarded rate-moving paths + * (withdraw(uint256,uint256), rebase) are intentionally out of scope. + * + * I8 — LP-buffer solvency: totalValueInLp <= address(this).balance + * Enforced by `_checkTotalValueInLp()` (line 668) on every write path. + * + * NOTE: rate = P/S is NOT a stored variable; it is derived from two contracts + * (LiquidityPool P, EETH S). We capture P and S before/after so the prover + * reasons over the pair. + */ + +using EETH as eeth; + +methods { + function totalValueInLp() external returns (uint128) envfree; + function totalValueOutOfLp() external returns (uint128) envfree; + function getTotalPooledEther() external returns (uint256) envfree; + function eeth.totalShares() external returns (uint256) envfree; + + // Resolve cross-contract totalShares() reads through the linked EETH. + function _.totalShares() external => DISPATCHER(true); +} + +// ---------------------------------------------------------------------------- +// I8 — LP-buffer solvency, proved in the HONEST, provable form. +// +// `totalValueInLp <= address(this).balance` CANNOT be stated as a pure CVL +// `invariant`: an invariant must survive *every* method, including ones whose +// bodies make external calls to UNLINKED contracts (the eETH rate-limiter, the +// WithdrawRequestNFT, PriorityWithdrawalQueue, StakingManager, the arbitrary +// `_recipient.call` inside `_sendFund`). For those calls the Prover must HAVOC +// `address(this).balance`, which can drop it below `totalValueInLp` — a sound +// over-approximation, not a real reachable state. (That is exactly the set of +// methods the first run flagged: requestWithdraw*, withdraw(uint256,uint256), +// burnEEthShares*, upgradeToAndCall, and every EETH.* method.) +// +// The security property `_checkTotalValueInLp` actually delivers is: +// "any write path that ENDS in `_checkTotalValueInLp()` leaves the pool +// solvent, because the call reverts otherwise." +// In every guarded path the check is the LAST state-relevant statement (it runs +// AFTER the ETH send in `_sendFund` / `_lockEth` / `_accountForEthSentOut`), so +// it constrains the post-havoc balance. We therefore prove, per guarded method: +// method completes without reverting => totalValueInLp <= balance. +// +// Guarded write paths (each UNCONDITIONALLY reaches `_checkTotalValueInLp`, +// call sites at lines 175/189/274/594/651/662): +// deposit() / deposit(address) / deposit(address,address) / +// depositToRecipient -> _deposit -> 594 +// withdraw(address,uint256) -> 274 +// addEthAmountLockedForWithdrawal / transferLockedEthForPriority +// -> _lockEth -> 651 +// batchCreateBeaconValidators / confirmAndFundBeaconValidators +// -> _accountForEthSentOut -> 662 +// initializeOnUpgradeV2() -> 175 +// receive() -> 189 +// `receive()` IS covered: CVL exposes the receive/fallback dispatch as the +// parametric method with `f.isFallback == true`, so we include it in the filter +// (rather than by selector, which a fallback has no distinct value for). +// NOTE ON SCOPE: rebase() also transitively reaches the check (via +// depositToRecipient) but only WHEN _protocolFees > 0, so it does not +// unconditionally end in the check and is intentionally excluded — including it +// would let the prover start from an already-insolvent havoc state that rebase +// leaves untouched, a spurious counterexample. +// ---------------------------------------------------------------------------- +rule I8_lp_buffer_solvency_guarded(method f, env e, calldataarg args) + filtered { + f -> f.isFallback + || f.selector == sig:deposit().selector + || f.selector == sig:deposit(address).selector + || f.selector == sig:deposit(address,address).selector + || f.selector == sig:depositToRecipient(address,uint256,address).selector + || f.selector == sig:withdraw(address,uint256).selector + || f.selector == sig:addEthAmountLockedForWithdrawal(uint128).selector + || f.selector == sig:transferLockedEthForPriority(uint128).selector + || f.selector == sig:batchCreateBeaconValidators(IStakingManager.DepositData[],uint256[],address).selector + || f.selector == sig:confirmAndFundBeaconValidators(IStakingManager.DepositData[],uint256).selector + || f.selector == sig:initializeOnUpgradeV2().selector + } +{ + f@withrevert(e, args); + bool reverted = lastReverted; + + // If the method completed, `_checkTotalValueInLp()` did not revert, so the + // solvency relation held at the (final) check and nothing changes after it. + assert !reverted => + to_mathint(totalValueInLp()) <= to_mathint(nativeBalances[currentContract]), + "I8: LP buffer insolvent after a guarded write path (totalValueInLp > balance)"; +} + +// ---------------------------------------------------------------------------- +// I7 — the `nonDecreasingRate` guard is correctly wired on its entry points. +// +// This is regression protection for the modifier's wiring, NOT a proof that +// share math can never dilute holders: it asserts that on exactly the methods +// carrying `nonDecreasingRate`, the rate P/S does not decrease across the call. +// The two rate-moving paths that are unguarded BY DESIGN — withdraw(uint256, +// uint256) (frozen-rate finalized claim, bounded by that function's three-guard +// design) and rebase() (oracle path, bounded by EtherFiAdmin's APR cap) — are +// out of scope here on purpose. The filter below must stay in exact sync with +// the modifier sites in LiquidityPool.sol: withdraw(address,uint256):261, +// burnEEthShares:504, burnEEthSharesForNonETHWithdrawal:515, and _deposit:585 +// (reached by the four deposit entry points). +// +// Expressed cross-multiplied to avoid division and rounding: +// P_after * S_before >= P_before * S_after +// (bootstrap-exempt when either S is zero — no rate to compare, matching +// `_checkRateNonDec`'s `S0 != 0 && S1 != 0` guard). +// ---------------------------------------------------------------------------- +rule I7_rate_non_decreasing_on_guarded_methods(method f, env e, calldataarg args) + filtered { + f -> f.selector == sig:withdraw(address,uint256).selector + || f.selector == sig:burnEEthShares(uint256).selector + || f.selector == sig:burnEEthSharesForNonETHWithdrawal(uint256,uint256).selector + || f.selector == sig:deposit().selector + || f.selector == sig:deposit(address).selector + || f.selector == sig:deposit(address,address).selector + || f.selector == sig:depositToRecipient(address,uint256,address).selector + } +{ + uint256 P0 = getTotalPooledEther(); + uint256 S0 = eeth.totalShares(); + + f(e, args); + + uint256 P1 = getTotalPooledEther(); + uint256 S1 = eeth.totalShares(); + + // bootstrap exemption (mirrors _checkRateNonDec) + assert (S0 != 0 && S1 != 0) => + to_mathint(P1) * to_mathint(S0) >= to_mathint(P0) * to_mathint(S1), + "I7: exchange rate decreased across a nonDecreasingRate-guarded call"; +} diff --git a/certora/specs/RoleRegistryAuthority.spec b/certora/specs/RoleRegistryAuthority.spec new file mode 100644 index 000000000..98adf12cf --- /dev/null +++ b/certora/specs/RoleRegistryAuthority.spec @@ -0,0 +1,194 @@ +/* + * Certora CVL spec for ether.fi RoleRegistry — authority invariants (I6). + * + * I6 = authority-registry consistency / no unauthorized privilege change. + * RoleRegistry is Ownable2StepUpgradeable + UUPSUpgradeable + solady's + * EnumerableRoles. Role membership is stored by solady in a custom slot and + * read back through the public `hasRole` view. + * + * The two non-internal write paths to a role bit are: + * - setRole / grantRole / revokeRole : guarded by solady _authorizeSetRole, + * which reverts unless msg.sender == owner(). + * - revokeFast(role,account) : guarded by msg.sender == revokeAdmin, + * can ONLY clear a bit, and reverts on the 3 protected roles. + * + * =========================================================================== + * MODELLING NOTE — resolving solady's assembly self-staticcalls. + * solady's `_enumerableRolesSenderIsContractOwner` decides grant-path + * authorization by STATICCALLing owner() on address(this) from HAND-ROLLED + * ASSEMBLY (EnumerableRoles.sol:295-305), and `_validateRole` likewise + * STATICCALLs MAX_ROLE() (EnumerableRoles.sol:193-205). The Prover cannot + * recover the 4-byte selectors from that assembly calldata, reports "callee + * sighash unresolved", and AUTO-havocs the return values — which previously + * produced spurious "non-owner changed a role" counterexamples on + * grantRole/revokeRole/setRole. Modelling _authorizeSetRole with an + * INTERNAL-function CVL summary crashed the Prover backend (it interacts badly + * with solady's assembly storage writes). + * + * The sound fix is a DISPATCH list on the UNRESOLVED EXTERNAL calls (methods + * block). Both STATICCALLs target literally address(this), and the only + * external calls reachable inside setRole/grantRole/revokeRole are these two + * self-calls, so resolving them to currentContract.owner()/MAX_ROLE() is EXACT, + * not an over-approximation. `optimistic=true` drops the "no match" havoc + * branch that would otherwise re-introduce the spurious counterexample; the + * entry is scoped to the three grant-path methods ONLY, so upgradeToAndCall's + * delegatecall is left to the Prover's default handling. + * + * I6.1 revokeFast AUTHORITY: a successful revokeFast requires the immutable + * revokeAdmin — plain Solidity the Prover models natively. [VERIFIED] + * I6.2 revokeFast reverts on the 3 protected roles (InvalidRoleToRevoke is an + * explicit guard the Prover sees). [VERIFIED] + * I6.3 revokeFast never grants (false->true). [VERIFIED] + * I6.4 the owner-gated paths (grantRole/revokeRole/setRole) and revokeFast + * are the ONLY methods that can change a role bit — no OTHER method + * (transfers, views) mutates membership. Proven by filtering to + * all-other-methods and asserting no change. (upgradeToAndCall excluded: + * UUPS delegatecall havocs all storage, a modelling artifact, gated + * separately by onlyUpgradeTimelock — see I6.6.) [VERIFIED] + * I6.5 the owner-gated paths succeed ONLY for msg.sender == owner() — the + * grant-path authorization itself, provable directly thanks to the + * self-call dispatch above (no longer resting on solady's audit alone). + * I6.6 upgradeToAndCall succeeds ONLY for a caller holding + * UPGRADE_TIMELOCK_ROLE (_authorizeUpgrade/onlyUpgradeTimelock, + * RoleRegistry.sol:252-254); closes the one path I6.4 must exclude. + * =========================================================================== + */ + +methods { + function owner() external returns (address) envfree; + function revokeAdmin() external returns (address) envfree; + function hasRole(bytes32, address) external returns (bool) envfree; + + function UPGRADE_TIMELOCK_ROLE() external returns (bytes32) envfree; + function OPERATION_TIMELOCK_ROLE() external returns (bytes32) envfree; + function OPERATION_MULTISIG_ROLE() external returns (bytes32) envfree; + + // Resolve solady's two assembly self-STATICCALLs (see MODELLING NOTE): + // owner() in _authorizeSetRole and MAX_ROLE() in _validateRole. Both target + // address(this), and they are the ONLY external calls reachable inside the + // grant-path methods, so dispatching to currentContract.owner()/MAX_ROLE() + // is exact. optimistic=true removes the "no match" havoc branch that would + // otherwise re-create the spurious non-owner counterexample. Scoped to the + // three grant-path methods so upgradeToAndCall is left untouched. + unresolved external in currentContract.setRole(address,uint256,bool) => + DISPATCH(optimistic=true) [ currentContract.owner(), currentContract.MAX_ROLE() ]; + unresolved external in currentContract.grantRole(bytes32,address) => + DISPATCH(optimistic=true) [ currentContract.owner(), currentContract.MAX_ROLE() ]; + unresolved external in currentContract.revokeRole(bytes32,address) => + DISPATCH(optimistic=true) [ currentContract.owner(), currentContract.MAX_ROLE() ]; +} + +// ---------------------------------------------------------------------------- +// I6.4 NO STRAY MUTATION: only the role-management entry points +// (grantRole / revokeRole / setRole / revokeFast) may change a role bit. +// Every OTHER method must leave all (role,account) memberships unchanged. +// +// This is the registry-integrity property: no transfer, config, or view +// path can silently alter authority. upgradeToAndCall is excluded — a UUPS +// upgrade delegatecalls an arbitrary impl and the Prover havocs all storage +// (a modelling artifact, not a real grant); that path is gated by +// onlyUpgradeTimelock, a separate authority. Matches EtherFiOracle.spec. +// ---------------------------------------------------------------------------- +rule I6_only_role_mgmt_methods_change_membership(method f, env e, calldataarg args) + filtered { + f -> f.selector != sig:grantRole(bytes32,address).selector + && f.selector != sig:revokeRole(bytes32,address).selector + && f.selector != sig:setRole(address,uint256,bool).selector + && f.selector != sig:revokeFast(bytes32,address).selector + && f.selector != sig:upgradeToAndCall(address,bytes).selector + } +{ + bytes32 role; address account; + + bool before = hasRole(role, account); + f(e, args); + bool afterCall = hasRole(role, account); + + assert before == afterCall, + "I6.4: a non-role-management method changed role membership"; +} + +// ---------------------------------------------------------------------------- +// I6.5 OWNER-GATED WRITE PATHS: a successful grantRole / revokeRole / setRole +// requires msg.sender == owner(). This is the grant-path authorization +// solady enforces via _authorizeSetRole (owner-or-revert). It is provable +// here ONLY because the methods block resolves solady's owner()/MAX_ROLE() +// self-staticcalls (see MODELLING NOTE); without that resolution the Prover +// havocs the owner() return and reports spurious non-owner counterexamples. +// ---------------------------------------------------------------------------- +rule I6_owner_gated_paths_require_owner(method f, env e, calldataarg args) + filtered { + f -> f.selector == sig:grantRole(bytes32,address).selector + || f.selector == sig:revokeRole(bytes32,address).selector + || f.selector == sig:setRole(address,uint256,bool).selector + } +{ + f@withrevert(e, args); + + assert !lastReverted => e.msg.sender == owner(), + "I6.5: an owner-gated role change succeeded for a non-owner caller"; +} + +// ---------------------------------------------------------------------------- +// I6.6 UPGRADE AUTHORITY: a successful upgradeToAndCall requires msg.sender to +// hold UPGRADE_TIMELOCK_ROLE. upgradeToAndCall is excluded from I6.4 +// because the UUPS delegatecall havocs all storage (a modelling artifact), +// leaving its authorization otherwise unproven. _authorizeUpgrade calls +// onlyUpgradeTimelock(msg.sender) (RoleRegistry.sol:252-254), which reverts +// unless hasRole(UPGRADE_TIMELOCK_ROLE, msg.sender) — it does NOT allow the +// owner. We capture that membership BEFORE the call (the delegatecall may +// havoc it) and assert a successful upgrade implies the caller held it. +// ---------------------------------------------------------------------------- +rule I6_upgrade_requires_timelock_role(env e, calldataarg args) { + bool hadRole = hasRole(UPGRADE_TIMELOCK_ROLE(), e.msg.sender); + + upgradeToAndCall@withrevert(e, args); + + assert !lastReverted => hadRole, + "I6.6: upgradeToAndCall succeeded for a caller without UPGRADE_TIMELOCK_ROLE"; +} + +// ---------------------------------------------------------------------------- +// I6.2 PROTECTED ROLES: revokeFast can NEVER revoke UPGRADE_TIMELOCK_ROLE, +// OPERATION_TIMELOCK_ROLE, or OPERATION_MULTISIG_ROLE — it reverts +// (InvalidRoleToRevoke) before reaching solady's _setRole. A reverting +// call changes no membership, so the three roles are untouchable here. +// ---------------------------------------------------------------------------- +rule I6_revokeFast_reverts_on_protected_roles(env e, bytes32 role, address account) { + require role == UPGRADE_TIMELOCK_ROLE() + || role == OPERATION_TIMELOCK_ROLE() + || role == OPERATION_MULTISIG_ROLE(); + + revokeFast@withrevert(e, role, account); + + assert lastReverted, + "I6.2: revokeFast did not revert on a protected role"; +} + +// ---------------------------------------------------------------------------- +// I6.1 revokeFast AUTHORITY: a successful revokeFast requires msg.sender to be +// the immutable revokeAdmin. (Native check — no assembly, Prover sees it.) +// ---------------------------------------------------------------------------- +rule I6_revokeFast_requires_revokeAdmin(env e, bytes32 role, address account) { + revokeFast@withrevert(e, role, account); + bool reverted = lastReverted; + + assert !reverted => e.msg.sender == revokeAdmin(), + "I6.1: revokeFast succeeded for a non-revokeAdmin caller"; +} + +// ---------------------------------------------------------------------------- +// I6.3 revokeFast ONLY REMOVES: across any successful revokeFast, no +// (role,account) bit may go false->true; it can only stay or clear. +// ---------------------------------------------------------------------------- +rule I6_revokeFast_only_removes(env e, bytes32 role, address account) { + bytes32 r; address a; + bool before = hasRole(r, a); + + revokeFast(e, role, account); + + bool afterCall = hasRole(r, a); + + assert !(before == false && afterCall == true), + "I6.3: revokeFast granted a role (false->true), it must only revoke"; +} diff --git a/test/EtherFiRestaker.t.sol b/test/EtherFiRestaker.t.sol index 0fa8a5a25..cbc9b29dc 100644 --- a/test/EtherFiRestaker.t.sol +++ b/test/EtherFiRestaker.t.sol @@ -33,6 +33,16 @@ contract EtherFiRestakerTest is TestSetup { liquifierInstance.updateQuoteStEthWithCurve(false); } + /// Pin the Liquifier's stETH/ETH feed to a fresh ~1:1 answer so deposits + /// don't revert StalePriceFeed after vm.warp on a realistic fork. + function _mockFreshStEthFeed() internal { + vm.mockCall( + address(liquifierInstance.stEthPriceFeed()), + abi.encodeWithSignature("latestRoundData()"), + abi.encode(uint80(0), int256(1 ether), uint256(0), block.timestamp, uint80(0)) + ); + } + function _deposit_stEth(uint256 _amount) internal { uint256 restakerTvl = etherFiRestakerInstance.getTotalPooledEther(); uint256 lpTvl = liquidityPoolInstance.getTotalPooledEther(); @@ -188,6 +198,12 @@ contract EtherFiRestakerTest is TestSetup { uint32 timeBoundCapRefreshInterval = liquifierInstance.timeBoundCapRefreshInterval(); vm.warp(block.timestamp + timeBoundCapRefreshInterval + 1); + // The realistic fork wires the Liquifier to the live stETH/ETH Chainlink + // aggregator (~24h heartbeat). Warping past timeBoundCapRefreshInterval + // pushes block.timestamp beyond updatedAt + stalePriceWindow, so the + // deposit below would revert StalePriceFeed. Pin a fresh ~1:1 round. + _mockFreshStEthFeed(); + _deposit_stEth(10 ether); ISignatureUtilsMixinTypes.SignatureWithExpiry memory signature = ISignatureUtilsMixinTypes.SignatureWithExpiry({ diff --git a/test/invariant/OracleIntegrity.invariant.t.sol b/test/invariant/OracleIntegrity.invariant.t.sol new file mode 100644 index 000000000..487b7b3ff --- /dev/null +++ b/test/invariant/OracleIntegrity.invariant.t.sol @@ -0,0 +1,206 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../TestSetup.sol"; +import "@etherfi/core/interfaces/ILiquidityPool.sol"; +import "./handlers/OracleIntegrityHandler.sol"; + +/// @notice Stateful FUZZ-INVARIANT suite for invariant I5 (Oracle Integrity). +/// +/// I5 (protocol-ops/security/architecture/invariants.md): every applied +/// OracleReport — one that advances EtherFiAdmin.lastHandledReportRefSlot via +/// executeTasks — MUST satisfy ALL THREE gates at execution time: +/// (a) quorum — consensus reached with >= EtherFiOracle.quorumSize() sigs +/// (b) APR cap — abs(rebase APR) <= EtherFiAdmin.acceptableRebaseAprInBps() +/// (c) freshness — currentSlot >= postReportWaitTimeInSlots + consensusSlot +/// Equivalently: executeTasks reverts (ReportValidationFailed) on any report +/// failing quorum / APR / freshness, and only advances state when all hold. +/// +/// Defenses under test: EtherFiAdmin._validateReport -> _validateReportFreshness +/// (consensus + refSlotFrom + postReportWaitTimeInSlots) and _validateRebaseApr +/// (|apr| > acceptableRebaseAprInBps); quorum enforced upstream in +/// EtherFiOracle.submitReport (support >= quorumSize). +/// +/// HANDLER MODEL: the fuzzer drives a single `step(magnitude)` action. Each +/// call exercises all four scenarios (apply / quorum-fail / apr-fail / +/// fresh-fail) against the real EtherFiOracle + EtherFiAdmin, each leaving the +/// oracle in the un-stuck state. The fuzzed `magnitude` (and the random call +/// ordering / sequence length the invariant engine chooses) vary the rebase +/// sizes and the slot/epoch timeline across the run, so the safety property is +/// exercised over a wide state space. Before every executeTasks the handler +/// computes an INDEPENDENT, contract-faithful mirror of the three gates and +/// flips a ghost if a state-advancing report ever violated any gate (the I5 +/// proof), with a mirror-consistency cross-check against the contract's own +/// revert reasons so the safety ghosts can't be vacuously satisfied. +/// +/// SOUNDNESS ASSUMPTIONS (also in the handler): +/// * committee == {alice, bob}, quorumSize == 2 (TestSetup) — a single +/// submission is strictly sub-quorum. +/// * TVL seeded > 0 so the APR formula is non-trivial; postReportWaitTimeInSlots +/// set > 0 so the freshness gate is non-vacuous. +/// * A valid "apply" bounds its reward under the per-range APR-cap boundary +/// (the contract caps APR over the elapsed window), so the accepting path is +/// genuinely accepted rather than spuriously tripping the APR gate. +/// +/// fail-on-revert is false: the handler INTENTIONALLY drives reverting paths +/// (sub-quorum, over-cap APR, too-fresh) and asserts the safety post-condition +/// via ghosts. Non-vacuity is enforced in afterInvariant(). +/// +/// forge-config: default.invariant.runs = 64 +/// forge-config: default.invariant.depth = 30 +/// forge-config: default.invariant.fail-on-revert = false +contract OracleIntegrityInvariantTest is TestSetup { + OracleIntegrityHandler internal handler; + + function setUp() public { + setUpTests(); + + // SOUNDNESS: non-zero, stable TVL so the APR formula is non-trivial + // (currentTVL > 0). Without it getTotalPooledEther()==0 makes APR + // identically 0 and the APR gate could never be exercised. + vm.deal(alice, 1_000 ether); + vm.prank(alice); + liquidityPoolInstance.deposit{value: 1_000 ether}(); + + // SOUNDNESS: setUpTests initializes postReportWaitTimeInSlots == 0, which + // would make the freshness gate vacuous. Set a strictly-positive window. + vm.prank(alice); + etherFiAdminInstance.updatePostReportWaitTimeInSlots(16); + + // SOUNDNESS: pin the negative-rebase cap to the production default (3 bps). + // In this deployment the effective cap is otherwise 100% of TVL, which makes + // the negative-rebase gate unreachable while staying under the (annualized) + // APR cap — so no report could ever exercise it. 3 bps is the realistic + // on-chain value (DEFAULT_MAX_NEGATIVE_REBASE_BPS) and leaves a drop window + // that exceeds the negative cap yet stays under the APR cap for a report + // spanning one report period. + vm.prank(alice); + etherFiAdminInstance.setMaxNegativeRebaseBps(3); + + handler = new OracleIntegrityHandler( + etherFiOracleInstance, + etherFiAdminInstance, + ILiquidityPool(address(liquidityPoolInstance)), + alice, // committee member A + bob, // committee member B + owner, // holds OPERATION_MULTISIG_ROLE (unpublishReport recovery) + genesisSlotTimestamp + ); + + targetContract(address(handler)); + bytes4[] memory sels = new bytes4[](1); + sels[0] = handler.step.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: sels})); + } + + // ===================================================================== + // I5 core safety invariants — proven by handler ghosts flipped ONLY if a + // state-advancing executeTasks ever occurred while a gate was violated + // (per an independent, contract-faithful gate mirror). + // ===================================================================== + + /// (a) No report may advance lastHandledReportRefSlot without quorum consensus. + /// NOTE: the load-bearing detection for the quorum gate is afterInvariant's + /// numRejQuorum counter (its mirror leg reads the contract's own + /// isConsensusReached), which proves the gate was actually exercised. Do not + /// relax that counter's assertGt when editing — this ghost alone is vacuously + /// satisfiable if no sub-quorum report is ever driven. + function invariant_i5_quorum_required() public view { + assertFalse( + handler.ghost_appliedWithoutQuorum(), + "I5(a): a report advanced state without reaching quorum consensus" + ); + } + + /// (b) No report may advance state while its |rebase APR| exceeds the cap. + function invariant_i5_apr_capped() public view { + assertFalse( + handler.ghost_appliedAprViolation(), + "I5(b): a report advanced state with APR above acceptableRebaseAprInBps" + ); + } + + /// (c) No report may advance state before the post-report freshness window. + function invariant_i5_freshness_enforced() public view { + assertFalse( + handler.ghost_appliedWhileStale(), + "I5(c): a report advanced state before the post-report wait window" + ); + } + + /// (d) No report may advance state while its negative rebase exceeds the cap. + function invariant_i5_neg_rebase_capped() public view { + assertFalse( + handler.ghost_appliedNegRebaseViolation(), + "I5(d): a report advanced state with a negative rebase above the cap" + ); + } + + /// Mirror fidelity: every categorised ReportValidationFailed reason agrees + /// with our independent gate mirror, keeping the safety ghosts non-vacuous. + function invariant_i5_mirror_consistent() public view { + assertFalse(handler.ghost_mirrorMismatch(), handler.mismatchReason()); + } + + // ===================================================================== + // Submission-layer safety: duplicate and conflicting reports never let a + // sub-quorum report through, and the exact gate boundaries behave as the + // production comparisons specify. + // ===================================================================== + + /// A member's duplicate submission must revert (ReportNotNeeded) — never + /// succeed and never revert with a different, unexpected error. + function invariant_i5_duplicate_rejected() public view { + assertFalse(handler.ghost_duplicateSubmitSucceeded(), "duplicate submit was accepted"); + assertFalse(handler.ghost_duplicateWrongError(), handler.duplicateWrongErrorReason()); + } + + /// A single member's submissions (or two conflicting one-vote reports) must + /// never reach quorum consensus. + function invariant_i5_no_consensus_below_quorum() public view { + assertFalse(handler.ghost_consensusFromSingle(), "consensus reached from a single member"); + assertFalse(handler.ghost_conflictReachedConsensus(), "conflicting one-vote reports reached consensus"); + } + + /// The exact freshness / APR / negative boundaries that MUST apply actually did. + function invariant_i5_boundaries_apply() public view { + assertFalse(handler.ghost_freshBoundaryRejected(), "report at consensusSlot+wait failed to apply"); + assertFalse(handler.ghost_aprBoundaryRejected(), "report at the exact APR cap failed to apply"); + assertFalse(handler.ghost_negValidRejected(), "a valid small negative drop failed to apply"); + } + + /// The oracle must never stay permanently wedged (published != handled) across + /// a long tail of steps; each scenario is designed to leave it un-stuck. + function invariant_i5_never_permanently_stuck() public view { + assertFalse(handler.ghost_everStuck(), "oracle stayed wedged across too many consecutive steps"); + } + + // ===================================================================== + // Non-vacuity: the run must have actually exercised BOTH the accepting + // path (>=1 applied) AND each rejecting gate (quorum / APR / freshness). + // ===================================================================== + function afterInvariant() public { + emit log_named_uint("I5 reports APPLIED", handler.numApplied()); + emit log_named_uint("I5 quorum-gate rejections", handler.numRejQuorum()); + emit log_named_uint("I5 apr-gate rejections", handler.numRejApr()); + emit log_named_uint("I5 freshness-gate rejections", handler.numRejFresh()); + emit log_named_uint("I5 neg-rebase-gate rejections", handler.numRejNegRebase()); + emit log_named_uint("I5 duplicate submits rejected", handler.numDupRejected()); + emit log_named_uint("I5 conflicting scenarios run", handler.numConflictExercised()); + emit log_named_uint("I5 freshness-boundary applies", handler.numFreshBoundaryApplied()); + emit log_named_uint("I5 apr-boundary applies", handler.numAprBoundaryApplied()); + emit log_named_uint("I5 valid negative applies", handler.numNegAccepted()); + assertGt(handler.numApplied(), 0, "non-vacuity: no report was ever APPLIED"); + assertGt(handler.numRejected(), 0, "non-vacuity: no report was ever REJECTED"); + assertGt(handler.numRejQuorum(), 0, "non-vacuity: quorum gate never exercised"); + assertGt(handler.numRejApr(), 0, "non-vacuity: APR gate never exercised"); + assertGt(handler.numRejFresh(), 0, "non-vacuity: freshness gate never exercised"); + assertGt(handler.numRejNegRebase(), 0, "non-vacuity: negative-rebase gate never exercised"); + assertGt(handler.numDupRejected(), 0, "non-vacuity: duplicate submit never exercised"); + assertGt(handler.numConflictExercised(), 0, "non-vacuity: conflicting-report scenario never ran"); + assertGt(handler.numFreshBoundaryApplied(), 0, "non-vacuity: freshness boundary never applied"); + assertGt(handler.numAprBoundaryApplied(), 0, "non-vacuity: APR boundary never applied"); + assertGt(handler.numNegAccepted(), 0, "non-vacuity: valid negative rebase never applied"); + assertEq(handler.numRejOther(), 0, "an executeTasks revert was uncategorised"); + } +} diff --git a/test/invariant/RateLimiter.invariant.t.sol b/test/invariant/RateLimiter.invariant.t.sol new file mode 100644 index 000000000..1469e7010 --- /dev/null +++ b/test/invariant/RateLimiter.invariant.t.sol @@ -0,0 +1,152 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../TestSetup.sol"; +import "./handlers/RateLimiterHandler.sol"; + +/// @notice Stateful invariant suite for the GENERAL EtherFiRateLimiter, +/// proving invariant I4 (rate-limit budget conservation) for the +/// global-bucket path. This is the global rate limiter — distinct +/// from the redemption-specific BucketRateLimiter covered by the +/// RedemptionManager invariant suite. +/// +/// The handler (the fuzz target) creates a set of buckets, whitelists +/// itself as a consumer, and drives consume / refill (via warp) / +/// freeze / parameter mutations / gating probes. fail-on-revert is +/// false so legitimate reverts (LimitExceeded when drained, etc.) do +/// not fail the run; every I4 sub-property is asserted as a ghost flag +/// that must NEVER trip, plus a non-vacuity check in afterInvariant(). +/// +/// Only the handler's `act_*` functions are fuzzed (selector-targeted) +/// so the fuzzer spends its budget on real rate-limiter actions. +/// +/// forge-config: default.invariant.runs = 256 +/// forge-config: default.invariant.depth = 128 +/// forge-config: default.invariant.fail-on-revert = false +/// forge-config: default.invariant.call-override = false +contract RateLimiterInvariantTest is TestSetup { + RateLimiterHandler internal handler; + + function setUp() public { + setUpTests(); + + // `admin` holds OPERATION_TIMELOCK_ROLE (== onlyAdmin) in TestSetup. + handler = new RateLimiterHandler(rateLimiterInstance, admin); + + // Restrict the fuzzer to the handler's action functions only — no + // view getters, no constructor-style helpers — so the run exercises + // real consume/refill/parameter ops (non-vacuity). + bytes4[] memory selectors = new bytes4[](10); + selectors[0] = handler.act_consume.selector; + selectors[1] = handler.act_consumeFrozen.selector; + selectors[2] = handler.act_drainAndRefill.selector; + selectors[3] = handler.act_advanceTime.selector; + selectors[4] = handler.act_consumeUnknown.selector; + selectors[5] = handler.act_consumeUnwhitelisted.selector; + selectors[6] = handler.act_setCapacity.selector; + selectors[7] = handler.act_setRefillRate.selector; + selectors[8] = handler.act_setRemaining.selector; + selectors[9] = handler.act_revokeConsumer.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: selectors})); + targetContract(address(handler)); + } + + // ===================================================================== + // I4(a) — a bucket's remaining/consumable NEVER exceeds its capacity. + // ===================================================================== + function invariant_I4a_remaining_never_exceeds_capacity() public view { + assertFalse(handler.ghost_overfill(), "I4(a): remaining/consumable exceeded capacity (overfill)"); + // Independent end-of-run cross-check across every bucket. + for (uint256 i = 0; i < handler.N_BUCKETS(); i++) { + bytes32 id = handler.bucketId(i); + (uint64 cap, uint64 rem,,) = rateLimiterInstance.getLimit(id); + assertLe(rem, cap, "I4(a): on-chain remaining > capacity"); + assertLe(rateLimiterInstance.consumable(id), cap, "I4(a): on-chain consumable > capacity"); + } + } + + // ===================================================================== + // I4(b) — consume succeeds IFF canConsume(amount) was true just before, + // and a success reduces remaining by EXACTLY `amount`. + // ===================================================================== + function invariant_I4b_consume_iff_canConsume_and_exact_decrease() public view { + assertFalse(handler.ghost_iffViolated(), "I4(b): consume success != canConsume(before)"); + assertFalse(handler.ghost_exactDecreaseViolated(), "I4(b): consume did not reduce remaining by exactly amount"); + } + + // ===================================================================== + // I4(c) — capacity==0 on an existing bucket => consume reverts LimitExceeded. + // ===================================================================== + function invariant_I4c_zero_capacity_freezes_consume() public view { + assertFalse(handler.ghost_freezeViolated(), "I4(c): consume on a frozen (cap==0) bucket did not revert LimitExceeded"); + } + + // ===================================================================== + // I4(d) — refill is monotonic, bounded, and matches the EXACT formula. + // ===================================================================== + function invariant_I4d_refill_monotonic_and_bounded() public view { + assertFalse(handler.ghost_refillMonotonicViolated(), "I4(d): consumable decreased as time advanced (non-monotonic refill)"); + // boundedness is folded into ghost_overfill, re-asserted here. + assertFalse(handler.ghost_overfill(), "I4(d): refill overshot capacity"); + // Exact refill: consumable_after == min(capacity, before + refillRate*dt). + assertFalse(handler.ghost_refillModelViolated(), "I4(d): refill did not match min(capacity, before + refillRate*dt)"); + } + + // ===================================================================== + // I4(b') — draining exactly `consumable(id)` then consuming it never + // reverts (canConsume was true by construction). + // ===================================================================== + function invariant_I4b_drain_boundary_consume_succeeds() public view { + assertFalse(handler.ghost_drainConsumeReverted(), "I4(b'): consume(consumable(id)) reverted despite canConsume==true"); + } + + // ===================================================================== + // I4(e) — gating: UnknownLimit if no bucket, InvalidConsumer if not + // whitelisted, and consumer revocation/re-grant behaves exactly. + // ===================================================================== + function invariant_I4e_unknown_and_consumer_gating() public view { + assertFalse(handler.ghost_gatingViolated(), "I4(e): UnknownLimit / InvalidConsumer gating failed"); + assertFalse(handler.ghost_revokeViolated(), "I4(e): revoked consumer succeeded, or re-grant failed to restore consume"); + } + + // ===================================================================== + // I4(f) — the admin setters land on their EXACT documented post-state and + // never revert on valid inputs. + // ===================================================================== + function invariant_I4f_setter_exact_post_state() public view { + assertFalse(handler.ghost_setterPostStateViolated(), "I4(f): a setter's post-state != documented clamp result"); + assertFalse(handler.ghost_setterReverted(), "I4(f): a setter with valid inputs + admin role reverted"); + } + + // ===================================================================== + // Non-vacuity: the fuzzer must have exercised real consume + refill. + // ===================================================================== + function afterInvariant() public { + emit log_named_uint("consume_ok ", handler.consume_ok()); + emit log_named_uint("consume_rejected ", handler.consume_rejected()); + emit log_named_uint("act_consume ", handler.callCounts("act_consume")); + emit log_named_uint("act_consumeFrozen ", handler.callCounts("act_consumeFrozen")); + emit log_named_uint("act_drainAndRefill ", handler.callCounts("act_drainAndRefill")); + emit log_named_uint("act_advanceTime ", handler.callCounts("act_advanceTime")); + emit log_named_uint("act_consumeUnknown ", handler.callCounts("act_consumeUnknown")); + emit log_named_uint("act_consumeUnwhitelisted ", handler.callCounts("act_consumeUnwhitelisted")); + emit log_named_uint("act_setCapacity ", handler.callCounts("act_setCapacity")); + emit log_named_uint("act_setRefillRate ", handler.callCounts("act_setRefillRate")); + emit log_named_uint("act_setRemaining ", handler.callCounts("act_setRemaining")); + emit log_named_uint("act_revokeConsumer ", handler.callCounts("act_revokeConsumer")); + + assertGt(handler.consume_ok(), 0, "non-vacuity: no successful (amount>0) consume was ever exercised"); + assertTrue(handler.refillObserved(), "non-vacuity: no real (strictly-positive) refill was ever observed"); + + // Probe coverage: each deterministic-outcome probe must have run this + // run, otherwise its ghost flag is vacuously false. With depth 128 over + // 10 selectors each expects ~13 calls, so > 0 holds comfortably. + assertGt(handler.callCounts("act_consumeFrozen"), 0, "coverage: freeze probe never ran"); + assertGt(handler.callCounts("act_consumeUnknown"), 0, "coverage: UnknownLimit probe never ran"); + assertGt(handler.callCounts("act_consumeUnwhitelisted"), 0, "coverage: InvalidConsumer probe never ran"); + assertGt(handler.callCounts("act_revokeConsumer"), 0, "coverage: consumer-revocation probe never ran"); + assertGt(handler.callCounts("act_setCapacity"), 0, "coverage: setCapacity never succeeded"); + assertGt(handler.callCounts("act_setRefillRate"), 0, "coverage: setRefillRate never succeeded"); + assertGt(handler.callCounts("act_setRemaining"), 0, "coverage: setRemaining never succeeded"); + } +} diff --git a/test/invariant/RewardsDistributor.invariant.t.sol b/test/invariant/RewardsDistributor.invariant.t.sol new file mode 100644 index 000000000..1fee27174 --- /dev/null +++ b/test/invariant/RewardsDistributor.invariant.t.sol @@ -0,0 +1,201 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../TestSetup.sol"; +import "./handlers/RewardsDistributorHandler.sol"; + +/// @notice Stateful invariant suite for CumulativeMerkleRewardsDistributor. +/// Proves the two PR-defended invariants: +/// +/// I12 - cumulative-claim monotonicity & no double-pay +/// (defense: CumulativeMerkleRewardsDistributor.sol L112-114). +/// I13 - reward-root finalization delay +/// (defense: CumulativeMerkleRewardsDistributor.sol L79). +/// +/// The handler is the fuzz target; it drives set-pending / finalize / +/// claim / replay / time+block warps and maintains independent ghost +/// oracles. fail-on-revert is false so legitimate reverts (e.g. a +/// premature finalize hitting InsufficentDelay) do not fail the run; +/// the invariants assert the safety post-conditions. +/// +/// forge-config: default.invariant.runs = 256 +/// forge-config: default.invariant.depth = 64 +/// forge-config: default.invariant.fail-on-revert = false +/// forge-config: default.invariant.call-override = false +contract RewardsDistributorInvariantTest is TestSetup { + RewardsDistributorHandler internal handler; + address internal rdToken; + + function setUp() public { + setUpTests(); + + handler = new RewardsDistributorHandler( + cumulativeMerkleRewardsDistributorInstance, + admin + ); + + rdToken = cumulativeMerkleRewardsDistributorInstance.ETH_ADDRESS(); + + // Fund the distributor with ETH so ETH-token claims can pay out. + vm.deal(address(cumulativeMerkleRewardsDistributorInstance), 1_000_000 ether); + + // Restrict fuzzing to the handler's ACTION functions. Without an explicit + // selector list the engine also targets the handler's public view getters + // (numClaimants / claimants / callCounts / ghost*), wasting the call budget + // on no-ops so the lifecycle (setPending -> finalize -> claim) is never + // driven and the run is vacuous (all counters 0). Curate the selectors so + // every call advances the state machine. + bytes4[] memory selectors = new bytes4[](10); + selectors[0] = handler.doSetPendingRoot.selector; + selectors[1] = handler.doFinalize.selector; + selectors[2] = handler.doClaim.selector; + selectors[3] = handler.doReplayClaim.selector; + selectors[4] = handler.doSetClaimDelay.selector; + selectors[5] = handler.doWarp.selector; + selectors[6] = handler.doRoll.selector; + selectors[7] = handler.doLowerCumulativeClaim.selector; + selectors[8] = handler.doDelayBoundaryProbe.selector; + selectors[9] = handler.doMerkleTreeClaim.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: selectors})); + targetContract(address(handler)); + + // Deterministically drive ONE full lifecycle here so the afterInvariant + // non-vacuity floor is guaranteed regardless of the fuzzed sequence. + // Foundry snapshots state after setUp and reverts to it before every run, + // so these counter increments persist as a baseline on EVERY run. Without + // this, an unlucky seed dominated by the no-op-ish selectors + // (doWarp/doRoll/doSetClaimDelay) leaves finalize_ok/claim_ok/lower_rejected + // at 0 at evaluation time and the gate flakes red (latent in #470; the 8th + // selector merely perturbed the distribution enough to surface it). + // + // doClaim is self-contained (establish root -> finalize -> claim -> inline + // replay-rejected), so this one call seeds finalize_ok, claim_ok AND + // replay_revert. doLowerCumulativeClaim seeds lower_rejected (it bootstraps + // its own cumulative, then drives the monotonic-decrease guard). These run + // through the handler's REAL ops (admin-pranked), identical to fuzzed calls, + // so the fuzzer still independently exercises every path at runtime — this + // only establishes the floor. + handler.doClaim(0, 1 ether); + handler.doLowerCumulativeClaim(1, 0); + // Seed the delay-boundary probe (S1) and the real-Merkle-tree claim (S2) + // once so both edges of the finalization delay and the _verifyAsm proof + // loop are exercised on EVERY run regardless of the fuzzed sequence. + handler.doDelayBoundaryProbe(1); + handler.doMerkleTreeClaim(1); + } + + // ===================================================================== + // I12 - cumulative-claim monotonicity & no double-pay + // ===================================================================== + + function invariant_I12_cumulative_monotonic_no_double_pay() public view { + // Ghost flags tripped inside the handler on any violation. + assertFalse(handler.ghost_monotonicViolated(), "I12: cumulativeClaimed decreased (non-monotonic)"); + assertFalse(handler.ghost_doublePayViolated(), "I12: replay / double-payment observed"); + + // Independent end-of-run reconciliation for every claimant: + // on-chain cumulativeClaimed == ETH actually received == ghost-tracked paid. + uint256 n = handler.numClaimants(); + for (uint256 i = 0; i < n; i++) { + address account = handler.claimants(i); + uint256 cum = cumulativeMerkleRewardsDistributorInstance.cumulativeClaimed(rdToken, account); + // Claimants start at balance 0 and never spend, so balance == total paid. + assertEq(account.balance, cum, "I12: ETH paid != cumulativeClaimed (double-pay/replay)"); + assertEq(handler.ghostPaid(account), cum, "I12: ghost paid ledger drift vs cumulativeClaimed"); + assertEq(handler.lastSeenCumulative(account), cum, "I12: last-seen cumulative drift"); + } + } + + // ===================================================================== + // I13 - reward-root finalization delay + // ===================================================================== + + function invariant_I13_finalization_delay_enforced() public view { + assertFalse( + handler.ghost_finalizeDelayViolated(), + "I13: finalize succeeded before claimDelay elapsed" + ); + assertFalse( + handler.ghost_finalizeRootMismatch(), + "I13: claimable root != root that was pending for >= claimDelay" + ); + assertFalse( + handler.ghost_boundaryRejectedAtDelay(), + "I13: finalize rejected AT setAt + claimDelay (delay guard too strict)" + ); + } + + // ===================================================================== + // Merkle-proof integrity (S2) — the claim path verifies real proofs. + // ===================================================================== + + function invariant_merkle_proof_integrity() public view { + assertFalse( + handler.ghost_validProofRejected(), + "merkle: a claim with a genuine in-tree 2-element proof reverted" + ); + assertFalse( + handler.ghost_badProofAccepted(), + "merkle: a claim with a proof for the wrong leaf/amount succeeded" + ); + } + + // ===================================================================== + // Non-vacuity: the run MUST have actually exercised the merkle-delay and + // payout logic this suite defends. Without this, the I12/I13 ghost flags + // stay false and balances stay zero if those paths are never hit, so the + // invariants could pass without proving anything. Asserted once at the end. + // ===================================================================== + function afterInvariant() public { + // I13 path: at least one root must have been finalized after its delay. + assertGt(handler.callCounts("finalize_ok"), 0, "non-vacuity: no merkle root was ever finalized (I13 unexercised)"); + // I12 path: at least one successful claim must have paid out. + assertGt(handler.callCounts("claim_ok"), 0, "non-vacuity: no claim ever succeeded (I12 payout unexercised)"); + // Double-pay defense: at least one replay must have been attempted AND rejected. + assertGt(handler.callCounts("replay_revert"), 0, "non-vacuity: replay/double-pay path never exercised"); + // I12 monotonic-decrease guard: at least one strictly-lower-cumulative + // claim must have been attempted AND rejected, positively driving the + // `preclaimed >= cumulativeAmount` revert path. + assertGt(handler.callCounts("lower_rejected"), 0, "non-vacuity: monotonic-decrease guard never exercised"); + + // And the run must have actually moved ETH: total ghost-paid across all + // claimants > 0 (independent of the counters above). + uint256 totalPaid; + uint256 n = handler.numClaimants(); + for (uint256 i = 0; i < n; i++) { + totalPaid += handler.ghostPaid(handler.claimants(i)); + } + assertGt(totalPaid, 0, "non-vacuity: zero ETH paid across the whole run (claims never settled)"); + } + + // ===================================================================== + // Coverage summary (soft observability, not a hard assertion). + // ===================================================================== + + function invariant_call_coverage_summary() public { + emit log_named_uint("setPending ", handler.callCounts("setPending")); + emit log_named_uint("setPending_revert ", handler.callCounts("setPending_revert")); + emit log_named_uint("finalize_ok ", handler.callCounts("finalize_ok")); + emit log_named_uint("finalize_delay_revert ", handler.callCounts("finalize_delay_revert")); + emit log_named_uint("finalize_other_revert ", handler.callCounts("finalize_other_revert")); + emit log_named_uint("claim_ok ", handler.callCounts("claim_ok")); + emit log_named_uint("claim_revert ", handler.callCounts("claim_revert")); + emit log_named_uint("replay_revert ", handler.callCounts("replay_revert")); + emit log_named_uint("lower_rejected ", handler.callCounts("lower_rejected")); + emit log_named_uint("lower_unexpected_ok ", handler.callCounts("lower_unexpected_ok")); + emit log_named_uint("lower_boot_failed ", handler.callCounts("lower_boot_failed")); + emit log_named_uint("replay_unexpected_ok ", handler.callCounts("replay_unexpected_ok")); + emit log_named_uint("replay_skipped ", handler.callCounts("replay_skipped")); + emit log_named_uint("boundary_early_rejected", handler.callCounts("boundary_early_rejected")); + emit log_named_uint("boundary_early_ok ", handler.callCounts("boundary_early_ok")); + emit log_named_uint("boundary_at_ok ", handler.callCounts("boundary_at_ok")); + emit log_named_uint("boundary_at_rejected ", handler.callCounts("boundary_at_rejected")); + emit log_named_uint("tree_claim_ok ", handler.callCounts("tree_claim_ok")); + emit log_named_uint("tree_claim_revert ", handler.callCounts("tree_claim_revert")); + emit log_named_uint("tree_proof_rejected ", handler.callCounts("tree_proof_rejected")); + emit log_named_uint("tree_proof_unexpected_ok", handler.callCounts("tree_proof_unexpected_ok")); + emit log_named_uint("setClaimDelay ", handler.callCounts("setClaimDelay")); + emit log_named_uint("warp ", handler.callCounts("warp")); + emit log_named_uint("roll ", handler.callCounts("roll")); + } +} diff --git a/test/invariant/ValidatorLifecycle.invariant.t.sol b/test/invariant/ValidatorLifecycle.invariant.t.sol new file mode 100644 index 000000000..87c82f033 --- /dev/null +++ b/test/invariant/ValidatorLifecycle.invariant.t.sol @@ -0,0 +1,114 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../TestSetup.sol"; +import "./handlers/ValidatorLifecycleHandler.sol"; + +/// @notice Stateful invariant suite for validator pubkey->node uniqueness. +/// +/// I11 — pubkey -> node uniqueness: each validator pubkey hash maps to +/// exactly one EtherFiNode, set once, never overwritten or repointed. +/// Defense: EtherFiNodesManager.linkPubkeyToNode reverts AlreadyLinked +/// when etherFiNodeFromPubkeyHash[hash] (or the legacyId slot) is +/// already set (src/EtherFiNodesManager.sol ~lines 343-349). +/// +/// The handler drives linkPubkeyToNode directly (pranked as the +/// StakingManager, its only authorized caller) over a deliberately +/// small pubkey space so collisions and re-link attempts are frequent, +/// and includes an explicit re-link-attack action. +/// +/// NOTE on I10 (validator-creation state machine): driving the real +/// beacon flow (registerValidatorBeaconDeposit -> createBeaconValidators) +/// in a stateful fuzzer requires a deployed EtherFiNode + EigenPod, +/// an active auction bid, and valid beacon deposit-data roots — the +/// existing scaffolding for that lives in fork-based tests +/// (test/StakingManager.t.sol uses initializeRealisticFork). That is +/// out of scope for this non-fork suite and is tracked separately. +/// I11 is proven here cleanly without beacon deposits. +/// +/// forge-config: default.invariant.runs = 256 +/// forge-config: default.invariant.depth = 64 +/// forge-config: default.invariant.fail-on-revert = false +contract ValidatorLifecycleInvariantTest is TestSetup { + ValidatorLifecycleHandler internal handler; + + address internal executorOps = address(0xE0E0); + + function setUp() public { + setUpTests(); + + // linkLegacyValidatorIds is onlyExecutorOperations; grant the role to a + // dedicated address the handler pranks for the legacy-path re-link attack. + // startPrank (not prank) so the nested EXECUTOR_OPERATIONS_ROLE() read doesn't + // consume the prank before grantRole runs. + vm.startPrank(roleRegistryInstance.owner()); + roleRegistryInstance.grantRole(roleRegistryInstance.EXECUTOR_OPERATIONS_ROLE(), executorOps); + vm.stopPrank(); + + handler = new ValidatorLifecycleHandler(managerInstance, address(stakingManagerInstance), executorOps); + targetContract(address(handler)); + + // Restrict fuzzing to the three action functions. Without this, the engine + // also targets the handler's view getters (linkedCount, ghostLinkedNode, + // the counters), wasting call budget on no-ops. + bytes4[] memory sel = new bytes4[](3); + sel[0] = handler.doLink.selector; + sel[1] = handler.doRelinkAttack.selector; + sel[2] = handler.doLegacyLinkAttack.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: sel})); + } + + /// I11: no pubkey-hash link was ever overwritten / repointed after first set. + function invariant_I11_pubkey_node_link_immutable() public view { + assertFalse(handler.sawOverwrite(), "I11: a pubkey-hash->node link was overwritten"); + } + + /// I11: re-linking an already-linked pubkey (same or different node) never succeeds. + function invariant_I11_no_relink_succeeds() public view { + assertFalse(handler.sawRelinkSucceed(), "I11: re-link of an already-linked pubkey succeeded"); + } + + /// I11 (global sweep): every pubkey hash the handler ever linked still points at + /// the exact node it was FIRST set to. The per-step sawOverwrite ghost only checks + /// the hash touched by the current call; this walks the whole recorded set each + /// invariant round so a stray repoint of any other hash is caught too. + function invariant_I11_all_links_match_first_node() public view { + uint256 n = handler.linkedCount(); + for (uint256 i = 0; i < n; i++) { + bytes32 h = handler.linkedHashes(i); + assertEq( + address(managerInstance.etherFiNodeFromPubkeyHash(h)), + handler.ghostLinkedNode(h), + "I11: a linked pubkey hash diverged from its first-set node" + ); + } + } + + /// Soft coverage observability (mirrors existing suites' convention). + function invariant_call_coverage_summary() public view { + // no assertion; surfaced under -vv + handler.link_ok(); + handler.link_already_revert(); + handler.relink_attempt(); + handler.legacy_link_attempt(); + } + + /// Non-vacuity gate: prove the fuzzer actually drove the I11 lifecycle — + /// at least one successful link, at least one rejected re-link (either via + /// doLink hitting an already-linked hash or the explicit re-link attack). + /// Without this, both invariant_I11_* could pass trivially because no link + /// or re-link attempt ever fired. + function afterInvariant() public { + emit log_named_uint("link_ok ", handler.link_ok()); + emit log_named_uint("link_already_revert", handler.link_already_revert()); + emit log_named_uint("relink_attempt ", handler.relink_attempt()); + emit log_named_uint("legacy_link_attempt", handler.legacy_link_attempt()); + + assertGt(handler.link_ok(), 0, "non-vacuity: no pubkey->node link ever succeeded"); + assertGt( + handler.link_already_revert() + handler.relink_attempt() + handler.legacy_link_attempt(), + 0, + "non-vacuity: no re-link / already-linked path was ever exercised" + ); + } +} diff --git a/test/invariant/ValidatorStateMachine.invariant.t.sol b/test/invariant/ValidatorStateMachine.invariant.t.sol new file mode 100644 index 000000000..b9475fed3 --- /dev/null +++ b/test/invariant/ValidatorStateMachine.invariant.t.sol @@ -0,0 +1,289 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../TestSetup.sol"; +import "../../script/deploys/Deployed.s.sol"; +import "@etherfi/staking/interfaces/IStakingManager.sol"; +import "@etherfi/staking/interfaces/IEtherFiNode.sol"; +import "@etherfi/staking/libraries/DepositDataRootGenerator.sol"; +import "@etherfi/core/LiquidityPool.sol"; +import "@etherfi/staking/StakingManager.sol"; +import "@etherfi/staking/NodeOperatorManager.sol"; +import "@etherfi/withdrawals/WithdrawRequestNFT.sol"; +import "@etherfi/withdrawals/PriorityWithdrawalQueue.sol"; +import "./handlers/ValidatorStateMachineHandler.sol"; + +/// @notice FORK stateful-invariant suite for the validator-creation state machine (I10). +/// NOT_REGISTERED -> REGISTERED -> CONFIRMED, or REGISTERED -> INVALIDATED; +/// CONFIRMED/INVALIDATED terminal; no skip/reverse/illegal edge. +/// Reuses the mainnet-fork scaffolding from ValidatorFlowsIntegrationTest +/// (duplicated here because that contract's setUp is non-virtual). +/// Requires MAINNET_RPC_URL. +/// +/// forge-config: default.invariant.runs = 16 +/// forge-config: default.invariant.depth = 24 +/// forge-config: default.invariant.fail-on-revert = false +contract ValidatorStateMachineInvariantTest is TestSetup, Deployed { + ValidatorStateMachineHandler internal handler; + uint256 internal constant POOL = 4; + function setUp() public { + // Pin the fork so the state-machine run is reproducible across CI and reruns. + initializeRealisticForkWithBlock(MAINNET_FORK, 25447657); + + // Mainnet NodeOperatorManager hasn't been upgraded to the role-based ACL yet, + // so its NODE_OPERATOR_MANAGER_ADMIN_ROLE() getter doesn't exist on-chain. + // Upgrade in place so the new role getters used by _ensureValCreationRoles are reachable. + NodeOperatorManager nodeOperatorManagerImpl = new NodeOperatorManager(address(roleRegistryInstance), address(auctionInstance)); + vm.prank(roleRegistryInstance.owner()); + nodeOperatorManagerInstance.upgradeTo(address(nodeOperatorManagerImpl)); + + // Upgrade LiquidityPool to the consolidated role model — the on-chain impl + // still checks LIQUIDITY_POOL_ADMIN_ROLE on registerValidatorSpawner. + LiquidityPool newLpImpl = new LiquidityPool(ILiquidityPool.ConstructorAddresses({ + stakingManager: address(stakingManagerInstance), + nodesManager: address(managerInstance), + eETH: address(eETHInstance), + withdrawRequestNFT: address(withdrawRequestNFTInstance), + liquifier: address(liquifierInstance), + etherFiRedemptionManager: address(etherFiRedemptionManagerInstance), + roleRegistry: address(roleRegistryInstance), + priorityWithdrawalQueue: address(priorityQueueInstance), + blacklister: address(blacklisterInstance), + etherFiAdminContract: address(etherFiAdminInstance), + // Use the REAL deployed membership manager, not the V0-typed + // `membershipManagerInstance` which is never populated on a realistic + // fork (only `membershipManagerV1Instance` is, from deployed.MEMBERSHIP_MANAGER()). + // Passing address(0) here would diverge the immutable from the production + // bootstrap and mis-auth any membership-routed LP path. + membershipManager: MEMBERSHIP_MANAGER + })); + address lpOwner = roleRegistryInstance.owner(); + vm.prank(lpOwner); + liquidityPoolInstance.upgradeTo(address(newLpImpl)); + + // Upgrade WithdrawRequestNFT so it has a receive() function and accepts the + // ETH-escrow transfer triggered by initializeOnUpgradeV2. + address wrnOwner = roleRegistryInstance.owner(); + // Hoist the impl deploy ABOVE the prank: an inlined `new` inside the + // upgradeTo() arg would consume the prank (CREATE counts as the next + // call), so upgradeTo would run as the test contract and revert + // OnlyUpgradeTimelock. + WithdrawRequestNFT newWrnImpl = new WithdrawRequestNFT(address(liquidityPoolInstance), address(roleRegistryInstance), address(blacklisterInstance), address(etherFiAdminInstance)); + vm.prank(wrnOwner); + withdrawRequestNFTInstance.upgradeTo(address(newWrnImpl)); + + // The production queue proxy on mainnet still runs the master impl which + // has no receive(); initializeOnUpgradeV2 below sweeps queue-locked ETH + // into the queue and would revert with SendFail. Upgrade the queue first. + // Constructor order is (liquidityPool, eETH, weETH, blacklister, roleRegistry, minDelay). + // Pass blacklisterInstance + roleRegistryInstance in their correct slots so the + // upgraded mainnet queue proxy's role checks match production wiring. + address newPQ = address(new PriorityWithdrawalQueue( + address(liquidityPoolInstance), address(eETHInstance), address(weEthInstance), + address(blacklisterInstance), address(roleRegistryInstance), 1 hours + )); + vm.prank(UPGRADE_TIMELOCK); + PriorityWithdrawalQueue(payable(PRIORITY_WITHDRAWAL_QUEUE)).upgradeTo(newPQ); + + // One-shot migration: move pre-existing locked ETH into NFT escrow so the + // post-upgrade LP can route through addEthAmountLockedForWithdrawal. + if (!liquidityPoolInstance.escrowMigrationCompleted()) { + vm.prank(lpOwner); + liquidityPoolInstance.initializeOnUpgradeV2(); + } + + // Upgrade Oracle and Admin to local impls so the new OracleReport ABI matches. + _upgradeOracleAndAdminForFork(); + + // Raise the per-day approval cap so executeTasks doesn't reject the validator approval. + address rrOwner = roleRegistryInstance.owner(); + vm.startPrank(rrOwner); + roleRegistryInstance.grantRole(roleRegistryInstance.OPERATION_TIMELOCK_ROLE(), rrOwner); + // ORACLE_OPERATIONS_ROLE (formerly ETHERFI_ORACLE_EXECUTOR_TASK_MANAGER_ROLE) is required by + // EtherFiAdmin.executeValidatorApprovalTask. + roleRegistryInstance.grantRole(roleRegistryInstance.ORACLE_OPERATIONS_ROLE(), ADMIN_EOA); + etherFiAdminInstance.updateMaxNumValidatorsToApprovePerDay(etherFiAdminInstance.maxAcceptableNumValidatorsToApprovePerDay()); + vm.stopPrank(); + + // Handle any pending oracle report that hasn't been processed yet + _syncOracleReportState(); + + _provisionPoolAndTarget(); + } + + /// @dev Advances the admin's lastHandledReportRefSlot to match the oracle's lastPublishedReportRefSlot. + function _syncOracleReportState() internal { + // Step A: sync admin to oracle so submitReport doesn't fail with + // "Last published report is not handled yet". + uint32 lastPublished = etherFiOracleInstance.lastPublishedReportRefSlot(); + uint32 lastHandled = etherFiAdminInstance.lastHandledReportRefSlot(); + + if (lastPublished != lastHandled) { + uint32 lastPublishedBlock = etherFiOracleInstance.lastPublishedReportRefBlock(); + + // EtherFiAdmin slot 209 packs: lastHandledReportRefSlot (4B @ offset 0) + + // lastHandledReportRefBlock (4B @ offset 4) + other fields in higher bytes + bytes32 slot209 = vm.load(address(etherFiAdminInstance), bytes32(uint256(209))); + uint256 val = uint256(slot209); + val &= ~uint256(0xFFFFFFFFFFFFFFFF); // clear low 64 bits (both uint32 fields) + val |= uint256(lastPublished); + val |= uint256(lastPublishedBlock) << 32; + vm.store(address(etherFiAdminInstance), bytes32(uint256(209)), bytes32(val)); + } + + // Step B: unconditionally reset operator submissions by removing and re-adding each one. + // addCommitteeMember() resets CommitteeMemberState to + // (registered=true, enabled=true, lastReportRefSlot=0, numReports=0), clearing any stale + // submission from mainnet without adding new committee members. + address oracleOwner = roleRegistryInstance.owner(); + // Each add/remove now requires a _quorumSize that satisfies the strict-majority + // invariant for the resulting numActive. Compute a fresh value at each step + // so this works regardless of mainnet's current quorum. + vm.startPrank(oracleOwner); + uint32 active = etherFiOracleInstance.numActiveCommitteeMembers(); + uint32 quorumAfterRemove = active > 1 ? (active - 1) / 2 + 1 : 1; + uint32 quorumAfterAdd = active / 2 + 1; + etherFiOracleInstance.removeCommitteeMember(AVS_OPERATOR_1, quorumAfterRemove); + etherFiOracleInstance.addCommitteeMember(AVS_OPERATOR_1, quorumAfterAdd); + etherFiOracleInstance.removeCommitteeMember(AVS_OPERATOR_2, quorumAfterRemove); + etherFiOracleInstance.addCommitteeMember(AVS_OPERATOR_2, quorumAfterAdd); + vm.stopPrank(); + } + + function _toArray(IStakingManager.DepositData memory d) internal pure returns (IStakingManager.DepositData[] memory arr) { + arr = new IStakingManager.DepositData[](1); + arr[0] = d; + } + + function _toArrayU256(uint256 x) internal pure returns (uint256[] memory arr) { + arr = new uint256[](1); + arr[0] = x; + } + + function _ensureValCreationRoles() internal { + address roleOwner = roleRegistryInstance.owner(); + + // Ensure the operating admin can manage LP spawners + create validators. + vm.startPrank(roleOwner); + roleRegistryInstance.grantRole(roleRegistryInstance.OPERATION_TIMELOCK_ROLE(), ETHERFI_OPERATING_ADMIN); + roleRegistryInstance.grantRole(roleRegistryInstance.ORACLE_OPERATIONS_ROLE(), ETHERFI_OPERATING_ADMIN); + + // Ensure operating timelock can create nodes. + roleRegistryInstance.grantRole(roleRegistryInstance.EXECUTOR_OPERATIONS_ROLE(), OPERATING_TIMELOCK); + vm.stopPrank(); + + // The mainnet NodeOperatorManager implementation predates this PR and + // does not expose NODE_OPERATOR_MANAGER_ADMIN_ROLE(). Upgrade in place + // so the new role getter and role-gated modifier are reachable, then + // grant the role used by whitelist ops. + address nodeOpMgrOwner = roleRegistryInstance.owner(); + vm.startPrank(nodeOpMgrOwner); + NodeOperatorManager newNodeOpMgrImpl = new NodeOperatorManager(address(roleRegistryInstance), address(auctionInstance)); + nodeOperatorManagerInstance.upgradeTo(address(newNodeOpMgrImpl)); + vm.stopPrank(); + + vm.startPrank(roleOwner); + roleRegistryInstance.grantRole(roleRegistryInstance.OPERATION_MULTISIG_ROLE(), ETHERFI_OPERATING_ADMIN); + vm.stopPrank(); + } + + function _prepareSingleValidator(address spawner) + internal + returns (IStakingManager.DepositData memory depositData, uint256 bidId, address etherFiNode) + { + _ensureValCreationRoles(); + + // Step 1: Whitelist + register node operator. + vm.prank(ETHERFI_OPERATING_ADMIN); + nodeOperatorManagerInstance.addToWhitelist(spawner); + + vm.deal(spawner, 10 ether); + vm.startPrank(spawner); + if (!nodeOperatorManagerInstance.registered(spawner)) { + nodeOperatorManagerInstance.registerNodeOperator("test_ipfs_hash", 1000); + } + uint256[] memory bidIds = auctionInstance.createBid{value: 0.1 ether}(1, 0.1 ether); + vm.stopPrank(); + bidId = bidIds[0]; + + // Step 2: Create a new EtherFiNode (with EigenPod) for compounding withdrawal creds. + vm.prank(OPERATING_TIMELOCK); + etherFiNode = stakingManagerInstance.instantiateEtherFiNode(true /*createEigenPod*/); + address eigenPod = address(IEtherFiNode(etherFiNode).getEigenPod()); + + // Step 3: Register validator spawner. + vm.prank(ETHERFI_OPERATING_ADMIN); + liquidityPoolInstance.registerValidatorSpawner(spawner); + + // Step 4: Build 1-ETH deposit data (must match compounding withdrawal creds). + bytes memory pubkey = vm.randomBytes(48); + bytes memory signature = vm.randomBytes(96); + bytes memory withdrawalCredentials = managerInstance.addressToCompoundingWithdrawalCredentials(eigenPod); + bytes32 depositDataRoot = + depositDataRootGenerator.generateDepositDataRoot(pubkey, signature, withdrawalCredentials, stakingManagerInstance.INITIAL_DEPOSIT_AMOUNT()); + + depositData = IStakingManager.DepositData({ + publicKey: pubkey, + signature: signature, + depositDataRoot: depositDataRoot, + ipfsHashForEncryptedValidatorKey: "test_ipfs_hash" + }); + } + // ---- invariants ---- + function invariant_I10_only_legal_status_transitions() public view { + assertFalse(handler.sawIllegalTransition(), handler.illegalReason()); + } + + /// I10, end-state half: a call that reported success must land in the exact + /// expected status (register -> REGISTERED, create -> CONFIRMED, + /// invalidate -> INVALIDATED), not merely on some legal edge. + function invariant_I10_success_reaches_expected_state() public view { + assertFalse(handler.sawWrongEndState(), handler.wrongEndStateReason()); + } + + /// Non-vacuity: the fuzzer must actually have driven real transitions, not just + /// bounced off reverts — otherwise "no illegal transition" would be trivially true. + /// Checked once at the END of the run (afterInvariant), not per-step. Both terminal + /// edges are gated SEPARATELY so a run that only ever created (or only ever + /// invalidated) still fails the vacuity check. + function afterInvariant() public view { + assertGt(handler.register_ok(), 0, "no REGISTERED transition ever fired"); + assertGt(handler.create_ok(), 0, "no CONFIRMED (create) transition ever fired"); + assertGt(handler.invalidate_ok(), 0, "no INVALIDATED (invalidate) transition ever fired"); + } + + function invariant_call_coverage_summary() public view { + handler.register_ok(); + handler.create_ok(); + handler.invalidate_ok(); + } + + // ---- pool provisioning, invoked at end of setUp ---- + function _provisionPoolAndTarget() internal { + // _prepareSingleValidator registers the spawner as a validator spawner, which + // reverts AlreadyRegistered on reuse — so use a DISTINCT spawner per validator. + handler = new ValidatorStateMachineHandler( + stakingManagerInstance, + address(liquidityPoolInstance), + address(0), // unused: each validator carries its own spawner via the LP registration + ETHERFI_OPERATING_ADMIN, + ETHERFI_OPERATING_ADMIN + ); + for (uint256 i = 0; i < POOL; i++) { + address spawner = vm.addr(uint256(keccak256(abi.encodePacked("spawner", i)))); + (IStakingManager.DepositData memory d, uint256 bidId, address node) = _prepareSingleValidator(spawner); + bytes32 h = keccak256( + abi.encode(d.publicKey, d.signature, d.depositDataRoot, d.ipfsHashForEncryptedValidatorKey, bidId, node) + ); + handler.addValidator(d, bidId, node, spawner, h); + } + vm.deal(address(liquidityPoolInstance), address(liquidityPoolInstance).balance + 100 ether); + targetContract(address(handler)); + // Only fuzz the three transition actions — exclude addValidator (setup-only). + bytes4[] memory sels = new bytes4[](3); + sels[0] = handler.doRegister.selector; + sels[1] = handler.doCreate.selector; + sels[2] = handler.doInvalidate.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: sels})); + } +} diff --git a/test/invariant/WithdrawalSolvency.invariant.t.sol b/test/invariant/WithdrawalSolvency.invariant.t.sol new file mode 100644 index 000000000..643657ded --- /dev/null +++ b/test/invariant/WithdrawalSolvency.invariant.t.sol @@ -0,0 +1,477 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../TestSetup.sol"; +import "./handlers/WithdrawalSolvencyHandler.sol"; + +/// @notice FORK-based stateful invariant suite for I3 — Withdrawal Queue +/// Accounting / Solvency — exercised against the WithdrawRequestNFT +/// escrow path on a *latest-block mainnet fork* via +/// `initializeRealisticFork(MAINNET_FORK)`. +/// +/// ───────────────────────────────────────────────────────────────────────── +/// I3 PROPERTY (protocol-ops/security/architecture/invariants.md) +/// ───────────────────────────────────────────────────────────────────────── +/// Informal: the total outstanding withdrawal claim never exceeds the +/// protocol's redeemable ETH. +/// Formal: WithdrawRequestNFT outstanding finalizable claims +/// <= LP.getTotalPooledEther() +/// + EigenLayer-queued withdrawals (all pods) +/// - already-finalized claims. +/// +/// ───────────────────────────────────────────────────────────────────────── +/// WHAT IS PROVABLE ON A FORK vs WHAT IS RECLASSIFIED +/// ───────────────────────────────────────────────────────────────────────── +/// The `+ EigenLayer-queued withdrawals(all pods)` term is LIVE state spread +/// across every EtherFiNode/EigenPod on mainnet. It cannot be deterministically +/// controlled at a latest-block fork (it drifts block-to-block and depends on +/// beacon-chain / EL checkpoint state we cannot author). Asserting an absolute +/// bound that includes that term would either (a) require us to fabricate EL +/// state (forbidden — would make the test assert something we didn't really +/// prove) or (b) be vacuous. We therefore RECLASSIFY that part to the +/// SC-enforced bound the contracts actually guarantee and which is strictly +/// STRONGER for the protocol's solvency (it ignores the favorable EL term and +/// requires the obligation be backed by in-protocol accounting alone): +/// +/// (P1) finalize-never-exceeds-liquidity [PROVED, SC-enforced] +/// Every successful finalize+lock had its locked eETH amount +/// <= LiquidityPool.totalValueInLp() at lock time. This is the exact +/// bound EtherFiAdmin._validateWithdrawals enforces +/// (`finalizedWithdrawalAmount <= totalValueInLp`) and that +/// LiquidityPool._lockEth re-enforces (`totalValueInLp < _amount` +/// reverts). Driven non-vacuously: see ghost_finalizeBoundChecks. +/// +/// (P2) locked-within-accounted-state [ASSUMPTION-SCOPED: bounded rebases] +/// ethAmountLockedForWithdrawal <= totalValueOutOfLp +/// <= getTotalPooledEther. +/// Finalize moves `amount` 1:1 from inLp->outOfLp AND adds `amount` to +/// the lock; claim removes `amountOfEEth` (full) from the lock but only +/// `amountToWithdraw (<= amountOfEEth)` from outOfLp (plus a stranded-ETH +/// sweep). Those two operations keep the lock a subset of out-of-LP value. +/// A NEGATIVE rebase, however, decrements totalValueOutOfLp WITHOUT +/// touching the lock, so a large enough slash could push outOfLp below the +/// lock and break this bound. This suite holds the bound only under the +/// assumption that rebases are bounded — enforced HERE by the handler's +/// rebaseNegative input filter (WithdrawalSolvencyHandler L416-431, which +/// caps the slash to <=0.5% of TVL and keeps headroom above the lock). +/// The corresponding PROTOCOL-level defense is EtherFiAdmin's rebase-APR +/// caps. So P2 is assumption-scoped, not unconditionally true. Also assert +/// WRN raw-ETH escrow >= lock (the segregated-balance solvency the claim +/// path relies on). +/// +/// (P3) finalized-always-claimable [PROVED, SC-enforced] +/// A finalized, valid, owned request whose frozen rate is in +/// [min,max] always claims successfully (escrow segregated at finalize +/// covers the payout; the frozen-rate share burn is bounded by the +/// request's own shares). Any revert under those preconditions trips +/// ghost_finalizedClaimFailed. +/// +/// ───────────────────────────────────────────────────────────────────────── +/// SOUNDNESS ASSUMPTIONS (documented, not weakening) +/// ───────────────────────────────────────────────────────────────────────── +/// - We mirror production's finalize flow EXACTLY: WithdrawRequestNFT.finalizeRequests +/// the newly-finalized range, then lock its summed eETH via +/// LP.addEthAmountLockedForWithdrawal — the same finalize-then-lock order as +/// EtherFiAdmin._finalizeWithdrawals (both pranked as the real EtherFiAdmin +/// immutable that gates them). We do NOT call any path src/ doesn't expose. +/// - Negative rebases are bounded to <= 0.5% of TVL and kept above the WRN +/// lock. An extreme slash that drives amountForShare(1e18) below +/// LiquidityPool.minAmountForShare would legitimately block claims via +/// `_checkMinAmountForShare` — that is a *liveness* edge of the rate guard, +/// NOT an I3 solvency violation, so we keep it out of the P3 property by +/// bounding the slash. (Documented; the bound does not weaken P1/P2.) +/// - All assertions are DELTA-AWARE / construction-true: we never assume a +/// zero baseline. Mainnet starts with ~20.3k ETH locked, ~876 ETH in-LP, +/// ~1.84M ETH out-of-LP, and 69 pending unfinalized requests; the +/// invariants hold against that live state. +/// +/// forge-config: default.invariant.runs = 32 +/// forge-config: default.invariant.depth = 64 +/// forge-config: default.invariant.fail-on-revert = false +/// forge-config: default.invariant.call-override = false +contract WithdrawalSolvencyInvariantTest is TestSetup { + WithdrawalSolvencyHandler internal handler; + address[5] internal handlerActors; + + /// @dev Pinned mainnet block (M1). Pinning removes the block-to-block drift + /// that made the old latest-block setUp's hardcoded state assumptions + /// (pending count, in-LP size) fragile. Every state-dependent value + /// below is DERIVED from the fork at this block, not hardcoded. + uint256 internal constant PINNED_BLOCK = 25447657; + + // N1: post-setUp baselines. setUp seeds a full lifecycle (creates + finalizes + // requests), so the created/finalized non-vacuity gates are pre-satisfied by + // the seed. Record the seeded baselines and require the fuzzer to move + // STRICTLY ABOVE them, so those gates reflect genuine fuzz activity. + uint256 internal baselineCreated; + uint256 internal baselineFinalized; + + function setUp() public { + initializeRealisticForkWithBlock(MAINNET_FORK, PINNED_BLOCK); + + // WithdrawRequestNFT is already unpaused on the fork at the current + // block; unpause defensively only if needed (OPERATION_MULTISIG = alice). + if (withdrawRequestNFTInstance.paused()) { + vm.prank(alice); + withdrawRequestNFTInstance.unpause(); + } + + // Grant GUARDIAN_ROLE to alice so the S3 probe can call the + // guardian-gated invalidateRequest. The fork setUp intentionally does not + // grant GUARDIAN to anyone; this test needs it. alice already holds + // OPERATION_TIMELOCK_ROLE, used for the timelock-gated validateRequest. + // Resolve the role id and owner BEFORE vm.prank — an external call in the + // grantRole arguments would otherwise consume the single-shot prank and + // run grantRole as the test contract (EnumerableRolesUnauthorized). + bytes32 _guardianRole = roleRegistryInstance.GUARDIAN_ROLE(); + address _rrOwner = roleRegistryInstance.owner(); + vm.prank(_rrOwner); + roleRegistryInstance.grantRole(_guardianRole, alice); + + // DERIVE the pre-existing pending backlog (M1): sum the requested eETH of + // every unfinalized request at the pinned block. This is the exact ETH + // that must be lockable to finalize the whole backlog; we size the actor + // deposits from it so the finalize can never be starved (no silent skip + // in _finalizePreExistingPending), regardless of how the backlog drifts + // if the pinned block is ever changed. + uint256 backlogTotal = _preExistingBacklogTotal(); + + // 5 actors. Each deposit is DERIVED from the backlog: a per-actor share + // of the backlog plus a fixed working buffer for our own seed/fuzz + // requests. This guarantees totalValueInLp backs both the backlog + // finalize and our requests without assuming any particular baseline + // in-LP size. + uint256 perActorDeposit = backlogTotal / 5 + 800 ether; + for (uint256 i = 0; i < 5; i++) { + address a = address(uint160(uint256(keccak256(abi.encodePacked("i3.solvency.actor.", i))))); + handlerActors[i] = a; + vm.deal(a, perActorDeposit + 1 ether); + vm.prank(a); + liquidityPoolInstance.deposit{value: perActorDeposit}(); + vm.prank(a); + eETHInstance.approve(address(liquidityPoolInstance), type(uint256).max); + } + + // Finalize the PRE-EXISTING mainnet pending range once, mirroring what + // EtherFiAdmin does in production (finalizeRequests the range, then lock + // its summed eETH via addEthAmountLockedForWithdrawal). This clears + // the legacy pending requests that would otherwise sit ahead of our fresh + // tokenIds in id-order and make finalizing+claiming OUR requests + // unreachable within a single fuzz sequence. The lock amount is fully + // backed by the derived deposits above. This is setup, not an + // assertion-bearing path; the fuzzed finalize op then operates on our own + // fresh requests. P1's bound is still exercised (and counted) on every + // fuzzed finalize. + _finalizePreExistingPending(); + + handler = new WithdrawalSolvencyHandler( + liquidityPoolInstance, + eETHInstance, + withdrawRequestNFTInstance, + address(etherFiAdminInstance), + handlerActors, + alice, // guardian (GUARDIAN_ROLE granted above) + alice // operating timelock (OPERATION_TIMELOCK_ROLE on the fork) + ); + + targetContract(address(handler)); + + // Restrict fuzzing to the action functions. Without this, the engine + // also targets the handler's public getters/counters, burning call + // budget on no-ops. probeOverLiquidityLock is included so the I3/P1 + // liquidity guard is positively driven on every run. rebasePositive/ + // rebaseNegative add rate churn (bounded so the share rate stays well + // above minAmountForShare) and are driven through the real + // etherFiAdminContract caller that LiquidityPool.rebase requires. + // doInvalidateValidateProbe drives the S3 invalidate/validate lifecycle. + bytes4[] memory sel = new bytes4[](7); + sel[0] = handler.requestWithdraw.selector; + sel[1] = handler.finalizeRequests.selector; + sel[2] = handler.claimWithdraw.selector; + sel[3] = handler.probeOverLiquidityLock.selector; + sel[4] = handler.rebasePositive.selector; + sel[5] = handler.rebaseNegative.selector; + sel[6] = handler.doInvalidateValidateProbe.selector; + targetSelector(FuzzSelector({addr: address(handler), selectors: sel})); + + // Pre-seed a batch of OUR OWN requests and finalize them, so every fuzz + // run starts with claimable inventory the `claimWithdraw` op can hit. + // Foundry resets handler/contract state to this post-setUp snapshot + // before each run, so this inventory is present at the start of every + // run — making the request→finalize→claim chain reachable within the + // run depth (otherwise a claim, which requires three distinct ops in + // sequence, almost never completes and the non-vacuity gate is unmet). + // + // NOTE: these seed requests are created/finalized THROUGH the handler + // (its real ops, EtherFiAdmin-pranked finalize), so they are + // indistinguishable from fuzzed ones. The fuzzer still independently + // exercises requestWithdraw / finalizeRequests / claimWithdraw at + // runtime (see the call-coverage summary), so non-vacuity reflects + // genuine fuzz activity, not just this seed. + for (uint256 i = 0; i < 24; i++) { + handler.requestWithdraw(i, uint128(uint256(keccak256(abi.encodePacked("seed", i))))); + } + handler.finalizeRequests(type(uint256).max); + + // Seed the S3 invalidate/validate probe once so its non-vacuity counters + // (invalidate/validate round-trip + finalized-invalidate rejection) fire + // reliably on every run regardless of the fuzzed sequence. + handler.doInvalidateValidateProbe(0, uint128(uint256(keccak256("seed.probe")))); + + // N1: record the seeded lifecycle baselines AFTER all seeding, so the + // created/finalized gates require strictly-above-baseline fuzz activity. + baselineCreated = handler.ghost_requestsCreated(); + baselineFinalized = handler.ghost_requestsFinalized(); + } + + /// @dev DERIVE the summed requested eETH of the pre-existing pending range at + /// the pinned block. Used to size actor deposits so the backlog finalize + /// is always backed (M1). + function _preExistingBacklogTotal() internal view returns (uint256 total) { + uint32 lastFin = withdrawRequestNFTInstance.lastFinalizedRequestId(); + uint32 nextId = withdrawRequestNFTInstance.nextRequestId(); + for (uint32 id = lastFin + 1; id < nextId; id++) { + total += uint256(withdrawRequestNFTInstance.getRequest(id).amountOfEEth); + } + } + + /// @dev Finalize the pre-existing mainnet pending range in bounded batches, + /// mirroring EtherFiAdmin._finalizeWithdrawals order EXACTLY: + /// `finalizeRequests` first, then `addEthAmountLockedForWithdrawal` for + /// the batch's summed eETH (order is inert here since neither call reads + /// the other's state, but it stays identical to production and to the + /// handler's _finalizeThenLock so all paths agree on the flow). The + /// actor deposits in setUp are DERIVED from the backlog total, so every + /// batch is backed by construction; if a batch is ever unbacked the + /// setUp fails loudly (require) rather than silently skipping it and + /// leaving the seeds starved behind an unfinalized backlog (M1). + function _finalizePreExistingPending() internal { + uint32 lastFin = withdrawRequestNFTInstance.lastFinalizedRequestId(); + uint32 nextId = withdrawRequestNFTInstance.nextRequestId(); + while (lastFin + 1 < nextId) { + uint32 remaining = nextId - 1 - lastFin; + uint32 advance = remaining > 80 ? 80 : remaining; + uint32 target = lastFin + advance; + + uint256 lockAmount; + for (uint32 id = lastFin + 1; id <= target; id++) { + lockAmount += uint256(withdrawRequestNFTInstance.getRequest(id).amountOfEEth); + } + require( + lockAmount <= uint256(liquidityPoolInstance.totalValueInLp()), + "setUp: derived deposits do not back the pre-existing backlog" + ); + + vm.prank(address(etherFiAdminInstance)); + withdrawRequestNFTInstance.finalizeRequests(uint256(target)); + if (lockAmount > 0) { + vm.prank(address(etherFiAdminInstance)); + liquidityPoolInstance.addEthAmountLockedForWithdrawal(uint128(lockAmount)); + } + lastFin = target; + } + } + + // ===================================================================== + // I3 — P1: finalize never exceeds liquidity (SC-enforced bound) + // ===================================================================== + + function invariant_i3_finalized_backed_by_liquidity() public view { + assertFalse( + handler.ghost_finalizeExceededLiquidity(), + string.concat( + "I3/P1: a finalize+lock SUCCEEDED with lockAmount > totalValueInLp - lock=", + vm.toString(handler.ghost_failLockAmount()), + " inLp=", vm.toString(handler.ghost_failInLp()) + ) + ); + // Dual direction: the guard must not reject a lock that WAS backed. + assertFalse( + handler.ghost_lockRejectedWhileBacked(), + string.concat( + "I3/P1: _lockEth rejected a backed lock (lockAmount <= totalValueInLp) - lock=", + vm.toString(handler.ghost_failLockAmount()), + " inLp=", vm.toString(handler.ghost_failInLp()) + ) + ); + } + + // ===================================================================== + // I3 — P2: locked obligation within accounted state + // (ASSUMPTION-SCOPED: bounded rebases — see file header) + // ===================================================================== + + /// The outstanding finalized-but-unclaimed obligation (the lock) stays a + /// subset of out-of-LP value under the finalize/claim operations alone. This + /// bound is NOT unconditional: a large negative rebase drops totalValueOutOfLp + /// without touching the lock. It holds here because the handler caps negative + /// rebases (rebaseNegative input filter); the protocol-level defense is + /// EtherFiAdmin's rebase-APR caps. + function invariant_i3_locked_within_accounted_state() public view { + uint256 lock = uint256(withdrawRequestNFTInstance.ethAmountLockedForWithdrawal()); + uint256 outOfLp = uint256(liquidityPoolInstance.totalValueOutOfLp()); + assertLe(lock, outOfLp, "I3/P2: ethAmountLockedForWithdrawal > totalValueOutOfLp"); + assertLe(lock, liquidityPoolInstance.getTotalPooledEther(), + "I3/P2: ethAmountLockedForWithdrawal > getTotalPooledEther"); + } + + /// Segregated-escrow solvency: WRN's own ETH balance always backs its lock + /// counter. This is what the claim payout draws on. + function invariant_i3_escrow_backs_lock() public view { + assertGe( + address(withdrawRequestNFTInstance).balance, + uint256(withdrawRequestNFTInstance.ethAmountLockedForWithdrawal()), + "I3/P2: WRN balance < ethAmountLockedForWithdrawal" + ); + } + + // ===================================================================== + // I3 — P3: a finalized request is always claimable (SC-enforced) + // ===================================================================== + + function invariant_i3_finalized_always_claimable() public view { + assertFalse( + handler.ghost_finalizedClaimFailed(), + string.concat( + "I3/P3: a finalized+valid+owned+in-escrow request reverted on claim - tokenId=", + vm.toString(handler.ghost_failTokenId()), + " selector=", vm.toString(uint256(uint32(handler.ghost_failSelector()))) + ) + ); + } + + // ===================================================================== + // I3 — M3: every successful claim moves the exact contract-correct deltas + // ===================================================================== + + /// A successful claimWithdraw must move all three balances by their exact, + /// independently-recomputed deltas: recipient += amountToWithdraw, lock -= + /// request.amountOfEEth (the FULL escrowed amount), totalValueOutOfLp -= + /// (amountToWithdraw + stranded-ETH sweep). Any mismatch means the withdrawal + /// accounting silently diverged from the value actually paid out. + function invariant_i3_claim_deltas_exact() public view { + assertFalse( + handler.ghost_claimDeltaViolated(), + string.concat( + "I3/M3: claim moved a balance by the wrong amount - tokenId=", + vm.toString(handler.ghost_deltaFailTokenId()), + " expected=", vm.toString(handler.ghost_deltaFailExpected()), + " actual=", vm.toString(handler.ghost_deltaFailActual()) + ) + ); + } + + // ===================================================================== + // I3 — S3: invalidate/validate lifecycle behaves as specified + // ===================================================================== + + /// Invalidating a non-finalized request makes it unclaimable (claim reverts + /// RequestNotValid); validating it restores its validity; and invalidating a + /// FINALIZED request is always rejected with CannotInvalidateFinalizedRequest. + function invariant_i3_invalidate_validate_lifecycle() public view { + assertFalse( + handler.ghost_invalidateProbeFailed(), + "I3/S3: invalidate/validate round-trip produced an unexpected outcome" + ); + assertFalse( + handler.ghost_finalizedInvalidateAllowed(), + "I3/S3: invalidateRequest on a finalized request was not rejected" + ); + } + + // ===================================================================== + // LP TVL decomposition sanity (must always hold) + // ===================================================================== + + function invariant_i3_tvl_decomposition() public view { + assertEq( + uint256(liquidityPoolInstance.totalValueInLp()) + + uint256(liquidityPoolInstance.totalValueOutOfLp()), + liquidityPoolInstance.getTotalPooledEther(), + "TVL decomposition broken" + ); + } + + function invariant_i3_lp_solvent_in_lp() public view { + assertGe( + address(liquidityPoolInstance).balance, + uint256(liquidityPoolInstance.totalValueInLp()), + "LP balance < totalValueInLp" + ); + } + + // ===================================================================== + // NON-VACUITY GATES (afterInvariant) + // ===================================================================== + // + // Proves the fuzzer actually drove the full lifecycle — requests created + // AND finalized AND claimed — and that P1's bound was positively verified + // through at least one successful lock. Without these gates, "no violation" + // could be trivially true because no request was ever finalized/claimed. + + function afterInvariant() public { + emit log_named_uint("requestsCreated ", handler.ghost_requestsCreated()); + emit log_named_uint("requestsFinalized ", handler.ghost_requestsFinalized()); + emit log_named_uint("requestsClaimed ", handler.ghost_requestsClaimed()); + emit log_named_uint("finalizeBoundChecks ", handler.ghost_finalizeBoundChecks()); + emit log_named_uint("lockBoundEnforced ", handler.ghost_lockBoundEnforced()); + emit log_named_uint("claimDeltaChecks ", handler.ghost_claimDeltaChecks()); + emit log_named_uint("invValidateProbes ", handler.ghost_invalidateValidateProbes()); + emit log_named_uint("finalizedInvRejected", handler.ghost_finalizedInvalidateRejected()); + emit log_named_uint("baselineCreated ", baselineCreated); + emit log_named_uint("baselineFinalized ", baselineFinalized); + + // N1: created/finalized are pre-satisfied by the setUp seed, so require + // the fuzzer to move STRICTLY ABOVE the recorded baselines (genuine fuzz + // activity, not just the seed). + assertGt(handler.ghost_requestsCreated(), baselineCreated, "non-vacuity: fuzzer created no NEW withdraw request beyond the seed"); + assertGt(handler.ghost_requestsFinalized(), baselineFinalized, "non-vacuity: fuzzer finalized no NEW request beyond the seed"); + // Claims are never seeded in setUp, so `> 0` is already fuzz-genuine. + assertGt(handler.ghost_requestsClaimed(), 0, "non-vacuity: no finalized request was ever claimed"); + assertGt(handler.ghost_finalizeBoundChecks(), 0, "non-vacuity: P1 liquidity bound never exercised"); + // P1 enforcement must be POSITIVELY driven: the liquidity guard rejected + // at least one genuinely over-backed lock. This is what makes I3/P1 a + // live assertion rather than dead code. + assertGt(handler.ghost_lockBoundEnforced(), 0, "non-vacuity: P1 liquidity guard never rejected an over-bound lock"); + // M3: at least one claim's exact three-way deltas were verified (never + // seeded — a claim only happens under the fuzzer, so this is fuzz-genuine). + assertGt(handler.ghost_claimDeltaChecks(), 0, "non-vacuity: M3 claim-delta check never exercised"); + // S3: the invalidate/validate lifecycle and finalized-invalidate rejection + // were driven (seeded once in setUp, so reliably > 0 every run). + assertGt(handler.ghost_invalidateValidateProbes(), 0, "non-vacuity: S3 invalidate/validate round-trip never completed"); + assertGt(handler.ghost_finalizedInvalidateRejected(), 0, "non-vacuity: S3 finalized-invalidate rejection never exercised"); + } + + // ===================================================================== + // COVERAGE SUMMARY + // ===================================================================== + + function invariant_call_coverage_summary() public { + emit log_named_uint("req ", handler.callCounts("req")); + emit log_named_uint("req_skipped_funds ", handler.callCounts("req_skipped_funds")); + emit log_named_uint("req_revert ", handler.callCounts("req_revert")); + emit log_named_uint("finalize ", handler.callCounts("finalize")); + emit log_named_uint("finalize_skipped_none ", handler.callCounts("finalize_skipped_none")); + emit log_named_uint("finalize_skipped_liquidity ", handler.callCounts("finalize_skipped_liquidity")); + emit log_named_uint("finalize_revert ", handler.callCounts("finalize_revert")); + emit log_named_uint("lock_revert_liquidity ", handler.callCounts("lock_revert_liquidity")); + emit log_named_uint("lock_revert_migration ", handler.callCounts("lock_revert_migration")); + emit log_named_uint("lock_revert_other ", handler.callCounts("lock_revert_other")); + emit log_named_uint("probe_rejected_liquidity ", handler.callCounts("probe_rejected_liquidity")); + emit log_named_uint("probe_unexpected_ok ", handler.callCounts("probe_unexpected_ok")); + emit log_named_uint("claim ", handler.callCounts("claim")); + emit log_named_uint("claim_skipped_empty ", handler.callCounts("claim_skipped_empty")); + emit log_named_uint("claim_skipped_unfinalized ", handler.callCounts("claim_skipped_unfinalized")); + emit log_named_uint("claim_skipped_claimed ", handler.callCounts("claim_skipped_claimed")); + emit log_named_uint("claim_skipped_rate ", handler.callCounts("claim_skipped_rate")); + emit log_named_uint("claim_revert ", handler.callCounts("claim_revert")); + emit log_named_uint("rebase_pos ", handler.callCounts("rebase_pos")); + emit log_named_uint("rebase_neg ", handler.callCounts("rebase_neg")); + emit log_named_uint("rebase_neg_skipped ", handler.callCounts("rebase_neg_skipped")); + emit log_named_uint("invalidate_ok ", handler.callCounts("invalidate_ok")); + emit log_named_uint("invalidated_claim_rejected ", handler.callCounts("invalidated_claim_rejected")); + emit log_named_uint("validate_ok ", handler.callCounts("validate_ok")); + emit log_named_uint("revalidated_claim_rejected ", handler.callCounts("revalidated_claim_rejected")); + emit log_named_uint("invalidate_finalized_reject", handler.callCounts("invalidate_finalized_rejected")); + } +} diff --git a/test/invariant/handlers/OracleIntegrityHandler.sol b/test/invariant/handlers/OracleIntegrityHandler.sol new file mode 100644 index 000000000..32c608367 --- /dev/null +++ b/test/invariant/handlers/OracleIntegrityHandler.sol @@ -0,0 +1,759 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "forge-std/Test.sol"; +import "@etherfi/oracle/EtherFiOracle.sol"; +import "@etherfi/oracle/EtherFiAdmin.sol"; +import "@etherfi/oracle/interfaces/IEtherFiOracle.sol"; +import "@etherfi/core/interfaces/ILiquidityPool.sol"; + +/// @notice Stateful-fuzz handler for invariant I5 (Oracle Integrity). +/// +/// I5: an OracleReport may only ADVANCE EtherFiAdmin.lastHandledReportRefSlot +/// (i.e. be "applied" by executeTasks) when ALL gates hold at the +/// moment of execution: +/// (a) quorum — consensus reached with >= quorumSize() submissions +/// (b) APR cap — abs(rebase APR) <= acceptableRebaseAprInBps() +/// (c) freshness — currentSlot >= postReportWaitTimeInSlots + consensusSlot +/// (d) neg cap — a negative rebase drops TVL by at most +/// effectiveMaxNegativeRebaseBps() (independent of elapsedTime) +/// +/// The handler drives ONE fuzzer-selectable, self-healing action (`step`) +/// whose seed selects among several scenarios against the real EtherFiOracle + +/// EtherFiAdmin contracts. Each scenario is self-contained and leaves the +/// oracle in the un-stuck state on exit: +/// - apply : a fully valid report -> MUST apply (all gates hold) +/// - quorum-fail : only ONE committee member submits (< quorum=2) +/// -> consensus never reached -> executeTasks MUST revert +/// - apr-fail : accruedRewards sized so |APR| > cap +/// -> executeTasks MUST revert ("TVL changed too much"), +/// then unpublished to leave the oracle un-stuck +/// - fresh-fail : consensus reached but executeTasks called BEFORE the +/// post-report wait window -> MUST revert ("too fresh"), +/// then (after warping past it) applied to leave state +/// un-stuck. +/// - duplicate : one member submits, then submits the SAME report again +/// -> the second submit MUST revert ReportNotNeeded, a +/// single member is sub-quorum so consensus is NOT +/// reached, and executeTasks MUST reject on quorum. +/// - conflicting : A submits reward X, B submits reward Y != X for the same +/// range -> the two distinct hashes each carry one vote, so +/// NEITHER reaches consensus and executeTasks reverts for +/// both. Nothing is published, so the sequence resolves on +/// the next fresh range (no permanent stuck state). +/// - fresh-bound : exact freshness boundary. At consensusSlot + wait - 1 +/// executeTasks MUST revert ("too fresh"); at exactly +/// consensusSlot + wait it MUST apply. +/// - apr-bound : exact APR boundary. The largest reward whose annualized +/// |APR| still satisfies the cap MUST apply; that reward + 1 +/// wei MUST revert ("TVL changed too much"). +/// - neg-rebase : a small valid negative drop (under both the APR cap and +/// the negative-rebase cap) MUST apply; a drop one wei above +/// the negative-rebase cap (but under the APR cap) MUST +/// revert ("negative rebase exceeds cap"). +/// +/// Before every executeTasks call the handler computes an INDEPENDENT mirror +/// of the gates (re-deriving the APR / negative cap exactly as EtherFiAdmin +/// does) and: +/// 1. SAFETY: if lastHandledReportRefSlot advanced, asserts all mirror gates +/// held — any false flips a ghost that the invariant functions assert +/// against (this is the actual I5 proof). +/// 2. MIRROR-CONSISTENCY: when executeTasks reverts with a known +/// ReportValidationFailed reason, asserts our independent mirror agrees +/// on which gate failed — cross-validating that the mirror is faithful, +/// so the safety check above is sound (not vacuously satisfied by a +/// broken oracle). +/// +/// SOUNDNESS ASSUMPTIONS (all documented inline below): +/// * The committee is exactly {alice, bob} with quorumSize == 2, as set up by +/// TestSetup. doQuorumFail / the duplicate + conflicting scenarios rely on a +/// single submission being strictly below quorum. +/// * Reports are built so that ONLY the gate under test (or none) can fail: +/// refSlot/refBlock stamps are taken from blockStampForNextReport(), +/// protocolFees == 0, no validator approvals, no withdrawals. Thus a revert +/// is attributable to quorum / freshness / APR / negative-cap (or, harmlessly, +/// a structural reason which we simply don't attribute). +contract OracleIntegrityHandler is Test { + // --- I5 contract constants mirrored from EtherFiAdmin --- + uint256 internal constant BASIS_POINTS_DENOMINATOR = 10_000; + uint256 internal constant SECONDS_PER_SLOT = 12; + // Mirror of LiquidityPool.MAX_POSITIVE_REBASE_BPS (not exposed on ILiquidityPool): + // an absolute per-report positive-rebase cap enforced in LiquidityPool.rebase, + // independent of the oracle-side annualized APR cap. A boundary "apply" whose + // reward sits at the APR cap must also stay under this or LiquidityPool reverts + // with RebaseExceedsPositiveCap (a different, non-I5 error). + int256 internal constant LP_MAX_POSITIVE_REBASE_BPS = 25; + + EtherFiOracle internal immutable oracle; + EtherFiAdmin internal immutable admin; + ILiquidityPool internal immutable lp; + address internal immutable memberA; // alice + address internal immutable memberB; // bob + address internal immutable multisig; // holds OPERATION_MULTISIG_ROLE (unpublishReport) + uint256 internal immutable genesisTime; // BEACON_GENESIS_TIME used by oracle + + // ---- I5 violation ghosts (any true => invariant broken) ---- + bool public ghost_appliedWithoutQuorum; + bool public ghost_appliedWhileStale; + bool public ghost_appliedAprViolation; + bool public ghost_appliedNegRebaseViolation; // applied while the negative-rebase cap was violated + // mirror-consistency ghost: a revert reason disagreed with our gate mirror + bool public ghost_mirrorMismatch; + string public mismatchReason; + + // ---- duplicate / conflicting submission ghosts ---- + bool public ghost_duplicateSubmitSucceeded; // a member's duplicate submit did NOT revert + bool public ghost_duplicateWrongError; // duplicate submit reverted with a non-ReportNotNeeded error + string public duplicateWrongErrorReason; + bool public ghost_consensusFromSingle; // consensus reached from a single member's submissions + bool public ghost_conflictReachedConsensus; // two conflicting one-vote reports reached consensus + + // ---- exact-boundary ghosts (a boundary report that MUST apply failed to) ---- + bool public ghost_freshBoundaryRejected; // report at consensusSlot+wait failed to apply + bool public ghost_aprBoundaryRejected; // report at the exact APR cap failed to apply + bool public ghost_negValidRejected; // a valid small negative drop failed to apply + + // ---- permanent-wedge ghost: the oracle never recovered from a stuck state ---- + bool public ghost_everStuck; + uint256 internal consecutiveGuardSkips; // consecutive `step` calls short-circuited by the top guard + // A single scenario intentionally passes through a transient published-but-unapplied + // state (apr-fail / neg-reject before the unpublish recovery). What we must never + // observe is the oracle staying wedged: many `step` calls in a row unable to make + // any progress because lastPublished != lastHandled. Flag if that tail runs long. + uint256 internal constant MAX_CONSECUTIVE_STUCK_SKIPS = 10; + + // ---- coverage / non-vacuity counters ---- + uint256 public numApplied; // executeTasks that advanced lastHandledReportRefSlot + uint256 public numRejected; // executeTasks that reverted + uint256 public numRejQuorum; // reverts attributed to the quorum gate + uint256 public numRejFresh; // reverts attributed to the freshness gate + uint256 public numRejApr; // reverts attributed to the APR gate + uint256 public numRejNegRebase; // reverts attributed to the negative-rebase cap + uint256 public numRejOther; // reverts for structural/uncategorised reasons + uint256 public numDupRejected; // duplicate submits correctly rejected + uint256 public numConflictExercised; // conflicting-report scenarios that ran to executeTasks + uint256 public numFreshBoundaryApplied; // reports applied at exactly consensusSlot+wait + uint256 public numAprBoundaryApplied; // reports applied at exactly the APR cap boundary + uint256 public numNegAccepted; // valid small negative drops applied + + constructor( + EtherFiOracle _oracle, + EtherFiAdmin _admin, + ILiquidityPool _lp, + address _memberA, + address _memberB, + address _multisig, + uint256 _genesisTime + ) { + oracle = _oracle; + admin = _admin; + lp = _lp; + memberA = _memberA; + memberB = _memberB; + multisig = _multisig; + genesisTime = _genesisTime; + } + + // ------------------------------------------------------------------------- + // clock helpers (mirror TestSetup._moveClock for the local non-fork setup, + // where BEACON_GENESIS_TIME == genesisTime and slot == block.number) + // ------------------------------------------------------------------------- + function _moveClock(uint256 numSlots) internal { + vm.roll(block.number + numSlots); + vm.warp(genesisTime + SECONDS_PER_SLOT * block.number); + } + + /// @dev Advance the clock so that the report range ending at `refSlotTo` + /// is considered finalized by the oracle (>= 3 epochs past), mirroring + /// TestSetup._executeAdminTasks / _submitForConsensus. + function _finalizeEpochFor(uint32 refSlotTo) internal { + uint32 currentSlot = oracle.computeSlotAtTimestamp(block.timestamp); + uint32 currentEpoch = currentSlot / 32; + uint32 reportEpoch = (refSlotTo / 32) + 3; + if (currentEpoch < reportEpoch) { + _moveClock(32 * uint256(reportEpoch - currentEpoch)); + } + } + + function _baseReport() internal view returns (IEtherFiOracle.OracleReport memory r) { + uint256[] memory emptyVals = new uint256[](0); + uint32 cv = oracle.consensusVersion(); + r = IEtherFiOracle.OracleReport(cv, 0, 0, 0, 0, 0, 0, emptyVals, 0, 0); + (uint32 slotFrom, uint32 slotTo, uint32 blockFrom) = oracle.blockStampForNextReport(); + r.refSlotFrom = slotFrom; + r.refSlotTo = slotTo; + r.refBlockFrom = blockFrom; + r.refBlockTo = slotTo; // same convention as TestSetup._initReportBlockStamp + } + + // ------------------------------------------------------------------------- + // independent gate mirror — re-derives the I5 gates from live state, + // WITHOUT calling EtherFiAdmin's internal validators. Kept byte-for-byte + // faithful to EtherFiAdmin._validateReportFreshness / _validateRebaseApr so + // the consistency cross-check below can confirm fidelity. + // ------------------------------------------------------------------------- + function _gatesHold(IEtherFiOracle.OracleReport memory r, bytes32 reportHash) + internal + view + returns (bool quorum, bool fresh, bool apr, bool negOk) + { + // (a) quorum: consensus flag is only set once support >= quorumSize. + quorum = oracle.isConsensusReached(reportHash); + + // (c) freshness: contract checks this only after consensus; getConsensusSlot + // reverts when no consensus, so guard on `quorum`. Without consensus the + // freshness gate is, by construction, not satisfiable. + if (quorum) { + uint32 curSlot = oracle.computeSlotAtTimestamp(block.timestamp); + uint32 consSlot = oracle.getConsensusSlot(reportHash); + fresh = curSlot >= uint256(admin.postReportWaitTimeInSlots()) + consSlot; + } else { + fresh = false; + } + + // (b) APR cap: identical arithmetic to EtherFiAdmin._validateRebaseApr. + int256 currentTVL = int128(uint128(lp.getTotalPooledEther())); + uint256 elapsedSlots = uint256(r.refSlotTo) - uint256(admin.lastHandledReportRefSlot()); + uint256 elapsedTime = elapsedSlots * SECONDS_PER_SLOT; + int256 aprVal; + if (currentTVL > 0 && elapsedTime > 0) { + aprVal = int256(BASIS_POINTS_DENOMINATOR) * (int256(r.accruedRewards) * int256(365 days)) + / (currentTVL * int256(elapsedTime)); + } + int256 absApr = aprVal > 0 ? aprVal : -aprVal; + apr = absApr <= admin.acceptableRebaseAprInBps(); + + // (d) negative-rebase cap: identical arithmetic to EtherFiAdmin._validateRebaseApr's + // independent negative branch. negOk == "the drop is within the cap". + negOk = true; + if (r.accruedRewards < 0 && currentTVL > 0) { + int256 drop = -int256(r.accruedRewards); + if (drop * int256(BASIS_POINTS_DENOMINATOR) > currentTVL * int256(admin.effectiveMaxNegativeRebaseBps())) { + negOk = false; + } + } + } + + function _strEq(string memory a, string memory b) internal pure returns (bool) { + return keccak256(bytes(a)) == keccak256(bytes(b)); + } + + /// @dev Decode the reason string out of a ReportValidationFailed(string) revert. + function _decodeReason(bytes memory err) internal pure returns (bool ok, string memory reason) { + // selector(4) + offset(32) + length(32) + data + if (err.length < 4) return (false, ""); + bytes4 sel; + assembly { sel := mload(add(err, 0x20)) } + if (sel != EtherFiAdmin.ReportValidationFailed.selector) return (false, ""); + bytes memory payload = new bytes(err.length - 4); + for (uint256 i = 0; i < payload.length; i++) payload[i] = err[i + 4]; + reason = abi.decode(payload, (string)); + ok = true; + } + + /// @dev Core driver: snapshots lastHandledReportRefSlot, computes the mirror + /// gates, calls executeTasks, then runs the SAFETY + MIRROR checks. + function _executeAndCheck(IEtherFiOracle.OracleReport memory r) internal { + bytes32 reportHash = oracle.generateReportHash(r); + (bool quorum, bool fresh, bool apr, bool negOk) = _gatesHold(r, reportHash); + uint32 before = admin.lastHandledReportRefSlot(); + + try admin.executeTasks(r) { + uint32 afterSlot = admin.lastHandledReportRefSlot(); + bool applied = afterSlot != before; + if (applied) { + numApplied++; + // ---- I5 SAFETY: a state-advancing report MUST satisfy all gates ---- + if (!quorum) ghost_appliedWithoutQuorum = true; + if (!fresh) ghost_appliedWhileStale = true; + if (!apr) ghost_appliedAprViolation = true; + if (!negOk) ghost_appliedNegRebaseViolation = true; + } + } catch (bytes memory err) { + numRejected++; + (bool ok, string memory reason) = _decodeReason(err); + if (ok) { + // ---- MIRROR-CONSISTENCY: the first failing gate the contract + // reports must match our independent mirror. ---- + if (_strEq(reason, "EtherFiAdmin: report didn't reach consensus")) { + numRejQuorum++; + if (quorum) { ghost_mirrorMismatch = true; mismatchReason = "quorum gate disagreement"; } + } else if (_strEq(reason, "EtherFiAdmin: report is too fresh")) { + numRejFresh++; + // contract reached the freshness stage => consensus held but window not elapsed + if (!quorum || fresh) { ghost_mirrorMismatch = true; mismatchReason = "freshness gate disagreement"; } + } else if (_strEq(reason, "EtherFiAdmin: TVL changed too much")) { + numRejApr++; + // contract reached the APR stage => consensus + freshness held, APR failed + if (!quorum || !fresh || apr) { ghost_mirrorMismatch = true; mismatchReason = "apr gate disagreement"; } + } else if (_strEq(reason, "EtherFiAdmin: negative rebase exceeds cap")) { + numRejNegRebase++; + // contract reached the neg-cap stage => consensus + freshness + APR-cap + // held (APR is checked first), and the negative-drop cap failed. + if (!quorum || !fresh || !apr || negOk) { ghost_mirrorMismatch = true; mismatchReason = "negative-rebase gate disagreement"; } + } else { + numRejOther++; + } + } else { + numRejOther++; + } + } + } + + // ------------------------------------------------------------------------- + // FUZZ ACTION — a SINGLE self-healing step. + // + // The oracle is a strict state machine: it can only accept a new report when + // `lastPublishedReportRefSlot == lastHandledReportRefSlot` (enforced by + // shouldSubmitReport's LastReportNotHandled guard). A half-finished + // (published-but-unapplied) state between fuzz calls bricks every subsequent + // submitReport. To be fully robust to fuzzer call ordering AND to Foundry's + // sequence shrinking (which replays arbitrary single-call subsequences), a + // single `step` call runs ALL scenarios in sequence — each self-contained and + // each leaving the oracle in the un-stuck state on exit. This makes EVERY + // single call non-vacuous by construction (>=1 apply and >=1 of each reject + // gate), so the non-vacuity gates in afterInvariant hold regardless of how the + // fuzzer schedules or shrinks calls. The fuzzer's `magnitude` varies the rebase + // size across calls, exercising the safety property over a wide state space. + // ------------------------------------------------------------------------- + + /// @param magnitude bounded magnitude used for the rebase reward (fuzzed) + function step(uint256 magnitude) external { + // Self-heal: never proceed from a stuck state (defensive; by construction + // each sub-scenario below leaves the oracle un-stuck). Track how many calls + // in a row are wedged so afterInvariant can flag a PERMANENT stuck oracle. + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) { + consecutiveGuardSkips++; + if (consecutiveGuardSkips > MAX_CONSECUTIVE_STUCK_SKIPS) ghost_everStuck = true; + return; + } + consecutiveGuardSkips = 0; + + _scenarioApply(magnitude); + _scenarioQuorumFail(magnitude); + _scenarioAprFail(magnitude); + _scenarioFreshFail(magnitude); + _scenarioDuplicateSubmit(magnitude); + _scenarioConflictingReports(magnitude); + _scenarioFreshBoundary(magnitude); + _scenarioAprBoundary(magnitude); + _scenarioNegRebase(magnitude); + } + + /// @dev Open a fresh, finalized, un-handled report range. Returns (ok, report). + /// ok=false when no new range is available yet (caller should skip). + function _freshRange() internal returns (bool ok, IEtherFiOracle.OracleReport memory r) { + _moveClock(1024 + 2 * 32); + r = _baseReport(); + if (r.refSlotTo <= admin.lastHandledReportRefSlot()) return (false, r); + _finalizeEpochFor(r.refSlotTo); + r = _resyncStamps(r); + ok = true; + } + + /// @dev Largest rebase reward that keeps |APR| strictly under the cap for the + /// given report range (the boundary reward at which apr == cap), CLAMPED + /// to LiquidityPool's absolute positive-rebase cap + /// (MAX_POSITIVE_REBASE_BPS of TVL). The APR gate scales with the range's + /// elapsed time, so over a long range the APR-derived bound alone can + /// exceed the LP's per-rebase cap; a reward in that gap passes + /// EtherFiAdmin validation but reverts inside LiquidityPool.rebase + /// (RebaseExceedsPositiveCap), leaving the report published-but-unhandled + /// and wedging the oracle. A valid "apply" must stay BELOW both caps; + /// callers use half of this for safe margin. + function _maxSafeReward(IEtherFiOracle.OracleReport memory r) internal view returns (int256) { + int256 tvl = int128(uint128(lp.getTotalPooledEther())); + uint256 elapsedTime = (uint256(r.refSlotTo) - uint256(admin.lastHandledReportRefSlot())) * SECONDS_PER_SLOT; + if (tvl <= 0 || elapsedTime == 0) return 0; + int256 cap = admin.acceptableRebaseAprInBps(); + // reward at apr==cap boundary: cap = 10000 * (reward*365d)/(tvl*elapsedTime) + int256 aprMax = cap * tvl * int256(elapsedTime) / (int256(BASIS_POINTS_DENOMINATOR) * int256(365 days)); + int256 lpMax = _lpPositiveCap(); + return aprMax < lpMax ? aprMax : lpMax; + } + + /// @dev EXACT largest reward R (in wei) whose annualized |APR| still satisfies + /// the cap, i.e. the maximum acceptable accruedRewards for this range. + /// The contract computes apr = floor(K*R / D) with K = 10000*365d and + /// D = tvl*elapsedTime, and rejects when apr > cap. So R is accepted iff + /// floor(K*R/D) <= cap <=> K*R < (cap+1)*D. The largest such integer R + /// is floor(((cap+1)*D - 1) / K); R+1 makes K*(R+1) >= (cap+1)*D, forcing + /// apr >= cap+1 (a strict rejection). This is the exact APR boundary. + function _aprBoundaryReward(IEtherFiOracle.OracleReport memory r) internal view returns (int256) { + int256 tvl = int128(uint128(lp.getTotalPooledEther())); + uint256 elapsedTime = (uint256(r.refSlotTo) - uint256(admin.lastHandledReportRefSlot())) * SECONDS_PER_SLOT; + if (tvl <= 0 || elapsedTime == 0) return 0; + int256 cap = admin.acceptableRebaseAprInBps(); + int256 D = tvl * int256(elapsedTime); + int256 K = int256(BASIS_POINTS_DENOMINATOR) * int256(365 days); + return ((cap + 1) * D - 1) / K; + } + + /// @dev LiquidityPool positive-rebase absolute cap (in wei) for the current TVL. + function _lpPositiveCap() internal view returns (int256) { + int256 tvl = int128(uint128(lp.getTotalPooledEther())); + return tvl * LP_MAX_POSITIVE_REBASE_BPS / int256(BASIS_POINTS_DENOMINATOR); + } + + /// APPLY: valid report, all gates hold => MUST advance state. + function _scenarioApply(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + // SOUNDNESS: the APR gate caps |reward| relative to the (short) elapsed + // window for this range. Bound the reward to HALF the cap-boundary so the + // apply is guaranteed under the APR cap regardless of the fuzzed magnitude + // and the range length the clock happens to produce. Without this, a large + // reward over a short range trips the APR gate and the "valid" apply + // reverts -> report stays published-but-unapplied -> oracle bricked. + int256 safeMax = _maxSafeReward(r); + if (safeMax <= 1) return; // range too short to carry any reward safely + r.accruedRewards = int128(int256(bound(magnitude, 0, uint256(safeMax / 2)))); + r = _resyncStamps(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + _moveClock(uint256(wait) + 1); + _executeAndCheck(r); + } + + /// QUORUM-FAIL: only ONE member submits => consensus never reached. + /// SOUNDNESS: quorumSize == 2, committee == {memberA, memberB}; a single + /// submission is strictly below quorum. Report never published => un-stuck. + function _scenarioQuorumFail(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + r.accruedRewards = int128(int256(bound(magnitude, 0, 0.5 ether))); + r = _resyncStamps(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + _moveClock(uint256(wait) + 1); + _executeAndCheck(r); + } + + /// APR-FAIL: size accruedRewards so |APR| strictly exceeds the cap => MUST + /// revert on the APR gate. Unpublish afterward to leave the oracle un-stuck. + function _scenarioAprFail(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + // unpublish recovery computes refSlotFrom-1, so needs refSlotFrom > 0. + if (r.refSlotFrom == 0) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + uint32 lastHandled = admin.lastHandledReportRefSlot(); + int256 tvl = int128(uint128(lp.getTotalPooledEther())); + uint256 elapsedTime = (uint256(r.refSlotTo) - uint256(lastHandled)) * SECONDS_PER_SLOT; + if (tvl <= 0 || elapsedTime == 0) return; + int256 cap = admin.acceptableRebaseAprInBps(); + // reward at the cap boundary: cap = 10000 * (reward*365d)/(tvl*elapsedTime) + int256 boundaryReward = + cap * tvl * int256(elapsedTime) / (int256(BASIS_POINTS_DENOMINATOR) * int256(365 days)); + int256 extra = int256(bound(magnitude, 1 ether, 50 ether)); + int256 reward = boundaryReward + extra; + if (magnitude % 2 == 0) reward = -reward; // exercise both positive and negative over-cap + if (reward > type(int128).max || reward < type(int128).min) return; + r.accruedRewards = int128(reward); + + bytes32 reportHash = oracle.generateReportHash(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + _moveClock(uint256(wait) + 1); + // consensus + freshness hold, APR does not => MUST revert on APR gate. + _executeAndCheck(r); + // RECOVERY: published-but-unappliable. Unpublish to un-stick the oracle. + if (oracle.isConsensusReached(reportHash) && r.refSlotTo > admin.lastHandledReportRefSlot()) { + address[] memory members = new address[](2); + members[0] = memberA; + members[1] = memberB; + vm.prank(multisig); + try oracle.unpublishReport(r, members) {} catch {} + } + } + + /// FRESH-FAIL: consensus reached but executeTasks called BEFORE the wait + /// window => MUST revert on freshness; then warp past it and apply, leaving + /// the oracle un-stuck. No-op when wait window is 0 (then freshness is vacuous). + function _scenarioFreshFail(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + if (wait == 0) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + // Same APR-safety bound as _scenarioApply: this report is applied after the + // freshness window elapses, so it must stay under the APR cap. + int256 safeMax = _maxSafeReward(r); + if (safeMax <= 1) return; + r.accruedRewards = int128(int256(bound(magnitude, 0, uint256(safeMax / 2)))); + r = _resyncStamps(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + // do NOT advance the clock yet -> too fresh. + _executeAndCheck(r); + // now elapse the window and apply for real, leaving the system un-stuck. + _moveClock(uint256(wait) + 1); + _executeAndCheck(r); + } + + /// DUPLICATE: one member submits, then submits the SAME report again. + /// SOUNDNESS: after the first submit, committeeMemberStates[member].lastReportRefSlot + /// == refSlotTo == slotForNextReport(), so shouldSubmitReport returns false and + /// the second submit reverts ReportNotNeeded (checked BEFORE consensus can form, + /// since a single member is strictly below quorum). Nothing is published => + /// un-stuck naturally; the sub-quorum report is then rejected by executeTasks. + function _scenarioDuplicateSubmit(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + r.accruedRewards = int128(int256(bound(magnitude, 0, 0.4 ether))); + r = _resyncStamps(r); + bytes32 reportHash = oracle.generateReportHash(r); + + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + // a single submission must NOT reach quorum (quorumSize == 2). + if (oracle.isConsensusReached(reportHash)) { ghost_consensusFromSingle = true; return; } + + // duplicate submit by the same member MUST revert with ReportNotNeeded. + vm.prank(memberA); + try oracle.submitReport(r) returns (bool) { + ghost_duplicateSubmitSucceeded = true; + } catch (bytes memory err) { + numDupRejected++; + bytes4 sel; + if (err.length >= 4) { assembly { sel := mload(add(err, 0x20)) } } + if (sel != EtherFiOracle.ReportNotNeeded.selector) { + ghost_duplicateWrongError = true; + duplicateWrongErrorReason = "duplicate submit reverted with a non-ReportNotNeeded error"; + } + } + // still sub-quorum: executeTasks MUST reject on the quorum gate. + _moveClock(uint256(wait) + 1); + _executeAndCheck(r); + // nothing was published (sub-quorum) => the oracle is un-stuck. + } + + /// CONFLICTING: A submits reward X, B submits reward Y != X for the same range. + /// The two distinct report hashes each carry a single vote, so NEITHER reaches + /// consensus and executeTasks reverts for both. Nothing is published, so the + /// stuck-guard (lastPublished != lastHandled) is never tripped and the sequence + /// resolves on the next fresh range — no explicit resolution step is required. + function _scenarioConflictingReports(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok,) = _freshRange(); + if (!ok) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + // Two INDEPENDENT report structs for the same finalized range (no clock has + // moved since _freshRange, so both read the same stamps). They must be + // distinct memory objects — `memory rB = rA` aliases in Solidity and would + // make both members vote for one hash, reaching consensus. + IEtherFiOracle.OracleReport memory rA = _baseReport(); + IEtherFiOracle.OracleReport memory rB = _baseReport(); + rA.accruedRewards = int128(int256(bound(magnitude, 0, 0.3 ether))); + rB.accruedRewards = rA.accruedRewards + int128(int256(1 ether)); // Y != X + bytes32 hA = oracle.generateReportHash(rA); + bytes32 hB = oracle.generateReportHash(rB); + + vm.prank(memberA); + try oracle.submitReport(rA) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(rB) {} catch { return; } + // two distinct one-vote reports must not reach consensus. + if (oracle.isConsensusReached(hA) || oracle.isConsensusReached(hB)) { + ghost_conflictReachedConsensus = true; + return; + } + _moveClock(uint256(wait) + 1); + // both hashes are sub-quorum: executeTasks MUST reject each on the quorum gate. + _executeAndCheck(rA); + _executeAndCheck(rB); + numConflictExercised++; + } + + /// FRESH-BOUNDARY: exact freshness edge. Drive executeTasks at exactly + /// consensusSlot + wait - 1 (MUST revert "too fresh", since the contract + /// requires current_slot >= wait + consensusSlot) and at exactly + /// consensusSlot + wait (MUST apply). Leaves the oracle un-stuck via the apply. + function _scenarioFreshBoundary(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + if (wait == 0) return; // freshness gate vacuous + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + int256 safeMax = _maxSafeReward(r); + if (safeMax <= 1) return; + r.accruedRewards = int128(int256(bound(magnitude, 0, uint256(safeMax / 2)))); + r = _resyncStamps(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + bytes32 reportHash = oracle.generateReportHash(r); + if (!oracle.isConsensusReached(reportHash)) return; + + uint32 consSlot = oracle.getConsensusSlot(reportHash); + uint32 cur = oracle.computeSlotAtTimestamp(block.timestamp); + // Move to exactly consSlot + wait - 1 (one slot short of the window). + uint256 target = uint256(consSlot) + uint256(wait) - 1; + if (target > cur) _moveClock(target - cur); + // At consSlot + wait - 1: current_slot < wait + consSlot => MUST revert "too fresh". + _executeAndCheck(r); + // Advance the final slot to exactly consSlot + wait: current_slot == wait + consSlot + // => the strict `<` comparison is false => MUST apply. + _moveClock(1); + uint32 beforeSlot = admin.lastHandledReportRefSlot(); + _executeAndCheck(r); + if (admin.lastHandledReportRefSlot() == beforeSlot) { + ghost_freshBoundaryRejected = true; + } else { + numFreshBoundaryApplied++; + } + } + + /// APR-BOUNDARY: exact APR edge. The largest reward whose annualized |APR| still + /// satisfies the cap MUST apply; that reward + 1 wei MUST revert on the APR gate. + function _scenarioAprBoundary(uint256 magnitude) internal { + // ---- ACCEPT leg: reward at the exact APR cap boundary MUST apply. ---- + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + uint16 wait = admin.postReportWaitTimeInSlots(); + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + int256 rmax = _aprBoundaryReward(r); + // Guard the accept against LiquidityPool's separate absolute positive cap: + // if the APR-boundary reward exceeds MAX_POSITIVE_REBASE_BPS of TVL, applying + // it would revert in LiquidityPool.rebase (RebaseExceedsPositiveCap), not I5. + int256 lpCap = _lpPositiveCap(); + if (rmax > 1 && rmax <= lpCap && rmax <= type(int128).max) { + r.accruedRewards = int128(rmax); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + _moveClock(uint256(wait) + 1); + uint32 beforeSlot = admin.lastHandledReportRefSlot(); + _executeAndCheck(r); // apr == cap boundary, all other gates hold => MUST apply + if (admin.lastHandledReportRefSlot() == beforeSlot) { + ghost_aprBoundaryRejected = true; + return; // boundary report stuck; bail before it wedges the sequence + } + numAprBoundaryApplied++; + } + + // ---- REJECT leg: boundary reward + 1 wei MUST revert on the APR gate. ---- + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok2, IEtherFiOracle.OracleReport memory r2) = _freshRange(); + if (!ok2) return; + if (r2.refSlotFrom == 0) return; // unpublish recovery needs refSlotFrom > 0 + int256 rmax2 = _aprBoundaryReward(r2); + if (rmax2 <= 0 || rmax2 + 1 > int256(type(int128).max)) return; + r2.accruedRewards = int128(rmax2 + 1); // one wei over the boundary => apr > cap + bytes32 h2 = oracle.generateReportHash(r2); + vm.prank(memberA); + try oracle.submitReport(r2) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r2) {} catch { return; } + _moveClock(uint256(wait) + 1); + _executeAndCheck(r2); // MUST revert "TVL changed too much" -> numRejApr + // RECOVERY: published-but-unappliable. Unpublish to un-stick the oracle. + if (oracle.isConsensusReached(h2) && r2.refSlotTo > admin.lastHandledReportRefSlot()) { + address[] memory members = new address[](2); + members[0] = memberA; + members[1] = memberB; + vm.prank(multisig); + try oracle.unpublishReport(r2, members) {} catch {} + } + } + + /// NEG-REBASE: a small valid negative drop (under both the APR cap and the + /// negative-rebase cap) MUST apply; a drop one wei above the negative-rebase cap + /// (but still under the APR cap) MUST revert "negative rebase exceeds cap". + function _scenarioNegRebase(uint256 magnitude) internal { + _negRebaseAccept(magnitude); + _negRebaseReject(magnitude); + } + + /// ACCEPT leg: small valid negative drop under BOTH caps MUST apply. + function _negRebaseAccept(uint256 magnitude) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + int256 tvl = int128(uint128(lp.getTotalPooledEther())); + // negative-cap boundary drop: largest drop with drop*10000 <= tvl*negBps. + int256 negBoundary = tvl * int256(admin.effectiveMaxNegativeRebaseBps()) / int256(BASIS_POINTS_DENOMINATOR); + // largest drop whose |APR| still satisfies the cap for this range. + int256 aprDropMax = _aprBoundaryReward(r); + // accept drop must stay under BOTH caps. + int256 dropAcceptMax = negBoundary < aprDropMax ? negBoundary : aprDropMax; + if (dropAcceptMax <= 1) return; + r.accruedRewards = int128(-int256(bound(magnitude, 1, uint256(dropAcceptMax)))); + r = _resyncStamps(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + _moveClock(uint256(admin.postReportWaitTimeInSlots()) + 1); + uint32 beforeSlot = admin.lastHandledReportRefSlot(); + _executeAndCheck(r); // under both caps => MUST apply + if (admin.lastHandledReportRefSlot() == beforeSlot) ghost_negValidRejected = true; + else numNegAccepted++; + } + + /// REJECT leg: drop one wei above the negative-rebase cap (but under the APR + /// cap) MUST revert "negative rebase exceeds cap". Unpublish to leave un-stuck. + function _negRebaseReject(uint256 /*magnitude*/) internal { + if (oracle.lastPublishedReportRefSlot() != admin.lastHandledReportRefSlot()) return; + (bool ok, IEtherFiOracle.OracleReport memory r) = _freshRange(); + if (!ok) return; + if (r.refSlotFrom == 0) return; // unpublish recovery needs refSlotFrom > 0 + int256 tvl = int128(uint128(lp.getTotalPooledEther())); + int256 negBoundary = tvl * int256(admin.effectiveMaxNegativeRebaseBps()) / int256(BASIS_POINTS_DENOMINATOR); + int256 dropReject = negBoundary + 1; // minimal increment above the negative cap + // SOUNDNESS: keep the drop UNDER the APR cap so the contract reverts on the + // NEGATIVE-rebase gate (checked after APR), not the APR gate. With the 3-bps + // negative cap and a range spanning one report period this holds with margin. + if (dropReject > _aprBoundaryReward(r)) return; + if (dropReject > int256(type(int128).max)) return; + r.accruedRewards = int128(-dropReject); + r = _resyncStamps(r); + bytes32 reportHash = oracle.generateReportHash(r); + vm.prank(memberA); + try oracle.submitReport(r) {} catch { return; } + vm.prank(memberB); + try oracle.submitReport(r) {} catch { return; } + _moveClock(uint256(admin.postReportWaitTimeInSlots()) + 1); + _executeAndCheck(r); // MUST revert "negative rebase exceeds cap" -> numRejNegRebase + // RECOVERY: published-but-unappliable. Unpublish to un-stick the oracle. + if (oracle.isConsensusReached(reportHash) && r.refSlotTo > admin.lastHandledReportRefSlot()) { + address[] memory members = new address[](2); + members[0] = memberA; + members[1] = memberB; + vm.prank(multisig); + try oracle.unpublishReport(r, members) {} catch {} + } + } + + /// @dev After any extra clock movement the block stamps must be re-derived + /// so submitReport's verifyReport (which checks against the live + /// blockStampForNextReport) passes. refSlotTo can grow as the clock + /// advances; we re-read just before submitting. + function _resyncStamps(IEtherFiOracle.OracleReport memory r) + internal + view + returns (IEtherFiOracle.OracleReport memory) + { + (uint32 slotFrom, uint32 slotTo, uint32 blockFrom) = oracle.blockStampForNextReport(); + r.refSlotFrom = slotFrom; + r.refSlotTo = slotTo; + r.refBlockFrom = blockFrom; + r.refBlockTo = slotTo; + return r; + } +} diff --git a/test/invariant/handlers/RateLimiterHandler.sol b/test/invariant/handlers/RateLimiterHandler.sol new file mode 100644 index 000000000..c4fa0b470 --- /dev/null +++ b/test/invariant/handlers/RateLimiterHandler.sol @@ -0,0 +1,432 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "forge-std/StdUtils.sol"; +import "forge-std/Vm.sol"; + +import "@etherfi/governance/rate-limiting/EtherFiRateLimiter.sol"; + +/// @notice Stateful-invariant handler (fuzz target) for the GENERAL +/// EtherFiRateLimiter — the global-bucket path (createNewLimiter + +/// updateConsumers + consume) plus the admin parameter surface +/// (setCapacity / setRefillRate / setRemaining) and time warps that +/// drive BucketLimiter refill. This is the GLOBAL rate limiter, NOT +/// the redemption-specific BucketRateLimiter already covered by +/// RedemptionManagerHandler. +/// +/// I4 — rate-limit budget conservation. The handler is the fuzz +/// target; it whitelists ITSELF as a consumer on a fixed set of +/// buckets and drives consume/refill/parameter ops, maintaining ghost +/// flags that the invariant file asserts NEVER trip: +/// +/// (a) remaining/consumable NEVER exceeds capacity (no overfill). +/// (b) consume succeeds IFF canConsume(amount) was true the same block, +/// and a success reduces remaining by EXACTLY `amount` (after the +/// refill that consume applies first). +/// (c) capacity==0 on an existing bucket => consume(amount>=1) always +/// reverts LimitExceeded (freeze semantics). +/// (d) refill is monotonic and bounded: as time passes consumable only +/// increases, capped at capacity. +/// (e) gating: consume reverts UnknownLimit if the bucket does not +/// exist, and InvalidConsumer if the caller is not whitelisted. +/// +/// The bucket admin functions are onlyAdmin == onlyOperatingTimelock; +/// the handler pranks `admin`, which holds OPERATION_TIMELOCK_ROLE in +/// TestSetup. `consume` is whenNotPaused only — the handler whitelists +/// itself, so an un-pranked self-call passes the consumer check. +/// +/// The per-address bucket API (tightenAddressLimit / setAddressLimit / +/// consumeForAddressIfConfigured) is `onlyToken` (eETH/weETH only) and +/// is intentionally NOT driven here — the handler is not the token +/// proxy, so it cannot reach that surface locally. Those paths share +/// the identical BucketLimiter math proven on the global bucket. +contract RateLimiterHandler is StdUtils { + Vm internal constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code"))))); + + EtherFiRateLimiter public immutable rl; + address public immutable admin; // holds OPERATION_TIMELOCK_ROLE + address public immutable stranger; // never whitelisted on any bucket + + uint256 public constant N_BUCKETS = 4; + bytes32[N_BUCKETS] public ids; + + /// @dev An id that is never created — used to prove the UnknownLimit gate. + bytes32 public constant UNKNOWN_ID = keccak256("rate-limiter.unknown.bucket"); + + bytes4 internal constant SEL_LIMIT_EXCEEDED = bytes4(keccak256("LimitExceeded()")); + bytes4 internal constant SEL_UNKNOWN_LIMIT = bytes4(keccak256("UnknownLimit()")); + bytes4 internal constant SEL_INVALID_CONSUMER = bytes4(keccak256("InvalidConsumer()")); + + // ---- Ghost / violation flags (asserted false by the invariant file) ----- + + bool public ghost_overfill; // remaining/consumable > capacity + bool public ghost_iffViolated; // consume success != canConsume(before) + bool public ghost_exactDecreaseViolated; // remaining_after != consumable_before - amount + bool public ghost_freezeViolated; // cap==0 consume(>=1) did not revert LimitExceeded + bool public ghost_refillMonotonicViolated; // consumable decreased as time advanced + bool public ghost_refillModelViolated; // consumable_after != min(cap, before + rate*dt) + bool public ghost_drainConsumeReverted; // consume(consumable()) reverted despite canConsume + bool public ghost_revokeViolated; // revoked consumer succeeded, or re-grant broke consume + bool public ghost_setterPostStateViolated; // a setter's post-state != its documented clamp result + bool public ghost_setterReverted; // a setter with valid inputs + admin role reverted + bool public ghost_gatingViolated; // UnknownLimit / InvalidConsumer gate failed + + // ---- Non-vacuity counters ---------------------------------------------- + + uint256 public consume_ok; // successful real consumes + uint256 public consume_rejected; // consume reverted LimitExceeded (budget exhausted) + bool public refillObserved; // a strictly-positive refill was observed + + mapping(bytes32 => uint256) public callCounts; + + constructor(EtherFiRateLimiter _rl, address _admin) { + rl = _rl; + admin = _admin; + stranger = address(uint160(uint256(keccak256("rate-limiter.stranger")))); + + // Bucket 0 is the stable "refill probe": its capacity/refillRate are + // never mutated, so drain+warp deterministically observes refill. + // Buckets 1..N-1 are the mutable parameter-fuzz surface. + for (uint256 i = 0; i < N_BUCKETS; i++) { + ids[i] = keccak256(abi.encodePacked("rate-limiter.bucket.", i)); + vm.prank(admin); + // capacity 1e9 gwei, refillRate 1e6 gwei/s — both non-zero so + // refill is observable and buckets start full (remaining==cap). + rl.createNewLimiter(ids[i], uint64(1e9), uint64(1e6)); + vm.prank(admin); + rl.updateConsumers(ids[i], address(this), true); + } + } + + // ===================================================================== + // COVERAGE FLOOR: the afterInvariant gates require every deterministic + // probe to have fired at least once per run. Selector scheduling is + // random, so with 10 selectors a probe can starve (~1e-6/run, which + // compounds across 256 runs x 8 invariant campaigns into a real flake + // rate). The first handler action of each run therefore drives each + // gated probe exactly once with fixed seeds; the fuzzer still exercises + // them independently afterwards. + // ===================================================================== + bool private coverageBooted; + + modifier coverageFloor() { + if (!coverageBooted) { + coverageBooted = true; + this.act_consumeFrozen(1, 1); + this.act_consumeUnknown(1); + this.act_consumeUnwhitelisted(1, 1); + this.act_revokeConsumer(1, 1); + this.act_setCapacity(1, 100); + this.act_setRefillRate(1, 100); + this.act_setRemaining(1, 100); + } + _; + } + + // ===================================================================== + // CORE: consume — proves I4(b) IFF + exact-decrease, and I4(a) overfill. + // ===================================================================== + + function act_consume(uint256 bucketSeed, uint64 amount) external coverageFloor { + bytes32 id = ids[bucketSeed % N_BUCKETS]; + uint64 amt = uint64(bound(uint256(amount), 0, uint256(4e9))); // can exceed cap + + // All three views run at the SAME block.timestamp as the consume that + // follows, so the in-memory refill they apply is identical to the one + // consume applies — making the IFF and exact-decrease checks exact. + bool can = rl.canConsume(id, amt); + uint64 consumableBefore = rl.consumable(id); + (uint64 capBefore,,,) = rl.getLimit(id); + + // sanity: consumable never exceeds capacity (refill-bounded) + if (consumableBefore > capBefore) ghost_overfill = true; + + bool success; + // msg.sender == address(this), which is whitelisted on every bucket. + try rl.consume(id, amt) { + success = true; + // Only count strictly-positive consumes toward non-vacuity — a + // consume of 0 succeeds trivially and proves nothing. + if (amt > 0) consume_ok++; + (uint64 capAfter, uint64 remAfter,,) = rl.getLimit(id); + // I4(a): never overfilled. + if (remAfter > capAfter) ghost_overfill = true; + // I4(b) exact decrease: remaining drops by exactly `amount` + // relative to the refilled remaining (== consumableBefore). + if (remAfter != consumableBefore - amt) ghost_exactDecreaseViolated = true; + } catch (bytes memory err) { + success = false; + consume_rejected++; + // The only legitimate failure on an existing, whitelisted, + // unpaused bucket is LimitExceeded. + if (_sel(err) != SEL_LIMIT_EXCEEDED) ghost_gatingViolated = true; + } + + // I4(b) IFF: consume succeeds exactly when canConsume said it could. + if (success != can) ghost_iffViolated = true; + + callCounts["act_consume"]++; + } + + // ===================================================================== + // FREEZE: capacity==0 on an existing bucket => consume(>=1) reverts. I4(c) + // ===================================================================== + + function act_consumeFrozen(uint256 bucketSeed, uint64 amount) external coverageFloor { + // Use a mutable bucket (index >= 1) so the stable probe stays alive. + uint256 idx = 1 + (bucketSeed % (N_BUCKETS - 1)); + bytes32 id = ids[idx]; + + // Freeze it. + vm.prank(admin); + rl.setCapacity(id, 0); + + uint64 amt = uint64(bound(uint256(amount), 1, uint256(type(uint64).max))); // >= 1 + + try rl.consume(id, amt) { + // A non-zero consume on a zero-capacity bucket MUST revert. + ghost_freezeViolated = true; + } catch (bytes memory err) { + if (_sel(err) != SEL_LIMIT_EXCEEDED) ghost_freezeViolated = true; + } + + // Restore a usable capacity so subsequent ops on this bucket stay live. + vm.prank(admin); + rl.setCapacity(id, uint64(1e9)); + callCounts["act_consumeFrozen"]++; + } + + // ===================================================================== + // REFILL: monotonic + bounded across time. I4(d) (+ non-vacuity). + // ===================================================================== + + /// @notice Drains the stable probe bucket (0), warps, and asserts + /// consumable strictly increases (refill happened), stays capped at + /// capacity, AND matches the exact BucketLimiter refill formula. + /// Deterministically exercises real refill. + function act_drainAndRefill(uint256 secondsSeed) external coverageFloor { + bytes32 id = ids[0]; + uint64 c = rl.consumable(id); + if (c > 0) { + // `consumable(id)` == remaining after the refill for this block, and + // consume(id, c) applies that SAME refill (same block.timestamp, no + // drift within one tx), so canConsume(id, c) is true by construction + // and consume MUST succeed. A revert here is a real violation. + bool can = rl.canConsume(id, c); + try rl.consume(id, c) { if (c > 0) consume_ok++; } + catch { if (can) ghost_drainConsumeReverted = true; } + } + (uint64 cap,, uint64 rate,) = rl.getLimit(id); + uint64 before = rl.consumable(id); + + uint256 dt = bound(secondsSeed, 1, 600); + vm.warp(block.timestamp + dt); + + uint64 afterC = rl.consumable(id); + // I4(d): monotonic — never decreases as time advances. + if (afterC < before) ghost_refillMonotonicViolated = true; + // I4(a)/(d): bounded by capacity. + if (afterC > cap) ghost_overfill = true; + // I4(d) exact: consumable == min(capacity, before + refillRate*dt), in + // full uint256 precision — mirrors BucketLimiter._refill exactly. The + // `min` also covers capacity==type(uint64).max (no special case needed). + uint256 predicted = uint256(before) + uint256(rate) * dt; + if (predicted > cap) predicted = cap; + if (uint256(afterC) != predicted) ghost_refillModelViolated = true; + // Non-vacuity: a real, strictly-positive refill occurred. + if (rate > 0 && afterC > before) refillObserved = true; + + callCounts["act_drainAndRefill"]++; + } + + /// @notice Advances time and checks monotonicity/boundedness/exact-refill + /// across ALL buckets at their current (fuzzed) parameters. Each + /// bucket's parameters are constant across the single warp, so the + /// exact refill formula applies per bucket. + function act_advanceTime(uint256 secondsSeed) external coverageFloor { + uint64[N_BUCKETS] memory before; + for (uint256 i = 0; i < N_BUCKETS; i++) before[i] = rl.consumable(ids[i]); + + // Occasionally warp far (up to ~1e12s, still << uint64 max so the uint64 + // block.timestamp cast in _refill never wraps) so a near-max refillRate + // drives newRemaining into the type(uint64).max clamp / cast boundary. + uint256 dt = (secondsSeed % 16 == 0) + ? bound(secondsSeed, 1, uint256(1e12)) + : bound(secondsSeed, 1, 3600); + vm.warp(block.timestamp + dt); + + for (uint256 i = 0; i < N_BUCKETS; i++) { + (uint64 cap,, uint64 rate,) = rl.getLimit(ids[i]); + uint64 afterC = rl.consumable(ids[i]); + if (afterC < before[i]) ghost_refillMonotonicViolated = true; + if (afterC > cap) ghost_overfill = true; + // Exact refill: consumable == min(capacity, before + refillRate*dt). + uint256 predicted = uint256(before[i]) + uint256(rate) * dt; + if (predicted > cap) predicted = cap; + if (uint256(afterC) != predicted) ghost_refillModelViolated = true; + if (rate > 0 && afterC > before[i]) refillObserved = true; + } + callCounts["act_advanceTime"]++; + } + + // ===================================================================== + // GATING: UnknownLimit + InvalidConsumer. I4(e) + // ===================================================================== + + function act_consumeUnknown(uint64 amount) external coverageFloor { + uint64 amt = uint64(bound(uint256(amount), 0, uint256(type(uint64).max))); + try rl.consume(UNKNOWN_ID, amt) { + ghost_gatingViolated = true; // a non-existent bucket must revert + } catch (bytes memory err) { + if (_sel(err) != SEL_UNKNOWN_LIMIT) ghost_gatingViolated = true; + } + callCounts["act_consumeUnknown"]++; + } + + function act_consumeUnwhitelisted(uint256 bucketSeed, uint64 amount) external coverageFloor { + bytes32 id = ids[bucketSeed % N_BUCKETS]; + uint64 amt = uint64(bound(uint256(amount), 0, uint256(type(uint64).max))); + // `stranger` is never added as a consumer on any bucket. + vm.prank(stranger); + try rl.consume(id, amt) { + ghost_gatingViolated = true; // non-whitelisted caller must revert + } catch (bytes memory err) { + if (_sel(err) != SEL_INVALID_CONSUMER) ghost_gatingViolated = true; + } + callCounts["act_consumeUnwhitelisted"]++; + } + + // ===================================================================== + // CONSUMER REVOCATION: updateConsumers(false) revokes, (true) restores. I4(e) + // ===================================================================== + + /// @notice Revokes the handler's own consumer status on a mutable bucket, + /// asserts its consume then reverts InvalidConsumer, re-grants, and + /// asserts the consumer path is live again. Leaves the bucket + /// re-granted so it stays usable for later actions. + function act_revokeConsumer(uint256 bucketSeed, uint64 amount) external coverageFloor { + // Use a mutable bucket (index >= 1); bucket 0 stays a whitelisted probe. + uint256 idx = 1 + (bucketSeed % (N_BUCKETS - 1)); + bytes32 id = ids[idx]; + uint64 amt = uint64(bound(uint256(amount), 0, uint256(type(uint64).max))); + + vm.prank(admin); + rl.updateConsumers(id, address(this), false); + + // While revoked, the consumer check fires before any bucket math, so our + // own consume must revert InvalidConsumer regardless of amount/capacity. + try rl.consume(id, amt) { + ghost_revokeViolated = true; + } catch (bytes memory err) { + if (_sel(err) != SEL_INVALID_CONSUMER) ghost_revokeViolated = true; + } + + vm.prank(admin); + rl.updateConsumers(id, address(this), true); + + // Re-granted: a zero-amount consume never hits LimitExceeded, so it must + // succeed — any revert proves the re-grant failed to restore the path. + try rl.consume(id, 0) { } catch { ghost_revokeViolated = true; } + + callCounts["act_revokeConsumer"]++; + } + + // ===================================================================== + // ADMIN parameter surface — evolves state the bucket math depends on. + // Targets mutable buckets (index >= 1); bucket 0 stays a stable probe. + // ===================================================================== + + function act_setCapacity(uint256 bucketSeed, uint64 capSeed) external coverageFloor { + uint256 idx = 1 + (bucketSeed % (N_BUCKETS - 1)); + bytes32 id = ids[idx]; + // Occasionally set capacity near type(uint64).max — the documented + // soft-disable region (consumeToken) — to exercise the clamp/cast edge. + uint64 cap = (capSeed % 16 == 0) + ? uint64(bound(uint256(capSeed), uint256(type(uint64).max) - 4, uint256(type(uint64).max))) + : uint64(bound(uint256(capSeed), 0, uint256(2e9))); + + // `consumable(id)` == the refilled remaining at this block; setCapacity + // refills first, then sets capacity, then clamps remaining down to it. + (,, uint64 rateB,) = rl.getLimit(id); + uint64 refilled = rl.consumable(id); + + vm.prank(admin); + try rl.setCapacity(id, cap) { + callCounts["act_setCapacity"]++; + (uint64 capA, uint64 remA, uint64 rateA,) = rl.getLimit(id); + // Post-state: capacity := cap; remaining := min(refilled, cap); + // refillRate unchanged. + uint64 expRem = refilled < cap ? refilled : cap; + if (capA != cap || remA != expRem || rateA != rateB) ghost_setterPostStateViolated = true; + } catch { + // Bucket exists + admin holds the timelock role => must not revert. + ghost_setterReverted = true; + } + _checkBucketBounded(id); + } + + function act_setRefillRate(uint256 bucketSeed, uint64 rateSeed) external coverageFloor { + uint256 idx = 1 + (bucketSeed % (N_BUCKETS - 1)); + bytes32 id = ids[idx]; + // Occasionally set refillRate near type(uint64).max so a subsequent warp + // drives newRemaining into the clamp region. + uint64 rate = (rateSeed % 16 == 0) + ? uint64(bound(uint256(rateSeed), uint256(type(uint64).max) - 4, uint256(type(uint64).max))) + : uint64(bound(uint256(rateSeed), 0, uint256(1e7))); + + (uint64 capB,,,) = rl.getLimit(id); + uint64 refilled = rl.consumable(id); + + vm.prank(admin); + try rl.setRefillRate(id, rate) { + callCounts["act_setRefillRate"]++; + (uint64 capA, uint64 remA, uint64 rateA,) = rl.getLimit(id); + // Post-state: refillRate := rate; remaining := refilled; capacity unchanged. + if (capA != capB || remA != refilled || rateA != rate) ghost_setterPostStateViolated = true; + } catch { + ghost_setterReverted = true; + } + _checkBucketBounded(id); + } + + function act_setRemaining(uint256 bucketSeed, uint64 remSeed) external coverageFloor { + uint256 idx = 1 + (bucketSeed % (N_BUCKETS - 1)); + bytes32 id = ids[idx]; + uint64 rem = uint64(bound(uint256(remSeed), 0, uint256(4e9))); // can exceed cap + + (uint64 capB,, uint64 rateB,) = rl.getLimit(id); + + vm.prank(admin); + try rl.setRemaining(id, rem) { + callCounts["act_setRemaining"]++; + (uint64 capA, uint64 remA, uint64 rateA,) = rl.getLimit(id); + // Post-state: remaining := min(rem, capacity); capacity & refillRate + // unchanged. (setRemaining refills first but then overwrites + // remaining with the clamp of the input, so `refilled` is discarded.) + uint64 expRem = rem > capB ? capB : rem; + if (capA != capB || remA != expRem || rateA != rateB) ghost_setterPostStateViolated = true; + } catch { + ghost_setterReverted = true; + } + _checkBucketBounded(id); + } + + // ===================================================================== + // INTERNALS + // ===================================================================== + + function _checkBucketBounded(bytes32 id) internal { + (uint64 cap, uint64 rem,,) = rl.getLimit(id); + if (rem > cap) ghost_overfill = true; + if (rl.consumable(id) > cap) ghost_overfill = true; + } + + function _sel(bytes memory err) internal pure returns (bytes4 sel) { + if (err.length >= 4) { + assembly { sel := mload(add(err, 32)) } + } + } + + // Iterate all buckets for the invariant file's overfill cross-check. + function bucketId(uint256 i) external view returns (bytes32) { return ids[i]; } +} diff --git a/test/invariant/handlers/RewardsDistributorHandler.sol b/test/invariant/handlers/RewardsDistributorHandler.sol new file mode 100644 index 000000000..76201f667 --- /dev/null +++ b/test/invariant/handlers/RewardsDistributorHandler.sol @@ -0,0 +1,494 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "forge-std/StdUtils.sol"; +import "forge-std/Vm.sol"; + +import "@etherfi/rewards/CumulativeMerkleRewardsDistributor.sol"; + +/// @notice Stateful-invariant handler (fuzz target) for +/// CumulativeMerkleRewardsDistributor. It drives the full lifecycle +/// (set pending root -> finalize after delay -> claim) and maintains +/// independent ghost state used to prove two invariants: +/// +/// I12 - cumulative-claim monotonicity & no double-pay. +/// `cumulativeClaimed[token][account]` must be non-decreasing, +/// and the ETH actually delivered to an account over a run must +/// equal `final cumulativeClaimed - initial`. Claimant accounts +/// are dedicated fresh EOAs that NEVER spend, so their on-chain +/// `balance` is an independent oracle for "ETH actually paid". +/// +/// I13 - reward-root finalization delay. A pending merkle root cannot +/// become the claimable root until at least `claimDelay` has +/// elapsed since `setPendingMerkleRoot`. The handler reads the +/// on-chain delay predicate before each finalize attempt and +/// flips a ghost if a finalize ever SUCCEEDS while the delay was +/// not yet satisfied. +/// +/// Privileged calls (setPendingMerkleRoot / finalizeMerkleRoot are +/// onlyExecutorOperations; setClaimDelay / updateWhitelistedRecipient +/// are onlyAdmin == onlyOperatingTimelock) are pranked as `admin`, +/// which holds BOTH EXECUTOR_OPERATIONS_ROLE and OPERATION_TIMELOCK_ROLE +/// in TestSetup. `claim` is permissionless. +contract RewardsDistributorHandler is StdUtils { + Vm internal constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code"))))); + + CumulativeMerkleRewardsDistributor public immutable dist; + address public immutable admin; + address public immutable token; // ETH_ADDRESS + + bytes4 internal constant SEL_INSUFFICIENT_DELAY = bytes4(keccak256("InsufficentDelay()")); + + // Dedicated claimant accounts (fresh EOAs that only ever RECEIVE ETH). + // Four are needed so the S2 scenario can build a REAL 4-leaf Merkle tree + // (each claimant is one leaf) and have multiple users claim with genuine + // 2-element proofs. + address[] public claimants; + uint256 public constant N_CLAIMANTS = 4; + + // ---- Ghost state -------------------------------------------------------- + + // I12 ghosts + mapping(address => uint256) public lastSeenCumulative; // per claimant + mapping(address => uint256) public ghostPaid; // per claimant, summed (cum - preclaimed) + bool public ghost_monotonicViolated; + bool public ghost_doublePayViolated; + + // I13 ghosts + uint256 public ghost_pendingSetAt; // block.timestamp at last setPendingMerkleRoot + bytes32 public ghost_pendingRoot; // root last set pending + bool public ghost_hasPending; + // Independent mirror of the contract's claimDelay. Seeded from the contract + // once in the constructor (initial config, not the runtime predicate) and + // updated on every successful setClaimDelay, so doFinalize can recompute the + // delay predicate WITHOUT reading the contract's own storage (which would + // mirror a bug instead of catching it — see doFinalize). + uint256 public ghost_claimDelay; + bool public ghost_finalizeDelayViolated; // finalize succeeded while delay not met + bool public ghost_finalizeRootMismatch; // claimable root != recorded pending root after finalize + bool public ghost_boundaryRejectedAtDelay; // finalize reverted InsufficentDelay AT setAt + delay (too strict) + + // S2 (merkle-proof) ghosts + bool public ghost_validProofRejected; // a claim with a genuine, in-tree proof reverted + bool public ghost_badProofAccepted; // a claim with a proof for the wrong leaf/amount succeeded + + mapping(bytes32 => uint256) public callCounts; + + constructor(CumulativeMerkleRewardsDistributor _dist, address _admin) { + dist = _dist; + admin = _admin; + token = _dist.ETH_ADDRESS(); + // Seed the independent delay oracle from the contract's initial config. + ghost_claimDelay = _dist.claimDelay(); + + for (uint256 i = 0; i < N_CLAIMANTS; i++) { + address c = address(uint160(uint256(keccak256(abi.encodePacked("rd.claimant", i))))); + claimants.push(c); + // Whitelist via admin (onlyAdmin). + vm.prank(admin); + dist.updateWhitelistedRecipient(c, true); + } + } + + // ===================================================================== + // Helpers + // ===================================================================== + + function _claimant(uint256 seed) internal view returns (address) { + return claimants[seed % claimants.length]; + } + + /// @dev Establish a finalized claimable root deterministically: set it + /// pending, warp past the (current) claimDelay, then finalize. Used by + /// the claim path so claims succeed without building real trees. + function _establishRoot(bytes32 root) internal { + vm.prank(admin); + dist.setPendingMerkleRoot(token, root); + ghost_pendingSetAt = block.timestamp; + ghost_pendingRoot = root; + ghost_hasPending = true; + + uint256 delay = dist.claimDelay(); + vm.warp(block.timestamp + delay + 1); + + vm.prank(admin); + dist.finalizeMerkleRoot(token, block.number); + callCounts["finalize_ok"]++; + // Post-finalize: claimable root must equal what we set pending. + if (dist.claimableMerkleRoots(token) != root) ghost_finalizeRootMismatch = true; + ghost_hasPending = false; + } + + // ===================================================================== + // Fuzz actions + // ===================================================================== + + /// @notice Set a fresh pending merkle root (I13 setup). + function doSetPendingRoot(uint256 rootSeed) external { + bytes32 root = keccak256(abi.encodePacked("rd.root", rootSeed, block.timestamp)); + vm.prank(admin); + try dist.setPendingMerkleRoot(token, root) { + ghost_pendingSetAt = block.timestamp; + ghost_pendingRoot = root; + ghost_hasPending = true; + callCounts["setPending"]++; + } catch { + callCounts["setPending_revert"]++; + } + } + + /// @notice Attempt to finalize the pending root at the current time. This + /// is the core I13 probe: a finalize that SUCCEEDS while the + /// on-chain delay predicate is unmet is a violation. + function doFinalize(uint256 /*blockSeed*/) external { + // Independent recomputation of the contract's delay predicate from the + // handler's OWN ghost state — the timestamp we recorded when WE set the + // root pending (ghost_pendingSetAt) and our mirror of the delay + // (ghost_claimDelay), NOT the contract's lastPendingMerkleUpdatedToTimestamp + // / claimDelay storage. Reading the contract's storage back would mirror a + // bug that corrupted those fields instead of catching it. The assertion is + // gated on ghost_hasPending: only a FRESH pending root has a delay window to + // validate; re-finalizing when nothing new is pending makes no new root + // claimable and has no transition to check. + bool hadPending = ghost_hasPending; + bool delayMet = block.timestamp >= ghost_pendingSetAt + ghost_claimDelay; + bytes32 expectedRoot = ghost_pendingRoot; + + vm.prank(admin); + try dist.finalizeMerkleRoot(token, block.number) { + if (hadPending) { + // Finalize of a fresh pending root succeeded. The delay MUST have + // been satisfied, and the new claimable root MUST equal the root we + // recorded as pending. + if (!delayMet) ghost_finalizeDelayViolated = true; + if (dist.claimableMerkleRoots(token) != expectedRoot) ghost_finalizeRootMismatch = true; + } + ghost_hasPending = false; + callCounts["finalize_ok"]++; + } catch (bytes memory err) { + bytes4 sel; + if (err.length >= 4) { + sel = bytes4(err); + } + if (sel == SEL_INSUFFICIENT_DELAY) { + callCounts["finalize_delay_revert"]++; + } else { + callCounts["finalize_other_revert"]++; + } + } + } + + /// @notice Full deterministic claim: establish a single-leaf root for the + /// chosen claimant at a strictly higher cumulative amount, then + /// claim. Proves I12 monotonicity + exact payout. Self-contained: a + /// SINGLE call drives the entire lifecycle (setPending -> finalize + /// after delay -> claim -> replay-rejected), so the suite is + /// non-vacuous even on a 1-call sequence (Foundry shrinks a failing + /// run to its minimal subsequence and re-evaluates afterInvariant on + /// that replay; a self-contained action keeps the non-vacuity gates + /// satisfiable there). + function doClaim(uint256 acctSeed, uint128 amt) external { + address account = _claimant(acctSeed); + uint256 preCum = dist.cumulativeClaimed(token, account); + uint256 delta = bound(uint256(amt), 1, 50 ether); + uint256 newCum = preCum + delta; + + // Single-leaf tree: root == leaf, proof is empty. + bytes32 leaf = keccak256(abi.encodePacked(account, newCum)); + _establishRoot(leaf); + + uint256 preBal = account.balance; + bytes32[] memory proof = new bytes32[](0); + + try dist.claim(token, account, newCum, leaf, proof) { + uint256 postCum = dist.cumulativeClaimed(token, account); + uint256 postBal = account.balance; + + // I12: monotonic non-decrease. + if (postCum < preCum) ghost_monotonicViolated = true; + // I12: cumulative advanced to exactly the claimed amount. + if (postCum != newCum) ghost_doublePayViolated = true; + // I12: ETH actually delivered == (postCum - preCum), no double pay. + if (postBal - preBal != postCum - preCum) ghost_doublePayViolated = true; + + ghostPaid[account] += (postCum - preCum); + lastSeenCumulative[account] = postCum; + callCounts["claim_ok"]++; + + // Inline replay against the SAME (already-claimed) cumulative: must + // revert (NothingToClaim). Doing it here makes a single doClaim call + // exercise finalize + claim + replay-rejection together, so the + // non-vacuity gates hold even under sequence shrinking. + uint256 preBalReplay = account.balance; + try dist.claim(token, account, newCum, leaf, proof) { + // A successful replay at an equal cumulative is a double-pay. + ghost_doublePayViolated = true; + if (account.balance != preBalReplay) ghost_doublePayViolated = true; + callCounts["replay_unexpected_ok"]++; + } catch { + callCounts["replay_revert"]++; + } + } catch { + callCounts["claim_revert"]++; + } + } + + /// @notice (I12, monotonic-decrease guard) Attempt to claim a STRICTLY + /// LOWER cumulative than already recorded. The contract rejects this + /// at CumulativeMerkleRewardsDistributor.sol:113 + /// (`if (preclaimed >= cumulativeAmount) revert NothingToClaim()`). + /// If such a claim ever SUCCEEDS or moves ETH, the monotonic + /// guarantee is broken -> trip ghost_monotonicViolated. Self-contained + /// (establishes its own root) so it survives sequence-shrinking. + function doLowerCumulativeClaim(uint256 acctSeed, uint256 dropSeed) external { + address account = _claimant(acctSeed); + + // Self-contained: first ensure this account has a NON-ZERO cumulative by + // performing a real claim (establish root -> claim). This makes a SINGLE + // doLowerCumulativeClaim call drive the whole guard exercise, so the + // non-vacuity gate survives Foundry sequence-shrinking (a shrunk 1-call + // replay would otherwise skip on cum==0 and leave lower_rejected at 0). + uint256 cum = dist.cumulativeClaimed(token, account); + if (cum == 0) { + uint256 seed = bound(dropSeed, 1, 50 ether); + bytes32 bootLeaf = keccak256(abi.encodePacked(account, seed)); + _establishRoot(bootLeaf); + bytes32[] memory bootProof = new bytes32[](0); + try dist.claim(token, account, seed, bootLeaf, bootProof) { + ghostPaid[account] += seed; + lastSeenCumulative[account] = seed; + cum = seed; + callCounts["claim_ok"]++; + } catch { + callCounts["lower_boot_failed"]++; + return; + } + } + + // Strictly-lower target in [0, cum-1]. + uint256 lower = bound(dropSeed, 0, cum - 1); + bytes32 leaf = keccak256(abi.encodePacked(account, lower)); + _establishRoot(leaf); + + uint256 preBal = account.balance; + bytes32[] memory proof = new bytes32[](0); + try dist.claim(token, account, lower, leaf, proof) { + // MUST be unreachable: preclaimed (cum) >= lower by construction. + ghost_monotonicViolated = true; + if (account.balance != preBal) ghost_doublePayViolated = true; + callCounts["lower_unexpected_ok"]++; + } catch { + callCounts["lower_rejected"]++; + } + } + + /// @notice Attempt to replay the exact same cumulative amount: must revert + /// (NothingToClaim). If it ever succeeds, that is a double-pay. + function doReplayClaim(uint256 acctSeed) external { + address account = _claimant(acctSeed); + uint256 cum = dist.cumulativeClaimed(token, account); + if (cum == 0) { + callCounts["replay_skipped"]++; + return; + } + // Build & finalize a root for the already-claimed cumulative value. + bytes32 leaf = keccak256(abi.encodePacked(account, cum)); + _establishRoot(leaf); + + uint256 preBal = account.balance; + bytes32[] memory proof = new bytes32[](0); + try dist.claim(token, account, cum, leaf, proof) { + // A successful replay at an equal cumulative is a double-pay. + ghost_doublePayViolated = true; + if (account.balance != preBal) ghost_doublePayViolated = true; + callCounts["replay_unexpected_ok"]++; + } catch { + callCounts["replay_revert"]++; + } + } + + /// @notice (S1, I13 delay boundary) Deterministic two-sided probe of the + /// finalization-delay boundary. Sets a fresh pending root, then: + /// - warps to EXACTLY setAt + delay - 1 and asserts finalize + /// reverts InsufficentDelay (one second too early), + /// - warps +1s to setAt + delay and asserts finalize SUCCEEDS. + /// Positively drives both edges of the `block.timestamp >= setAt + + /// claimDelay` predicate rather than relying on the fuzzer to land on + /// the exact second. Self-contained (its own setPending -> finalize), + /// so it survives Foundry sequence-shrinking. Uses ghost_claimDelay + /// (the independent delay mirror), which equals the live claimDelay + /// here since we do not change the delay between setPending and + /// finalize. + function doDelayBoundaryProbe(uint256 rootSeed) external { + uint256 delay = ghost_claimDelay; + bytes32 root = keccak256(abi.encodePacked("rd.boundary", rootSeed, block.timestamp)); + + vm.prank(admin); + dist.setPendingMerkleRoot(token, root); + uint256 setAt = block.timestamp; + ghost_pendingSetAt = setAt; + ghost_pendingRoot = root; + ghost_hasPending = true; + + // Negative edge: one second before the boundary, finalize MUST revert + // InsufficentDelay. (When delay == 0 there is no "before"; skip it.) + if (delay > 0) { + vm.warp(setAt + delay - 1); + vm.prank(admin); + try dist.finalizeMerkleRoot(token, block.number) { + // Finalized strictly before the delay elapsed -> I13 violation. + ghost_finalizeDelayViolated = true; + ghost_hasPending = false; + callCounts["boundary_early_ok"]++; + } catch (bytes memory err) { + bytes4 sel = err.length >= 4 ? bytes4(err) : bytes4(0); + if (sel == SEL_INSUFFICIENT_DELAY) { + callCounts["boundary_early_rejected"]++; + } else { + callCounts["boundary_early_other_revert"]++; + } + } + } + + // Positive edge: exactly at the boundary, finalize MUST succeed. + vm.warp(setAt + delay); + vm.prank(admin); + try dist.finalizeMerkleRoot(token, block.number) { + if (dist.claimableMerkleRoots(token) != root) ghost_finalizeRootMismatch = true; + ghost_hasPending = false; + callCounts["boundary_at_ok"]++; + callCounts["finalize_ok"]++; // also counts toward the I13 non-vacuity gate + } catch (bytes memory err) { + bytes4 sel = err.length >= 4 ? bytes4(err) : bytes4(0); + if (sel == SEL_INSUFFICIENT_DELAY) { + // Rejected AT the boundary though the delay had elapsed -> the + // delay guard is too strict (an I13 liveness break). + ghost_boundaryRejectedAtDelay = true; + callCounts["boundary_at_rejected"]++; + } else { + callCounts["boundary_at_other_revert"]++; + } + } + } + + /// @notice (S2, merkle proofs) Build a REAL 4-leaf Merkle tree over the four + /// claimants — each at a strictly-higher cumulative than recorded — + /// finalize its root, then have every claimant claim with a genuine + /// 2-element proof. This is the ONLY scenario that exercises + /// `_verifyAsm`'s hashing loop (the single-leaf scenarios pass an + /// empty proof, so the loop never iterates). Leaf and internal-node + /// hashing replicate the contract EXACTLY: leaf = + /// keccak256(abi.encodePacked(account, cumulativeAmount)) (claim + /// L142) and internal nodes are the sorted-pair keccak that + /// `_verifyAsm` computes (L204-214), i.e. OZ's commutative + /// MerkleProof hashing. Also feeds a proof for the WRONG amount and + /// asserts it is rejected (InvalidProof). Self-contained, so it + /// survives sequence-shrinking. + function doMerkleTreeClaim(uint256 seed) external { + // Four distinct leaves, one per claimant, each at pre + delta. + address[4] memory accts; + uint256[4] memory cum; + bytes32[4] memory leaf; + for (uint256 i = 0; i < 4; i++) { + address a = claimants[i]; + uint256 pre = dist.cumulativeClaimed(token, a); + uint256 delta = bound( + uint256(keccak256(abi.encodePacked("rd.tree.delta", seed, i))), + 1, + 20 ether + ); + accts[i] = a; + cum[i] = pre + delta; + leaf[i] = keccak256(abi.encodePacked(a, cum[i])); + } + + // Level 1 then root, using the contract's sorted-pair hashing. + bytes32 n01 = _hashPair(leaf[0], leaf[1]); + bytes32 n23 = _hashPair(leaf[2], leaf[3]); + bytes32 root = _hashPair(n01, n23); + + // Genuine 2-element proofs (sibling leaf, then the opposite subtree node). + bytes32[][4] memory proofs; + proofs[0] = new bytes32[](2); proofs[0][0] = leaf[1]; proofs[0][1] = n23; + proofs[1] = new bytes32[](2); proofs[1][0] = leaf[0]; proofs[1][1] = n23; + proofs[2] = new bytes32[](2); proofs[2][0] = leaf[3]; proofs[2][1] = n01; + proofs[3] = new bytes32[](2); proofs[3][0] = leaf[2]; proofs[3][1] = n01; + + _establishRoot(root); + + // Negative case FIRST (state still clean): claimant[0]'s real proof but a + // TAMPERED amount. The recomputed leaf != leaf[0], so `_verifyAsm` yields + // the wrong root -> InvalidProof. The proof check (claim L143) precedes + // the NothingToClaim check (L147), so cum[0]+1 > preclaimed is irrelevant. + { + uint256 preBal = accts[0].balance; + try dist.claim(token, accts[0], cum[0] + 1, root, proofs[0]) { + ghost_badProofAccepted = true; + if (accts[0].balance != preBal) ghost_doublePayViolated = true; + callCounts["tree_proof_unexpected_ok"]++; + } catch { + callCounts["tree_proof_rejected"]++; + } + } + + // Positive case: every claimant claims with its genuine proof. Each must + // succeed, advance cumulative to exactly cum[i], and pay exactly the delta. + for (uint256 i = 0; i < 4; i++) { + uint256 preCum = dist.cumulativeClaimed(token, accts[i]); + uint256 preBal = accts[i].balance; + try dist.claim(token, accts[i], cum[i], root, proofs[i]) { + uint256 postCum = dist.cumulativeClaimed(token, accts[i]); + uint256 postBal = accts[i].balance; + if (postCum < preCum) ghost_monotonicViolated = true; + if (postCum != cum[i]) ghost_doublePayViolated = true; + if (postBal - preBal != postCum - preCum) ghost_doublePayViolated = true; + + ghostPaid[accts[i]] += (postCum - preCum); + lastSeenCumulative[accts[i]] = postCum; + callCounts["tree_claim_ok"]++; + callCounts["claim_ok"]++; // also counts toward the I12 non-vacuity gate + } catch { + // A genuine, in-tree proof at a strictly-higher cumulative MUST + // settle. A revert here means valid-proof verification failed. + ghost_validProofRejected = true; + callCounts["tree_claim_revert"]++; + } + } + } + + /// @dev Sorted-pair keccak, matching `_verifyAsm`'s node combination + /// (keccak of the smaller value concatenated with the larger). + function _hashPair(bytes32 a, bytes32 b) internal pure returns (bytes32) { + return a < b + ? keccak256(abi.encodePacked(a, b)) + : keccak256(abi.encodePacked(b, a)); + } + + function doSetClaimDelay(uint256 d) external { + uint256 nd = bound(d, 0, 7 days); + vm.prank(admin); + try dist.setClaimDelay(nd) { + ghost_claimDelay = nd; // keep the independent delay oracle in sync + callCounts["setClaimDelay"]++; + } catch { + callCounts["setClaimDelay_revert"]++; + } + } + + function doWarp(uint256 seconds_) external { + uint256 s = bound(seconds_, 1, 5 days); + vm.warp(block.timestamp + s); + callCounts["warp"]++; + } + + function doRoll(uint256 blocks_) external { + uint256 b = bound(blocks_, 1, 1000); + vm.roll(block.number + b); + callCounts["roll"]++; + } + + // Convenience views for the invariant file. + function numClaimants() external view returns (uint256) { + return claimants.length; + } +} diff --git a/test/invariant/handlers/ValidatorLifecycleHandler.sol b/test/invariant/handlers/ValidatorLifecycleHandler.sol new file mode 100644 index 000000000..e62545334 --- /dev/null +++ b/test/invariant/handlers/ValidatorLifecycleHandler.sol @@ -0,0 +1,154 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../../TestSetup.sol"; +import "@etherfi/staking/EtherFiNodesManager.sol"; + +/// @notice Stateful-fuzz handler driving EtherFiNodesManager.linkPubkeyToNode +/// directly, to prove invariant I11 (pubkey -> node uniqueness). +/// +/// linkPubkeyToNode is gated `msg.sender == address(stakingManager)`, +/// so the handler pranks as the StakingManager instance. The function +/// dual-writes two maps and guards both: +/// - etherFiNodeFromPubkeyHash[pubkeyHash] must be 0 (else AlreadyLinked) +/// - legacyState.DEPRECATED_etherfiNodeAddress[legacyId] must be 0 (else AlreadyLinked) +/// pubkeyHash = sha256(pubkey ++ bytes16(0)), pubkey is exactly 48 bytes. +/// +/// INVARIANT I11: once a pubkey hash is linked to a node, the mapping +/// is permanent and unique — it can never be overwritten or repointed, +/// and any re-link attempt (to the SAME or a DIFFERENT node) reverts. +contract ValidatorLifecycleHandler is Test { + EtherFiNodesManager internal immutable manager; + address internal immutable stakingManagerAddr; + address internal immutable executorOps; // linkLegacyValidatorIds caller (EXECUTOR_OPERATIONS_ROLE) + + // ---- ghost state ---- + // first node each pubkey hash was linked to (0 = never linked) + mapping(bytes32 => address) public ghostLinkedNode; + // legacyIds already consumed (a legacyId can only be used once) + mapping(uint256 => bool) public ghostLegacyUsed; + bytes32[] public linkedHashes; + // legacyIds that a successful link populated in DEPRECATED_etherfiNodeAddress + // (needed to drive linkLegacyValidatorIds past its UnknownNode guard) + uint256[] public usedLegacyIds; + + // failure flags — any true => invariant broken + bool public sawOverwrite; // a stored hash->node changed after first set + bool public sawRelinkSucceed; // re-linking an already-linked hash succeeded + + // coverage counters + uint256 public link_ok; + uint256 public link_already_revert; + uint256 public relink_attempt; + uint256 public legacy_link_attempt; + + constructor(EtherFiNodesManager _manager, address _stakingManagerAddr, address _executorOps) { + manager = _manager; + stakingManagerAddr = _stakingManagerAddr; + executorOps = _executorOps; + } + + function _pubkey(uint256 seed) internal pure returns (bytes memory pk) { + // deterministic 48-byte pubkey from a seed + pk = new bytes(48); + bytes32 a = keccak256(abi.encodePacked(seed, uint256(1))); + bytes32 b = keccak256(abi.encodePacked(seed, uint256(2))); + for (uint256 i = 0; i < 32; i++) pk[i] = a[i]; + for (uint256 i = 0; i < 16; i++) pk[32 + i] = b[i]; + } + + /// Try to link a fresh (or colliding) pubkey to a node. + function doLink(uint256 pubkeySeed, uint256 nodeSeed, uint256 legacyId) external { + pubkeySeed = bound(pubkeySeed, 0, 24); // small space => forces hash collisions / relinks + legacyId = bound(legacyId, 1, 24); + address node = address(uint160(uint256(keccak256(abi.encodePacked("node", nodeSeed))) | 1)); + + bytes memory pk = _pubkey(pubkeySeed); + bytes32 h = manager.calculateValidatorPubkeyHash(pk); + address pre = address(manager.etherFiNodeFromPubkeyHash(h)); + + vm.prank(stakingManagerAddr); + try manager.linkPubkeyToNode(pk, node, legacyId) { + link_ok++; + // success path: it MUST have been unlinked beforehand (both guards) + if (pre != address(0)) sawRelinkSucceed = true; + if (ghostLinkedNode[h] != address(0)) sawRelinkSucceed = true; + if (ghostLegacyUsed[legacyId]) sawRelinkSucceed = true; + ghostLinkedNode[h] = node; + ghostLegacyUsed[legacyId] = true; + usedLegacyIds.push(legacyId); + linkedHashes.push(h); + } catch { + link_already_revert++; + } + + // overwrite check: stored node for an already-ghosted hash must match ghost + if (ghostLinkedNode[h] != address(0)) { + if (address(manager.etherFiNodeFromPubkeyHash(h)) != ghostLinkedNode[h]) sawOverwrite = true; + } + } + + /// Actively attempt to re-link an already-linked pubkey to a DIFFERENT node — must always revert. + function doRelinkAttack(uint256 idx, uint256 nodeSeed, uint256 legacyId) external { + if (linkedHashes.length == 0) return; + relink_attempt++; + idx = bound(idx, 0, linkedHashes.length - 1); + bytes32 h = linkedHashes[idx]; + // recover a pubkey that hashes to h: we stored by seed, so re-derive by scanning small space + for (uint256 s = 0; s <= 24; s++) { + bytes memory pk = _pubkey(s); + if (manager.calculateValidatorPubkeyHash(pk) == h) { + address attackerNode = address(uint160(uint256(keccak256(abi.encodePacked("atk", nodeSeed))) | 1)); + address before = address(manager.etherFiNodeFromPubkeyHash(h)); + // Use a guaranteed-FRESH legacyId (1000..1024, disjoint from the + // 1..24 range doLink consumes) so the DEPRECATED_etherfiNodeAddress + // slot guard is satisfied and the revert isolates the pubkeyHash + // AlreadyLinked guard — the thing we're actually asserting here. + vm.prank(stakingManagerAddr); + try manager.linkPubkeyToNode(pk, attackerNode, bound(legacyId, 1000, 1024)) { + sawRelinkSucceed = true; // re-link of a linked hash MUST NOT succeed + } catch { + // expected + } + if (address(manager.etherFiNodeFromPubkeyHash(h)) != before) sawOverwrite = true; + return; + } + } + } + + /// Actively attempt to repoint an already-linked pubkey via the SECOND writer + /// to etherFiNodeFromPubkeyHash — linkLegacyValidatorIds (EXECUTOR_OPERATIONS_ROLE). + /// We feed it a legacyId that a prior link already populated in + /// DEPRECATED_etherfiNodeAddress (so the UnknownNode guard passes) paired with an + /// already-linked pubkey. The call MUST revert AlreadyLinked and leave the link + /// untouched — exercising that this path can't overwrite I11's mapping either. + function doLegacyLinkAttack(uint256 idx, uint256 legacyIdx) external { + if (linkedHashes.length == 0 || usedLegacyIds.length == 0) return; + legacy_link_attempt++; + idx = bound(idx, 0, linkedHashes.length - 1); + bytes32 h = linkedHashes[idx]; + uint256 legacyId = usedLegacyIds[bound(legacyIdx, 0, usedLegacyIds.length - 1)]; + + // recover a pubkey that hashes to h (stored by seed over the small space) + for (uint256 s = 0; s <= 24; s++) { + bytes memory pk = _pubkey(s); + if (manager.calculateValidatorPubkeyHash(pk) == h) { + uint256[] memory ids = new uint256[](1); + ids[0] = legacyId; + bytes[] memory pks = new bytes[](1); + pks[0] = pk; + address before = address(manager.etherFiNodeFromPubkeyHash(h)); + vm.prank(executorOps); + try manager.linkLegacyValidatorIds(ids, pks) { + sawRelinkSucceed = true; // legacy path re-linked an already-linked pubkey + } catch { + // expected: AlreadyLinked + } + if (address(manager.etherFiNodeFromPubkeyHash(h)) != before) sawOverwrite = true; + return; + } + } + } + + function linkedCount() external view returns (uint256) { return linkedHashes.length; } +} diff --git a/test/invariant/handlers/ValidatorStateMachineHandler.sol b/test/invariant/handlers/ValidatorStateMachineHandler.sol new file mode 100644 index 000000000..b6ea96af4 --- /dev/null +++ b/test/invariant/handlers/ValidatorStateMachineHandler.sol @@ -0,0 +1,218 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "../../TestSetup.sol"; +import "@etherfi/staking/interfaces/IStakingManager.sol"; +import "@etherfi/staking/interfaces/IEtherFiNode.sol"; +import "@etherfi/core/LiquidityPool.sol"; +import "@etherfi/staking/StakingManager.sol"; +import "@etherfi/staking/EtherFiNodesManager.sol"; + +interface ILPValidator { + function batchRegister(IStakingManager.DepositData[] calldata, uint256[] calldata, address) external; + // NOT payable: the pool funds the 1 ETH per validator from its own balance + // (LiquidityPool.batchCreateBeaconValidators -> createBeaconValidators{value: ...}). + function batchCreateBeaconValidators(IStakingManager.DepositData[] calldata, uint256[] calldata, address) external; +} + +/// @notice Stateful-fuzz handler for the validator-creation state machine (I10). +/// +/// Drives the three real transition functions against a fixed pool of +/// pre-provisioned (REGISTERED-able) validators, in fuzzer-chosen order: +/// - register : NOT_REGISTERED -> REGISTERED (LP.batchRegister, spawner) +/// - create : REGISTERED -> CONFIRMED (LP.batchCreateBeaconValidators, op-admin) +/// - invalidate : REGISTERED -> INVALIDATED (StakingManager.invalidateRegisteredBeaconValidator, oracle-ops) +/// +/// INVARIANT I10: validatorCreationStatus only ever advances along a +/// LEGAL edge. CONFIRMED and INVALIDATED are terminal; no skip, no +/// reverse, no illegal edge. The handler records each hash's status +/// before/after every attempted call and flips a failure ghost if any +/// observed transition is not in the legal set. +contract ValidatorStateMachineHandler is Test { + enum S { NOT_REGISTERED, REGISTERED, CONFIRMED, INVALIDATED } + + StakingManager internal immutable sm; + address internal immutable lp; + address internal immutable opAdmin; // batchCreateBeaconValidators caller + address internal immutable oracleOps; // invalidate caller + + struct Val { + IStakingManager.DepositData depositData; + uint256 bidId; + address node; + address spawner; + bytes32 hash; + } + Val[] internal pool; + + // failure ghost — any true => I10 broken + bool public sawIllegalTransition; + string public illegalReason; + // records the actual (before, after) status codes of the illegal edge observed + uint8 public illegalBefore; + uint8 public illegalAfter; + + // failure ghost — a successful call landed in the WRONG end-state + // (register that didn't reach REGISTERED, create that didn't reach CONFIRMED, + // invalidate that didn't reach INVALIDATED). Any true => I10 broken. + bool public sawWrongEndState; + string public wrongEndStateReason; + + // coverage + uint256 public register_ok; + uint256 public register_revert; + uint256 public create_ok; + uint256 public create_revert; + uint256 public invalidate_ok; + uint256 public invalidate_revert; + + constructor( + StakingManager _sm, + address _lp, + address /* _spawner (unused; per-validator spawner) */, + address _opAdmin, + address _oracleOps + ) { + sm = _sm; + lp = _lp; + opAdmin = _opAdmin; + oracleOps = _oracleOps; + } + + function addValidator( + IStakingManager.DepositData calldata d, + uint256 bidId, + address node, + address spawner, + bytes32 hash + ) external { + pool.push(Val({depositData: d, bidId: bidId, node: node, spawner: spawner, hash: hash})); + } + + function poolSize() external view returns (uint256) { return pool.length; } + + function _status(bytes32 h) internal view returns (S) { + return S(uint8(sm.validatorCreationStatus(h))); + } + + function _check(S before, S afterS) internal { + if (before == afterS) return; // no-op (revert path) is always fine + bool legal = + (before == S.NOT_REGISTERED && afterS == S.REGISTERED) || + (before == S.REGISTERED && afterS == S.CONFIRMED) || + (before == S.REGISTERED && afterS == S.INVALIDATED); + if (!legal) { + sawIllegalTransition = true; + illegalBefore = uint8(before); + illegalAfter = uint8(afterS); + illegalReason = string.concat( + "illegal status edge ", + vm.toString(uint256(uint8(before))), + "->", + vm.toString(uint256(uint8(afterS))) + ); + } + } + + /// After a call that reported success, the hash MUST sit in the expected + /// end-state. Records a ghost violation (total-function style) rather than + /// reverting inside the handler. + function _expectEndState(S expected, S actual) internal { + if (actual != expected) { + sawWrongEndState = true; + wrongEndStateReason = string.concat( + "success landed in ", + vm.toString(uint256(uint8(actual))), + " expected ", + vm.toString(uint256(uint8(expected))) + ); + } + } + + function _arrD(IStakingManager.DepositData memory d) internal pure returns (IStakingManager.DepositData[] memory a) { + a = new IStakingManager.DepositData[](1); + a[0] = d; + } + function _arrU(uint256 x) internal pure returns (uint256[] memory a) { + a = new uint256[](1); + a[0] = x; + } + + // ---- single-step transition primitives (shared by the fuzzed actions and + // the coverage bootstrap) ---- + + function _register(Val storage v) internal { + S before = _status(v.hash); + vm.prank(v.spawner); + try ILPValidator(lp).batchRegister(_arrD(v.depositData), _arrU(v.bidId), v.node) { + register_ok++; + _expectEndState(S.REGISTERED, _status(v.hash)); + } catch { + register_revert++; + } + _check(before, _status(v.hash)); + } + + function _create(Val storage v) internal { + S before = _status(v.hash); + // batchCreateBeaconValidators is NOT payable: the LiquidityPool funds the + // 1 ETH-per-validator initial deposit from its OWN balance (setUp deals it + // the ETH). Forwarding value here would revert on the non-payable fallback + // before any state transition, so no create could ever fire. + vm.prank(opAdmin); + try ILPValidator(lp).batchCreateBeaconValidators(_arrD(v.depositData), _arrU(v.bidId), v.node) { + create_ok++; + _expectEndState(S.CONFIRMED, _status(v.hash)); + } catch { + create_revert++; + } + _check(before, _status(v.hash)); + } + + function _invalidate(Val storage v) internal { + S before = _status(v.hash); + vm.prank(oracleOps); + try sm.invalidateRegisteredBeaconValidator(v.depositData, v.bidId, v.node) { + invalidate_ok++; + _expectEndState(S.INVALIDATED, _status(v.hash)); + } catch { + invalidate_revert++; + } + _check(before, _status(v.hash)); + } + + /// Coverage floor: create/invalidate both consume a REGISTERED validator and + /// compete for the few that exist, so a purely random action order starves one + /// or the other on some runs (a single doCreate on a random idx usually misses + /// the registered validator). To make coverage deterministic without weakening + /// the vacuity gate, the first fuzzed call of every run drives one full legal + /// register->create on pool[0] and one full register->invalidate on pool[1]. + /// The two now-terminal validators then double as illegal-edge targets that the + /// fuzzer keeps hammering (create/invalidate/register on a terminal status must + /// all revert with no status change). Runs revert to the setUp snapshot, so this + /// re-arms each run. + bool internal bootstrapped; + modifier coverageFloor() { + if (!bootstrapped) { + bootstrapped = true; + if (pool.length >= 1) { _register(pool[0]); _create(pool[0]); } + if (pool.length >= 2) { _register(pool[1]); _invalidate(pool[1]); } + } + _; + } + + function doRegister(uint256 idx) external coverageFloor { + if (pool.length == 0) return; + _register(pool[bound(idx, 0, pool.length - 1)]); + } + + function doCreate(uint256 idx) external coverageFloor { + if (pool.length == 0) return; + _create(pool[bound(idx, 0, pool.length - 1)]); + } + + function doInvalidate(uint256 idx) external coverageFloor { + if (pool.length == 0) return; + _invalidate(pool[bound(idx, 0, pool.length - 1)]); + } +} diff --git a/test/invariant/handlers/WithdrawalSolvencyHandler.sol b/test/invariant/handlers/WithdrawalSolvencyHandler.sol new file mode 100644 index 000000000..99a0fcdcb --- /dev/null +++ b/test/invariant/handlers/WithdrawalSolvencyHandler.sol @@ -0,0 +1,674 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "forge-std/StdUtils.sol"; +import "forge-std/Vm.sol"; + +import "@etherfi/core/LiquidityPool.sol"; +import "@etherfi/core/EETH.sol"; +import "@etherfi/withdrawals/WithdrawRequestNFT.sol"; +import "@etherfi/withdrawals/interfaces/IWithdrawRequestNFT.sol"; + +import "@openzeppelin/contracts/utils/math/Math.sol"; + +/// @notice Stateful-invariant handler for invariant I3 — Withdrawal Queue +/// Accounting / Solvency — exercised against the WithdrawRequestNFT +/// escrow path on a mainnet fork. +/// +/// I3 (informal): the total outstanding withdrawal claim never exceeds +/// the protocol's redeemable ETH. The formal statement involves live +/// EigenLayer-queued withdrawals across all pods, which cannot be +/// deterministically controlled on a latest-block mainnet fork (see +/// the invariant file's header for the full reclassification rationale). +/// This handler drives the SC-checkable core that the contracts +/// actually enforce: +/// +/// (P1) finalize-never-exceeds-liquidity. The protocol's finalize+lock +/// flow (`LiquidityPool.addEthAmountLockedForWithdrawal` -> +/// `_lockEth`) reverts when `totalValueInLp < lockAmount` +/// (mirrored by `EtherFiAdmin._validateWithdrawals`' +/// `finalizedWithdrawalAmount <= totalValueInLp` gate). We mirror +/// production exactly (lock the summed eETH amount of the +/// newly-finalized range, then `finalizeRequests`) and assert that +/// every SUCCESSFUL lock had `lockAmount <= totalValueInLp` at +/// lock time. A success with `lockAmount > inLpBefore` would be a +/// protocol bug. +/// +/// (P2) locked-within-accounted-state. Each finalize moves `lockAmount` +/// from `totalValueInLp` to `totalValueOutOfLp` 1:1 AND adds the +/// same amount to `WithdrawRequestNFT.ethAmountLockedForWithdrawal`. +/// Each claim decrements the lock by `request.amountOfEEth` and +/// `totalValueOutOfLp` by `amountToWithdraw <= amountOfEEth`. +/// Hence `ethAmountLockedForWithdrawal <= totalValueOutOfLp` +/// is preserved (the gap only widens), and trivially +/// `lock <= getTotalPooledEther`. Asserted in the invariant file. +/// +/// (P3) finalized-always-claimable. A finalized, valid, owned request +/// whose frozen rate sits inside [min,max] can always be claimed: +/// ETH was segregated to the NFT at finalize (escrow >= amount), +/// the frozen-rate share burn is bounded by the request's own +/// shares, and `totalValueOutOfLp` dwarfs any single payout. The +/// handler attempts the claim and trips `ghost_finalizedClaimFailed` +/// if a request meeting all preconditions ever reverts. +contract WithdrawalSolvencyHandler is StdUtils { + Vm internal constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code"))))); + + uint256 public constant N_EOAS = 5; + + // Revert selectors from LiquidityPool, used to classify lock reverts so the + // P1 probe can distinguish the liquidity guard (the I3 enforcement) from + // the migration guard that precedes it. + bytes4 internal constant SEL_INSUFFICIENT_LIQUIDITY = bytes4(keccak256("InsufficientLiquidity()")); + bytes4 internal constant SEL_MIGRATION_NOT_COMPLETE = bytes4(keccak256("MigrationNotComplete()")); + + // Selectors used by the S3 invalidate/validate probe to classify reverts. + bytes4 internal constant SEL_REQUEST_NOT_VALID = bytes4(keccak256("RequestNotValid()")); + bytes4 internal constant SEL_REQUEST_NOT_FINALIZED = bytes4(keccak256("RequestNotFinalized()")); + bytes4 internal constant SEL_CANNOT_INVALIDATE_FINALIZED = bytes4(keccak256("CannotInvalidateFinalizedRequest()")); + + LiquidityPool public immutable lp; + EETH public immutable eETH; + WithdrawRequestNFT public immutable wrn; + address public immutable etherFiAdminAddr; + /// @dev holder of GUARDIAN_ROLE (invalidateRequest) — granted in the test setUp. + address public immutable guardian; + /// @dev holder of OPERATION_TIMELOCK_ROLE (validateRequest). + address public immutable operatingTimelock; + + address[N_EOAS] public actors; + + /// @dev tokenIds minted through this handler (so we never touch the + /// pre-existing mainnet requests, whose legacy frozen-rate sentinel + /// was never pushed on this fork and would route through the + /// live-rate fallback). + uint256[] public ourTokenIds; + /// @dev mirror of each tokenId's requested eETH amount, so finalize can + /// size the ETH lock without re-reading the struct mapping. + mapping(uint256 => uint96) public tokenAmount; + /// @dev tokenIds already claimed (burned) — skip on re-selection. + mapping(uint256 => bool) public claimed; + + // ----- I3 ghosts ------------------------------------------------------ + + /// @notice (P1) Set true if a finalize+lock SUCCEEDED while the locked + /// amount exceeded `totalValueInLp` at lock time. Must stay false. + bool public ghost_finalizeExceededLiquidity; + /// @notice (P1) Set true if `_lockEth`'s liquidity guard REJECTED a lock + /// whose amount was actually backed (lockAmount <= inLp) — the + /// contract wrongly rejecting a solvent lock. Must stay false. + /// NOTE: `_lockEth` can emit InsufficientLiquidity from TWO sites — + /// the entry guard (totalValueInLp < _amount) and the post-send + /// `_checkTotalValueInLp`. This ghost conservatively flags EITHER + /// when the range was backed; the post-send variant only fires if + /// the LP is genuinely under-collateralized, which is itself a real + /// solvency violation, so catching it here is correct (the name is + /// narrower than the full set of conditions it guards). + bool public ghost_lockRejectedWhileBacked; + /// @notice (P3) Set true if a request meeting every claimability + /// precondition (finalized, valid, owned, frozen rate in band, + /// escrow sufficient) reverted on `claimWithdraw`. Must stay false. + bool public ghost_finalizedClaimFailed; + + /// @notice (M3) Set true if a successful claimWithdraw did not move the three + /// balances by their exact contract-correct deltas: recipient += + /// amountToWithdraw, lock -= request.amountOfEEth, totalValueOutOfLp + /// -= (amountToWithdraw + strandedSweep). Must stay false. + bool public ghost_claimDeltaViolated; + + /// @notice (S3) Set true if the invalidate/validate round-trip on a + /// non-finalized request produced an unexpected outcome (invalidate + /// did not block the claim, or validate did not restore validity). + bool public ghost_invalidateProbeFailed; + /// @notice (S3) Set true if invalidateRequest on a FINALIZED request was NOT + /// rejected with CannotInvalidateFinalizedRequest. Must stay false. + bool public ghost_finalizedInvalidateAllowed; + + /// @notice forensic crumbs for the first observed failure of either kind. + uint256 public ghost_failTokenId; + bytes4 public ghost_failSelector; + uint256 public ghost_failLockAmount; + uint256 public ghost_failInLp; + /// @notice (M3) forensic crumbs for the first claim-delta mismatch. + uint256 public ghost_deltaFailTokenId; + uint256 public ghost_deltaFailExpected; + uint256 public ghost_deltaFailActual; + + // ----- non-vacuity counters ------------------------------------------ + + uint256 public ghost_requestsCreated; + uint256 public ghost_requestsFinalized; + uint256 public ghost_requestsClaimed; + /// @notice number of finalize ops whose P1 bound (lockAmount <= inLp) was + /// positively verified through a successful lock — proves P1 was + /// actually exercised, not vacuously true. + uint256 public ghost_finalizeBoundChecks; + /// @notice number of times `_lockEth`'s liquidity guard POSITIVELY rejected + /// a genuinely over-backed lock (lockAmount > inLp) — proves the I3 + /// enforcement path is actually driven, not merely regression-guarded. + uint256 public ghost_lockBoundEnforced; + /// @notice (M3) number of successful claims whose exact three-way deltas + /// were verified — proves the delta assertion is actually driven. + uint256 public ghost_claimDeltaChecks; + /// @notice (S3) number of completed invalidate/validate round-trips. + uint256 public ghost_invalidateValidateProbes; + /// @notice (S3) number of times invalidateRequest on a finalized request was + /// correctly rejected with CannotInvalidateFinalizedRequest. + uint256 public ghost_finalizedInvalidateRejected; + + // ----- coverage / forensics ------------------------------------------ + + mapping(bytes32 => uint256) public callCounts; + + constructor( + LiquidityPool _lp, + EETH _eETH, + WithdrawRequestNFT _wrn, + address _etherFiAdmin, + address[N_EOAS] memory _actors, + address _guardian, + address _operatingTimelock + ) { + lp = _lp; + eETH = _eETH; + wrn = _wrn; + etherFiAdminAddr = _etherFiAdmin; + guardian = _guardian; + operatingTimelock = _operatingTimelock; + for (uint256 i = 0; i < N_EOAS; i++) { + actors[i] = _actors[i]; + } + } + + // ===================================================================== + // FUZZ OPS + // ===================================================================== + + /// @notice Deposit-backed withdrawal request through the LP, which routes + /// to WithdrawRequestNFT.requestWithdraw. Records the new tokenId. + function requestWithdraw(uint256 actorSeed, uint128 amountSeed) external { + address actor = _eoa(actorSeed); + uint256 actorEEth = eETH.balanceOf(actor); + // LP gates: amount in [minWithdrawAmount, maxWithdrawAmount]. + uint256 lo = lp.minWithdrawAmount(); + uint256 hiCap = lp.maxWithdrawAmount(); + if (actorEEth < lo) { callCounts["req_skipped_funds"]++; return; } + uint256 hi = actorEEth < hiCap ? actorEEth : hiCap; + if (hi > 30 ether) hi = 30 ether; // keep individual requests modest + if (hi < lo) { callCounts["req_skipped_funds"]++; return; } + uint256 amt = bound(uint256(amountSeed), lo, hi); + + vm.prank(actor); + try lp.requestWithdraw(actor, amt) returns (uint256 tokenId) { + ourTokenIds.push(tokenId); + tokenAmount[tokenId] = uint96(amt); + ghost_requestsCreated++; + callCounts["req"]++; + } catch { + callCounts["req_revert"]++; + } + } + + /// @notice Mirror production finalize ATOMICALLY: `finalizeRequests` then + /// `addEthAmountLockedForWithdrawal` for the summed eETH of the + /// newly-finalized range, in a SINGLE frame (exactly as + /// `EtherFiAdmin._finalizeWithdrawals` does). Running them as one + /// atomic unit (via the `this._finalizeThenLock` self-call) is what + /// prevents an orphaned lock: if either leg reverts the other rolls + /// back, so a lock is never committed while `lastFinalizedRequestId` + /// stays put (which would let a later step re-lock the SAME id range + /// and double-move ETH out of the LP). Only finalizes ranges that + /// include at least one of OUR tokenIds, capped to a modest batch so + /// the checkpoint trace and per-op gas stay bounded on the fork. + function finalizeRequests(uint256 countSeed) external { + uint32 nextId = wrn.nextRequestId(); + uint32 lastFin = wrn.lastFinalizedRequestId(); + if (nextId <= lastFin + 1) { callCounts["finalize_skipped_none"]++; return; } + + // Advance by a bounded batch within the pending range. Cap at 80 so a + // single finalize can clear the ~69 pre-existing mainnet pending + // requests (letting subsequent finalizes reach OUR tokenIds within the + // run depth) while keeping the view-loop and lock gas bounded. + uint32 maxAdvance = nextId - 1 - lastFin; + uint32 advance = uint32(bound(countSeed, 1, maxAdvance > 80 ? 80 : maxAdvance)); + uint32 target = lastFin + advance; + + // Sum the requested eETH for the newly-finalized (lastFin, target] range. + // This INCLUDES any pre-existing mainnet requests caught in the range, + // exactly as production would lock them. + uint256 lockAmount; + for (uint32 id = lastFin + 1; id <= target; id++) { + IWithdrawRequestNFT.WithdrawRequest memory r = wrn.getRequest(id); + lockAmount += uint256(r.amountOfEEth); + } + + uint256 inLpBefore = uint256(lp.totalValueInLp()); + + if (lockAmount > type(uint128).max) { callCounts["finalize_skipped_overflow"]++; return; } + + // ATOMIC finalize+lock (production order: finalize THEN lock, exactly as + // EtherFiAdmin._finalizeWithdrawals — EtherFiAdmin.sol:427-428). Both legs + // run inside the single `this._finalizeThenLock` frame, so the run gets + // all-or-nothing semantics: if EITHER leg reverts, the self-call reverts + // and BOTH state changes roll back. This is the fix for the orphaned-lock + // bug — previously the lock was committed in its own tx and a subsequent + // finalize revert left `ethAmountLockedForWithdrawal` bumped while + // `lastFinalizedRequestId` stayed put, so a later fuzz step could lock the + // SAME id range again and move extra ETH out of the LP. Production never + // exposes that window because the two calls share one transaction. + // + // P1 enforcement is still observed here (success => bound must have held; + // an InsufficientLiquidity revert => bound was genuinely violated), and is + // additionally driven adversarially & deterministically by the dedicated + // `probeOverLiquidityLock` op, which positively feeds the guard an + // over-bound lock every run so the non-vacuity gate never relies on the + // fuzzer stumbling onto one here. + try this._finalizeThenLock(uint256(target), lockAmount) { + // Whole unit committed: finalize landed AND (if non-zero) lock landed. + ghost_requestsFinalized++; + callCounts["finalize"]++; + if (lockAmount > 0) { + // SUCCESS path: a committed lock MUST have been backed. + if (lockAmount > inLpBefore) { + ghost_finalizeExceededLiquidity = true; + ghost_failLockAmount = lockAmount; + ghost_failInLp = inLpBefore; + } + ghost_finalizeBoundChecks++; + } + } catch (bytes memory err) { + // Atomic rollback: NEITHER finalize nor lock took effect, so there is + // no orphaned lock to undo and `lastFinalizedRequestId` is unchanged. + bytes4 sel = err.length >= 4 ? bytes4(err) : bytes4(0); + if (sel == SEL_INSUFFICIENT_LIQUIDITY) { + // The lock leg's liquidity guard fired. It MUST have been because + // the bound was genuinely violated; a liquidity revert while the + // range was fully backed would itself be a bug. + if (lockAmount <= inLpBefore) { + ghost_lockRejectedWhileBacked = true; + ghost_failLockAmount = lockAmount; + ghost_failInLp = inLpBefore; + } else { + ghost_lockBoundEnforced++; // positive: guard rejected an unbacked lock + } + callCounts["lock_revert_liquidity"]++; + } else if (sel == SEL_MIGRATION_NOT_COMPLETE) { + callCounts["lock_revert_migration"]++; + } else { + // finalize-leg revert (e.g. CannotFinalizeFutureRequests) or any + // other classification — the whole unit rolled back regardless. + callCounts["finalize_revert"]++; + } + } + } + + /// @notice Atomic production-order finalize+lock, executed in a SINGLE call + /// frame so the caller can wrap it in try/catch for all-or-nothing + /// semantics (the orphaned-lock fix). Mirrors + /// `EtherFiAdmin._finalizeWithdrawals`: `finalizeRequests` first, + /// then `addEthAmountLockedForWithdrawal` for the range's summed + /// eETH. If the lock leg reverts, the finalize leg reverts with it — + /// no committed lock can outlive a failed finalize. + /// @dev `external` purely so it can be invoked via `this.` to get a fresh + /// frame that reverts atomically. Self-call-gated so the fuzzer + /// cannot drive it out of band (it is not in the targetSelector set + /// either, but the guard is defensive). + function _finalizeThenLock(uint256 target, uint256 lockAmount) external { + require(msg.sender == address(this), "self-only"); + vm.prank(etherFiAdminAddr); + wrn.finalizeRequests(target); + if (lockAmount > 0) { + vm.prank(etherFiAdminAddr); + lp.addEthAmountLockedForWithdrawal(uint128(lockAmount)); + } + } + + /// @notice (P1, adversarial) Deliberately attempt to lock MORE than the LP + /// currently holds in-LP, and assert the contract REJECTS it. This + /// positively drives the I3/P1 enforcement (`_lockEth` reverts when + /// totalValueInLp < _amount) rather than relying on the fuzzer to + /// stumble onto an over-bound range. Self-contained: a single call + /// exercises the guard, so the non-vacuity gate + /// (ghost_lockBoundEnforced > 0) survives Foundry sequence-shrinking. + /// + /// If the lock SUCCEEDS despite asking for more than in-LP liquidity, + /// that is the exact solvency violation P1 forbids -> trip the ghost. + function probeOverLiquidityLock(uint256 overSeed) external { + uint256 inLp = uint256(lp.totalValueInLp()); + // Ask for strictly more than in-LP liquidity (bounded so the uint128 + // cast is safe). +1 wei over is enough to violate the guard; add a fuzzed + // margin for variety. + uint256 over = bound(overSeed, 1, 1_000 ether); + uint256 attempt = inLp + over; + if (attempt > type(uint128).max) { callCounts["probe_skipped_overflow"]++; return; } + + vm.prank(etherFiAdminAddr); + try lp.addEthAmountLockedForWithdrawal(uint128(attempt)) { + // Should be impossible: attempt > inLp by construction. + ghost_finalizeExceededLiquidity = true; + ghost_failLockAmount = attempt; + ghost_failInLp = inLp; + callCounts["probe_unexpected_ok"]++; + } catch (bytes memory err) { + bytes4 sel = err.length >= 4 ? bytes4(err) : bytes4(0); + if (sel == SEL_INSUFFICIENT_LIQUIDITY) { + ghost_lockBoundEnforced++; // positive observation of the guard + callCounts["probe_rejected_liquidity"]++; + } else if (sel == SEL_MIGRATION_NOT_COMPLETE) { + callCounts["probe_rejected_migration"]++; + } else { + callCounts["probe_rejected_other"]++; + } + } + } + + /// @notice (P3) Claim one of OUR finalized requests. Verifies every + /// claimability precondition first; if all hold and the claim + /// reverts, trips ghost_finalizedClaimFailed. + function claimWithdraw(uint256 idxSeed) external { + uint256 n = ourTokenIds.length; + if (n == 0) { callCounts["claim_skipped_empty"]++; return; } + uint256 idx = bound(idxSeed, 0, n - 1); + uint256 tokenId = ourTokenIds[idx]; + + if (claimed[tokenId]) { callCounts["claim_skipped_claimed"]++; return; } + if (tokenId > wrn.lastFinalizedRequestId()) { callCounts["claim_skipped_unfinalized"]++; return; } + + address ownerAddr; + try wrn.ownerOf(tokenId) returns (address o) { ownerAddr = o; } + catch { callCounts["claim_skipped_burned"]++; return; } + if (ownerAddr == address(0)) { callCounts["claim_skipped_burned"]++; return; } + + IWithdrawRequestNFT.WithdrawRequest memory req = wrn.getRequest(tokenId); + if (!req.isValid) { callCounts["claim_skipped_invalid"]++; return; } + + // For OUR tokenIds (finalized post-upgrade) the trace always returns a + // non-zero snapshot; legacy tokenIds fall back to the live rate exactly + // as _getClaimableAmount does (no rate-band guard exists anymore). + uint224 frozenRate = wrn.frozenRateFor(tokenId); + if (frozenRate == 0) { + frozenRate = uint224(lp.amountPerShareCeil()); + } + + // Independent recompute of the payout the contract will pay. + uint256 amountForShares = Math.mulDiv(uint256(req.shareOfEEth), uint256(frozenRate), 1e18); + uint256 amountToWithdraw = amountForShares < uint256(req.amountOfEEth) + ? amountForShares : uint256(req.amountOfEEth); + + // Escrow must cover the payout (it always does: lock added the full + // amountOfEEth >= amountToWithdraw at finalize). + if (wrn.ethAmountLockedForWithdrawal() < amountToWithdraw) { + // Would revert InsufficientEscrow — but by construction this cannot + // happen for a properly finalized request. Record as a claim + // failure so a real escrow shortfall surfaces. + ghost_finalizedClaimFailed = true; + ghost_failTokenId = tokenId; + callCounts["claim_escrow_short"]++; + return; + } + // lp.withdraw payout decrements totalValueOutOfLp -= amountToWithdraw; + // on a fork outOfLp is ~1.8M ETH so this never underflows, but guard + // defensively so an unrelated underflow isn't misread as a P3 failure. + if (uint256(lp.totalValueOutOfLp()) < amountToWithdraw) { callCounts["claim_skipped_outlp"]++; return; } + + // ---- (M3) snapshot the three balances the claim moves ---- + // Deltas confirmed from WithdrawRequestNFT._claimWithdraw (L327-360) and + // LiquidityPool.withdraw (L297-305) + receive (L185-190): + // recipient += amountToWithdraw (L345 payout) + // ethAmountLocked... -= request.amountOfEEth (L341, the FULL escrowed + // amount, not the payout) + // totalValueOutOfLp -= amountToWithdraw (LP.withdraw L303) + // -= strandedSweep (WRN L351-354 sweeps + // balance-above-lock back to LP; LP.receive then + // moves it outOfLp->inLp, L187-188) + // where strandedSweep = (wrnBal - amountToWithdraw) - (lock - amountOfEEth), + // which is provably >= 0 (escrow invariant wrnBal >= lock and + // amountToWithdraw <= amountOfEEth), so the sweep fires whenever it is > 0. + // Pack the pre-claim snapshot (in its own array to keep the claimWithdraw + // stack frame shallow — the delta recompute lives in _checkClaimDeltas). + // [0]=recipient bal, [1]=lock, [2]=totalValueOutOfLp, [3]=WRN bal. + uint256[4] memory pre = [ + ownerAddr.balance, + uint256(wrn.ethAmountLockedForWithdrawal()), + uint256(lp.totalValueOutOfLp()), + address(wrn).balance + ]; + + vm.prank(ownerAddr); + try wrn.claimWithdraw(tokenId) { + claimed[tokenId] = true; + ghost_requestsClaimed++; + callCounts["claim"]++; + _checkClaimDeltas(tokenId, ownerAddr, amountToWithdraw, uint256(req.amountOfEEth), pre); + } catch (bytes memory err) { + // A finalized, valid, owned, in-escrow request that reverts is a + // genuine I3 (P3) violation. + ghost_finalizedClaimFailed = true; + ghost_failTokenId = tokenId; + if (err.length >= 4) { + bytes4 sel; + assembly { sel := mload(add(err, 32)) } + ghost_failSelector = sel; + } + callCounts["claim_revert"]++; + } + } + + /// @notice (M3) Verify a successful claim moved the three balances by their + /// exact contract-correct deltas. Split out of claimWithdraw to keep + /// that function's stack frame shallow (avoids stack-too-deep). + /// @param pre packed pre-claim snapshot: [0]=recipient bal, [1]=lock, + /// [2]=totalValueOutOfLp, [3]=WRN bal. + /// @dev Deltas (see WithdrawRequestNFT._claimWithdraw L327-360, LiquidityPool + /// .withdraw L297-305 + receive L185-190): + /// recipient += amountToWithdraw + /// lock -= amountOfEEth (the FULL escrowed amount) + /// totalValueOutOfLp-= amountToWithdraw + strandedSweep + /// strandedSweep = (wrnBal - amountToWithdraw) - (lock - amountOfEEth), + /// provably >= 0 (escrow invariant wrnBal >= lock, amountToWithdraw + /// <= amountOfEEth), so the L351 sweep fires whenever it is > 0. + function _checkClaimDeltas( + uint256 tokenId, + address ownerAddr, + uint256 amountToWithdraw, + uint256 amountOfEEth, + uint256[4] memory pre + ) internal { + uint256 lockAfter = pre[1] - amountOfEEth; + uint256 wrnBalAfterPay = pre[3] - amountToWithdraw; + uint256 strandedSweep = wrnBalAfterPay > lockAfter ? wrnBalAfterPay - lockAfter : 0; + + uint256 expRecipient = pre[0] + amountToWithdraw; + uint256 expOutOfLp = pre[2] - amountToWithdraw - strandedSweep; + + if (ownerAddr.balance != expRecipient) { + ghost_claimDeltaViolated = true; + ghost_deltaFailTokenId = tokenId; + ghost_deltaFailExpected = expRecipient; + ghost_deltaFailActual = ownerAddr.balance; + } else if (uint256(wrn.ethAmountLockedForWithdrawal()) != lockAfter) { + ghost_claimDeltaViolated = true; + ghost_deltaFailTokenId = tokenId; + ghost_deltaFailExpected = lockAfter; + ghost_deltaFailActual = uint256(wrn.ethAmountLockedForWithdrawal()); + } else if (uint256(lp.totalValueOutOfLp()) != expOutOfLp) { + ghost_claimDeltaViolated = true; + ghost_deltaFailTokenId = tokenId; + ghost_deltaFailExpected = expOutOfLp; + ghost_deltaFailActual = uint256(lp.totalValueOutOfLp()); + } else { + ghost_claimDeltaChecks++; + } + } + + /// @notice (S3) Deterministic invalidate/validate probe. Two parts, both + /// self-contained so they fire reliably every run: + /// A. Create a FRESH (not-yet-finalized) request, have the guardian + /// invalidateRequest it, and assert the owner can no longer claim + /// (claim reverts RequestNotValid). Then have the operating + /// timelock validateRequest it back and assert validity is + /// restored (the claim's RequestNotValid block is gone — only the + /// RequestNotFinalized block remains, since it is unfinalized). + /// B. Attempt invalidateRequest on a FINALIZED request + /// (lastFinalizedRequestId) and assert it reverts + /// CannotInvalidateFinalizedRequest. + /// Roles: invalidateRequest is onlyGuardian, validateRequest is + /// onlyOperatingTimelock (WithdrawRequestNFT L258/L270). + function doInvalidateValidateProbe(uint256 actorSeed, uint128 amountSeed) external { + // ---- Part A: round-trip on a fresh, non-finalized request ---- + address actor = _eoa(actorSeed); + uint256 actorEEth = eETH.balanceOf(actor); + uint256 lo = lp.minWithdrawAmount(); + uint256 hiCap = lp.maxWithdrawAmount(); + if (actorEEth >= lo) { + uint256 hi = actorEEth < hiCap ? actorEEth : hiCap; + if (hi > 30 ether) hi = 30 ether; + if (hi >= lo) { + uint256 amt = bound(uint256(amountSeed), lo, hi); + vm.prank(actor); + try lp.requestWithdraw(actor, amt) returns (uint256 tokenId) { + ourTokenIds.push(tokenId); + tokenAmount[tokenId] = uint96(amt); + ghost_requestsCreated++; + callCounts["req"]++; + + // Guardian invalidates the not-yet-finalized request. + vm.prank(guardian); + try wrn.invalidateRequest(tokenId) { + callCounts["invalidate_ok"]++; + // MUST now be invalid. + if (wrn.getRequest(tokenId).isValid) ghost_invalidateProbeFailed = true; + // MUST no longer be claimable: claim reverts RequestNotValid. + vm.prank(actor); + try wrn.claimWithdraw(tokenId) { + ghost_invalidateProbeFailed = true; // invalidated request settled + callCounts["invalidated_claim_ok"]++; + } catch (bytes memory cerr) { + bytes4 csel = cerr.length >= 4 ? bytes4(cerr) : bytes4(0); + if (csel == SEL_REQUEST_NOT_VALID) { + callCounts["invalidated_claim_rejected"]++; + } else { + // Some other revert also blocks the claim, but the + // invalid flag should be the FIRST gate to trip. + ghost_invalidateProbeFailed = true; + callCounts["invalidated_claim_other_revert"]++; + } + } + + // Operating timelock validates it back. + vm.prank(operatingTimelock); + try wrn.validateRequest(tokenId) { + callCounts["validate_ok"]++; + // MUST be valid again. + if (!wrn.getRequest(tokenId).isValid) ghost_invalidateProbeFailed = true; + // The RequestNotValid block MUST be gone. Claiming an + // unfinalized-but-valid request now reverts + // RequestNotFinalized (proving validity was restored). + vm.prank(actor); + try wrn.claimWithdraw(tokenId) { + // Unfinalized request should not settle. + ghost_invalidateProbeFailed = true; + callCounts["revalidated_claim_ok"]++; + } catch (bytes memory rerr) { + bytes4 rsel = rerr.length >= 4 ? bytes4(rerr) : bytes4(0); + if (rsel == SEL_REQUEST_NOT_VALID) { + // Still blocked as invalid -> validate did not restore it. + ghost_invalidateProbeFailed = true; + callCounts["revalidated_still_invalid"]++; + } else { + // RequestNotFinalized (or any non-validity revert): the + // validity block is gone, as required. + callCounts["revalidated_claim_rejected"]++; + } + } + ghost_invalidateValidateProbes++; + } catch { + // validateRequest of an existing invalid, non-finalized + // request should always succeed. + ghost_invalidateProbeFailed = true; + callCounts["validate_revert"]++; + } + } catch { + // invalidateRequest of a valid, non-finalized request should + // always succeed for the guardian. + ghost_invalidateProbeFailed = true; + callCounts["invalidate_revert"]++; + } + } catch { + callCounts["req_revert"]++; + } + } + } + + // ---- Part B: invalidate on a FINALIZED request MUST revert ---- + // invalidateRequest checks `requestId <= lastFinalizedRequestId` FIRST + // (WithdrawRequestNFT L259), so lastFinalizedRequestId itself trips the + // guard regardless of that request's validity/existence. + uint32 lastFin = wrn.lastFinalizedRequestId(); + if (lastFin >= 1) { + vm.prank(guardian); + try wrn.invalidateRequest(uint256(lastFin)) { + ghost_finalizedInvalidateAllowed = true; + callCounts["invalidate_finalized_ok"]++; + } catch (bytes memory err) { + bytes4 sel = err.length >= 4 ? bytes4(err) : bytes4(0); + if (sel == SEL_CANNOT_INVALIDATE_FINALIZED) { + ghost_finalizedInvalidateRejected++; + callCounts["invalidate_finalized_rejected"]++; + } else { + ghost_finalizedInvalidateAllowed = true; // wrong revert reason + callCounts["invalidate_finalized_other"]++; + } + } + } + } + + /// @notice Positive rebase stress — keeps the rate climbing (frozen-rate + /// shield is irrelevant to solvency here, just adds state churn). + /// Bounded to <= 0.2% of TVL so it stays under the contract's + /// MAX_POSITIVE_REBASE_BPS (0.25%) cap and actually applies. + /// Caller is the etherFiAdminContract — the only address + /// `LiquidityPool.rebase` accepts (LiquidityPool.sol:456). + function rebasePositive(uint128 deltaSeed) external { + uint256 outOfLp = uint256(lp.totalValueOutOfLp()); + uint256 cap = outOfLp == 0 ? 1 ether : (outOfLp * 20) / 1e4; // <=0.2% + if (cap == 0) cap = 1; + if (cap > uint256(uint128(type(int128).max))) cap = uint256(uint128(type(int128).max)); + int128 delta = int128(int256(bound(uint256(deltaSeed), 0, cap))); + vm.prank(etherFiAdminAddr); + try lp.rebase(delta, 0) { callCounts["rebase_pos"]++; } + catch { callCounts["rebase_pos_revert"]++; } + } + + /// @notice Bounded NEGATIVE rebase (<= 0.5% of TVL). Bounded so the share + /// rate stays far above `minAmountForShare`: an extreme slash that + /// pushes `amountForShare(1e18) < minAmountForShare` would legitimately + /// block claims via `_checkMinAmountForShare` — that is a known + /// liveness edge, NOT a solvency bug, so we keep it out of the P3 + /// claimability property by bounding the slash conservatively. + function rebaseNegative(uint128 deltaSeed) external { + uint256 outOfLp = uint256(lp.totalValueOutOfLp()); + // Keep headroom above the WRN lock so a later claim's + // `totalValueOutOfLp -= amountToWithdraw` cannot underflow. + uint256 lock = uint256(wrn.ethAmountLockedForWithdrawal()); + if (outOfLp <= lock) { callCounts["rebase_neg_skipped"]++; return; } + uint256 headroom = outOfLp - lock; + uint256 cap = (outOfLp * 50) / 1e4; // <=0.5% of TVL + if (cap > headroom / 2) cap = headroom / 2; + if (cap == 0) { callCounts["rebase_neg_skipped"]++; return; } + if (cap > uint256(uint128(type(int128).max))) cap = uint256(uint128(type(int128).max)); + int128 delta = -int128(int256(bound(uint256(deltaSeed), 1, cap))); + vm.prank(etherFiAdminAddr); + try lp.rebase(delta, 0) { callCounts["rebase_neg"]++; } + catch { callCounts["rebase_neg_revert"]++; } + } + + // ===================================================================== + // VIEW HELPERS + // ===================================================================== + + function ourTokenIdsLength() external view returns (uint256) { return ourTokenIds.length; } + + function _eoa(uint256 seed) internal view returns (address) { + return actors[seed % N_EOAS]; + } +}