get tests working

Layr-Labs · Oct 13, 2023 · 8a799ea · 8a799ea
2 parents 49db581 + 3c683e7
commit 8a799ea
Show file tree

Hide file tree

Showing 77 changed files with 6,575 additions and 4,324 deletions.
diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml
@@ -38,10 +38,10 @@ jobs:
           python-version: '3.10'
           cache: 'pip'
       - name: Install java
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v2
         with:
-          java-version: '11'
-          java-package: 'jre'
+          distribution: temurin
+          java-version: '17'
       - name: Install certora
         run: pip install certora-cli
       - name: Install solc

diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
@@ -1,20 +0,0 @@
-diff -druN ../score/DelegationManager.sol core/DelegationManager.sol
---- ../score/DelegationManager.sol	2023-09-26 13:12:35
-+++ core/DelegationManager.sol	2023-09-26 13:40:04
-@@ -307,10 +307,12 @@
-      * @dev Callable only by the StrategyManager or EigenPodManager.
-      */
-     function decreaseDelegatedShares(
--        address staker,
--        IStrategy[] calldata strategies,
--        uint256[] calldata shares
--    ) external onlyStrategyManagerOrEigenPodManager {
-+        address staker, 
-+        // MUNGED calldata => memory
-+        IStrategy[] memory strategies,
-+        uint256[] memory shares
-+        // MUNGED external => public
-+    ) public onlyStrategyManagerOrEigenPodManager {
-         // if the staker is delegated to an operator
-         if (isDelegated(staker)) {
-             address operator = delegatedTo[staker];

diff --git a/certora/harnesses/DelegationManagerHarness.sol b/certora/harnesses/DelegationManagerHarness.sol
@@ -8,25 +8,21 @@ contract DelegationManagerHarness is DelegationManager {
     constructor(IStrategyManager _strategyManager, ISlasher _slasher, IEigenPodManager _eigenPodManager)
         DelegationManager(_strategyManager, _slasher, _eigenPodManager) {}
 
-
-    /// Harnessed functions
-    function decreaseDelegatedShares(
-        address staker,
-        IStrategy strategy1,
-        IStrategy strategy2,
-        uint256 share1,
-        uint256 share2
-        ) external {
-            IStrategy[] memory strategies = new IStrategy[](2);
-            uint256[] memory shares = new uint256[](2);
-            strategies[0] = strategy1;
-            strategies[1] = strategy2;
-            shares[0] = share1;
-            shares[1] = share2;
-            super.decreaseDelegatedShares(staker, strategies, shares);
+    function get_operatorShares(address operator, IStrategy strategy) public view returns (uint256) {
+        return operatorShares[operator][strategy];
     }
 
-    function get_operatorShares(address operator, IStrategy strategy) public view returns(uint256) {
-        return operatorShares[operator][strategy];
+    function get_stakerDelegateableShares(address staker, IStrategy strategy) public view returns (uint256) {
+        // this is the address of the virtual 'beaconChainETH' strategy
+        if (address(strategy) == 0xbeaC0eeEeeeeEEeEeEEEEeeEEeEeeeEeeEEBEaC0) {
+            int256 beaconChainETHShares = eigenPodManager.podOwnerShares(staker);
+            if (beaconChainETHShares <= 0) {
+                return 0;
+            } else {
+                return uint256(beaconChainETHShares);
+            }
+        } else {
+            return strategyManager.stakerStrategyShares(staker, strategy);
+        }
     }
 }
diff --git a/certora/harnesses/EigenPodManagerHarness.sol b/certora/harnesses/EigenPodManagerHarness.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity =0.8.12;
+
+import "../munged/pods/EigenPodManager.sol";
+
+contract EigenPodManagerHarness is EigenPodManager {
+
+    constructor(
+        IETHPOSDeposit _ethPOS,
+        IBeacon _eigenPodBeacon,
+        IStrategyManager _strategyManager,
+        ISlasher _slasher,
+        IDelegationManager _delegationManager
+    )
+        EigenPodManager(_ethPOS, _eigenPodBeacon, _strategyManager, _slasher, _delegationManager) {}
+
+    function get_podOwnerShares(address podOwner) public view returns (int256) {
+        return podOwnerShares[podOwner];
+    }
+}
diff --git 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];
     }
 }
diff --git a/certora/scripts/core/verifyDelegationManager.sh b/certora/scripts/core/verifyDelegationManager.sh
@@ -14,6 +14,6 @@ certoraRun certora/harnesses/DelegationManagerHarness.sol \
     --prover_args '-optimisticFallback true' \
     --optimistic_hashing \
     $RULE \
-    --loop_iter 3 \
+    --loop_iter 2 \
     --packages @openzeppelin=lib/openzeppelin-contracts @openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable \
     --msg "DelegationManager $1 $2" \
diff --git a/certora/scripts/pods/verifyEigenPodManager.sh b/certora/scripts/pods/verifyEigenPodManager.sh
@@ -0,0 +1,18 @@
+if [[ "$2" ]]
+then
+    RULE="--rule $2"
+fi
+
+solc-select use 0.8.12
+
+certoraRun certora/harnesses/EigenPodManagerHarness.sol \
+    certora/munged/core/DelegationManager.sol certora/munged/pods/EigenPod.sol certora/munged/strategies/StrategyBase.sol certora/munged/core/StrategyManager.sol \
+    certora/munged/core/Slasher.sol certora/munged/permissions/PauserRegistry.sol \
+    --verify EigenPodManagerHarness:certora/specs/pods/EigenPodManager.spec \
+    --optimistic_loop \
+    --prover_args '-optimisticFallback true' \
+    --optimistic_hashing \
+    $RULE \
+    --loop_iter 3 \
+    --packages @openzeppelin=lib/openzeppelin-contracts @openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable \
+    --msg "EigenPodManager $1 $2" \
diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
@@ -3,7 +3,7 @@ methods {
     //// External Calls
 	// external calls to DelegationManager 
     function undelegate(address) external;
-    function decreaseDelegatedShares(address,address[],uint256[]) external;
+    function decreaseDelegatedShares(address,address,uint256) external;
 	function increaseDelegatedShares(address,address,uint256) external;
 
 	// external calls to Slasher
@@ -13,32 +13,42 @@ methods {
 	// external calls to StrategyManager
     function _.getDeposits(address) external => DISPATCHER(true);
     function _.slasher() external => DISPATCHER(true);
-	function _.deposit(address,uint256) external => DISPATCHER(true);
-	function _.withdraw(address,address,uint256) external => DISPATCHER(true);
-	function _.stakerStrategyListLength(address) external => DISPATCHER(true);
-    function _.forceTotalWithdrawal(address staker) external => DISPATCHER(true);
+    function _.addShares(address,address,uint256) external => DISPATCHER(true);
+    function _.removeShares(address,address,uint256) external => DISPATCHER(true);
+    function _.withdrawSharesAsTokens(address, address, uint256, address) external => DISPATCHER(true);
 
 	// external calls to EigenPodManager
-	function _.withdrawRestakedBeaconChainETH(address,address,uint256) external => DISPATCHER(true);
-	function _.podOwnerHasActiveShares(address) external => DISPATCHER(true);
-    function _.forceIntoUndelegationLimbo(address podOwner, address delegatedTo) external => DISPATCHER(true);
+    function _.addShares(address,uint256) external => DISPATCHER(true);
+    function _.removeShares(address,uint256) external => DISPATCHER(true);
+    function _.withdrawSharesAsTokens(address, address, uint256) external => DISPATCHER(true);
 
     // external calls to EigenPod
 	function _.withdrawRestakedBeaconChainETH(address,uint256) external => DISPATCHER(true);
 
+    // external calls to DelayedWithdrawalRouter (from EigenPod)
+    function _.createDelayedWithdrawal(address, address) external => DISPATCHER(true);
+
     // external calls to PauserRegistry
     function _.isPauser(address) external => DISPATCHER(true);
 	function _.unpauser() external => DISPATCHER(true);
 
+    // external calls to Strategy contracts
+    function _.withdraw(address,address,uint256) external => DISPATCHER(true);
+    function _.deposit(address,uint256) external => DISPATCHER(true);
+
+    // external calls to ERC20
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
+    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
+
     // external calls to ERC1271 (can import OpenZeppelin mock implementation)
     // isValidSignature(bytes32 hash, bytes memory signature) returns (bytes4 magicValue) => DISPATCHER(true)
     function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true);
 
     //// Harnessed Functions
-    // Harnessed calls
-    function decreaseDelegatedShares(address,address,address,uint256,uint256) external;
-    // Harmessed getters
+    // Harnessed getters
     function get_operatorShares(address,address) external returns (uint256) envfree;
+    function get_stakerDelegateableShares(address,address) external returns (uint256) envfree;
 
     //envfree functions
     function delegatedTo(address staker) external returns (address) envfree;
@@ -204,6 +214,47 @@ rule canOnlyDelegateWithSpecificFunctions(address staker) {
     }
 }
 
+rule sharesBecomeDelegatedWhenStakerDelegates(address operator, address staker, address strategy) {
+    requireInvariant operatorsAlwaysDelegatedToSelf(operator);
+    // filter out zero address (not a valid operator)
+    require(operator != 0);
+    // assume the staker begins as undelegated
+    require(!isDelegated(staker));
+    mathint stakerDelegateableSharesInStrategy = get_stakerDelegateableShares(staker, strategy);
+    mathint operatorSharesBefore = get_operatorShares(operator, strategy);
+    // perform arbitrary function call
+    method f;
+    env e;
+    calldataarg arg;
+    mathint operatorSharesAfter = get_operatorShares(operator, strategy);
+    if (delegatedTo(staker) == operator) {
+        assert(operatorSharesAfter == operatorSharesBefore + stakerDelegateableSharesInStrategy, "operator shares did not increase appropriately");
+    } else {
+        assert(operatorSharesAfter == operatorSharesBefore, "operator shares changed inappropriately");
+    }
+}
+
+rule sharesBecomeUndelegatedWhenStakerUndelegates(address operator, address staker, address strategy) {
+    requireInvariant operatorsAlwaysDelegatedToSelf(operator);
+    // filter out zero address (not a valid operator)
+    require(operator != 0);
+    // assume the staker begins as delegated to the operator
+    require(delegatedTo(staker) == operator);
+    mathint stakerDelegateableSharesInStrategy = get_stakerDelegateableShares(staker, strategy);
+    mathint operatorSharesBefore = get_operatorShares(operator, strategy);
+    // perform arbitrary function call
+    method f;
+    env e;
+    calldataarg arg;
+    mathint operatorSharesAfter = get_operatorShares(operator, strategy);
+    if (!isDelegated(staker)) {
+        assert(operatorSharesAfter == operatorSharesBefore - stakerDelegateableSharesInStrategy, "operator shares did not decrease appropriately");
+    } else {
+        assert(operatorSharesAfter == operatorSharesBefore, "operator shares changed inappropriately");
+    }
+}
+
+
 /*
 rule batchEquivalence {
     env e;

diff --git a/certora/specs/core/Slasher.spec b/certora/specs/core/Slasher.spec
@@ -5,7 +5,7 @@ methods {
     function _.undelegate(address) external => DISPATCHER(true);
     function _.isDelegated(address) external => DISPATCHER(true);
     function _.delegatedTo(address) external => DISPATCHER(true);
-	function _.decreaseDelegatedShares(address,address[],uint256[]) external => DISPATCHER(true);
+	function _.decreaseDelegatedShares(address,address,uint256) external => DISPATCHER(true);
 	function _.increaseDelegatedShares(address,address,uint256) external => DISPATCHER(true);
 
 	// external calls to Slasher
@@ -15,15 +15,21 @@ methods {
 	// external calls to StrategyManager
     function _.getDeposits(address) external => DISPATCHER(true);
     function _.slasher() external => DISPATCHER(true);
-	function _.deposit(address,uint256) external => DISPATCHER(true);
-	function _.withdraw(address,address,uint256) external => DISPATCHER(true);
+    function _.addShares(address,address,uint256) external => DISPATCHER(true);
+    function _.removeShares(address,address,uint256) external => DISPATCHER(true);
+    function _.withdrawSharesAsTokens(address, address, uint256, address) external => DISPATCHER(true);
 
 	// external calls to EigenPodManager
-	function _.withdrawRestakedBeaconChainETH(address,address,uint256) external => DISPATCHER(true);
-
+    function _.addShares(address,uint256) external => DISPATCHER(true);
+    function _.removeShares(address,uint256) external => DISPATCHER(true);
+    function _.withdrawSharesAsTokens(address, address, uint256) external => DISPATCHER(true);
+
     // external calls to EigenPod
 	function _.withdrawRestakedBeaconChainETH(address,uint256) external => DISPATCHER(true);
-
+
+    // external calls to DelayedWithdrawalRouter (from EigenPod)
+    function _.createDelayedWithdrawal(address, address) external => DISPATCHER(true);
+
     // external calls to PauserRegistry
     function _.isPauser(address) external => DISPATCHER(true);
 	function _.unpauser() external => DISPATCHER(true);