Merge branch 'master' into add-bytes-lookup-lemmas

Author: palinatolmach

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

@@ -15,7 +15,7 @@ inputs:
     required: false
     type: string
     default: './'
-  os: 
+  os:
     description: 'OS to setup Docker for.'
     required: false
     type: string
@@ -55,6 +55,7 @@ runs:
       GROUP=${USER}
       Z3_VERSION=$(cat deps/z3)
       K_VERSION=$(cat deps/k_release)
+      UV_VERSION=$(cat deps/uv_release)
       USER_ID=1000
       GROUP_ID=${USER_ID}
 
@@ -67,7 +68,8 @@ runs:
         --build-arg BASE_DISTRO=${BASE_DISTRO}   \
         --build-arg K_VERSION=${K_VERSION}       \
         --build-arg Z3_VERSION=${Z3_VERSION}     \
-        --build-arg LLVM_VERSION=${LLVM_VERSION}
+        --build-arg LLVM_VERSION=${LLVM_VERSION} \
+        --build-arg UV_VERSION=${UV_VERSION}
 
       docker run                          \
         --name ${CONTAINER_NAME}          \

.github/workflows/Dockerfile

@@ -43,5 +43,6 @@ WORKDIR /home/${USER}/workspace
 
 ENV PATH=/home/${USER}/.local/bin:${PATH}
 
-RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.8.3 \
-    && poetry --version
+ARG UV_VERSION
+RUN    curl -LsSf https://astral.sh/uv/${UV_VERSION}/install.sh | sh \
+    && uv --version

.github/workflows/release.yml

@@ -36,7 +36,6 @@ jobs:
       matrix:
         include:
           - runner: normal
-          - runner: macos-13
           - runner: ARM64
     runs-on: ${{ matrix.runner }}
     needs: draft-release
@@ -46,23 +45,6 @@ jobs:
         with:
           ref: ${{ github.event.push.head.sha }}
           fetch-depth: 0
-      - name: 'Upgrade bash'
-        if: ${{ contains(matrix.os, 'macos') }}
-        run: brew install bash
-      - name: 'Install Nix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/install-nix-action@v19
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/cachix-action@v12
-        with:
-          name: k-framework
-          signingKey: ${{ secrets.CACHIX_SIGNING_KEY }}
-          skipPush: true
       - name: 'Build KEVM'
         run: |
           GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs

.github/workflows/test-pr.yml

@@ -12,14 +12,20 @@ jobs:
     name: 'Code Quality Checks'
     runs-on: ubuntu-latest
     steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
       - name: 'Setup Python 3.10'
         uses: actions/setup-python@v5
         with:
           python-version: '3.10'
-      - name: 'Check out code'
-        uses: actions/checkout@v4
-      - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v9
+      - name: 'Get uv release'
+        id: uv_release
+        run: |
+          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
+      - name: 'Install uv'
+        uses: astral-sh/setup-uv@v6
+        with:
+          version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Run code quality checks'
         run: make -C kevm-pyk check
       - name: 'Run pyupgrade'
@@ -32,8 +38,14 @@ jobs:
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4
-      - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v9
+      - name: 'Get uv release'
+        id: uv_release
+        run: |
+          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
+      - name: 'Install uv'
+        uses: astral-sh/setup-uv@v6
+        with:
+          version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Run unit tests'
         run: make -C kevm-pyk cov-unit
 
@@ -44,8 +56,14 @@ jobs:
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v4
-      - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v9
+      - name: 'Get uv release'
+        id: uv_release
+        run: |
+          echo uv_version=$(cat deps/uv_release) >> "${GITHUB_OUTPUT}"
+      - name: 'Install uv'
+        uses: astral-sh/setup-uv@v6
+        with:
+          version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Run profiling'
         run: |
           make -C kevm-pyk profile
@@ -64,14 +82,14 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kevm-ci-concrete-${{ github.sha }}
-      - 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 kdist --verbose build -j`nproc` evm-semantics.haskell evm-semantics.kllvm evm-semantics.kllvm-runtime'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 uv --project kevm-pyk run -- kdist --verbose build -j`nproc` evm-semantics.haskell evm-semantics.kllvm evm-semantics.kllvm-runtime'
       - name: 'Test integration'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
       - name: 'Test conformance'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-conformance'
+      - name: 'Test execution-spec-tests'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-fixtures'
       - name: 'Test llvm krun'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-interactive'
       - name: 'Tear down Docker'
@@ -108,10 +126,10 @@ jobs:
             timeout: 45
             parallel: 1
           - name: 'Summarization'
-            test-suite: 'test-summarize'
+            test-suite: 'test-prove-summaries'
             test-args:
-            timeout: 30
-            parallel: 6
+            timeout: 45
+            parallel: 4
           - name: 'DSS'
             test-suite: 'test-prove-dss'
             test-args:
@@ -129,10 +147,8 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
-      - 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 kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell evm-semantics.summary'
+        run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 uv --project kevm-pyk run -- kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell evm-semantics.haskell-summary'
       - name: 'Run proofs'
         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=${{ matrix.parallel }}"
       - name: 'Tear down Docker'
@@ -147,7 +163,6 @@ jobs:
       matrix:
         include:
           - runner: normal
-          - runner: macos-13
           - runner: ARM64
     needs: kevm-pyk-code-quality-checks
     runs-on: ${{ matrix.runner }}
@@ -162,20 +177,6 @@ jobs:
         run: |
           set -eux
           git submodule update --init --recursive -- kevm-pyk/src/kevm_pyk/kproj/plugin
-      - name: 'Install Nix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/install-nix-action@v25
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.19.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-            substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/cachix-action@v14
-        with:
-          name: k-framework
       - name: 'Build KEVM'
         run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs
       - name: 'Test KEVM'

.github/workflows/update-version.yml

@@ -4,6 +4,9 @@ on:
     branches:
       - '_update-deps/runtimeverification/blockchain-k-plugin'
       - '_update-deps/runtimeverification/k'
+      - '_update-deps/runtimeverification/rv-nix-tools'
+      - '_update-deps-cron/uv2nix'
+      - '_update-deps-cron/pyproject-build-systems'
   workflow_dispatch:
 # Stop in progress workflows on the same branch and same workflow to use latest committed code
 concurrency:
@@ -25,23 +28,34 @@ jobs:
         run: |
           git config user.name devops
           git config user.email devops@runtimeverification.com
-      - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v9
+      - name: 'Get uv release'
+        id: uv_release
+        run: |
+          UV2NIX_VERSION=$(cat deps/uv2nix)
+          UV_VERSION=$(curl -s https://raw.githubusercontent.com/pyproject-nix/uv2nix/$(cat deps/uv2nix)/pkgs/uv-bin/srcs.json | jq -r .version)
+          [[ "${UV_VERSION}" =~ ^[0-9]+\.[0-9]+\.[0-9]+$ ]]
+          echo ${UV_VERSION} > deps/uv_release
+          git add deps/uv_release && git commit -m "Sync uv version: uv ${UV_VERSION}" || true
+          echo uv_version=${UV_VERSION} >> "${GITHUB_OUTPUT}"
+      - name: 'Install uv'
+        uses: astral-sh/setup-uv@v6
+        with:
+          version: ${{ steps.uv_release.outputs.uv_version }}
       - name: 'Update pyk release tag'
         run: |
           K_VERSION=$(cat deps/k_release)
-          sed -i 's!kframework = "[0-9\.]*"!kframework = "'${K_VERSION}'"!' kevm-pyk/pyproject.toml
-          poetry -C kevm-pyk update
-          git add kevm-pyk/ && git commit -m "kevm-pyk/: sync poetry files pyk version ${K_VERSION}" || true
+          sed -i 's!    "kframework==[0-9\.]*,"!    "kframework=='${K_VERSION}'",!' kevm-pyk/pyproject.toml
+          uv --project kevm-pyk lock --upgrade
+          git add kevm-pyk/ && git commit -m "kevm-pyk/: sync uv files pyk version ${K_VERSION}" || true
       - name: 'Update plugin release file'
         run: |
           BKP_VERSION=$(git -C kevm-pyk/src/kevm_pyk/kproj/plugin rev-parse HEAD)
           echo ${BKP_VERSION} > deps/blockchain-k-plugin_release
           git add deps/blockchain-k-plugin_release && git commit -m "deps/blockchain-k-plugin_release: sync release file version ${BKP_VERSION}" || true
       - name: 'Install Nix/Cachix'
-        uses: cachix/install-nix-action@v19
+        uses: cachix/install-nix-action@v31.5.1
         with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
+          install_url: https://releases.nixos.org/nix/nix-2.30.1/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: cachix/cachix-action@v12
@@ -52,8 +66,14 @@ jobs:
         run: |
           K_VERSION=v$(cat deps/k_release)
           BKP_VERSION=$(cat deps/blockchain-k-plugin_release)
+          UV2NIX_VERSION=$(cat deps/uv2nix)
+          PYPROJECT_BUILD_SYSTEMS_VERSION=$(cat deps/pyproject-build-systems)
+          RV_NIX_TOOLS_VERSION=$(cat deps/rv-nix-tools)
           sed -i 's!    k-framework.url = "github:runtimeverification/k/[v0-9\.]*"!    k-framework.url = "github:runtimeverification/k/'"${K_VERSION}"'"!' flake.nix
           sed -i 's!        "github:runtimeverification/blockchain-k-plugin/[0-9a-f]*"!        "github:runtimeverification/blockchain-k-plugin/'"${BKP_VERSION}"'"!' flake.nix
+          sed -i 's!    uv2nix.url = "github:pyproject-nix/uv2nix/[a-z0-9\.]*"!    uv2nix.url = "github:pyproject-nix/uv2nix/'"${UV2NIX_VERSION}"'"!' flake.nix
+          sed -i 's!    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/[a-z0-9\.]*"!    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/'"${PYPROJECT_BUILD_SYSTEMS_VERSION}"'"!' flake.nix
+          sed -i 's!    rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/[a-z0-9\.]*"!    rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/'"${RV_NIX_TOOLS_VERSION}"'"!' flake.nix
           nix run .#update-from-submodules
           nix flake update
           git add flake.nix flake.lock && git commit -m 'flake.{nix,lock}: update Nix derivations' || true

.gitignore

@@ -17,6 +17,7 @@
 /tests/specs/opcodes/evm-optimizations-spec.md
 /tests/specs/**/*.prove.out
 /tests/specs/**/*.sol.json
+/tests/execution-spec-tests/fixtures
 /tests/vm/*.out
 .DS_Store
 .idea/