test: invariant fuzz + Certora CVL coverage for protocol invariants (I4,I6-I13)#470
Open
seongyun-ko wants to merge 32 commits into
Open
test: invariant fuzz + Certora CVL coverage for protocol invariants (I4,I6-I13)#470seongyun-ko wants to merge 32 commits into
seongyun-ko wants to merge 32 commits into
Conversation
…ants I10-I13 Adds stateful invariant coverage for the four promoted invariants that had none: I10 validator-creation state machine, I11 pubkey->node uniqueness, I12 cumulative-claim monotonicity, I13 reward-root finalization delay. I7/I8/I9/I14 already covered by the existing ProtocolInvariants suite.
…onotonicity) + I8 (LP solvency) I7: exchange-rate monotonicity across all nonDecreasingRate-guarded methods, asserted cross-multiplied (P1*S0 >= P0*S1) with the contract's own bootstrap exemption. I8: LP-buffer solvency in the provable success-implies-solvent form over every _checkTotalValueInLp-guarded write path. I9: pooled-ether decomposition lemma. All three VERIFIED by the Certora Prover. Verified locally: prover.certora.com report e3a0856b059a4511bf172dcc9c4a96b9 — No errors found.
…rFiRateLimiter) 5 invariants on the general rate limiter (global bucket): remaining<=capacity, consume-iff-canConsume + exact decrease, capacity==0 freeze, refill monotonic+bounded, unknown-limit/consumer gating. Non-vacuous (afterInvariant asserts consume_ok>0 + refill observed). Complements the existing redemption-bucket coverage; closes the I4 gap for the non-redemption limiters.
I6.4 no stray mutation (only role-mgmt methods change membership), I6.2 revokeFast reverts on the 3 protected timelock/multisig roles, I6.1 revokeFast requires revokeAdmin, I6.3 revokeFast only removes (never grants). No internal summaries — proven from native gates the prover models directly (solady's assembly owner() self-call is havoc'd, so authority is proven via the no-stray-mutation + revokeFast-gate angle). All VERIFIED. Verified locally: prover.certora.com report f5968588150140fcb172af8b72ca069b — No errors found.
…-rewards-invariants test: invariant fuzz + Certora CVL coverage for protocol invariants (I4,I6-I13)
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
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.
Stateful sequence test for I5 (oracle integrity) on EtherFiOracle + EtherFiAdmin: every applied OracleReport (advancing lastHandledReportRefSlot via executeTasks) must satisfy all three gates -- quorum (>= quorumSize sigs), APR cap (|rebase APR| <= acceptableRebaseAprInBps), freshness (past postReportWaitTimeInSlots). Proven via an independent, byte-faithful gate mirror that flips a ghost if any gate-violating apply ever occurs; mirror fidelity cross-checked against the contract's own revert reasons. Deterministic (not randomized invariant) because EtherFiOracle's strict slot/epoch state machine can't be driven reliably under Foundry's stateful- fuzz scheduling/shrinking -- matches how EtherFiOracle.t.sol tests it. 38 reports applied + 19/20/19 quorum/apr/freshness rejections, reproducible, 0 uncategorised reverts. src untouched.
This was referenced Jun 14, 2026
Replaces the deterministic sequence test with a true randomized stateful fuzz-invariant (Foundry invariant engine, 64 runs x 1920 calls, 0 reverts). Root cause of the earlier vacuity (numApplied==0 under the invariant runner): the 'valid apply' scenario bounded its rebase reward to a blind 0..0.5 ether constant. The APR gate caps |apr| = 10000*reward*365d/(tvl*elapsedTime); on reports after the first, elapsedTime is just the ~1100-slot range moved, so 0.5 ether computes to ~11900 bps > the 10000 cap -> the supposedly-valid apply reverted on APR, leaving the report published-but-unapplied -> oracle stuck -> every later step bailed at the un-stuck guard. The fuzzer found this; the deterministic loop (tiny uniform rewards) never did. Fix: _maxSafeReward() sizes the apply/fresh-fail reward to half the per-range APR-cap boundary, so the accepting path is genuinely accepted regardless of the fuzzed magnitude or the range length the clock produces. Result: 60 reports applied + 30/30/30 quorum/apr/freshness rejections, mirror-consistent, stable across seeds. No gate-violating apply ever observed. No assertion weakened; src untouched.
test_handleRemainder asserted totalRemainderShares strictly DECREASES after handleRemainder. On a mainnet fork the remainder is sub-share rounding dust: getRemainderAmount() rounds shares->amount DOWN, and handleRemainder converts amount->shares via sharesForAmount() rounding DOWN again, so the swept share delta can legitimately be ZERO. The strict-decrease assertion then fails non-deterministically depending on the live fork share rate (observed: 'Remainder should decrease: 1 >= 1'). Fix: replicate handleRemainder's exact share accounting (treasury split rounds up, burn gets the rest, both converted via sharesForAmount) and assert totalRemainderShares drops by EXACTLY that amount -- deterministic, fork-rate independent, and strictly stronger than the old inequality. Keep the strict decrease only in the genuinely-sweepable case (>=1 share moved). No src change; verified passing 3x on a mainnet fork.
Two Medium findings from Cursor Bugbot:
1. ValidatorStateMachine (I10): the fork suite re-deployed LiquidityPool and
WithdrawRequestNFT passing address(membershipManagerInstance) as the
membership-manager immutable, but on a realistic fork that V0-typed var is
never populated (only membershipManagerV1Instance is, from
deployed.MEMBERSHIP_MANAGER()). The new impls therefore got a zero membership
manager, diverging from the production bootstrap. Fixed to use the real
deployed MEMBERSHIP_MANAGER constant for both the LP and WRN constructors.
2. RewardsDistributor (I12/I13): the suite logged coverage counters but never
HARD-asserted that finalize/claim actually happened, so the ghost flags could
stay false and the invariants pass vacuously. Root causes found & fixed:
(a) no targetSelector -> the engine also fuzzed the handler's view getters,
wasting the call budget; added an explicit action-only selector list.
(b) added an afterInvariant() non-vacuity gate (finalize_ok / claim_ok /
replay_revert > 0 and total ETH paid > 0).
(c) made doClaim self-contained (it already finalizes via _establishRoot; now
also runs an inline replay-rejection and counts the finalize), so a single
call exercises finalize+claim+replay -- keeping the non-vacuity gate
satisfiable even when Foundry shrinks a failing run to a 1-call sequence.
Verified: rewards suite 256x16384 calls, 0 reverts, non-vacuous (finalize_ok=23,
claim_ok=9, replay_revert=16), stable across 3 seeds; I10 fork suite still passes
with the membership-manager fix. src untouched.
…le-remainder test(pwq): de-flake test_handleRemainder against fork rounding dust
test(invariant): fix Cursor Bugbot findings (I10 membership mgr + I12/I13 non-vacuity)
…lvency-i3-i5 test(invariant): I5 oracle-integrity stateful fuzz invariant
…cy-fork test(invariant): I3 withdrawal-queue solvency fork harness
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
…gates, I7 scope)
HIGH — I3/P1 was a dead-code assertion. WithdrawalSolvencyHandler.finalizeRequests
pre-filtered `lockAmount > inLpBefore` then re-checked it inside the success branch,
so ghost_finalizeExceededLiquidity was unreachable and invariant_i3_finalized_backed
_by_liquidity was structurally true. The handler refused to feed _lockEth the very
over-bound input the property claims to test (LiquidityPool.sol:598).
- Removed the pre-filter; attempt the lock UNCONDITIONALLY (mirrors the correct
I13 doFinalize pattern). Classify reverts by selector: liquidity-guard rejection
of an unbacked lock is a POSITIVE observation; a liquidity revert while the range
was backed trips ghost_lockRejectedWhileBacked.
- Added probeOverLiquidityLock: deliberately attempts a lock > totalValueInLp and
asserts rejection — positively drives the guard, self-contained so the gate
survives sequence-shrinking.
- Dual-direction P1 invariant + non-vacuity gate ghost_lockBoundEnforced > 0.
Verified: lockBoundEnforced=26, finalizeBoundChecks=7 (was provably dead).
MEDIUM — I11 (ValidatorLifecycle) had no targetSelector and no afterInvariant gate,
so the fuzzer burned budget on view getters and both invariants could pass trivially.
Added targetSelector(doLink/doRelinkAttack) + afterInvariant asserting link_ok>0 and
(link_already_revert+relink_attempt)>0. Verified non-vacuous: link_ok=15, relink=37.
LOW — I12 monotonic-decrease guard (preclaimed >= cumulativeAmount => NothingToClaim)
was never driven; doClaim only increases cumulative. Added doLowerCumulativeClaim
(self-contained: bootstraps a claim, then attempts a strictly-lower cumulative and
asserts rejection) + non-vacuity gate. Verified: lower_rejected=7, lower_unexpected_ok=0.
LOW — I7 Certora deposit filter only listed deposit(address,address) though
nonDecreasingRate guards _deposit (reached by all 4 deposit variants). Widened to
match I8. Re-verified on the cloud prover: SUCCESS across deposit()/deposit(address)/
deposit(address,address)/depositToRecipient + withdraw + both burn paths.
Test-only: no src/ changes. All four affected suites re-run and pass non-vacuously.
…obust floor) The afterInvariant gates assert on per-run handler counters that, on some fuzz seeds, read 0 at evaluation time — not just the new lower_rejected, but the pre-existing finalize_ok/claim_ok too. On unlucky seeds the no-op-ish selectors (doWarp/doRoll/doSetClaimDelay) dominate the sequence and the lifecycle never fires, so the gate flakes red (~1-in-5 with no pinned seed). This was latent in #470; adding doLowerCumulativeClaim as the 8th selector perturbed the distribution enough to surface it on seed 5. Fix (same pattern WithdrawalSolvency uses to guarantee its floor): deterministically drive one full lifecycle in setUp — handler.doClaim (self-contained: establish -> finalize -> claim -> replay-rejected, seeds finalize_ok/claim_ok/replay_revert) and handler.doLowerCumulativeClaim (seeds lower_rejected). Foundry reverts to the post-setUp snapshot before every run, so these counters are a guaranteed baseline on EVERY seed. The fuzzer still independently exercises all paths at runtime; this only establishes the non-vacuity floor. Verified across seeds 1-8 (incl. the seed-5 that failed pre-fix): 3/3 pass every time; floor counters non-zero (finalize_ok=32, claim_ok=9, lower_rejected=10 on seed 5). Confirmed the parent commit FAILS seed 5 (0 passed; 3 failed), so this commit is what removes the flake rather than masking it. Also clarified ghost_lockRejectedWhileBacked's docstring: _lockEth emits InsufficientLiquidity from two sites (entry guard + post-send _checkTotalValueInLp); the ghost conservatively flags either while backed — both are real solvency violations, so the name is narrower than what it correctly catches. Test-only: no src/ changes.
…-round2 test: address deep review of #470 (I3/P1 vacuity, I11/I12 non-vacuity gates, I7 scope)
0xpanicError
changed the base branch from
pankaj/feat/security-upgrades
to
pankaj/feat/security-upgrades-PR-scripts
|
Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits. |
…ad vars) Fixes the open Cursor Bugbot findings against the I3/I10 fork invariant suites (all confirmed against source, not the bot summary): - WithdrawalSolvency: rebasePositive/rebaseNegative pranked membershipManager, but LiquidityPool.rebase requires msg.sender == etherFiAdminContract (LiquidityPool.sol:456). On a realistic fork membershipManagerInstance is address(0) (only set in initializeTestingFork), so both helpers always reverted IncorrectCaller AND were never even in the fuzz selector set (dead code). Now prank the real etherFiAdminContract, drop the unused membershipManager immutable/ctor arg, add both ops to targetSelector, and bound the positive rebase to <=0.2% so it stays under MAX_POSITIVE_REBASE_BPS (0.25%) and actually applies. - WithdrawalSolvency: removed unused baseLocked/baseOutOfLp snapshots; the invariants assert the stronger construction-true absolute bound, so the baseline vars were dead. - ValidatorStateMachine: PriorityWithdrawalQueue ctor is (lp, eETH, weETH, blacklister, roleRegistry, minDelay); the fork upgrade passed roleRegistry as blacklister and treasury as roleRegistry. Now wired with blacklisterInstance + roleRegistryInstance in their correct slots. Verified on mainnet fork: WithdrawalSolvency 7/7 pass (requestsClaimed=14, finalizeBoundChecks=7, lockBoundEnforced=10), ValidatorStateMachine 2/2, RewardsDistributor 3/3 (its non-vacuity gates were already present).
…-comments test: address Bugbot review on #470 (rebase caller, PWQ ctor args, dead vars)
…ock finalize not rolled back") Bugbot (Medium): in WithdrawalSolvencyHandler.finalizeRequests the lock (addEthAmountLockedForWithdrawal) and finalize (finalizeRequests) ran as two separate calls. A committed lock followed by a finalize revert orphaned the lock: ethAmountLockedForWithdrawal stayed bumped while lastFinalizedRequestId did not advance, so a later fuzz step could re-lock the SAME id range and move extra ETH out of the LP. That diverges from production (EtherFiAdmin._finalizeWithdrawals, EtherFiAdmin.sol:427-428), which runs finalizeRequests then addEthAmountLockedForWithdrawal in ONE atomic transaction. Fix: route both legs through a single external self-call (this._finalizeThenLock) in production order (finalize -> lock), wrapped in try/catch. The shared frame gives all-or-nothing semantics: if either leg reverts, BOTH state changes roll back, so no committed lock can outlive a failed finalize and no id range is ever locked twice. P1 enforcement observation is preserved (success => bound held; InsufficientLiquidity revert => bound genuinely violated) and is still positively driven by probeOverLiquidityLock. Verified on mainnet fork: suite 7/7 pass, non-vacuity gates all positively satisfied (requestsCreated=31, finalized=5, claimed=10, finalizeBoundChecks=5, lockBoundEnforced=17).
…-finalize-atomicity test: atomic I3 finalize+lock (Bugbot #470 "Lock finalize not rolled back")
0xpanicError
changed the base branch from
pankaj/feat/security-upgrades-PR-scripts
to
pankaj/feat/security-upgrades
…nto seongyun/fuzz/security-upgrades
…th + upgrade gate The conf files pointed at pre-restructure paths (src/LiquidityPool.sol, src/EETH.sol, src/RoleRegistry.sol) and the I8 filter referenced the deleted returnLockedEth(uint128), so certoraRun could not execute against this tree and the previously cited reports attested to older contract revisions. - Fix file paths to src/core/ and src/governance/; refresh package maps and add the EETH:liquidityPool back-link. - I8: add batchCreateBeaconValidators (new guarded ETH-outflow path) and receive() (via f.isFallback) to the filter; drop returnLockedEth. - rule_sanity basic everywhere; the tautological I9 lemma moves to its own LiquidityPoolDecomposition conf with sanity none so vacuity checking stays on for I7/I8. - RoleRegistry: restore the grant-path proof (successful grantRole/ revokeRole/setRole implies msg.sender == owner()) via a scoped unresolved-call DISPATCH for solady's owner()/MAX_ROLE() self-staticcalls (sound: both target address(this)); add the upgradeToAndCall gate rule (success implies caller held UPGRADE_TIMELOCK_ROLE). - Reframe I7 comments honestly as guard-wiring regression protection; refresh all stale line references. All three configs re-verified at this head, No errors found by Prover, sanity basic passing: - LiquidityPoolPeg (I7/I8): report d9f2667b30f04c54b77f70e5080afa0a - LiquidityPoolDecomposition (I9): report acdc5726dc6143afaed9244e921f68a2 - RoleRegistryAuthority (I6.1-I6.6): report c2be9a4b97454e7ba9a3cb5b06a347ba Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… review Each fix targets a case where a buggy implementation would previously have passed the suite green. Validator suites: - doCreate sent 1 ether to the non-payable batchCreateBeaconValidators, so every call reverted and the REGISTERED->CONFIRMED edge was never tested; the combined create+invalidate vacuity gate hid it. Call is now valueless (the pool self-funds), the gate is split per-edge, and a one-shot coverage-floor bootstrap guarantees both terminals fire every run. - Successful transitions now assert their exact end state, not just any legal edge; illegal edges record the observed before/after pair. - linkLegacyValidatorIds (the second writer to etherFiNodeFromPubkeyHash) is now exercised with an already-linked pubkey and must revert AlreadyLinked; relink attacks use fresh legacy ids (1000+) so they isolate the pubkey-hash guard; I11 gains a global first-seen sweep. - Fork pinned at block 25447657. RateLimiter: - Refill asserted against the exact model min(capacity, before + rate*dt) instead of monotonic+bounded only; occasional near-uint64-max capacity/ rate and long warps reach the clamp regions. - Draining exactly consumable(id) must succeed (was a swallowed revert); consumer revocation/re-grant round-trip added; admin setters assert their exact documented post-state and must not revert on valid input; consume_ok counts only amount>0; depth 128; per-probe coverage gates with a deterministic coverage-floor bootstrap. Oracle: - Duplicate submission by one member must revert ReportNotNeeded and never reach quorum; conflicting same-range reports must not reach consensus. - Freshness probed at exactly wait-1 (reject) and wait (apply); APR probed at the exact boundary reward and one wei above; negative rebase gets a valid small apply plus a one-wei-over-3bps reject (new numRejNegRebase category); setUp pins maxNegativeRebaseBps to the production 3. - ghost_everStuck fails the run if the wedge guard eats a sequence tail. RewardsDistributor: - I13 delay predicate now computed from ghost state (setAt + tracked delay), not the contract's own storage, so write-side timestamp corruption is caught; deterministic boundary probe at delay-1/delay. - Real 4-leaf Merkle tree with genuine 2-element proofs (matching _verifyAsm's sorted-pair hashing) plus a tampered-amount reject, so the proof-verification loop finally executes. WithdrawalSolvency: - Fork pinned at 25447657; setUp derives backlog/deposit sizing from chain state instead of hardcoded live-state assumptions; the silent finalize break is now a loud require. - Claims assert exact deltas: recipient balance += payout, lock -= amountOfEEth, totalValueOutOfLp -= payout + stranded sweep. - invalidate/validate lifecycle probes incl. the finalized-invalidate rejection; P2 relabeled assumption-scoped (bounded rebases) instead of PROVED; vacuity gates baseline-aware against the seeded lifecycle. All six suites green: 36 invariant functions, fork suites at the pinned block, non-fork suites across 5 seeds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The workflow only triggered on PRs into staging-2.5 and master, so the invariant layer merging into pankaj/feat/security-upgrades* never executed in CI. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… into seongyun/fuzz/security-upgrades # Conflicts: # test/invariant/WithdrawalSolvency.invariant.t.sol # test/invariant/handlers/ValidatorStateMachineHandler.sol
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes using default effort and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Want higher recall? High effort reviews run extra passes and find more bugs. A team admin can switch effort levels in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 893bd9a. Configure here.
…rebase cap The generic valid-apply scenarios sized accruedRewards from the APR-cap boundary only (_maxSafeReward / 2). The APR gate scales with the report range's elapsed time, so over a long range that bound can exceed LiquidityPool's absolute MAX_POSITIVE_REBASE_BPS cap: the report passes EtherFiAdmin validation, reverts inside LiquidityPool.rebase with RebaseExceedsPositiveCap, and stays published-but-unhandled — wedging the oracle for the rest of the sequence. _maxSafeReward now returns min(APR boundary, LP positive cap), covering all three apply sites; the APR-boundary scenario keeps its own exact unclamped bound with its existing lpCap guard. Found by Cursor Bugbot on 893bd9a. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
📊 Forge Coverage ReportGenerated by workflow run #774 |
setUp reverted at fork creation in CI (both runs on this PR, deterministic, gas 0) while passing locally against an archive node: CI's MAINNET_RPC_URL provider does not serve state for the old pin 25383537 (~64k blocks deep). Re-pin to 25447657, the same block the invariant fork suites use, which the same CI runs served successfully. The test self-seeds its pre-state, so any block predating the on-chain security upgrade is equivalent. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ork pin Root cause of the ForwardedCallWhitelistRegrant setUp failure in CI: the workflow installs foundry 'nightly', and current nightlies enforce the EIP-3860 initcode-size limit inside tests. WhitelistHarness inherits the full SecurityUpgradesScript (~542 KB initcode, limit 48 KB), so 'new WhitelistHarness()' reverts and setUp dies with a bare EvmError at gas 0 — while the same test passes on stable, which does not enforce the limit in tests. Verified by isolating harness deployment on forge 1.7.2-nightly (fails) vs 1.5.1-stable (passes); fork creation at either pinned block works on both, so the earlier block re-pin (1019043) was a misdiagnosis and is reverted here. Pinning CI to the stable release used locally fixes the failure and stops nightly regressions from breaking CI unpredictably. Bump deliberately when upgrading toolchains. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
Merges
seongyun/fuzz/security-upgrades→pankaj/feat/security-upgrades-PR-scripts(the 26Q2 Security Upgrades release branch — its actual parent).Adds a full invariant/fuzz + Certora CVL test/proof layer for the promoted protocol invariants. No production code — test/spec only, plus a CI-trigger line so the suite actually runs on PRs into this release branch.
Coverage
Fuzz / stateful invariants (all non-vacuous —
afterInvariantgates plus deterministic coverage-floor bootstraps confirm every probe fires on every run):EtherFiRateLimiter): refill checked against the exact modelmin(capacity, before + rate·dt)(that is, a bucket refills linearly in elapsed time and never above its capacity), consume-iff-canConsume with exact decrease, capacity-0 freeze, consumer revocation/re-grant round-trip, setter exact post-state, unknown-limit/consumer gating, near-uint64-max parameter regions.EtherFiOracle/EtherFiAdmin): quorum (including duplicate-submission and conflicting-report shapes), freshness at the exact slot boundary, APR cap at the exact boundary reward and one wei above, negative-rebase cap (3 bps) with its own rejection category.StakingManager,EtherFiNodesManager): per-edge non-vacuity (register / create / invalidate each must fire), exact end-state assertion per transition,linkLegacyValidatorIdssecond-writer path, global first-seen link sweep. Fork pinned at block 25447657.totalValueOutOfLpincluding the stranded-ETH sweep), invalidate/validate lifecycle, drift-proof setUp derived from chain state.Certora CVL proofs — all "No errors found by Prover!",
rule_sanity: basicpassing (non-vacuous), at the current merged head:nonDecreasingRate-guarded entry point (plainly: on the guarded paths the eETH exchange rate can only stay equal or go up). Report355dd1d17bbf47b89dff803992b805c4.batchCreateBeaconValidatorsandreceive(). Same report.1552454d9dfe4bc492b178d3c061f4c1.grantRole/revokeRole/setRoleimplies caller is owner (provable via a scoped unresolved-call dispatch for solady's self-staticcalls — sound because both targetaddress(this)), and successfulupgradeToAndCallimplies caller heldUPGRADE_TIMELOCK_ROLE. Reportc2be9a4b97454e7ba9a3cb5b06a347ba.Review hardening
A dedicated security review of this PR found and fixed, in
4e12e7c1/861ec1e5/dafe9934:returnLockedEth, so the previously cited proofs attested to older contract revisions. Specs/configs reconciled and re-proven at the merged head (report IDs above).pankaj/feat/security-upgrades*(previously onlystaging-2.5/master, so this layer never ran in CI).Verification
Supersedes the mistargeted #469 (which pointed at
master).Note
Low Risk
Changes are limited to tests, Certora specs, and CI workflow configuration; no on-chain contract logic is modified.
Overview
This PR is test and verification only — it adds a full invariant/fuzz layer plus Certora CVL specs for promoted protocol invariants (I3–I5, I6–I13), with no
src/production changes.CI: Forge tests run on PRs targeting
pankaj/feat/security-upgrades*; Foundry is pinned to v1.5.1 instead ofnightlyto avoid EIP-3860 initcode-size failures on large harnesssetUpcontracts.Certora: New configs and specs for LiquidityPool (I7 rate monotonicity on
nonDecreasingRatepaths, I8 LP-buffer solvency on guarded writes, I9 decomposition lemma in a separate conf withrule_sanity: none) and RoleRegistry (I6 authority: owner-only grants,revokeFastguards, upgrade timelock).Foundry invariants: Stateful suites with handlers and non-vacuity
afterInvariantgates cover rate limiter budget (I4), oracle report gates (I5), withdrawal solvency on a pinned mainnet fork (I3), rewards Merkle delay and cumulative claims (I12–I13), validator pubkey→node immutability (I11), and validator creation state machine on fork (I10). EtherFiRestaker gains a stETH feed mock so fork time warps do not hitStalePriceFeed.Reviewed by Cursor Bugbot for commit 899023b. Bugbot is set up for automated code reviews on this repo. Configure here.