From 00975dec11a24b971a8cb7b2544226b0e986fd16 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 9 Oct 2024 15:45:52 +0200
Subject: [PATCH] chore(certora): add `accountMPGreaterEqualsAccountBalance`
 invariant

Closes #26
---
 certora/specs/RewardsStreamerMP.spec | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/certora/specs/RewardsStreamerMP.spec b/certora/specs/RewardsStreamerMP.spec
index 366cab2..cefbfc5 100644
--- a/certora/specs/RewardsStreamerMP.spec
+++ b/certora/specs/RewardsStreamerMP.spec
@@ -38,3 +38,6 @@ invariant sumOfBalancesIsTotalStaked()
 invariant accountMPLessEqualAccountMaxMP(address account)
   to_mathint(getAccountMP(account)) <= to_mathint(getAccountMaxMP(account));
 
+invariant accountMPGreaterEqualAccountStakedBalance(address account)
+  to_mathint(getAccountMP(account)) >= to_mathint(getAccountStakedBalance(account));
+