Merge branch 'certora' into certora-stata-adaptation

.github/workflows/certora-stata.yml

@@ -3,10 +3,10 @@ name: certora-stata
 on:
   push:
     branches:
-      - main certora
+      - main
   pull_request:
     branches:
-      - main certora
+      - main
 
   workflow_dispatch:
 
@@ -28,7 +28,11 @@ 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: |
@@ -38,11 +42,11 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          cd certora
+          cd certora/stata
           touch applyHarness.patch
           make munged
-          cd ..
-          certoraRun certora/conf/${{ matrix.rule }}
+          cd ../..
+          certoraRun certora/stata/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -51,14 +55,14 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyERC4626.conf --rule previewRedeemIndependentOfBalance  previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
+          - verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
           - verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
           # Timeout
           # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
           - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
           - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
           - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
-          verifyERC4626Extended.conf --rule maxDepositConstant
+          - verifyERC4626Extended.conf --rule maxDepositConstant
           - verifyERC4626Extended.conf --rule redeemSum
           - verifyERC4626Extended.conf --rule redeemATokensSum
           - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf

certora/stata/conf/verifyAToken.conf

@@ -35,6 +35,6 @@
   "optimistic_loop": true,
   "solc": "solc8.20",
   "smt_timeout": "1400",
-  "verify": "StataTokenV2Harness:certora/stata/specs/staticATokenLM/aTokenProperties.spec",
+  "verify": "StataTokenV2Harness:certora/stata/specs/StataToken/aTokenProperties.spec",
   "build_cache": true,
 }

certora/stata/conf/verifyDoubleClaim.conf

@@ -29,7 +29,7 @@
      "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
      "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
 ],
-  "verify":"StataTokenV2Harness:certora/stata/specs/staticATokenLM/double_claim.spec",
+  "verify":"StataTokenV2Harness:certora/stata/specs/StataToken/double_claim.spec",
   "solc": "solc8.20",
   "msg": "Multi rewards - double claim properties",
   "optimistic_loop": true,

certora/stata/harness/rewards/TransferStrategyMultiRewardHarness.sol

@@ -0,0 +1,31 @@
+
+pragma solidity ^0.8.10;
+
+import {IERC20} from '../../munged/lib/aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol';
+import {TransferStrategyBase} from '../../munged/lib/aave-v3-periphery/contracts/rewards/transfer-strategies/TransferStrategyBase.sol';
+
+contract TransferStrategyMultiRewardHarness is TransferStrategyBase{
+
+constructor(address incentivesController, address rewardsAdmin) TransferStrategyBase(incentivesController, rewardsAdmin) {}
+
+    IERC20 public REWARD;
+    IERC20 public REWARD_B;
+
+    // executes the actual transfer of the rewards to the receiver
+    function performTransfer(
+        address to,
+        address reward,
+        uint256 amount
+    ) external override(TransferStrategyBase) returns (bool){
+
+        require(reward == address(REWARD) || reward == address(REWARD_B));
+
+        if (reward == address(REWARD)){
+            return REWARD.transfer(to, amount);
+        }
+        else if (reward == address(REWARD_B)){
+            return REWARD_B.transfer(to, amount);
+        }
+        return false;
+    }
+}

certora/stata/scripts/run-all.sh

@@ -92,4 +92,4 @@ certoraRun $CMN certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplica
 
 echo "******** Running: 22  ***************"
 certoraRun $CMN certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient \
---msg "22: "
+--msg "22: "

src/deployments/contracts/procedures/AaveV3HelpersProcedureTwo.sol

@@ -2,7 +2,8 @@
 pragma solidity ^0.8.0;
 
 import '../../interfaces/IMarketReportTypes.sol';
-import {TransparentProxyFactory, ITransparentProxyFactory} from 'solidity-utils/contracts/transparent-proxy/TransparentProxyFactory.sol';
+import {ITransparentProxyFactory} from 'solidity-utils/contracts/transparent-proxy/interfaces/ITransparentProxyFactory.sol';
+import {TransparentProxyFactory} from 'solidity-utils/contracts/transparent-proxy/TransparentProxyFactory.sol';
 import {StataTokenV2} from 'aave-v3-periphery/contracts/static-a-token/StataTokenV2.sol';
 import {StataTokenFactory} from 'aave-v3-periphery/contracts/static-a-token/StataTokenFactory.sol';
 import {IErrors} from '../../interfaces/IErrors.sol';

src/periphery/contracts/static-a-token/ERC4626StataTokenUpgradeable.sol

@@ -115,7 +115,7 @@ abstract contract ERC4626StataTokenUpgradeable is ERC4626Upgradeable, IERC4626St
   }
 
   ///@inheritdoc IERC4626StataToken
-  function aToken() external view returns (IERC20) {
+  function aToken() public view returns (IERC20) {
     ERC4626StataTokenStorage storage $ = _getERC4626StataTokenStorage();
     return $._aToken;
   }

src/periphery/contracts/static-a-token/StataTokenV2.sol

@@ -2,13 +2,17 @@
 pragma solidity ^0.8.0;
 
 import {ERC20Upgradeable, ERC20PermitUpgradeable} from 'openzeppelin-contracts-upgradeable/contracts/token/ERC20/extensions/ERC20PermitUpgradeable.sol';
+import {IERC20Metadata} from '@openzeppelin/contracts/token/ERC20/extensions/IERC20Metadata.sol';
 import {PausableUpgradeable} from 'openzeppelin-contracts-upgradeable/contracts/utils/PausableUpgradeable.sol';
-import {IRescuable, Rescuable} from 'solidity-utils/contracts/utils/Rescuable.sol';
+import {IPermissionlessRescuable, PermissionlessRescuable} from 'solidity-utils/contracts/utils/PermissionlessRescuable.sol';
+import {IRescuableBase, RescuableBase} from 'solidity-utils/contracts/utils/RescuableBase.sol';
+import {IERC20Permit} from '@openzeppelin/contracts/token/ERC20/extensions/IERC20Permit.sol';
 
 import {IACLManager} from '../../../core/contracts/interfaces/IACLManager.sol';
-import {ERC4626Upgradeable, ERC4626StataTokenUpgradeable, IPool} from './ERC4626StataTokenUpgradeable.sol';
+import {ERC4626Upgradeable, ERC4626StataTokenUpgradeable, IPool, Math, IERC20} from './ERC4626StataTokenUpgradeable.sol';
 import {ERC20AaveLMUpgradeable, IRewardsController} from './ERC20AaveLMUpgradeable.sol';
 import {IStataTokenV2} from './interfaces/IStataTokenV2.sol';
+import {IAToken} from './interfaces/IAToken.sol';
 
 /**
  * @title StataTokenV2
@@ -20,9 +24,11 @@ contract StataTokenV2 is
   ERC20AaveLMUpgradeable,
   ERC4626StataTokenUpgradeable,
   PausableUpgradeable,
-  Rescuable,
+  PermissionlessRescuable,
   IStataTokenV2
 {
+  using Math for uint256;
+
   constructor(
     IPool pool,
     IRewardsController rewardsController
@@ -53,17 +59,43 @@ contract StataTokenV2 is
     else _unpause();
   }
 
-  /// @inheritdoc IRescuable
-  function whoCanRescue() public view override returns (address) {
-    return POOL_ADDRESSES_PROVIDER.getACLAdmin();
+  /// @inheritdoc IPermissionlessRescuable
+  function whoShouldReceiveFunds() public view override returns (address) {
+    return IAToken(address(aToken())).RESERVE_TREASURY_ADDRESS();
+  }
+
+  /// @inheritdoc IRescuableBase
+  function maxRescue(
+    address asset
+  ) public view override(IRescuableBase, RescuableBase) returns (uint256) {
+    IERC20 cachedAToken = aToken();
+    if (asset == address(cachedAToken)) {
+      uint256 requiredBacking = _convertToAssets(totalSupply(), Math.Rounding.Ceil);
+      uint256 balance = cachedAToken.balanceOf(address(this));
+      return balance > requiredBacking ? balance - requiredBacking : 0;
+    }
+    return type(uint256).max;
   }
 
   ///@inheritdoc IStataTokenV2
   function canPause(address actor) public view returns (bool) {
     return IACLManager(POOL_ADDRESSES_PROVIDER.getACLManager()).isEmergencyAdmin(actor);
   }
 
-  function decimals() public view override(ERC20Upgradeable, ERC4626Upgradeable) returns (uint8) {
+  ///@inheritdoc IERC20Permit
+  function nonces(
+    address owner
+  ) public view virtual override(ERC20PermitUpgradeable, IERC20Permit) returns (uint256) {
+    return super.nonces(owner);
+  }
+
+  ///@inheritdoc IERC20Metadata
+  function decimals()
+    public
+    view
+    override(IERC20Metadata, ERC20Upgradeable, ERC4626Upgradeable)
+    returns (uint8)
+  {
     /// @notice The initialization of ERC4626Upgradeable already assures that decimal are
     /// the same as the underlying asset of the StataTokenV2, e.g. decimals of WETH for stataWETH
     return ERC4626Upgradeable.decimals();

src/periphery/contracts/static-a-token/interfaces/IAToken.sol

@@ -8,6 +8,8 @@ interface IAToken {
 
   function UNDERLYING_ASSET_ADDRESS() external view returns (address);
 
+  function RESERVE_TREASURY_ADDRESS() external view returns (address);
+
   /**
    * @notice Returns the scaled total supply of the scaled balance token. Represents sum(debt/index)
    * @return The scaled total supply

src/periphery/contracts/static-a-token/interfaces/IStataTokenV2.sol

@@ -3,8 +3,10 @@ pragma solidity ^0.8.0;
 
 import {IERC4626StataToken} from './IERC4626StataToken.sol';
 import {IERC20AaveLM} from './IERC20AaveLM.sol';
+import {IERC4626} from '@openzeppelin/contracts/interfaces/IERC4626.sol';
+import {IERC20Permit} from '@openzeppelin/contracts/token/ERC20/extensions/IERC20Permit.sol';
 
-interface IStataTokenV2 is IERC4626StataToken, IERC20AaveLM {
+interface IStataTokenV2 is IERC4626, IERC20Permit, IERC4626StataToken, IERC20AaveLM {
   /**
    * @notice Checks if the passed actor is permissioned emergency admin.
    * @param actor The reward to claim

tests/periphery/static-a-token/ERC4626StataTokenUpgradeable.t.sol

@@ -60,6 +60,10 @@ contract ERC4626StataTokenUpgradeableTest is TestnetProcedures {
     assertEq(erc4626Upgradeable.previewRedeem(shares), assets);
   }
 
+  function test_totalAssets_shouldbeZeroOnZeroSupply() external view {
+    assertEq(erc4626Upgradeable.totalAssets(), 0);
+  }
+
   // ### DEPOSIT TESTS ###
   function test_depositATokens(uint128 assets, address receiver) public {
     _validateReceiver(receiver);

tests/periphery/static-a-token/StataTokenV2Rescuable.sol

@@ -1,31 +1,37 @@
 // SPDX-License-Identifier: BUSL-1.1
 pragma solidity ^0.8.10;
 
-import {IRescuable} from 'solidity-utils/contracts/utils/Rescuable.sol';
+import {IAToken} from '../../../src/periphery/contracts/static-a-token/StataTokenV2.sol';
 import {BaseTest} from './TestBase.sol';
 
 contract StataTokenV2RescuableTest is BaseTest {
-  function test_whoCanRescue() external view {
-    assertEq(IRescuable(address(stataTokenV2)).whoCanRescue(), poolAdmin);
-  }
+  event ERC20Rescued(
+    address indexed caller,
+    address indexed token,
+    address indexed to,
+    uint256 amount
+  );
 
-  function test_rescuable_shouldRevertForInvalidCaller() external {
+  function test_rescuable_shouldTransferAssetsToCollector() external {
     deal(tokenList.usdx, address(stataTokenV2), 1 ether);
-    vm.expectRevert('ONLY_RESCUE_GUARDIAN');
-    IRescuable(address(stataTokenV2)).emergencyTokenTransfer(
-      tokenList.usdx,
-      address(this),
-      1 ether
-    );
+    stataTokenV2.emergencyTokenTransfer(tokenList.usdx, 1 ether);
   }
 
-  function test_rescuable_shouldSuceedForOwner() external {
-    deal(tokenList.usdx, address(stataTokenV2), 1 ether);
-    vm.startPrank(poolAdmin);
-    IRescuable(address(stataTokenV2)).emergencyTokenTransfer(
-      tokenList.usdx,
-      address(this),
-      1 ether
-    );
+  function test_rescuable_shouldWorkForAToken() external {
+    _fundAToken(1 ether, address(stataTokenV2));
+    stataTokenV2.emergencyTokenTransfer(aToken, 1 ether);
+  }
+
+  function test_rescuable_shouldNotCauseInsolvency(uint256 donation, uint256 stake) external {
+    vm.assume(donation != 0 && donation <= type(uint96).max);
+    vm.assume(stake != 0 && stake <= type(uint96).max);
+    _fundAToken(donation, address(stataTokenV2));
+    _fund4626(stake, address(this));
+
+    address treasury = IAToken(aToken).RESERVE_TREASURY_ADDRESS();
+
+    vm.expectEmit(true, true, true, true);
+    emit ERC20Rescued(address(this), aToken, treasury, donation);
+    stataTokenV2.emergencyTokenTransfer(aToken, donation + stake);
   }
 }

tests/periphery/static-a-token/TestBase.sol

@@ -3,7 +3,7 @@ pragma solidity ^0.8.10;
 
 import {IERC20Metadata, IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol';
 import {TransparentUpgradeableProxy} from 'solidity-utils/contracts/transparent-proxy/TransparentUpgradeableProxy.sol';
-import {ITransparentProxyFactory} from 'solidity-utils/contracts/transparent-proxy/TransparentProxyFactory.sol';
+import {ITransparentProxyFactory} from 'solidity-utils/contracts/transparent-proxy/interfaces/ITransparentProxyFactory.sol';
 import {StataTokenFactory} from '../../../src/periphery/contracts/static-a-token/StataTokenFactory.sol';
 import {StataTokenV2} from '../../../src/periphery/contracts/static-a-token/StataTokenV2.sol';
 import {IERC20AaveLM} from '../../../src/periphery/contracts/static-a-token/interfaces/IERC20AaveLM.sol';