Split rule method_reachability and split borrow functionality tasks i…

…n the CI
Certora · Dec 13, 2023 · 2750416 · 2750416
1 parent 911a539
commit 2750416
Show file tree

Hide file tree

Showing 6 changed files with 194 additions and 10 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -69,11 +69,24 @@ jobs:
           - PoolSimpleProperties.conf --msg "Deposit functionality part 1" --rule "cannotDepositInInactiveReserve"
           - PoolSimpleProperties.conf --msg "Deposit functionality part 2" --rule "cannotDepositInFrozenReserve"
           - PoolSimpleProperties.conf --msg "Deposit functionality part 3" --rule "cannotDepositZeroAmount"
-          - PoolSimpleProperties.conf --msg "Methods reachability" --rule "method_reachability"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 1" --rule "method_reachability_split_for_CI_1"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 2" --rule "method_reachability_split_for_CI_02_backUnbacked"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 3" --rule "method_reachability_split_for_CI_03_repayWithATokens"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 4" --rule "method_reachability_split_for_CI_04_repayWithPermit"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 5" --rule "method_reachability_split_for_CI_05_liquidationCall"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 6" --rule "method_reachability_split_for_CI_06_flashLoan"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 7" --rule "method_reachability_split_for_CI_07_borrow"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 8" --rule "method_reachability_split_for_CI_08_supplyWithPermit"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 9" --rule "method_reachability_split_for_CI_09_rebalanceStableBorrowRate"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 10" --rule "method_reachability_split_for_CI_10_repay"
+          - PoolSimpleProperties.conf --msg "Methods reachability part 11" --rule "method_reachability_split_for_CI_11_flashLoanSimple"
           - PoolSimpleProperties.conf --msg "Withdraw functionality part 1" --rule "cannotWithdrawFromInactiveReserve"
           - PoolSimpleProperties.conf --msg "Withdraw functionality part 2" --rule "cannotWithdrawZeroAmount"
-          - PoolSimpleProperties.conf --msg "Borrow functionality" --rule "cannotBorrowZeroAmount" "cannotBorrowOnInactiveReserve" "cannotBorrowOnReserveDisabledForBorrowing" "cannotBorrowOnFrozenReserve"
-        timeoutdisabled:
-          - PoolAccurate.conf --msg "Deposit updates AToken scaled balance" --rule "depositUpdatesUserATokenSuperBalance"  "depositUpdatesUserATokenSuperBalance_sanity"
-          - PoolAccurate.conf --msg "Deposit cannot change other users scaled balance" --rule "depositCannotChangeOthersATokenSuperBalance"
-          - PoolAccurate.conf --msg "Index non decreasing part 2 -- timeouting when not split into different patches of methods" --rule _updateIndexesWrapperReachable
+          - PoolSimpleProperties.conf --msg "Borrow functionality part 1" --rule "cannotBorrowZeroAmount"
+          - PoolSimpleProperties.conf --msg "Borrow functionality part 2" --rule "cannotBorrowOnInactiveReserve"
+          - PoolSimpleProperties.conf --msg "Borrow functionality part 3" --rule "cannotBorrowOnReserveDisabledForBorrowing"
+          - PoolSimpleProperties.conf --msg "Borrow functionality part 4" --rule "cannotBorrowOnFrozenReserve"
+         # disabled because of TIMEOUT:
+         # - PoolAccurate.conf --msg "Deposit updates AToken scaled balance" --rule "depositUpdatesUserATokenSuperBalance"  "depositUpdatesUserATokenSuperBalance_sanity"
+         # - PoolAccurate.conf --msg "Deposit cannot change other users scaled balance" --rule "depositCannotChangeOthersATokenSuperBalance"
+         # - PoolAccurate.conf --msg "Index non decreasing part 2 -- timeouting when not split into different patches of methods" --rule _updateIndexesWrapperReachable
diff --git a/certora/conf/PoolAccurate.conf b/certora/conf/PoolAccurate.conf
@@ -33,6 +33,7 @@
     "solc": "solc8.10",
     "verify": "PoolHarness:certora/specs/pool-no-summarizations.spec",
     "parametric_contracts": ["PoolHarness"],
-    // "rule": ["_updateIndexesWrapperReachable"],
+    // "rule": ["indexChangesOnlyWith_updateIndexes"],
+    // "msg": "Run indexChangesOnlyWith_updateIndexes with cache none"
     // method repayWithPermit address,uint256,uint256,address,uint256,uint8,bytes32,bytes32 
 }
diff --git a/certora/conf/PoolIndexNonDecreasing.conf b/certora/conf/PoolIndexNonDecreasing.conf
@@ -0,0 +1,37 @@
+{
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/PoolHarness.sol",
+        "certora/harness/StableDebtTokenHarness.sol",
+        "certora/harness/SimpleERC20.sol",
+        "certora/munged/protocol/tokenization/VariableDebtToken.sol",
+        "certora/munged/misc/AaveProtocolDataProvider.sol",
+        // "contracts/protocol/libraries/configuration/ReserveConfiguration.sol",
+        "certora/munged/protocol/pool/DefaultReserveInterestRateStrategy.sol",
+        "certora/munged/protocol/configuration/ACLManager.sol",
+        "certora/munged/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
+        "certora/munged/protocol/configuration/PriceOracleSentinel.sol",
+        "certora/munged/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:stableDebtTokenAddress=StableDebtTokenHarness",
+        "PoolHarness:variableDebtTokenAddress=VariableDebtToken",
+        "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategy",
+    ],
+    "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.10",
+    "verify": "PoolHarness:certora/specs/pool-no-summarizations.spec",
+    "msg": "Index Non Decreasing",
+    "parametric_contracts": ["PoolHarness"],
+    "rule": ["_updateIndexesWrapperReachable", "indexChangesOnlyWith_updateIndexes", "indexesNonDecresingFor_updateIndexes", "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex"],
+}
diff --git a/certora/conf/PoolInvariant.conf b/certora/conf/PoolInvariant.conf
@@ -28,8 +28,8 @@
     "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
     "solc": "solc8.10",
     "verify": "PoolHarness:certora/specs/pool-AAVE-invariant.spec",
-    "msg": "Pool, try borrowOnlyVariableOrStableRate",
-    "rule": ["borrowOnlyVariableOrStableRate"],
+    // "msg": "Pool, try indexIncreasesMonotonically with cache none",
+    // "rule": ["indexIncreasesMonotonically"],
     "parametric_contracts": ["PoolHarness"],
     // "method": "liquidationCall(address,address,address,uint256,bool)",
 }
diff --git a/certora/conf/PoolSimpleProperties.conf b/certora/conf/PoolSimpleProperties.conf
@@ -27,7 +27,7 @@
     "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",
-    "msg": "Pool simple properties",
+    // "msg": "Pool simple properties with cache none",
     // "rule": ["cannotDepositInInactiveReserve"],
     "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
     "solc": "solc8.10",

diff --git a/certora/specs/pool-simple-properties.spec b/certora/specs/pool-simple-properties.spec
@@ -16,6 +16,139 @@ rule method_reachability(env e, method f) {
     satisfy true;
 }
 
+// @title based on this result of run in the CI:
+// https://prover.certora.com/output/33050/3e09e274b3644f6c9ed051b83a6e4dfb?anonymousKey=b6ade0dd3ada78730183db26a344bafb282861b4
+definition methodIsEasyForRuleMethodReachability(method f) returns bool = f.isView ||
+	     f.selector == sig:PoolHarness.getUserEMode(address).selector ||
+	     f.selector == sig:PoolHarness.mintUnbacked(address,uint256,address,uint16).selector ||
+	     f.selector == sig:PoolHarness.getUserConfiguration(address).selector ||
+	     f.selector == sig:PoolHarness.finalizeTransfer(address,address,address,uint256,uint256,uint256).selector ||
+	     // f.selector == sig:PoolHarness.POOL_REVISION().selector || // view function
+	     f.selector == sig:PoolHarness.supply(address,uint256,address,uint16).selector ||
+	     f.selector == sig:PoolHarness.getReserveAddressById(uint16).selector ||
+	     f.selector == sig:PoolHarness.isStableRateEnabled(address).selector ||
+	     f.selector == sig:PoolHarness.updateFlashloanPremiums(uint128,uint128).selector ||
+	     f.selector == sig:PoolHarness.cumulateToLiquidityIndex(address,uint256,uint256).selector ||
+	     f.selector == sig:PoolHarness.deposit(address,uint256,address,uint16).selector ||
+	     // f.selector == sig:PoolHarness.FLASHLOAN_PREMIUM_TOTAL().selector || // view function
+	     f.selector == sig:PoolHarness.swapBorrowRateMode(address,uint256).selector ||
+	     f.selector == sig:PoolHarness.getReserveNormalizedVariableDebt(address).selector ||
+	     f.selector == sig:PoolHarness.getReserveVariableBorrowIndex(address).selector ||
+	     f.selector == sig:PoolHarness.withdraw(address,uint256,address).selector ||
+	     // f.selector == sig:PoolHarness.FLASHLOAN_PREMIUM_TO_PROTOCOL().selector || // view function
+	     f.selector == sig:PoolHarness.dropReserve(address).selector ||
+	     f.selector == sig:PoolHarness.ballanceOfInAsset(address,address).selector ||
+	     f.selector == sig:PoolHarness.setConfiguration(address, DataTypes.ReserveConfigurationMap).selector ||
+	     f.selector == sig:PoolHarness.setUserEMode(uint8).selector ||
+	     f.selector == sig:PoolHarness.getReserveLiquidityIndex(address).selector ||
+	     f.selector == sig:PoolHarness.updateReserveIndexesWithCache(address,DataTypes.ReserveCache).selector ||
+	     // f.selector == sig:PoolHarness.MAX_STABLE_RATE_BORROW_SIZE_PERCENT().selector || // view function
+	     // f.selector == sig:PoolHarness.getReservesList().selector || // view function
+	     // f.selector == sig:PoolHarness.getAvailableLiquidity(address).selector || // view function
+	     // f.selector == sig:PoolHarness.getUserAccountData(address).selector || // view function
+	     f.selector == sig:PoolHarness.rescueTokens(address,address,uint256).selector ||
+	     // f.selector == sig:PoolHarness.getReserveStableBorrowRate(address).selector || // view function
+	     // f.selector == sig:PoolHarness.MAX_NUMBER_RESERVES().selector || // view function
+	     // f.selector == sig:PoolHarness.getVariableRateConstant().selector || // view function
+	     f.selector == sig:PoolHarness.configureEModeCategory(uint8,DataTypes.EModeCategory).selector ||
+	     f.selector == sig:PoolHarness.mintToTreasury(address[]).selector ||
+	     f.selector == sig:PoolHarness.updateBridgeProtocolFee(uint256).selector ||
+	     f.selector == sig:PoolHarness.setUserUseReserveAsCollateral(address,bool).selector ||
+	     // f.selector == sig:PoolHarness.getConfiguration(address).selector || // view function
+	     // f.selector == sig:PoolHarness.getTotalDebt(address).selector || // view function
+	     // f.selector == sig:PoolHarness.getStableRateConstant().selector || // view function
+	     // f.selector == sig:PoolHarness.getReserveNormalizedIncome(address).selector || // view function
+	     f.selector == sig:PoolHarness.setReserveInterestRateStrategyAddress(address,address).selector ||
+	     // f.selector == sig:PoolHarness.ADDRESSES_PROVIDER().selector || // view function
+	     f.selector == sig:PoolHarness.initReserve(address,address,address,address,address).selector ||
+	     // f.selector == sig:PoolHarness.getStableRate(address).selector || // view function
+	     f.selector == sig:PoolHarness.resetIsolationModeTotalDebt(address).selector ||
+	     // f.selector == sig:PoolHarness.getTotalATokenSupply(address).selector || // view function
+	     // f.selector == sig:PoolHarness.getCurrScaledVariableDebt(address).selector || // view function
+	     f.selector == sig:PoolHarness.initialize(address).selector ||
+	     // f.selector == sig:PoolHarness.getReserveVariableBorrowRate(address).selector || // view function
+	     // f.selector == sig:PoolHarness.getEModeCategoryData(uint8).selector || // view function
+	     f.selector == sig:PoolHarness.BRIDGE_PROTOCOL_FEE().selector ||
+	     // f.selector == sig:PoolHarness.getReserveData(address).selector || // view function
+	     f.selector == sig:PoolHarness.updateReserveIndexes(address).selector;
+
+rule method_reachability_split_for_CI_01(env e, method f, calldataarg args) filtered {
+    f -> methodIsEasyForRuleMethodReachability(f)
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_02_backUnbacked(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.backUnbacked(address,uint256,uint256).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_03_repayWithATokens(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.repayWithATokens(address,uint256,uint256).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_04_repayWithPermit(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.repayWithPermit(address,uint256,uint256,address,uint256,uint8,bytes32,bytes32).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_05_liquidationCall(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.liquidationCall(address,address,address,uint256,bool).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_06_flashLoan(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.flashLoan(address,address[],uint256[],uint256[],address,bytes,uint16).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_07_borrow(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.borrow(address,uint256,uint256,uint16,address).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_08_supplyWithPermit(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.supplyWithPermit(address,uint256,address,uint16,uint256,uint8,bytes32,bytes32).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_09_rebalanceStableBorrowRate(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.rebalanceStableBorrowRate(address,address).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_10_repay(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.repay(address,uint256,uint256,address).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
+rule method_reachability_split_for_CI_11_flashLoanSimple(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:PoolHarness.flashLoanSimple(address,address,uint256,bytes,uint16).selector
+} {
+    f(e, args);
+    satisfy true;
+}
+
 // @title It is impossible to deposit an inactive reserve
 // Proved:
 // https://prover.certora.com/output/40577/b8bd6244053e42e4bddb129f04e1dd93/?anonymousKey=5374001e512e1149d120f0efa19c18a3d531d115