chore(StakeManager.spec): fix spec to don't load totalMP greater than…

… current sumOfMultipliers
logos-co · Sep 28, 2024 · fefc4dc · fefc4dc
1 parent 41b4362
commit fefc4dc
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
@@ -60,6 +60,10 @@ hook Sstore accounts[KEY address addr].totalMP uint256 newValue (uint256 oldValu
     sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
 }
 
+hook Sload uint256 newValue accounts[KEY address addr].totalMP {
+    require sumOfBalances >= to_mathint(newValue);
+}
+
 invariant sumOfBalancesIsTotalSupplyBalance()
   sumOfBalances == to_mathint(totalSupplyBalance())
   filtered {