Merge pull request #458 from morpho-labs/certora/remove-sload-munging

[Certora] remove `extSloads` munging
morpho-org · Aug 30, 2023 · c3ba07a · c3ba07a
2 parents ecad5e1 + 43397a3
commit c3ba07a
Show file tree

Hide file tree

Showing 11 changed files with 11 additions and 36 deletions.
diff --git a/certora/applyMunging.patch b/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))
--            }
--        }
--    }
- }
diff --git a/certora/specs/Blue.spec b/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;

diff --git a/certora/specs/BlueAccrueInterests.spec b/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);

diff --git a/certora/specs/BlueExitLiquidity.spec 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;

diff --git a/certora/specs/BlueLibSummary.spec b/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;

diff --git a/certora/specs/BlueLiveness.spec b/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;

diff --git a/certora/specs/BlueRatioMath.spec b/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;

diff --git a/certora/specs/BlueReverts.spec b/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;

diff --git a/certora/specs/DifficultMath.spec b/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;

diff --git a/certora/specs/Health.spec b/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;

diff --git a/certora/specs/Reentrancy.spec b/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;
 }