for PR (#30)

.github/workflows/certora.yml → .github/workflows/certora-basic.yml

@@ -39,7 +39,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.0.7
+        run: pip install certora-cli==7.14.2
 
       - name: Install solc
         run: |
@@ -49,12 +49,12 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          cd certora
+          cd certora/basic
           touch applyHarness.patch
           make munged
-          cd ..
+          cd ../..
           echo "key length" ${#CERTORAKEY}
-          certoraRun certora/conf/${{ matrix.rule }} --wait_for_results
+          certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -68,6 +68,8 @@ jobs:
           - UserConfiguration.conf
           - VariableDebtToken.conf
           - NEW-pool-no-summarizations.conf
+          - stableRemoved.conf
+          - EModeConfiguration.conf
           - NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
           - NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
           - NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"

.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,32 @@
+{
+  "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",
+  "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/conf/stableRemoved.conf

@@ -0,0 +1,20 @@
+{
+	"assert_autofinder_success": true,
+	"build_cache": true,
+	"cache": "aave_inv",
+	"files": [
+                "certora/basic/harness/PoolInstanceHarness.sol"
+	],
+        "disable_solc_optimizers": ["cse","peephole"],
+	"java_args": [" -ea -Dlevel.setup.helpers=info"],
+	"msg": "Stable fields are un-touched",
+	"optimistic_loop": true,
+	"process": "emv",
+//	"prover_args": [" -split false"	],
+        "server": "prover",               
+	"smt_timeout": "6000",
+	"solc": "solc8.19",
+	"solc_optimize": "200",
+        "rule_sanity": "basic",
+	"verify": "PoolInstanceHarness:certora/basic/specs/stableRemoved.spec"
+}

certora/basic/harness/DummyContract.sol

@@ -0,0 +1,8 @@
+
+contract DummyContract {
+    function havoc_all_dummy() external {
+      //        havoc_all_dummy_internal();
+    }
+
+    //function havoc_all_dummy_internal() internal {}
+}

certora/basic/harness/EModeConfigurationHarness.sol

@@ -0,0 +1,30 @@
+// 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 enabled) public {
+    DataTypes.EModeCategory memory emode_new = eModeCategory;
+    eModeCategory.collateralBitmap = EModeConfiguration.setReserveBitmapBit(emode_new.collateralBitmap, reserveIndex, enabled);
+  }
+
+  function isCollateralAsset(uint256 reserveIndex) public returns (bool) {
+    return EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.collateralBitmap, reserveIndex);
+  }
+
+
+
+  function setBorrowable(uint256 reserveIndex,bool enabled) public {
+    DataTypes.EModeCategory memory emode_new = eModeCategory;
+    eModeCategory.borrowableBitmap = EModeConfiguration.setReserveBitmapBit(emode_new.borrowableBitmap, reserveIndex, enabled);
+  }
+
+  function isBorrowableAsset(uint256 reserveIndex) public returns (bool) {
+    return EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.borrowableBitmap, reserveIndex);
+  }
+}

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