From f1c1de7993068712e00a89d66b5cae1c3416e302 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 11 Mar 2024 15:34:15 +0100
Subject: [PATCH] chore(StakeManager.spec): add two more MP related invariants

This adds two more invariants about multiplier points:

1. Initial multiplier points can never be less than an account's balance
2. Current multiplier points can never be less than initial MP
---
 certora/specs/StakeManager.spec | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 4c6bd58..255bc5b 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -113,14 +113,26 @@ invariant highEpochsAreNull(uint256 epochNumber)
     m -> !requiresPreviousManager(m) && !requiresNextManager(m)
   }
 
+invariant InitialMPIsNeverSmallerThanBalance(address addr)
+  to_mathint(getAccountInitialMultiplierPoints(addr)) >= to_mathint(getAccountBalance(addr))
+  filtered {
+    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
+  }
+
+invariant CurrentMPIsNeverSmallerThanInitialMP(address addr)
+  to_mathint(getAccountCurrentMultiplierPoints(addr)) >= to_mathint(getAccountInitialMultiplierPoints(addr))
+  filtered {
+    f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
+  }
+
 invariant MPcantBeGreaterThanMaxMP(address addr)
   to_mathint(getAccountCurrentMultiplierPoints(addr)) <= (getAccountBalance(addr) * 8) + getAccountInitialMultiplierPoints(addr)
   filtered {
     f -> f.selector != sig:migrateFrom(address,bool,StakeManager.Account).selector
   }
   { preserved {
-      require getAccountInitialMultiplierPoints(addr) >= getAccountBalance(addr);
-      require getAccountCurrentMultiplierPoints(addr) >= getAccountInitialMultiplierPoints(addr);
+      requireInvariant InitialMPIsNeverSmallerThanBalance(addr);
+      requireInvariant CurrentMPIsNeverSmallerThanInitialMP(addr);
     }
   }