Merge remote-tracking branch 'origin/master' into balance-verification

Author: hjorthjort

Makefile

@@ -21,10 +21,10 @@ export LUA_PATH
 
 .PHONY: all clean \
         deps haskell-deps \
-        defn defn-llvm defn-java defn-haskell \
+        defn defn-llvm defn-haskell \
         definition-deps wasm-definitions eei-definitions \
-        build build-llvm build-java build-haskell \
-        test test-execution test-simple test-prove test-klab-prove \
+        build build-llvm build-haskell \
+        test test-execution test-simple test-prove \
         media presentations reports
 
 all: build
@@ -52,12 +52,10 @@ deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definitio
 definition-deps: wasm-definitions eei-definitions
 
 wasm-definitions:
-	$(wasm_make) -B defn-java
 	$(wasm_make) -B defn-llvm
 	$(wasm_make) -B defn-haskell
 
 eei-definitions: $(eei_source_files)
-	$(eei_make) -B defn-java
 	$(eei_make) -B defn-llvm
 	$(eei_make) -B defn-haskell
 
@@ -77,10 +75,6 @@ llvm_dir:=$(defn_dir)/llvm
 llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files))
 llvm_kompiled:=$(llvm_dir)/ewasm-test-kompiled/interpreter
 
-java_dir:=$(defn_dir)/java
-java_defn:=$(patsubst %, $(java_dir)/%, $(all_k_files))
-java_kompiled:=$(java_dir)/ewasm-test-kompiled/compiled.txt
-
 haskell_dir:=$(defn_dir)/haskell
 haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files))
 haskell_kompiled:=$(haskell_dir)/ewasm-test-kompiled/definition.kore
@@ -90,21 +84,15 @@ syntax_module=EWASM-TEST-SYNTAX
 
 # Tangle definition from *.md files
 
-defn: defn-llvm defn-java defn-haskell
+defn: defn-llvm defn-haskell
 defn-llvm: $(llvm_defn)
-defn-java: $(java_defn)
 defn-haskell: $(haskell_defn)
 
 $(llvm_dir)/%.k: %.md $(tangler)
 	@echo "==  tangle: $@"
 	mkdir -p $(dir $@)
 	pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@
 
-$(java_dir)/%.k: %.md $(tangler)
-	@echo "==  tangle: $@"
-	mkdir -p $(dir $@)
-	pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@
-
 $(haskell_dir)/%.k: %.md $(tangler)
 	@echo "==  tangle: $@"
 	mkdir -p $(dir $@)
@@ -114,9 +102,8 @@ $(haskell_dir)/%.k: %.md $(tangler)
 
 KOMPILE_OPTS :=
 
-build: build-llvm build-java build-haskell
+build: build-llvm build-haskell
 build-llvm: $(llvm_kompiled)
-build-java: $(java_kompiled)
 build-haskell: $(haskell_kompiled)
 
 $(llvm_kompiled): $(llvm_defn)
@@ -127,14 +114,6 @@ $(llvm_kompiled): $(llvm_defn)
 	    --syntax-module $(syntax_module) $<    \
 	    $(KOMPILE_OPTS)
 
-$(java_kompiled): $(java_defn)
-	@echo "== kompile: $@"
-	$(k_bin)/kompile --backend java            \
-	    --directory $(java_dir) -I $(java_dir) \
-	    --main-module   $(main_module)         \
-	    --syntax-module $(syntax_module) $<    \
-	    $(KOMPILE_OPTS)
-
 $(haskell_kompiled): $(haskell_defn)
 	@echo "== kompile: $@"
 	$(k_bin)/kompile --backend haskell               \
@@ -150,6 +129,7 @@ TEST_CONCRETE_BACKEND:=llvm
 TEST_SYMBOLIC_BACKEND:=haskell
 TEST:=./kewasm
 KPROVE_MODULE:=KEWASM-LEMMAS
+KPROVE_OPTS:=
 CHECK:=git --no-pager diff --no-index --ignore-all-space
 
 tests/proofs/wrc20-do-balance-spec.k.prove: KPROVE_MODULE=VERIFICATION
@@ -177,10 +157,7 @@ tests/%.parse: tests/%
 	rm -rf $@-out
 
 tests/%.prove: tests/%
-	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)
-
-tests/%.klab-prove: tests/%
-	$(TEST) klab-prove --backend $(TEST_SYMBOLIC_BACKEND) $< --format-failures --def-module $(KPROVE_MODULE)
+	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS))
 
 ### Execution Tests
 
@@ -197,6 +174,3 @@ quick_proof_tests:=$(filter-out $(slow_proof_tests), $(proof_tests))
 
 test-prove: $(proof_tests:=.prove)
 
-### KLab interactive
-
-test-klab-prove: $(quick_proof_tests:=.klab-prove)

README.md

@@ -10,12 +10,33 @@ K Semantics of Ewasm
 
 Prototype semantics of [Ewasm](https://github.com/ewasm/design) in the K framework.
 
-```
+```sh
 git submodule update --init --recursive
 make deps
 make build
 ```
 
+# Proving
+
+Run existing proofs using `make` rules.
+
+```sh
+make tests/proofs/example-spec.k.prove
+make tests/proofs/example-spec.k.repl
+```
+
+You can run the prover on your own specification, with a lemmas module of your choice.
+
+```sh
+./kewasm prove <path>/<to>/<spec> -m <LEMMAS-MODULE>  # Runs the prover on the given spec, using LEMMAS-MODULE as the top-level sematics module.
+```
+
+You can add the `--repl` flag to run the proof in an interactive REPL, where you can step through the proof and explore its branches.
+
+```sh
+./kewasm prove <path>/<to>/<spec> -m <LEMMAS-MODULE>  # Runs the prover on the given spec, using LEMMAS-MODULE as the top-level sematics module.
+```
+
 # Structure
 
 This project makes use of the K framework [EEI](https://github.com/kframework/eei-semantics) and [Wasm](https://github.com/kframework/wasm-semantics) semantics.

deps/wasm-semantics

@@ -0,0 +1,8 @@
+alias kclaim x   = claim x  | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias kaxiom x   = axiom x  | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias konfig     = config   | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias konfig-n x = config x | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias ktry x     = try x    | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias ktryf x    = tryf x   | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias krule      = rule     | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin
+alias krule-n x  = rule x   | kast -i kore -o pretty -d .build/defn/haskell /dev/stdin

kast.kscript

@@ -8,6 +8,7 @@ wasm_dir="${WASM_DIR:-$ewasm_dir/deps/wasm-semantics}"
 build_dir="$ewasm_dir/.build"
 defn_dir="$build_dir/defn"
 lib_dir="$build_dir/local/lib"
+haskell_backend_dir="$wasm_dir/deps/k/haskell-backend/src/main/native/haskell-backend"
 k_release_dir="${K_RELEASE:-$wasm_dir/deps/k/k-distribution/target/release/k}"
 
 export PATH="$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH"
@@ -17,10 +18,6 @@ test_logs="$build_dir/logs"
 mkdir -p "$test_logs"
 test_log="$test_logs/tests.log"
 
-KLAB_OUT="${KLAB_OUT:-$build_dir/klab}"
-KLAB_NODE_STACK_SIZE="${KLAB_NODE_STACK_SIZE:-30000}"
-export KLAB_OUT
-
 # Utilities
 # ---------
 
@@ -53,60 +50,31 @@ run_kast() {
 
 run_prove() {
     export K_OPTS=-Xmx8G
-    kprove --directory "$backend_dir" "$run_file" "$@"
-}
-
-run_klab() {
-    local run_mode klab_log
-
-    run_mode="$1" ; shift
-    klab_log="$(basename "${run_file%-spec.k}")"
-
-    "$0" "$run_mode" --backend java "$run_file" \
-        --state-log --state-log-path "$KLAB_OUT/data" --state-log-id "$klab_log" \
-        --state-log-events OPEN,EXECINIT,SEARCHINIT,REACHINIT,REACHTARGET,REACHPROVED,NODE,RULE,SRULE,RULEATTEMPT,IMPLICATION,Z3QUERY,Z3RESULT,CLOSE \
-        --output-flatten "_Map_ #And" \
-        --output-tokenize "listStmt listValTypes <_>_ i32_WASM-DATA i64_WASM-DATA _:__WASM-DATA" \
-        --no-alpha-renaming --restore-original-names --no-sort-collections \
-        --output json \
-        "$@"
-}
-
-view_klab() {
-    local klab_log
-
-    klab_log="$(basename "${run_file%-spec.k}")"
-
-    # klab often runs out of stack space when running long-running KWasm programs
-    # klab debug "$klab_log"
-    node --stack-size=$KLAB_NODE_STACK_SIZE $(dirname $(which klab))/../libexec/klab-debug "$klab_log"
+    haskell_backend_command="$k_release_dir/bin/kore-exec"
+    if $repl; then
+        haskell_backend_command="$k_release_dir/bin/kore-repl --repl-script $ewasm_dir/kast.kscript"
+    fi
+    kprove --directory "$backend_dir" "$run_file" "$@" --haskell-backend-command "$haskell_backend_command"
 }
 
 # Main
 # ----
 
 usage() {
     echo "
-    usage: $0 run        [--backend (llvm|java|haskell)] <pgm>  <K args>*
-           $0 kast       [--backend (llvm|java)]         <pgm>  <output format> <K args>*
-           $0 prove      [--backend (java|haskell)]       <spec> <K args>* -m <def_module>
-           $0 klab-run                                    <pgm>  <K arg>*
-           $0 klab-prove                                  <spec> <K arg>* -m <def_module>
-           $0 klab-view                                   [<pgm>|<spec>]
+    usage: $0 run        [--backend (llvm|haskell)]      <pgm>  <K args>*
+           $0 kast       [--backend (llvm)]              <pgm>  <output format> <K args>*
+           $0 prove      [--backend (haskell)] [--repl]  <spec> <K args>* -m <def_module>
 
        $0 run   : Run a single WebAssembly program
        $0 kast  : Parse a single WebAssembly program and output it in supported format
        $0 prove : Run a WebAssembly K proof
-       $0 klab-(run|prove) : Run or prove a spec and dump StateLogs which KLab can read
-       $0 klab-view : Launch KLab on the StateLog associated with the given program/spec.
 
-       Note: <pgm> is a path to a file containing a WebAssembly program.
+       Note: <pgm> is a path to a file containing a EWasm program.
              <spec> is a K specification to be proved.
              <K args> are any arguments you want to pass to K when executing/proving.
              <output format> is the format for Kast to output the term in.
              <def_module> is the module to take as axioms for verification.
-
-       KLab: Make sure that the 'klab/bin' directory is on your PATH to use this option.
 "
 }
 
@@ -126,25 +94,30 @@ run_command="$1"; shift
 [[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to work on."
 
 backend="llvm"
+repl=false
 [[ ! "$run_command" == 'prove' ]] || backend='haskell'
-[[ ! "$run_command" =~ klab*   ]] || backend='java'
-if [[ $# -gt 1 ]] && [[ $1 == '--backend' ]] || [[ $1 == '--definition' ]]; then
-    backend="${2#wasm-}"
-    shift 2
-fi
+args=()
+while [[ $# -gt 0 ]]; do
+    arg="$1"
+    case $arg in
+        --backend)    args+=("$arg" "$2") ; backend="$2"      ; shift 2 ;;
+        --repl)       args+=("$arg")      ; repl=true         ; shift   ;;
+        *)            break                                             ;;
+    esac
+done
+
+! $repl || [[ "$backend" == "haskell" ]] || fatal "REPL option only available for Haskell backend."
+
 backend_dir="$defn_dir/$backend"
-[[ ! "$backend" == "llvm" ]] || eval $(opam config env)
 
 # get the run file
 [[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to run on."
 run_file="$1" ; shift
 [[ -f "$run_file" ]] || fatal "File does not exist: $run_file"
 
 case "$run_command-$backend" in
-    run-@(llvm|java|haskell)  ) run_krun                        "$@" ;;
-    kast-@(llvm|java)         ) run_kast                        "$@" ;;
-    prove-@(java|haskell)      ) run_prove                       "$@" ;;
-    klab-@(run|prove)-java     ) run_klab "${run_command#klab-}" "$@" ;;
-    klab-view-java             ) view_klab                       "$@" ;;
+    run-@(llvm|haskell)  ) run_krun                        "$@" ;;
+    kast-llvm            ) run_kast                        "$@" ;;
+    prove-haskell        ) run_prove                       "$@" ;;
     *) usage_fatal "Unknown command on '$backend' backend: $run_command" ;;
 esac