Merge pull request #411 from morpho-org/certora/distinct-performance

[Certora] Fix solver setup

certora/confs/DistinctIdentifiers.conf

@@ -7,7 +7,7 @@
     "loop_iter": "2",
     "optimistic_loop": true,
     "prover_args": [
-        "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]",
+        "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]",
         "-depth 3",
         "-mediumTimeout 20",
         "-timeout 2000",

certora/confs/PendingValues.conf

@@ -9,7 +9,7 @@
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
-        "-timeout 300",
+        "-timeout 3600",
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/confs/Reverts.conf

@@ -18,9 +18,14 @@
     "loop_iter": "2",
     "optimistic_loop": true,
     "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
+        "-depth 5",
+        "-mediumTimeout 40",
+        "-newSplitParallel true",
+        "-splitParallelInitialDepth 4",
+        "-splitParallelTimelimit 7000",
+        "-adaptiveSolverConfig false",
+        "-smt_nonLinearArithmetic true",
+        "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/confs/Timelock.conf

@@ -16,7 +16,7 @@
     "prover_args": [
         "-depth 3",
         "-mediumTimeout 20",
-        "-timeout 300",
+        "-timeout 3600",
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/specs/ConsistentState.spec

@@ -71,10 +71,6 @@ function isNotEnabledIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool
 invariant notEnabledIsNotMarkedForRemoval(MetaMorphoHarness.Id id)
     isNotEnabledIsNotMarkedForRemoval(id);
 
-function hasPendingCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool {
-    return pendingCap_(id).validAt > 0 => config_(id).removableAt == 0;
-}
-
 // Check that a market with a pending cap cannot be marked for removal.
 invariant pendingCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id)
-    hasPendingCapIsNotMarkedForRemoval(id);
+    pendingCap_(id).validAt > 0 => config_(id).removableAt == 0;

certora/specs/DistinctIdentifiers.spec

@@ -1,13 +1,9 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "PendingValues.spec";
 
-function hasDistinctIdentifiers(uint256 i, uint256 j) returns bool {
-    return i != j => withdrawQueue(i) != withdrawQueue(j);
-}
-
 // Check that there are no duplicate markets in the withdraw queue.
 invariant distinctIdentifiers(uint256 i, uint256 j)
-    hasDistinctIdentifiers(i, j)
+    i != j => withdrawQueue(i) != withdrawQueue(j)
 {
     preserved updateWithdrawQueue(uint256[] indexes) with (env e) {
         requireInvariant distinctIdentifiers(indexes[i], indexes[j]);

certora/specs/Enabled.spec

@@ -20,8 +20,7 @@ rule inWithdrawQueueIsEnabledPreservedUpdateWithdrawQueue(env e, uint256 i, uint
     uint256 j;
     require isInWithdrawQueueIsEnabled(indexes[i]);
 
-    // Safe require because it is a verified invariant.
-    require hasDistinctIdentifiers(indexes[i], j);
+    requireInvariant distinctIdentifiers(indexes[i], j);
 
     updateWithdrawQueue(e, indexes);
 
@@ -45,13 +44,9 @@ function isWithdrawRankCorrect(MetaMorphoHarness.Id id) returns bool {
 invariant withdrawRankCorrect(MetaMorphoHarness.Id id)
     isWithdrawRankCorrect(id);
 
-function isEnabledHasPositiveRank(MetaMorphoHarness.Id id) returns bool {
-    return config_(id).enabled => withdrawRank(id) > 0;
-}
-
 // Checks that enabled markets have a positive withdraw rank, according to the withdrawRank ghost variable.
 invariant enabledHasPositiveRank(MetaMorphoHarness.Id id)
-    isEnabledHasPositiveRank(id);
+    config_(id).enabled => withdrawRank(id) > 0;
 
 // Check that enabled markets are in the withdraw queue.
 rule enabledIsInWithdrawQueue(MetaMorphoHarness.Id id) {

certora/specs/LastUpdated.spec

@@ -20,7 +20,7 @@ function hasGuardianRole(address user) returns bool {
 }
 
 // Check that any market with positive cap is created on Morpho Blue.
-// The corresponding invariant cannot be verified because it requires to check properties on MetaMorpho and on Blue at the same time:
+// The corresponding invariant is difficult to verify because it requires to check properties on MetaMorpho and on Blue at the same time:
 // - on MetaMorpho, that it holds when the cap is positive for the first time
 // - on Blue, that a created market always has positive last update
 function hasPositiveSupplyCapIsUpdated(MetaMorphoHarness.Id id) returns bool {

certora/specs/Liveness.spec

@@ -27,11 +27,9 @@ rule canPauseSupply() {
 rule canForceRemoveMarket(MetaMorphoHarness.MarketParams marketParams) {
     MetaMorphoHarness.Id id = Util.libId(marketParams);
 
-    // Safe require because it is a verified invariant.
-    require hasSupplyCapIsEnabled(id);
-    // Safe require because it is a verified invariant.
-    require isEnabledHasConsistentAsset(marketParams);
-    // Safe require because it is a verified invariant.
+    requireInvariant supplyCapIsEnabled(id);
+    requireInvariant enabledHasConsistentAsset(marketParams);
+    // Safe require because this holds as an invariant.
     require hasPositiveSupplyCapIsUpdated(id);
 
     MetaMorphoHarness.MarketConfig config = config_(id);
@@ -55,8 +53,7 @@ rule canForceRemoveMarket(MetaMorphoHarness.MarketParams marketParams) {
     assert !lastReverted;
 
     require e3.msg.value == 0;
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
     // Safe require as it corresponds to some time very far into the future.
     require e3.block.timestamp < 2^63;
     submitMarketRemoval@withrevert(e3, marketParams);

certora/specs/MarketInteractions.spec

@@ -27,8 +27,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
     assert data.length == 0;
 
     MetaMorphoHarness.Id id = Util.libId(marketParams);
-    // Safe require because it is a verified invariant
-    require hasSupplyCapIsEnabled(id);
+    requireInvariant supplyCapIsEnabled(id);
 
     // Check that all markets on which MetaMorpho supplies are enabled markets.
     assert config_(id).enabled;
@@ -44,8 +43,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
 
     MetaMorphoHarness.Id id = Util.libId(marketParams);
     uint256 index = lastIndexWithdraw();
-    // Safe require because it is a verified invariant.
-    require isInWithdrawQueueIsEnabled(index);
+    requireInvariant inWithdrawQueueIsEnabled(index);
 
     // Check that all markets from which MetaMorpho withdraws are enabled markets.
     assert config_(id).enabled;

certora/specs/PendingValues.spec

@@ -12,26 +12,19 @@ invariant noBadPendingTimelock()
     hasNoBadPendingTimelock()
 {
     preserved with (env e) {
-        // Safe require because it is a verified invariant.
-        require isTimelockInRange();
+        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the future.
         require e.block.timestamp < 2^63;
     }
 }
 
-function isSmallerPendingTimelock() returns bool {
-    return assert_uint256(pendingTimelock_().value) < timelock();
-}
-
 // Check that the pending timelock value is always strictly smaller than the current timelock value.
 invariant smallerPendingTimelock()
-    isSmallerPendingTimelock()
+    assert_uint256(pendingTimelock_().value) < timelock()
 {
     preserved {
-        // safe require as it is a verified invariant.
-        require isPendingTimelockInRange();
-        // Safe require because it is a verified invariant.
-        require isTimelockInRange();
+        requireInvariant pendingTimelockInRange();
+        requireInvariant timelockInRange();
     }
 }
 
@@ -46,8 +39,7 @@ invariant noBadPendingCap(MetaMorphoHarness.Id id)
     hasNoBadPendingCap(id)
 {
     preserved with (env e) {
-        // Safe require because it is a verified invariant.
-        require isTimelockInRange();
+        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the future.
         require e.block.timestamp < 2^63;
     }
@@ -76,8 +68,7 @@ invariant noBadPendingGuardian()
     hasNoBadPendingGuardian()
 {
     preserved with (env e) {
-        // Safe require because it is a verified invariant.
-        require isTimelockInRange();
+        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the future.
         require e.block.timestamp < 2^63;
     }

certora/specs/Range.spec

@@ -41,13 +41,9 @@ function isPendingTimelockInRange() returns bool {
 invariant pendingTimelockInRange()
     isPendingTimelockInRange();
 
-function isTimelockInRange() returns bool {
-    return timelock() <= maxTimelock() && timelock() >= minTimelock();
-}
-
 // Check that the timelock is bounded by the min timelock and the max timelock.
 invariant timelockInRange()
-    isTimelockInRange()
+    timelock() <= maxTimelock() && timelock() >= minTimelock()
 {
     preserved {
         requireInvariant pendingTimelockInRange();

certora/specs/Reverts.spec

@@ -83,8 +83,7 @@ rule submitGuardianRevertCondition(env e, address newGuardian) {
     address oldGuardian = guardian();
     uint64 pendingGuardianValidAt = pendingGuardian_().validAt;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
     // Safe require as it corresponds to some time very far into the future.
     require e.block.timestamp < 2^63;
 
@@ -107,12 +106,10 @@ rule submitCapRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams
     uint256 pendingCapValidAt = pendingCap_(id).validAt;
     MetaMorphoHarness.MarketConfig config = config_(id);
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
     // Safe require as it corresponds to some time very far into the future.
     require e.block.timestamp < 2^63;
-    // Safe require because it is a verified invariant.
-    require hasSupplyCapIsEnabled(id);
+    requireInvariant supplyCapIsEnabled(id);
 
     submitCap@withrevert(e, marketParams, newSupplyCap);
 
@@ -135,8 +132,7 @@ rule submitMarketRemovalRevertCondition(env e, MetaMorphoHarness.MarketParams ma
     uint256 pendingCapValidAt = pendingCap_(id).validAt;
     MetaMorphoHarness.MarketConfig config = config_(id);
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
     // Safe require as it corresponds to some time very far into the future.
     require e.block.timestamp < 2^63;
 

certora/specs/Timelock.spec

@@ -29,10 +29,8 @@ rule nextGuardianUpdateTimeDoesNotRevert() {
     env e;
     require e.msg.value == 0;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
-    // Safe require because it is a verified invariant.
-    require isPendingTimelockInRange();
+    requireInvariant timelockInRange();
+    requireInvariant pendingTimelockInRange();
 
     nextGuardianUpdateTime@withrevert(e);
 
@@ -44,8 +42,7 @@ rule guardianUpdateTime(env e_next, method f, calldataarg args) {
     // The environment e yields the current time.
     env e;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
 
     uint256 nextTime = nextGuardianUpdateTime(e);
     address prevGuardian = guardian();
@@ -73,10 +70,8 @@ rule nextCapIncreaseTimeDoesNotRevert(MetaMorphoHarness.Id id) {
     env e;
     require e.msg.value == 0;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
-    // Safe require because it is a verified invariant.
-    require isPendingTimelockInRange();
+    requireInvariant timelockInRange();
+    requireInvariant pendingTimelockInRange();
 
     nextCapIncreaseTime@withrevert(e, id);
 
@@ -90,8 +85,7 @@ rule capIncreaseTime(env e_next, method f, calldataarg args) {
 
     MetaMorphoHarness.Id id;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
 
     uint256 nextTime = nextCapIncreaseTime(e, id);
     uint184 prevCap = config_(id).cap;
@@ -117,10 +111,8 @@ rule nextTimelockDecreaseTimeDoesNotRevert() {
     env e;
     require e.msg.value == 0;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
-    // Safe require because it is a verified invariant.
-    require isPendingTimelockInRange();
+    requireInvariant timelockInRange();
+    requireInvariant pendingTimelockInRange();
 
     nextTimelockDecreaseTime@withrevert(e);
 
@@ -132,8 +124,7 @@ rule timelockDecreaseTime(env e_next, method f, calldataarg args) {
     // The environment e yields the current time.
     env e;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
 
     uint256 nextTime = nextTimelockDecreaseTime(e);
     uint256 prevTimelock = timelock();
@@ -159,10 +150,8 @@ rule nextRemovableTimeDoesNotRevert(MetaMorphoHarness.Id id) {
     env e;
     require e.msg.value == 0;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
-    // Safe require because it is a verified invariant.
-    require isPendingTimelockInRange();
+    requireInvariant timelockInRange();
+    requireInvariant pendingTimelockInRange();
 
     nextRemovableTime@withrevert(e, id);
 
@@ -178,8 +167,7 @@ rule removableTime(env e_next, method f, calldataarg args) {
 
     MetaMorphoHarness.Id id;
 
-    // Safe require because it is a verified invariant.
-    require isTimelockInRange();
+    requireInvariant timelockInRange();
 
     uint256 nextTime = nextRemovableTime(e, id);
 

certora/specs/Tokens.spec

@@ -31,10 +31,8 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse
     assert onBehalf == currentContract;
     assert data.length == 0;
 
-    // Safe require because it is a verified invariant.
-    require hasSupplyCapIsEnabled(Util.libId(marketParams));
-    // Safe require because it is a verified invariant.
-    require isEnabledHasConsistentAsset(marketParams);
+    requireInvariant supplyCapIsEnabled(Util.libId(marketParams));
+    requireInvariant enabledHasConsistentAsset(marketParams);
 
     // Summarize supply as just a transfer for the purpose of this specification file, which is sound because only the properties about tokens are verified in this file.
     Util.safeTransferFrom(marketParams.loanToken, currentContract, MORPHO(), assets);
@@ -50,8 +48,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
 
     // Safe require because it is verifed in MarketInteractions.
     require config_(id).enabled;
-    // Safe require because it is a verified invariant.
-    require isEnabledHasConsistentAsset(marketParams);
+    requireInvariant enabledHasConsistentAsset(marketParams);
 
     // Use effective withdrawn assets if shares are given as input.
     uint256 withdrawn = Util.withdrawnAssets(MORPHO(), id, assets, shares);