morpho-org · MathisGD · Sep 26, 2024 · Jul 31, 2024 · Jul 31, 2024 · Jul 31, 2024
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -22,6 +22,8 @@ jobs:
           - Immutability
           - LastUpdated
           - Liveness
+          - LostAssetsLink
+          - LostAssetsNoLink
           - MarketInteractions
           - PendingValues
           - Range
@@ -50,11 +52,11 @@ jobs:
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
-      - name: Install solc (0.8.21)
+      - name: Install solc (0.8.26)
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.26/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc-0.8.21
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.26
 
       - name: Apply munging
         run: make -C certora munged

diff --git a/README.md b/README.md
@@ -28,7 +28,9 @@ Those rewards can be transferred to the `skimRecipient`.
 The vault's owner has the choice to distribute back these rewards to vault depositors however they want.
 For more information about this use case, see the [Rewards](#rewards) section.
 
-All actions that may be against users' interests (e.g. enabling a market with a high exposure) are subject to a timelock of minimum 24 hours.
+All actions that may be against users' interests (e.g. enabling a market with a high exposure) is subject to a timelock.
+To make vault setup easier, the initial timelock can be either 0 or anywhere between 24 hours and 2 weeks.
+Any further timelock change must set the value between 24 hours and 2 weeks.
 The `owner`, or the `guardian` if set, can revoke the action during the timelock.
 After the timelock, the action can be executed by anyone.
 
@@ -51,6 +53,7 @@ It can:
 - [Timelocked if already set] Set the guardian.
 - Set the performance fee (capped at 50%).
 - Set the fee recipient.
+- Set the name and symbol of the vault.
 
 #### Curator
 

diff --git a/audits/2024-09-16-metamorpho-diff-open-zeppelin.pdf b/audits/2024-09-16-metamorpho-diff-open-zeppelin.pdf
diff --git a/audits/2024-09-23-metamorpho-diff-cantina-managed-review.pdf b/audits/2024-09-23-metamorpho-diff-cantina-managed-review.pdf
diff --git a/certora/README.md b/certora/README.md
@@ -4,8 +4,8 @@ This folder contains the verification of MetaMorpho using CVL, Certora's Verific
 
 The code is compiled using 2 versions of solidity, which must be installed to run the verification as:
 
-- `solc` for solidity compiler version 0.8.21 which is used for compiling MetaMorpho
-- `solc8.19` for solidity compiler version 0.8.19 which is used for compiling Morpho Blue.
+- `solc-0.8.26` for solidity compiler version 0.8.26 which is used for compiling MetaMorpho
+- `solc-0.8.19` for solidity compiler version 0.8.19 which is used for compiling Morpho Blue.
 
 The verification is run on modified source files, which are made available by running:
 
@@ -68,7 +68,7 @@ The following function defined in [`PendingValues.spec`](specs/PendingValues.spe
 
 ```solidity
 function isSmallerPendingTimelock() returns bool {
-    return assert_uint256(pendingTimelock_().value) < timelock();
+    return assert_uint256(pendingTimelock_().value) <= timelock();
 }
 ```
 

diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch
@@ -1,6 +1,6 @@
 diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol
---- interfaces/IMetaMorpho.sol	2024-03-20 15:13:25.818251404 +0100
-+++ interfaces/IMetaMorpho.sol	2024-03-22 11:22:35.598510490 +0100
+--- interfaces/IMetaMorpho.sol	2024-08-19 12:35:33.153217935 +0200
++++ interfaces/IMetaMorpho.sol	2024-09-04 10:44:42.493695519 +0200
 @@ -1,9 +1,9 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity >=0.5.0;
@@ -24,8 +24,8 @@ diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol
 
      /// @notice The address of the curator.
 diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
---- libraries/ErrorsLib.sol	2024-03-20 15:13:25.802251714 +0100
-+++ libraries/ErrorsLib.sol	2024-03-22 11:22:35.598510490 +0100
+--- libraries/ErrorsLib.sol	2024-08-19 13:28:08.003401745 +0200
++++ libraries/ErrorsLib.sol	2024-09-04 10:44:42.493695519 +0200
 @@ -1,7 +1,7 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity ^0.8.0;
@@ -36,8 +36,8 @@ diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
  /// @title ErrorsLib
  /// @author Morpho Labs
 diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
---- libraries/EventsLib.sol	2024-03-20 15:13:25.802251714 +0100
-+++ libraries/EventsLib.sol	2024-03-22 11:22:35.598510490 +0100
+--- libraries/EventsLib.sol	2024-08-16 18:17:20.260781030 +0200
++++ libraries/EventsLib.sol	2024-09-04 10:44:42.493695519 +0200
 @@ -1,7 +1,7 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity ^0.8.0;
@@ -48,8 +48,8 @@ diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
  import {PendingAddress} from "./PendingLib.sol";
 
 diff -ruN MetaMorpho.sol MetaMorpho.sol
---- MetaMorpho.sol	2024-03-20 15:13:25.862250553 +0100
-+++ MetaMorpho.sol	2024-03-22 14:27:33.670423544 +0100
+--- MetaMorpho.sol	2024-09-04 10:44:33.985829466 +0200
++++ MetaMorpho.sol	2024-09-04 10:44:42.497695457 +0200
 @@ -9,24 +9,22 @@
      IMetaMorphoBase,
      IMetaMorphoStaticTyping
@@ -114,9 +114,9 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
 
      /// @notice OpenZeppelin decimals offset used by the ERC4626 implementation.
      /// @dev Calculated to be max(0, 18 - underlyingDecimals) at construction, so the initial conversion rate maximizes
-@@ -107,6 +103,19 @@
-     /// @inheritdoc IMetaMorphoBase
-     uint256 public lastTotalAssets;
+@@ -116,6 +112,19 @@
+     /// @dev "Overrides" the ERC20's storage variable to be able to modify it.
+     string private _symbol;
 
 +    // HARNESS
 +    // The index of the identifier of the last market withdrawn.
@@ -134,16 +134,16 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
      /* CONSTRUCTOR */
 
      /// @dev Initializes the contract.
-@@ -126,7 +135,7 @@
-     ) ERC4626(IERC20(_asset)) ERC20Permit(_name) ERC20(_name, _symbol) Ownable(owner) {
-         if (morpho == address(0)) revert ErrorsLib.ZeroAddress();
+@@ -144,7 +153,7 @@
+         _symbol = __symbol;
+         emit EventsLib.SetSymbol(__symbol);
 
 -        MORPHO = IMorpho(morpho);
 +        MORPHO = IMorphoHarness(morpho);
          DECIMALS_OFFSET = uint8(uint256(18).zeroFloorSub(IERC20Metadata(_asset).decimals()));
 
-         _checkTimelockBounds(initialTimelock);
-@@ -338,6 +347,9 @@
+         IERC20(_asset).forceApprove(morpho, type(uint256).max);
+@@ -365,6 +374,9 @@
              seen[prevIndex] = true;
 
              newWithdrawQueue[i] = id;
@@ -153,7 +153,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          }
 
          for (uint256 i; i < currLength; ++i) {
-@@ -355,6 +367,10 @@
+@@ -382,6 +394,10 @@
                      }
                  }
 
@@ -164,7 +164,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  delete config[id];
              }
          }
-@@ -743,6 +759,9 @@
+@@ -770,6 +786,9 @@
 
          if (supplyCap > 0) {
              if (!marketConfig.enabled) {
@@ -174,7 +174,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  withdrawQueue.push(id);
 
                  if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded();
-@@ -802,6 +821,9 @@
+@@ -829,6 +848,9 @@
      /// @dev Withdraws `assets` from Morpho.
      function _withdrawMorpho(uint256 assets) internal {
          for (uint256 i; i < withdrawQueue.length; ++i) {

diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
@@ -3,7 +3,7 @@
         "certora/helpers/MetaMorphoHarness.sol",
         "certora/helpers/Util.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "parametric_contracts": [
         "MetaMorphoHarness",
     ],

diff --git a/certora/confs/DistinctIdentifiers.conf b/certora/confs/DistinctIdentifiers.conf
@@ -2,7 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "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,7 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "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,7 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "verify": "MetaMorphoHarness:certora/specs/Immutability.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf
@@ -6,8 +6,8 @@
     ],
     "solc_map": {
         "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-        "Util": "solc-0.8.21",
+        "MetaMorphoHarness": "solc-0.8.26",
+        "Util": "solc-0.8.26",
     },
     "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec",
     "loop_iter": "2",

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

diff --git a/certora/confs/LostAssetsLink.conf b/certora/confs/LostAssetsLink.conf
@@ -0,0 +1,28 @@
+{
+    "files": [
+        "certora/helpers/MetaMorphoHarness.sol",
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/helpers/Util.sol",
+    ],
+    "solc_map": {
+        "MetaMorphoHarness": "solc-0.8.26",
+        "MorphoHarness": "solc-0.8.19",
+        "Util": "solc-0.8.26"
+    },
+    "solc_evm_version": "paris",
+    "link": [
+        "MetaMorphoHarness:MORPHO=MorphoHarness",
+    ],
+    "verify": "MetaMorphoHarness:certora/specs/LostAssetsLink.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 3600",
+        "-superOptimisticReturnsize true",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho LostAssets Link",
+}
diff --git a/certora/confs/LostAssetsNoLink.conf b/certora/confs/LostAssetsNoLink.conf
@@ -0,0 +1,18 @@
+{
+    "files": [
+        "certora/helpers/MetaMorphoHarness.sol",
+    ],
+    "solc": "solc-0.8.26",
+    "verify": "MetaMorphoHarness:certora/specs/LostAssetsNoLink.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "prover_args": [
+        "-depth 3",
+        "-mediumTimeout 20",
+        "-timeout 240",
+        "-superOptimisticReturnsize true",
+    ],
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho LostAssets No Link",
+}
diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf
@@ -3,7 +3,7 @@
         "certora/helpers/MetaMorphoHarness.sol",
         "certora/helpers/Util.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "parametric_contracts": [
         "MetaMorphoHarness",
     ],

diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf
@@ -2,7 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "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,7 +2,7 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc": "solc-0.8.26",
     "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,7 +2,8 @@
     "files": [
         "certora/helpers/MetaMorphoHarness.sol",
     ],
-    "solc": "solc-0.8.21",
+    "solc_evm_version": "paris",
+    "solc": "solc-0.8.26",
     "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec",
     "loop_iter": "2",
     "optimistic_loop": true,

diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
@@ -8,11 +8,12 @@
     "link": [
         "MetaMorphoHarness:MORPHO=MorphoHarness",
     ],
+    "solc_evm_version": "paris",
     "solc_map": {
         "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
-        "Util": "solc-0.8.21",
-        "ERC20Standard": "solc-0.8.21",
+        "MetaMorphoHarness": "solc-0.8.26",
+        "Util": "solc-0.8.26",
+        "ERC20Standard": "solc-0.8.26",
     },
     "verify": "MetaMorphoHarness:certora/specs/Reverts.spec",
     "loop_iter": "2",

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

diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf
@@ -8,7 +8,7 @@
     ],
     "solc_map": {
         "MorphoHarness": "solc-0.8.19",
-        "MetaMorphoHarness": "solc-0.8.21",
+        "MetaMorphoHarness": "solc-0.8.26",
     },
     "verify": "MetaMorphoHarness:certora/specs/Timelock.spec",
     "loop_iter": "2",

diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf
@@ -10,13 +10,14 @@
     "link": [
         "MetaMorphoHarness:MORPHO=MorphoHarness",
     ],
+    "solc_evm_version": "paris",
     "solc_map": {
         "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",
+        "MetaMorphoHarness": "solc-0.8.26",
+        "Util": "solc-0.8.26",
+        "ERC20NoRevert": "solc-0.8.26",
+        "ERC20Standard": "solc-0.8.26",
+        "ERC20USDT": "solc-0.8.26",
     },
     "verify": "MetaMorphoHarness:certora/specs/Tokens.spec",
     "loop_iter": "2",

diff --git a/certora/helpers/IMorphoHarness.sol b/certora/helpers/IMorphoHarness.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
-pragma solidity 0.8.21;
+pragma solidity 0.8.26;
 
 import {Id, MarketParams, Market, IMorpho} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";