From e1bd0f31f8e04a3297efc9edf229f297308ade34 Mon Sep 17 00:00:00 2001
From: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
Date: Wed, 24 Jan 2024 12:16:01 +0100
Subject: [PATCH] chore: add cerora rules for `totalSupplyBalance` ghost rule

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

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 819b13b..c1ab2b3 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -42,15 +42,15 @@ ghost mathint sumOfEpochRewards
   init_state axiom sumOfEpochRewards == 0;
 }
 
-ghost mathint sumOfBalances { /* sigma account[u].balance forall u */
-	init_state axiom sumOfBalances == 0;
-}
-
 ghost mathint sumOfMultipliers /* sigma account[u].multiplier forall u */
 {
 	init_state axiom sumOfMultipliers == 0;
 }
 
+ghost mathint sumOfBalances /* sigma account[u].balance forall u */ {
+	init_state axiom sumOfBalances == 0;
+}
+
 hook Sstore epochs[KEY uint256 epochId].epochReward uint256 newValue (uint256 oldValue) STORAGE {
   sumOfEpochRewards = sumOfEpochRewards - oldValue + newValue;
 }
@@ -83,7 +83,6 @@ invariant sumOfEpochRewardsIsPendingRewards()
 invariant highEpochsAreNull(uint256 epochNumber)
   epochNumber >= currentContract.currentEpoch => currentContract.epochs[epochNumber].epochReward == 0;
 
-
 rule reachability(method f)
 {
   calldataarg args;