[Certora] First liveness properties

.github/workflows/certora.yml

@@ -20,6 +20,8 @@ jobs:
           - DistinctIdentifiers
           - Enabled
           - Immutability
+          - LastUpdated
+          - Liveness
           - PendingValues
           - Range
           - Reentrancy

certora/confs/ConsistentState.conf

@@ -1,7 +1,15 @@
 {
     "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/harness/MetaMorphoHarness.sol",
     ],
+    "parametric_contracts": [
+        "MetaMorphoHarness",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc8.19",
+        "MetaMorphoHarness": "solc",
+    },
     "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

certora/confs/DistinctIdentifiers.conf

@@ -9,7 +9,7 @@
         "-solvers [z3:lia2,cvc5:nonlinNoDio,cvc4:nonlin,yices:def,z3:arith2]",
         "-depth 3",
         "-mediumTimeout 20",
-        "-timeout 1000",
+        "-timeout 2000",
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/confs/LastUpdated.conf

@@ -0,0 +1,24 @@
+{
+    "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/harness/MetaMorphoHarness.sol",
+    ],
+    "parametric_contracts": [
+        "MetaMorphoHarness",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc8.19",
+        "MetaMorphoHarness": "solc",
+    },
+    "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 300",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Last Updated"
+}

certora/confs/Liveness.conf

@@ -0,0 +1,24 @@
+{
+    "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/harness/MetaMorphoHarness.sol",
+    ],
+    "link": [
+        "MetaMorphoHarness:MORPHO=MorphoHarness",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc8.19",
+        "MetaMorphoHarness": "solc",
+    },
+    "verify": "MetaMorphoHarness:certora/specs/Liveness.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 120",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Liveness"
+}

certora/specs/ConsistentState.spec

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "Enabled.spec";
+import "LastUpdated.spec";
 
 // Check that fee cannot accrue to an unset fee recipient.
 invariant noFeeToUnsetFeeRecipient()
@@ -17,7 +17,38 @@ function hasSupplyCapIsEnabled(MetaMorphoHarness.Id id) returns bool {
 // This invariant is useful to conclude that markets that are not enabled cannot be interacted with (notably for reallocate).
 invariant supplyCapIsEnabled(MetaMorphoHarness.Id id)
     hasSupplyCapIsEnabled(id);
-// Check that a market with a positive cap cannot be marked for removal.
+
+function hasPendingSupplyCapHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams) returns bool {
+    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+
+    uint64 pendingAt;
+    _, pendingAt = pendingCap(id);
+
+    return pendingAt > 0 => marketParams.loanToken == asset();
+}
+
+// Check that there can only be pending caps on markets where the loan asset is the asset of the vault.
+invariant pendingSupplyCapHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams)
+    hasPendingSupplyCapHasConsistentAsset(marketParams);
+
+function isEnabledHasConsistentState(MetaMorphoHarness.MarketParams marketParams) returns bool {
+    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+
+    bool enabled;
+    _, enabled, _ = config(id);
+
+    return enabled => marketParams.loanToken == asset();
+}
+
+// Check that having a positive cap implies that the loan asset is the asset of the vault.
+invariant enabledHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams)
+    isEnabledHasConsistentState(marketParams)
+{ preserved acceptCap(MetaMorphoHarness.MarketParams _mp) with (env e) {
+    requireInvariant pendingSupplyCapHasConsistentAsset(marketParams);
+    require e.block.timestamp > 0;
+  }
+}
+
 function hasSupplyCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool {
     uint192 supplyCap;
     uint64 removableAt;
@@ -26,10 +57,10 @@ function hasSupplyCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool
     return supplyCap > 0 => removableAt == 0;
 }
 
+// Check that a market with a positive cap cannot be marked for removal.
 invariant supplyCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id)
     hasSupplyCapIsNotMarkedForRemoval(id);
 
-// Check that a market with a pending cap cannot be marked for removal.
 function hasPendingCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns bool {
     uint64 pendingAt;
     _, pendingAt = pendingCap(id);
@@ -39,5 +70,6 @@ function hasPendingCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id) returns boo
     return pendingAt > 0 => removableAt == 0;
 }
 
+// Check that a market with a pending cap cannot be marked for removal.
 invariant pendingCapIsNotMarkedForRemoval(MetaMorphoHarness.Id id)
     hasPendingCapIsNotMarkedForRemoval(id);

certora/specs/LastUpdated.spec

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+import "Enabled.spec";
+
+using MorphoHarness as Morpho;
+
+methods {
+    function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree;
+    function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
+}
+
+// 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:
+// - 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 {
+    uint192 supplyCap;
+    supplyCap, _, _ = config(id);
+
+    return supplyCap > 0 => Morpho.lastUpdate(id) > 0;
+}
+
+// Check that any new market in the supply queue necessarily has a positive cap.
+rule newSupplyQueueEnsuresPositiveCap(env e, MetaMorphoHarness.Id[] newSupplyQueue) {
+    uint256 i;
+
+    setSupplyQueue(e, newSupplyQueue);
+
+    MetaMorphoHarness.Id id = supplyQueue(i);
+
+    uint192 supplyCap;
+    supplyCap, _, _ = config(id);
+    assert supplyCap > 0;
+}

certora/specs/Liveness.spec

@@ -0,0 +1,78 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+import "Reverts.spec";
+
+// Check that having the allocator role allows to pause supply on the vault.
+rule canPauseSupply() {
+    env e1; MetaMorphoHarness.Id[] newSupplyQueue;
+    require newSupplyQueue.length == 0;
+    require e1.msg.value == 0;
+    require hasAllocatorRole(e1.msg.sender);
+
+    setSupplyQueue@withrevert(e1, newSupplyQueue);
+    assert !lastReverted;
+
+    storage pausedSupply = lastStorage;
+
+    env e2; uint256 assets2; address receiver2;
+    require assets2 != 0;
+    deposit@withrevert(e2, assets2, receiver2) at pausedSupply;
+    assert lastReverted;
+
+    env e3; uint256 shares3; address receiver3;
+    uint256 assets3 = mint@withrevert(e3, shares3, receiver3) at pausedSupply;
+    require assets3 != 0;
+    assert lastReverted;
+}
+
+rule canForceRemoveMarket(MetaMorphoHarness.MarketParams marketParams) {
+    MetaMorphoHarness.Id id = Morpho.libId(marketParams);
+
+    // Safe require because this is a verified invariant.
+    require hasSupplyCapIsEnabled(id);
+    // Safe require because this is a verified invariant.
+    require isEnabledHasConsistentState(marketParams);
+    // Safe require because this is a verified invariant.
+    require hasPositiveSupplyCapIsUpdated(id);
+
+    uint184 supplyCap; uint64 removableAt;
+    supplyCap, _, removableAt = config(id);
+    require supplyCap > 0;
+    require removableAt == 0;
+    // Assume that the withdraw queue is [X, id];
+    require withdrawQueue(1) == id;
+    require withdrawQueueLength() == 2;
+
+    env e1; env e2; env e3;
+    require hasCuratorRole(e1.msg.sender);
+    require e2.msg.sender == e1.msg.sender;
+    require e3.msg.sender == e1.msg.sender;
+
+    require e1.msg.value == 0;
+    revokePendingCap@withrevert(e1, id);
+    assert !lastReverted;
+
+    require e2.msg.value == 0;
+    submitCap@withrevert(e2, marketParams, 0);
+    assert !lastReverted;
+
+    require e3.msg.value == 0;
+    // Safe require because it is a verified invariant.
+    require isTimelockInRange();
+    // Safe require as it corresponds to year 2262.
+    require e3.block.timestamp < 2^63;
+    submitMarketRemoval@withrevert(e3, marketParams);
+    assert !lastReverted;
+
+    env e4; uint256[] newWithdrawQueue;
+    require newWithdrawQueue.length == 1;
+    require newWithdrawQueue[0] == 0;
+    require e4.msg.value == 0;
+    require hasAllocatorRole(e4.msg.sender);
+    require to_mathint(e4.block.timestamp) >= e3.block.timestamp + timelock();
+    updateWithdrawQueue@withrevert(e4, newWithdrawQueue);
+    assert !lastReverted;
+
+    bool enabled;
+    _, enabled, _ = config(id);
+    assert !enabled;
+}

certora/specs/Range.spec

@@ -2,19 +2,27 @@
 methods {
     function multicall(bytes[]) external returns(bytes[]) => NONDET DELETE;
 
+    function asset() external returns(address) envfree;
     function pendingTimelock() external returns(uint192, uint64) envfree;
     function timelock() external returns(uint256) envfree;
     function guardian() external returns(address) envfree;
     function pendingGuardian() external returns(address, uint64) envfree;
     function pendingCap(MetaMorphoHarness.Id) external returns(uint192, uint64) envfree;
     function config(MetaMorphoHarness.Id) external returns(uint184, bool, uint64) envfree;
     function supplyQueueLength() external returns(uint256) envfree;
+    function supplyQueue(uint256) external returns(MetaMorphoHarness.Id) envfree;
     function withdrawQueueLength() external returns(uint256) envfree;
     function withdrawQueue(uint256) external returns(MetaMorphoHarness.Id) envfree;
     function withdrawRank(MetaMorphoHarness.Id) external returns(uint256) envfree;
     function deletedAt(MetaMorphoHarness.Id) external returns(uint256) envfree;
     function fee() external returns(uint96) envfree;
     function feeRecipient() external returns(address) envfree;
+    function owner() external returns(address) envfree;
+    function curator() external returns(address) envfree;
+    function isAllocator(address) external returns(bool) envfree;
+    function skimRecipient() external returns(address) envfree;
+    function totalSupply(address) external returns(uint256) envfree;
+    function balanceOf(address, address) external returns(uint256) envfree;
 
     function minTimelock() external returns(uint256) envfree;
     function maxTimelock() external returns(uint256) envfree;

certora/specs/Reverts.spec

@@ -1,28 +1,9 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "ConsistentState.spec";
 
-using MorphoHarness as Morpho;
-
 methods {
-    function asset() external returns(address) envfree;
-    function owner() external returns(address) envfree;
-    function curator() external returns(address) envfree;
-    function isAllocator(address) external returns(bool) envfree;
-    function skimRecipient() external returns(address) envfree;
-    function fee() external returns(uint96) envfree;
-    function feeRecipient() external returns(address) envfree;
-    function guardian() external returns(address) envfree;
-    function pendingGuardian() external returns(address, uint64) envfree;
-    function config(MorphoHarness.Id) external returns(uint184, bool, uint64) envfree;
-    function pendingCap(MorphoHarness.Id) external returns(uint192, uint64) envfree;
-
     function _.transfer(address, uint256) external => DISPATCHER(true);
     function _.balanceOf(address) external => DISPATCHER(true);
-    function totalSupply(address) external returns(uint256) envfree;
-    function balanceOf(address, address) external returns(uint256) envfree;
-
-    function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree;
-    function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree;
 }
 
 function hasCuratorRole(address user) returns bool {