diff --git a/certora/confs/DistinctIdentifiers.conf b/certora/confs/DistinctIdentifiers.conf index a14ba101..59de60bc 100644 --- a/certora/confs/DistinctIdentifiers.conf +++ b/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", diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf index c2e22bc5..7db7a5e8 100644 --- a/certora/confs/PendingValues.conf +++ b/certora/confs/PendingValues.conf @@ -9,7 +9,7 @@ "prover_args": [ "-depth 3", "-mediumTimeout 20", - "-timeout 300", + "-timeout 3600", ], "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index a3407b2b..15b75556 100644 --- a/certora/confs/Reverts.conf +++ b/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", diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf index c98a9ae8..e80470a5 100644 --- a/certora/confs/Timelock.conf +++ b/certora/confs/Timelock.conf @@ -16,7 +16,7 @@ "prover_args": [ "-depth 3", "-mediumTimeout 20", - "-timeout 300", + "-timeout 3600", ], "rule_sanity": "basic", "server": "production", diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index be81fb49..7e825094 100644 --- a/certora/specs/ConsistentState.spec +++ b/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; diff --git a/certora/specs/DistinctIdentifiers.spec b/certora/specs/DistinctIdentifiers.spec index 272b7c80..074199ee 100644 --- a/certora/specs/DistinctIdentifiers.spec +++ b/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]); diff --git a/certora/specs/Enabled.spec b/certora/specs/Enabled.spec index 237d716d..65210cfc 100644 --- a/certora/specs/Enabled.spec +++ b/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) { diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec index a7a75001..4fee4e59 100644 --- a/certora/specs/LastUpdated.spec +++ b/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 { diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index fe3160e5..27bf9cc9 100644 --- a/certora/specs/Liveness.spec +++ b/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); diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec index cbfc6d09..43be7d52 100644 --- a/certora/specs/MarketInteractions.spec +++ b/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; diff --git a/certora/specs/PendingValues.spec b/certora/specs/PendingValues.spec index 698bdc98..f04e84f4 100644 --- a/certora/specs/PendingValues.spec +++ b/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; } diff --git a/certora/specs/Range.spec b/certora/specs/Range.spec index 0d225395..f5df8854 100644 --- a/certora/specs/Range.spec +++ b/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(); diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 5394efe9..b8e66951 100644 --- a/certora/specs/Reverts.spec +++ b/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; diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec index e5d38c9b..734e93e3 100644 --- a/certora/specs/Timelock.spec +++ b/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); diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec index 703e874c..0c4eca41 100644 --- a/certora/specs/Tokens.spec +++ b/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);