From f51bb61160f98ad5af3c2f4c5bb06199b253dc31 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Mon, 17 Apr 2023 23:25:32 +0000
Subject: [PATCH 01/17] .github/: update github workflows

---
 .github/actions/with-docker/action.yml | 40 +++++++++++++++++++++++
 .github/workflows/Dockerfile           | 44 ++++++++++++++++++++++++++
 .github/workflows/Dockerfile.z3        | 22 +++++++++++++
 .github/workflows/test-pr.yml          | 34 ++++++++++++++++++++
 .github/workflows/test.yml             | 34 --------------------
 5 files changed, 140 insertions(+), 34 deletions(-)
 create mode 100644 .github/actions/with-docker/action.yml
 create mode 100644 .github/workflows/Dockerfile
 create mode 100644 .github/workflows/Dockerfile.z3
 create mode 100644 .github/workflows/test-pr.yml
 delete mode 100644 .github/workflows/test.yml

diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
new file mode 100644
index 0000000..693d97a
--- /dev/null
+++ b/.github/actions/with-docker/action.yml
@@ -0,0 +1,40 @@
+name: 'With Docker'
+description: 'Run a given stage with Docker Image'
+inputs:
+  tag:
+    description: 'Docker image tag to use'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+  - name: 'Set up Docker'
+    shell: bash {0}
+    env:
+      TAG_NAME: ${{ inputs.tag }}
+    run: |
+      set -euxo pipefail
+
+      Z3_VERSION=4.8.15
+      K_COMMIT=$(cat deps/k_release)
+
+      docker build .                           \
+        --file .github/workflows/Dockerfile.z3 \
+        --tag z3:${Z3_VERSION}                 \
+
+      docker build . --file .github/workflows/Dockerfile \
+        --tag runtimeverification/${TAG_NAME}            \
+        --build-arg K_COMMIT=${K_COMMIT}                 \
+        --build-arg Z3_VERSION=${Z3_VERSION}             \
+
+      docker run                        \
+        --name ${TAG_NAME}              \
+        --rm                            \
+        --interactive                   \
+        --tty                           \
+        --detach                        \
+        --user root                     \
+        --workdir /home/user            \
+        runtimeverification/${TAG_NAME} \
+
+      docker cp . ${TAG_NAME}:/home/user
+      docker exec ${TAG_NAME} chown -R user:user /home/user
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
new file mode 100644
index 0000000..c7e41a0
--- /dev/null
+++ b/.github/workflows/Dockerfile
@@ -0,0 +1,44 @@
+ARG K_COMMIT
+ARG Z3_VERSION
+FROM ghcr.io/foundry-rs/foundry:nightly-aeba75e4799f1e11e3daba98d967b83e286b0c4a as FOUNDRY
+
+ARG K_COMMIT
+ARG Z3_VERSION
+FROM z3:${Z3_VERSION} as Z3
+
+ARG K_COMMIT
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT}
+
+COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
+COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
+COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+
+COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
+
+RUN    apt-get update                                   \
+    && apt-get install --yes software-properties-common \
+    && add-apt-repository ppa:ethereum/ethereum
+
+RUN    apt-get update         \
+    && apt-get upgrade --yes  \
+    && apt-get install --yes  \
+            cmake             \
+            curl              \
+            libcrypto++-dev   \
+            libprocps-dev     \
+            libsecp256k1-dev  \
+            libssl-dev        \
+            netcat            \
+            protobuf-compiler \
+            python3           \
+            python3-pip       \
+            solc
+
+RUN curl -sSL https://install.python-poetry.org | POETRY_HOME=/usr python3 - --version 1.3.2
+
+ARG USER_ID=1000
+ARG GROUP_ID=1000
+RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
+
+USER user:user
+WORKDIR /home/user
diff --git a/.github/workflows/Dockerfile.z3 b/.github/workflows/Dockerfile.z3
new file mode 100644
index 0000000..50d2d1a
--- /dev/null
+++ b/.github/workflows/Dockerfile.z3
@@ -0,0 +1,22 @@
+FROM ubuntu:jammy
+
+ENV TZ=America/Chicago
+RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
+
+RUN    apt-get update        \
+    && apt-get upgrade --yes \
+    && apt-get install --yes \
+            clang            \
+            cmake            \
+            git              \
+            python3
+
+ARG Z3_VERSION=4.8.15
+RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-${Z3_VERSION} \
+    && cd z3                                                                \
+    && python3 scripts/mk_make.py                                           \
+    && cd build                                                             \
+    && make -j8                                                             \
+    && make install                                                         \
+    && cd ../..                                                             \
+    && rm -rf z3
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
new file mode 100644
index 0000000..a559b32
--- /dev/null
+++ b/.github/workflows/test-pr.yml
@@ -0,0 +1,34 @@
+name: 'Test PR'
+on:
+  pull_request:
+    branches:
+      - 'master'
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+
+  test-forge:
+    name: 'Build and Test KEVM concrete execution'
+    needs: version-bump
+    runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 25
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          fetch-depth: 0
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          tag: foundry-demo-ci-forge-${{ github.sha }}
+      - name: 'Forge build'
+        run: docker exec -u user foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
+      - name: 'Forge test'
+        run: docker exec -u user foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge test -vvv'
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 foundry-demo-ci-forge-${GITHUB_SHA}
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
deleted file mode 100644
index 09880b1..0000000
--- a/.github/workflows/test.yml
+++ /dev/null
@@ -1,34 +0,0 @@
-name: test
-
-on: workflow_dispatch
-
-env:
-  FOUNDRY_PROFILE: ci
-
-jobs:
-  check:
-    strategy:
-      fail-fast: true
-
-    name: Foundry project
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          submodules: recursive
-
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-        with:
-          version: nightly
-
-      - name: Run Forge build
-        run: |
-          forge --version
-          forge build --sizes
-        id: build
-
-      - name: Run Forge tests
-        run: |
-          forge test -vvv
-        id: test

From 424027646b389d994b26c27ace20f9d2f9672299 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Mon, 17 Apr 2023 23:28:40 +0000
Subject: [PATCH 02/17] .github/test-pr: run KEVM prover on CI too

---
 .github/workflows/test-pr.yml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index a559b32..dd5d9d8 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -32,3 +32,30 @@ jobs:
         if: always()
         run: |
           docker stop --time=0 foundry-demo-ci-forge-${GITHUB_SHA}
+
+  test-prove:
+    name: 'Build and Test KEVM concrete execution'
+    needs: version-bump
+    runs-on: [self-hosted, linux, normal]
+    needs: forge-test
+    timeout-minutes: 90
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          fetch-depth: 0
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          tag: foundry-demo-ci-kevm-${{ github.sha }}
+      - name: 'Forge build'
+        run: docker exec -u user foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
+      - name: 'KEVM kompile'
+        run: docker exec -u user foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose'
+      - name: 'KEVM prove'
+        run: docker exec -u user foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-prove --verbose -j8'
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 foundry-demo-ci-kevm-${GITHUB_SHA}

From 938f184ede55fe8019b69f93d3fc5f6bbfe92663 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Mon, 17 Apr 2023 23:29:39 +0000
Subject: [PATCH 03/17] .github/test-pr: remove needs clause from test-forge

---
 .github/workflows/test-pr.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index dd5d9d8..ecf7721 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -11,7 +11,6 @@ jobs:
 
   test-forge:
     name: 'Build and Test KEVM concrete execution'
-    needs: version-bump
     runs-on: [self-hosted, linux, normal]
     timeout-minutes: 25
     steps:

From 7296ad64b11ecb32720d1a683467237c1fbfe58b Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Mon, 17 Apr 2023 23:30:15 +0000
Subject: [PATCH 04/17] .github/test-pr: correct needs name

---
 .github/workflows/test-pr.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index ecf7721..36b315f 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -36,7 +36,7 @@ jobs:
     name: 'Build and Test KEVM concrete execution'
     needs: version-bump
     runs-on: [self-hosted, linux, normal]
-    needs: forge-test
+    needs: test-forge
     timeout-minutes: 90
     steps:
       - name: 'Check out code'

From e1e57032ef3672b364891f1f7ca5ec90837baf2e Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Mon, 17 Apr 2023 23:33:50 +0000
Subject: [PATCH 05/17] .github/test-pr: correct syntax

---
 .github/workflows/test-pr.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 36b315f..3cd30ad 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -34,9 +34,8 @@ jobs:
 
   test-prove:
     name: 'Build and Test KEVM concrete execution'
-    needs: version-bump
-    runs-on: [self-hosted, linux, normal]
     needs: test-forge
+    runs-on: [self-hosted, linux, normal]
     timeout-minutes: 90
     steps:
       - name: 'Check out code'

From 93df39f194feb7182b3912a1a846318d6f59e35e Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 03:55:44 +0000
Subject: [PATCH 06/17] .github/, Dockerfile: updates

---
 .github/actions/with-docker/action.yml | 28 ++++++++++++--------------
 .github/workflows/Dockerfile           |  2 ++
 .github/workflows/Dockerfile.z3        | 22 --------------------
 Dockerfile                             | 26 ++++++++++++++++++++++++
 4 files changed, 41 insertions(+), 37 deletions(-)
 delete mode 100644 .github/workflows/Dockerfile.z3
 create mode 100644 Dockerfile

diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index 693d97a..7d05252 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -14,17 +14,15 @@ runs:
     run: |
       set -euxo pipefail
 
-      Z3_VERSION=4.8.15
-      K_COMMIT=$(cat deps/k_release)
+      USER=$(id -un)
+      USER_ID=$(id -u)
+      GROUP=$(id -gn)
+      GROUP_ID=$(id -g)
 
-      docker build .                           \
-        --file .github/workflows/Dockerfile.z3 \
-        --tag z3:${Z3_VERSION}                 \
-
-      docker build . --file .github/workflows/Dockerfile \
-        --tag runtimeverification/${TAG_NAME}            \
-        --build-arg K_COMMIT=${K_COMMIT}                 \
-        --build-arg Z3_VERSION=${Z3_VERSION}             \
+      docker build . --file Dockerfile                              \
+        --tag runtimeverification/${TAG_NAME}                       \
+        --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
+        --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID}
 
       docker run                        \
         --name ${TAG_NAME}              \
@@ -32,9 +30,9 @@ runs:
         --interactive                   \
         --tty                           \
         --detach                        \
-        --user root                     \
-        --workdir /home/user            \
+        --user ${USER}:${GROUP}         \
+        -v "$(pwd):/opt/workspace"      \
+        -v "/etc/passwd:/etc/passwd:ro" \
+        -v "/etc/group:/etc/group:ro"   \
+        --workdir /opt/workspace        \
         runtimeverification/${TAG_NAME} \
-
-      docker cp . ${TAG_NAME}:/home/user
-      docker exec ${TAG_NAME} chown -R user:user /home/user
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
index c7e41a0..c829b11 100644
--- a/.github/workflows/Dockerfile
+++ b/.github/workflows/Dockerfile
@@ -42,3 +42,5 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
 
 USER user:user
 WORKDIR /home/user
+
+RUN bash <(curl https://kframework.org/install)
diff --git a/.github/workflows/Dockerfile.z3 b/.github/workflows/Dockerfile.z3
deleted file mode 100644
index 50d2d1a..0000000
--- a/.github/workflows/Dockerfile.z3
+++ /dev/null
@@ -1,22 +0,0 @@
-FROM ubuntu:jammy
-
-ENV TZ=America/Chicago
-RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
-
-RUN    apt-get update        \
-    && apt-get upgrade --yes \
-    && apt-get install --yes \
-            clang            \
-            cmake            \
-            git              \
-            python3
-
-ARG Z3_VERSION=4.8.15
-RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-${Z3_VERSION} \
-    && cd z3                                                                \
-    && python3 scripts/mk_make.py                                           \
-    && cd build                                                             \
-    && make -j8                                                             \
-    && make install                                                         \
-    && cd ../..                                                             \
-    && rm -rf z3
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..14d2041
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,26 @@
+ARG Z3_VERSION
+FROM ghcr.io/foundry-rs/foundry:nightly-aeba75e4799f1e11e3daba98d967b83e286b0c4a as FOUNDRY
+
+FROM ubuntu:jammy
+
+COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
+COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
+COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+
+RUN    apt-get update           \
+    && apt-get upgrade --yes    \
+    && apt-get install --yes    \
+            curl                \
+            sudo
+
+ARG USER=user
+ARG GROUP=${USER}
+ARG USER_ID=1000
+ARG GROUP_ID=${USER_ID}
+RUN    groupadd -g ${GROUP_ID} ${USER} \
+    && useradd -m -u ${USER_ID} -s /bin/sh -g ${GROUP} -G sudo ${USER}
+
+RUN echo "${USER} ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
+
+USER user:user
+WORKDIR /home/user

From 83d58bf4855562d88525dad088bfdff62b953d26 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 16:54:22 +0000
Subject: [PATCH 07/17] .github/with-docker: no need to copy in shadow iles

---
 .github/actions/with-docker/action.yml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
index 7d05252..c394ff1 100644
--- a/.github/actions/with-docker/action.yml
+++ b/.github/actions/with-docker/action.yml
@@ -32,7 +32,5 @@ runs:
         --detach                        \
         --user ${USER}:${GROUP}         \
         -v "$(pwd):/opt/workspace"      \
-        -v "/etc/passwd:/etc/passwd:ro" \
-        -v "/etc/group:/etc/group:ro"   \
         --workdir /opt/workspace        \
         runtimeverification/${TAG_NAME} \

From 3a279ba22559555867bb554e90055774169b0629 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 16:55:10 +0000
Subject: [PATCH 08/17] .github/test-pr: better stage names

---
 .github/workflows/test-pr.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 3cd30ad..c5268f3 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -10,7 +10,7 @@ concurrency:
 jobs:
 
   test-forge:
-    name: 'Build and Test KEVM concrete execution'
+    name: 'Test with Foundry'
     runs-on: [self-hosted, linux, normal]
     timeout-minutes: 25
     steps:
@@ -33,7 +33,7 @@ jobs:
           docker stop --time=0 foundry-demo-ci-forge-${GITHUB_SHA}
 
   test-prove:
-    name: 'Build and Test KEVM concrete execution'
+    name: 'Verify with KEVM'
     needs: test-forge
     runs-on: [self-hosted, linux, normal]
     timeout-minutes: 90

From ef38e493ae141434f2609baf78878c80bbd54c08 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 17:10:23 +0000
Subject: [PATCH 09/17] .github/test-pr: adjust docker exec invocations

---
 .github/workflows/test-pr.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index c5268f3..1fdbb8b 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -24,9 +24,9 @@ jobs:
         with:
           tag: foundry-demo-ci-forge-${{ github.sha }}
       - name: 'Forge build'
-        run: docker exec -u user foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
+        run: docker exec --tty foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'Forge test'
-        run: docker exec -u user foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge test -vvv'
+        run: docker exec --tty foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge test -vvv'
       - name: 'Tear down Docker'
         if: always()
         run: |
@@ -48,11 +48,11 @@ jobs:
         with:
           tag: foundry-demo-ci-kevm-${{ github.sha }}
       - name: 'Forge build'
-        run: docker exec -u user foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
+        run: docker exec --tty foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'KEVM kompile'
-        run: docker exec -u user foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose'
+        run: docker exec --tty foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose'
       - name: 'KEVM prove'
-        run: docker exec -u user foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-prove --verbose -j8'
+        run: docker exec --tty foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-prove --verbose -j8'
       - name: 'Tear down Docker'
         if: always()
         run: |

From c3a8a62cc2bf7448404255ba17a7bae726c7efc7 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 21:33:12 +0000
Subject: [PATCH 10/17] .github/test-pr: remove tty

---
 .github/workflows/test-pr.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 1fdbb8b..5c1a573 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -24,9 +24,9 @@ jobs:
         with:
           tag: foundry-demo-ci-forge-${{ github.sha }}
       - name: 'Forge build'
-        run: docker exec --tty foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
+        run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'Forge test'
-        run: docker exec --tty foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge test -vvv'
+        run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge test -vvv'
       - name: 'Tear down Docker'
         if: always()
         run: |
@@ -48,11 +48,11 @@ jobs:
         with:
           tag: foundry-demo-ci-kevm-${{ github.sha }}
       - name: 'Forge build'
-        run: docker exec --tty foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'KEVM kompile'
-        run: docker exec --tty foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose'
       - name: 'KEVM prove'
-        run: docker exec --tty foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-prove --verbose -j8'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-prove --verbose -j8'
       - name: 'Tear down Docker'
         if: always()
         run: |

From 46412a20d2ab71e8f8607b48f3b2f2839a9d045a Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 21:37:15 +0000
Subject: [PATCH 11/17] Dockerfile: adjustments

---
 Dockerfile | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 14d2041..707f4a6 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,11 +1,9 @@
-ARG Z3_VERSION
 FROM ghcr.io/foundry-rs/foundry:nightly-aeba75e4799f1e11e3daba98d967b83e286b0c4a as FOUNDRY
 
 FROM ubuntu:jammy
 
-COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
-COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
-COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+ENV TZ America/Chicago
+ENV DEBIAN_FRONTEND=noninteractive
 
 RUN    apt-get update           \
     && apt-get upgrade --yes    \
@@ -13,6 +11,15 @@ RUN    apt-get update           \
             curl                \
             sudo
 
+COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
+COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
+COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+
+RUN locale-gen en_US.UTF-8
+ENV LANG en_US.UTF-8
+ENV LANGUAGE en_US:en
+ENV LC_ALL en_US.UTF-8
+
 ARG USER=user
 ARG GROUP=${USER}
 ARG USER_ID=1000

From e45939acdb1e9591f861d1b62932b0d5b6199ba2 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 21:40:05 +0000
Subject: [PATCH 12/17] Dockerfile: add locales

---
 Dockerfile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Dockerfile b/Dockerfile
index 707f4a6..7ca277a 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -9,6 +9,7 @@ RUN    apt-get update           \
     && apt-get upgrade --yes    \
     && apt-get install --yes    \
             curl                \
+            locales             \
             sudo
 
 COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge

From 1dc3a336bd434ad0fd9268e20e2da49d49a4b5c2 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 21:41:53 +0000
Subject: [PATCH 13/17] Dockerfile: attempt with foundryup installer

---
 Dockerfile | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 7ca277a..5fb2099 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,5 +1,3 @@
-FROM ghcr.io/foundry-rs/foundry:nightly-aeba75e4799f1e11e3daba98d967b83e286b0c4a as FOUNDRY
-
 FROM ubuntu:jammy
 
 ENV TZ America/Chicago
@@ -12,10 +10,6 @@ RUN    apt-get update           \
             locales             \
             sudo
 
-COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
-COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
-COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
-
 RUN locale-gen en_US.UTF-8
 ENV LANG en_US.UTF-8
 ENV LANGUAGE en_US:en
@@ -32,3 +26,6 @@ RUN echo "${USER} ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
 
 USER user:user
 WORKDIR /home/user
+
+RUN    curl -L https://foundry.paradigm.xyz | bash \
+    && foundryup

From c9d56ec408d7e304dd6c2b5f2c981ab624dafacb Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Tue, 18 Apr 2023 21:46:46 +0000
Subject: [PATCH 14/17] Dockerfile: correct usernames

---
 Dockerfile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 5fb2099..1c95460 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -24,8 +24,8 @@ RUN    groupadd -g ${GROUP_ID} ${USER} \
 
 RUN echo "${USER} ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
 
-USER user:user
-WORKDIR /home/user
+USER ${USER}:${GROUP}
+WORKDIR /home/${USER}
 
 RUN    curl -L https://foundry.paradigm.xyz | bash \
     && foundryup

From 3839ae3b15a3c44a9231f23966a580b10275a012 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Wed, 19 Apr 2023 00:11:27 +0000
Subject: [PATCH 15/17] .github/test-pr, Dockerfile: install Foundry/KEVM in
 workflow

---
 .github/workflows/test-pr.yml | 6 ++++++
 Dockerfile                    | 3 ---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 5c1a573..bc64063 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -23,6 +23,8 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           tag: foundry-demo-ci-forge-${{ github.sha }}
+      - name: 'Install Foundry'
+        run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'curl -L https://foundry.paradigm.xyz | bash && foundryup'
       - name: 'Forge build'
         run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'Forge test'
@@ -47,6 +49,10 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           tag: foundry-demo-ci-kevm-${{ github.sha }}
+      - name: 'Install Foundry'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'curl -L https://foundry.paradigm.xyz | bash && foundryup'
+      - name: 'Install KEVM'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'curl -L https://kframework.org/install | bash && kup install kevm'
       - name: 'Forge build'
         run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'KEVM kompile'
diff --git a/Dockerfile b/Dockerfile
index 1c95460..e0104a7 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -26,6 +26,3 @@ RUN echo "${USER} ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
 
 USER ${USER}:${GROUP}
 WORKDIR /home/${USER}
-
-RUN    curl -L https://foundry.paradigm.xyz | bash \
-    && foundryup

From 300606c07623f093430a09342c49631e735288d7 Mon Sep 17 00:00:00 2001
From: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Date: Wed, 19 Apr 2023 01:04:04 +0000
Subject: [PATCH 16/17] .github, Dockerfile: install foundry in dockerfile
 again

---
 .github/workflows/test-pr.yml |  4 ----
 Dockerfile                    | 17 +++++++++++------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index bc64063..ca7cb53 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -23,8 +23,6 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           tag: foundry-demo-ci-forge-${{ github.sha }}
-      - name: 'Install Foundry'
-        run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'curl -L https://foundry.paradigm.xyz | bash && foundryup'
       - name: 'Forge build'
         run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'Forge test'
@@ -49,8 +47,6 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           tag: foundry-demo-ci-kevm-${{ github.sha }}
-      - name: 'Install Foundry'
-        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'curl -L https://foundry.paradigm.xyz | bash && foundryup'
       - name: 'Install KEVM'
         run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'curl -L https://kframework.org/install | bash && kup install kevm'
       - name: 'Forge build'
diff --git a/Dockerfile b/Dockerfile
index e0104a7..52bbaff 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,20 +1,25 @@
+FROM ghcr.io/foundry-rs/foundry:nightly-aeba75e4799f1e11e3daba98d967b83e286b0c4a as FOUNDRY
+
 FROM ubuntu:jammy
 
 ENV TZ America/Chicago
+RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
 ENV DEBIAN_FRONTEND=noninteractive
 
+COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
+COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
+COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+
 RUN    apt-get update           \
     && apt-get upgrade --yes    \
     && apt-get install --yes    \
+            build-essential     \
             curl                \
-            locales             \
+            git                 \
+            python3             \
+            python3-pip         \
             sudo
 
-RUN locale-gen en_US.UTF-8
-ENV LANG en_US.UTF-8
-ENV LANGUAGE en_US:en
-ENV LC_ALL en_US.UTF-8
-
 ARG USER=user
 ARG GROUP=${USER}
 ARG USER_ID=1000

From 2442b087bfe07b9b3ddfc29f910f00e5bbb19972 Mon Sep 17 00:00:00 2001
From: Andrei <andrei.vacaru@runtimeverification.com>
Date: Tue, 25 Jul 2023 15:14:20 +0300
Subject: [PATCH 17/17] run erc20 with booster on ci

---
 .github/workflows/test-pr.yml | 35 ++++-------------------------------
 erc20.sh                      |  2 +-
 2 files changed, 5 insertions(+), 32 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index ca7cb53..7889a2c 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -8,33 +8,8 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-
-  test-forge:
-    name: 'Test with Foundry'
-    runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 25
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
-          fetch-depth: 0
-      - name: 'Set up Docker'
-        uses: ./.github/actions/with-docker
-        with:
-          tag: foundry-demo-ci-forge-${{ github.sha }}
-      - name: 'Forge build'
-        run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge build'
-      - name: 'Forge test'
-        run: docker exec foundry-demo-ci-forge-${GITHUB_SHA} /bin/bash -c 'forge test -vvv'
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 foundry-demo-ci-forge-${GITHUB_SHA}
-
-  test-prove:
-    name: 'Verify with KEVM'
-    needs: test-forge
+  run-erc20:
+    name: 'Run ERC20 tests with KEVM Booster Integration'
     runs-on: [self-hosted, linux, normal]
     timeout-minutes: 90
     steps:
@@ -49,12 +24,10 @@ jobs:
           tag: foundry-demo-ci-kevm-${{ github.sha }}
       - name: 'Install KEVM'
         run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'curl -L https://kframework.org/install | bash && kup install kevm'
-      - name: 'Forge build'
-        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'forge build'
       - name: 'KEVM kompile'
-        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-kompile --verbose --with-llvm-library'
       - name: 'KEVM prove'
-        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'kevm foundry-prove --verbose -j8'
+        run: docker exec foundry-demo-ci-kevm-${GITHUB_SHA} /bin/bash -c 'cat erc20.sh | bash'
       - name: 'Tear down Docker'
         if: always()
         run: |
diff --git a/erc20.sh b/erc20.sh
index 5f00c02..f463e4f 100755
--- a/erc20.sh
+++ b/erc20.sh
@@ -5,7 +5,7 @@ set -euxo pipefail
 #### Get only the ERC20 tests in 'tests-to-run' using jq
 # jq '.ast.nodes[] | .name + "." + ( .nodes[].name | select(. |startswith("test")))' -r out/*.t.sol/*json | sort -u | grep -v -F -f exclude > tests-to-run
 
-time kevm foundry-kompile --with-llvm-library
+#time kevm foundry-kompile --with-llvm-library
 
 for TEST in $(cat tests-to-run); do
   echo "++++++++++++++++++++++++ $TEST +++++++++++++++++++++++++"