Merge remote-tracking branch 'certora-private/pool-solvency' into cer…

…tora
Certora · Dec 12, 2024 · 7871726 · 7871726
2 parents bfdf50b + 28d1cde
commit 7871726
Show file tree

Hide file tree

Showing 208 changed files with 17,133 additions and 45 deletions.
diff --git a/certora/basic/conf/NEW-pool-no-summarizations.conf b/certora/basic/conf/NEW-pool-no-summarizations.conf
@@ -3,13 +3,13 @@
     "certora/basic/harness/ATokenHarness.sol",
     "certora/basic/harness/PoolHarness.sol",
     "certora/basic/harness/SimpleERC20.sol",
-    "src/contracts/instances/VariableDebtTokenInstance.sol",
-    "src/contracts/helpers/AaveProtocolDataProvider.sol",
-    "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
-    "src/contracts/protocol/configuration/ACLManager.sol",
-    "src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
-    "src/contracts/misc/PriceOracleSentinel.sol",
-    "src/contracts/protocol/configuration/PoolAddressesProvider.sol",
+    "certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol",
+    "certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol",
+    "certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
+    "certora/basic/munged/contracts/protocol/configuration/ACLManager.sol",
+    "certora/basic/munged/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
+    "certora/basic/munged/contracts/misc/PriceOracleSentinel.sol",
+    "certora/basic/munged/contracts/protocol/configuration/PoolAddressesProvider.sol",
   ],
   "link": [
     "ATokenHarness:POOL=PoolHarness",

diff --git a/certora/basic/conf/NEW-pool-simple-properties.conf b/certora/basic/conf/NEW-pool-simple-properties.conf
@@ -3,11 +3,11 @@
     "certora/basic/harness/ATokenHarness.sol",
     "certora/basic/harness/PoolHarness.sol",
     "certora/basic/harness/SimpleERC20.sol",
-    "src/contracts/instances/VariableDebtTokenInstance.sol",
-    "src/contracts/helpers/AaveProtocolDataProvider.sol",
-    "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
-    "src/contracts/protocol/libraries/types/DataTypes.sol",
-    "src/contracts/protocol/configuration/PoolAddressesProvider.sol",
+    "certora/basic/munged/contracts/instances/VariableDebtTokenInstance.sol",
+    "certora/basic/munged/contracts/helpers/AaveProtocolDataProvider.sol",
+    "certora/basic/munged/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
+    "certora/basic/munged/contracts/protocol/libraries/types/DataTypes.sol",
+    "certora/basic/munged/contracts/protocol/configuration/PoolAddressesProvider.sol",
   ],
   "link": [
     "ATokenHarness:POOL=PoolHarness",

diff --git a/certora/basic/scripts/run-all.sh b/certora/basic/scripts/run-all.sh
@@ -33,9 +33,9 @@ certoraRun $CMN certora/basic/conf/stableRemoved.conf \
            --msg "6: Stable fields are un-touched"
 
 echo
-echo "******** Running:  6 EModeConfiguration ***************"
+echo "******** Running:  7 EModeConfiguration ***************"
 certoraRun $CMN certora/basic/conf/EModeConfiguration.conf \
-           --msg "6: EModeConfiguration"
+           --msg "7: EModeConfiguration"
 
 
 echo

diff --git a/certora/basic/specs/EModeConfiguration.spec b/certora/basic/specs/EModeConfiguration.spec
@@ -56,5 +56,3 @@ rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) {
   assert (reserveIndex != reserveIndex_other => before == after);
 }
 
-
-
diff --git a/certora/basic/specs/NEW-pool-base.spec b/certora/basic/specs/NEW-pool-base.spec
@@ -99,36 +99,36 @@ function calculateCompoundedInterestSummary(uint256 rate, uint40 t0, uint256 t1)
 }
 
 function isActiveReserve(env e, address asset) returns bool {
-  DataTypes.ReserveData data = getReserveDataExtended(e, asset);
+  DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
   DataTypes.ReserveConfigurationMap configuration = data.configuration;
   bool isActive = getActive(e, configuration);
 
   return isActive;
 }
 
 function isFrozenReserve(env e, address asset) returns bool {
-  DataTypes.ReserveData data = getReserveDataExtended(e, asset);
+  DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
   DataTypes.ReserveConfigurationMap configuration = data.configuration;
   bool isFrozen = getFrozen(e, configuration);
 
   return isFrozen;
 }
 
 function isEnabledForBorrow(env e, address asset) returns bool {
-  DataTypes.ReserveData data = getReserveDataExtended(e, asset);
+  DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
   DataTypes.ReserveConfigurationMap configuration = data.configuration;
   bool isBorrowEnabled = getBorrowingEnabled(e, configuration);
 
   return isBorrowEnabled;
 }
 
 function getCurrentLiquidityRate(env e, address asset) returns mathint {
-  DataTypes.ReserveData data = getReserveDataExtended(e, asset);
+  DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
   return data.currentLiquidityRate;
 }
 
 function getLiquidityIndex(env e, address asset) returns mathint {
-  DataTypes.ReserveData data = getReserveDataExtended(e, asset);
+  DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
   return data.liquidityIndex;
 }
 

diff --git a/certora/basic/specs/NEW-pool-no-summarizations.spec b/certora/basic/specs/NEW-pool-no-summarizations.spec
@@ -81,7 +81,7 @@ rule liquidityIndexNonDecresingFor_cumulateToLiquidityIndex() {
 
 
 function get_AToken_of_asset(env e, address asset) returns address {
-  DataTypes.ReserveData data = getReserveDataExtended(e, asset);
+  DataTypes.ReserveDataLegacy data = getReserveData(e, asset);
   return data.aTokenAddress;
 }
 

diff --git a/certora/basic/specs/stableRemoved.spec b/certora/basic/specs/stableRemoved.spec
@@ -4,7 +4,7 @@ import "aux/aToken.spec";
 //import "AddressProvider.spec";
 
 methods {
-  function getReserveDataExtended(address) external returns (DataTypes.ReserveData memory) envfree;
+  //  function getReserveDataExtended(address) external returns (DataTypes.ReserveData memory) envfree;
   function getReserveData(address) external returns (DataTypes.ReserveDataLegacy memory) envfree;
 
   function ValidationLogic.validateLiquidationCall(
@@ -21,22 +21,22 @@ methods {
                                                  DataTypes.CalculateUserAccountDataParams memory params
   ) internal returns (uint256, uint256, uint256, uint256, uint256, bool) => NONDET;
 
-  function LiquidationLogic._calculateDebt(
+  /*  function LiquidationLogic._calculateDebt(
                                            DataTypes.ReserveCache memory debtReserveCache,
                                            DataTypes.ExecuteLiquidationCallParams memory params,
                                            uint256 healthFactor
-  ) internal returns (uint256, uint256) => NONDET;
+                                           ) internal returns (uint256, uint256) => NONDET;*/
 
   function LiquidationLogic._calculateAvailableCollateralToLiquidate(
-                                                                     DataTypes.ReserveData storage collateralReserve,
-                                                                     DataTypes.ReserveCache memory debtReserveCache,
-                                                                     address collateralAsset,
-                                                                     address debtAsset,
-                                                                     uint256 debtToCover,
-                                                                     uint256 userCollateralBalance,
-                                                                     uint256 liquidationBonus,
-                                                                     address // IPriceOracleGetter 
-  ) internal returns (uint256,uint256,uint256) => NONDET;
+    DataTypes.ReserveConfigurationMap memory collateralReserveConfiguration,
+    uint256 collateralAssetPrice,
+    uint256 collateralAssetUnit,
+    uint256 debtAssetPrice,
+    uint256 debtAssetUnit,
+    uint256 debtToCover,
+    uint256 userCollateralBalance,
+    uint256 liquidationBonus
+  ) internal returns (uint256, uint256, uint256, uint256) => NONDET;
 }
 
 
@@ -55,9 +55,9 @@ function init_state() {
 }
 
 
-hook Sstore _reserves[KEY address a].__deprecatedStableBorrowRate uint128 rate (uint128 old_rate) {
-  assert false, "writing the field __deprecatedStableBorrowRate";
-}
+//hook Sstore _reserves[KEY address a].__deprecatedStableBorrowRate uint128 rate (uint128 old_rate) {
+//  assert false, "writing the field __deprecatedStableBorrowRate";
+//}
 
 hook Sstore _reserves[KEY address a].__deprecatedStableDebtTokenAddress address stable (address old_stable) {
   assert false, "writing the field __deprecatedStableDebtTokenAddress";
@@ -83,27 +83,27 @@ rule stableFieldsUntouched(method f, env e, address _asset)
     &&
     aTokenToUnderlying[currentContract._reserves[asset].variableDebtTokenAddress]==asset;
 
-  DataTypes.ReserveData reserve = getReserveDataExtended(_asset);
+  //DataTypes.ReserveData reserve = getReserveDataExtended(_asset);
   DataTypes.ReserveDataLegacy reserveLegasy = getReserveData(_asset);
 
-  uint128 __deprecatedStableBorrowRate_BEFORE = reserve.__deprecatedStableBorrowRate;
-  address __deprecatedStableDebtTokenAddress_BEFORE = reserve.__deprecatedStableDebtTokenAddress;
+  //uint128 __deprecatedStableBorrowRate_BEFORE = reserve.__deprecatedStableBorrowRate;
+  //address __deprecatedStableDebtTokenAddress_BEFORE = reserve.__deprecatedStableDebtTokenAddress;
   uint128 currentStableBorrowRate_BEFORE = reserveLegasy.currentStableBorrowRate;
   //  address stableDebtTokenAddress_BEFORE = reserveLegasy.stableDebtTokenAddress;
 
   calldataarg args;
   f(e,args);
 
-  DataTypes.ReserveData reserve2 = getReserveDataExtended(_asset);
+  //  DataTypes.ReserveData reserve2 = getReserveDataExtended(_asset);
   DataTypes.ReserveDataLegacy reserveLegasy2 = getReserveData(_asset);
 
-  uint128 __deprecatedStableBorrowRate_AFTER = reserve2.__deprecatedStableBorrowRate;
-  address __deprecatedStableDebtTokenAddress_AFTER = reserve2.__deprecatedStableDebtTokenAddress;
+  //uint128 __deprecatedStableBorrowRate_AFTER = reserve2.__deprecatedStableBorrowRate;
+  //address __deprecatedStableDebtTokenAddress_AFTER = reserve2.__deprecatedStableDebtTokenAddress;
   uint128 currentStableBorrowRate_AFTER = reserveLegasy2.currentStableBorrowRate;
   address stableDebtTokenAddress_AFTER = reserveLegasy2.stableDebtTokenAddress;
 
-  assert __deprecatedStableBorrowRate_BEFORE == __deprecatedStableBorrowRate_AFTER;
-  assert __deprecatedStableDebtTokenAddress_BEFORE == __deprecatedStableDebtTokenAddress_AFTER;
+  //  assert __deprecatedStableBorrowRate_BEFORE == __deprecatedStableBorrowRate_AFTER;
+  //assert __deprecatedStableDebtTokenAddress_BEFORE == __deprecatedStableDebtTokenAddress_AFTER;
   assert currentStableBorrowRate_BEFORE == currentStableBorrowRate_AFTER;
   //  assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER;
Original file line number	Diff line number	Diff line change
Expand Up		@@ -56,5 +56,3 @@ rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) {
		assert (reserveIndex != reserveIndex_other => before == after);
		}