update stata to fit the new directories arrangment of the solidity

.github/workflows/certora-stata.yml

@@ -56,8 +56,7 @@ jobs:
           # - 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 previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
           - verifyERC4626Extended.conf --rule redeemSum
           - verifyERC4626Extended.conf --rule redeemATokensSum
           - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf

certora/basic/Makefile

@@ -0,0 +1,24 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../../src/
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./src/++g' | sed 's+munged/++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+

certora/basic/conf/AToken.conf

@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/basic/harness/ATokenHarness.sol",
+    "certora/basic/harness/SimpleERC20.sol"
+  ],
+  "link": [
+    "ATokenHarness:_underlyingAsset=SimpleERC20"
+  ],
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic".
+  "optimistic_loop": true,
+  "process": "emv",
+  "solc": "solc8.19",
+  "verify": "ATokenHarness:certora/basic/specs/AToken.spec",
+  "build_cache": true,
+  "msg": "aToken spec"
+}

certora/basic/conf/EModeConfiguration.conf

@@ -0,0 +1,14 @@
+{
+  "files": [
+    "certora/basic/harness/EModeConfigurationHarness.sol"
+  ],
+  "msg": "EModeConfiguration",
+  "optimistic_loop": true,
+  "process": "emv",
+  //  "prover_args": [],
+  "precise_bitwise_ops": true,
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "EModeConfigurationHarness:certora/basic/specs/EModeConfiguration.spec"
+}

certora/basic/conf/NEW-pool-no-summarizations.conf

@@ -0,0 +1,40 @@
+{
+  "files": [
+    "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",
+  ],
+  "link": [
+    "ATokenHarness:POOL=PoolHarness",
+    "ATokenHarness:_underlyingAsset=SimpleERC20",
+    "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+    "AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider",
+  ],
+  "struct_link": [
+    "PoolHarness:aTokenAddress=ATokenHarness",
+    "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
+    "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
+  ],
+  "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+  "optimistic_loop": true,
+  "process": "emv",
+  "global_timeout": "7198",
+  "prover_args": ["-depth 11"], // If reachability passes and the time is ok, this number is ok, dont touch it.
+  "solc": "solc8.19",
+  "verify": "PoolHarness:certora/basic/specs/NEW-pool-no-summarizations.spec",
+  "rule": [
+    "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
+    "depositUpdatesUserATokenSuperBalance",
+    "depositCannotChangeOthersATokenSuperBalance"
+  ],
+  "build_cache": true,
+  "parametric_contracts": ["PoolHarness"],
+  "msg": "pool-no-summarizations::partial rules",
+}

certora/basic/conf/NEW-pool-simple-properties.conf

@@ -0,0 +1,43 @@
+{
+  "files": [
+    "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",
+  ],
+  "link": [
+    "ATokenHarness:POOL=PoolHarness",
+    "ATokenHarness:_underlyingAsset=SimpleERC20",
+    "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+  ],
+  "struct_link": [
+    "PoolHarness:aTokenAddress=ATokenHarness",
+    "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
+    "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
+  ],
+  "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+  "optimistic_loop": true,
+  "process": "emv",
+  "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
+  "solc": "solc8.19",
+  "verify": "PoolHarness:certora/basic/specs/NEW-pool-simple-properties.spec",
+  "rule": [
+    "cannotDepositInInactiveReserve",
+    "cannotDepositInFrozenReserve",
+    "cannotDepositZeroAmount",
+    "cannotWithdrawZeroAmount",
+    "cannotWithdrawFromInactiveReserve",
+    "cannotBorrowZeroAmount",
+    "cannotBorrowOnInactiveReserve",
+    "cannotBorrowOnReserveDisabledForBorrowing",
+    "cannotBorrowOnFrozenReserve"
+  ],
+  "build_cache": true,
+  "parametric_contracts": ["PoolHarness"],
+  "smt_timeout": "6000",
+  "msg": "pool-simple-properties::ALL",
+}

certora/basic/conf/ReserveConfiguration.conf

@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/basic/harness/ReserveConfigurationHarness.sol"
+  ],
+  "msg": "ReserveConfiguration",
+  "optimistic_loop": true,
+  "process": "emv",
+  //  "prover_args": [
+  //  "-precise_bitwise_ops"
+  //],
+  "precise_bitwise_ops": true,
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "ReserveConfigurationHarness:certora/basic/specs/ReserveConfiguration.spec"
+}

certora/basic/conf/UserConfiguration.conf

@@ -0,0 +1,17 @@
+{
+  "files": [
+    "certora/basic/harness/UserConfigurationHarness.sol"
+  ],
+  // No rule sanity because a there are invariant s.t. the invariant can be proven
+  // without assuming it first. (for some of the functions.)
+  "msg": "UserConfiguration All spec",
+  "optimistic_loop": true,
+  "process": "emv",
+//  "prover_args": [
+  //  "-precise_bitwise_ops"
+  //],
+  "precise_bitwise_ops": true,
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "UserConfigurationHarness:certora/basic/specs/UserConfiguration.spec"
+}

certora/basic/conf/VariableDebtToken.conf

@@ -0,0 +1,12 @@
+{
+  "files": [
+    "certora/basic/harness/VariableDebtTokenHarness.sol"
+  ],
+  "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+  "msg": "variable debt token",
+  "optimistic_loop": true,
+  "process": "emv",
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "VariableDebtTokenHarness:certora/basic/specs/VariableDebtToken.spec"
+}

certora/basic/harness/EModeConfigurationHarness.sol

@@ -0,0 +1,47 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.19;
+pragma experimental ABIEncoderV2;
+
+import {EModeConfiguration} from '../munged/contracts/protocol/libraries/configuration/EModeConfiguration.sol';
+import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol';
+
+contract EModeConfigurationHarness {
+  DataTypes.EModeCategory public eModeCategory;
+
+  function setCollateral(uint256 reserveIndex,bool collateral) public {
+    DataTypes.EModeCategory memory emode_new = eModeCategory;
+    EModeConfiguration.setCollateral(emode_new, reserveIndex, collateral);
+    eModeCategory.isCollateralBitmap = emode_new.isCollateralBitmap;
+  }
+
+  function isCollateralAsset(uint256 reserveIndex) public returns (bool) {
+    return EModeConfiguration.isCollateralAsset(eModeCategory.isCollateralBitmap, reserveIndex);
+  }
+
+
+  function setBorrowable(uint256 reserveIndex,bool borrowable) public {
+    DataTypes.EModeCategory memory emode_new = eModeCategory;
+    EModeConfiguration.setBorrowable(emode_new, reserveIndex, borrowable);
+    eModeCategory.isBorrowableBitmap = emode_new.isBorrowableBitmap;
+  }
+
+  function isBorrowableAsset(uint256 reserveIndex) public returns (bool) {
+    return EModeConfiguration.isBorrowableAsset(eModeCategory.isBorrowableBitmap, reserveIndex);
+  }
+
+
+  /*
+
+  // Sets the Loan to Value of the reserve
+  function setLtv(uint256 ltv) public {
+    DataTypes.ReserveConfigurationMap memory configNew = reservesConfig;
+    ReserveConfiguration.setLtv(configNew, ltv);
+    reservesConfig.data = configNew.data;
+  }
+
+  // Gets the Loan to Value of the reserve
+  function getLtv() public view returns (uint256) {
+    return ReserveConfiguration.getLtv(reservesConfig);
+  }
+  */
+}

certora/basic/harness/PoolHarness.sol

@@ -0,0 +1,79 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.19;
+
+import {PoolInstance} from '../munged/contracts/instances/PoolInstance.sol';
+import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.sol';
+import {ReserveLogic} from '../munged/contracts/protocol/libraries/logic/ReserveLogic.sol';
+import {IPoolAddressesProvider} from '../munged/contracts/interfaces/IPoolAddressesProvider.sol';
+
+import {IERC20} from '../../../src/contracts/dependencies/openzeppelin/contracts/IERC20.sol';
+import {ReserveConfiguration} from '../munged/contracts/protocol/libraries/configuration/ReserveConfiguration.sol';
+
+contract PoolHarness is PoolInstance {
+  using ReserveLogic for DataTypes.ReserveData;
+  using ReserveLogic for DataTypes.ReserveCache;
+
+  constructor(IPoolAddressesProvider provider) public PoolInstance(provider) {}
+
+  function getCurrScaledVariableDebt(address asset) public view returns (uint256) {
+    DataTypes.ReserveData storage reserve = _reserves[asset];
+    DataTypes.ReserveCache memory reserveCache = reserve.cache();
+    return reserveCache.currScaledVariableDebt;
+  }
+
+  function getTotalDebt(address asset) public view returns (uint256) {
+    uint256 totalVariable = IERC20(_reserves[asset].variableDebtTokenAddress).totalSupply();
+    return totalVariable;
+  }
+
+  function getTotalATokenSupply(address asset) public view returns (uint256) {
+    return IERC20(_reserves[asset].aTokenAddress).totalSupply();
+  }
+
+  function getReserveLiquidityIndex(address asset) public view returns (uint256) {
+    return _reserves[asset].liquidityIndex;
+  }
+
+  function getReserveVariableBorrowIndex(address asset) public view returns (uint256) {
+    return _reserves[asset].variableBorrowIndex;
+  }
+
+  function getReserveVariableBorrowRate(address asset) public view returns (uint256) {
+    return _reserves[asset].currentVariableBorrowRate;
+  }
+
+  function updateReserveIndexes(address asset) public returns (bool) {
+    ReserveLogic._updateIndexes(_reserves[asset], _reserves[asset].cache());
+    return true;
+  }
+
+  function updateReserveIndexesWithCache(
+    address asset,
+    DataTypes.ReserveCache memory cache
+  ) public returns (bool) {
+    ReserveLogic._updateIndexes(_reserves[asset], cache);
+    return true;
+  }
+
+  function cumulateToLiquidityIndex(
+    address asset,
+    uint256 totalLiquidity,
+    uint256 amount
+  ) public returns (uint256) {
+    return ReserveLogic.cumulateToLiquidityIndex(_reserves[asset], totalLiquidity, amount);
+  }
+
+  function getActive(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
+    return ReserveConfiguration.getActive(self);
+  }
+
+  function getFrozen(DataTypes.ReserveConfigurationMap memory self) external pure returns (bool) {
+    return ReserveConfiguration.getFrozen(self);
+  }
+
+  function getBorrowingEnabled(
+    DataTypes.ReserveConfigurationMap memory self
+  ) external pure returns (bool) {
+    return ReserveConfiguration.getBorrowingEnabled(self);
+  }
+}