runtimeverification · tothtamas28 · Jul 17, 2025 · Jul 17, 2025 · Jul 17, 2025 · Jul 17, 2025
diff --git a/.github/actions/with-docker/action.yml b/.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}          \

diff --git a/.github/workflows/Dockerfile b/.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
diff --git a/.github/workflows/test-pr.yml b/.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,10 +82,8 @@ 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'
@@ -131,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.haskell-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'

diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml
@@ -5,6 +5,8 @@ on:
       - '_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:
@@ -26,23 +28,34 @@ jobs:
         run: |
           git config user.name devops
           git config user.email [email protected]
-      - 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
@@ -53,9 +66,13 @@ 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

diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-all: poetry
+default: kevm-pyk
 
 
 # Building
@@ -11,21 +11,11 @@ else
 endif
 
 KEVM_PYK_DIR := ./kevm-pyk
-POETRY       := poetry -C $(KEVM_PYK_DIR)
-POETRY_RUN   := $(POETRY) run --
+UV           := uv --project $(KEVM_PYK_DIR)
+UV_RUN       := $(UV) run --
 
-
-.PHONY: poetry-env download-json-fixtures
-poetry-env:
-	$(POETRY) env use --no-cache $(PYTHON_BIN)
-
-poetry: poetry-env
-	$(POETRY) install
-
-shell: poetry
-	$(POETRY) shell
-
-kevm-pyk: poetry-env
+.PHONY: kevm-pyk
+kevm-pyk:
 	$(MAKE) -C $(KEVM_PYK_DIR)
 
 
@@ -37,10 +27,12 @@ test: test-integration test-conformance test-prove test-interactive
 
 # Conformance Tests
 
-test-conformance: poetry
+.PHONY: test-conformance
+test-conformance:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_conformance.py"
 
-conformance-failing-list: poetry
+.PHONY: conformance-failing-list
+conformance-failing-list:
 	cat /dev/null > tests/failing.llvm
 	- $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_conformance.py --save-failing --maxfail=10000"
 	LC_ALL=en_US.UTF-8 sort -f -d -o tests/failing.llvm tests/failing.llvm
@@ -51,14 +43,15 @@ conformance-failing-list: poetry
 		sed -i '1{/^[[:space:]]*$$/d;}' tests/failing.llvm ;\
 	fi
 
+.PHONY: download-json-fixtures
 download-json-fixtures:
 	rm -rf tests/execution-spec-tests/fixtures
 	cd tests/execution-spec-tests && bash get_execution_spec_tests.sh
 
-test-fixtures: poetry download-json-fixtures
+test-fixtures: download-json-fixtures
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_execution_spec_tests.py"
 
-fixtures-failing-list: poetry download-json-fixtures
+fixtures-failing-list: download-json-fixtures
 	cat /dev/null > tests/execution-spec-tests/failing.llvm
 	- $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_execution_spec_tests.py --save-failing --maxfail=10000"
 	LC_ALL=en_US.UTF-8 sort -f -d -o tests/execution-spec-tests/failing.llvm tests/execution-spec-tests/failing.llvm
@@ -69,49 +62,61 @@ fixtures-failing-list: poetry download-json-fixtures
 		sed -i '1{/^[[:space:]]*$$/d;}' tests/execution-spec-tests/failing.llvm ;\
 	fi
 
-test-vm: poetry
+.PHONY: test-vm
+test-vm:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_vm"
 
-test-rest-vm: poetry
+.PHONY: test-rest-vm
+test-rest-vm:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_rest_vm"
 
-test-bchain: poetry
+.PHONY: test-bchain
+test-bchain:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_bchain"
 
-test-rest-bchain: poetry
+.PHONY: test-rest-bchain
+test-rest-bchain:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_rest_bchain"
 
 
 # Proof Tests
 
 test-prove: test-prove-rules test-prove-functional test-prove-optimizations test-prove-dss
 
-test-prove-rules: poetry
+.PHONY: test-prove-rules
+test-prove-rules:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_rules"
 
-test-prove-functional: poetry
+.PHONY: test-prove-functional
+test-prove-functional:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_functional"
 
-test-prove-optimizations: poetry
+.PHONY: test-prove-optimizations
+test-prove-optimizations:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_optimizations"
 
-test-prove-summaries: poetry
+.PHONY: test-prove-summaries
+test-prove-summaries:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_summaries"
 
-test-prove-dss: poetry
+.PHONY: test-prove-dss
+test-prove-dss:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_dss"
 
 
 # Integration Tests
 
-test-integration: poetry
-	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+='-k "(test_kast.py or test_run.py or test_solc_to_k.py)"'
+.PHONY: test-integration
+test-integration:
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+='-k "(test_kast.py or test_run.py)"'
 
-profile: poetry
+.PHONY: profile
+profile:
 	$(MAKE) -C kevm-pyk/ profile
 	find /tmp/pytest-of-$$(whoami)/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
 
-test-summarize: poetry
+.PHONY: test-summarize
+test-summarize:
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+='-k "test_summarize"'
 
 
@@ -126,31 +131,13 @@ KPROVE_EXT    = k
 KEVM_OPTS    ?=
 KPROVE_OPTS  ?=
 
-
-tests/specs/examples/%-bin-runtime.k: KEVM_OPTS += --verbose
-
-tests/specs/examples/erc20-spec/haskell/timestamp: tests/specs/examples/erc20-bin-runtime.k
-tests/specs/examples/erc20-bin-runtime.k: tests/specs/examples/ERC20.sol $(KEVM_LIB)/$(haskell_kompiled) poetry
-	$(KEVM) solc-to-k $< ERC20 $(KEVM_OPTS) --verbose --definition $(KEVM_LIB)/$(haskell_dir) --main-module ERC20-VERIFICATION > $@
-
-tests/specs/examples/erc721-spec/haskell/timestamp: tests/specs/examples/erc721-bin-runtime.k
-tests/specs/examples/erc721-bin-runtime.k: tests/specs/examples/ERC721.sol $(KEVM_LIB)/$(haskell_kompiled) poetry
-	$(KEVM) solc-to-k $< ERC721 $(KEVM_OPTS) --verbose --definition $(KEVM_LIB)/$(haskell_dir) --main-module ERC721-VERIFICATION > $@
-
-tests/specs/examples/storage-spec/haskell/timestamp: tests/specs/examples/storage-bin-runtime.k
-tests/specs/examples/storage-bin-runtime.k: tests/specs/examples/Storage.sol $(KEVM_LIB)/$(haskell_kompiled) poetry
-	$(KEVM) solc-to-k $< Storage $(KEVM_OPTS) --verbose --definition $(KEVM_LIB)/$(haskell_dir) --main-module STORAGE-VERIFICATION > $@
-
-tests/specs/examples/empty-bin-runtime.k: tests/specs/examples/Empty.sol $(KEVM_LIB)/$(haskell_kompiled) poetry
-	$(KEVM) solc-to-k $< Empty $(KEVM_OPTS) --verbose --definition $(KEVM_LIB)/$(haskell_dir) --main-module EMPTY-VERIFICATION > $@
-
 .SECONDEXPANSION:
 tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)/timestamp
-	$(POETRY_RUN) kevm-pyk prove $< $(KEVM_OPTS) $(KPROVE_OPTS) \
+	$(UV_RUN) kevm-pyk prove $< $(KEVM_OPTS) $(KPROVE_OPTS) \
 		--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-spec                                                                         \
+	$(UV_RUN) kevm-pyk kompile-spec                                                                             \
 		$<                                                                                                      \
 		--target $(word 3, $(subst /, , $*))                                                                    \
 		--output-definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \
@@ -181,9 +168,9 @@ tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_MODE
 tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_SCHEDULE = DEFAULT
 
 tests/%.run-interactive: tests/%
-	$(POETRY_RUN) kevm-pyk run $< $(KEVM_OPTS) $(KRUN_OPTS) --target $(TEST_CONCRETE_BACKEND)                          \
-	    --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID)                                      \
-	    > tests/$*.$(TEST_CONCRETE_BACKEND)-out                                                                        \
+	$(UV_RUN) kevm-pyk run $< $(KEVM_OPTS) $(KRUN_OPTS) --target $(TEST_CONCRETE_BACKEND) \
+	    --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID)         \
+	    > tests/$*.$(TEST_CONCRETE_BACKEND)-out                                           \
 	    || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
 	$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out