morpho-org · QGarchery · Sep 20, 2023 · Sep 15, 2023 · Sep 15, 2023 · Sep 16, 2023
diff --git a/.gitignore b/.gitignore
@@ -19,7 +19,6 @@ docs/
 # Certora
 .certora**
 emv-*-certora*
-certora/munged
 
 # Hardhat
 /types

diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol
@@ -1,9 +1,9 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.19;
 
-import "../munged/Morpho.sol";
-import "../munged/libraries/SharesMathLib.sol";
-import "../munged/libraries/MarketParamsLib.sol";
+import "../../src/Morpho.sol";
+import "../../src/libraries/SharesMathLib.sol";
+import "../../src/libraries/MarketParamsLib.sol";
 
 contract MorphoHarness is Morpho {
     using MarketParamsLib for MarketParams;
@@ -74,10 +74,8 @@ contract MorphoHarness is Morpho {
         return marketParams.id();
     }
 
-    function optimizedId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
-        assembly ("memory-safe") {
-            marketParamsId := keccak256(marketParams, mul(5, 32))
-        }
+    function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
+        marketParamsId = Id.wrap(keccak256(abi.encode(marketParams)));
     }
 
     function libMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {

diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol
@@ -1,8 +1,8 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity ^0.8.12;
 
-import "../munged/libraries/SafeTransferLib.sol";
-import "../munged/interfaces/IERC20.sol";
+import "../../src/libraries/SafeTransferLib.sol";
+import "../../src/interfaces/IERC20.sol";
 
 interface IERC20Extended is IERC20 {
     function balanceOf(address) external view returns (uint256);

diff --git a/certora/makefile b/certora/makefile
diff --git a/certora/munging.patch b/certora/munging.patch
diff --git a/certora/scripts/verifyAccrueInterest.sh b/certora/scripts/verifyAccrueInterest.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/AccrueInterest.spec \

diff --git a/certora/scripts/verifyConsistentState.sh b/certora/scripts/verifyConsistentState.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ConsistentState.spec \

diff --git a/certora/scripts/verifyExactMath.sh b/certora/scripts/verifyExactMath.sh
@@ -2,11 +2,9 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ExactMath.spec \
-    --prover_args '-smt_hashingScheme plaininjectivity -mediumTimeout 12' \
+    --prover_args '-smt_hashingScheme plaininjectivity -mediumTimeout 30' \
     --msg "Morpho Blue Exact Math" \
     "$@"
diff --git a/certora/scripts/verifyExitLiquidity.sh b/certora/scripts/verifyExitLiquidity.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/ExitLiquidity.spec \

diff --git a/certora/scripts/verifyHealth.sh b/certora/scripts/verifyHealth.sh
@@ -2,11 +2,9 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
-    certora/munged/mocks/OracleMock.sol \
+    src/mocks/OracleMock.sol \
     --verify MorphoHarness:certora/specs/Health.spec \
     --prover_args '-smt_hashingScheme plaininjectivity' \
     --msg "Morpho Blue Health Check" \

diff --git a/certora/scripts/verifyLibSummary.sh b/certora/scripts/verifyLibSummary.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/LibSummary.spec \

diff --git a/certora/scripts/verifyLiveness.sh b/certora/scripts/verifyLiveness.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoInternalAccess.sol \
     --verify MorphoInternalAccess:certora/specs/Liveness.spec \

diff --git a/certora/scripts/verifyRatioMath.sh b/certora/scripts/verifyRatioMath.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/RatioMath.spec \

diff --git a/certora/scripts/verifyReentrancy.sh b/certora/scripts/verifyReentrancy.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/Reentrancy.spec \

diff --git a/certora/scripts/verifyReverts.sh b/certora/scripts/verifyReverts.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/MorphoHarness.sol \
     --verify MorphoHarness:certora/specs/Reverts.spec \

diff --git a/certora/scripts/verifyTransfer.sh b/certora/scripts/verifyTransfer.sh
@@ -2,8 +2,6 @@
 
 set -euxo pipefail
 
-make -C certora munged
-
 certoraRun \
     certora/harness/TransferHarness.sol \
     certora/dispatch/ERC20Standard.sol \

diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec
@@ -4,22 +4,22 @@ methods {
     function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
     function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
-    function optimizedId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 }
 
-// Check the summary of mulDivUp required by RatioMath.spec
+// Check the summary of MathLib.mulDivUp required by RatioMath.spec
 rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) {
     uint256 result = libMulDivUp(x, y, d);
     assert result * d >= x * y;
 }
 
-// Check the summary of mulDivDown required by RatioMath.spec
+// Check the summary of MathLib.mulDivDown required by RatioMath.spec
 rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) {
     uint256 result = libMulDivDown(x, y, d);
     assert result * d <= x * y;
 }
 
-// Check the munging of the MarketParams.id function.
+// Check the summary of MarketParamsLib.id required by Liveness.spec
 rule checkSummaryId(MorphoHarness.MarketParams marketParams) {
-    assert optimizedId(marketParams) == libId(marketParams);
+    assert libId(marketParams) == refId(marketParams);
 }
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
@@ -11,9 +11,11 @@ methods {
     function fee(MorphoInternalAccess.Id) external returns uint256 envfree;
     function lastUpdate(MorphoInternalAccess.Id) external returns uint256 envfree;
     function libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree;
+    function refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree;
 
     function _._accrueInterest(MorphoInternalAccess.MarketParams memory marketParams, MorphoInternalAccess.Id id) internal with (env e) => summaryAccrueInterest(e, marketParams, id) expect void;
 
+    function MarketParamsLib.id(MorphoInternalAccess.MarketParams memory marketParams) internal returns MorphoInternalAccess.Id => summaryId(marketParams);
     function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value);
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
 }
@@ -22,6 +24,10 @@ ghost mapping(address => mathint) myBalances {
     init_state axiom (forall address token. myBalances[token] == 0);
 }
 
+function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id {
+    return refId(marketParams);
+}
+
 function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
     if (from == currentContract) {
         // Safe require because the reference implementation would revert.