Merge branch 'certora' of github.com:Certora/aave-v3-core into certora

.github/workflows/certora.yml

@@ -58,7 +58,7 @@ jobs:
       matrix:
         rule:
           - AToken.conf
-          - Pool.conf
+          - PoolAccurate.conf
           - ReserveConfiguration.conf
           - StableTokenCLI.conf
           - UserConfigCLI.conf

certora/conf/PoolSimpleProperties.conf

@@ -0,0 +1,38 @@
+{
+    "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",
+        "certora/munged/protocol/libraries/configuration/ReserveConfiguration.sol",
+        "certora/munged/protocol/pool/DefaultReserveInterestRateStrategy.sol",
+        "certora/munged/protocol/configuration/PoolAddressesProvider.sol",
+        "certora/munged/protocol/configuration/ACLManager.sol",
+        // "certora/munged/protocol/libraries/types/DataTypes.sol",
+        "certora/munged/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
+        "certora/munged/protocol/configuration/PriceOracleSentinel.sol",
+    ],
+    "link": [
+        "ATokenHarness:POOL=PoolHarness",
+        "ATokenHarness:_underlyingAsset=SimpleERC20",
+        "VariableDebtToken:POOL=PoolHarness",
+        "AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider",
+        "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+    ],
+    "struct_link": [
+        "PoolHarness:aTokenAddress=ATokenHarness",
+        "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
+        "PoolHarness:variableDebtTokenAddress=VariableDebtToken",
+        "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategy",
+    ],
+    "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.10",
+    "verify": "PoolHarness:certora/specs/pool-simple-properties.spec",
+    "msg": "Pool, normalized_income_changes_with",
+    "parametric_contracts": ["PoolHarness"],
+}