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.

Author: 0x-r4bbit

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)