fix(specs): make sumOfMultiplierPointsIsMultiplierpoints work again

This invariant failed as the prover started making wrong assumptions
about the relationship between anyone's account's `totalMP` and its
`balance`, as well as an account's `bonusMP` and its `balance`.

This commit fixes it by adding the necessary invariants to proof the
property.

certora/specs/StakeManager.spec

@@ -75,6 +75,11 @@ invariant sumOfMultipliersIsMultiplierSupply()
   filtered {
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
+  { preserved with (env e){
+    requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender);
+    requireInvariant accountBonusMPIsZeroIfBalanceIsZero(e.msg.sender);
+    }
+  }
 
 invariant sumOfEpochRewardsIsPendingRewards()
   sumOfEpochRewards == to_mathint(currentContract.pendingReward)
@@ -89,6 +94,12 @@ invariant highEpochsAreNull(uint256 epochNumber)
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
 
+invariant accountBonusMPIsZeroIfBalanceIsZero(address addr)
+  to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountBonusMultiplierPoints(addr)) == 0
+  filtered {
+    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
+  }
+
 invariant accountMPIsZeroIfBalanceIsZero(address addr)
   to_mathint(getAccountBalance(addr)) == 0 => to_mathint(getAccountCurrentMultiplierPoints(addr)) == 0
   filtered {