From 28d1cde2333ee08307d80cbf95d3a146e68076a2 Mon Sep 17 00:00:00 2001 From: nisnislevi Date: Thu, 12 Dec 2024 12:19:13 +0200 Subject: [PATCH] closing pool-solvency work before moving to public repo --- certora/solvency/applyHarness.patch | 103 +++++++++++++++++++++++----- 1 file changed, 87 insertions(+), 16 deletions(-) diff --git a/certora/solvency/applyHarness.patch b/certora/solvency/applyHarness.patch index 0de63e18..ac645499 100644 --- 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,7 +113,31 @@ 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; @@ -83,7 +145,7 @@ diff -ruN src/contracts/protocol/libraries/logic/LiquidationLogic.sol src/contra _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) {