test: address deep review of #470 (I3/P1 vacuity, I11/I12 non-vacuity gates, I7 scope)#475
Merged
seongyun-ko merged 2 commits intoJun 16, 2026
Conversation
…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.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
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
1 participant
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.
Addresses the full hand-review of the #470 invariant suite. Test/spec only — zero
src/changes. Every fix was re-run and verified.HIGH — I3/P1 was a dead-code assertion (no-op)
WithdrawalSolvencyHandler.finalizeRequestspre-filteredlockAmount > inLpBeforeand then re-checked the same condition inside the lock's success branch — unreachable.ghost_finalizeExceededLiquiditycould never be set, soinvariant_i3_finalized_backed_by_liquiditywas structurally true regardless of contract behaviour. The suite refused to feed_lockEth(LiquidityPool.sol:598) the exact over-bound input P1 claims to test.Fix (mirrors the correct I13
doFinalizepattern):ghost_lockBoundEnforced); a liquidity revert while the range was backed tripsghost_lockRejectedWhileBacked.probeOverLiquidityLock— deliberately attempts a lock> totalValueInLpand asserts rejection. Self-contained, so the non-vacuity gate survives Foundry sequence-shrinking.ghost_lockBoundEnforced > 0.lockBoundEnforced=26,finalizeBoundChecks=7, 7/7 pass, 0 reverts (the guard was provably dead before).MEDIUM — I11 (ValidatorLifecycle) missing non-vacuity gate + targetSelector
Only suite with no
afterInvariantand notargetSelector: the fuzzer wasted budget on view getters, and bothinvariant_I11_*could pass trivially if no link/re-link ever fired.Fix:
targetSelector(doLink, doRelinkAttack)+afterInvariantassertinglink_ok > 0andlink_already_revert + relink_attempt > 0. Verified:link_ok=15,relink_attempt=37, 3/3 pass.LOW — I12 monotonic-decrease guard untested
doClaimalways usesnewCum = preCum + delta(delta ≥ 1), sopostCum < preCumwas impossible and the contract'spreclaimed >= cumulativeAmount => NothingToClaimguard (L113) was never driven.Fix:
doLowerCumulativeClaim— bootstraps a claim, then attempts a strictly-lower cumulative and asserts rejection (self-contained for shrink-safety) + non-vacuity gate. Verified:lower_rejected=7,lower_unexpected_ok=0, 3/3 pass.LOW — I7 Certora deposit filter narrower than the modifier
nonDecreasingRateguards_deposit, reached bydeposit(),deposit(address),deposit(address,address), anddepositToRecipient— but the I7 filter only listeddeposit(address,address). Widened to match I8.Re-verified on the cloud prover —
SUCCESSacross all four deposit variants +withdraw+ both burn paths. (report)Also worth folding into the #470 PR body (doc-only, reviewer's nits)
revokeFastguards + "no other method mutates membership" — it does not provegrantRole/revokeRole/setRoleare owner-gated (punted to trusting solady's assembly self-call).rule_sanity: none) — a lemma, not coverage.afterInvariantassertsnumRejOther == 0— strict/brittle by design; flagged for maintainers.Note
Low Risk
Changes are confined to Foundry invariant handlers, non-vacuity gates, and Certora spec filters; no
src/or runtime protocol logic is modified.Overview
Test and Certora spec only — no production contract changes. The PR hardens the #470 invariant suite so properties are actually exercised instead of passing vacuously.
I3/P1 (WithdrawalSolvency) —
finalizeRequestsno longer skips locks whenlockAmount > totalValueInLp; it always attemptsaddEthAmountLockedForWithdrawaland classifies success vsInsufficientLiquidity/ migration / other reverts. AddsprobeOverLiquidityLockto deliberately over-lock, ghosts for wrongly accepting or rejecting backed locks, dual-direction P1 checks,targetSelectoron real actions, and anafterInvariantfloor thatghost_lockBoundEnforced > 0.I11 (ValidatorLifecycle) — Fuzzing is limited to
doLink/doRelinkAttack;afterInvariantrequires at least one successful link and one re-link rejection path.I12 (RewardsDistributor) — New
doLowerCumulativeClaimdrives the monotonic-decrease /NothingToClaimguard;setUpseeds a baseline claim + lower-cumulative attempt so gates survive shrinking;afterInvariantassertslower_rejected > 0.Certora I7 — The guarded-method filter now includes all
nonDecreasingRatedeposit entry points (deposit(),deposit(address),depositToRecipient), aligned with I8.Reviewed by Cursor Bugbot for commit c4cc526. Bugbot is set up for automated code reviews on this repo. Configure here.