[Certora] remove extSloads munging

certora/applyMunging.patch

@@ -1,14 +1,4 @@
-diff -ruN interfaces/IMorpho.sol interfaces/IMorpho.sol
---- interfaces/IMorpho.sol	2023-08-29 09:58:51.628147127 +0200
-+++ interfaces/IMorpho.sol	2023-08-29 10:15:36.946593577 +0200
-@@ -292,7 +292,4 @@
-     /// @param authorization The `Authorization` struct.
-     /// @param signature The signature.
-     function setAuthorizationWithSig(Authorization calldata authorization, Signature calldata signature) external;
--
--    /// @notice Returns the data stored on the different `slots`.
--    function extSloads(bytes32[] memory slots) external view returns (bytes32[] memory);
- }
+
 diff -ruN libraries/MarketParamsLib.sol libraries/MarketParamsLib.sol
 --- libraries/MarketParamsLib.sol	2023-08-29 09:59:37.937583556 +0200
 +++ libraries/MarketParamsLib.sol	2023-08-29 10:16:10.519752188 +0200
@@ -22,28 +12,3 @@ diff -ruN libraries/MarketParamsLib.sol libraries/MarketParamsLib.sol
 +        marketParamsId = Id.wrap(keccak256(abi.encode(marketParams)));
      }
  }
-diff -ruN Morpho.sol Morpho.sol
---- Morpho.sol	2023-08-29 09:58:43.158169812 +0200
-+++ Morpho.sol	2023-08-29 10:15:20.650012827 +0200
-@@ -502,21 +502,4 @@
-
-         return maxBorrow >= borrowed;
-     }
--
--    /* STORAGE VIEW */
--
--    /// @inheritdoc IMorpho
--    function extSloads(bytes32[] calldata slots) external view returns (bytes32[] memory res) {
--        uint256 nSlots = slots.length;
--
--        res = new bytes32[](nSlots);
--
--        for (uint256 i; i < nSlots;) {
--            bytes32 slot = slots[i++];
--
--            assembly ("memory-safe") {
--                mstore(add(res, mul(i, 32)), sload(slot))
--            }
--        }
--    }
- }

certora/specs/Blue.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;

certora/specs/BlueAccrueInterests.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c);
     function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b);

certora/specs/BlueExitLiquidity.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getSupplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function getCollateral(MorphoHarness.Id, address) external returns uint256 envfree;

certora/specs/BlueLibSummary.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
     function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
     function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;

certora/specs/BlueLiveness.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getTotalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
     function getTotalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree;
     function getTotalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree;

certora/specs/BlueRatioMath.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;

certora/specs/BlueReverts.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function owner() external returns address envfree;
     function getTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;

certora/specs/DifficultMath.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;

certora/specs/Health.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function getLastUpdate(MorphoHarness.Id) external returns uint256 envfree;
     function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree;

certora/specs/Reentrancy.spec

@@ -1,4 +1,5 @@
 methods {
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
     function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256;
 }