diff --git a/Makefile b/Makefile
index 315161ec85..edba19354e 100644
--- a/Makefile
+++ b/Makefile
@@ -44,18 +44,13 @@ PLUGIN_FULL_PATH := $(abspath ${PLUGIN_SUBMODULE})
export PLUGIN_FULL_PATH
-.PHONY: all clean distclean \
- deps k-deps plugin-deps protobuf \
- poetry-env poetry shell kevm-pyk \
- build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm \
- test \
- test-integration test-conformance test-prove test-foundry-prove \
- test-vm test-rest-vm test-bchain test-rest-bchain \
- test-node \
- test-prove-smoke test-klab-prove \
- test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search \
- media media-pdf metropolis-theme \
- install uninstall
+.PHONY: all clean distclean install uninstall \
+ deps k-deps plugin-deps protobuf proto-tester \
+ poetry-env poetry shell kevm-pyk \
+ build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm \
+ test test-integration test-conformance test-prove test-foundry-prove test-prove-smoke \
+ test-vm test-rest-vm test-bchain test-rest-bchain test-node test-interactive test-interactive-run \
+ media media-pdf metropolis-theme
.SECONDARY:
@@ -70,8 +65,8 @@ distclean:
# Non-K Dependencies
# ------------------
-protobuf_out := $(LOCAL_LIB)/proto/proto/msg.pb.cc
-protobuf: $(protobuf_out)
+protobuf_out := $(LOCAL_LIB)/proto/proto/msg.pb.cc
+protobuf: $(protobuf_out)
$(protobuf_out): $(NODE_DIR)/proto/msg.proto
@mkdir -p $(LOCAL_LIB)/proto
@@ -320,7 +315,6 @@ install_libs := $(haskell_kompiled) \
$(foundry_kompiled) \
$(haskell_standalone_kompiled) \
$(patsubst %, include/kframework/lemmas/%, $(kevm_lemmas)) \
- kore-json.py \
release.md \
version
@@ -348,12 +342,12 @@ $(KEVM_LIB)/release.md: INSTALL.md
build: $(patsubst %, $(KEVM_BIN)/%, $(install_bins)) $(patsubst %, $(KEVM_LIB)/%, $(install_libs))
-build-llvm: $(KEVM_LIB)/$(llvm_kompiled) $(KEVM_LIB)/kore-json.py
-build-haskell: $(KEVM_LIB)/$(haskell_kompiled) $(KEVM_LIB)/kore-json.py
-build-haskell-standalone: $(KEVM_LIB)/$(haskell_standalone_kompiled) $(KEVM_LIB)/kore-json.py
+build-llvm: $(KEVM_LIB)/$(llvm_kompiled)
+build-haskell: $(KEVM_LIB)/$(haskell_kompiled)
+build-haskell-standalone: $(KEVM_LIB)/$(haskell_standalone_kompiled)
build-node: $(KEVM_LIB)/$(node_kompiled)
build-kevm: $(KEVM_BIN)/kevm $(KEVM_LIB)/version $(kevm_includes) $(plugin_includes)
-build-foundry: $(KEVM_BIN)/kevm $(KEVM_LIB)/$(foundry_kompiled) $(KEVM_LIB)/kore-json.py
+build-foundry: $(KEVM_BIN)/kevm $(KEVM_LIB)/$(foundry_kompiled)
all_bin_sources := $(shell find $(KEVM_BIN) -type f | sed 's|^$(KEVM_BIN)/||')
all_lib_sources := $(shell find $(KEVM_LIB) -type f \
@@ -408,32 +402,13 @@ test: test-integration test-conformance test-prove test-interactive
tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_MODE = VMTESTS
tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_SCHEDULE = DEFAULT
-tests/%.run: tests/%
- $(KEVM) interpret $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND) \
- --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID) \
- > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
- || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
- $(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
-
tests/%.run-interactive: tests/%
- $(KEVM) run $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND) \
+ $(POETRY_RUN) $(KEVM) run $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND) \
--mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID) \
> tests/$*.$(TEST_CONCRETE_BACKEND)-out \
|| $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
-tests/%.run-expected: tests/% tests/%.expected
- $(KEVM) run $< $(KEVM_OPTS) $(KRUN_OPTS) --backend $(TEST_CONCRETE_BACKEND) \
- --mode $(KEVM_MODE) --schedule $(KEVM_SCHEDULE) --chainid $(KEVM_CHAINID) \
- > tests/$*.$(TEST_CONCRETE_BACKEND)-out \
- || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/$*.expected
- $(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
-
-tests/interactive/%.json.gst-to-kore.check: tests/ethereum-tests/GeneralStateTests/VMTests/%.json $(KEVM_BIN)/kevm
- $(KEVM) kast $< $(KEVM_OPTS) $(KAST_OPTS) > tests/interactive/$*.gst-to-kore.out
- $(CHECK) tests/interactive/$*.gst-to-kore.out tests/interactive/$*.gst-to-kore.expected
- $(KEEP_OUTPUTS) || rm -rf tests/interactive/$*.gst-to-kore.out
-
# solc-to-k
# ---------
@@ -443,7 +418,7 @@ PYTEST_ARGS :=
test-foundry-prove: poetry build-kevm build-foundry
$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+="-k test_foundry_prove.py -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)"
-tests/specs/examples/%-bin-runtime.k: KEVM_OPTS += --pyk --verbose
+tests/specs/examples/%-bin-runtime.k: KEVM_OPTS += --verbose
tests/specs/examples/%-bin-runtime.k: KEVM := $(POETRY_RUN) kevm
tests/specs/examples/erc20-spec/haskell/timestamp: tests/specs/examples/erc20-bin-runtime.k
@@ -475,11 +450,6 @@ tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_F
--syntax-module $(KPROVE_MODULE) \
$(KOMPILE_OPTS)
-tests/%.search: tests/%
- $(KEVM) search $< " EVMC_INVALID_INSTRUCTION " $(KEVM_OPTS) $(KSEARCH_OPTS) --backend $(TEST_SYMBOLIC_BACKEND) > $@-out
- $(CHECK) $@-out $@-expected
- $(KEEP_OUTPUTS) || rm -rf $@-out
-
# Smoke Tests
smoke_tests_run = tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json \
@@ -514,9 +484,6 @@ test-prove: tests/specs/opcodes/evm-optimizations-spec.md poetry build-kevm buil
test-prove-smoke: $(prove_smoke_tests:=.prove)
-test-klab-prove: KPROVE_OPTS += --debugger
-test-klab-prove: $(smoke_tests_prove:=.prove)
-
# 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)' > $@
@@ -528,16 +495,12 @@ test-integration: poetry build-kevm build-haskell build-llvm
# Interactive Tests
-test-interactive: test-interactive-run test-interactive-prove test-interactive-search test-interactive-help
+test-interactive: test-interactive-run
test-interactive-run: $(smoke_tests_run:=.run-interactive)
-test-interactive-prove: $(smoke_tests_prove:=.prove)
-search_tests:=$(wildcard tests/interactive/search/*.evm)
-test-interactive-search: $(search_tests:=.search)
-
-test-interactive-help:
- $(KEVM) help
+node_tests:=$(wildcard tests/vm/*.bin)
+test-node: $(node_tests:=.run-node)
proto_tester := $(LOCAL_BIN)/proto_tester
proto-tester: $(proto_tester)
@@ -545,9 +508,6 @@ $(proto_tester): tests/vm/proto_tester.cpp
@mkdir -p $(LOCAL_BIN)
$(CXX) -I $(LOCAL_LIB)/proto $(protobuf_out) $< -o $@ -lprotobuf -lpthread
-node_tests:=$(wildcard tests/vm/*.bin)
-test-node: $(node_tests:=.run-node)
-
tests/vm/%.run-node: tests/vm/%.expected $(KEVM_BIN)/kevm-vm $(proto_tester)
bash -c " \
kevm-vm 8888 127.0.0.1 & \
diff --git a/README.md b/README.md
index 0994cde5da..03a3c9ed2f 100644
--- a/README.md
+++ b/README.md
@@ -262,7 +262,7 @@ make build-llvm KEVM_OPTS=--enable-llvm-debug
To debug a conformance test, add the `--debugger` flag to the command:
```sh
-kevm interpret tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --backend llvm --mode NORMAL --schedule MERGE --chainid 1 --debugger
+kevm run tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --backend llvm --mode NORMAL --schedule MERGE --chainid 1 --debugger
```
### Keeping in mind while developing
diff --git a/VERIFICATION.md b/VERIFICATION.md
index 27aa66def0..6f60561656 100644
--- a/VERIFICATION.md
+++ b/VERIFICATION.md
@@ -18,7 +18,7 @@ It has two modules:
The first step is kompiling the `.k` file with the below command.
```sh
-kevm kompile sum-to-n-spec.k --pyk --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile sum-to-n-spec.k --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
```
In this example, the arguments used are:
@@ -49,7 +49,7 @@ In this example, we rely on a helper module, `ERC20-VERIFICATION`, which must be
The module is generated using the following `solc-to-k` command.
```sh
-kevm solc-to-k ERC20.sol ERC20 --pyk --main-module ERC20-VERIFICATION > erc20-bin-runtime.k
+kevm solc-to-k ERC20.sol ERC20 --main-module ERC20-VERIFICATION > erc20-bin-runtime.k
```
- `solc-to-k` will parse a Solidity contract and generate a helper K module.
@@ -61,13 +61,13 @@ These rules are then used in the claims. As an example, the `#binRuntime(ERC20)`
Following this, we can compile the Markdown file with:
```sh
-kevm kompile erc20-spec.md --pyk --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
+kevm kompile erc20-spec.md --backend haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
```
Next, run the prover with:
```sh
-kevm prove erc20-spec.md --backend haskell --definition erc20-spec/haskell --pyk --claim ERC20-SPEC.decimals
+kevm prove erc20-spec.md --backend haskell --definition erc20-spec/haskell --claim ERC20-SPEC.decimals
```
Here, `--claim` tells the prover to run only the `decimals` spec from the `ERC20-SPEC` module.
@@ -89,10 +89,10 @@ kevm prove tests/specs/erc20/ds/transfer-failure-1-a-spec.k --definition tests/s
In addition to this, you can use `kevm show-kcfg ...` or `kevm view-kcfg ...` to get a visualization.
-`kevm view-kcfg [spec_file] [--save-directory save_directory] [--claim claim_label] ...` command takes the same basic arguments as `kevm prove --pyk ...` does, including:
+`kevm view-kcfg [spec_file] [--save-directory save_directory] [--claim claim_label] ...` command takes the same basic arguments as `kevm prove ...` does, including:
- `spec_file` is the file to look in for specifications. This file is read like with `kevm prove —pyk …`; the `KProve.get_claims` invokes the frontend.
- - `--save_directory` must be passed as where the KCFGs have been saved (by a previous call to `kevm prove --pyk --save-directory save_directory ...`
- - `--claim claim_label` option is added, but unlike the `kevm prove --pyk ...`, you can only repeat it once. This option lets you select an individual claim out of the `spec_file`; if not supplied, it’s assumed that only one spec is present.
+ - `--save_directory` must be passed as where the KCFGs have been saved (by a previous call to `kevm prove --save-directory save_directory ...`
+ - `--claim claim_label` option is added, but unlike the `kevm prove ...`, you can only repeat it once. This option lets you select an individual claim out of the `spec_file`; if not supplied, it’s assumed that only one spec is present.
- `--spec-module spec_module` is also an inherited option.
The interactive KCFG (`view-kcfg`) puts your terminal in *application mode*. To select text in this mode, hold the modifier key provided by your terminal emulator (typically SHIFT or OPTION) while clicking and dragging. Refer to the [Textualize documentation](https://github.com/Textualize/textual/blob/main/FAQ.md#how-can-i-select-and-copy-text-in-a-textual-app) for more information.
@@ -101,8 +101,8 @@ A running example:
```sh
mkdir kcfgs
-kevm kompile --pyk --backend haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
-kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --pyk --verbose --save-directory kcfgs
+kevm kompile --backend haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --verbose --save-directory kcfgs
kevm view-kcfg --verbose kcfgs tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell
```
diff --git a/bin/kevm b/bin/kevm
index 8f2c43d385..0856f61fb5 100755
--- a/bin/kevm
+++ b/bin/kevm
@@ -54,47 +54,33 @@ run_kevm_pyk() {
pyk_args+=(-I "${INSTALL_INCLUDE}/kframework")
;;
esac
- ! ${verbose} || pyk_args+=(--verbose)
- ! ${debug} || pyk_args+=(--debug)
- ! ${bug_report} || pyk_args+=(--bug-report)
+ ! ${verbose} || pyk_args+=(--verbose)
+ ! ${debug} || pyk_args+=(--debug)
execute python3 -m kevm_pyk "${pyk_command}" "$@" "${pyk_args[@]}"
}
# User Commands
-run_kompile() {
- local kompile_opts
- ! ${verbose} || kompile_opts+=(--verbose)
- ! ${debug} || kompile_opts+=(--debug)
- ! ${bug_report} || kompile_opts+=(--bug-report)
- execute python3 -m kevm_pyk kompile "${run_file}" "$@" "${kompile_opts[@]}"
-}
-
run_krun() {
local cschedule cmode cchainid parser krun_args
check_k_install
- cschedule=$cSCHEDULE_kore
- cmode=$cMODE_kore
- cchainid=$cCHAINID_kore
- parser='cat'
-
krun_args=(--definition "${backend_dir}" "${run_file}")
- if ! ${pyk}; then
- ! ${debugger} || krun_args+=(--debugger)
+ if ${debugger}; then
+ cmode="Lbl${mode}{}()"
+ cschedule="Lbl${schedule}'Unds'EVM{}()"
+ cchainid="\dv{SortInt{}}(\"${chainid}\")"
+ parser='cat'
+ krun_args+=(--debugger)
krun_args+=(-cSCHEDULE="${cschedule}" -pSCHEDULE="${parser}")
krun_args+=(-cMODE="${cmode}" -pMODE="${parser}")
krun_args+=(-cCHAINID="${cchainid}" -pCHAINID="${parser}")
+ execute krun "${krun_args[@]}" "$@"
else
krun_args+=(--schedule ${schedule})
krun_args+=(--mode ${mode})
krun_args+=(--chainid ${chainid})
- fi
-
- if ! ${pyk}; then
- execute krun "${krun_args[@]}" "$@"
- else
run_kevm_pyk run "${krun_args[@]}" "$@"
fi
}
@@ -102,113 +88,25 @@ run_krun() {
run_kast() {
local output_mode
- if [ $# -eq 0 ]; then
- output_mode=kore
- else
+ output_mode=kore
+ if [[ $# -gt 0 ]]; then
output_mode="$1"; shift
fi
case "${run_file}-${output_mode}" in
- *.json-kore) if ! ${pyk}; then
- execute kore-json.py "${run_file}" "${cSCHEDULE_kore}" "${cMODE_kore}" "${cCHAINID_kore}"
- else
- check_k_install
- gst-to-kore "${run_file}" --schedule "${schedule}" --mode "${mode}" --chainid "${chainid}" "$@"
- fi
- ;;
- *.json-kast) fatal "kast output is not supported for .json input"
- ;;
- *) check_k_install ; kast --definition "${backend_dir}" "${run_file}" --output "${output_mode}" "$@"
- ;;
+ *.json-kore) check_k_install ; gst-to-kore "${run_file}" --schedule "${schedule}" --mode "${mode}" --chainid "${chainid}" "$@" ;;
+ *) check_k_install ; kast --definition "${backend_dir}" "${run_file}" --output "${output_mode}" "$@" ;;
esac
}
-run_prove() {
- local prove_args
-
- check_k_install
-
- if ${pyk}; then
- run_kevm_pyk prove "${run_file}" "$@"
- else
- prove_args=(prove-legacy "${run_file}")
- ! ${debugger} || prove_args+=(--debugger)
- if ${profile_haskell}; then
- eventlog_name="${run_file}.eventlog"
- prove_args+=("--haskell-backend-arg=\"+RTS -l -ol${eventlog_name} -RTS\"")
- cur_dir=$(pwd)
- run_script="cd "${cur_dir}" && run_kevm_pyk "${prove_args[@]}" "$@""
- timeout -s INT "${profile_timeout}" bash -c "${run_script}" || true
- execute kore-prof "${eventlog_name}" ${kore_prof_arg} > "${eventlog_name}.json"
- else
- run_kevm_pyk "${prove_args[@]}" "$@"
- fi
- fi
-}
-
-run_search() {
- local search_pattern
- search_pattern="$1" ; shift
- run_krun --search --pattern "$search_pattern" "$@"
-}
-
-run_interpret() {
- local kast output exit_status krun_args bug_report_name
-
- kast="$(mktemp)"
- output="$(mktemp)"
- trap "rm -rf ${kast} ${output}" INT TERM EXIT
- exit_status=0
- run_kast kore > ${kast}
- run_file="${kast}"
- krun_args=(--term --parser cat --no-expand-macros --output kore)
- if [[ ${backend} == haskell ]]; then
- KORE_EXEC_OPTS="${KORE_EXEC_OPTS:-} --smt none"
- bug_report_name="kevm-bug-$(basename "${run_file%.json}")"
- ! ${bug_report} || KORE_EXEC_OPTS="${KORE_EXEC_OPTS} --bug-report ${bug_report_name}"
- export KORE_EXEC_OPTS
- fi
- if ${debugger}; then
- run_krun "${krun_args[@]}" "$@" || exit_status="$?"
- else
- run_krun "${krun_args[@]}" "$@" > "${output}" || exit_status="$?"
- fi
- if ${unparse} || [[ "${exit_status}" != '0' ]]; then
- cat "${output}" | "${KEVM}" kast --backend "${backend}" - pretty --input kore --sort GeneratedTopCell
- fi
- exit "${exit_status}"
-}
-
-run_solc() {
- local contract_name
-
- contract_name="$1" ; shift
- run_kevm_pyk solc-to-k "${run_file}" "${contract_name}" --definition "${backend_dir}" "$@"
-}
-
-run_foundry() {
- local foundry_command
- foundry_command=("${run_command}")
- if [[ "${run_command}" == foundry-kompile ]]; then
- foundry_command+=(--definition "${backend_dir}")
- fi
- run_kevm_pyk "${foundry_command[@]}" "$@"
-}
-
# Main
# ----
backend="llvm"
-unparse=true
debugger=false
-profile_haskell=false
-profile_timeout="0"
-kore_prof_arg=""
-bug_report=false
mode=NORMAL
schedule=MERGE
chainid=1
-pyk=false
if [[ $# -eq 0 ]]; then
run_command='help'
@@ -219,51 +117,24 @@ fi
if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
echo "
usage: ${KEVM} run [--backend (llvm|haskell)] [--profile|--debug] * *
- ${KEVM} interpret [--backend (llvm|haskell)] [--no-unparse] [--profile|--debug] * *
${KEVM} kast [--backend (llvm|haskell)] [--profile|--debug] *