From e3f841276dc9ad42a61306f519f2f5ea9c5e8853 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 5 Sep 2023 16:41:38 +0200
Subject: [PATCH] feat: add CI and munging

---
 .github/workflows/certora.yml                 | 53 +++++++++++++++++++
 .gitignore                                    |  5 ++
 certora/makefile                              | 12 +++++
 certora/munging.patch                         | 12 +++++
 .../{liveness.sh => verifyLiveness.sh}        |  6 ++-
 .../specs/{liveness.spec => Liveness.spec}    |  0
 6 files changed, 86 insertions(+), 2 deletions(-)
 create mode 100644 .github/workflows/certora.yml
 create mode 100644 certora/makefile
 create mode 100644 certora/munging.patch
 rename certora/scripts/{liveness.sh => verifyLiveness.sh} (54%)
 rename certora/specs/{liveness.spec => Liveness.spec} (100%)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 00000000..f6fda62c
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,53 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Generate a token
+        id: generate-token
+        uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92
+        with:
+          app_id: ${{ secrets.APP_ID }}
+          private_key: ${{ secrets.APP_PRIVATE_KEY }}
+
+      - uses: actions/checkout@v3
+        with:
+          token: ${{ steps.generate-token.outputs.token }}
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v4
+        with:
+          python-version: "3.10"
+
+      - name: Install certora
+        run: pip install certora-cli-beta
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
+
+      - name: Verify rule ${{ matrix.script }}
+        run: |
+          echo "key length" ${#CERTORAKEY}
+          bash certora/scripts/${{ matrix.script }} --solc solc8.19
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        script:
+          - verifyLiveness.sh
diff --git a/.gitignore b/.gitignore
index 85198aaa..49dd509d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,5 +10,10 @@ out/
 # Docs
 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/liveness.sh b/certora/scripts/verifyLiveness.sh
similarity index 54%
rename from certora/scripts/liveness.sh
rename to certora/scripts/verifyLiveness.sh
index 5d6cb71e..226ea6b2 100755
--- a/certora/scripts/liveness.sh
+++ b/certora/scripts/verifyLiveness.sh
@@ -2,10 +2,12 @@
 
 set -euxo pipefail
 
+make -C certora munged
+
 certoraRun \
     src/Irm.sol \
-    --verify Irm:certora/specs/liveness.spec \
-    --msg "IRM liveness" \
+    --verify Irm:certora/specs/Liveness.spec \
+    --msg "IRM Liveness" \
     --solc_via_ir \
     --solc_optimize 200 \
     "$@"
diff --git a/certora/specs/liveness.spec b/certora/specs/Liveness.spec
similarity index 100%
rename from certora/specs/liveness.spec
rename to certora/specs/Liveness.spec