Certora Review

.github/workflows/certora-basic.yml

@@ -1,4 +1,4 @@
-name: certora
+name: certora-basic
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
@@ -34,7 +34,7 @@ jobs:
         with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.17.2
+        run: pip install certora-cli==7.20.3
 
       - name: Install solc
         run: |

.github/workflows/certora-stata.yml

@@ -31,7 +31,7 @@ jobs:
         with: { distribution: "zulu", java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.17.2
+        run: pip install certora-cli==7.20.3
       - name: Install solc
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux

.github/workflows/comment.yml

@@ -12,6 +12,7 @@ permissions:
   checks: read
   statuses: read
   pull-requests: write
+  contents: write
 
 jobs:
   comment:

.github/workflows/test.yml

@@ -47,20 +47,20 @@ jobs:
         run: npm ci --prefer-offline --no-audit
 
       - name: Run Foundry setup
-        uses: bgd-labs/github-workflows/.github/actions/foundry-setup@d738561b5afce35ca3752b28236c9dd68a3fa822
+        uses: bgd-labs/github-workflows/.github/actions/foundry-setup@4f16d15e380bbcf7e3933698c08b9fd34e967f78
 
       - name: Run Forge tests
-        uses: bgd-labs/github-workflows/.github/actions/foundry-test@d738561b5afce35ca3752b28236c9dd68a3fa822
+        uses: bgd-labs/github-workflows/.github/actions/foundry-test@4f16d15e380bbcf7e3933698c08b9fd34e967f78
 
       - name: Run Gas report
-        uses: bgd-labs/github-workflows/.github/actions/foundry-gas-report@d738561b5afce35ca3752b28236c9dd68a3fa822
+        uses: bgd-labs/github-workflows/.github/actions/foundry-gas-report@4f16d15e380bbcf7e3933698c08b9fd34e967f78
 
       - name: Cleanup
         # This test will currently fail on coverage due to the gas limit beaing breached with optimizer disabled
         run: rm tests/deployments/DeploymentsGasLimits.t.sol
 
       - name: Run Lcov report
-        uses: bgd-labs/github-workflows/.github/actions/foundry-lcov-report@d738561b5afce35ca3752b28236c9dd68a3fa822
+        uses: bgd-labs/github-workflows/.github/actions/foundry-lcov-report@4f16d15e380bbcf7e3933698c08b9fd34e967f78
 
       - name: Save PR number
         if: github.event_name == 'pull_request' || github.event_name == 'pull_request_target'

Makefile

@@ -11,7 +11,7 @@ test-contract :; forge test --match-contract ${filter} -vvv
 test-watch   :; forge test --watch -vvv --no-match-contract DeploymentsGasLimits
 
 # Coverage
-coverage-base :; forge coverage --report lcov --no-match-coverage "(scripts|tests|deployments|mocks)"
+coverage-base :; forge coverage --fuzz-runs 50 --report lcov --no-match-coverage "(scripts|tests|deployments|mocks)"
 coverage-clean :; lcov --rc derive_function_end_line=0 --remove ./lcov.info -o ./lcov.info.p \
 	'src/contracts/extensions/v3-config-engine/*' \
 	'src/contracts/treasury/*' \
@@ -37,7 +37,7 @@ coverage :
 download :; cast etherscan-source --chain ${chain} -d src/etherscan/${chain}_${address} ${address}
 git-diff :
 	@mkdir -p diffs
-	@npx prettier ${before} ${after} --write
+	# @npx prettier ${before} ${after} --write
 	@printf '%s\n%s\n%s\n' "\`\`\`diff" "$$(git diff --no-index --ignore-space-at-eol ${before} ${after})" "\`\`\`" > diffs/${out}.md
 
 # Deploy
@@ -51,3 +51,5 @@ deploy-libs :
 	npx catapulta-verify -b broadcast/LibraryPreCompileOne.sol/${chainId}/run-latest.json
 	make deploy-libs-two chain=${chain}
 	npx catapulta-verify -b broadcast/LibraryPreCompileTwo.sol/${chainId}/run-latest.json
+
+gas-report :; forge test --fuzz-runs 50 --gas-report

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",

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",

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

certora/basic/specs/EModeConfiguration.spec

@@ -56,5 +56,3 @@ rule independencyOfBorrowableSetters(uint256 reserveIndex, bool borrowable) {
   assert (reserveIndex != reserveIndex_other => before == after);
 }
 
-
-

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;
 }
 

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;
 }
 

certora/basic/specs/aux/aToken.spec

@@ -131,6 +131,7 @@ function indexForToken(address token, env e) returns uint256 {
 
 // todo: adjust for stable debt token
 function aTokenBalanceOfCVL(address token, address user, env e) returns uint256 {
+  require token != 0;
     uint storedBalance = balanceOfCVL(token, user);
     if (aTokenToUnderlying[token] == 0) {
         // not a properly initialized aToken, return the regular ERC20 balance

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,43 @@ 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;
+}
+
+
+// For flashloan
+methods {
+    function _.executeOperation(
+        address[] assets,
+        uint256[] amounts,
+        uint256[] premiums,
+        address initiator,
+        bytes params
+    ) external => NONDET; // expect bool;
+
+    // simple receiver
+    function _.executeOperation(
+        address asset,
+        uint256 amount,
+        uint256 premium,
+        address initiator,
+        bytes params
+    ) external => NONDET; // expect bool;
 }
 
 
@@ -55,9 +76,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";
@@ -82,29 +103,19 @@ rule stableFieldsUntouched(method f, env e, address _asset)
     aTokenToUnderlying[currentContract._reserves[asset].aTokenAddress]==asset
     &&
     aTokenToUnderlying[currentContract._reserves[asset].variableDebtTokenAddress]==asset;
+
 
-  DataTypes.ReserveData reserve = getReserveDataExtended(_asset);
   DataTypes.ReserveDataLegacy reserveLegasy = getReserveData(_asset);
 
-  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.ReserveDataLegacy reserveLegasy2 = getReserveData(_asset);
 
-  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 currentStableBorrowRate_BEFORE == currentStableBorrowRate_AFTER;
-  //  assert stableDebtTokenAddress_BEFORE == stableDebtTokenAddress_AFTER;
-
 }