From c0bf36d14bf1ff4752c28e54ef31ee7d304d6204 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Thu, 3 Oct 2024 00:24:13 -0300
Subject: [PATCH] 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 | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 416c5a8..e99dc6f 100644
--- a/certora/specs/StakeManager.spec
+++ b/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)