diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml new file mode 100644 index 0000000..c394ff1 --- /dev/null +++ b/.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} \ diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile new file mode 100644 index 0000000..c829b11 --- /dev/null +++ b/.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) diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml new file mode 100644 index 0000000..7889a2c --- /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: + 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} 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 diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..52bbaff --- /dev/null +++ b/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} 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 +++++++++++++++++++++++++"