Deleted PR

.github/workflows/test-pr.yml

@@ -3,11 +3,15 @@ on:
   pull_request:
     branches:
       - 'master'
+  push:
+    branches:
+      - 'master-update'
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
+
   kevm-pyk-code-quality-checks:
     name: 'Code Quality Checks'
     runs-on: ubuntu-latest
@@ -63,7 +67,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 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 poetry -C kevm-pyk run kdist --verbose build -j`nproc` 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'
@@ -74,100 +78,3 @@ jobs:
         if: always()
         run: |
           docker stop --time=0 kevm-ci-concrete-${{ github.sha }}
-
-  test-prove:
-    name: 'Proofs: ${{ matrix.name }}'
-    needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, fast]
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - name: 'Rules (booster)'
-            test-suite: 'test-prove-rules'
-            test-args:
-            timeout: 100
-            parallel: 6
-          - name: 'Rules (booster-dev)'
-            test-suite: 'test-prove-rules'
-            test-args: '--use-booster-dev'
-            timeout: 45
-            parallel: 8
-          - name: 'Functional'
-            test-suite: 'test-prove-functional'
-            test-args:
-            timeout: 45
-            parallel: 2
-          - name: 'Optimizations'
-            test-suite: 'test-prove-optimizations'
-            test-args:
-            timeout: 45
-            parallel: 1
-          - name: 'DSS'
-            test-suite: 'test-prove-dss'
-            test-args:
-            timeout: 45
-            parallel: 1
-    timeout-minutes: ${{ matrix.timeout }}
-    steps:
-      - name: 'Check out code'
-        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:
-          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'
-      - 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'
-        if: always()
-        run: |
-          docker stop --time=0 kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }}
-
-  nix:
-    name: 'Nix'
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - runner: normal
-          - runner: macos-13
-          - runner: ARM64
-    needs: kevm-pyk-code-quality-checks
-    runs-on: ${{ matrix.runner }}
-    timeout-minutes: 60
-    steps:
-      - name: 'Check out code'
-        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
-        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'
-        run: GC_DONT_GC=1 nix build --extra-experimental-features 'nix-command flakes' --print-build-logs .#kevm-test

.github/workflows/update-version.yml

@@ -38,24 +38,5 @@ jobs:
           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
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-      - uses: cachix/cachix-action@v12
-        with:
-          name: k-framework
-          authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
-      - name: 'Update nix flake inputs'
-        run: |
-          K_VERSION=v$(cat deps/k_release)
-          BKP_VERSION=$(cat deps/blockchain-k-plugin_release)
-          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
-          nix run .#update-from-submodules
-          nix flake update
-          git add flake.nix flake.lock && git commit -m 'flake.{nix,lock}: update Nix derivations' || true
       - name: 'Push updates'
         run: git push

Makefile

@@ -143,7 +143,7 @@ KEEP_OUTPUTS  := false
 CHECK         := git --no-pager diff --no-index --ignore-all-space -R
 
 tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_MODE     = VMTESTS
-tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_SCHEDULE = DEFAULT
+tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_SCHEDULE = HOMESTEAD
 
 tests/%.run-interactive: tests/%
 	$(POETRY_RUN) kevm-pyk run $< $(KEVM_OPTS) $(KRUN_OPTS) --target $(TEST_CONCRETE_BACKEND)                          \

README.md

@@ -219,7 +219,7 @@ You can call `kevm-pyk --help` to get a quick summary of how to use the script.
 Run the file `tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json`:
 
 ```sh
-poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/BlockchainTests/GeneralStateTests/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 HOMESTEAD --mode VMTESTS
 ```
 
 To enable the debug symbols for the llvm backend, build using this command:

kevm-pyk/src/kevm_pyk/__main__.py

@@ -598,15 +598,30 @@ def exec_run(options: RunOptions) -> None:
             kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas
         )
 
-    kevm.run(
-        kore_pattern,
-        depth=options.depth,
-        term=True,
-        expand_macros=options.expand_macros,
-        output=options.output,
-        check=True,
-        debugger=options.debugger,
-    )
+    if options.proof_hint:
+        logging.warning(
+            'Running KEVM with proof hint options enabled, remember to not use this with any `--verbose` mode if you are redirecting its output.'
+        )
+        output_bytes = kevm.run_proof_hint(
+            kore_pattern,
+            depth=options.depth,
+            parser='cat',
+            term=True,
+            expand_macros=options.expand_macros,
+            debugger=options.debugger,
+            proof_hint=True,
+        )
+        sys.stdout.buffer.write(output_bytes)
+    else:
+        kevm.run(
+            kore_pattern,
+            depth=options.depth,
+            term=True,
+            expand_macros=options.expand_macros,
+            output=options.output,
+            check=True,
+            debugger=options.debugger,
+        )
 
 
 def exec_kast(options: KastOptions) -> None:

kevm-pyk/src/kevm_pyk/cli.py

@@ -255,6 +255,13 @@ def _create_argument_parser() -> ArgumentParser:
         action='store_true',
         help='Run GDB debugger for execution.',
     )
+    run_args.add_argument(
+        '--proof-hint',
+        dest='proof_hint',
+        default=None,
+        action='store_true',
+        help='Generate proof hint instead of final configuration.',
+    )
 
     kast_args = command_parser.add_parser(
         'kast',
@@ -706,13 +713,15 @@ class RunOptions(
     output: KRunOutput
     expand_macros: bool
     debugger: bool
+    proof_hint: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
         return {
             'output': KRunOutput.PRETTY,
             'expand_macros': True,
             'debugger': False,
+            'proof_hint': False,
         }
 
     @staticmethod
@@ -723,6 +732,9 @@ def from_option_string() -> dict[str, str]:
             | EVMChainOptions.from_option_string()
             | TargetOptions.from_option_string()
             | SaveDirOptions.from_option_string()
+            | {
+                'proof-hint': 'proof_hint',
+            }
         )
 
     @staticmethod
@@ -896,7 +908,6 @@ def kprove_legacy_args(self) -> ArgumentParser:
     @cached_property
     def evm_chain_args(self) -> ArgumentParser:
         schedules = (
-            'DEFAULT',
             'FRONTIER',
             'HOMESTEAD',
             'TANGERINE_WHISTLE',

kevm-pyk/src/kevm_pyk/gst_to_kore.py

@@ -1,13 +1,12 @@
 from __future__ import annotations
 
-import json
 import logging
 import sys
 from argparse import ArgumentParser
 from typing import TYPE_CHECKING
 
 from pyk.cli.utils import file_path
-from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer
+from pyk.kore.prelude import INT, SORT_JSON, SORT_K_ITEM, inj, int_dv, json_to_kore, top_cell_initializer
 from pyk.kore.syntax import App, SortApp
 
 from .cli import KEVMCLIArgs
@@ -39,7 +38,6 @@ def kore_pgm_to_kore(pgm: Pattern, pattern_sort: SortApp, schedule: str, mode: s
         '$SCHEDULE': inj(SORT_SCHEDULE, SORT_K_ITEM, _schedule_to_kore(schedule)),
         '$MODE': inj(SORT_MODE, SORT_K_ITEM, _mode_to_kore(mode)),
         '$CHAINID': inj(INT, SORT_K_ITEM, int_dv(chainid)),
-        '$USEGAS': inj(BOOL, SORT_K_ITEM, bool_dv(usegas)),
     }
     return top_cell_initializer(config)
 
@@ -59,7 +57,7 @@ def main() -> None:
 
 
 def _exec_gst_to_kore(input_file: Path, schedule: str, mode: str, chainid: int, usegas: bool) -> None:
-    gst_data = json.loads(input_file.read_text())
+    gst_data = input_file.read_text()
     kore = gst_to_kore(gst_data, schedule, mode, chainid, usegas)
     kore.write(sys.stdout)
     sys.stdout.write('\n')

kevm-pyk/src/kevm_pyk/kdist/plugin.py

@@ -26,6 +26,8 @@ def __init__(self, kompile_args: Mapping[str, Any]):
         self._kompile_args = dict(kompile_args)
 
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], verbose: bool) -> None:
+        llvm_proof_hint_debugging = bool(args.get('llvm-proof-hint-debugging', ''))
+        llvm_proof_hint_instrumentation = bool(args.get('llvm-proof-hint-instrumentation', ''))
         enable_llvm_debug = bool(args.get('enable-llvm-debug', ''))
         debug_build = bool(args.get('debug-build', ''))
         ccopts = [ccopt for ccopt in args.get('ccopts', '').split(' ') if ccopt]
@@ -37,6 +39,8 @@ def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any], v
             ccopts=ccopts,
             plugin_dir=deps['evm-semantics.plugin'],
             debug_build=debug_build,
+            llvm_proof_hint_debugging=llvm_proof_hint_debugging,
+            llvm_proof_hint_instrumentation=llvm_proof_hint_instrumentation,
             **self._kompile_args,
         )
 

kevm-pyk/src/kevm_pyk/kompile.py

@@ -55,6 +55,8 @@ def kevm_kompile(
     ccopts: Iterable[str] = (),
     optimization: int = 0,
     llvm_kompile_type: LLVMKompileType | None = None,
+    llvm_proof_hint_debugging: bool = False,
+    llvm_proof_hint_instrumentation: bool = False,
     enable_llvm_debug: bool = False,
     plugin_dir: Path | None = None,
     debug_build: bool = False,
@@ -79,6 +81,8 @@ def kevm_kompile(
         ccopts=ccopts,
         optimization=optimization,
         llvm_kompile_type=llvm_kompile_type,
+        llvm_proof_hint_debugging=llvm_proof_hint_debugging,
+        llvm_proof_hint_instrumentation=llvm_proof_hint_instrumentation,
         enable_llvm_debug=enable_llvm_debug,
         debug_build=debug_build,
         debug=debug,
@@ -101,6 +105,8 @@ def run_kompile(
     ccopts: Iterable[str] = (),
     optimization: int = 0,
     llvm_kompile_type: LLVMKompileType | None = None,
+    llvm_proof_hint_debugging: bool = False,
+    llvm_proof_hint_instrumentation: bool = False,
     enable_llvm_debug: bool = False,
     debug_build: bool = False,
     debug: bool = False,
@@ -135,6 +141,8 @@ def run_kompile(
                 ccopts=ccopts,
                 opt_level=optimization,
                 llvm_kompile_type=llvm_kompile_type,
+                llvm_proof_hint_debugging=llvm_proof_hint_debugging,
+                llvm_proof_hint_instrumentation=llvm_proof_hint_instrumentation,
                 enable_llvm_debug=enable_llvm_debug,
             )
             return kompile(