test: formally verify that MPs only decrease when unstaking/leaving

vacp2p · Dec 5, 2024 · c041d5d · c041d5d
1 parent be89292
commit c041d5d
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/certora/specs/RewardsStreamerMP.spec b/certora/specs/RewardsStreamerMP.spec
@@ -109,3 +109,15 @@ rule stakingGreaterLockupTimeMeansGreaterMPs {
   assert lockupTime1 >= lockupTime2 => to_mathint(multiplierPointsAfter1) >= to_mathint(multiplierPointsAfter2);
   satisfy to_mathint(multiplierPointsAfter1) > to_mathint(multiplierPointsAfter2);
 }
+
+
+rule MPsOnlyDecreaseWhenUnstaking(method f) filtered { f -> f.selector != sig:upgradeToAndCall(address,bytes).selector } {
+  env e;
+  calldataarg args;
+
+  uint256 totalMPBefore = totalMP(e);
+  f(e, args);
+  uint256 totalMPAfter = totalMP(e);
+
+  assert totalMPAfter < totalMPBefore => f.selector == sig:unstake(uint256).selector || f.selector == sig:leave().selector;
+}