feat: harness last index withdraw

morpho-org · Mar 22, 2024 · d7cfaf0 · d7cfaf0
1 parent 5f50dc9
commit d7cfaf0
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 15 deletions.
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-01-03 14:41:15.012185229 +0100
-+++ interfaces/IMetaMorpho.sol	2024-03-04 17:27:18.336468241 +0100
+--- interfaces/IMetaMorpho.sol	2024-03-20 15:13:25.818251404 +0100
++++ interfaces/IMetaMorpho.sol	2024-03-22 11:22:35.598510490 +0100
 @@ -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-01-03 14:27:38.058744959 +0100
-+++ libraries/ErrorsLib.sol	2024-02-13 10:07:21.879957695 +0100
+--- libraries/ErrorsLib.sol	2024-03-20 15:13:25.802251714 +0100
++++ libraries/ErrorsLib.sol	2024-03-22 11:22:35.598510490 +0100
 @@ -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	2023-11-27 12:37:13.369852625 +0100
-+++ libraries/EventsLib.sol	2024-02-13 10:07:21.879957695 +0100
+--- libraries/EventsLib.sol	2024-03-20 15:13:25.802251714 +0100
++++ libraries/EventsLib.sol	2024-03-22 11:22:35.598510490 +0100
 @@ -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-02-02 13:00:21.238074050 +0100
-+++ MetaMorpho.sol	2024-03-04 23:26:21.562604750 +0100
+--- MetaMorpho.sol	2024-03-20 15:13:25.862250553 +0100
++++ MetaMorpho.sol	2024-03-22 11:25:47.991055286 +0100
 @@ -9,24 +9,22 @@
      IMetaMorphoBase,
      IMetaMorphoStaticTyping
@@ -114,10 +114,14 @@ 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,15 @@
+@@ -107,6 +103,19 @@
      /// @inheritdoc IMetaMorphoBase
      uint256 public lastTotalAssets;
 
++    // HARNESS
++    // The index of the identifier of the last market withdrawn.
++    uint256 lastIndexWithdraw;
++
 +    // HARNESS
 +    // The rank of a market identifier in the withdraw queue.
 +    // Returns 0 if the corresponding market is not in the withdraw queue.
@@ -130,7 +134,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
      /* CONSTRUCTOR */
 
      /// @dev Initializes the contract.
-@@ -126,7 +131,7 @@
+@@ -126,7 +135,7 @@
      ) ERC4626(IERC20(_asset)) ERC20Permit(_name) ERC20(_name, _symbol) Ownable(owner) {
          if (morpho == address(0)) revert ErrorsLib.ZeroAddress();
 
@@ -139,7 +143,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          DECIMALS_OFFSET = uint8(uint256(18).zeroFloorSub(IERC20Metadata(_asset).decimals()));
 
          _checkTimelockBounds(initialTimelock);
-@@ -338,6 +343,9 @@
+@@ -338,6 +347,9 @@
              seen[prevIndex] = true;
 
              newWithdrawQueue[i] = id;
@@ -149,7 +153,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
          }
 
          for (uint256 i; i < currLength; ++i) {
-@@ -355,6 +363,10 @@
+@@ -355,6 +367,10 @@
                      }
                  }
 
@@ -160,7 +164,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  delete config[id];
              }
          }
-@@ -743,6 +755,9 @@
+@@ -743,6 +759,9 @@
 
          if (supplyCap > 0) {
              if (!marketConfig.enabled) {
@@ -170,3 +174,13 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol
                  withdrawQueue.push(id);
 
                  if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded();
+@@ -802,6 +821,9 @@
+     /// @dev Withdraws `assets` from Morpho.
+     function _withdrawMorpho(uint256 assets) internal {
+         for (uint256 i; i < withdrawQueue.length; ++i) {
++            // HARNESS
++            lastIndexWithdraw = i;
++
+             Id id = withdrawQueue[i];
+             MarketParams memory marketParams = _marketParams(id);
+             (uint256 supplyAssets,, Market memory market) = _accruedSupplyBalance(marketParams, id);
diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
@@ -5,6 +5,8 @@ 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 _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL;
+
+    function lastIndexWithdraw() external returns(uint256) envfree;
 }
 
 function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams {
@@ -39,9 +41,9 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     assert receiver == currentContract;
 
     MetaMorphoHarness.Id id = Util.libId(marketParams);
-    uint256 rank = withdrawRank(id);
+    uint256 index = lastIndexWithdraw();
     // Safe require because it is a verified invariant.
-    require isInWithdrawQueueIsEnabled(assert_uint256(rank - 1));
+    require isInWithdrawQueueIsEnabled(index);
     // Safe require because it is a verified invariant
     require isWithdrawRankCorrect(id);