Introduce RPC based prover to kevm

.github/workflows/test-pr.yml

@@ -61,7 +61,7 @@ jobs:
       - name: 'Build Definitions'
         run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make build-prove-haskell -j4'
       - name: 'Prove Haskell'
-        run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove -j6 TEST_SYMBOLIC_BACKEND=haskell'
+        run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove -j9 TEST_SYMBOLIC_BACKEND=haskell'
       - name: 'Tear down Docker'
         if: always()
         run: |
@@ -85,7 +85,7 @@ jobs:
       - name: 'Build Foundry'
         run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
       - name: 'Test Foundry'
-        run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=4 KPROVE_OPTS=--retry'
+        run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=12'
       - name: 'Tear down Docker'
         if: always()
         run: |

Makefile

@@ -506,7 +506,7 @@ tests/foundry/out/kompiled/foundry.k: tests/foundry/out/kompiled/timestamp
 
 tests/foundry/out/kompiled/foundry.k.prove: tests/foundry/out/kompiled/timestamp
 	$(KEVM) foundry-prove tests/foundry/out                              \
-	    -j$(FOUNDRY_PAR) --no-simplify-init                              \
+	    -j$(FOUNDRY_PAR) --no-simplify-init --max-depth 1000             \
 	    $(KEVM_OPTS) $(KPROVE_OPTS)                                      \
 	    $(addprefix --exclude-test , $(shell cat tests/foundry/exclude))
 
@@ -533,7 +533,7 @@ tests/specs/examples/empty-bin-runtime.k: tests/specs/examples/Empty.sol $(KEVM_
 
 .SECONDEXPANSION:
 tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)/timestamp
-	$(KEVM) prove $< $(KEVM_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) $(KPROVE_OPTS)                   \
+	$(POETRY_RUN) $(KEVM) prove $< $(KEVM_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) $(KPROVE_OPTS) \
 	    --definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
 
 tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT) $(kevm_includes) $(plugin_includes) $(KEVM_BIN)/kevm
@@ -592,6 +592,7 @@ test-bchain: $(passing_bchain_tests:=.run)
 
 prove_specs_dir          := tests/specs
 prove_failing_tests      := $(shell cat tests/failing-symbolic.$(TEST_SYMBOLIC_BACKEND))
+prove_pyk_failing_tests  := $(shell cat tests/failing-symbolic.pyk)
 prove_slow_tests         := $(shell cat tests/slow.$(TEST_SYMBOLIC_BACKEND))
 prove_skip_tests         := $(prove_failing_tests) $(prove_slow_tests)
 prove_benchmarks_tests   := $(filter-out $(prove_skip_tests), $(wildcard $(prove_specs_dir)/benchmarks/*-spec.k))
@@ -602,6 +603,8 @@ prove_bihu_tests         := $(filter-out $(prove_skip_tests), $(wildcard $(prove
 prove_examples_tests     := $(filter-out $(prove_skip_tests), $(wildcard $(prove_specs_dir)/examples/*-spec.k) $(wildcard $(prove_specs_dir)/examples/*-spec.md))
 prove_mcd_tests          := $(filter-out $(prove_skip_tests), $(wildcard $(prove_specs_dir)/mcd/*-spec.k))
 prove_optimization_tests := $(filter-out $(prove_skip_tests), tests/specs/opcodes/evm-optimizations-spec.md)
+prove_all_tests          := $(prove_benchmarks_tests) $(prove_functional_tests) $(prove_opcodes_tests) $(prove_erc20_tests) $(prove_bihu_tests) $(prove_examples_tests) $(prove_mcd_tests) $(prove_optimization_tests)
+prove_pyk_tests          := $(filter-out $(prove_pyk_failing_tests), $(prove_all_tests))
 prove_smoke_tests        := $(shell cat tests/specs/smoke)
 
 ## best-effort list of prove kompiled definitions to produce ahead of time
@@ -643,6 +646,8 @@ test-failing-prove: $(prove_failing_tests:=.prove)
 test-klab-prove: KPROVE_OPTS += --debugger
 test-klab-prove: $(smoke_tests_prove:=.prove)
 
+$(prove_pyk_tests:=.prove): KPROVE_OPTS += --pyk --max-depth 1000
+
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
 tests/specs/opcodes/evm-optimizations-spec.md: include/kframework/optimizations.md
 	cat $< | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@

bin/kevm

@@ -53,7 +53,7 @@ run_kevm_pyk() {
     local pyk_command pyk_args
     pyk_command="$1" ; shift
     case "${pyk_command}" in
-        kompile|run|prove|solc-to-k|foundry-kompile|foundry-prove)
+        kompile|run|prove|solc-to-k|foundry-kompile|foundry-prove|view-kcfg)
             pyk_args=(--definition "${backend_dir}")
             pyk_args+=(-I "${INSTALL_INCLUDE}/kframework")
             ;;
@@ -365,6 +365,7 @@ kevm_port='8545'
 kevm_host='127.0.0.1'
 [[ ! "${run_command}" == prove     ]] || backend=haskell
 [[ ! "${run_command}" == solc-to-k ]] || backend=haskell
+[[ ! "${run_command}" == view-kcfg ]] || backend=haskell
 [[ ! "${run_command}" == foundry-* ]] || backend=foundry
 [[ ! "${run_command}" == interpret ]] || unparse=false
 args=()
@@ -410,7 +411,7 @@ if ${pyk}; then
 fi
 
 # get the run file
-if [[ "${run_command}" != foundry-* ]]; then
+if [[ "${run_command}" != foundry-* ]] && [[ "${run_command}" != 'view-kcfg' ]]; then
     run_file="$1" ; shift
     if [[ "${run_file}" == '-' ]]; then
         tmp_input="$(mktemp)"
@@ -432,14 +433,15 @@ cCHAINID_kast="#token(\"${chainid}\",\"Int\")"
 ! ${debug} || set -x
 
 case "$run_command-$backend" in
-    kompile-@(llvm|haskell|node|foundry)    ) run_kompile   "$@" ;;
-    run-@(llvm|haskell)                     ) run_krun      "$@" ;;
-    kast-@(llvm|haskell)                    ) run_kast      "$@" ;;
-    interpret-@(llvm|haskell)               ) run_interpret "$@" ;;
-    prove-@(haskell|foundry)                ) run_prove     "$@" ;;
-    search-@(haskell)                       ) run_search    "$@" ;;
-    klab-view-*                             ) view_klab     "$@" ;;
-    solc-to-k-*                             ) run_solc      "$@" ;;
-    foundry-*                               ) run_foundry   "$@" ;;
+    kompile-@(llvm|haskell|node|foundry) ) run_kompile            "$@" ;;
+    run-@(llvm|haskell)                  ) run_krun               "$@" ;;
+    kast-@(llvm|haskell)                 ) run_kast               "$@" ;;
+    interpret-@(llvm|haskell)            ) run_interpret          "$@" ;;
+    prove-@(haskell|foundry)             ) run_prove              "$@" ;;
+    search-@(haskell)                    ) run_search             "$@" ;;
+    klab-view-*                          ) view_klab              "$@" ;;
+    view-kcfg-*                          ) run_kevm_pyk view-kcfg "$@" ;;
+    solc-to-k-*                          ) run_solc               "$@" ;;
+    foundry-*                            ) run_foundry            "$@" ;;
     *) ${KEVM} help ; fatal "Unknown command on backend: $run_command $backend" ;;
 esac