diff --git a/test/ProtocolInvariants.t.sol b/test/ProtocolInvariants.t.sol index 06d55b3..126fdbe 100644 --- a/test/ProtocolInvariants.t.sol +++ b/test/ProtocolInvariants.t.sol @@ -45,11 +45,21 @@ contract ProtocolHandler is Test { // rule so stakes are productive rather than reverting on OppositeSideStaked. mapping(address => mapping(uint256 => uint8)) public sidePlusOne; - // Ghost ledger of net principal flowing through the engine. With no epoch - // crossing (no warp action), the engine is a pure escrow, so these tie out - // exactly against the sum of on-chain post totals. + // patch_prD_invariant_warp: settlement-aware ghost ledger. hWarp settles + // EVERY post immediately after warping, so the invariant contract always + // inspects SETTLED state (getPostTotals returns stored totals, never a + // projection). Settlement mints/burns move post totals; ghostSettleNet + // captures that net, measured from the totals delta across updatePost + // (mint == applied gains, burn == applied losses by construction in + // _applyEpoch/_settleBucket). Bucket share<->index floor division can + // strand up to 1 wei per mutating op inside the engine (always + // engine-favoring), so conservation is one-sided with a dust allowance + // of ghostOps wei; ghostWithdrawn records the ACTUAL engine outflow + // (balance delta), not the requested amount, for the same reason. uint256 public ghostDeposited; uint256 public ghostWithdrawn; + int256 public ghostSettleNet; + uint256 public ghostOps; constructor(PostRegistry _registry, StakeEngine _stakeEng, LinkGraph _graph, ScoreEngine _score, MockVSP _vsp) { registry = _registry; @@ -139,6 +149,7 @@ contract ProtocolHandler is Test { try stakeEng.stake(post, side, amt) { sidePlusOne[actor][post] = side + 1; ghostDeposited += amt; + ghostOps++; // patch_prD_invariant_warp: dust bound } catch {} } @@ -161,11 +172,41 @@ contract ProtocolHandler is Test { } uint256 amt = bound(amtSeed, 1, avail); + uint256 balBefore = vsp.balanceOf(address(stakeEng)); vm.prank(actor); try stakeEng.withdraw(post, side, amt, false) { - ghostWithdrawn += amt; + // patch_prD_invariant_warp: the engine transfers `removed`, which + // under a settled bucket (bucketIndexRay != RAY) may differ from + // the requested amount by floor-dust. Record the ACTUAL outflow. + ghostWithdrawn += balBefore - vsp.balanceOf(address(stakeEng)); + ghostOps++; } catch {} } + + /// patch_prD_invariant_warp: THE settlement action. Warps 1..7 epochs and + /// then force-settles every post, so invariants always run against settled + /// state — invariant_engineSolvent finally exercises the regime where the + /// S-01 class lived (bucketIndexRay rebase, epoch mint/burn, rescale). + /// Totals are read BEFORE the warp (state is settled at entry, so + /// getPostTotals is stored, not projected) and again after each + /// updatePost; the delta is settlement's net effect on principal. + function hWarp(uint256 daysSeed) public { + uint256 nDays = bound(daysSeed, 1, 7); + uint256 n = allPosts.length; + uint256[] memory beforeT = new uint256[](n); + for (uint256 i = 0; i < n; i++) { + (uint256 s, uint256 c) = stakeEng.getPostTotals(allPosts[i]); + beforeT[i] = s + c; + } + vm.warp(block.timestamp + nDays * 1 days); + for (uint256 i = 0; i < n; i++) { + try stakeEng.updatePost(allPosts[i]) {} catch {} + } + for (uint256 i = 0; i < n; i++) { + (uint256 s, uint256 c) = stakeEng.getPostTotals(allPosts[i]); + ghostSettleNet += int256(s + c) - int256(beforeT[i]); + } + } } /// @title Protocol invariants (item 253) @@ -174,12 +215,14 @@ contract ProtocolHandler is Test { /// and safety guarantees: /// INV-1 Solvency: the StakeEngine always holds at least the sum of all /// recorded positions, so it can always pay out. -/// INV-2 Conservation: the sum of all on-chain post totals equals net -/// principal (deposited - withdrawn) tracked by the handler ledger. -/// Holds EXACTLY because this suite stays in the materialized regime: -/// it has no warp action, so no epoch settlement / mint / burn fires -/// and the engine behaves as a pure escrow. (The settlement / decay / -/// projection path is covered by StakeEngineFuzz + StakeEngineRescale.) +/// INV-2 Conservation (patch_prD_invariant_warp): post totals equal net +/// principal (deposited - actual-withdrawn) plus settlement's net +/// mint/burn (ghostSettleNet), one-sided with a dust allowance: +/// bucket share<->index floor division strands <=1 wei per mutating +/// op inside the engine, always engine-favoring, so the ledger side +/// may exceed the totals side by at most ghostOps wei — and never +/// the other way around. hWarp settles every post right after +/// warping, so all reads here are stored (settled), not projected. /// INV-3 VS bounded: baseVSRay and effectiveVSRay are always within /// [-RAY, +RAY] for every claim, after any sequence. /// INV-4 Single-sided: no (actor, post) ever holds both support and challenge @@ -256,15 +299,13 @@ contract ProtocolInvariantsTest is Test { ); } - /// INV-2: on-chain totals equal net principal tracked by the handler. - /// Exact because there is no epoch settlement in this suite (no warp). - /// Additive form avoids any underflow: positions + withdrawn == deposited. + /// INV-2: totals track net principal + settlement, up to engine-favoring + /// floor-dust (<=1 wei per mutating op). patch_prD_invariant_warp function invariant_totalsConserved() public view { - assertEq( - _sumAllPositions() + handler.ghostWithdrawn(), - handler.ghostDeposited(), - "post totals + withdrawn != deposited" - ); + int256 lhs = int256(_sumAllPositions() + handler.ghostWithdrawn()); + int256 rhs = int256(handler.ghostDeposited()) + handler.ghostSettleNet(); + assertLe(lhs, rhs, "totals + withdrawn exceed deposited + settled (engine leaked value)"); + assertLe(rhs - lhs, int256(handler.ghostOps()), "conservation gap exceeds 1-wei-per-op dust bound"); } function _sumAllPositions() internal view returns (uint256 sumPositions) { diff --git a/test/StakeEngineBucket.t.sol b/test/StakeEngineBucket.t.sol index 10625d3..5177ccb 100644 --- a/test/StakeEngineBucket.t.sol +++ b/test/StakeEngineBucket.t.sol @@ -124,8 +124,21 @@ contract StakeEngineBucketTest is Test { eng.updatePost(POST); } (uint256 s0, uint256 c0) = eng.getPostTotals(POST); - // engine must hold at least the winning-side claimable it minted toward - assertGe(vsp.balanceOf(address(eng)), 0); + // patch_prD_invariant_warp: the previous assertGe(balance, 0) was + // vacuous (uint >= 0 always holds). Real solvency: state is settled + // (updatePost ran at this timestamp, so totals are stored, not + // projected) and the engine must hold every wei of post totals AND + // every wei of per-staker claimable value. + assertGe(vsp.balanceOf(address(eng)), s0 + c0, "engine insolvent: balance < settled post totals"); + uint256 claimable; + for (uint256 i = 0; i < 100; i++) { + claimable += eng.getUserStake(address(uint160(0x4000 + i)), POST, 0); + } + for (uint256 i = 0; i < 50; i++) { + claimable += eng.getUserStake(address(uint160(0x5000 + i)), POST, 0); + } + claimable += eng.getUserStake(address(0x6001), POST, 1); + assertGe(vsp.balanceOf(address(eng)), claimable, "engine insolvent: balance < sum of claimables"); assertGt(s0 + c0, 0, "totals collapsed"); }