diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol index 600515f4b..8101fc251 100644 --- a/certora/harness/MorphoHarness.sol +++ b/certora/harness/MorphoHarness.sol @@ -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/munging.patch b/certora/munging.patch index 8b490be5c..e69de29bb 100644 --- a/certora/munging.patch +++ b/certora/munging.patch @@ -1,14 +0,0 @@ - -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 -@@ -10,8 +10,6 @@ - library MarketParamsLib { - /// @notice Returns the id of the market `marketParams`. - function id(MarketParams memory marketParams) internal pure returns (Id marketParamsId) { -- assembly ("memory-safe") { -- marketParamsId := keccak256(marketParams, mul(5, 32)) -- } -+ marketParamsId = Id.wrap(keccak256(abi.encode(marketParams))); - } - } diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 784ca38d7..76cb6d80c 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -19,7 +19,7 @@ rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { assert result * d <= x * y; } -// Check the munging of the MarketParams.id function. +// Check the optimization of the MarketParams.id function. rule checkSummaryId(MorphoHarness.MarketParams marketParams) { - assert optimizedId(marketParams) == libId(marketParams); + assert libId(marketParams) == refId(marketParams); }