From 75b62896a22179a392bb4c92ee431bc509ad1f6d Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Fri, 29 May 2020 07:08:17 +0000 Subject: [PATCH 01/38] deps/wasm-semantics: 2c4f62c - Update dependency: deps/k (#348) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index a959393..2c4f62c 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit a95939358242fd7050c0a94b606d04c1cb1e8fea +Subproject commit 2c4f62c49003b2db0bd4094fc230b505155b507c From a9b8beef87b6823ac1e5b400463284d2650ed443 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Sat, 30 May 2020 07:23:30 +0000 Subject: [PATCH 02/38] deps/wasm-semantics: 6941fb6 - Unfold definitions (#345) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 2c4f62c..6941fb6 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 2c4f62c49003b2db0bd4094fc230b505155b507c +Subproject commit 6941fb696099b69f21c713222300d197fee83724 From 3660fd1b50f9a0e479f0dddb02c2a6b11073a1aa Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 16:21:09 +0000 Subject: [PATCH 03/38] Preprocess modules in driver --- Makefile | 2 +- driver.md | 3 +-- ewasm.md | 4 ++-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 41f219d..5d1d86c 100644 --- a/Makefile +++ b/Makefile @@ -51,7 +51,7 @@ clean: # Build Dependencies (K Submodule) # -------------------------------- -wasm_files=test.k wasm.k data.k kwasm-lemmas.k +wasm_files=test.k wasm.k wasm-text.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))) diff --git a/driver.md b/driver.md index 1c7e069..966bfad 100644 --- a/driver.md +++ b/driver.md @@ -7,7 +7,6 @@ require "data.k" module DRIVER-SYNTAX imports EWASM-SYNTAX - imports WASM-SYNTAX imports DRIVER endmodule @@ -111,7 +110,7 @@ Setting up the blockchain state ```k syntax EthereumCommand ::= "#createContract" CallData ModuleDecl // ---------------------------------------------------------------- - rule #createContract ADDRESS CODE => CODE ~> #storeModuleAt CallData2Int(ADDRESS) ... + rule #createContract ADDRESS CODE => text2abstract(CODE .Stmts) ~> #storeModuleAt CallData2Int(ADDRESS) ... syntax EthereumCommand ::= "#storeModuleAt" CallData // ---------------------------------------------------- diff --git a/ewasm.md b/ewasm.md index c3fb81a..ba8dc5c 100644 --- a/ewasm.md +++ b/ewasm.md @@ -6,7 +6,7 @@ require "wasm.k" require "eei.k" module EWASM-SYNTAX - imports WASM-TOKEN-SYNTAX + imports WASM-TEXT-SYNTAX imports EWASM endmodule ``` @@ -19,7 +19,7 @@ Ewasm consists of a WebAssembly (Wasm) semantics, and an Ethereum Environment In ```k imports EEI - imports WASM + imports WASM-TEXT ``` The configuration composes both the top level cells of the Wasm and EEI semantics. From b1041945bcc6649161b75ee6c636888b28f77251 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 16:49:55 +0000 Subject: [PATCH 04/38] success-llvm: remove nextFreshId --- tests/success-llvm.out | 3 --- 1 file changed, 3 deletions(-) diff --git a/tests/success-llvm.out b/tests/success-llvm.out index 5969a42..e2e0683 100644 --- a/tests/success-llvm.out +++ b/tests/success-llvm.out @@ -143,9 +143,6 @@ true - - 0 - .ParamStack From 3af12477b88379a1fcaa5edd484a5a6874d3f7bc Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 16:56:08 +0000 Subject: [PATCH 05/38] proofs: remove nextFreshId --- tests/proofs/invoke-contract-spec.k | 3 --- 1 file changed, 3 deletions(-) diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index c956858..472e012 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -58,8 +58,5 @@ module INVOKE-CONTRACT-SPEC ... - - 0 => ?_ - endmodule From 60826debe4bbd208eae89f5e5f222f955fe3fac0 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Mon, 1 Jun 2020 13:23:52 +0000 Subject: [PATCH 06/38] deps/wasm-semantics: 60895c3 - kwasm-lemmas: use upstreamed integer symbolic reasoning (#350) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 6941fb6..60895c3 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 6941fb696099b69f21c713222300d197fee83724 +Subproject commit 60895c32c96f87ce16b6a096c2a42f08446be815 From 5ad1a2cc0d1098279ee696f99036a831677d94cc Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Thu, 4 Jun 2020 14:57:48 +0000 Subject: [PATCH 07/38] deps/wasm-semantics: 05d42eb - Standardize Makefile (#351) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 60895c3..05d42eb 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 60895c32c96f87ce16b6a096c2a42f08446be815 +Subproject commit 05d42eb7e38dc74e43409e10ab199414108f3dd1 From 9f101d342d61d54faae408915e7485b8c6bf0052 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Fri, 5 Jun 2020 14:53:28 +0000 Subject: [PATCH 08/38] deps/wasm-semantics: ea521a7 - Sort text module (#349) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 05d42eb..ea521a7 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 05d42eb7e38dc74e43409e10ab199414108f3dd1 +Subproject commit ea521a77c1c127846e3a757c291c9d41e0045571 From fec3c63ec648dbd8f420e0800484bb3be1512cf0 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Sat, 6 Jun 2020 13:23:31 +0000 Subject: [PATCH 09/38] deps/wasm-semantics: 9d7bb2c - Remove contextlookup for functions (#355) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index ea521a7..9d7bb2c 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit ea521a77c1c127846e3a757c291c9d41e0045571 +Subproject commit 9d7bb2c1b587c58b05b3422487366e966b389200 From 4cdf82e4d3bccfe0176e8d75657f1ef76a5b5566 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 9 Jun 2020 12:53:51 +0000 Subject: [PATCH 10/38] deps/wasm-semantics: d944601 - Remove named valtypes (#356) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 9d7bb2c..d944601 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 9d7bb2c1b587c58b05b3422487366e966b389200 +Subproject commit d944601658d863a142ceab9f5385f733c6e81e07 From 40abea861b31615f284eb469a22eb9c3f390bf97 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 10 Jun 2020 15:52:55 +0000 Subject: [PATCH 11/38] deps/wasm-semantics: 435e43f - Module metadata (#357) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index d944601..435e43f 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit d944601658d863a142ceab9f5385f733c6e81e07 +Subproject commit 435e43ff8760fb9e25475848ebb25c76fb1a35d2 From 7e2ac62567bdb4fa516d428ac3b509b04f1c4747 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Thu, 11 Jun 2020 11:53:17 +0000 Subject: [PATCH 12/38] deps/wasm-semantics: 08042d9 - Use native md file support from K (#358) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 435e43f..08042d9 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 435e43ff8760fb9e25475848ebb25c76fb1a35d2 +Subproject commit 08042d993316397a165486484ea34ec177396340 From 8e0355fc6bd460baa72fc2851776f65b4d519ab9 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Fri, 12 Jun 2020 19:24:33 +0000 Subject: [PATCH 13/38] deps/wasm-semantics: 8794dd4 - Fix typo (`eq` instead of `ne`) (#359) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 08042d9..8794dd4 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 08042d993316397a165486484ea34ec177396340 +Subproject commit 8794dd41faf968e434f9e634c1c5be27631163ab From e7e4c3c3035599c36a4c72c509c3de7dc6879eab Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 22:24:55 +0000 Subject: [PATCH 14/38] Update Makefile for native Markdown support --- Makefile | 116 +++++++++++----------------- driver.md | 4 +- ewasm-test.md | 4 +- ewasm.md | 4 +- kewasm-lemmas.md | 3 +- tests/proofs/invoke-contract-spec.k | 2 +- 6 files changed, 54 insertions(+), 79 deletions(-) diff --git a/Makefile b/Makefile index 5d1d86c..43a3f9c 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ # Settings # -------- -deps_dir := deps -wasm_submodule := $(deps_dir)/wasm-semantics -eei_submodule := $(deps_dir)/eei-semantics -k_submodule := $(wasm_submodule)/deps/k +deps_dir := deps +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,17 +15,17 @@ 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 +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) +KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) +eei_make := make --directory $(eei_submodule) DEFN_DIR=../../$(DEFN_DIR) -pandoc_tangle_submodule := $(wasm_submodule)/deps/pandoc-tangle +pandoc_tangle_submodule := $(KWASM_SUBMODULE)/deps/pandoc-tangle tangler := $(pandoc_tangle_submodule)/tangle.lua LUA_PATH := $(pandoc_tangle_submodule)/?.lua;; export LUA_PATH @@ -34,7 +34,7 @@ export LUA_PATH deps haskell-deps \ defn defn-llvm defn-haskell \ definition-deps wasm-definitions eei-definitions \ - build build-llvm build-haskell \ + build \ test test-execution test-simple test-prove \ media presentations reports @@ -42,96 +42,72 @@ all: build clean: rm -rf $(build_dir) - rm -f $(wasm_submodule)/make.timestamp + rm -f $(KWASM_SUBMODULE)/make.timestamp rm -f $(eei_submodule)/make.timestamp git submodule update --init --recursive - $(MAKE) clean -C $(wasm_submodule) + $(MAKE) clean -C $(KWASM_SUBMODULE) $(MAKE) clean -C $(eei_submodule) # Build Dependencies (K Submodule) # -------------------------------- -wasm_files=test.k wasm.k wasm-text.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 +wasm_files=test.md wasm.md wasm-text.md data.md kwasm-lemmas.md +wasm_source_files:=$(patsubst %, $(KWASM_SUBMODULE)/%, $(wasm_files)) +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) all_k_files:=$(ewasm_files) $(wasm_files) $(eei_files) -deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definition-deps +llvm_dir:=$(DEFN_DIR)/llvm +llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files)) + +haskell_dir:=$(DEFN_DIR)/haskell +haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files)) -definition-deps: wasm-definitions eei-definitions +definition-deps: eei-definitions +deps: $(KWASM_SUBMODULE)/make.timestamp $(eei_submodule)/make.timestamp definition-deps wasm-definitions: - $(wasm_make) -B defn-llvm - $(wasm_make) -B defn-haskell + $(KWASM_MAKE) -B defn-llvm + $(KWASM_MAKE) -B defn-haskell 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 +$(KWASM_SUBMODULE)/make.timestamp: $(wasm_source_files) + $(KWASM_MAKE) deps + touch $(KWASM_SUBMODULE)/make.timestamp $(eei_submodule)/make.timestamp: $(eei_source_files) - git submodule update --init --recursive touch $(eei_submodule)/make.timestamp # 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-%: + cp $(eei_source_files) $(ewasm_source_files) $(KWASM_SUBMODULE) + $(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="$(eei_files) $(ewasm_files)" \ + KOMPILE_OPTS="$(KOMPILE_OPTS)" # Testing # ------- diff --git a/driver.md b/driver.md index 966bfad..b3b4a7e 100644 --- a/driver.md +++ b/driver.md @@ -2,8 +2,8 @@ Ethereum Simulation =================== ```k -require "ewasm.k" -require "data.k" +require "ewasm.md" +require "data.md" module DRIVER-SYNTAX imports EWASM-SYNTAX diff --git a/ewasm-test.md b/ewasm-test.md index afb0f12..a724d2f 100644 --- a/ewasm-test.md +++ b/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 diff --git a/ewasm.md b/ewasm.md index ba8dc5c..0a60c6a 100644 --- a/ewasm.md +++ b/ewasm.md @@ -2,8 +2,8 @@ Ewasm Specification ================= ```k -require "wasm.k" -require "eei.k" +require "wasm.md" +require "eei.md" module EWASM-SYNTAX imports WASM-TEXT-SYNTAX diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index b1fa300..89d0b1f 100644 --- a/kewasm-lemmas.md +++ b/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 diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index 472e012..1face3c 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/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 From 9eb40fbf65dd7a1c286f61c859fcf45bdb246d90 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 22:33:01 +0000 Subject: [PATCH 15/38] ewasm: bugfix: correct file import --- ewasm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ewasm.md b/ewasm.md index 0a60c6a..bad670c 100644 --- a/ewasm.md +++ b/ewasm.md @@ -2,7 +2,7 @@ Ewasm Specification ================= ```k -require "wasm.md" +require "wasm-text.md" require "eei.md" module EWASM-SYNTAX From e3609a08dfc041af2afd3bd851cfc087e188e2da Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 22:41:49 +0000 Subject: [PATCH 16/38] Use new core func type --- ewasm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ewasm.md b/ewasm.md index bad670c..d5cd51a 100644 --- a/ewasm.md +++ b/ewasm.md @@ -72,7 +72,7 @@ Then, when a `HostCall` instruction is encountered, parameters are gathered from ```k rule ( 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)) ... requires MODNAME ==K #ethereumModule From de5f4dac40fada731f7aeb457438f7dbc10cab97 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 22:44:09 +0000 Subject: [PATCH 17/38] Only import WASM-TEXT in DRIVER, not in EWASM --- driver.md | 3 +++ ewasm.md | 6 +++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/driver.md b/driver.md index b3b4a7e..28b4471 100644 --- a/driver.md +++ b/driver.md @@ -2,16 +2,19 @@ Ethereum Simulation =================== ```k +require "wasm-text.md" require "ewasm.md" require "data.md" module DRIVER-SYNTAX imports EWASM-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. diff --git a/ewasm.md b/ewasm.md index d5cd51a..1e34c25 100644 --- a/ewasm.md +++ b/ewasm.md @@ -2,11 +2,11 @@ Ewasm Specification ================= ```k -require "wasm-text.md" +require "wasm.md" require "eei.md" module EWASM-SYNTAX - imports WASM-TEXT-SYNTAX + imports WASM-SYNTAX imports EWASM endmodule ``` @@ -19,7 +19,7 @@ Ewasm consists of a WebAssembly (Wasm) semantics, and an Ethereum Environment In ```k imports EEI - imports WASM-TEXT + imports WASM ``` The configuration composes both the top level cells of the Wasm and EEI semantics. From 5eb24130810c13331823915f5c67c33156b1480f Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 22:59:51 +0000 Subject: [PATCH 18/38] Makefile cleanup --- Makefile | 56 ++++++++++++-------------------------------------------- 1 file changed, 12 insertions(+), 44 deletions(-) diff --git a/Makefile b/Makefile index 43a3f9c..a25a05c 100644 --- a/Makefile +++ b/Makefile @@ -1,9 +1,9 @@ # Settings # -------- -deps_dir := deps -KWASM_SUBMODULE := $(deps_dir)/wasm-semantics -eei_submodule := $(deps_dir)/eei-semantics +DEPS_DIR := deps +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/*)) @@ -23,18 +23,9 @@ DEFN_DIR := $(build_dir)/defn kompiled_dir_name := ewasm-test KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) -eei_make := make --directory $(eei_submodule) DEFN_DIR=../../$(DEFN_DIR) - -pandoc_tangle_submodule := $(KWASM_SUBMODULE)/deps/pandoc-tangle -tangler := $(pandoc_tangle_submodule)/tangle.lua -LUA_PATH := $(pandoc_tangle_submodule)/?.lua;; -export LUA_PATH .PHONY: all clean \ - deps haskell-deps \ - defn defn-llvm defn-haskell \ - definition-deps wasm-definitions eei-definitions \ - build \ + deps defn build \ test test-execution test-simple test-prove \ media presentations reports @@ -43,6 +34,7 @@ all: build clean: rm -rf $(build_dir) rm -f $(KWASM_SUBMODULE)/make.timestamp + rm -f $(KWASM_SUBMODULE)/make.timestamp rm -f $(eei_submodule)/make.timestamp git submodule update --init --recursive $(MAKE) clean -C $(KWASM_SUBMODULE) @@ -51,37 +43,13 @@ clean: # Build Dependencies (K Submodule) # -------------------------------- -wasm_files=test.md wasm.md wasm-text.md data.md kwasm-lemmas.md -wasm_source_files:=$(patsubst %, $(KWASM_SUBMODULE)/%, $(wasm_files)) -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) -all_k_files:=$(ewasm_files) $(wasm_files) $(eei_files) - -llvm_dir:=$(DEFN_DIR)/llvm -llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files)) - -haskell_dir:=$(DEFN_DIR)/haskell -haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files)) +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) -definition-deps: eei-definitions -deps: $(KWASM_SUBMODULE)/make.timestamp $(eei_submodule)/make.timestamp definition-deps - -wasm-definitions: - $(KWASM_MAKE) -B defn-llvm - $(KWASM_MAKE) -B defn-haskell - -eei-definitions: $(eei_source_files) - $(eei_make) -B defn-llvm - $(eei_make) -B defn-haskell - -$(KWASM_SUBMODULE)/make.timestamp: $(wasm_source_files) +deps: $(KWASM_MAKE) deps - touch $(KWASM_SUBMODULE)/make.timestamp - -$(eei_submodule)/make.timestamp: $(eei_source_files) - touch $(eei_submodule)/make.timestamp # Building Definition # ------------------- @@ -97,7 +65,7 @@ KOMPILE_OPTS := build: build-llvm build-haskell build-%: - cp $(eei_source_files) $(ewasm_source_files) $(KWASM_SUBMODULE) + cp $(EEI_SOURCE_FILES) $(EWASM_SOURCE_FILES) $(KWASM_SUBMODULE) $(KWASM_MAKE) build-$* \ DEFN_DIR=../../$(DEFN_DIR) \ llvm_main_module=$(MAIN_MODULE) \ @@ -106,7 +74,7 @@ build-%: haskell_main_module=$(MAIN_MODULE) \ haskell_syntax_module=$(MAIN_SYNTAX_MODULE) \ haskell_main_file=$(MAIN_DEFN_FILE) \ - EXTRA_SOURCE_FILES="$(eei_files) $(ewasm_files)" \ + EXTRA_SOURCE_FILES="$(EEI_FILES) $(EWASM_FILES)" \ KOMPILE_OPTS="$(KOMPILE_OPTS)" # Testing From c3fad9a5e4eadeeaa1dd7ad2a146a37cb82c8ad9 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 23:43:26 +0000 Subject: [PATCH 19/38] Jenkinsfile: remove tangling target --- Jenkinsfile | 1 - 1 file changed, 1 deletion(-) diff --git a/Jenkinsfile b/Jenkinsfile index fdcc43b..01e8226 100644 --- a/Jenkinsfile +++ b/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') } From 3870f98bfc568f79c2cf62bbd4d593ea7e83e174 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 10:19:25 +0000 Subject: [PATCH 20/38] Makefile: only rebuild definitions when source files change --- Makefile | 44 ++++++++++++++++++++++++++------------------ 1 file changed, 26 insertions(+), 18 deletions(-) diff --git a/Makefile b/Makefile index a25a05c..0024504 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ DEPS_DIR := deps KWASM_SUBMODULE := $(DEPS_DIR)/wasm-semantics -eei_submodule := $(DEPS_DIR)/eei-semantics +EEI_SUBMODULE := $(DEPS_DIR)/eei-semantics k_submodule := $(KWASM_SUBMODULE)/deps/k ifneq (,$(wildcard $(k_submodule)/k-distribution/target/release/k/bin/*)) @@ -24,9 +24,10 @@ kompiled_dir_name := ewasm-test KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) -.PHONY: all clean \ - deps defn build \ - test test-execution test-simple test-prove \ +.PHONY: all clean deps \ + build build-llvm build-haskell \ + test test-execution test-simple \ + test-prove \ media presentations reports all: build @@ -35,18 +36,20 @@ clean: rm -rf $(build_dir) rm -f $(KWASM_SUBMODULE)/make.timestamp rm -f $(KWASM_SUBMODULE)/make.timestamp - rm -f $(eei_submodule)/make.timestamp + rm -f $(EEI_SUBMODULE)/make.timestamp git submodule update --init --recursive $(MAKE) clean -C $(KWASM_SUBMODULE) - $(MAKE) clean -C $(eei_submodule) + $(MAKE) clean -C $(EEI_SUBMODULE) # Build Dependencies (K Submodule) # -------------------------------- EEI_FILES:=eei.md -EEI_SOURCE_FILES:=$(patsubst %, $(eei_submodule)/%, $(EEI_FILES)) +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)) deps: $(KWASM_MAKE) deps @@ -64,19 +67,24 @@ KOMPILE_OPTS := build: build-llvm build-haskell -build-%: - cp $(EEI_SOURCE_FILES) $(EWASM_SOURCE_FILES) $(KWASM_SUBMODULE) - $(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="$(EEI_FILES) $(EWASM_FILES)" \ +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 # ------- From b82de8c0aa4064828c8850ee770d297a82532fe5 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 10:47:43 +0000 Subject: [PATCH 21/38] Makefile: cleanups --- Makefile | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index 0024504..5f3a7c5 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,10 @@ # Settings # -------- -DEPS_DIR := deps +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 @@ -18,9 +21,6 @@ export K_RELEASE PATH:=$(K_BIN):$(abspath $(KWASM_SUBMODULE)):$(PATH) export PATH -build_dir := .build -DEFN_DIR := $(build_dir)/defn -kompiled_dir_name := ewasm-test KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) @@ -34,9 +34,6 @@ all: build clean: rm -rf $(build_dir) - rm -f $(KWASM_SUBMODULE)/make.timestamp - rm -f $(KWASM_SUBMODULE)/make.timestamp - rm -f $(EEI_SUBMODULE)/make.timestamp git submodule update --init --recursive $(MAKE) clean -C $(KWASM_SUBMODULE) $(MAKE) clean -C $(EEI_SUBMODULE) From c341f964ccbdd603a11b06fe50d59866a1dbfa4d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 10:59:11 +0000 Subject: [PATCH 22/38] Makefile: remove phony targets --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 5f3a7c5..bb5cc2d 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ export PATH KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) .PHONY: all clean deps \ - build build-llvm build-haskell \ + build \ test test-execution test-simple \ test-prove \ media presentations reports From bde084042c447d1e281bd796c92b8330d1a535c9 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 11:01:01 +0000 Subject: [PATCH 23/38] Makefile: build_dir => BUILD_DIR --- Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index bb5cc2d..32629cd 100644 --- a/Makefile +++ b/Makefile @@ -1,9 +1,9 @@ # Settings # -------- -build_dir := .build +BUILD_DIR := .build DEPS_DIR := deps -DEFN_DIR := $(build_dir)/defn +DEFN_DIR := $(BUILD_DIR)/defn KWASM_SUBMODULE := $(DEPS_DIR)/wasm-semantics EEI_SUBMODULE := $(DEPS_DIR)/eei-semantics @@ -33,7 +33,7 @@ KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) R all: build clean: - rm -rf $(build_dir) + rm -rf $(BUILD_DIR) git submodule update --init --recursive $(MAKE) clean -C $(KWASM_SUBMODULE) $(MAKE) clean -C $(EEI_SUBMODULE) From aa3c1bcd45b17f3e585c9ece58b48b201b55b7b7 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 11:04:59 +0000 Subject: [PATCH 24/38] Makefile: add build-\% as .PHONY target --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 32629cd..472b8a6 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ export PATH KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) .PHONY: all clean deps \ - build \ + build build-% \ test test-execution test-simple \ test-prove \ media presentations reports From 315c6c0e7f4be9c89083842a15743a07f9620594 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 11:23:21 +0000 Subject: [PATCH 25/38] Makefile: proofs should depend on presence of lemmas file --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 472b8a6..711e918 100644 --- a/Makefile +++ b/Makefile @@ -89,6 +89,7 @@ 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 @@ -114,7 +115,7 @@ tests/%.parse: tests/% $(CHECK) $@-expected $@-out rm -rf $@-out -tests/%.prove: tests/% +tests/%.prove: tests/% $(KWASM_SUBMODULE)/$(KRPOVE_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 From 306ab728204ccb10e35ad3c1e4dd195cc1d60c0a Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 11:23:31 +0000 Subject: [PATCH 26/38] Makefile: remove unused target --- Makefile | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Makefile b/Makefile index 711e918..d9e3246 100644 --- a/Makefile +++ b/Makefile @@ -93,11 +93,6 @@ 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 From 0cd1975bf5f7835d95e8034ae9cea602869520a6 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 17:19:26 +0000 Subject: [PATCH 27/38] fix: typo --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index d9e3246..b3a9b15 100644 --- a/Makefile +++ b/Makefile @@ -110,7 +110,7 @@ tests/%.parse: tests/% $(CHECK) $@-expected $@-out rm -rf $@-out -tests/%.prove: tests/% $(KWASM_SUBMODULE)/$(KRPOVE_MODULE_FILE) +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 From fb1bd139986d7bac58a0de7bd807d2798ab4523c Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sun, 14 Jun 2020 17:20:28 +0000 Subject: [PATCH 28/38] Makefile: Remove build-% PHONY target --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b3a9b15..4828c91 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ export PATH KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) .PHONY: all clean deps \ - build build-% \ + build \ test test-execution test-simple \ test-prove \ media presentations reports From 1b4607905b85f96a40d17b68d1083c9db519db60 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Sun, 14 Jun 2020 20:53:15 +0000 Subject: [PATCH 29/38] deps/wasm-semantics: 1dca85e - Explicit instruction sequencing (#360) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 8794dd4..1dca85e 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 8794dd41faf968e434f9e634c1c5be27631163ab +Subproject commit 1dca85e38b73ddbf639646eff26a1e0eecc2ac54 From 3ec56f50fb1e02fee1a6c9224722787e7214adec Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 17 Jun 2020 13:28:59 +0000 Subject: [PATCH 30/38] deps/wasm-semantics: 51bb2ab - Embedded Wasm (#362) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 1dca85e..51bb2ab 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 1dca85e38b73ddbf639646eff26a1e0eecc2ac54 +Subproject commit 51bb2abb1210d71be883b48285ad08b1b2c7f13d From b9f91c21d37c1052ad22d22d2348bb61a728a395 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 17 Jun 2020 15:53:21 +0000 Subject: [PATCH 31/38] deps/wasm-semantics: af4e537 - Update dependency: deps/k (#352) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 51bb2ab..af4e537 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 51bb2abb1210d71be883b48285ad08b1b2c7f13d +Subproject commit af4e537fe8f57321a3a63a5b289c54773aebfa98 From 20015a5976c678208d094fc43b7de545152b86ef Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 24 Jun 2020 21:25:16 +0000 Subject: [PATCH 32/38] deps/wasm-semantics: 470f34e - Update dependency: deps/k (#364) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index af4e537..470f34e 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit af4e537fe8f57321a3a63a5b289c54773aebfa98 +Subproject commit 470f34e47e2e98164beee4fe50313ef08d7646a8 From c4bb796b534f1aa8ece16371ef0da6fe7b81d2d1 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Thu, 25 Jun 2020 18:23:47 +0000 Subject: [PATCH 33/38] deps/wasm-semantics: 1b18811 - Use WASM-TEXT as main cell for Haskell kompile (#365) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 470f34e..1b18811 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 470f34e47e2e98164beee4fe50313ef08d7646a8 +Subproject commit 1b188115edff987ba0400bfb26b7a5ded11dce62 From 510d64bac0c6f79133a9ada81f7e22814adf570e Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Fri, 26 Jun 2020 16:24:18 +0000 Subject: [PATCH 34/38] deps/wasm-semantics: 117eeb0 - Add underscore to unsed variables (#366) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 1b18811..117eeb0 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 1b188115edff987ba0400bfb26b7a5ded11dce62 +Subproject commit 117eeb0ebc510f6c075d7881eb706c7e24bdc7d0 From 9d7606ea4a91cbac652a26610ed0cefd67376091 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 8 Jul 2020 10:24:02 +0000 Subject: [PATCH 35/38] deps/wasm-semantics: 54eb26f - Type desugaring during text -> core phase (#367) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 117eeb0..54eb26f 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 117eeb0ebc510f6c075d7881eb706c7e24bdc7d0 +Subproject commit 54eb26f0a532dfde443d7ac39f0e6cb0f9275a6c From 9cd41854ac66e035d401019a9186a0cd4b08493d Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Fri, 10 Jul 2020 03:54:57 +0000 Subject: [PATCH 36/38] deps/wasm-semantics: 221a9d9 - deps/k: ab078f6d5 - Update issue templates (#1407) (#369) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 54eb26f..221a9d9 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 54eb26f0a532dfde443d7ac39f0e6cb0f9275a6c +Subproject commit 221a9d92bfac383961ffc3ab1d78372eb52c85fb From 2e6a3cdd610022c8cf1383b1c14374555c35ea4c Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 14 Jul 2020 17:24:18 +0000 Subject: [PATCH 37/38] deps/wasm-semantics: 520245d - Remove #ContextLookup for types when allocating functions (#368) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 221a9d9..520245d 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 221a9d92bfac383961ffc3ab1d78372eb52c85fb +Subproject commit 520245de72d7ef308327ab553ca1d52f8ff55dc7 From ae9e930f4f655f705e9bbe9b953ef1a5eed42616 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 29 Jul 2020 17:08:11 +0000 Subject: [PATCH 38/38] deps/wasm-semantics: d56298b - Update dependency: deps/k (#370) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 520245d..d56298b 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 520245de72d7ef308327ab553ca1d52f8ff55dc7 +Subproject commit d56298b602b7f5b30f6282125bb82610b68e7a7d