test(invariant): I3 withdrawal-queue solvency fork harness#471
Conversation
Fork-based stateful invariants for I3 (withdrawal queue accounting / solvency) on EtherFiRedemptionManager + WithdrawRequestNFT + LiquidityPool: - finalized claims always backed by LP liquidity (SC-enforced bound) - locked-for-withdrawal ETH within accounted state (totalValueInLp/OutOfLp) - finalized requests always claimable; TVL decomposition; LP solvency - WRN raw-ETH escrow >= lock 7 invariants, 2048 calls each, 0 reverts, non-vacuous (requests created/ finalized/claimed counters all > 0). EigenLayer-queued-withdrawals term reclassified to the strictly-stronger in-protocol bound (documented inline) since live EL state can't be deterministically controlled on a latest fork. src untouched.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 2 potential issues.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 353f8f5. Configure here.
| callCounts["finalize"]++; | ||
| } catch { | ||
| callCounts["finalize_revert"]++; | ||
| } |
There was a problem hiding this comment.
Finalize revert leaves orphan lock
Medium Severity
In finalizeRequests, a successful addEthAmountLockedForWithdrawal is not rolled back when the following finalizeRequests call reverts. lastFinalizedRequestId stays unchanged, so a later finalize can lock the same request range again, inflating ethAmountLockedForWithdrawal and escrow without matching finalization—unlike production, where EtherFiAdmin._finalizeWithdrawals applies both steps atomically.
Reviewed by Cursor Bugbot for commit 353f8f5. Configure here.
| assertGt(handler.ghost_requestsCreated(), 0, "non-vacuity: no withdraw request was ever created"); | ||
| assertGt(handler.ghost_requestsFinalized(), 0, "non-vacuity: no request was ever finalized"); | ||
| 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"); |
There was a problem hiding this comment.
Non-vacuity counts setUp seeds
Low Severity
afterInvariant requires ghost_requestsCreated, ghost_requestsFinalized, and ghost_finalizeBoundChecks to be greater than zero, but setUp already drives those counters via seeded requestWithdraw and finalizeRequests before fuzz runs reset to that snapshot. Those gates can pass without the fuzzer creating, finalizing, or exercising P1 during the run.
Reviewed by Cursor Bugbot for commit 353f8f5. Configure here.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
1 participant
I3 — Withdrawal-queue accounting / solvency (fork-based fuzz)
Closes the live-state half of invariant I3 with a mainnet-fork stateful invariant harness on
EtherFiRedemptionManager+WithdrawRequestNFT+LiquidityPool.7 invariants, 2048 calls each, 0 reverts — independently re-run on a mainnet fork. Non-vacuous: requests created / finalized / claimed counters all > 0.
invariant_i3_finalized_backed_by_liquidity— finalized claims never exceedtotalValueInLp(theEtherFiAdmin._validateWithdrawalsbound)invariant_i3_locked_within_accounted_state—ethAmountLockedForWithdrawal ≤ totalValueInLp + totalValueOutOfLpinvariant_i3_finalized_always_claimable— every finalized request claims with 0 revertsinvariant_i3_escrow_backs_lock,invariant_i3_tvl_decomposition,invariant_i3_lp_solvent_in_lpSoundness note (documented inline): the formal I3 includes
+ EigenLayer-queued withdrawals(all pods), which is live, block-drifting state that can't be deterministically controlled on a latest-block fork without fabricating EL state. Reclassified to the strictly-stronger in-protocol bound (ignores the favorable EL term, requires obligations backed by accounting alone). All assertions delta-aware vs captured live mainnet baselines — never zero-baseline.src/untouched (test/ only). Base:seongyun/fuzz/security-upgrades(same as #470).Note
Low Risk
Test-only additions; no production contract or deployment logic changes.
Overview
Adds a mainnet-fork stateful invariant suite for withdrawal-queue I3 solvency, with no
src/changes.WithdrawalSolvency.invariant.t.solwiresinitializeRealisticFork, funds five actors, clears legacy pending mainnet requests via production-style lock+finalize, seeds handler-owned requests, and asserts P1–P3 (finalize vstotalValueInLp, lock within accounted TVL + WRN escrow, finalized claims succeed) plus LP TVL decomposition and in-LP balance checks.afterInvariantenforces non-vacuity (create/finalize/claim and P1 bound checks). Inline docs reclassify the full I3 formula (EigenLayer-queued withdrawals) to the stronger in-protocol bounds the contracts enforce.WithdrawalSolvencyHandler.solfuzzesrequestWithdraw, adminaddEthAmountLockedForWithdrawal+finalizeRequests,claimWithdraw, and bounded positive/negative rebases, tracking ghosts and call counts for failures and coverage.Reviewed by Cursor Bugbot for commit 353f8f5. Bugbot is set up for automated code reviews on this repo. Configure here.