From 1f712616be59c14e8c904ea49df0eb8ee0bf4ef8 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 `stakeSupply` ghost rule

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

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 79bef19..e0da6c9 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -1,6 +1,7 @@
 using ERC20A as staked;
 methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
+  function stakeSupply() external returns (uint256) envfree;
 }
 
 function isMigrationfunction(method f) returns bool {
@@ -15,6 +16,17 @@ function simplification() {
   require currentContract.migration == 0;
 }
 
+ghost mathint sumOfBalances /* sigma account[u].balance forall u */ {
+	init_state axiom sumOfBalances == 0;
+}
+
+hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
+invariant sumOfBalancesIsStakeSupply()
+      sumOfBalances == to_mathint(stakeSupply());
+
 
 rule reachability(method f)
 {