From b3c7038f95defbeb82486574e84a0506fabb3a7f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 15 Sep 2023 15:28:57 +0200 Subject: [PATCH 1/5] feat: remove munging --- certora/harness/MorphoHarness.sol | 6 ++---- certora/munging.patch | 14 -------------- certora/specs/LibSummary.spec | 6 +++--- 3 files changed, 5 insertions(+), 21 deletions(-) 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..bfa47b7a7 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -4,7 +4,7 @@ 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 @@ -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); } From 73ad72d0bccb0fecbf6f2c8bfb7e08892f32da15 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 15 Sep 2023 16:28:11 +0200 Subject: [PATCH 2/5] feat: use summary of id in liveness --- certora/specs/LibSummary.spec | 6 +++--- certora/specs/Liveness.spec | 6 ++++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index bfa47b7a7..19251e0d6 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -7,19 +7,19 @@ methods { 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 optimization of the MarketParams.id function. +// Check the summary of MarketParams.id required by Liveness.spec rule checkSummaryId(MorphoHarness.MarketParams marketParams) { assert libId(marketParams) == refId(marketParams); } diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index cc4afba3d..c00456242 100644 --- 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. From 602804d524e61178e1f7a0fc836d5183e3f43a56 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sat, 16 Sep 2023 09:12:56 +0200 Subject: [PATCH 3/5] refactor: actual removal of munging files --- .gitignore | 1 - certora/harness/MorphoHarness.sol | 6 +++--- certora/harness/TransferHarness.sol | 4 ++-- certora/makefile | 12 ------------ certora/munging.patch | 0 certora/scripts/verifyAccrueInterest.sh | 2 -- certora/scripts/verifyConsistentState.sh | 2 -- certora/scripts/verifyExactMath.sh | 2 -- certora/scripts/verifyExitLiquidity.sh | 2 -- certora/scripts/verifyHealth.sh | 4 +--- certora/scripts/verifyLibSummary.sh | 2 -- certora/scripts/verifyLiveness.sh | 2 -- certora/scripts/verifyRatioMath.sh | 2 -- certora/scripts/verifyReentrancy.sh | 2 -- certora/scripts/verifyReverts.sh | 2 -- certora/scripts/verifyTransfer.sh | 2 -- certora/specs/ExactMath.spec | 6 ++++++ certora/specs/LibSummary.spec | 2 +- 18 files changed, 13 insertions(+), 42 deletions(-) delete mode 100644 certora/makefile delete mode 100644 certora/munging.patch diff --git a/.gitignore b/.gitignore index 718ea1943..84536674b 100644 --- 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 index 8101fc251..0f4ac6ed6 100644 --- 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; diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol index 1227e3fc7..5e6954a46 100644 --- 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 deleted file mode 100644 index 664ff4fb9..000000000 --- a/certora/makefile +++ /dev/null @@ -1,12 +0,0 @@ -munged: $(wildcard ../src/*.sol) munging.patch - @rm -rf munged - @cp -r ../src munged - @patch -p0 -d munged < munging.patch - -record: - diff -ruN ../src munged | sed 's+\.\./src/++g' | sed 's+munged/++g' > munging.patch - -clean: - rm -rf munged - -.PHONY: record clean # do not add munged here, as it is useful to protect munged edits diff --git a/certora/munging.patch b/certora/munging.patch deleted file mode 100644 index e69de29bb..000000000 diff --git a/certora/scripts/verifyAccrueInterest.sh b/certora/scripts/verifyAccrueInterest.sh index cf075e77a..7311c9e9c 100755 --- 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 index cd833fab3..47dd684f2 100755 --- 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 index b617213c8..f7c9bbe30 100755 --- a/certora/scripts/verifyExactMath.sh +++ b/certora/scripts/verifyExactMath.sh @@ -2,8 +2,6 @@ set -euxo pipefail -make -C certora munged - certoraRun \ certora/harness/MorphoHarness.sol \ --verify MorphoHarness:certora/specs/ExactMath.spec \ diff --git a/certora/scripts/verifyExitLiquidity.sh b/certora/scripts/verifyExitLiquidity.sh index 63c847707..afdd603e6 100755 --- 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 index 9d63978af..0bd7a7c2b 100755 --- 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 index 85b78dd6e..41dcf9ca0 100755 --- 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 index 396a94383..260bc3757 100755 --- 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 index 4faa6516f..c17eb1fc9 100755 --- 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 index cc9d7dbfc..0ffa2d570 100755 --- 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 index e89bc970d..ae2675499 100755 --- 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 index 633880f35..396585896 100755 --- 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/ExactMath.spec b/certora/specs/ExactMath.spec index 3ca2c3736..309ab7bdf 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -8,7 +8,9 @@ methods { function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; function fee(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function MarketParamsLib.id(MorphoHarness.MarketParams memory marketParams) internal returns MorphoHarness.Id => summaryId(marketParams); function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => NONDET; @@ -18,6 +20,10 @@ methods { function maxFee() external returns uint256 envfree; } +function summaryId(MorphoHarness.MarketParams marketParams) returns MorphoHarness.Id { + return refId(marketParams); +} + function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { // Safe require because the reference implementation would revert. return require_uint256((x * y + (d - 1)) / d); diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 19251e0d6..1f145d9ea 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 summary of MarketParams.id required by Liveness.spec +// Check the summary of MarketParamsLib.id required by Liveness.spec and ExactMath.spec rule checkSummaryId(MorphoHarness.MarketParams marketParams) { assert libId(marketParams) == refId(marketParams); } From c9142fdfb3e12d56590dd826a8fbd3e1040a2f98 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sat, 16 Sep 2023 13:07:47 +0200 Subject: [PATCH 4/5] refactor: remove summary id on ExactMath --- certora/specs/ExactMath.spec | 6 ------ certora/specs/LibSummary.spec | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index 309ab7bdf..3ca2c3736 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -8,9 +8,7 @@ methods { function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; function fee(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function MarketParamsLib.id(MorphoHarness.MarketParams memory marketParams) internal returns MorphoHarness.Id => summaryId(marketParams); function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => NONDET; @@ -20,10 +18,6 @@ methods { function maxFee() external returns uint256 envfree; } -function summaryId(MorphoHarness.MarketParams marketParams) returns MorphoHarness.Id { - return refId(marketParams); -} - function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { // Safe require because the reference implementation would revert. return require_uint256((x * y + (d - 1)) / d); diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 1f145d9ea..21cd67538 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 summary of MarketParamsLib.id required by Liveness.spec and ExactMath.spec +// Check the summary of MarketParamsLib.id required by Liveness.spec rule checkSummaryId(MorphoHarness.MarketParams marketParams) { assert libId(marketParams) == refId(marketParams); } From b8680aeba206f1998666f1525d8082d0545f5314 Mon Sep 17 00:00:00 2001 From: ALEX JOSEPH Date: Wed, 20 Sep 2023 08:32:38 +0100 Subject: [PATCH 5/5] increase medium timeout to 30 --- certora/scripts/verifyExactMath.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/scripts/verifyExactMath.sh b/certora/scripts/verifyExactMath.sh index f7c9bbe30..0effcb7bd 100755 --- a/certora/scripts/verifyExactMath.sh +++ b/certora/scripts/verifyExactMath.sh @@ -5,6 +5,6 @@ set -euxo pipefail 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" \ "$@"