From 34abc6415499debda359366c8e036c07ef7a86ec Mon Sep 17 00:00:00 2001
From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com>
Date: Fri, 13 Oct 2023 11:19:27 -0700
Subject: [PATCH] deprecate broken rule and add a new one

Remove the `totalSharesGeqSumOfShares` invariant, since the way we are enforcing this is now split between the StrategyManager + DelegationManager (rather than being solely enforced by the StrategyManager). Add  a new `newSharesIncreaseTotalShares` rule in its place, which verifies the modified behavior around share changes, and in particular verifies that the StrategyManager still exhibits the same behavior as before, when considered in isolation of the DelegationManager (i.e. ignoring the new `removeShares` + `addShares` functions)
---
 certora/harnesses/StrategyManagerHarness.sol |  6 ++-
 certora/specs/core/StrategyManager.spec      | 43 ++++++++++----------
 2 files changed, 27 insertions(+), 22 deletions(-)

diff --git a/certora/harnesses/StrategyManagerHarness.sol b/certora/harnesses/StrategyManagerHarness.sol
index 73e5d9255..695dce119 100644
--- a/certora/harnesses/StrategyManagerHarness.sol
+++ b/certora/harnesses/StrategyManagerHarness.sol
@@ -49,6 +49,10 @@ contract StrategyManagerHarness is StrategyManager {
     }
 
     function totalShares(address strategy) public view returns (uint256) {
-        return  IStrategy(strategy).totalShares();
+        return IStrategy(strategy).totalShares();
+    }
+
+    function get_stakerStrategyShares(address staker, IStrategy strategy) public view returns (uint256) {
+        return stakerStrategyShares[staker][strategy];
     }
 }
\ No newline at end of file
diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec
index 3abbfaa07..9af8f8562 100644
--- a/certora/specs/core/StrategyManager.spec
+++ b/certora/specs/core/StrategyManager.spec
@@ -59,6 +59,7 @@ methods {
     function strategy_is_in_stakers_array(address, address) external returns (bool) envfree;
     function num_times_strategy_is_in_stakers_array(address, address) external returns (uint256) envfree;
     function totalShares(address) external returns (uint256) envfree;
+    function get_stakerStrategyShares(address, address) external returns (uint256) envfree;
 
 	//// Normal Functions
 	function stakerStrategyListLength(address) external returns (uint256) envfree;
@@ -113,29 +114,29 @@ rule sharesAmountsChangeOnlyWhenAppropriateFunctionsCalled(address staker, addre
     assert(sharesAfter < sharesBefore => methodCanDecreaseShares(f));
 }
 
-// based on Certora's example here https://github.com/Certora/Tutorials/blob/michael/ethcc/EthCC/Ghosts/ghostTest.spec
-ghost mapping(address => mathint) sumOfSharesInStrategy {
-  init_state axiom forall address strategy. sumOfSharesInStrategy[strategy] == 0;
-}
-
-hook Sstore stakerStrategyShares[KEY address staker][KEY address strategy] uint256 newValue (uint256 oldValue) STORAGE {
-    sumOfSharesInStrategy[strategy] = sumOfSharesInStrategy[strategy] + newValue - oldValue;
-}
-
 /**
-* Verifies that the `totalShares` returned by an Strategy is always greater than or equal to the sum of shares in the `stakerStrategyShares`
-* mapping -- specifically, that `strategy.totalShares() >= sum_over_all_stakers(stakerStrategyShares[staker][strategy])`
-* We cannot show strict equality here, since the withdrawal process first decreases a staker's shares (when `queueWithdrawal` is called) and
-* only later is `totalShares` decremented (when `completeQueuedWithdrawal` is called).
+* Verifies that the `totalShares` returned by an Strategy increases appropriately when new Strategy shares are issued by the StrategyManager
+* contract (specifically as a result of a call to `StrategyManager.depositIntoStrategy` or `StrategyManager.depositIntoStrategyWithSignature`).
+* This rule excludes the `addShares` and `removeShares` functions, since these are called only by the DelegationManager, and do not
+* "create new shares", but rather represent existing shares being "moved into a withdrawal".
 */
-invariant totalSharesGeqSumOfShares(address strategy)
-    to_mathint(totalShares(strategy)) >= sumOfSharesInStrategy[strategy]
-    // preserved block since does not apply for 'beaconChainETH'
-    { preserved {
-        // 0xbeaC0eeEeeeeEEeEeEEEEeeEEeEeeeEeeEEBEaC0 converted to decimal (this is the address of the virtual 'beaconChainETH' strategy)
-        // require strategy != beaconChainETHStrategy();
-        require strategy != 1088545275507480024404324736574744392984337050304;
-    } }
+rule newSharesIncreaseTotalShares(address strategy) {
+    method f;
+    env e;
+    uint256 stakerStrategySharesBefore = get_stakerStrategyShares(e.msg.sender, strategy);
+    uint256 totalSharesBefore = totalShares(strategy);
+    if (
+        f.selector == sig:addShares(address, address, uint256).selector
+        || f.selector == sig:removeShares(address, address, uint256).selector
+    ) {
+        uint256 totalSharesAfter = totalShares(strategy);
+        assert(totalSharesAfter == totalSharesBefore, "total shares changed unexpectedly");
+    } else {
+        uint256 stakerStrategySharesAfter = get_stakerStrategyShares(e.msg.sender, strategy);
+        uint256 totalSharesAfter = totalShares(strategy);
+        assert(stakerStrategySharesAfter - stakerStrategySharesBefore == totalSharesAfter - totalSharesBefore, "diffs don't match");
+    }
+}
 
 /**
  * Verifies that ERC20 tokens are transferred out of the account only of the msg.sender.