Merge pull request #409 from morpho-org/certora/timelock-formula

[Certora] Timelock computations
morpho-org · Mar 22, 2024 · 6b2de91 · 6b2de91
2 parents fcf3c41 + e655ec7
commit 6b2de91
Show file tree

Hide file tree

Showing 18 changed files with 313 additions and 27 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -27,6 +27,7 @@ jobs:
           - Reentrancy
           - Reverts
           - Roles
+          - Timelock
           - Tokens
 
     steps:
@@ -46,13 +47,13 @@ jobs:
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.19
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
       - name: Install solc (0.8.21)
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.21
 
       - name: Apply munging
         run: make -C certora munged

diff --git a/certora/README.md b/certora/README.md
@@ -63,6 +63,7 @@ rule revokePendingTimelockRevertCondition(env e) {
 ## Timelock
 
 MetaMorpho features a timelock mechanism that applies to every operation that could potentially increase risk for users.
+There are computations that give a lower bound for the period during which we know the values are under timelock, and this is verified in [`Timelock.spec`](specs/Timelock.spec).
 The following function defined in [`PendingValues.spec`](specs/PendingValues.spec) is verified to always return `true`.
 
 ```solidity
@@ -196,6 +197,7 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that MetaMorpho is reentrancy safe by making sure that there are no untrusted external calls.
 - [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints.
 - [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective MetaMorpho roles. In particular it checks the hierarchy of roles.
+- [`Timelock.spec`](specs/Timelock.spec) gives computations (and verifies them) for periods during which we know the values are under timelock.
 - [`Tokens.spec`](specs/Tokens.spec) checks that tokens are not kept on the MetaMorpho contract. Any deposit ends up in Morpho Blue and any withdrawal is forwarded to the user.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
@@ -212,7 +214,8 @@ graph
 Tokens --> ConsistentState
 Liveness --> ConsistentState
 Reverts --> ConsistentState
-ConsistentState --> LastUpdated
+ConsistentState --> Timelock
+Timelock --> LastUpdated
 LastUpdated --> Enabled
 Enabled --> DistinctIdentifiers
 DistinctIdentifiers --> PendingValues

diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
@@ -3,13 +3,13 @@
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc_map": {
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+    },
     "parametric_contracts": [
         "MetaMorphoHarness",
     ],
-    "solc_map": {
-        "MorphoHarness": "solc8.19",
-        "MetaMorphoHarness": "solc",
-    },
     "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/DistinctIdentifiers.conf b/certora/confs/DistinctIdentifiers.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/DistinctIdentifiers.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/Enabled.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/Immutability.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf
@@ -3,12 +3,9 @@
         "lib/morpho-blue/certora/harness/MorphoHarness.sol",
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "parametric_contracts": [
-        "MetaMorphoHarness",
-    ],
     "solc_map": {
-        "MorphoHarness": "solc8.19",
-        "MetaMorphoHarness": "solc",
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec",
     "loop_iter": "2",

diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
@@ -8,9 +8,9 @@
         "MetaMorphoHarness:MORPHO=MorphoHarness",
     ],
     "solc_map": {
-        "MorphoHarness": "solc8.19",
-        "MetaMorphoHarness": "solc",
-        "Util": "solc",
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+        "Util": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/Liveness.spec",
     "loop_iter": "2",

diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/PendingValues.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Range.conf b/certora/confs/Range.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/Range.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
@@ -9,10 +9,10 @@
         "MetaMorphoHarness:MORPHO=MorphoHarness",
     ],
     "solc_map": {
-        "MorphoHarness": "solc8.19",
-        "MetaMorphoHarness": "solc",
-        "Util": "solc",
-        "ERC20Standard": "solc",
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+        "Util": "solc-0.8.21",
+        "ERC20Standard": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/Reverts.spec",
     "loop_iter": "2",

diff --git a/certora/confs/Roles.conf b/certora/confs/Roles.conf
@@ -2,6 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
+    "solc": "solc-0.8.21",
     "verify": "MetaMorphoHarness:certora/specs/Roles.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf
@@ -0,0 +1,24 @@
+{
+    "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/helpers/MetaMorphoHarness.sol",
+    ],
+    "parametric_contracts": [
+        "MetaMorphoHarness",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+    },
+    "verify": "MetaMorphoHarness:certora/specs/Timelock.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 300",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Timelock"
+}
diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf
@@ -11,12 +11,12 @@
         "MetaMorphoHarness:MORPHO=MorphoHarness",
     ],
     "solc_map": {
-        "MorphoHarness": "solc8.19",
-        "MetaMorphoHarness": "solc",
-        "Util": "solc",
-        "ERC20NoRevert": "solc",
-        "ERC20Standard": "solc",
-        "ERC20USDT": "solc",
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+        "Util": "solc-0.8.21",
+        "ERC20NoRevert": "solc-0.8.21",
+        "ERC20Standard": "solc-0.8.21",
+        "ERC20USDT": "solc-0.8.21",
     },
     "verify": "MetaMorphoHarness:certora/specs/Tokens.spec",
     "loop_iter": "2",

diff --git a/certora/helpers/MetaMorphoHarness.sol b/certora/helpers/MetaMorphoHarness.sol
@@ -1,7 +1,9 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.21;
 
-import {MetaMorpho, Id, ConstantsLib, PendingUint192, PendingAddress, MarketConfig} from "../munged/MetaMorpho.sol";
+import {
+    Math, MetaMorpho, Id, ConstantsLib, PendingUint192, PendingAddress, MarketConfig
+} from "../munged/MetaMorpho.sol";
 
 contract MetaMorphoHarness is MetaMorpho {
     constructor(
@@ -44,4 +46,43 @@ contract MetaMorphoHarness is MetaMorpho {
     function maxFee() external pure returns (uint256) {
         return ConstantsLib.MAX_FEE;
     }
+
+    function nextGuardianUpdateTime() external view returns (uint256 nextTime) {
+        nextTime = block.timestamp + timelock;
+
+        if (pendingTimelock.validAt != 0) {
+            nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value);
+        }
+
+        uint256 validAt = pendingGuardian.validAt;
+        if (validAt != 0) nextTime = Math.min(nextTime, validAt);
+    }
+
+    function nextCapIncreaseTime(Id id) external view returns (uint256 nextTime) {
+        nextTime = block.timestamp + timelock;
+
+        if (pendingTimelock.validAt != 0) {
+            nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value);
+        }
+
+        uint256 validAt = pendingCap[id].validAt;
+        if (validAt != 0) nextTime = Math.min(nextTime, validAt);
+    }
+
+    function nextTimelockDecreaseTime() external view returns (uint256 nextTime) {
+        nextTime = block.timestamp + timelock;
+
+        if (pendingTimelock.validAt != 0) nextTime = Math.min(nextTime, pendingTimelock.validAt);
+    }
+
+    function nextRemovableTime(Id id) external view returns (uint256 nextTime) {
+        nextTime = block.timestamp + timelock;
+
+        if (pendingTimelock.validAt != 0) {
+            nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value);
+        }
+
+        uint256 removableAt = config[id].removableAt;
+        if (removableAt != 0) nextTime = Math.min(nextTime, removableAt);
+    }
 }
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-import "LastUpdated.spec";
+import "Timelock.spec";
 
 function hasCuratorRole(address user) returns bool {
     return user == owner() || user == curator();