chore(specs): add invariant that account balance == 0 => accountMP == 0

logos-co · Sep 27, 2024 · ff243e7 · ff243e7
1 parent 44b4476
commit ff243e7
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
@@ -85,6 +85,12 @@ invariant highEpochsAreNull(uint256 epochNumber)
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
 
+invariant accountMPIsZeroIfBalanceIsZero(address addr)
+  to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0
+  filtered {
+    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
+  }
+
 invariant InitialMPIsNeverSmallerThanBalance(address addr)
   to_mathint(getAccountBonusMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
   filtered {
@@ -126,6 +132,7 @@ rule stakingMintsMultiplierPoints1To1Ratio {
 
   requireInvariant InitialMPIsNeverSmallerThanBalance(e.msg.sender);
   requireInvariant CurrentMPIsNeverSmallerThanInitialMP(e.msg.sender);
+  requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
 
   require getAccountLockUntil(e.msg.sender) <= e.block.timestamp;