Skip to content

Commit b7ef38f

Browse files
ehildenbrv-jenkinsanvacaru
authored
Introduce RPC based prover to kevm (#1538)
* include/evm: name various CALL rules * kevm-pyk/kevm: add KEVM.{is_terminal,extract_branches,abstract} * kevm-pyk/kevm: make KEVM.abstract a staticmethod * kevm-pyk/kevm: refine the KEVM.is_terminal check * kevm-pyk/kevm: avoid duplicate unique call * kevm-pyk/{__main__,utils}: use upstream KCFGExplore class for auto-exploration * kevm-pyk/__main__: remove unused --lemma argument * kevm-pyk/__main__: remove unused arguments * kevm-pyk/__main__: set defauft for max_depth, max_iterations * kevm-pyk/__main__: more default arguments * kevm-pyk/{utils,__main__}: factor out parallel_kcfg_explore * kevm-pyk/gst_to_kore: fix quoting warning * kevm_pyk/{utils,__main__}: simplify passing proof problems to parallel_kcfg_explore * kevm_pyk/__main__: adapt exec_prove to use parallel_kcfg_explore * kevm_pyk/__main__: promote --md-selector to k_args from k_kompile_args * kevm-pyk/{utils,__main__}: correctly handle saving proofs to a given directory * kevm-pyk/utils: pack arguments to _call_rpc correctly * bin/kevm, kevm-pyk/__main__: add kevm view-kcfg command * Makefile: go further for each block on CI, simplify initial states * .github/test-pr: increase parallelism * kevm-pyk/utils: remove unused function * kevm-pyk/{utils,__main__}: adapt to new upstream KCFGExplore * kevm-pyk/kevm: implement short-info method * kevm_pyk/kevm: avoid crashes due to missing cells in configuration * Makefile, tests/failing-symbolic.pyk: enable pyk prover for haskell backend * kevm-pyk/: default to random base port, not hardcoded one * Makefile: activate pyk before calling prover * tests/foundry: exclude tests that reach #Bottom * tests/failing-symbolic.pyk: add tests which are not passing with incremental exploration * kevm-pyk/__main__: default to checking implication every block of execution * tests/failing-symbolic.pyk: re-enable tests with incremental exploration * .github/test-pr: increases parallelism * kevm-pyk/__main__: new foundry-simplify-node command * kevm-pyk/__main__: use KCFGExplore for foundry-simplify-node * tests/failing-symbolic.pyk: add failing tests * kevm-pyk/__main__: do not crash on bottom result * .github/test-pr: remove --retry option for foundry proofs * kevm-pyk/__main__: small fix to simplify_init logic * tests/failing-symbolic.pyk: ignore functional specs * kevm-pyk/__main__: factor out explore_args * Makefile: increase block size on proofs * kevm-pyk/__main__: factor out more explore_args * kevm-pyk/kevm: remove comment * kevm-pyk/kevm: remove useless statement * kevm-pyk/utils: simplify zip call * kevm-pyk/{utils,__main__}: hoist effectful printing of results to main methods * Makefile: run proofs with poetry * kevm-pyk/__main__: make sure to actually save Foundry KCFGs * kevm-pyk/{utils,__main__}: make sure we are using consistent naming scheme for KCFG files * tests/failing-symbolic.pyk: add bihu functional tests * tests/failing-symbolic.pyk: add another two failing tests * kevm-pyk/{utils,__main__}: use KCFGExplore.{read_cfg,write_cfg} * kevm-pyk/__main__: use short info node printer in KCFGViewer * bin/kevm: pass --debug through to kevm-pyk * kevm-pyk/__main__: correct how logging levels are handled * tests/foundry/exclude: remove tests failing due to out of gas * .github/test-pr: decrease parallelism slightly * tests/specs/functional/infinite-gas-spec: add failing gas comparison check for foundry * include/kframework/{infinite-gas,lemmas/int-simplification}: add lemmas for simplifying infinite gas query * kevm-pyk/kevm: remove unused method KEVM.abstract * Makefile: bring back --no-simplify-init on CI * tests/specs/function/infinite-gas-spec: another failing test * include/{infinite-gas,lemmas/int-simplification}: more simplifications * kevm-pyk/utils: remove unused function --------- Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Andrei <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
1 parent becd772 commit b7ef38f

File tree

7 files changed

+521
-295
lines changed

7 files changed

+521
-295
lines changed

‎.github/workflows/test-pr.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ jobs:
6161
- name: 'Build Definitions'
6262
run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make build-prove-haskell -j4'
6363
- name: 'Prove Haskell'
64-
run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove -j6 TEST_SYMBOLIC_BACKEND=haskell'
64+
run: docker exec -u user kevm-ci-haskell-${GITHUB_SHA} /bin/bash -c 'make test-prove -j9 TEST_SYMBOLIC_BACKEND=haskell'
6565
- name: 'Tear down Docker'
6666
if: always()
6767
run: |
@@ -85,7 +85,7 @@ jobs:
8585
- name: 'Build Foundry'
8686
run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
8787
- name: 'Test Foundry'
88-
run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=4 KPROVE_OPTS=--retry'
88+
run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry -j2 FOUNDRY_PAR=12'
8989
- name: 'Tear down Docker'
9090
if: always()
9191
run: |

‎Makefile

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -506,7 +506,7 @@ tests/foundry/out/kompiled/foundry.k: tests/foundry/out/kompiled/timestamp
506506

507507
tests/foundry/out/kompiled/foundry.k.prove: tests/foundry/out/kompiled/timestamp
508508
$(KEVM) foundry-prove tests/foundry/out \
509-
-j$(FOUNDRY_PAR) --no-simplify-init \
509+
-j$(FOUNDRY_PAR) --no-simplify-init --max-depth 1000 \
510510
$(KEVM_OPTS) $(KPROVE_OPTS) \
511511
$(addprefix --exclude-test , $(shell cat tests/foundry/exclude))
512512

@@ -533,7 +533,7 @@ tests/specs/examples/empty-bin-runtime.k: tests/specs/examples/Empty.sol $(KEVM_
533533

534534
.SECONDEXPANSION:
535535
tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)/timestamp
536-
$(KEVM) prove $< $(KEVM_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) $(KPROVE_OPTS) \
536+
$(POETRY_RUN) $(KEVM) prove $< $(KEVM_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) $(KPROVE_OPTS) \
537537
--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
538538

539539
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)
592592

593593
prove_specs_dir := tests/specs
594594
prove_failing_tests := $(shell cat tests/failing-symbolic.$(TEST_SYMBOLIC_BACKEND))
595+
prove_pyk_failing_tests := $(shell cat tests/failing-symbolic.pyk)
595596
prove_slow_tests := $(shell cat tests/slow.$(TEST_SYMBOLIC_BACKEND))
596597
prove_skip_tests := $(prove_failing_tests) $(prove_slow_tests)
597598
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
602603
prove_examples_tests := $(filter-out $(prove_skip_tests), $(wildcard $(prove_specs_dir)/examples/*-spec.k) $(wildcard $(prove_specs_dir)/examples/*-spec.md))
603604
prove_mcd_tests := $(filter-out $(prove_skip_tests), $(wildcard $(prove_specs_dir)/mcd/*-spec.k))
604605
prove_optimization_tests := $(filter-out $(prove_skip_tests), tests/specs/opcodes/evm-optimizations-spec.md)
606+
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)
607+
prove_pyk_tests := $(filter-out $(prove_pyk_failing_tests), $(prove_all_tests))
605608
prove_smoke_tests := $(shell cat tests/specs/smoke)
606609

607610
## best-effort list of prove kompiled definitions to produce ahead of time
@@ -643,6 +646,8 @@ test-failing-prove: $(prove_failing_tests:=.prove)
643646
test-klab-prove: KPROVE_OPTS += --debugger
644647
test-klab-prove: $(smoke_tests_prove:=.prove)
645648

649+
$(prove_pyk_tests:=.prove): KPROVE_OPTS += --pyk --max-depth 1000
650+
646651
# to generate optimizations.md, run: ./optimizer/optimize.sh &> output
647652
tests/specs/opcodes/evm-optimizations-spec.md: include/kframework/optimizations.md
648653
cat $< | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@

‎bin/kevm

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ run_kevm_pyk() {
5353
local pyk_command pyk_args
5454
pyk_command="$1" ; shift
5555
case "${pyk_command}" in
56-
kompile|run|prove|solc-to-k|foundry-kompile|foundry-prove)
56+
kompile|run|prove|solc-to-k|foundry-kompile|foundry-prove|view-kcfg)
5757
pyk_args=(--definition "${backend_dir}")
5858
pyk_args+=(-I "${INSTALL_INCLUDE}/kframework")
5959
;;
@@ -365,6 +365,7 @@ kevm_port='8545'
365365
kevm_host='127.0.0.1'
366366
[[ ! "${run_command}" == prove ]] || backend=haskell
367367
[[ ! "${run_command}" == solc-to-k ]] || backend=haskell
368+
[[ ! "${run_command}" == view-kcfg ]] || backend=haskell
368369
[[ ! "${run_command}" == foundry-* ]] || backend=foundry
369370
[[ ! "${run_command}" == interpret ]] || unparse=false
370371
args=()
@@ -410,7 +411,7 @@ if ${pyk}; then
410411
fi
411412

412413
# get the run file
413-
if [[ "${run_command}" != foundry-* ]]; then
414+
if [[ "${run_command}" != foundry-* ]] && [[ "${run_command}" != 'view-kcfg' ]]; then
414415
run_file="$1" ; shift
415416
if [[ "${run_file}" == '-' ]]; then
416417
tmp_input="$(mktemp)"
@@ -432,14 +433,15 @@ cCHAINID_kast="#token(\"${chainid}\",\"Int\")"
432433
! ${debug} || set -x
433434

434435
case "$run_command-$backend" in
435-
kompile-@(llvm|haskell|node|foundry) ) run_kompile "$@" ;;
436-
run-@(llvm|haskell) ) run_krun "$@" ;;
437-
kast-@(llvm|haskell) ) run_kast "$@" ;;
438-
interpret-@(llvm|haskell) ) run_interpret "$@" ;;
439-
prove-@(haskell|foundry) ) run_prove "$@" ;;
440-
search-@(haskell) ) run_search "$@" ;;
441-
klab-view-* ) view_klab "$@" ;;
442-
solc-to-k-* ) run_solc "$@" ;;
443-
foundry-* ) run_foundry "$@" ;;
436+
kompile-@(llvm|haskell|node|foundry) ) run_kompile "$@" ;;
437+
run-@(llvm|haskell) ) run_krun "$@" ;;
438+
kast-@(llvm|haskell) ) run_kast "$@" ;;
439+
interpret-@(llvm|haskell) ) run_interpret "$@" ;;
440+
prove-@(haskell|foundry) ) run_prove "$@" ;;
441+
search-@(haskell) ) run_search "$@" ;;
442+
klab-view-* ) view_klab "$@" ;;
443+
view-kcfg-* ) run_kevm_pyk view-kcfg "$@" ;;
444+
solc-to-k-* ) run_solc "$@" ;;
445+
foundry-* ) run_foundry "$@" ;;
444446
*) ${KEVM} help ; fatal "Unknown command on backend: $run_command $backend" ;;
445447
esac

0 commit comments

Comments
 (0)