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

@@ -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;
 

certora/specs/StakeManagerProcessAccount.spec

@@ -36,7 +36,7 @@ hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValu
   https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8
 */
 rule checkAccountProcessedBeforeStoring(method f) filtered {
-  f -> !requiresPreviousManager(f) && !requiresNextManager(f)
+  f -> !requiresPreviousManager(f) && !requiresNextManager(f) && f.selector != sig:stake(uint256,uint256).selector
 } {
   address account;