From f8d52e27e12e43b0a02763b0783c44a52979ee14 Mon Sep 17 00:00:00 2001
From: Ricardo Guilherme Schmidt <3esmit@gmail.com>
Date: Thu, 3 Oct 2024 00:24:12 -0300
Subject: [PATCH] chore(StakeManager.spec): fix spec to don't load totalMP
 greater than current sumOfMultipliers

---
 certora/specs/StakeManager.spec | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 227bb0f..350ac9f 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -60,6 +60,10 @@ hook Sstore accounts[KEY address addr].totalMP uint256 newValue (uint256 oldValu
     sumOfMultipliers = sumOfMultipliers - oldValue + newValue;
 }
 
+hook Sload uint256 newValue accounts[KEY address addr].totalMP {
+    require sumOfBalances >= to_mathint(newValue);
+}
+
 invariant sumOfBalancesIsTotalSupplyBalance()
   sumOfBalances == to_mathint(totalSupplyBalance())
   filtered {