adapting spec to permissionless rescue

bgd-labs · Sep 10, 2024 · 51b20d1 · 51b20d1
1 parent 706f625
commit 51b20d1
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 21 deletions.
diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml
@@ -28,11 +28,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-<<<<<<< HEAD
-        run: pip install certora-cli==7.10.2
-=======
         run: pip install certora-cli==7.14.2
->>>>>>> certora
 
       - name: Install solc
         run: |

diff --git a/certora/stata/specs/StataToken/StataToken.spec b/certora/stata/specs/StataToken/StataToken.spec
@@ -102,7 +102,7 @@ import "../methods/methods_base.spec";
             f.contract == currentContract &&
             !harnessOnlyMethods(f) &&
             f.selector != sig:initialize(address, string, string).selector) &&
-            f.selector != sig:emergencyEtherTransfer(address,uint256).selector 
+            f.selector != sig:emergencyEtherTransfer(uint256).selector 
         } {
         // Assuming single reward
         single_RewardToken_setup();
@@ -123,8 +123,7 @@ import "../methods/methods_base.spec";
             (f.selector == sig:claimRewardsOnBehalf(address, address, address[]).selector) ||
             (f.selector == sig:claimRewards(address, address[]).selector) ||
             (f.selector == sig:claimRewardsToSelf(address[]).selector) ||
-            (f.selector == sig:claimSingleRewardOnBehalf(address,address,address).selector) || 
-            (f.selector == sig:emergencyTokenTransfer(address,address,uint256).selector)
+            (f.selector == sig:claimSingleRewardOnBehalf(address,address,address).selector)
         ), "Total rewards decline due to function other than claim or emergency rescue";
     }
 
@@ -137,8 +136,7 @@ import "../methods/methods_base.spec";
         && !harnessMethodsMinusHarnessClaimMethods(f) 
         && !claimFunctions(f)
         && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector
-        && f.selector != sig:emergencyTokenTransfer(address,address,uint256).selector
-        && f.selector != sig:emergencyEtherTransfer(address,uint256).selector
+        && f.selector != sig:emergencyEtherTransfer(uint256).selector
         }
             {
             preserved redeem(uint256 shares, address receiver, address owner) with (env e1) {
@@ -153,7 +151,9 @@ import "../methods/methods_base.spec";
                 requireInvariant solvency_total_asset_geq_total_supply();
                 require balanceOf(owner) <= totalSupply(); 
             }
-
+            preserved emergencyTokenTransfer(address asset, uint256 amount) with (env e3) {
+                require rate() >= RAY();
+            }
             }
 
 
@@ -169,8 +169,7 @@ import "../methods/methods_base.spec";
         f.contract == currentContract 
         && !harnessMethodsMinusHarnessClaimMethods(f)
         && !claimFunctions(f)
-        && f.selector != sig:emergencyEtherTransfer(address,uint256).selector
-        && f.selector != sig:emergencyTokenTransfer(address,address,uint256).selector
+        && f.selector != sig:emergencyEtherTransfer(uint256).selector
         && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector }
         {
             preserved withdraw(uint256 assets, address receiver, address owner)  with (env e3) {
@@ -198,6 +197,9 @@ import "../methods/methods_base.spec";
             preserved redeemATokens(uint256 shares, address receiver, address owner) with (env e2) {
                 require balanceOf(owner) <= totalSupply(); 
             }
+            preserved emergencyTokenTransfer(address asset, uint256 amount) with (env e1) {
+                require rate() >= RAY();
+            }
         }
 
         
@@ -213,7 +215,7 @@ import "../methods/methods_base.spec";
     => (_RewardsController.getUserAccruedReward(_asset, reward, user) == _RewardsController.getUserAccruedRewards(reward, user)))
     filtered {f ->
                 f.contract == currentContract &&
-                f.selector != sig:emergencyEtherTransfer(address,uint256).selector &&
+                f.selector != sig:emergencyEtherTransfer(uint256).selector &&
                 !harnessOnlyMethods(f) 
             } 
     {
@@ -253,7 +255,8 @@ import "../methods/methods_base.spec";
                     && !collectAndUpdateFunction(f)
                     && !harnessOnlyMethods(f)
                     && f.selector != sig:initialize(address,string,string).selector 
-                    && f.selector != sig:emergencyEtherTransfer(address,uint256).selector 
+                    && f.selector != sig:emergencyEtherTransfer(uint256).selector 
+                    && f.selector != sig:emergencyTokenTransfer(address,uint256).selector
                  }
         {
             env e;
@@ -282,8 +285,7 @@ import "../methods/methods_base.spec";
             mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward);
             f(e, args); 
             mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward);
-            assert  totalClaimableRewardsAfter == totalClaimableRewardsBefore ||
-                    f.selector == sig:emergencyTokenTransfer(address,address,uint256).selector;
+            assert  totalClaimableRewardsAfter == totalClaimableRewardsBefore;
         }
 
 
@@ -298,7 +300,7 @@ rule getClaimableRewards_stable(method f)
     && !claimFunctions(f)
     && !collectAndUpdateFunction(f)
     && f.selector != sig:initialize(address,string,string).selector
-    && f.selector != sig:emergencyEtherTransfer(address,uint256).selector
+    && f.selector != sig:emergencyEtherTransfer(uint256).selector
     && !harnessOnlyMethods(f)
     }
     {

diff --git a/certora/stata/specs/StataToken/aTokenProperties.spec b/certora/stata/specs/StataToken/aTokenProperties.spec
@@ -193,7 +193,7 @@ import "../methods/methods_base.spec";
         !f.isView &&
         f.selector != sig:redeem(uint256,address,address).selector &&
         f.selector != sig:redeemATokens(uint256,address,address).selector &&
-        f.selector != sig:emergencyEtherTransfer(address,uint256).selector &&
+        f.selector != sig:emergencyEtherTransfer(uint256).selector &&
         !harnessOnlyMethods(f)}
         {
             preserved with (env e){

diff --git a/certora/stata/specs/erc4626/erc4626Extended.spec b/certora/stata/specs/erc4626/erc4626Extended.spec
@@ -235,7 +235,7 @@ import "../methods/methods_base.spec";
         f.contract == currentContract &&
         !f.isView &&
         !harnessOnlyMethods(f) &&
-        f.selector != sig:emergencyEtherTransfer(address,uint256).selector &&
+        f.selector != sig:emergencyEtherTransfer(uint256).selector &&
         f.selector != sig:deposit(uint256,address).selector &&
         f.selector != sig:depositWithPermit(uint256,address,uint256,IERC4626StataToken.SignatureParams,bool).selector &&
         f.selector != sig:withdraw(uint256,address,address).selector &&

diff --git a/certora/stata/specs/methods/methods_base.spec b/certora/stata/specs/methods/methods_base.spec
@@ -48,7 +48,7 @@ using DummyERC20_rewardToken as _DummyERC20_rewardToken;
             // In RewardsDistributor.sol called by RewardsController.sol
             function _.getAssetIndex(address, address) external=> DISPATCHER(true);
             // In ScaledBalanceTokenBase.sol called by getAssetIndex
-            function _.scaledTotalSupply() external  => DISPATCHER(true);
+            function _.scaledTotalSupply() external => DISPATCHER(true);
             // Called by RewardsController._transferRewards()
             // Defined in TransferStrategyHarness as simple transfer() 
             function _.performTransfer(address,address,uint256) external  =>  DISPATCHER(true);
@@ -78,6 +78,7 @@ using DummyERC20_rewardToken as _DummyERC20_rewardToken;
             function _AToken.totalSupply() external returns (uint256) envfree;
             function _AToken.allowance(address, address) external returns (uint256) envfree;
             function _AToken.UNDERLYING_ASSET_ADDRESS() external returns (address) envfree;
+            function _.RESERVE_TREASURY_ADDRESS() external => CONSTANT;
             function _AToken.scaledBalanceOf(address) external returns (uint256) envfree;
             function _AToken.scaledTotalSupply() external returns (uint256) envfree;
 
@@ -142,7 +143,7 @@ using DummyERC20_rewardToken as _DummyERC20_rewardToken;
 
 
 ////////////////// FUNCTIONS //////////////////////
-
+    
     /**
     * @title Single reward setup
     * Setup the `StaticATokenLM`'s rewards so they contain a single reward token