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

Author: palinatolmach

.github/workflows/Dockerfile

@@ -23,6 +23,7 @@ RUN    apt-get update                  \
             libboost-test-dev          \
             libcrypto++-dev            \
             libprocps-dev              \
+            libsecp256k1-dev           \
             libssl-dev                 \
             libyaml-dev                \
             llvm-${LLVM_VERSION}-dev   \

.github/workflows/test-pr.yml

@@ -11,7 +11,7 @@ jobs:
 
   version-bump:
     name: 'Version Bump'
-    runs-on: [self-hosted, linux, flyweight-ephemeral]
+    runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -37,13 +37,12 @@ jobs:
 
   kevm-pyk-code-quality-checks:
     name: 'Code Quality Checks'
-    runs-on: [self-hosted, linux, flyweight-ephemeral]
+    runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
-      - uses: actions/setup-python@v4
         with:
-            python-version: "3.10"
+          submodules: recursive
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
       - name: 'Run code quality checks'
@@ -54,36 +53,26 @@ jobs:
   kevm-pyk-unit-tests:
     needs: kevm-pyk-code-quality-checks
     name: 'Unit Tests'
-    runs-on: [self-hosted, linux, normal-ephemeral]
+    runs-on: ubuntu-latest
     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"
+          submodules: recursive
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
       - name: 'Run unit tests'
-        run: |
-          make -C kevm-pyk cov-unit
+        run: make -C kevm-pyk cov-unit
 
   kevm-pyk-profile:
     needs: kevm-pyk-code-quality-checks
     name: 'Profiling'
-    runs-on: [self-hosted, linux, normal-ephemeral]
+    runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
         with:
           submodules: recursive
-          fetch-depth: 0
-      - name: Setup Python
-        uses: actions/setup-python@v4
-        with:
-          python-version: '3.10'
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
       - name: 'Run profiling'
@@ -100,15 +89,14 @@ jobs:
         uses: actions/checkout@v3
         with:
           submodules: recursive
-          fetch-depth: 0
       - name: 'Set up Docker'
         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.llvm evm-semantics.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.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'
@@ -178,16 +166,16 @@ jobs:
           ref: ${{ github.event.pull_request.head.sha }}
       - name: 'Install Nix'
         if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/install-nix-action@v19
+        uses: cachix/install-nix-action@v25
         with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
+          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@v12
+        uses: cachix/cachix-action@v14
         with:
           name: k-framework
           authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}

.github/workflows/update-version.yml

@@ -3,7 +3,7 @@ on:
   push:
     branches:
       - '_update-deps/runtimeverification/blockchain-k-plugin'
-      - '_update-deps/runtimeverification/pyk'
+      - '_update-deps/runtimeverification/k'
   workflow_dispatch:
 # Stop in progress workflows on the same branch and same workflow to use latest committed code
 concurrency:
@@ -30,15 +30,10 @@ jobs:
         uses: Gr1N/setup-poetry@v8
       - name: 'Update pyk release tag'
         run: |
-          PYK_VERSION="$(cat deps/pyk_release)"
-          sed -i 's!pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="[v0-9\.]*" }!pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="'${PYK_VERSION}'" }!' kevm-pyk/pyproject.toml
+          K_VERSION=v$(cat deps/k_release)
+          sed -i 's!pyk = { git = "https://github.com/runtimeverification/k.git", tag="[v0-9\.]*", subdirectory = "pyk" }!pyk = { git = "https://github.com/runtimeverification/k.git", tag="'${K_VERSION}'", subdirectory = "pyk" }!' kevm-pyk/pyproject.toml
           poetry -C kevm-pyk update
-          git add kevm-pyk/ && git commit -m "kevm-pyk/: sync poetry files pyk version ${PYK_VERSION}" || true
-      - name: 'Update K release file'
-        run: |
-          K_VERSION=$(poetry -C kevm-pyk run python3 -c 'import pyk; print(pyk.K_VERSION)')
-          echo ${K_VERSION} > deps/k_release
-          git add deps/k_release && git commit -m "deps/k_release: sync release file version ${K_VERSION}" || true
+          git add kevm-pyk/ && git commit -m "kevm-pyk/: sync poetry 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)
@@ -56,12 +51,11 @@ jobs:
           authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
       - name: 'Update nix flake inputs'
         run: |
-          K_VERSION=$(cat deps/k_release)
+          K_VERSION=v$(cat deps/k_release)
           BKP_VERSION=$(cat deps/blockchain-k-plugin_release)
-          PYK_VERSION=$(cat deps/pyk_release)
-          sed -i 's!    k-framework.url = "github:runtimeverification/k/[v0-9\.]*"!    k-framework.url = "github:runtimeverification/k/v'"${K_VERSION}"'"!' flake.nix
+          sed -i 's!    k-framework.url = "github:runtimeverification/k/[v0-9\.]*"!    k-framework.url = "github:runtimeverification/k/'"${K_VERSION}"'"!' flake.nix
           sed -i 's!    blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/[0-9a-f]*"!    blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/'"${BKP_VERSION}"'"!' flake.nix
-          sed -i 's!    pyk.url = "github:runtimeverification/pyk/[v0-9\.]*"!    pyk.url = "github:runtimeverification/pyk/'"${PYK_VERSION}"'"!' flake.nix
+          sed -i 's!    pyk.url = "github:runtimeverification/k/[v0-9\.]*?dir=pyk"!    pyk.url = "github:runtimeverification/k/'"${K_VERSION}"'?dir=pyk"!' 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

Makefile

@@ -60,7 +60,7 @@ test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
 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)' > $@
+	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)' > $@
 
 
 # Integration Tests

README.md

@@ -61,42 +61,41 @@ This repository generates the build-products for each backend in `$XDG_CACHE_HOM
 
 ### System Dependencies
 
-First install the following tools:
-
--   [git](https://git-scm.com/)
--   GNU [Bison](https://www.gnu.org/software/bison/), [Flex](https://github.com/westes/flex), and [Autoconf](http://www.gnu.org/software/autoconf/).
--   GNU [libmpfr](https://www.mpfr.org/) and [libtool](https://www.gnu.org/software/libtool/).
--   [Z3](https://github.com/Z3Prover/z3) version 4.12.1
-
-#### Installing Z3
-
-KEVM requires Z3 version 4.12.1, which you may need to install from a source build if your package manager supplies a different version.
-To do so, follow the instructions [here](https://github.com/Z3Prover/z3#building-z3-using-make-and-gccclang) after checking out the correct tag in the Z3 repository:
-
-```sh
-git clone https://github.com/Z3Prover/z3.git
-cd z3
-git checkout z3-4.12.1
-python scripts/mk_make.py
-cd build
-make
-sudo make install
-```
-
-On macOS, it is easiest to install Z3 from Homebrew.
-If you wish to install from the source, install it to an appropriate prefix (e.g. `/usr/local` on Intel machines).
 
 #### Ubuntu
 
 On Ubuntu >= 22.04 (for example):
 
 ```sh
-sudo apt-get install --yes                                                         \
-            autoconf bison clang-12 cmake curl flex gcc jq libboost-test-dev       \
-            libcrypto++-dev libffi-dev libgflags-dev libjemalloc-dev libmpfr-dev   \
-            libprocps-dev libsecp256k1-dev libssl-dev libtool libyaml-dev lld-12   \
-            llvm-12-tools make maven openjdk-11-jdk pkg-config python3 python3-dev \
-            python3-pip rapidjson-dev time zlib1g-dev libfmt-dev
+sudo apt-get install    \
+    bison               \
+    build-essential     \
+    clang-15            \
+    cmake               \
+    curl                \
+    flex                \
+    g++                 \
+    gcc                 \
+    libboost-test-dev   \
+    libfmt-dev          \
+    libgmp-dev          \
+    libjemalloc-dev     \
+    libmpfr-dev         \
+    libsecp256k1-dev    \
+    libstdc++-12-dev    \
+    libtool             \
+    libyaml-dev         \
+    libz3-dev           \
+    lld-15              \
+    llvm-15-tools       \
+    m4                  \
+    maven               \
+    openjdk-17-jdk      \
+    pkg-config          \
+    python3             \
+    python3-dev         \
+    z3                  \
+    zlib1g-dev
 ```
 
 On Ubuntu < 18.04, you'll need to skip `libsecp256k1-dev` and instead build it from source (via our `Makefile`):
@@ -122,8 +121,27 @@ After installing the Command Line Tools, [Homebrew](https://brew.sh/), and getti
 
 ```sh
 brew tap runtimeverification/k
-brew install java automake libtool gmp mpfr pkg-config maven libffi llvm@14 openssl python bash runtimeverification/k/[email protected] poetry solidity
-make libsecp256k1
+brew install    \
+    bison       \
+    boost       \
+    cmake       \
+    flex        \
+    fmt         \
+    gcc         \
+    gmp         \
+    openjdk     \
+    jemalloc    \
+    libyaml     \
+    llvm        \
+    make        \
+    maven       \
+    mpfr        \
+    pkg-config  \
+    python      \
+    secp256k1   \
+    stack       \
+    zlib        \
+    z3
 ```
 
 **NOTE**: It is recommended to use the homebrew version of `flex` and XCode.
@@ -204,10 +222,10 @@ APPLE_SILICON=true poetry -C kevm-pyk run kdist --verbose build evm-semantics.pl
 Finally, you can build the semantics.
 
 ```sh
-poetry -C kevm-pyk run kdist --verbose build -j4
+poetry -C kevm-pyk run kdist --verbose build -j6
 ```
 
-You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone,plugin}`, e.g.:
+You can build specific targets using options `evm-semantics.{llvm,kllvm,kllvm-runtime,haskell,haskell-standalone,plugin}`, e.g.:
 
 ```sh
 poetry -C kevm-pyk run kdist build -j2 evm-semantics.llvm evm-semantics.haskell

VERIFICATION.md

@@ -1 +1 @@
-b42e6ede9f6b72cedabc519810416e2994caad45
+4bbc741e910e41fd6c590edf5488d2b0bcf740e2

deps/blockchain-k-plugin_release

@@ -1 +1 @@
-6.1.46
+7.0.70