test(invariant): fix Cursor Bugbot findings (I10 membership mgr + I12/I13 non-vacuity)

test/invariant/RewardsDistributor.invariant.t.sol

@@ -39,6 +39,21 @@ contract RewardsDistributorInvariantTest is TestSetup {
         // 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[](7);
+        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;
+        targetSelector(FuzzSelector({addr: address(handler), selectors: selectors}));
         targetContract(address(handler));
     }
 
@@ -79,6 +94,30 @@ contract RewardsDistributorInvariantTest is TestSetup {
         );
     }
 
+    // =====================================================================
+    // 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");
+
+        // 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).
     // =====================================================================

test/invariant/ValidatorStateMachine.invariant.t.sol

@@ -49,7 +49,12 @@ contract ValidatorStateMachineInvariantTest is TestSetup, Deployed {
             priorityWithdrawalQueue: address(priorityQueueInstance),
             blacklister: address(blacklisterInstance),
             etherFiAdminContract: address(etherFiAdminInstance),
-            membershipManager: address(membershipManagerInstance)
+            // 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
         }), 0);
         address lpOwner = liquidityPoolInstance.owner();
         vm.prank(lpOwner);
@@ -60,7 +65,7 @@ contract ValidatorStateMachineInvariantTest is TestSetup, Deployed {
         address wrnOwner = withdrawRequestNFTInstance.owner();
         vm.prank(wrnOwner);
         withdrawRequestNFTInstance.upgradeTo(
-            address(new WithdrawRequestNFT(WITHDRAW_REQUEST_NFT_BUYBACK_SAFE, address(eETHInstance), address(liquidityPoolInstance), address(membershipManagerInstance), address(roleRegistryInstance), address(blacklisterInstance), address(etherFiAdminInstance), 1, 4e18))
+            address(new WithdrawRequestNFT(WITHDRAW_REQUEST_NFT_BUYBACK_SAFE, address(eETHInstance), address(liquidityPoolInstance), MEMBERSHIP_MANAGER, address(roleRegistryInstance), address(blacklisterInstance), address(etherFiAdminInstance), 1, 4e18))
         );
 
         // The production queue proxy on mainnet still runs the master impl which

test/invariant/handlers/RewardsDistributorHandler.sol

@@ -97,6 +97,7 @@ contract RewardsDistributorHandler is StdUtils {
 
         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;
@@ -154,7 +155,13 @@ contract RewardsDistributorHandler is StdUtils {
 
     /// @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.
+    ///         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);
@@ -182,6 +189,20 @@ contract RewardsDistributorHandler is StdUtils {
             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"]++;
         }