chore: fix certora errors

Cryptobroker01 · Aug 3, 2024 · 3c2f857 · 3c2f857
1 parent 0e59845
commit 3c2f857
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 14 deletions.
diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile
@@ -4,4 +4,5 @@ FROM mcr.microsoft.com/vscode/devcontainers/base:0-${VARIANT}
 
 # [Optional] Uncomment this section to install additional OS packages.
 RUN apt-get update && export DEBIAN_FRONTEND=noninteractive \
-    && apt-get -y install --no-install-recommends libssl-dev ripgrep
+    && apt-get -y install --no-install-recommends libssl-dev \
+    ripgrep python3-pip python3-venv python3
diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
@@ -16,7 +16,6 @@ methods {
 	// external calls to StrategyManager
     function _.getDeposits(address) external => DISPATCHER(true);
     function _.slasher() 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);
 
@@ -28,9 +27,6 @@ methods {
 
     // 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);
@@ -285,7 +281,7 @@ rule withdrawalDelayIsEnforced() {
     uint256 middlewareTimesIndex;
     bool receiveAsTokens;
     env e;
-    completeQueuedWithdrawal(e, queuedWithdrawal, tokens, middlewareTimesIndex, receiveAsTokens);
+    completeQueuedWithdrawal@withrevert(e, queuedWithdrawal, tokens, middlewareTimesIndex, receiveAsTokens);
     bool callReverted = lastReverted;
     assert(
         callReverted

diff --git a/certora/specs/pods/EigenPod.spec b/certora/specs/pods/EigenPod.spec
@@ -30,7 +30,6 @@ methods {
 	// external calls to StrategyManager
     function _.getDeposits(address) external => DISPATCHER(true);
     function _.slasher() 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);
 
@@ -52,9 +51,6 @@ methods {
     // external calls to ETH2Deposit contract
     function _.deposit(bytes, bytes, bytes, bytes32) external => NONDET;
 
-    // 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);

diff --git a/certora/specs/pods/EigenPodManager.spec b/certora/specs/pods/EigenPodManager.spec
@@ -16,7 +16,6 @@ methods {
 	// external calls to StrategyManager
     function _.getDeposits(address) external => DISPATCHER(true);
     function _.slasher() 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);
 
@@ -28,9 +27,6 @@ methods {
     // 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);