diff --git a/.gitignore b/.gitignore index 391cee8d..49dd509d 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,7 @@ docs/ # Certora .certora** emv-*-certora* +certora/munged # Dotenv file .env diff --git a/certora/makefile b/certora/makefile new file mode 100644 index 00000000..664ff4fb --- /dev/null +++ b/certora/makefile @@ -0,0 +1,12 @@ +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 new file mode 100644 index 00000000..d3fd532a --- /dev/null +++ b/certora/munging.patch @@ -0,0 +1,12 @@ +diff -ruN Irm.sol Irm.sol +--- Irm.sol 2023-09-19 15:59:58.045886731 +0200 ++++ Irm.sol 2023-09-19 16:09:50.491751975 +0200 +@@ -38,7 +38,7 @@ + /// @notice Speed factor (scaled by WAD). + uint256 public immutable SPEED_FACTOR; + /// @notice Target utilization (scaled by WAD). +- uint256 public immutable TARGET_UTILIZATION; ++ uint256 public TARGET_UTILIZATION; + /// @notice Initial rate (scaled by WAD). + uint128 public immutable INITIAL_RATE; + diff --git a/certora/scripts/verifyLiveness.sh b/certora/scripts/verifyLiveness.sh index 033de521..226ea6b2 100755 --- a/certora/scripts/verifyLiveness.sh +++ b/certora/scripts/verifyLiveness.sh @@ -2,6 +2,8 @@ set -euxo pipefail +make -C certora munged + certoraRun \ src/Irm.sol \ --verify Irm:certora/specs/Liveness.spec \