diff --git a/certora/Makefile b/certora/Makefile index 2068786..bd52f7a 100644 --- a/certora/Makefile +++ b/certora/Makefile @@ -1,12 +1,14 @@ -munged: $(wildcard ../src/*.sol) applyMunging.patch - @rm -rf munged - @cp -r ../src munged - @patch -p0 -d munged < applyMunging.patch +munged: ../munged + +../munged: $(wildcard ../src/*.sol) applyMunging.patch + @rm -rf ../munged + @cp -r ../src ../munged + @patch -p0 -d ../munged < applyMunging.patch record: - diff -ruN ../src munged | sed 's+ \.\./src/+ +g' | sed 's+munged/++g' > applyMunging.patch + diff -ruN ../src ../munged | sed 's+ \.\./src/+ +g' | sed 's+ \.\./munged/+ +g' > applyMunging.patch clean: - rm -rf munged + rm -rf ../munged -.PHONY: help clean # do not add munged here, as it is useful to protect munged edits +.PHONY: clean record munged # Do not add ../munged here, as it is useful to protect munged edits diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch index 27ff6e8..1e5b4e6 100644 --- a/certora/applyMunging.patch +++ b/certora/applyMunging.patch @@ -1,26 +1,6 @@ diff -ruN DelegationToken.sol DelegationToken.sol --- DelegationToken.sol 2024-11-14 11:00:56.877231237 +0100 -+++ DelegationToken.sol 2024-11-20 16:18:55.750677310 +0100 -@@ -4,14 +4,14 @@ - import {IDelegation, Signature, Delegation} from "./interfaces/IDelegation.sol"; - - import {ERC20PermitUpgradeable} from -- "../lib/openzeppelin-contracts-upgradeable/contracts/token/ERC20/extensions/ERC20PermitUpgradeable.sol"; -+ "../../lib/openzeppelin-contracts-upgradeable/contracts/token/ERC20/extensions/ERC20PermitUpgradeable.sol"; - import {ECDSA} from -- "../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol"; -+ "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/cryptography/ECDSA.sol"; - import {Ownable2StepUpgradeable} from -- "../lib/openzeppelin-contracts-upgradeable/contracts/access/Ownable2StepUpgradeable.sol"; --import {UUPSUpgradeable} from "../lib/openzeppelin-contracts-upgradeable/contracts/proxy/utils/UUPSUpgradeable.sol"; -+ "../../lib/openzeppelin-contracts-upgradeable/contracts/access/Ownable2StepUpgradeable.sol"; -+import {UUPSUpgradeable} from "../../lib/openzeppelin-contracts-upgradeable/contracts/proxy/utils/UUPSUpgradeable.sol"; - import {ERC1967Utils} from -- "../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/proxy/ERC1967/ERC1967Utils.sol"; -+ "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/proxy/ERC1967/ERC1967Utils.sol"; - - /// @title DelegationToken - /// @author Morpho Association ++++ DelegationToken.sol 2024-11-20 16:37:42.398598564 +0100 @@ -44,6 +44,9 @@ mapping(address => uint256) _delegationNonce; } @@ -48,21 +28,9 @@ diff -ruN DelegationToken.sol DelegationToken.sol } } } -diff -ruN interfaces/IOptimismMintableERC20.sol interfaces/IOptimismMintableERC20.sol ---- interfaces/IOptimismMintableERC20.sol 2024-11-14 11:00:56.877231237 +0100 -+++ interfaces/IOptimismMintableERC20.sol 2024-11-20 16:30:24.300071161 +0100 -@@ -2,7 +2,7 @@ - pragma solidity >=0.5.0; - - import {IERC165} from -- "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/introspection/IERC165.sol"; -+ "../../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/introspection/IERC165.sol"; - - /// @title IOptimismMintableERC20 - /// @author Morpho Association diff -ruN MorphoTokenEthereum.sol MorphoTokenEthereum.sol --- MorphoTokenEthereum.sol 2024-11-14 11:00:56.877231237 +0100 -+++ MorphoTokenEthereum.sol 2024-11-20 13:29:38.986459880 +0100 ++++ MorphoTokenEthereum.sol 2024-11-20 16:37:42.399598538 +0100 @@ -26,16 +26,19 @@ __ERC20Permit_init(NAME); __Ownable_init(owner); @@ -85,16 +53,7 @@ diff -ruN MorphoTokenEthereum.sol MorphoTokenEthereum.sol } diff -ruN MorphoTokenOptimism.sol MorphoTokenOptimism.sol --- MorphoTokenOptimism.sol 2024-11-14 11:00:56.877231237 +0100 -+++ MorphoTokenOptimism.sol 2024-11-20 16:19:11.314241653 +0100 -@@ -3,7 +3,7 @@ - - import {IOptimismMintableERC20} from "./interfaces/IOptimismMintableERC20.sol"; - import {IERC165} from -- "../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/introspection/IERC165.sol"; -+ "../../lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts/utils/introspection/IERC165.sol"; - - import {DelegationToken} from "./DelegationToken.sol"; - ++++ MorphoTokenOptimism.sol 2024-11-20 16:37:42.399598538 +0100 @@ -69,12 +69,14 @@ /// @dev Allows the StandardBridge on this network to mint tokens. diff --git a/certora/confs/DelegationEthereum.conf b/certora/confs/DelegationEthereum.conf index a46b73b..6aa775c 100644 --- a/certora/confs/DelegationEthereum.conf +++ b/certora/confs/DelegationEthereum.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/munged/MorphoTokenEthereum.sol" + "munged/MorphoTokenEthereum.sol" ], "parametric_contracts": [ "MorphoTokenEthereum" diff --git a/certora/confs/DelegationOptimism.conf b/certora/confs/DelegationOptimism.conf index afb9a73..fb3517e 100644 --- a/certora/confs/DelegationOptimism.conf +++ b/certora/confs/DelegationOptimism.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/munged/MorphoTokenOptimism.sol" + "munged/MorphoTokenOptimism.sol" ], "parametric_contracts": [ "MorphoTokenOptimism"