Merge branch 'main' into test/metamorpho-mock

.gitignore

@@ -25,9 +25,8 @@ broadcast/
 node_modules/
 
 # Certora
-.certora**
-emv-*-certora*
-certora/munged/
+.certora_internal
+munged/
 
 # Hardhat
 /types

README.md

@@ -1,10 +1,12 @@
-# MetaMorpho No Bad Debt Realization
+# MetaMorpho v1.1
 
-> [!NOTE]  
-> This repo is a fork of [metamorpho](https://github.com/morpho-org/metamorpho), with 3 changes:
-> - this MetaMorpho vault does not realize the bad debt (more on this [here](https://github.com/morpho-org/metamorpho-no-bad-debt-realization/blob/d16ecfed0da4b4c51ed65c2eba865f5623c2242b/src/interfaces/IMetaMorpho.sol#L81));
+> [!NOTE]
+> This repo is a fork of [metamorpho](https://github.com/morpho-org/metamorpho), with 4 changes:
+>
+> - this MetaMorpho vault does not realize the bad debt (more on this [here](https://github.com/morpho-org/metamorpho-no-bad-debt-realization/blob/d16ecfed0da4b4c51ed65c2eba865f5623c2242b/src/interfaces/IMetaMorphoV1_1.sol#L81));
 > - the timelock can be set to zero at deployment;
-> - the name and symbol are mutable.
+> - the name and symbol are mutable;
+> - `reallocate` always reverts if the market is not enabled in the vault.
 
 ## Overview
 
@@ -16,9 +18,9 @@ Users of MetaMorpho are liquidity providers who want to earn from borrowing inte
 The active management of the deposited assets is the responsibility of a set of different roles (owner, curator and allocators).
 These roles are primarily responsible for enabling and disabling markets on Morpho Blue and managing the allocation of users’ funds.
 
-[`MetaMorpho`](./src/MetaMorpho.sol) vaults are [ERC-4626](https://eips.ethereum.org/EIPS/eip-4626) vaults, with ([ERC-2612](https://eips.ethereum.org/EIPS/eip-2612)) permit.
+[`MetaMorphoV1_1`](./src/MetaMorphoV1_1.sol) vaults are [ERC-4626](https://eips.ethereum.org/EIPS/eip-4626) vaults, with ([ERC-2612](https://eips.ethereum.org/EIPS/eip-2612)) permit.
 One MetaMorpho vault is related to one loan asset on Morpho Blue.
-The [`MetaMorphoFactory`](./src/MetaMorphoFactory.sol) is deploying immutable onchain instances of MetaMorpho vaults.
+The [`MetaMorphoV1_1Factory`](./src/MetaMorphoV1_1Factory.sol) is deploying immutable onchain instances of MetaMorpho vaults.
 
 Users can supply or withdraw assets at any time, depending on the available liquidity on Morpho Blue.
 A maximum of 30 markets can be enabled on a given MetaMorpho vault.

certora/Makefile

@@ -0,0 +1,14 @@
+munged: ../munged
+
+../munged: $(wildcard ../src/*.sol) applyMunging.patch
+	@rm -rf ../munged
+	@cp -r ../src ../munged
+	@patch -p0 -d ../munged < applyMunging.patch
+
+record:
+	diff -ruN ../src ../munged | sed -E 's,\.\./src/|\.\./munged/,,g' | sed -E 's,((\-\-\-|\+\+\+) [^[:space:]]*).*,\1,' > applyMunging.patch
+
+clean:
+	rm -rf ../munged
+
+.PHONY: clean record munged # Do not add ../munged here, as it is useful to protect munged edits

certora/applyMunging.patch

@@ -1,100 +1,47 @@
-diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol
---- 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 @@
+diff -ruN interfaces/IMetaMorphoV1_1.sol interfaces/IMetaMorphoV1_1.sol
+--- interfaces/IMetaMorphoV1_1.sol
++++ interfaces/IMetaMorphoV1_1.sol
+@@ -1,7 +1,7 @@
  // SPDX-License-Identifier: GPL-2.0-or-later
  pragma solidity >=0.5.0;
 
 -import {IMorpho, Id, MarketParams} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
--import {IERC4626} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
--import {IERC20Permit} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Permit.sol";
-+import {IMorphoHarness, Id, MarketParams} from "../../helpers/IMorphoHarness.sol";
-+import {IERC4626} from "../../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
-+import {IERC20Permit} from "../../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Permit.sol";
-
- import {MarketConfig, PendingUint192, PendingAddress} from "../libraries/PendingLib.sol";
++import {IMorphoHarness, Id, MarketParams} from "../../certora/helpers/IMorphoHarness.sol";
+ import {IERC4626} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
+ import {IERC20Permit} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Permit.sol";
 
 @@ -30,7 +30,7 @@
- /// @dev Consider using the IMetaMorpho interface instead of this one.
- interface IMetaMorphoBase {
+ /// @dev Consider using the IMetaMorphoV1_1 interface instead of this one.
+ interface IMetaMorphoV1_1Base {
      /// @notice The address of the Morpho contract.
 -    function MORPHO() external view returns (IMorpho);
 +    function MORPHO() external view returns (IMorphoHarness);
      function DECIMALS_OFFSET() external view returns (uint8);
 
      /// @notice The address of the curator.
-diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol
---- 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;
-
--import {Id} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {Id} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-
- /// @title ErrorsLib
- /// @author Morpho Labs
-diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol
---- 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;
-
--import {Id} from "../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {Id} from "../../../lib/morpho-blue/src/interfaces/IMorpho.sol";
-
- import {PendingAddress} from "./PendingLib.sol";
-
-diff -ruN MetaMorpho.sol MetaMorpho.sol
---- 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
- } from "./interfaces/IMetaMorpho.sol";
+diff -ruN MetaMorphoV1_1.sol MetaMorphoV1_1.sol
+--- MetaMorphoV1_1.sol
++++ MetaMorphoV1_1.sol
+@@ -9,7 +9,7 @@
+     IMetaMorphoV1_1Base,
+     IMetaMorphoV1_1StaticTyping
+ } from "./interfaces/IMetaMorphoV1_1.sol";
 -import {Id, MarketParams, Market, IMorpho} from "../lib/morpho-blue/src/interfaces/IMorpho.sol";
-+import {Id, MarketParams, Market, IMorphoHarness} from "../helpers/IMorphoHarness.sol";
++import {Id, MarketParams, Market, IMorphoHarness} from "../certora/helpers/IMorphoHarness.sol";
 
  import {PendingUint192, PendingAddress, PendingLib} from "./libraries/PendingLib.sol";
  import {ConstantsLib} from "./libraries/ConstantsLib.sol";
- import {ErrorsLib} from "./libraries/ErrorsLib.sol";
- import {EventsLib} from "./libraries/EventsLib.sol";
--import {WAD} from "../lib/morpho-blue/src/libraries/MathLib.sol";
--import {UtilsLib} from "../lib/morpho-blue/src/libraries/UtilsLib.sol";
--import {SafeCast} from "../lib/openzeppelin-contracts/contracts/utils/math/SafeCast.sol";
--import {SharesMathLib} from "../lib/morpho-blue/src/libraries/SharesMathLib.sol";
+@@ -19,10 +19,8 @@
+ import {UtilsLib} from "../lib/morpho-blue/src/libraries/UtilsLib.sol";
+ import {SafeCast} from "../lib/openzeppelin-contracts/contracts/utils/math/SafeCast.sol";
+ import {SharesMathLib} from "../lib/morpho-blue/src/libraries/SharesMathLib.sol";
 -import {MorphoLib} from "../lib/morpho-blue/src/libraries/periphery/MorphoLib.sol";
--import {MarketParamsLib} from "../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
--import {IERC20Metadata} from "../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol";
+ import {MarketParamsLib} from "../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
+ import {IERC20Metadata} from "../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol";
 -import {MorphoBalancesLib} from "../lib/morpho-blue/src/libraries/periphery/MorphoBalancesLib.sol";
--
--import {Multicall} from "../lib/openzeppelin-contracts/contracts/utils/Multicall.sol";
--import {Ownable2Step, Ownable} from "../lib/openzeppelin-contracts/contracts/access/Ownable2Step.sol";
--import {ERC20Permit} from "../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC20Permit.sol";
-+import {WAD} from "../../lib/morpho-blue/src/libraries/MathLib.sol";
-+import {UtilsLib} from "../../lib/morpho-blue/src/libraries/UtilsLib.sol";
-+import {SafeCast} from "../../lib/openzeppelin-contracts/contracts/utils/math/SafeCast.sol";
-+import {SharesMathLib} from "../../lib/morpho-blue/src/libraries/SharesMathLib.sol";
-+import {MarketParamsLib} from "../../lib/morpho-blue/src/libraries/MarketParamsLib.sol";
-+import {IERC20Metadata} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol";
-+
-+import {Multicall} from "../../lib/openzeppelin-contracts/contracts/utils/Multicall.sol";
-+import {Ownable2Step, Ownable} from "../../lib/openzeppelin-contracts/contracts/access/Ownable2Step.sol";
-+import {ERC20Permit} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC20Permit.sol";
- import {
-     IERC20,
-     IERC4626,
-@@ -34,7 +32,7 @@
-     ERC4626,
-     Math,
-     SafeERC20
--} from "../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol";
-+} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol";
-
- /// @title MetaMorpho
- /// @author Morpho Labs
+
+ import {Multicall} from "../lib/openzeppelin-contracts/contracts/utils/Multicall.sol";
+ import {Ownable2Step, Ownable} from "../lib/openzeppelin-contracts/contracts/access/Ownable2Step.sol";
 @@ -45,9 +43,7 @@
      using UtilsLib for uint256;
      using SafeCast for uint256;
@@ -108,7 +55,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
 @@ -56,7 +52,7 @@
      /* IMMUTABLES */
 
-     /// @inheritdoc IMetaMorphoBase
+     /// @inheritdoc IMetaMorphoV1_1Base
 -    IMorpho public immutable MORPHO;
 +    IMorphoHarness public immutable MORPHO;
 
@@ -134,7 +81,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
      /* CONSTRUCTOR */
 
      /// @dev Initializes the contract.
-@@ -144,7 +153,7 @@
+@@ -145,7 +154,7 @@
          _symbol = __symbol;
          emit EventsLib.SetSymbol(__symbol);
 
@@ -143,7 +90,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          DECIMALS_OFFSET = uint8(uint256(18).zeroFloorSub(IERC20Metadata(_asset).decimals()));
 
          IERC20(_asset).forceApprove(morpho, type(uint256).max);
-@@ -365,6 +374,9 @@
+@@ -366,6 +375,9 @@
              seen[prevIndex] = true;
 
              newWithdrawQueue[i] = id;
@@ -153,7 +100,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          }
 
          for (uint256 i; i < currLength; ++i) {
-@@ -382,6 +394,10 @@
+@@ -383,6 +395,10 @@
                      }
                  }
 
@@ -164,7 +111,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  delete config[id];
              }
          }
-@@ -770,6 +786,9 @@
+@@ -772,6 +788,9 @@
 
          if (supplyCap > 0) {
              if (!marketConfig.enabled) {
@@ -174,7 +121,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  withdrawQueue.push(id);
 
                  if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded();
-@@ -829,6 +848,9 @@
+@@ -831,6 +850,9 @@
      /// @dev Withdraws `assets` from Morpho.
      function _withdrawMorpho(uint256 assets) internal {
          for (uint256 i; i < withdrawQueue.length; ++i) {

certora/confs/MarketInteractions.conf

@@ -16,7 +16,7 @@
   "prover_args": [
     "-depth 3",
     "-mediumTimeout 20",
-    "-timeout 120",
+    "-timeout 300",
     "-smt_nonLinearArithmetic false"
   ],
   "rule_sanity": "basic",

certora/confs/Range.conf

@@ -8,7 +8,7 @@
   "optimistic_loop": true,
   "prover_args": [
     "-depth 0",
-    "-timeout 300",
+    "-timeout 1000",
     "-smt_nonLinearArithmetic true",
     "-adaptiveSolverConfig false",
     "-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}]"

certora/gambit.conf

@@ -1,5 +1,5 @@
  {
-      "filename" : "../src/MetaMorpho.sol",
+      "filename" : "../src/MetaMorphoV1_1.sol",
       "sourceroot": "..",
       "num_mutants": 15,
       "solc_remappings": []

certora/helpers/ERC20Helper.sol

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.26;
 
-import {IERC20, SafeERC20} from "../munged/MetaMorpho.sol";
+import {IERC20, SafeERC20} from "../../munged/MetaMorphoV1_1.sol";
 
 contract ERC20Helper {
     using SafeERC20 for IERC20;

certora/helpers/MetaMorphoHarness.sol

@@ -2,18 +2,24 @@
 pragma solidity 0.8.26;
 
 import {
-    Math, MetaMorpho, Id, ConstantsLib, PendingUint192, PendingAddress, MarketConfig
-} from "../munged/MetaMorpho.sol";
-
-contract MetaMorphoHarness is MetaMorpho {
+    Math,
+    MetaMorphoV1_1,
+    Id,
+    ConstantsLib,
+    PendingUint192,
+    PendingAddress,
+    MarketConfig
+} from "../../munged/MetaMorphoV1_1.sol";
+
+contract MetaMorphoHarness is MetaMorphoV1_1 {
     constructor(
         address owner,
         address morpho,
         uint256 initialTimelock,
         address _asset,
         string memory _name,
         string memory _symbol
-    ) MetaMorpho(owner, morpho, initialTimelock, _asset, _name, _symbol) {}
+    ) MetaMorphoV1_1(owner, morpho, initialTimelock, _asset, _name, _symbol) {}
 
     function pendingTimelock_() external view returns (PendingUint192 memory) {
         return pendingTimelock;
@@ -87,20 +93,20 @@ contract MetaMorphoHarness is MetaMorpho {
     }
 
     function realTotalAssets() public view returns (uint256) {
-        uint256 realTotalAssets;
+        uint256 _realTotalAssets;
         for (uint256 i; i < withdrawQueue.length; ++i) {
-            realTotalAssets += MORPHO.expectedSupplyAssets(_marketParams(withdrawQueue[i]), address(this));
+            _realTotalAssets += MORPHO.expectedSupplyAssets(_marketParams(withdrawQueue[i]), address(this));
         }
-        return realTotalAssets;
+        return _realTotalAssets;
     }
 
     function newLostAssets() external view returns (uint256) {
-        uint256 realTotalAssets = realTotalAssets();
+        uint256 _realTotalAssets = realTotalAssets();
 
-        uint256 newLostAssets;
-        if (realTotalAssets < lastTotalAssets - lostAssets) newLostAssets = lastTotalAssets - realTotalAssets;
-        else newLostAssets = lostAssets;
+        uint256 _newLostAssets;
+        if (_realTotalAssets < lastTotalAssets - lostAssets) _newLostAssets = lastTotalAssets - _realTotalAssets;
+        else _newLostAssets = lostAssets;
 
-        return newLostAssets;
+        return _newLostAssets;
     }
 }

certora/specs/MarketInteractions.spec

@@ -4,6 +4,7 @@ import "ConsistentState.spec";
 methods {
     function _.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams, assets, shares, onBehalf, data) expect (uint256, uint256) ALL;
     function _.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver) expect (uint256, uint256) ALL;
+    function _.accrueInterest(MetaMorphoHarness.MarketParams marketParams) external => summaryAccrueInterest(marketParams) expect void ALL;
     function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
 
     function lastIndexWithdraw() external returns(uint256) envfree;
@@ -52,6 +53,18 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     return (_, _);
 }
 
+function summaryAccrueInterest(MetaMorphoHarness.MarketParams marketParams) {
+    MetaMorphoHarness.Id id = Util.libId(marketParams);
+    uint256 index = lastIndexWithdraw();
+    requireInvariant inWithdrawQueueIsEnabled(index);
+    requireInvariant supplyCapIsEnabled(id);
+
+    // Check that all markets from which MetaMorpho accrues interest are enabled markets.
+    assert config_(id).enabled;
+
+    // View summary, which is sound because all non view functions in Morpho Blue are abstracted away.
+}
+
 // Check assertions in the summaries.
 rule checkSummary(method f, env e, calldataarg args) {
     f(e, args);