Fix simple properties spec

Certora · Dec 11, 2023 · 3236b98 · 3236b98
1 parent 933fab2
commit 3236b98
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 77 deletions.
diff --git a/certora/conf/PoolInvariant.conf b/certora/conf/PoolInvariant.conf
@@ -28,7 +28,8 @@
     "prover_args": ["-depth 120"], // 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, supply_gte_debt",
+    // "msg": "Pool, try cannotDepositInInactiveReserve",
+    // "rule": ["cannotDepositInInactiveReserve"],
     "parametric_contracts": ["PoolHarness"],
     // "method": "liquidationCall(address,address,address,uint256,bool)",
 }
diff --git a/certora/conf/PoolSimpleProperties.conf b/certora/conf/PoolSimpleProperties.conf
@@ -6,13 +6,10 @@
         "certora/harness/SimpleERC20.sol",
         "certora/munged/protocol/tokenization/VariableDebtToken.sol",
         "certora/munged/misc/AaveProtocolDataProvider.sol",
-        "certora/munged/protocol/libraries/configuration/ReserveConfiguration.sol",
+        // "certora/munged/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",
+        "certora/munged/protocol/configuration/ACLManager.sol"
     ],
     "link": [
         "ATokenHarness:POOL=PoolHarness",
@@ -30,6 +27,8 @@
     "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",
+    // "rule": ["cannotDepositInInactiveReserve"],
     "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",

diff --git a/certora/specs/pool-simple-properties.spec b/certora/specs/pool-simple-properties.spec
@@ -1,80 +1,11 @@
 import "pool-base.spec";
 
 methods {
-    // math
-    // function _.rayMul(uint256 a, uint256 b) internal => NONDET;
-    // function _.rayDiv(uint256 a, uint256 b) internal => NONDET;
-    // function _.percentMul(uint256 value, uint256 percentage) internal => NONDET;
     function _._getUserDebtInBaseCurrency(address user, DataTypes.ReserveData storage reserve, uint256 assetPrice, uint256 assetUnit) internal => NONDET;
-    // function _.rayMul(uint256 a, uint256 b) internal => rayMulSummariztion(a, b) expect uint256 ALL;
-    // function _.rayDiv(uint256 a, uint256 b) internal => rayDivSummariztion(a, b) expect uint256 ALL;
-
     function _.rayMul(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, b, 10^27) expect uint256 ALL;
     function _.rayDiv(uint256 a, uint256 b) internal => mulDivDownAbstractPlus(a, 10^27, b) expect uint256 ALL;
-    // function _.rayDiv(uint256 a, uint256 b) internal => NONDET; //JB UC
-    function _.getFlags(DataTypes.ReserveConfigurationMap memory self) internal => NONDET;
-}
-
-ghost mapping(uint256 => mapping(uint256 => uint256)) rayMulSummariztionValues;
-ghost mapping(uint256 => mapping(uint256 => uint256)) rayDivSummariztionValues;
-
-function rayMulSummariztion(uint256 x, uint256 y) returns uint256
-{
-	if (x == 0) || (y == 0)
-	{
-		return 0;
-	}
-	if (x == RAY())
-	{
-		return y;
-	}
-	if (y == RAY())
-	{
-		return x;
-	}
-
-	if (y > x)
-	{
-		if (y > RAY())
-		{
-			require rayMulSummariztionValues[y][x] >= x;
-		}
-		if (x > RAY())
-		{
-			require rayMulSummariztionValues[y][x] >= y;
-		}
-		return rayMulSummariztionValues[y][x];
-	}
-	else{
-		if (x > RAY())
-		{
-			require rayMulSummariztionValues[x][y] >= y;
-		}
-		if (y > RAY())
-		{
-			require rayMulSummariztionValues[x][y] >= x;
-		}
-		return rayMulSummariztionValues[x][y];
-	}
-}
-
-function rayDivSummariztion(uint256 x, uint256 y) returns uint256
-{
-	if (x == 0)
-	{
-		return 0;
-	}
-	if (y == RAY())
-	{
-		return x;
-	}
-	if (y == x)
-	{
-		return RAY();
-	}
-	require y > RAY() => rayDivSummariztionValues[x][y] <= x;
-	require y < RAY() => x <= rayDivSummariztionValues[x][y];
-	return rayDivSummariztionValues[x][y];
+    // function _.getFlags(DataTypes.ReserveConfigurationMap memory self) internal => NONDET;
+	// function _.calculateInterestRates(DataTypes.CalculateInterestRatesParams params) external => NONDET;
 }
 
 // Passing for PoolHarness:

diff --git a/certora/specs/pool.spec b/certora/specs/pool.spec
@@ -289,6 +289,7 @@ function aTokenBalanceOf(env e, address user) returns uint256
 // }
 
 
+
 // @title P19: It's not possible to borrow with an interest rate mode that is different than 1 (stable) or 2 (variable)
 // Passing: https://prover.certora.com/output/31688/5cb1398883fb4162854b74af0bae79e9/?anonymousKey=0d7f3c6dc8249ba58a6af0d749ac7c9782611817
 rule borrowOnlyVariableOrStableRate(env e) {