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

Author: palinatolmach

.github/workflows/test-pr.yml

@@ -96,7 +96,7 @@ jobs:
             test-suite: 'test-prove-rules'
             test-args: '--use-booster-dev'
             timeout: 45
-            parallel: 8
+            parallel: 6
           - name: 'Functional'
             test-suite: 'test-prove-functional'
             test-args:
@@ -107,6 +107,11 @@ jobs:
             test-args:
             timeout: 45
             parallel: 1
+          - name: 'Summarization'
+            test-suite: 'test-summarize'
+            test-args:
+            timeout: 30
+            parallel: 6
           - name: 'DSS'
             test-suite: 'test-prove-dss'
             test-args:
@@ -127,7 +132,7 @@ jobs:
       - 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'
+        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'
       - 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'

Makefile

@@ -90,6 +90,9 @@ profile: poetry
 	$(MAKE) -C kevm-pyk/ profile
 	find /tmp/pytest-of-$$(whoami)/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
 
+test-summarize: poetry
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+='-k "test_summarize"'
+
 
 # Smoke Tests
 

deps/blockchain-k-plugin_release

@@ -1 +1 @@
-c9264b240c00d1f6cc20e22aac83c94d1a499138
+651a2db5afc1789c89553f9113c1afa39e391e35

deps/k_release

@@ -1 +1 @@
-7.1.212
+7.1.219

flake.lock

@@ -2,14 +2,14 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.212";
+    k-framework.url = "github:runtimeverification/k/v7.1.219";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
     poetry2nix.follows = "k-framework/poetry2nix";
     blockchain-k-plugin = {
       url =
-        "github:runtimeverification/blockchain-k-plugin/c9264b240c00d1f6cc20e22aac83c94d1a499138";
+        "github:runtimeverification/blockchain-k-plugin/651a2db5afc1789c89553f9113c1afa39e391e35";
       inputs.flake-utils.follows = "k-framework/flake-utils";
       inputs.nixpkgs.follows = "k-framework/nixpkgs";
     };

flake.nix

@@ -1,3 +1,5 @@
 /dist/
 __pycache__/
 .coverage
+proofs/
+summaries/