Merge branch 'master' into raoul/is-valid-jump-dest

Author: RaoulSchaffranek

.github/workflows/Dockerfile

@@ -3,26 +3,19 @@ ARG K_VERSION
 ARG BASE_DISTRO
 ARG LLVM_VERSION
 
-FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY
-
 ARG Z3_VERSION
 FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
 
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
-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
 
 ARG LLVM_VERSION
 
 RUN    apt-get update                  \
     && apt-get upgrade --yes           \
     && apt-get install --yes           \
-            cargo                      \
             clang-${LLVM_VERSION}      \
             cmake                      \
             curl                       \
@@ -48,11 +41,7 @@ USER ${USER}:${GROUP}
 RUN mkdir /home/${USER}/workspace
 WORKDIR /home/${USER}/workspace
 
-ENV PATH=/home/${USER}/.cargo/bin:/home/${USER}/.local/bin:/usr/local/bin/:${PATH}
+ENV PATH=/home/${USER}/.local/bin:${PATH}
 
-RUN    curl -sSL https://install.python-poetry.org | python3 - \
+RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.6.1 \
     && poetry --version
-
-RUN    cargo install svm-rs --version 0.3.0 --locked \
-    && svm install 0.8.13                            \
-    && solc --version

.github/workflows/test-pr.yml

@@ -11,7 +11,7 @@ jobs:
 
   version-bump:
     name: 'Version Bump'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, flyweight-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -36,12 +36,14 @@ jobs:
         run: git push origin HEAD:${GITHUB_HEAD_REF}
 
   kevm-pyk-code-quality-checks:
-    needs: version-bump
     name: 'Code Quality Checks'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, flyweight-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
+      - uses: actions/setup-python@v4
+        with:
+            python-version: "3.10"
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
       - name: 'Run code quality checks'
@@ -52,13 +54,16 @@ jobs:
   kevm-pyk-unit-tests:
     needs: kevm-pyk-code-quality-checks
     name: 'Unit Tests'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, normal-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
         with:
           submodules: true
           fetch-depth: 0
+      - uses: actions/setup-python@v4
+        with:
+            python-version: "3.10"
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
       - name: 'Run unit tests'
@@ -68,29 +73,22 @@ jobs:
   kevm-pyk-profile:
     needs: kevm-pyk-code-quality-checks
     name: 'Profiling'
-    runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 15
+    runs-on: [self-hosted, linux, normal-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
         with:
           submodules: recursive
           fetch-depth: 0
-      - name: 'Set up Docker'
-        uses: ./.github/actions/with-docker
+      - name: Setup Python
+        uses: actions/setup-python@v4
         with:
-          container-name: kevm-ci-profile-${{ github.sha }}
-      - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-profile-${{ github.sha }} /bin/bash -c 'make poetry'
-      - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-profile-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
+          python-version: '3.10'
+      - name: 'Install Poetry'
+        uses: Gr1N/setup-poetry@v8
       - name: 'Run profiling'
         run: |
-          docker exec -u github-user kevm-ci-profile-${{ github.sha }} /bin/bash -c 'make profile'
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kevm-ci-profile-${{ github.sha }}
+          make -C kevm-pyk profile
 
   test-concrete-execution:
     name: 'Build and Test KEVM concrete execution'
@@ -110,7 +108,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin llvm haskell'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.llvm evm-semantics.haskell'
       - name: 'Test integration'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
       - name: 'Test conformance'
@@ -125,7 +123,7 @@ jobs:
   test-prove:
     name: 'Build and Test KEVM proofs'
     needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, normal, fast]
+    runs-on: [self-hosted, linux, fast]
     strategy:
       fail-fast: false
       matrix:
@@ -135,10 +133,10 @@ jobs:
             timeout: 45
           - test-suite: 'test-prove-pyk'
             test-args:
-            timeout: 120
+            timeout: 180
           - test-suite: 'test-prove-pyk'
             test-args: '--use-booster'
-            timeout: 90
+            timeout: 150
     timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'
@@ -152,50 +150,14 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build distribution'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin haskell'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell'
       - name: 'Prove Haskell'
-        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=7"
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=4"
       - name: 'Tear down Docker'
         if: always()
         run: |
           docker stop --time=0 kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
 
-  test-prove-foundry:
-    name: 'Build and Test KEVM Foundry proofs'
-    needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, normal, fast]
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - test-suite: 'legacy'
-            test-args:
-            timeout: 180
-          - test-suite: 'booster'
-            test-args: '--use-booster'
-            timeout: 90
-    timeout-minutes: ${{ matrix.timeout }}
-    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:
-          container-name: kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }}
-      - name: 'Build kevm-pyk'
-        run: docker exec -u github-user kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
-      - name: 'Build targets'
-        run: docker exec -u github-user kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kevm-dist --verbose build -j`nproc` plugin foundry'
-      - name: 'Foundry Prove'
-        run: docker exec -u github-user kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make test-foundry-prove PYTEST_ARGS='-vv ${{ matrix.test-args }}'"
-      - name: 'Tear down Docker'
-        if: always()
-        run: |
-          docker stop --time=0 kevm-ci-foundry-${{ matrix.test-suite }}-${{ github.sha }}
-
   nix:
     name: 'Nix'
     strategy:

.github/workflows/update-foundry-prove.yml

@@ -10,19 +10,7 @@
 /package/src
 /pkg
 /tests/**/*.debug-log
-/tests/foundry/cache
-/tests/foundry/foundry.k
-/tests/foundry/foundry.k.check.stripped
-/tests/foundry/contracts.k.check.stripped
-/tests/foundry/foundry-list.check.stripped
-/tests/foundry/golden/*.out
-/tests/foundry/*.out
-/tests/foundry/out
-/tests/foundry/test/filecopy2.txt
-/tests/foundry/test/filecopy.txt
-/tests/foundry/test/fileline.txt
 /tests/**/*.rule-profile
-/tests/specs/**/*-bin-runtime.k
 /tests/specs/foundry/*.out
 /tests/specs/**/haskell
 /tests/specs/**/java

.gitignore

@@ -14,6 +14,3 @@
 [submodule "web/k-web-theme"]
 	path = web/k-web-theme
 	url = https://github.com/runtimeverification/k-web-theme
-[submodule "tests/foundry/lib/forge-std"]
-	path = tests/foundry/lib/forge-std
-	url = https://github.com/foundry-rs/forge-std

.gitmodules

@@ -30,11 +30,6 @@ kevm-pyk: poetry-env
 test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-interactive
 
 
-# Foundry Tests
-
-test-foundry-prove: poetry
-	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_foundry_prove.py"
-
 # Conformance Tests
 
 test-conformance: poetry
@@ -64,7 +59,7 @@ test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_kprove_prove"
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
-tests/specs/opcodes/evm-optimizations-spec.md:
+tests/specs/opcodes/evm-optimizations-spec.md: kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
 	cat kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
 
 
@@ -113,7 +108,7 @@ tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$
 		--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
 
 tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT)
-	$(POETRY_RUN) kevm-pyk kompile                                                                             \
+	$(POETRY_RUN) kevm-pyk kompile-spec                                                                         \
 		$<                                                                                                      \
 		--target $(word 3, $(subst /, , $*))                                                                    \
 		--output-definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \