closing pool-solvency work before moving to public repo

Certora · Dec 12, 2024 · 28d1cde · 28d1cde
1 parent 56363df
commit 28d1cde
Showing 1 changed file with 87 additions and 16 deletions.
diff --git a/certora/solvency/applyHarness.patch b/certora/solvency/applyHarness.patch
@@ -1,13 +1,50 @@
 diff -ruN .gitignore .gitignore
 --- .gitignore	1970-01-01 02:00:00.000000000 +0200
-+++ .gitignore	2024-11-28 09:37:40.688170748 +0200
++++ .gitignore	2024-12-01 11:47:54.000000000 +0200
 @@ -0,0 +1,2 @@
 +*
 +!.gitignore
 \ No newline at end of file
+diff -ruN src/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol src/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol
+--- src/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol	2024-12-12 12:17:18.477210656 +0200
++++ src/contracts/dependencies/gnosis/contracts/GPv2SafeERC20.sol	2024-12-01 11:47:54.000000000 +0200
+@@ -10,6 +10,8 @@
+   /// @dev Wrapper around a call to the ERC20 function `transfer` that reverts
+   /// also when the token returns `false`.
+   function safeTransfer(IERC20 token, address to, uint256 value) internal {
++    require(token.transfer(to,value));
++    /*
+     bytes4 selector_ = token.transfer.selector;
+
+     // solhint-disable-next-line no-inline-assembly
+@@ -24,6 +26,7 @@
+         revert(0, returndatasize())
+       }
+     }
++    */
+
+     require(getLastTransferResult(token), 'GPv2: failed transfer');
+   }
+@@ -31,6 +34,8 @@
+   /// @dev Wrapper around a call to the ERC20 function `transferFrom` that
+   /// reverts also when the token returns `false`.
+   function safeTransferFrom(IERC20 token, address from, address to, uint256 value) internal {
++    require(token.transferFrom(from,to,value));
++    /*
+     bytes4 selector_ = token.transferFrom.selector;
+
+     // solhint-disable-next-line no-inline-assembly
+@@ -48,6 +53,7 @@
+     }
+
+     require(getLastTransferResult(token), 'GPv2: failed transferFrom');
++    */
+   }
+
+   /// @dev Verifies that the last return was a successful `transfer*` call.
 diff -ruN src/contracts/protocol/libraries/logic/BorrowLogic.sol src/contracts/protocol/libraries/logic/BorrowLogic.sol
---- src/contracts/protocol/libraries/logic/BorrowLogic.sol	2024-11-28 19:17:13.680142695 +0200
-+++ src/contracts/protocol/libraries/logic/BorrowLogic.sol	2024-11-28 09:37:40.688170748 +0200
+--- src/contracts/protocol/libraries/logic/BorrowLogic.sol	2024-12-12 12:17:18.481210672 +0200
++++ src/contracts/protocol/libraries/logic/BorrowLogic.sol	2024-12-01 11:47:54.000000000 +0200
 @@ -160,7 +160,7 @@
      DataTypes.ReserveData storage reserve = reservesData[params.asset];
      DataTypes.ReserveCache memory reserveCache = reserve.cache();
@@ -48,8 +85,8 @@ diff -ruN src/contracts/protocol/libraries/logic/BorrowLogic.sol src/contracts/p
 +  function repay_hook_4(DataTypes.ReserveCache memory reserveCache) internal {}
  }
 diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contracts/protocol/libraries/logic/LiquidationLogic.sol
---- src/contracts/protocol/libraries/logic/LiquidationLogic.sol	2024-11-28 19:17:13.685142696 +0200
-+++ src/contracts/protocol/libraries/logic/LiquidationLogic.sol	2024-11-28 19:09:01.430978734 +0200
+--- src/contracts/protocol/libraries/logic/LiquidationLogic.sol	2024-12-12 12:17:18.481210672 +0200
++++ src/contracts/protocol/libraries/logic/LiquidationLogic.sol	2024-12-01 11:47:54.000000000 +0200
 @@ -126,7 +126,9 @@
      DataTypes.ReserveData storage debtReserve = reservesData[params.debtAsset];
      DataTypes.UserConfigurationMap storage userConfig = usersConfig[params.user];
@@ -60,13 +97,14 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
 
      (
        vars.totalCollateralInBaseCurrency,
-@@ -149,11 +151,13 @@
+@@ -149,11 +151,14 @@
      );
 
      vars.collateralAToken = IAToken(collateralReserve.aTokenAddress);
 -    vars.userCollateralBalance = vars.collateralAToken.balanceOf(params.user);
-+    //vars.userCollateralBalance = vars.collateralAToken.balanceOf(params.user);
++
 +    vars.userCollateralBalance = get_userCollateralBalance();
++    //vars.userCollateralBalance = vars.collateralAToken.balanceOf(params.user);
      vars.userReserveDebt = IERC20(vars.debtReserveCache.variableDebtTokenAddress).balanceOf(
        params.user
      );
@@ -75,15 +113,39 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
      ValidationLogic.validateLiquidationCall(
        userConfig,
        collateralReserve,
-@@ -272,6 +276,7 @@
+@@ -165,7 +170,7 @@
+         priceOracleSentinel: params.priceOracleSentinel
+       })
+     );
+-
++    /* MUNGED
+     if (
+       params.userEModeCategory != 0 &&
+       EModeConfiguration.isReserveEnabledOnBitmap(
+@@ -191,6 +196,14 @@
+     vars.userReserveCollateralInBaseCurrency =
+       (vars.userCollateralBalance * vars.collateralAssetPrice) /
+       vars.collateralAssetUnit;
++    */
++    vars.liquidationBonus = get_liquidationBonus();
++    vars.collateralAssetPrice = get_collateralAssetPrice();
++    vars.debtAssetPrice = get_debtAssetPrice();
++    vars.collateralAssetUnit = get_collateralAssetUnit();
++    vars.debtAssetUnit = get_debtAssetUnit();
++    vars.userReserveDebtInBaseCurrency = get_userReserveDebtInBaseCurrency();
++    vars.userReserveCollateralInBaseCurrency = get_userReserveCollateralInBaseCurrency();
+
+     // by default whole debt in the reserve could be liquidated
+     uint256 maxLiquidatableDebt = vars.userReserveDebt;
+@@ -272,6 +285,7 @@
 
      bool hasNoCollateralLeft = vars.totalCollateralInBaseCurrency ==
        vars.collateralToLiquidateInBaseCurrency;
 +    /*HOOK !!*/ HOOK_liquidation_before_burnDebtTokens(hasNoCollateralLeft);
      _burnDebtTokens(
        vars.debtReserveCache,
        debtReserve,
-@@ -282,7 +287,8 @@
+@@ -282,7 +296,8 @@
        vars.actualDebtToLiquidate,
        hasNoCollateralLeft
      );
@@ -93,7 +155,7 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
      // IsolationModeTotalDebt only discounts `actualDebtToLiquidate`, not the fully burned amount in case of deficit creation.
      // This is by design as otherwise debt debt ceiling would render ineffective if a collateral asset faces bad debt events.
      // The governance can decide the raise the ceiling to discount manifested deficit.
-@@ -294,10 +300,12 @@
+@@ -294,10 +309,12 @@
        vars.actualDebtToLiquidate
      );
 
@@ -106,7 +168,7 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
      }
 
      // Transfer fee to treasury if it is non-zero
-@@ -321,9 +329,11 @@
+@@ -321,9 +338,11 @@
      // burn bad debt if necessary
      // Each additional debt asset already adds around ~75k gas to the liquidation.
      // To keep the liquidation gas under control, 0 usd collateral positions are not touched, as there is no immediate benefit in burning or transfering to treasury.
@@ -118,7 +180,7 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
 
      // Transfers the debt asset being repaid to the aToken, where the liquidity is kept
      IERC20(params.debtAsset).safeTransferFrom(
-@@ -363,6 +373,8 @@
+@@ -363,6 +382,8 @@
    ) internal {
      DataTypes.ReserveCache memory collateralReserveCache = collateralReserve.cache();
      collateralReserve.updateState(collateralReserveCache);
@@ -127,7 +189,7 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
      collateralReserve.updateInterestRatesAndVirtualBalance(
        collateralReserveCache,
        params.collateralAsset,
-@@ -624,9 +636,9 @@
+@@ -624,9 +645,9 @@
        DataTypes.ReserveData storage currentReserve = reservesData[reserveAddress];
        DataTypes.ReserveCache memory reserveCache = currentReserve.cache();
        if (!reserveCache.reserveConfiguration.getActive()) continue;
@@ -139,7 +201,7 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
        _burnDebtTokens(
          reserveCache,
          currentReserve,
-@@ -637,6 +649,22 @@
+@@ -637,6 +658,31 @@
          0,
          true
        );
@@ -161,10 +223,19 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra
 +  function HOOK_liquidation_after_burnBadDebt() internal {}
 +
 +  function get_userCollateralBalance() internal returns(uint256) {return 0;}
++
++  function get_liquidationBonus() internal returns(uint256) {return 0;}
++  function get_collateralAssetPrice() internal returns(uint256) {return 0;}
++  function get_debtAssetPrice() internal returns(uint256) {return 0;}
++  function get_collateralAssetUnit() internal returns(uint256) {return 0;}
++  function get_debtAssetUnit() internal returns(uint256) {return 0;}
++  function get_userReserveDebtInBaseCurrency() internal returns(uint256) {return 0;}
++  function get_userReserveCollateralInBaseCurrency() internal returns(uint256) {return 0;}
++
  }
 diff -ruN src/contracts/protocol/libraries/logic/ReserveLogic.sol src/contracts/protocol/libraries/logic/ReserveLogic.sol
---- src/contracts/protocol/libraries/logic/ReserveLogic.sol	2024-11-28 19:17:13.680142695 +0200
-+++ src/contracts/protocol/libraries/logic/ReserveLogic.sol	2024-11-28 09:37:40.691170771 +0200
+--- src/contracts/protocol/libraries/logic/ReserveLogic.sol	2024-12-12 12:17:18.481210672 +0200
++++ src/contracts/protocol/libraries/logic/ReserveLogic.sol	2024-12-01 11:47:54.000000000 +0200
 @@ -53,17 +53,19 @@
      DataTypes.ReserveData storage reserve
    ) internal view returns (uint256) {