Lost assets (no share price decrease)

.github/workflows/certora.yml

@@ -22,6 +22,8 @@ jobs:
           - Immutability
           - LastUpdated
           - Liveness
+          - LostAssetsLink
+          - LostAssetsNoLink
           - MarketInteractions
           - PendingValues
           - Range

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-12 17:01:51.540516233 +0200
++++ interfaces/IMetaMorpho.sol	2024-08-13 13:46:23.645208968 +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-12 17:00:02.975663176 +0200
++++ libraries/ErrorsLib.sol	2024-08-13 13:46:23.645208968 +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-12 17:01:51.540516233 +0200
++++ libraries/EventsLib.sol	2024-08-13 13:46:23.645208968 +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-08-12 17:01:51.540516233 +0200
++++ MetaMorpho.sol	2024-08-13 13:46:23.649208876 +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 @@
+@@ -110,6 +106,19 @@
      /// @inheritdoc IMetaMorphoBase
-     uint256 public lastTotalAssets;
+     uint256 public lostAssets;
 
 +    // HARNESS
 +    // The index of the identifier of the last market withdrawn.
@@ -134,7 +134,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
      /* CONSTRUCTOR */
 
      /// @dev Initializes the contract.
-@@ -126,7 +135,7 @@
+@@ -129,7 +138,7 @@
      ) ERC4626(IERC20(_asset)) ERC20Permit(_name) ERC20(_name, _symbol) Ownable(owner) {
          if (morpho == address(0)) revert ErrorsLib.ZeroAddress();
 
@@ -143,7 +143,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          DECIMALS_OFFSET = uint8(uint256(18).zeroFloorSub(IERC20Metadata(_asset).decimals()));
 
          _checkTimelockBounds(initialTimelock);
-@@ -338,6 +347,9 @@
+@@ -341,6 +350,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 @@
+@@ -358,6 +370,10 @@
                      }
                  }
 
@@ -164,7 +164,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  delete config[id];
              }
          }
-@@ -743,6 +759,9 @@
+@@ -735,6 +751,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 @@
+@@ -794,6 +813,9 @@
      /// @dev Withdraws `assets` from Morpho.
      function _withdrawMorpho(uint256 assets) internal {
          for (uint256 i; i < withdrawQueue.length; ++i) {

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.21",
+        "MorphoHarness": "solc-0.8.19",
+        "Util": "solc-0.8.21"
+    },
+    "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",
+}
+

certora/confs/LostAssetsNoLink.conf

@@ -0,0 +1,18 @@
+{
+    "files": [
+        "certora/helpers/MetaMorphoHarness.sol",
+    ],
+    "solc": "solc-0.8.21",
+    "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",
+}

certora/helpers/MetaMorphoHarness.sol

@@ -85,4 +85,22 @@ contract MetaMorphoHarness is MetaMorpho {
         uint256 removableAt = config[id].removableAt;
         if (removableAt != 0) nextTime = Math.min(nextTime, removableAt);
     }
+
+    function realTotalAssets() public view returns (uint256) {
+        uint256 realTotalAssets;
+        for (uint256 i; i < withdrawQueue.length; ++i) {
+            realTotalAssets += MORPHO.expectedSupplyAssets(_marketParams(withdrawQueue[i]), address(this));
+        }
+        return realTotalAssets;
+    }
+
+    function newLostAssets() external view returns (uint256) {
+        uint256 realTotalAssets = realTotalAssets();
+
+        uint256 newLostAssets;
+        if (realTotalAssets < lastTotalAssets - lostAssets) newLostAssets = lastTotalAssets - realTotalAssets;
+        else newLostAssets = lostAssets;
+
+        return newLostAssets;
+    }
 }

certora/specs/LostAssetsLink.spec

@@ -0,0 +1,115 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using MorphoHarness as Morpho;
+using Util as Util;
+
+methods {
+    function multicall(bytes[]) external returns(bytes[]) => NONDET DELETE;
+
+    function lostAssets() external returns(uint256) envfree;
+    function totalAssets() external returns(uint256) envfree;
+    function totalSupply() external returns(uint256) envfree;
+    function lastTotalAssets() external returns(uint256) envfree;
+    function realTotalAssets() external returns(uint256) envfree;
+    function newLostAssets() external returns(uint256) envfree;
+    function MORPHO() external returns(address) envfree;
+
+    // Summaries.
+    function _.expectedSupplyAssets(MorphoHarness.MarketParams marketParams, address user) external => summaryExpectedSupplyAssets(marketParams, user) expect (uint256);
+    function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
+    function _.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal => summaryMulDiv(x, y, denominator, rounding) expect (uint256);
+
+    // We assume that the erc20 is view. It's ok as we don't care about what happens in the token.
+    function _.transfer(address, uint256) external => NONDET;
+    function _.transferFrom(address, address, uint256) external => NONDET;
+    function _.balanceOf(address) external => NONDET;
+
+    // We assume that the IRM and oracle are view.
+    function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => NONDET;
+    function _.price() external => NONDET;
+
+    // We deactivate callbacks.
+    // Ideally we can assume that they can't change arbitrarily the storage of Morpho
+    // and Metamorpho, but can only reenter through public entry-points, but I don't
+    // know how to do this.
+    function _.onMorphoSupply(uint256, bytes) external => NONDET;
+    function _.onMorphoRepay(uint256, bytes) external => NONDET;
+    function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET;
+    function _.onMorphoLiquidate(uint256, bytes) external => NONDET;
+    function _.onMorphoFlashLoan(uint256, bytes) external => NONDET;
+
+    function Morpho.supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
+    function Morpho.virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
+    function Morpho.virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
+    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
+
+    function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree;
+}
+
+function summaryExpectedSupplyAssets(MorphoHarness.MarketParams marketParams, address user) returns uint256 {
+    MorphoHarness.Id id = Util.libId(marketParams);
+
+    uint256 userShares = Morpho.supplyShares(id, user);
+    uint256 totalSupplyAssets = Morpho.virtualTotalSupplyAssets(id);
+    uint256 totalSupplyShares = Morpho.virtualTotalSupplyShares(id);
+
+    // Safe require because the reference implementation would revert.
+    return require_uint256(userShares * totalSupplyAssets / totalSupplyShares);
+}
+
+// Metamorpho's mulDiv (from OZ).
+function summaryMulDiv(uint256 x, uint256 y, uint256 d, Math.Rounding rounding) returns uint256 {
+    if (rounding == Math.Rounding.Floor) {
+        // Safe require because the reference implementation would revert.
+        return require_uint256((x * y) / d);
+    } else {
+        // Safe require because the reference implementation would revert.
+        return require_uint256((x * y + (d - 1)) / d);
+    }
+}
+
+// Morpho's mulDivUp.
+function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y + (d - 1)) / d);
+}
+
+// Morpho's mulDivDown.
+function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y) / d);
+}
+
+function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
+    MetaMorphoHarness.MarketParams marketParams;
+
+    // Safe require because:
+    // - markets in the supply/withdraw queue have positive lastUpdate (see LastUpdated.spec)
+    // - lastUpdate(id) > 0 => marketParams.id() == id is a verified invariant in Morpho Blue.
+    require Util.libId(marketParams) == id;
+
+    return marketParams;
+}
+
+// Note that it implies newLostAssets <= totalAssets.
+// Note that it implies realTotalAssets + lostAssets = lastTotalAssets after accrueInterest().
+invariant realPlusLostEqualsTotal()
+    realTotalAssets() + newLostAssets() == to_mathint(totalAssets());
+
+
+// LostAssets can only change after some bad debt has been realised or a market has been forced removed.
+rule lostAssetsOnlyMovesAfterUpdateWQueueAndLiquidate(method f, env e, calldataarg args)
+filtered {
+    f -> f.selector != sig:MorphoHarness.liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector &&
+        f.selector != sig:updateWithdrawQueue(uint256[]).selector
+}
+{
+    uint256 lostAssetsBefore = newLostAssets();
+
+    f(e, args);
+
+    uint256 lostAssetsAfter = newLostAssets();
+
+    assert lostAssetsBefore == lostAssetsAfter;
+}