DO NOT REVIEW - K version test

.github/workflows/test-pr.yml

@@ -109,8 +109,6 @@ jobs:
         run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} poetry -C pykwasm install
       - name: 'Build ulm-wasm'
         run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} bash -c "CXX=clang++-16 make ulm-wasm"
-      - name: 'Build ulm-contract-compiler'
-        run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} bash -c "CXX=clang++-16 make ulm-contract-compiler"
       - name: 'Build ulm-build'
         run: docker exec -u user kwasm-ci-erc20-${GITHUB_SHA} bash -c "CXX=clang++-16 make ulm-build"
       - name: 'Build erc20-bin'

Makefile

@@ -63,8 +63,6 @@ ULM_WASM_TARGET=$(ULM_LIB_DIR)/$(ULM_WASM_LIB)
 ULM_WASM_MAIN=$(ULM_WASM_SRC_DIR)/ulm-wasm.md
 ULM_WASM_SRC=$(wildcard $(ULM_WASM_SRC_DIR)/*.md $(ULM_WASM_SRC_DIR)/data/*.k)
 
-ULM_WASM_COMPILER_TARGET=$(ULM_BUILD_DIR)/ulm-contract-compiler
-
 ## Depedencies
 
 ULM_KRYPTO_DIR=$(ULM_DEP_DIR)/plugin
@@ -186,27 +184,9 @@ ulm-wasm: $(ULM_WASM_TARGET)
 $(ULM_WASM_TARGET): $(ULM_KRYPTO_TARGET) $(ULM_HOOKS_TARGET) $(ULM_WASM_SRC) pykwasm
 	$(KDIST) -v build wasm-semantics.$(ULM_WASM_TARGET_NAME) -j3
 	$(eval ULM_WASM_DIR := $(shell $(KDIST) which wasm-semantics.$(ULM_WASM_TARGET_NAME)))
-	kore-rich-header "$(ULM_WASM_DIR)/definition.kore" -o "$(ULM_WASM_DIR)/header.bin"
 	$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/$(ULM_WASM_LIB)" "$(ULM_LIB_DIR)";)
-	$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/header.bin"      "$(ULM_LIB_DIR)";)
-
 
-### ULM Wasm Contract Compiler
 
-$(ULM_WASM_COMPILER_TARGET): $(ULM_WASM_TARGET)
-	$(CXX) "$(ULM_HOOKS_DIR)/emit_contract_bytes.cpp" \
-	  -I "$(ULM_KF_INCLUDE_DIR)" \
-	  -I "$(ULM_KF_INCLUDE_DIR)/kllvm" \
-	  -std=c++20 \
-	  -DULM_LANG_ID=wasm \
-	  -Wno-return-type-c-linkage \
-	  -L"$(ULM_LIB_DIR)" \
-	  -lulmkllvm \
-	  -lkwasm \
-	  -o "$(ULM_WASM_COMPILER_TARGET)"
-
-.PHONY: ulm-contract-compiler
-ulm-contract-compiler: $(ULM_WASM_COMPILER_TARGET)
 
 ERC20_DIR=tests/ulm/erc20/rust
 ERC20_SRC=$(shell find "$(ERC20_DIR)" -type f -a '(' -name '*.rs' -or -name '*.toml' -or -name '*.lock' ')')
@@ -223,10 +203,9 @@ $(ERC20_WASM_TARGET): $(ERC20_SRC) $(ERC20_BUILD_DIR)
 	cd $(ERC20_DIR) && cargo build --target=wasm32-unknown-unknown --release
 	cp $(ERC20_DIR)/target/wasm32-unknown-unknown/release/erc20.wasm $@
 
-$(ERC20_BIN_TARGET): $(ERC20_WASM_TARGET) $(ULM_WASM_COMPILER_TARGET) $(ULM_WASM_TARGET)
-	$(eval ULM_WASM_DIR := $(shell $(KDIST) which wasm-semantics.$(ULM_WASM_TARGET_NAME)))
-	poetry -C pykwasm run wasm2kore $(ULM_WASM_DIR) $< $(ERC20_BUILD_DIR)/erc20.kore
-	scripts/compile-contract $(ERC20_BUILD_DIR)/erc20.kore > $@
+$(ERC20_BIN_TARGET): $(ERC20_WASM_TARGET)
+	echo -n "7761736D" > $@
+	xxd -p $< | tr -d '\n' >> $@
 
 .PHONY: erc20-bin
 erc20-bin: $(ERC20_BIN_TARGET)

deps/k_release

@@ -1 +1 @@
-7.1.191
+7.1.167

pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser-test.md

@@ -27,11 +27,6 @@ module BINARY-PARSER-TEST
             , _D:GlobalDefn
             , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(GlobalDefn) branch called." )))
         [owise]
-    rule addDefnToModule
-            ( false => true
-            , _D:TableDefn
-            , #module(... metadata: _ => #meta (... id:  , funcIds: .Map , filename: "error: test addDefnToModule(TableDefn) branch called." )))
-        [owise]
     rule addDefnToModule
             ( false => true
             , _D:MemoryDefn

pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md

@@ -10,40 +10,47 @@ requires "binary-parsing/binary-defn-convert.md"
 requires "binary-parsing/block.md"
 requires "binary-parsing/bytes.md"
 requires "binary-parsing/code.md"
-requires "binary-parsing/code-section.md"
 requires "binary-parsing/constant.md"
+requires "binary-parsing/data.md"
+requires "binary-parsing/data-count-section.md"
 requires "binary-parsing/defn.md"
+requires "binary-parsing/elem.md"
+requires "binary-parsing/export.md"
+requires "binary-parsing/expr.md"
+requires "binary-parsing/expr-vec.md"
 requires "binary-parsing/float.md"
-requires "binary-parsing/func-section.md"
 requires "binary-parsing/func-section-entry.md"
 requires "binary-parsing/functype.md"
+requires "binary-parsing/global.md"
 requires "binary-parsing/globaltype.md"
 requires "binary-parsing/helpers.md"
 requires "binary-parsing/if.md"
 requires "binary-parsing/import.md"
-requires "binary-parsing/import-section.md"
 requires "binary-parsing/instr.md"
 requires "binary-parsing/instr-list.md"
 requires "binary-parsing/int.md"
 requires "binary-parsing/limits.md"
 requires "binary-parsing/locals.md"
 requires "binary-parsing/loop.md"
 requires "binary-parsing/memarg.md"
+requires "binary-parsing/memory.md"
 requires "binary-parsing/module.md"
 requires "binary-parsing/name.md"
 requires "binary-parsing/resulttype.md"
+requires "binary-parsing/reftype.md"
 requires "binary-parsing/section.md"
+requires "binary-parsing/start-section.md"
 requires "binary-parsing/tags.md"
-requires "binary-parsing/type-section.md"
+requires "binary-parsing/table.md"
 requires "binary-parsing/valtype.md"
 
 
 module BINARY-PARSER-SYNTAX
   imports BINARY-PARSER-BASE-SYNTAX
   imports WASM
 
-  syntax ModuleOrError ::= ModuleDecl | ParseError
-  syntax ModuleOrError ::= parseModule(Bytes)  [function, total]
+  syntax ModuleDeclOrError ::= ModuleDecl | ParseError
+  syntax ModuleDeclOrError ::= parseModule(Bytes)  [function, total]
 endmodule
 
 module BINARY-PARSER  [private]
@@ -53,35 +60,42 @@ module BINARY-PARSER  [private]
   imports BINARY-PARSER-BLOCK
   imports BINARY-PARSER-BYTES
   imports BINARY-PARSER-CODE
-  imports BINARY-PARSER-CODE-SECTION
   imports BINARY-PARSER-CONSTANT
+  imports BINARY-PARSER-DATA
+  imports BINARY-PARSER-DATA-COUNT-SECTION
+  imports BINARY-PARSER-ELEM
+  imports BINARY-PARSER-EXPORT
+  imports BINARY-PARSER-EXPR
+  imports BINARY-PARSER-EXPR-VEC
   imports BINARY-PARSER-FLOAT
-  imports BINARY-PARSER-FUNC-SECTION
   imports BINARY-PARSER-FUNC-SECTION-ENTRY
   imports BINARY-PARSER-FUNCTYPE
+  imports BINARY-PARSER-GLOBAL
   imports BINARY-PARSER-GLOBALTYPE
   imports BINARY-PARSER-HELPERS
   imports BINARY-PARSER-IF
   imports BINARY-PARSER-IMPORT
-  imports BINARY-PARSER-IMPORT-SECTION
   imports BINARY-PARSER-INSTR-LIST
   imports BINARY-PARSER-INSTR
   imports BINARY-PARSER-INT
   imports BINARY-PARSER-LIMITS
   imports BINARY-PARSER-LOCALS
   imports BINARY-PARSER-LOOP
   imports BINARY-PARSER-MEMARG
+  imports BINARY-PARSER-MEMORY
   imports BINARY-PARSER-MODULE
   imports BINARY-PARSER-NAME
   imports BINARY-PARSER-RESULTTYPE
+  imports BINARY-PARSER-REFTYPE
   imports BINARY-PARSER-SECTION
   imports BINARY-PARSER-SYNTAX
-  imports BINARY-PARSER-TYPE-SECTION
+  imports BINARY-PARSER-START-SECTION
+  imports BINARY-PARSER-TABLE
   imports BINARY-PARSER-VALTYPE
 
   rule parseModule(B:Bytes) => checkAllBytesParsed(parseModule(bwi(B, 0)))
 
-  syntax ModuleOrError ::= checkAllBytesParsed(ModuleResult)  [function, total]
+  syntax ModuleDeclOrError ::= checkAllBytesParsed(ModuleResult)  [function, total]
   rule checkAllBytesParsed(moduleResult(M, bwi(B:Bytes, Index:Int))) => M requires Index ==Int lengthBytes(B)
   rule checkAllBytesParsed(E:ParseError) => E
 

pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/binary-defn-convert.md

@@ -4,11 +4,17 @@ Convert BinaryDefn to Defn.
 module BINARY-PARSER-BINARY-DEFN-CONVERT-SYNTAX
   imports BINARY-PARSER-BASE-SYNTAX
   imports BINARY-PARSER-CODE-SYNTAX
+  imports BINARY-PARSER-DATA-SYNTAX
   imports BINARY-PARSER-DEFN-SYNTAX
+  imports BINARY-PARSER-ELEM-SYNTAX
+  imports BINARY-PARSER-GLOBAL-SYNTAX
   imports BINARY-PARSER-FUNC-SECTION-ENTRY-SYNTAX
   imports WASM-DATA-COMMON
 
   syntax DefnsOrError ::= buildFunctionDefns(Defns, BinaryDefnFunctionTypes, BinaryDefnFunctionBodies)  [function, total]
+  syntax DefnsOrError ::= buildElementDefns(Defns, BinaryDefnElements)  [function, total]
+  syntax DefnsOrError ::= buildGlobalDefns(Defns, BinaryDefnGlobals)  [function, total]
+  syntax DefnsOrError ::= buildDataDefns(Defns, BinaryDefnDatas)  [function, total]
 
 endmodule
 
@@ -119,5 +125,78 @@ module BINARY-PARSER-BINARY-DEFN-CONVERT  [private]
   rule resolvedBlockInstrsToIf(E:ParseError, _:InstrsOrError) => E
   rule resolvedBlockInstrsToIf(_:ResolvedBlockOrError, E:ParseError) => E
       [owise]
+
+
+  rule buildElementDefns(_:Defns, .BinaryDefnElements) => .Defns
+  rule buildElementDefns
+          ( Ds:Defns
+          , E:BinaryDefnElem Es:BinaryDefnElements
+          )
+      => addDefnOrError(buildElementDefn(Ds, E), buildElementDefns(Ds, Es))
+
+  syntax DefnOrError  ::= buildElementDefn(Defns, BinaryDefnElem)  [function, total]
+                        | #buildElementDefn(RefValType, ListRef, Int, InstrsOrError)  [function, total]
+  rule buildElementDefn
+          ( Ds:Defns
+          , #binaryElem
+              ( T:RefValType
+              , Segment:ListRef
+              , #binaryElemActive(Table:Int, Offset:BinaryInstrs)
+              )
+          )
+      => #buildElementDefn(T, Segment, Table, binaryInstrsToInstrs(Ds, Offset))
+  rule #buildElementDefn(T:RefValType, Segment:ListRef, Table:Int, Is:Instrs)
+      => #elem(T, Segment, #elemActive(Table, Is), )
+  rule #buildElementDefn(_:RefValType, _:ListRef, _:Int, E:ParseError) => E
+
+
+  rule buildGlobalDefns(_:Defns, .BinaryDefnGlobals) => .Defns
+  rule buildGlobalDefns
+          ( Ds:Defns
+          , E:BinaryDefnGlobal Es:BinaryDefnGlobals
+          )
+      => addDefnOrError(buildGlobalDefn(Ds, E), buildGlobalDefns(Ds, Es))
+
+  syntax DefnOrError  ::= buildGlobalDefn(Defns, BinaryDefnGlobal)  [function, total]
+                        | #buildGlobalDefn(GlobalType, InstrsOrError)  [function, total]
+  rule buildGlobalDefn
+          ( Ds:Defns
+          , #binaryGlobal
+              ( T:GlobalType
+              , Is:BinaryInstrs
+              )
+          )
+      => #buildGlobalDefn(T, binaryInstrsToInstrs(Ds, Is))
+  rule #buildGlobalDefn(T:GlobalType, Is:Instrs) => #global(T, Is, )
+  rule #buildGlobalDefn(_:GlobalType, E:ParseError) => E
+
+
+  rule buildDataDefns(_:Defns, .BinaryDefnDatas) => .Defns
+  rule buildDataDefns
+          ( Ds:Defns
+          , E:BinaryDefnData Es:BinaryDefnDatas
+          )
+      => addDefnOrError(buildDataDefn(Ds, E), buildDataDefns(Ds, Es))
+
+  syntax DefnOrError  ::= buildDataDefn(Defns, BinaryDefnData)  [function, total]
+                        | #buildDataDefn(Int, Bytes, InstrsOrError)  [function, total]
+  rule buildDataDefn
+          ( Ds:Defns
+          , #binaryData
+              (... index: Index:Int
+              , offset: Is:BinaryInstrs
+              , data: B:Bytes
+              )
+          )
+      => #buildDataDefn(Index, B, binaryInstrsToInstrs(Ds, Is))
+  rule #buildDataDefn(Index:Int, B:Bytes, Is:Instrs) => #data(Index, Is, B)
+  rule #buildDataDefn(_:Int, _:Bytes, E:ParseError) => E
+
+
+  syntax DefnsOrError ::= addDefnOrError(DefnOrError, DefnsOrError)  [function, total]
+  rule addDefnOrError(D:Defn, Ds:Defns) => D Ds
+  rule addDefnOrError(E:ParseError, _:DefnsOrError) => E
+  rule addDefnOrError(_:Defn, E:ParseError) => E
+
 endmodule
 ```

pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/code.md

@@ -6,24 +6,28 @@ module BINARY-PARSER-CODE-SYNTAX
   imports BINARY-PARSER-INSTR-LIST-SYNTAX
   imports WASM
 
+  syntax DefnKind ::= "defnCode"
+
   syntax BinaryDefn ::= BinaryDefnFunctionBody
   syntax BinaryDefnFunctionBody ::= binaryDefnFunctionBody(VecType, BinaryInstrs)
 
   syntax BinaryDefnFunctionBodies ::= List{BinaryDefnFunctionBody, ""}
 
-  syntax DefnResult ::= parseDefnCode(BytesWithIndex)  [function, total]
 endmodule
 
 module BINARY-PARSER-CODE  [private]
   imports BINARY-PARSER-CODE-SYNTAX
+  imports BINARY-PARSER-DEFN-SYNTAX
   imports BINARY-PARSER-INSTR-LIST-SYNTAX
   imports BINARY-PARSER-INT-SYNTAX
   imports BINARY-PARSER-LOCALS-SYNTAX
-  imports BINARY-PARSER-SECTION-SYNTAX
   imports BINARY-PARSER-VALTYPE-SYNTAX
   imports BOOL
 
-  syntax DefnResult ::= #parseDefnCode(sizeInBytes:IntResult)  [function, total]
+  rule parseDefn(defnCode, BWI:BytesWithIndex) => parseDefnCode(BWI)
+
+  syntax DefnResult ::= parseDefnCode(BytesWithIndex)  [function, total]
+                      | #parseDefnCode(sizeInBytes:IntResult)  [function, total]
                       | #parseDefnCode1(sizeInBytes:Int, LocalsVecResult)  [function, total]
                       | #parseDefnCode2(sizeInBytes:Int, ValTypes, InstrListResult)  [function, total]
   rule parseDefnCode(BWI:BytesWithIndex) => #parseDefnCode(parseLeb128UInt(BWI))

pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parsing/data-count-section.md

@@ -0,0 +1,33 @@
+Parse the [data count section](https://webassembly.github.io/spec/core/binary/modules.html#binary-datacountsec)
+
+```k
+module BINARY-PARSER-DATA-COUNT-SECTION-SYNTAX
+  imports BINARY-PARSER-BASE-SYNTAX
+  imports BINARY-PARSER-SECTION-SYNTAX
+
+  syntax SectionResult ::= parseDataCountSection(BytesWithIndex)  [function, total]
+endmodule
+
+module BINARY-PARSER-DATA-COUNT-SECTION
+  imports BINARY-PARSER-INT-SYNTAX
+  imports BINARY-PARSER-DATA-COUNT-SECTION-SYNTAX
+  imports BINARY-PARSER-DEFN-SYNTAX
+  imports WASM
+
+  syntax SectionResult ::= #parseDataCountSection(IntResult)  [function, total]
+
+  rule parseDataCountSection(BWI:BytesWithIndex) => #parseDataCountSection(parseLeb128UInt(BWI))
+```
+
+It seems that there is no existing constructor for the data count. The
+documentation says that is is useful only for validation, so we are ignoring it
+for now.
+
+```k
+  rule #parseDataCountSection(intResult(_Count:Int, BWI:BytesWithIndex))
+      => sectionResult(defnsSection(.BinaryDefns), BWI)
+  rule #parseDataCountSection(E:ParseError) => E
+
+endmodule
+
+```