Updates to the conformance test suite

.github/workflows/Dockerfile

@@ -44,5 +44,5 @@ WORKDIR /home/${USER}/workspace
 
 ENV PATH=/home/${USER}/.local/bin:${PATH}
 
-RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.6.1 \
+RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.8.3 \
     && poetry --version

.github/workflows/master-push.yml

@@ -20,7 +20,7 @@ jobs:
     runs-on: ${{ matrix.runner }}
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           ref: ${{ github.event.push.head.sha }}
           fetch-depth: 0
@@ -59,7 +59,7 @@ jobs:
     needs: nix-cache
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           ref: ${{ github.event.push.head.sha }}
           fetch-depth: 0
@@ -88,7 +88,7 @@ jobs:
     needs: make-release
     steps:
       - name: 'Check out gh-pages'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
           submodules: true

.github/workflows/test-pr.yml

@@ -14,7 +14,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           # fetch-depth 0 means deep clone the repo
@@ -40,11 +40,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Run code quality checks'
         run: make -C kevm-pyk check
       - name: 'Run pyupgrade'
@@ -56,11 +54,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Run unit tests'
         run: make -C kevm-pyk cov-unit
 
@@ -70,11 +66,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Run profiling'
         run: |
           make -C kevm-pyk profile
@@ -86,7 +80,7 @@ jobs:
     timeout-minutes: 45
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
       - name: 'Set up Docker'
@@ -128,9 +122,11 @@ jobs:
     timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
+      - name: 'Check out select submodules'
+        run: |
+          set -eux
+          git submodule update --init --recursive -- kevm-pyk/src/kevm_pyk/kproj/plugin
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
@@ -160,10 +156,14 @@ jobs:
     timeout-minutes: 60
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           # Check out pull request HEAD instead of merge commit.
           ref: ${{ github.event.pull_request.head.sha }}
+      - name: 'Check out select submodules'
+        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

.github/workflows/update-version.yml

@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
@@ -27,7 +27,7 @@ jobs:
           git config user.name devops
           git config user.email [email protected]
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Update pyk release tag'
         run: |
           K_VERSION=v$(cat deps/k_release)

Makefile

@@ -135,8 +135,8 @@ KRUN_OPTS     ?=
 KEEP_OUTPUTS  := false
 CHECK         := git --no-pager diff --no-index --ignore-all-space -R
 
-tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_MODE     = VMTESTS
-tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_SCHEDULE = DEFAULT
+tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_MODE     = VMTESTS
+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)                          \
@@ -145,8 +145,7 @@ tests/%.run-interactive: tests/%
 	    || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
 	$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 
-interactive_tests = tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json      \
-                    tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmIOandFlowOperations/pop1.json \
+interactive_tests = tests/interactive/add.json    \
                     tests/interactive/sumTo10.evm
 
 .PHONY: test-interactive

README.md

@@ -284,10 +284,10 @@ For Developers
 If built from the source, the `kevm-pyk` executable will be installed in a virtual environemtn handled by Poetry.
 You can call `kevm-pyk --help` to get a quick summary of how to use the script.
 
-Run the file `tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json`:
+Run the file `tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json`:
 
 ```sh
-poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS
+poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS
 ```
 
 To enable the debug symbols for the llvm backend, build using this command:

flake.nix

@@ -15,20 +15,10 @@
       inputs.flake-utils.follows = "k-framework/flake-utils";
       inputs.nixpkgs.follows = "k-framework/nixpkgs";
     };
-    ethereum-tests = {
-      url = "github:ethereum/tests/6401889dec4eee58e808fd178fb2c7f628a3e039";
-      flake = false;
-    };
-    ethereum-legacytests = {
-      url =
-        "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7";
-      flake = false;
-    };
     haskell-backend.follows = "k-framework/haskell-backend";
   };
   outputs = { self, k-framework, haskell-backend, nixpkgs, flake-utils
-    , blockchain-k-plugin, ethereum-tests, ethereum-legacytests, rv-utils, pyk
-    , ... }@inputs:
+    , blockchain-k-plugin, rv-utils, pyk, ... }@inputs:
     let
       nixLibs = pkgs:
         with pkgs;
@@ -127,9 +117,6 @@
             buildInputs = [ final.kevm prev.which prev.git ];
 
             buildPhase = ''
-              mkdir -p tests/ethereum-tests/LegacyTests
-              cp -r ${ethereum-tests}/* tests/ethereum-tests/
-              cp -r ${ethereum-legacytests}/* tests/ethereum-tests/LegacyTests/
               chmod -R u+w tests
               APPLE_SILICON=${
                 if prev.stdenv.isAarch64 && prev.stdenv.isDarwin then
@@ -237,16 +224,12 @@
           };
 
           check-submodules = rv-utils.lib.check-submodules pkgs {
-            inherit k-framework blockchain-k-plugin ethereum-tests
-              ethereum-legacytests;
+            inherit k-framework blockchain-k-plugin;
           };
 
           update-from-submodules =
             rv-utils.lib.update-from-submodules pkgs ./flake.lock {
               blockchain-k-plugin.submodule = "deps/plugin";
-              ethereum-tests.submodule = "tests/ethereum-tests";
-              ethereum-legacytests.submodule =
-                "tests/ethereum-tests/LegacyTests";
             };
         };
       }) // {

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.569"
+version = "1.0.570"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.569'
+VERSION: Final = '1.0.570'

kevm-pyk/src/tests/integration/test_conformance.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 import json
+import logging
 import sys
 from typing import TYPE_CHECKING
 
@@ -21,22 +22,24 @@
     from pyk.kore.syntax import Pattern
 
 
+_LOGGER: Final = logging.getLogger(__name__)
+_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+
+
 sys.setrecursionlimit(10**8)
 
 TEST_DIR: Final = REPO_ROOT / 'tests/ethereum-tests'
 GOLDEN: Final = (REPO_ROOT / 'tests/templates/output-success-llvm.json').read_text().rstrip()
 
 
 def _test(gst_file: Path, schedule: str, mode: str, chainid: int, usegas: bool) -> None:
-    # Given
     with gst_file.open() as f:
         gst_data = json.load(f)
 
-    # When
-    res = interpret(gst_data, schedule, mode, chainid, usegas, check=False)
-
-    # Then
-    _assert_exit_code_zero(res)
+    for test_name, test in gst_data.items():
+        _LOGGER.info(f'Running test: {gst_file} - {test_name}')
+        res = interpret({test_name: test}, schedule, mode, chainid, usegas, check=False)
+        _assert_exit_code_zero(res)
 
 
 def _assert_exit_code_zero(pattern: Pattern) -> None:
@@ -65,7 +68,7 @@ def read_test_list(path: Path) -> list[Path]:
 
 SKIPPED_TESTS: Final = _skipped_tests()
 
-VM_TEST_DIR: Final = TEST_DIR / 'LegacyTests/Constantinople/VMTests'
+VM_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests/VMTests'
 ALL_VM_TESTS: Final = tuple(VM_TEST_DIR.glob('*/*.json'))
 VM_TESTS: Final = tuple(test_file for test_file in ALL_VM_TESTS if test_file not in SKIPPED_TESTS)
 REST_VM_TESTS: Final = tuple(test_file for test_file in ALL_VM_TESTS if test_file in SKIPPED_TESTS)
@@ -90,15 +93,14 @@ def test_rest_vm(test_file: Path) -> None:
     _test(test_file, 'DEFAULT', 'VMTESTS', 1, True)
 
 
-BCHAIN_NEW_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests'
-BCHAIN_NEW_TESTS: Final = tuple(BCHAIN_NEW_TEST_DIR.glob('**/*.json'))
-
-BCHAIN_LEGACY_TEST_DIR: Final = TEST_DIR / 'LegacyTests/Constantinople/BlockchainTests/GeneralStateTests'
-BCHAIN_LEGACY_TESTS: Final = tuple(BCHAIN_LEGACY_TEST_DIR.glob('*/*.json'))
-
-ALL_BCHAIN_TESTS: Final = BCHAIN_NEW_TESTS + BCHAIN_LEGACY_TESTS
-BCHAIN_TESTS: Final = tuple(test_file for test_file in ALL_BCHAIN_TESTS if test_file not in SKIPPED_TESTS)
-REST_BCHAIN_TESTS: Final = tuple(test_file for test_file in ALL_BCHAIN_TESTS if test_file in SKIPPED_TESTS)
+BCHAIN_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests'
+ALL_BCHAIN_TESTS: Final = tuple(BCHAIN_TEST_DIR.glob('**/*.json'))
+BCHAIN_TESTS: Final = tuple(
+    test_file for test_file in ALL_BCHAIN_TESTS if test_file not in (list(SKIPPED_TESTS) + list(ALL_VM_TESTS))
+)
+REST_BCHAIN_TESTS: Final = tuple(
+    test_file for test_file in ALL_BCHAIN_TESTS if test_file in SKIPPED_TESTS and test_file not in ALL_VM_TESTS
+)
 
 
 @pytest.mark.parametrize(

kevm-pyk/src/tests/profiling/test_gst_to_kore.py

@@ -9,7 +9,7 @@
     from pyk.testing import Profiler
 
 
-GST_FILE = REPO_ROOT / 'tests/ethereum-tests/BlockchainTests/GeneralStateTests/stEIP1559/intrinsic.json'
+GST_FILE = REPO_ROOT / 'tests/interactive/intrinsic.json'
 
 
 def test_gst_to_kore(profile: Profiler) -> None:

kevm-pyk/src/tests/unit/test_gst_to_kore.py

@@ -16,8 +16,8 @@
 
 TEST_DATA: Final = (
     (
-        'tests/ethereum-tests/GeneralStateTests/VMTests/vmLogTest/log3.json',
-        'tests/interactive/vmLogTest/log3.gst-to-kore.expected',
+        'tests/interactive/log3.json',
+        'tests/interactive/log3.gst-to-kore.expected',
     ),
     (
         'tests/interactive/log3_MaxTopic_d0g0v0.json',