remove munged (#373)

Layr-Labs · Dec 15, 2023 · 134c3e8 · 134c3e8
1 parent ec4baff
commit 134c3e8
Show file tree

Hide file tree

Showing 18 changed files with 26 additions and 62 deletions.
diff --git a/certora/.gitignore b/certora/.gitignore
diff --git a/certora/Makefile b/certora/Makefile
diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
diff --git a/certora/harnesses/DelegationManagerHarness.sol b/certora/harnesses/DelegationManagerHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity =0.8.12;
 
-import "../munged/core/DelegationManager.sol";
+import "../../src/contracts/core/DelegationManager.sol";
 
 contract DelegationManagerHarness is DelegationManager {
 

diff --git a/certora/harnesses/EigenPodHarness.sol b/certora/harnesses/EigenPodHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity =0.8.12;
 
-import "../munged/pods/EigenPod.sol";
+import "../../src/contracts/pods/EigenPod.sol";
 
 contract EigenPodHarness is EigenPod {
 

diff --git a/certora/harnesses/EigenPodManagerHarness.sol b/certora/harnesses/EigenPodManagerHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity =0.8.12;
 
-import "../munged/pods/EigenPodManager.sol";
+import "../../src/contracts/pods/EigenPodManager.sol";
 
 contract EigenPodManagerHarness is EigenPodManager {
 

diff --git a/certora/harnesses/PausableHarness.sol b/certora/harnesses/PausableHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity =0.8.12;
 
-import "../munged/permissions/Pausable.sol";
+import "../../src/contracts/permissions/Pausable.sol";
 
 contract PausableHarness is Pausable {
     // getters

diff --git a/certora/harnesses/SlasherHarness.sol b/certora/harnesses/SlasherHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity =0.8.12;
 
-import "../munged/core/Slasher.sol";
+import "../../src/contracts/core/Slasher.sol";
 
 contract SlasherHarness is Slasher {
 

diff --git a/certora/harnesses/StrategyManagerHarness.sol b/certora/harnesses/StrategyManagerHarness.sol
@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity =0.8.12;
 
-import "../munged/core/StrategyManager.sol";
+import "../../src/contracts/core/StrategyManager.sol";
 
 contract StrategyManagerHarness is StrategyManager {
     constructor(IDelegationManager _delegation, IEigenPodManager _eigenPodManager, ISlasher _slasher)

diff --git a/certora/harnesses/StructuredLinkedListHarness.sol b/certora/harnesses/StructuredLinkedListHarness.sol
@@ -2,7 +2,7 @@
 
 pragma solidity ^0.8.0;
 
-import "../munged/libraries/StructuredLinkedList.sol";
+import "../../src/contracts/libraries/StructuredLinkedList.sol";
 
 /**
  * @title StructuredLinkedList

diff --git a/certora/harnesses/properties.md b/certora/harnesses/properties.md
diff --git a/certora/scripts/core/verifyDelegationManager.sh b/certora/scripts/core/verifyDelegationManager.sh
@@ -7,8 +7,8 @@ solc-select use 0.8.12
 
 certoraRun certora/harnesses/DelegationManagerHarness.sol \
     lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol \
-    certora/munged/pods/EigenPodManager.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 \
+    src/contracts/pods/EigenPodManager.sol src/contracts/pods/EigenPod.sol src/contracts/strategies/StrategyBase.sol src/contracts/core/StrategyManager.sol \
+    src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
     --verify DelegationManagerHarness:certora/specs/core/DelegationManager.spec \
     --optimistic_loop \
     --prover_args '-optimisticFallback true' \

diff --git a/certora/scripts/core/verifyStrategyManager.sh b/certora/scripts/core/verifyStrategyManager.sh
@@ -7,9 +7,9 @@ solc-select use 0.8.12
 
 certoraRun certora/harnesses/StrategyManagerHarness.sol \
     lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol \
-    certora/munged/pods/EigenPodManager.sol certora/munged/pods/EigenPod.sol certora/munged/pods/DelayedWithdrawalRouter.sol \
-    certora/munged/strategies/StrategyBase.sol certora/munged/core/DelegationManager.sol \
-    certora/munged/core/Slasher.sol certora/munged/permissions/PauserRegistry.sol \
+    src/contracts/pods/EigenPodManager.sol src/contracts/pods/EigenPod.sol src/contracts/pods/DelayedWithdrawalRouter.sol \
+    src/contracts/strategies/StrategyBase.sol src/contracts/core/DelegationManager.sol \
+    src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
     --verify StrategyManagerHarness:certora/specs/core/StrategyManager.spec \
     --optimistic_loop \
     --prover_args '-optimisticFallback true' \

diff --git a/certora/scripts/permissions/verifyPausable.sh b/certora/scripts/permissions/verifyPausable.sh
@@ -6,7 +6,7 @@ fi
 solc-select use 0.8.12
 
 certoraRun certora/harnesses/PausableHarness.sol \
-    certora/munged/permissions/PauserRegistry.sol \
+    src/contracts/permissions/PauserRegistry.sol \
     --verify PausableHarness:certora/specs/permissions/Pausable.spec \
     --optimistic_loop \
     --prover_args '-optimisticFallback true -recursionErrorAsAssert false -recursionEntryLimit 3' \

diff --git a/certora/scripts/pods/verifyEigenPod.sh b/certora/scripts/pods/verifyEigenPod.sh
@@ -6,10 +6,10 @@ fi
 solc-select use 0.8.12
 
 certoraRun certora/harnesses/EigenPodHarness.sol \
-    certora/munged/core/DelegationManager.sol certora/munged/pods/EigenPodManager.sol \
-    certora/munged/core/Slasher.sol certora/munged/permissions/PauserRegistry.sol \
-    certora/munged/core/StrategyManager.sol \
-    certora/munged/strategies/StrategyBase.sol \
+    src/contracts/core/DelegationManager.sol src/contracts/pods/EigenPodManager.sol \
+    src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
+    src/contracts/core/StrategyManager.sol \
+    src/contracts/strategies/StrategyBase.sol \
     lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol \
     lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol \
     --verify EigenPodHarness:certora/specs/pods/EigenPod.spec \

diff --git a/certora/scripts/pods/verifyEigenPodManager.sh b/certora/scripts/pods/verifyEigenPodManager.sh
@@ -6,8 +6,8 @@ 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 \
+    src/contracts/core/DelegationManager.sol src/contracts/pods/EigenPod.sol src/contracts/strategies/StrategyBase.sol src/contracts/core/StrategyManager.sol \
+    src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
     --verify EigenPodManagerHarness:certora/specs/pods/EigenPodManager.spec \
     --optimistic_loop \
     --prover_args '-optimisticFallback true' \

diff --git a/certora/scripts/strategies/verifyStrategyBase.sh b/certora/scripts/strategies/verifyStrategyBase.sh
@@ -5,11 +5,11 @@ fi
 
 solc-select use 0.8.12
 
-certoraRun certora/munged/strategies/StrategyBase.sol \
+certoraRun src/contracts/strategies/StrategyBase.sol \
     lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol \
-    certora/munged/core/StrategyManager.sol \
-    certora/munged/permissions/PauserRegistry.sol \
-    certora/munged/core/Slasher.sol \
+    src/contracts/core/StrategyManager.sol \
+    src/contracts/permissions/PauserRegistry.sol \
+    src/contracts/core/Slasher.sol \
     --verify StrategyBase:certora/specs/strategies/StrategyBase.spec \
     --optimistic_loop \
     --prover_args '-optimisticFallback true -recursionErrorAsAssert false -recursionEntryLimit 3' \

diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
@@ -54,9 +54,9 @@ methods {
     function get_stakerDelegateableShares(address,address) external returns (uint256) envfree;
 
     //envfree functions
-    function delegatedTo(address staker) external returns (address) envfree;
-    function operatorDetails(address operator) external returns (IDelegationManager.OperatorDetails memory) envfree;
-    function earningsReceiver(address operator) external returns (address) envfree;
+    function delegatedTo(address) external returns (address) envfree;
+    function operatorDetails(address) external returns (IDelegationManager.OperatorDetails memory) envfree;
+    function earningsReceiver(address) external returns (address) envfree;
     function delegationApprover(address operator) external returns (address) envfree;
     function stakerOptOutWindowBlocks(address operator) external returns (uint256) envfree;
     function operatorShares(address operator, address strategy) external returns (uint256) envfree;