From df0257c343722fa595d754982649f25d2938b7a4 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Thu, 7 Nov 2024 10:50:13 -0300
Subject: [PATCH] fix(certora): exclude `stake()` from rule that checks account
 balance change

The rule is failing since we've removed the `lockUntil > 0` check in
`stake` and `processAccount` is no longer used in `stake()`.
The rule requires `lockUntil > 0` so it will always fail there and can't
find a non-reverting cases (which makes the rule pass).

The reason it hasn't happened before was because:

The rule required account.lockUntil > 0
Stake required lockUntil > 0 || account balance == 0

Also this commit adds an invariant:

add invariant that account balance == 0 => accountMP == 0
---
 certora/specs/StakeManager.spec | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index e99dc6f..075cd7c 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -94,8 +94,14 @@ invariant highEpochsAreNull(uint256 epochNumber)
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
 
-invariant accountBonusMPIsZeroIfBalanceIsZero(address addr)
-  to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountBonusMultiplierPoints(addr)) == 0
+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 {
     f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
   }