Merge remote-tracking branch 'origin/fix/allocator-issue' into fix/al…

…locator-issue

.gitignore

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

README.md

@@ -1,10 +1,11 @@
 # MetaMorpho No Bad Debt Realization
 
 > [!NOTE]  
-> This repo is a fork of [metamorpho](https://github.com/morpho-org/metamorpho), with 3 changes:
+> 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/IMetaMorpho.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
 

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,18 +1,14 @@
 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 @@
+--- interfaces/IMetaMorpho.sol
++++ interfaces/IMetaMorpho.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.
@@ -23,78 +19,29 @@ diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol
      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 @@
+--- MetaMorpho.sol
++++ MetaMorpho.sol
+@@ -9,7 +9,7 @@
      IMetaMorphoBase,
      IMetaMorphoStaticTyping
  } from "./interfaces/IMetaMorpho.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;
@@ -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/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/MetaMorpho.sol";
 
 contract ERC20Helper {
     using SafeERC20 for IERC20;

certora/helpers/MetaMorphoHarness.sol

@@ -2,8 +2,14 @@
 pragma solidity 0.8.26;
 
 import {
-    Math, MetaMorpho, Id, ConstantsLib, PendingUint192, PendingAddress, MarketConfig
-} from "../munged/MetaMorpho.sol";
+    Math,
+    MetaMorpho,
+    Id,
+    ConstantsLib,
+    PendingUint192,
+    PendingAddress,
+    MarketConfig
+} from "../../munged/MetaMorpho.sol";
 
 contract MetaMorphoHarness is MetaMorpho {
     constructor(
@@ -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);