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 600515f4b..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; @@ -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 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 8b490be5c..000000000 --- a/certora/munging.patch +++ /dev/null @@ -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/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..0effcb7bd 100755 --- 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 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/LibSummary.spec b/certora/specs/LibSummary.spec index 784ca38d7..21cd67538 100644 --- 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 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.