Merge pull request #10 from aave-dao/fix/cleanup

fix: cleanup and added more tests
Certora · Apr 12, 2024 · cf6e2ac · cf6e2ac
2 parents 3c48610 + 910e4c8
commit cf6e2ac
Show file tree

Hide file tree

Showing 28 changed files with 1,546 additions and 1,388 deletions.
diff --git a/.gitignore b/.gitignore
@@ -21,4 +21,12 @@ node_modules
 # ignore foundry deploy artifacts
 broadcast/
 
-.DS_Store
+.DS_Store
+
+# certora
+.certora*
+.certora*.json
+**.last_conf*
+certora-logs
+certora_debug_log.txt
+resource_errors.json
diff --git a/certora/README.md b/certora/README.md
@@ -28,6 +28,8 @@ root directory:
 bash certora/scripts/run-all.sh
 ```
 
+_Note: When running the rules locally, please remove the solc version from the `.conf` files as when using solc-select solc version should not be specified in `.conf`_
+
 After the jobs are complete, the results will be available on
 [the staging Certora portal](https://prover.certora.com/).
 

diff --git a/certora/conf/AToken.conf b/certora/conf/AToken.conf
@@ -1,15 +1,15 @@
 {
-    "files": [
-        "certora/harness/ATokenHarness.sol",
-        "certora/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/specs/AToken.spec",
-    "msg": "aToken spec"
- }
+  "files": [
+    "certora/harness/ATokenHarness.sol",
+    "certora/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/specs/AToken.spec",
+  "msg": "aToken spec"
+}
diff --git a/certora/conf/NEW-pool-no-summarizations.conf b/certora/conf/NEW-pool-no-summarizations.conf
@@ -1,40 +1,41 @@
 {
-    "files": [
-        "certora/harness/ATokenHarness.sol",
-        "certora/harness/PoolHarness.sol",
-        "certora/harness/StableDebtTokenHarness.sol",
-        "certora/harness/SimpleERC20.sol",
-        "src/core/instances/VariableDebtTokenInstance.sol",
-        "src/core/contracts/misc/AaveProtocolDataProvider.sol",
-        "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol",
-        "src/core/contracts/protocol/configuration/ACLManager.sol",
-        "src/core/contracts/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
-        "src/core/contracts/protocol/configuration/PriceOracleSentinel.sol",
-        "src/core/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:stableDebtTokenAddress=StableDebtTokenHarness",
-        "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/specs/NEW-pool-no-summarizations.spec",
-    "rule": ["liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
-             "depositUpdatesUserATokenSuperBalance",
-             "depositCannotChangeOthersATokenSuperBalance"
-            ],
-    "parametric_contracts": ["PoolHarness"],
-    "msg": "pool-no-summarizations::partial rules",
+  "files": [
+    "certora/harness/ATokenHarness.sol",
+    "certora/harness/PoolHarness.sol",
+    "certora/harness/StableDebtTokenHarness.sol",
+    "certora/harness/SimpleERC20.sol",
+    "src/core/instances/VariableDebtTokenInstance.sol",
+    "src/core/contracts/misc/AaveProtocolDataProvider.sol",
+    "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol",
+    "src/core/contracts/protocol/configuration/ACLManager.sol",
+    "src/core/contracts/protocol/libraries/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
+    "src/core/contracts/protocol/configuration/PriceOracleSentinel.sol",
+    "src/core/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:stableDebtTokenAddress=StableDebtTokenHarness",
+    "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/specs/NEW-pool-no-summarizations.spec",
+  "rule": [
+    "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
+    "depositUpdatesUserATokenSuperBalance",
+    "depositCannotChangeOthersATokenSuperBalance"
+  ],
+  "parametric_contracts": ["PoolHarness"],
+  "msg": "pool-no-summarizations::partial rules",
 }
diff --git a/certora/conf/NEW-pool-simple-properties.conf b/certora/conf/NEW-pool-simple-properties.conf
@@ -1,42 +1,43 @@
 {
-    "files": [
-        "certora/harness/ATokenHarness.sol",
-        "certora/harness/PoolHarness.sol",
-        "certora/harness/StableDebtTokenHarness.sol",
-        "certora/harness/SimpleERC20.sol",
-        "src/core/instances/VariableDebtTokenInstance.sol",
-        "src/core/contracts/misc/AaveProtocolDataProvider.sol",
-        "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol",
-        "src/core/contracts/protocol/libraries/types/DataTypes.sol",
-        "src/core/contracts/protocol/configuration/PoolAddressesProvider.sol",
-    ],
-    "link": [
-        "ATokenHarness:POOL=PoolHarness",
-        "ATokenHarness:_underlyingAsset=SimpleERC20",
-        "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
-    ],
-    "struct_link": [
-        "PoolHarness:aTokenAddress=ATokenHarness",
-        "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
-        "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/specs/NEW-pool-simple-properties.spec",
-    "rule": ["cannotDepositInInactiveReserve",
-            "cannotDepositInFrozenReserve",
-            "cannotDepositZeroAmount",
-            "cannotWithdrawZeroAmount",
-            "cannotWithdrawFromInactiveReserve",
-            "cannotBorrowZeroAmount",
-            "cannotBorrowOnInactiveReserve",
-            "cannotBorrowOnReserveDisabledForBorrowing",
-            "cannotBorrowOnFrozenReserve"
-            ],
-    "parametric_contracts": ["PoolHarness"],
-    "msg": "pool-simple-properties::ALL",
+  "files": [
+    "certora/harness/ATokenHarness.sol",
+    "certora/harness/PoolHarness.sol",
+    "certora/harness/StableDebtTokenHarness.sol",
+    "certora/harness/SimpleERC20.sol",
+    "src/core/instances/VariableDebtTokenInstance.sol",
+    "src/core/contracts/misc/AaveProtocolDataProvider.sol",
+    "src/core/contracts/protocol/pool/DefaultReserveInterestRateStrategyV2.sol",
+    "src/core/contracts/protocol/libraries/types/DataTypes.sol",
+    "src/core/contracts/protocol/configuration/PoolAddressesProvider.sol",
+  ],
+  "link": [
+    "ATokenHarness:POOL=PoolHarness",
+    "ATokenHarness:_underlyingAsset=SimpleERC20",
+    "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+  ],
+  "struct_link": [
+    "PoolHarness:aTokenAddress=ATokenHarness",
+    "PoolHarness:stableDebtTokenAddress=StableDebtTokenHarness",
+    "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/specs/NEW-pool-simple-properties.spec",
+  "rule": [
+    "cannotDepositInInactiveReserve",
+    "cannotDepositInFrozenReserve",
+    "cannotDepositZeroAmount",
+    "cannotWithdrawZeroAmount",
+    "cannotWithdrawFromInactiveReserve",
+    "cannotBorrowZeroAmount",
+    "cannotBorrowOnInactiveReserve",
+    "cannotBorrowOnReserveDisabledForBorrowing",
+    "cannotBorrowOnFrozenReserve"
+  ],
+  "parametric_contracts": ["PoolHarness"],
+  "msg": "pool-simple-properties::ALL",
 }
diff --git a/certora/conf/ReserveConfiguration.conf b/certora/conf/ReserveConfiguration.conf
@@ -1,14 +1,14 @@
 {
-    "files": [
-        "certora/harness/ReserveConfigurationHarness.sol"
-    ],
-    "msg": "ReserveConfiguration",
-    "optimistic_loop": true,
-    "process": "emv",
-    "prover_args": [
-        "-useBitVectorTheory"
-    ],
-    "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
-    "solc": "solc8.19",
-    "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
-}
+  "files": [
+    "certora/harness/ReserveConfigurationHarness.sol"
+  ],
+  "msg": "ReserveConfiguration",
+  "optimistic_loop": true,
+  "process": "emv",
+  "prover_args": [
+    "-useBitVectorTheory"
+  ],
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
+  "solc": "solc8.19",
+  "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
+}
diff --git a/certora/conf/StableDebtToken.conf b/certora/conf/StableDebtToken.conf
@@ -1,18 +1,18 @@
 //===================================================================================
 //  IMPORTANT:
-//  This file can be DELETED, since Stable coins are removed. 
+//  This file can be DELETED, since Stable coins are removed.
 //  In the implementation all the function either revert or return 0
 //  ===================================================================================
 
 {
-    "cache": "StableToken",
-    "files": [
-        "certora/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness"
-    ],
-    "loop_iter": "4",
-    "msg": "stableTokenCLI",
-    "optimistic_loop": true,
-    "process": "emv",
-    "solc": "solc8.19",
-    "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
-}
+  "cache": "StableToken",
+  "files": [
+    "certora/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness"
+  ],
+  "loop_iter": "4",
+  "msg": "stableTokenCLI",
+  "optimistic_loop": true,
+  "process": "emv",
+  "solc": "solc8.19",
+  "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
+}
diff --git a/certora/conf/UserConfiguration.conf b/certora/conf/UserConfiguration.conf
@@ -1,15 +1,15 @@
 {
-    "files": [
-        "certora/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": [
-        "-useBitVectorTheory"
-    ],
-    "solc": "solc8.19",
-    "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
-}
+  "files": [
+    "certora/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": [
+    "-useBitVectorTheory"
+  ],
+  "solc": "solc8.19",
+  "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
+}
diff --git a/certora/conf/VariableDebtToken.conf b/certora/conf/VariableDebtToken.conf
@@ -1,11 +1,11 @@
 {
-    "files": [
-        "certora/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",
-    "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
-}
+  "files": [
+    "certora/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",
+  "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
+}