Run Foundry prover on CI

.github/actions/with-docker/action.yml

@@ -0,0 +1,36 @@
+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
+
+      USER=$(id -un)
+      USER_ID=$(id -u)
+      GROUP=$(id -gn)
+      GROUP_ID=$(id -g)
+
+      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}              \
+        --rm                            \
+        --interactive                   \
+        --tty                           \
+        --detach                        \
+        --user ${USER}:${GROUP}         \
+        -v "$(pwd):/opt/workspace"      \
+        --workdir /opt/workspace        \
+        runtimeverification/${TAG_NAME} \

.github/workflows/Dockerfile

@@ -0,0 +1,46 @@
+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
+
+RUN bash <(curl https://kframework.org/install)

.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:
+  run-erc20:
+    name: 'Run ERC20 tests with KEVM Booster Integration'
+    runs-on: [self-hosted, linux, normal]
+    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: '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: 'KEVM kompile'
+        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 'cat erc20.sh | bash'
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 foundry-demo-ci-kevm-${GITHUB_SHA}

Dockerfile

@@ -0,0 +1,33 @@
+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                \
+            git                 \
+            python3             \
+            python3-pip         \
+            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}:${GROUP}
+WORKDIR /home/${USER}

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 +++++++++++++++++++++++++"