Update dependency: deps/wasm-semantics

Jenkinsfile

@@ -11,7 +11,6 @@ pipeline {
       when { changeRequest() }
       steps { script { currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}" } }
     }
-    stage('Definition Deps') { steps { sh 'make definition-deps -j4' } }
     stage('Build')           { steps { sh 'make build -j4'           } }
     stage('Test') {
       options { timeout(time: 15, unit: 'MINUTES') }

Makefile

@@ -1,10 +1,13 @@
 # Settings
 # --------
 
-deps_dir       := deps
-wasm_submodule := $(deps_dir)/wasm-semantics
-eei_submodule  := $(deps_dir)/eei-semantics
-k_submodule    := $(wasm_submodule)/deps/k
+BUILD_DIR := .build
+DEPS_DIR  := deps
+DEFN_DIR  := $(BUILD_DIR)/defn
+
+KWASM_SUBMODULE := $(DEPS_DIR)/wasm-semantics
+EEI_SUBMODULE   := $(DEPS_DIR)/eei-semantics
+k_submodule     := $(KWASM_SUBMODULE)/deps/k
 
 ifneq (,$(wildcard $(k_submodule)/k-distribution/target/release/k/bin/*))
     K_RELEASE ?= $(abspath $(k_submodule)/k-distribution/target/release/k)
@@ -15,123 +18,69 @@ K_BIN := $(K_RELEASE)/bin
 K_LIB := $(K_RELEASE)/lib/kframework
 export K_RELEASE
 
-PATH:=$(K_BIN):$(abspath $(wasm_submodule)):$(PATH)
+PATH:=$(K_BIN):$(abspath $(KWASM_SUBMODULE)):$(PATH)
 export PATH
 
-build_dir         := .build
-defn_dir          := $(build_dir)/defn
-kompiled_dir_name := ewasm-test
-
-wasm_make := make --directory $(wasm_submodule) DEFN_DIR=../../$(defn_dir)
-eei_make  := make --directory $(eei_submodule)  DEFN_DIR=../../$(defn_dir)
 
-pandoc_tangle_submodule := $(wasm_submodule)/deps/pandoc-tangle
-tangler                 := $(pandoc_tangle_submodule)/tangle.lua
-LUA_PATH                := $(pandoc_tangle_submodule)/?.lua;;
-export LUA_PATH
+KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE)
 
-.PHONY: all clean \
-        deps haskell-deps \
-        defn defn-llvm defn-haskell \
-        definition-deps wasm-definitions eei-definitions \
-        build build-llvm build-haskell \
-        test test-execution test-simple test-prove \
+.PHONY: all clean deps                  \
+        build                           \
+        test test-execution test-simple \
+        test-prove                      \
         media presentations reports
 
 all: build
 
 clean:
-	rm -rf $(build_dir)
-	rm -f $(wasm_submodule)/make.timestamp
-	rm -f $(eei_submodule)/make.timestamp
+	rm -rf $(BUILD_DIR)
 	git submodule update --init --recursive
-	$(MAKE) clean -C $(wasm_submodule)
-	$(MAKE) clean -C $(eei_submodule)
+	$(MAKE) clean -C $(KWASM_SUBMODULE)
+	$(MAKE) clean -C $(EEI_SUBMODULE)
 
 # Build Dependencies (K Submodule)
 # --------------------------------
 
-wasm_files=test.k wasm.k data.k kwasm-lemmas.k
-wasm_source_files:=$(patsubst %, $(wasm_submodule)/%, $(patsubst %.k, %.md, $(wasm_files)))
-eei_files:=eei.k
-eei_source_files:=$(patsubst %, $(eei_submodule)/%, $(patsubst %.k, %.md, $(eei_files)))
-ewasm_files:=ewasm-test.k driver.k ewasm.k kewasm-lemmas.k
-all_k_files:=$(ewasm_files) $(wasm_files) $(eei_files)
-
-deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definition-deps
-
-definition-deps: wasm-definitions eei-definitions
-
-wasm-definitions:
-	$(wasm_make) -B defn-llvm
-	$(wasm_make) -B defn-haskell
+EEI_FILES:=eei.md
+EEI_SOURCE_FILES:=$(patsubst %, $(EEI_SUBMODULE)/%, $(EEI_FILES))
+EWASM_FILES:=ewasm-test.md driver.md ewasm.md kewasm-lemmas.md
+EWASM_SOURCE_FILES:=$(EWASM_FILES)
+EXTRA_FILES:=$(EEI_FILES) $(EWASM_FILES)
+EXTRA_SOURCE_FILES:=$(patsubst %, $(KWASM_SUBMODULE)/%, $(EXTRA_FILES))
 
-eei-definitions: $(eei_source_files)
-	$(eei_make) -B defn-llvm
-	$(eei_make) -B defn-haskell
-
-$(wasm_submodule)/make.timestamp: $(wasm_source_files)
-	git submodule update --init --recursive
-	$(wasm_make) deps
-	touch $(wasm_submodule)/make.timestamp
-
-$(eei_submodule)/make.timestamp: $(eei_source_files)
-	git submodule update --init --recursive
-	touch $(eei_submodule)/make.timestamp
+deps:
+	$(KWASM_MAKE) deps
 
 # Building Definition
 # -------------------
 
-llvm_dir:=$(defn_dir)/llvm
-llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files))
-llvm_kompiled:=$(llvm_dir)/ewasm-test-kompiled/interpreter
-
-haskell_dir:=$(defn_dir)/haskell
-haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files))
-haskell_kompiled:=$(haskell_dir)/ewasm-test-kompiled/definition.kore
-
-main_module=EWASM-TEST
-syntax_module=EWASM-TEST-SYNTAX
-
-# Tangle definition from *.md files
-
-defn: defn-llvm defn-haskell
-defn-llvm: $(llvm_defn)
-defn-haskell: $(haskell_defn)
-
-$(llvm_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 $@)
-	pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@
+MAIN_MODULE=EWASM-TEST
+MAIN_SYNTAX_MODULE=EWASM-TEST-SYNTAX
+MAIN_DEFN_FILE=ewasm-test
 
 # Build definitions
 
 KOMPILE_OPTS :=
 
 build: build-llvm build-haskell
-build-llvm: $(llvm_kompiled)
-build-haskell: $(haskell_kompiled)
-
-$(llvm_kompiled): $(llvm_defn)
-	@echo "== kompile: $@"
-	kompile --backend llvm                     \
-	    --directory $(llvm_dir) -I $(llvm_dir) \
-	    --main-module $(main_module)           \
-	    --syntax-module $(syntax_module) $<    \
-	    $(KOMPILE_OPTS)
-
-$(haskell_kompiled): $(haskell_defn)
-	@echo "== kompile: $@"
-	kompile --backend haskell                        \
-	    --directory $(haskell_dir) -I $(haskell_dir) \
-	    --main-module   $(main_module)               \
-	    --syntax-module $(syntax_module) $<          \
-	    $(KOMPILE_OPTS)
+
+build-%: $(EXTRA_SOURCE_FILES)
+	$(KWASM_MAKE) build-$*                           \
+	    DEFN_DIR=../../$(DEFN_DIR)                   \
+	    llvm_main_module=$(MAIN_MODULE)              \
+	    llvm_syntax_module=$(MAIN_SYNTAX_MODULE)     \
+	    llvm_main_file=$(MAIN_DEFN_FILE)             \
+	    haskell_main_module=$(MAIN_MODULE)           \
+	    haskell_syntax_module=$(MAIN_SYNTAX_MODULE)  \
+	    haskell_main_file=$(MAIN_DEFN_FILE)          \
+	    EXTRA_SOURCE_FILES="$(EXTRA_FILES)"          \
+	    KOMPILE_OPTS="$(KOMPILE_OPTS)"
+
+$(KWASM_SUBMODULE)/%.md: %.md
+	cp $< $@
+
+$(KWASM_SUBMODULE)/%.md: $(EEI_SUBMODULE)/%.md
+	cp $< $@
 
 # Testing
 # -------
@@ -140,14 +89,10 @@ TEST_CONCRETE_BACKEND:=llvm
 TEST_SYMBOLIC_BACKEND:=haskell
 TEST:=./kewasm
 KPROVE_MODULE:=KEWASM-LEMMAS
+KPROVE_MODULE_FILE=kewasm-lemmas.md
 KPROVE_OPTS:=
 CHECK:=git --no-pager diff --no-index --ignore-all-space
 
-tests/%/make.timestamp:
-	@echo "== submodule: $@"
-	git submodule update --init -- tests/$*
-	touch $@
-
 test: test-execution test-prove
 
 # Generic Test Harnesses
@@ -165,7 +110,7 @@ tests/%.parse: tests/%
 	$(CHECK) $@-expected $@-out
 	rm -rf $@-out
 
-tests/%.prove: tests/%
+tests/%.prove: tests/% $(KWASM_SUBMODULE)/$(KPROVE_MODULE_FILE)
 	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS))
 
 ### Execution Tests

driver.md

@@ -2,17 +2,19 @@ Ethereum Simulation
 ===================
 
 ```k
-require "ewasm.k"
-require "data.k"
+require "wasm-text.md"
+require "ewasm.md"
+require "data.md"
 
 module DRIVER-SYNTAX
     imports EWASM-SYNTAX
-    imports WASM-SYNTAX
+    imports WASM-TEXT-SYNTAX
     imports DRIVER
 endmodule
 
 module DRIVER
     imports EWASM
+    imports WASM-TEXT
 ```
 
 An Ewasm program is the invocation of an Ethereum contract containing Ewasm code.
@@ -111,7 +113,7 @@ Setting up the blockchain state
 ```k
     syntax EthereumCommand ::= "#createContract" CallData ModuleDecl
  // ----------------------------------------------------------------
-    rule <k> #createContract ADDRESS CODE => CODE ~> #storeModuleAt CallData2Int(ADDRESS) ... </k>
+    rule <k> #createContract ADDRESS CODE => text2abstract(CODE .Stmts) ~> #storeModuleAt CallData2Int(ADDRESS) ... </k>
 
     syntax EthereumCommand ::= "#storeModuleAt" CallData
  // ----------------------------------------------------

ewasm-test.md

@@ -4,8 +4,8 @@ Testing
 We make use of the testing module for Wasm, which will let us make assertions about the Wasm runtime state.
 
 ```k
-requires "test.k" // WASM-TEST
-requires "driver.k"
+requires "test.md" // WASM-TEST
+requires "driver.md"
 
 module EWASM-TEST-SYNTAX
    imports WASM-TEST-SYNTAX

ewasm.md

@@ -2,11 +2,11 @@ Ewasm Specification
 =================
 
 ```k
-require "wasm.k"
-require "eei.k"
+require "wasm.md"
+require "eei.md"
 
 module EWASM-SYNTAX
-    imports WASM-TOKEN-SYNTAX
+    imports WASM-SYNTAX
     imports EWASM
 endmodule
 ```
@@ -72,7 +72,7 @@ Then, when a `HostCall` instruction is encountered, parameters are gathered from
 
 ```k
     rule <k> ( import MODNAME FNAME (func OID:OptionalId TUSE:TypeUse) )
-          => ( func OID TUSE .LocalDecls #eeiFunction(FNAME) .Instrs )
+          => #func(... type: TUSE, locals: .LocalDecls, body: #eeiFunction(FNAME) .Instrs, metadata: #meta(... id: OID, localIds: .Map))
          ...
          </k>
       requires MODNAME ==K #ethereumModule

kewasm-lemmas.md

@@ -5,8 +5,7 @@ These lemmas aid in verifying Ewasm programs behavior.
 They are part of the *trusted* base, and so should be scrutinized carefully.
 
 ```k
-requires "kwasm-lemmas.k"
-requires "kewasm-lemmas.k"
+requires "kwasm-lemmas.md"
 
 module KEWASM-LEMMAS
   imports EWASM-TEST

tests/proofs/invoke-contract-spec.k

@@ -1,4 +1,4 @@
-requires "kewasm-lemmas.k"
+requires "kewasm-lemmas.md"
 
 module INVOKE-CONTRACT-SPEC
   imports KEWASM-LEMMAS
@@ -58,8 +58,5 @@ module INVOKE-CONTRACT-SPEC
          </nextMemAddr>
          ...
        </mainStore>
-       <nextFreshId>
-           0 => ?_
-       </nextFreshId>
 
 endmodule

tests/success-llvm.out

@@ -143,9 +143,6 @@
     <deterministicMemoryGrowth>
       true
     </deterministicMemoryGrowth>
-    <nextFreshId>
-      0
-    </nextFreshId>
   </wasm>
   <paramstack>
     .ParamStack