chore(certora): add accountMPGreaterEqualsAccountBalance invariant

Closes #26
vacp2p · Oct 16, 2024 · 00975de · 00975de
1 parent 59f2566
commit 00975de
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/certora/specs/RewardsStreamerMP.spec b/certora/specs/RewardsStreamerMP.spec
@@ -38,3 +38,6 @@ invariant sumOfBalancesIsTotalStaked()
 invariant accountMPLessEqualAccountMaxMP(address account)
   to_mathint(getAccountMP(account)) <= to_mathint(getAccountMaxMP(account));
 
+invariant accountMPGreaterEqualAccountStakedBalance(address account)
+  to_mathint(getAccountMP(account)) >= to_mathint(getAccountStakedBalance(account));
+