Merge branch 'eigenpodupdates' of https://github.com/Layr-Labs/eigenl…

…ayer-contracts into eigenpodupdates
Layr-Labs · Aug 7, 2023 · dfda728 · dfda728
2 parents 4c8b360 + c679c2c
commit dfda728
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 435 deletions.
diff --git a/certora/harnesses/StrategyManagerHarness.sol b/certora/harnesses/StrategyManagerHarness.sol
@@ -41,6 +41,10 @@ contract StrategyManagerHarness is StrategyManager {
                 }
             }
 
+            if (strategies[i] == beaconChainETHStrategy) {
+                 //withdraw the beaconChainETH to the recipient
+                eigenPodManager.withdrawRestakedBeaconChainETH(slashedAddress, recipient, shareAmounts[i]);
+            }
             else {
                 // withdraw the shares and send funds to the recipient
                 strategies[i].withdraw(recipient, tokens[i], shareAmounts[i]);

diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec
@@ -103,10 +103,10 @@ definition methodCanIncreaseShares(method f) returns bool =
 * `queueWithdrawal`, `slashShares`, or `recordBeaconChainETHBalanceUpdate` has been called
 */
 definition methodCanDecreaseShares(method f) returns bool =
-    f.selector == queueWithdrawal(uint256[],address[],uint256[],address,bool).selector
-    || f.selector == slashShares(address,address,address[],address[],uint256[],uint256[]).selector
-    || f.selector == slashSharesSinglet(address,address,address,address,uint256,uint256).selector
-    || f.selector == recordBeaconChainETHBalanceUpdate(address,uint256,uint256, uint256).selector;
+    f.selector == sig:queueWithdrawal(uint256[],address[],uint256[],address,bool).selector
+    || f.selector == sig:slashShares(address,address,address[],address[],uint256[],uint256[]).selector
+    || f.selector == sig:slashSharesSinglet(address,address,address,address,uint256,uint256).selector
+    || f.selector == sig:recordBeaconChainETHBalanceUpdate(address,uint256,int256).selector;
 
 rule sharesAmountsChangeOnlyWhenAppropriateFunctionsCalled(address staker, address strategy) {
     uint256 sharesBefore = stakerStrategyShares(staker, strategy);