From 2b99c91de2a14eb133a836ea692e714a2b072d2c Mon Sep 17 00:00:00 2001
From: Stephen Skeirik <stephen.skeirik@runtimeverification.com>
Date: Fri, 20 Dec 2024 18:11:38 -0500
Subject: [PATCH 1/9] add partial binary parser

---
 .../kdist/wasm-semantics/binary-parser.md     | 379 ++++++++++++++++++
 1 file changed, 379 insertions(+)
 create mode 100644 pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
new file mode 100644
index 000000000..69d7ba6b4
--- /dev/null
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -0,0 +1,379 @@
+# Wasm Binary Parser
+
+This file defines a Wasm binary parser.
+To begin, we define constant macros which drive the parser process.
+
+```k
+module BINARY_PARSER_DATA
+  imports BYTES
+```
+
+## Wasm Metadata Parser Tags
+
+Every Wasm module starts with a 4-byte header and a 4-byte version.
+
+```k
+  syntax Bytes ::= MAGIC   [macro] rule MAGIC   => b"x00x61x73x6D"
+                 | VERSION [macro] rule VERSION => b"x01x00x00x00"
+```
+
+After that, a Wasm module is an ordered list of sections, each prefixed with a section id.
+
+```k
+                 | CUSTOM_SEC [macro] rule CUSTOM_SEC => b"x00"
+                 | TYPE_SEC   [macro] rule TYPE_SEC   => b"x01"
+                 | IMPORT_SEC [macro] rule IMPORT_SEC => b"x02"
+                 | FUNC_SEC   [macro] rule FUNC_SEC   => b"x03"
+                 | TABLE_SEC  [macro] rule TABLE_SEC  => b"x04"
+                 | MEMORY_SEC [macro] rule MEMORY_SEC => b"x05"
+                 | GLOBAL_SEC [macro] rule GLOBAL_SEC => b"x06"
+                 | EXPORT_SEC [macro] rule EXPORT_SEC => b"x07"
+                 | START_SEC  [macro] rule START_SEC  => b"x08"
+                 | ELT_SEC    [macro] rule ELT_SEC    => b"x09"
+                 | CODE_SEC   [macro] rule CODE_SEC   => b"x0a"
+                 | DAT_SEC    [macro] rule DAT_SEC    => b"x0b"
+                 | CNT_SEC    [macro] rule CNT_SEC    => b"x0c"
+```
+
+In the import/export sections, different kinds of imports/exports are tagged.
+
+```k
+                 | IMPORT_FUNC [macro] rule IMPORT_FUNC => b"x00"
+                 | IMPORT_TBLT [macro] rule IMPORT_TBLT => b"x01"
+                 | IMPORT_MEMT [macro] rule IMPORT_MEMT => b"x02"
+                 | IMPORT_GLBT [macro] rule IMPORT_GLBT => b"x03"
+                 | EXPORT_FUNC [macro] rule EXPORT_FUNC => b"x00"
+                 | EXPORT_TBLT [macro] rule EXPORT_TBLT => b"x01"
+                 | EXPORT_MEMT [macro] rule EXPORT_MEMT => b"x02"
+                 | EXPORT_GLBT [macro] rule EXPORT_GLBT => b"x03"
+```
+
+_Element_ sections have various possible formats which are stored in a 3-bit code.
+The possible code words are explained in the table below:
+
+Bit # | Constraint | 0 State         | 1 State              |
+----- | ---------- | --------------- | -------------------- |
+0     | None       | active          | passive/declarative  |
+1     | Bit[0]=0   | has table index | zero table index     |
+1     | Bit[0]=1   | passive         | declarative          |
+2     | None       | elts by ref     | elts by value        |
+
+```k
+                 | ELTS_ACTIVE_ZERO_BY_REF [macro] // 000
+                 | ELTS_PASSIVE_BY_REF     [macro] // 001
+                 | ELTS_ACTIVE_IDX_BY_REF  [macro] // 010
+                 | ELTS_DECL_BY_REF        [macro] // 011
+                 | ELTS_ACTIVE_ZERO_BY_VAL [macro] // 100
+                 | ELTS_PASSIVE_BY_VAL     [macro] // 101
+                 | ELTS_ACTIVE_IDX_BY_VAL  [macro] // 110
+                 | ELTS_DECL_BY_VAL        [macro] // 110
+
+  rule ELTS_ACTIVE_ZERO_BY_REF => b"x00"
+  rule ELTS_PASSIVE_BY_REF     => b"x01"
+  rule ELTS_ACTIVE_IDX_BY_REF  => b"x02"
+  rule ELTS_DECL_BY_REF        => b"x03"
+  rule ELTS_ACTIVE_ZERO_BY_VAL => b"x04"
+  rule ELTS_PASSIVE_BY_VAL     => b"x05"
+  rule ELTS_ACTIVE_IDX_BY_VAL  => b"x06"
+  rule ELTS_DECL_BY_VAL        => b"x07"
+```
+
+The special _element kind_ constant is used to describe possible element kinds.
+Currently, only one element kind is supported.
+
+```k
+                 | ELT_KIND [macro] rule ELT_KIND => b"x00"
+```
+
+_Data_ sections are tagged based on their kind.
+
+```k
+                 | DATA_ACTIVE_ZERO [macro] rule DATA_ACTIVE_ZERO  => b"x00"
+                 | DATA_PASSIVE     [macro] rule DATA_PASSIVE_ZERO => b"x01"
+                 | DATA_ACTIVE_IDX  [macro] rule DATA_ACTIVE_IDX   => b"x02"
+```
+
+Each value _type_ is tagged by a unique integer.
+There are two special types: functions and empty types.
+These have special use requirements as we will see later.
+
+```k
+                 | TYPE_I32     [macro] rule TYPE_I32     => b"x7F"
+                 | TYPE_I64     [macro] rule TYPE_I64     => b"x7E"
+                 | TYPE_F32     [macro] rule TYPE_F32     => b"x7D"
+                 | TYPE_F64     [macro] rule TYPE_F64     => b"x7C"
+                 | TYPE_VEC     [macro] rule TYPE_VEC     => b"x7B"
+                 | TYPE_FUN_REF [macro] rule TYPE_FUN_REF => b"x70"
+                 | TYPE_EXT_REF [macro] rule TYPE_EXT_REF => b"x64"
+                 | TYPE_FUN     [macro] rule TYPE_FUN     => b"x60"
+                 | TYPE_EMPTY   [macro] rule TYPE_EMPTY   => b"x40"
+```
+
+_Limits_ are used to encode the minimum size of memories and tables;
+a separate form that also specifies a maximum size is available.
+
+```k
+                 | LIMITS     [macro] rule LIMITS     => b"x00"
+                 | LIMITS_MAX [macro] rule LIMITS_MAX => b"x01"
+```
+
+_Globals_ may be declared as mutable or immutable.
+
+```k
+                 | GLOBAL_CNST [macro] rule GLOBAL_CNST => b"x00"
+                 | GLOBAL_VAR  [macro] rule GLOBAL_VAR  => b"x01"
+```
+
+## Wasm Instruction Parser Tags
+
+Wasm _control instructions_ are encoded with the follow tags.
+Note that `ELSE` instructions must appear in conjunction with `IF` instructions.
+
+```k
+  syntax Bytes ::= UNREACHABLE   [macro] rule UNREACHABLE   => b"x00"
+                 | NOP           [macro] rule NOP           => b"x01"
+                 | BLOCK         [macro] rule BLOCK         => b"x02"
+                 | LOOP          [macro] rule LOOP          => b"x03"
+                 | IF            [macro] rule IF            => b"x04"
+                 | ELSE          [macro] rule ELSE          => b"x05"
+                 | BR            [macro] rule BR            => b"x0C"
+                 | BR_IF         [macro] rule BR_IF         => b"x0D"
+                 | BR_TABLE      [macro] rule BR_TABLE      => b"x0E"
+                 | RETURN        [macro] rule RETURN        => b"x0F"
+                 | CALL          [macro] rule CALL          => b"x10"
+                 | CALL_INDIRECT [macro] rule CALL_INDIRECT => b"x11"
+```
+
+_Reference instructions_ are encoded with the following tags:
+
+```k
+  syntax Bytes ::= REF_NULL   [macro] rule REF_NULL   => b"xD0"
+                 | REF_ISNULL [macro] rule REF_ISNULL => b"xD1"
+                 | REF_FUNC   [macro] rule REF_FUNC   => b"xD2"
+```
+
+_Variable instructions_ are encoded with the following tags:
+
+```k
+  syntax Bytes ::= LOCAL_GET  [macro] rule LOCAL_GET  => b"x20"
+                 | LOCAL_SET  [macro] rule LOCAL_SET  => b"x21"
+                 | LOCAL_TEE  [macro] rule LOCAL_TEE  => b"x22"
+                 | GLOBAL_GET [macro] rule GLOBAL_GET => b"x23"
+                 | GLOBAL_SET [macro] rule GLOBAL_SET => b"x24"
+```
+
+_Table instructions_ are encoded with the following tags:
+
+```k
+  syntax Bytes ::= TABLE_GET  [macro] rule TABLE_GET  => b"x25"
+                 | TABLE_SET  [macro] rule TABLE_SET  => b"x26"
+                 | TABLE_INIT [macro] rule TABLE_INIT => b"xFCx0C"
+                 | ELEM_DROP  [macro] rule ELEM_DROP  => b"xFCx0D"
+                 | TABLE_COPY [macro] rule TABLE_COPY => b"xFCx0E"
+                 | TABLE_GROW [macro] rule TABLE_GROW => b"xFCx0F"
+                 | TABLE_SIZE [macro] rule TABLE_SIZE => b"xFCx10"
+                 | TABLE_FILL [macro] rule TABLE_FILL => b"xFCx11"
+```
+
+_Memory instructions_ are encoded with the following tags:
+
+```k
+                 | I32_LOAD      [macro] rule I32_LOAD      => b"x28"
+                 | I64_LOAD      [macro] rule I64_LOAD      => b"x29"
+                 | F32_LOAD      [macro] rule F32_LOAD      => b"x2A"
+                 | F64_LOAD      [macro] rule F64_LOAD      => b"x2B"
+                 | I32_LOAD_8_S  [macro] rule I32_LOAD_8_S  => b"x2C"
+                 | I32_LOAD_8_U  [macro] rule I32_LOAD_8_U  => b"x2D"
+                 | I32_LOAD_16_S [macro] rule I32_LOAD_16_S => b"x2E"
+                 | I32_LOAD_16_U [macro] rule I32_LOAD_16_U => b"x2F"
+                 | I64_LOAD_8_S  [macro] rule I64_LOAD_8_S  => b"x30"
+                 | I64_LOAD_8_U  [macro] rule I64_LOAD_8_U  => b"x31"
+                 | I64_LOAD_16_S [macro] rule I64_LOAD_16_S => b"x32"
+                 | I64_LOAD_16_U [macro] rule I64_LOAD_16_U => b"x33"
+                 | I64_LOAD_32_S [macro] rule I64_LOAD_32_S => b"x34"
+                 | I64_LOAD_32_U [macro] rule I64_LOAD_32_U => b"x35"
+                 | I32_STORE     [macro] rule I32_STORE     => b"x36"
+                 | I64_STORE     [macro] rule I64_STORE     => b"x37"
+                 | F32_STORE     [macro] rule F32_STORE     => b"x38"
+                 | F64_STORE     [macro] rule F64_STORE     => b"x39"
+                 | I32_STORE_8   [macro] rule I32_STORE_8   => b"x3A"
+                 | I32_STORE_16  [macro] rule I32_STORE_16  => b"x3B"
+                 | I64_STORE_8   [macro] rule I64_STORE_8   => b"x3C"
+                 | I64_STORE_16  [macro] rule I64_STORE_16  => b"x3D"
+                 | I64_STORE_32  [macro] rule I64_STORE_32  => b"x3E"
+                 | MEM_SIZE      [macro] rule MEM_SIZE      => b"x3F"
+                 | MEM_GROW      [macro] rule MEM_GROW      => b"x40"
+                 | MEM_INIT      [macro] rule MEM_INIT      => b"xFCx08"
+                 | DATA_DROP     [macro] rule DATA_DROP     => b"xFCx09"
+                 | MEM_COPY      [macro] rule MEM_COPY      => b"xFCx0A"
+                 | MEM_FILL      [macro] rule MEM_FILL      => b"xFCx0B"
+```
+
+_Numeric instructions_ have the following tags:
+
+```k
+                 | I32_CONST           [macro] rule I32_CONST => b"x41"
+                 | I64_CONST           [macro] rule I64_CONST => b"x42"
+                 | F32_CONST           [macro] rule F32_CONST => b"x43"
+                 | F64_CONST           [macro] rule F64_CONST => b"x44"
+
+                 | I32_EQZ             [macro] rule I32_EQZ  => b"x45"
+                 | I32_EQ              [macro] rule I32_EQ   => b"x46"
+                 | I32_NE              [macro] rule I32_NE   => b"x47"
+                 | I32_LT_S            [macro] rule I32_LT_S => b"x48"
+                 | I32_LT_U            [macro] rule I32_LT_U => b"x49"
+                 | I32_GT_S            [macro] rule I32_GT_S => b"x4A"
+                 | I32_GT_U            [macro] rule I32_GT_U => b"x4B"
+                 | I32_LE_S            [macro] rule I32_LE_S => b"x4C"
+                 | I32_LE_U            [macro] rule I32_LE_U => b"x4D"
+                 | I32_GE_S            [macro] rule I32_GE_S => b"x4E"
+                 | I32_GE_U            [macro] rule I32_GE_U => b"x4F"
+
+                 | I64_EQZ             [macro] rule I64_EQZ  => b"x50"
+                 | I64_EQ              [macro] rule I64_EQ   => b"x51"
+                 | I64_NE              [macro] rule I64_NE   => b"x52"
+                 | I64_LT_S            [macro] rule I64_LT_S => b"x53"
+                 | I64_LT_U            [macro] rule I64_LT_U => b"x54"
+                 | I64_GT_S            [macro] rule I64_GT_S => b"x55"
+                 | I64_GT_U            [macro] rule I64_GT_U => b"x56"
+                 | I64_LE_S            [macro] rule I64_LE_S => b"x57"
+                 | I64_LE_U            [macro] rule I64_LE_U => b"x58"
+                 | I64_GE_S            [macro] rule I64_GE_S => b"x59"
+                 | I64_GE_U            [macro] rule I64_GE_U => b"x5A"
+
+                 | F32_EQ              [macro] rule F32_EQ => b"x5B"
+                 | F32_NE              [macro] rule F32_NE => b"x5C"
+                 | F32_LT              [macro] rule F32_LT => b"x5D"
+                 | F32_GT              [macro] rule F32_GT => b"x5E"
+                 | F32_LE              [macro] rule F32_LE => b"x5F"
+                 | F32_GE              [macro] rule F32_GE => b"x60"
+
+                 | F64_EQ              [macro] rule F64_EQ => b"x61"
+                 | F64_NE              [macro] rule F64_NE => b"x62"
+                 | F64_LT              [macro] rule F64_LT => b"x63"
+                 | F64_GT              [macro] rule F64_GT => b"x64"
+                 | F64_LE              [macro] rule F64_LE => b"x65"
+                 | F64_GE              [macro] rule F64_GE => b"x66"
+
+                 | I32_CLZ             [macro]
+                 | I32_CTZ             [macro]
+                 | I32_POPCNT          [macro]
+                 | I32_ADD             [macro]
+                 | I32_SUB             [macro]
+                 | I32_MUL             [macro]
+                 | I32_DIV_S           [macro]
+                 | I32_DIV_U           [macro]
+                 | I32_REM_S           [macro]
+                 | I32_REM_U           [macro]
+                 | I32_AND             [macro]
+                 | I32_OR              [macro]
+                 | I32_XOR             [macro]
+                 | I32_SHL             [macro]
+                 | I32_SHR_S           [macro]
+                 | I32_SHR_U           [macro]
+                 | I32_ROTL            [macro]
+                 | I32_ROTR            [macro]
+
+                 | I64_CLZ             [macro]
+                 | I64_CTZ             [macro]
+                 | I64_POPCNT          [macro]
+                 | I64_ADD             [macro]
+                 | I64_SUB             [macro]
+                 | I64_MUL             [macro]
+                 | I64_DIV_S           [macro]
+                 | I64_DIV_U           [macro]
+                 | I64_REM_S           [macro]
+                 | I64_REM_U           [macro]
+                 | I64_AND             [macro]
+                 | I64_OR              [macro]
+                 | I64_XOR             [macro]
+                 | I64_SHL             [macro]
+                 | I64_SHR_S           [macro]
+                 | I64_SHR_U           [macro]
+                 | I64_ROTL            [macro]
+                 | I64_ROTR            [macro]
+
+                 | F32_ABS             [macro]
+                 | F32_NEG             [macro]
+                 | F32_CEIL            [macro]
+                 | F32_FLOOR           [macro]
+                 | F32_TRUNC           [macro]
+                 | F32_NEARSET         [macro]
+                 | F32_SQRT            [macro]
+                 | F32_ADD             [macro]
+                 | F32_SUB             [macro]
+                 | F32_MUL             [macro]
+                 | F32_DIV             [macro]
+                 | F32_MIN             [macro]
+                 | F32_MAX             [macro]
+                 | F32_COPYSIGN        [macro]
+
+                 | F64_ABS             [macro]
+                 | F64_NEG             [macro]
+                 | F64_CEIL            [macro]
+                 | F64_FLOOR           [macro]
+                 | F64_TRUNC           [macro]
+                 | F64_NEARSET         [macro]
+                 | F64_SQRT            [macro]
+                 | F64_ADD             [macro]
+                 | F64_SUB             [macro]
+                 | F64_MUL             [macro]
+                 | F64_DIV             [macro]
+                 | F64_MIN             [macro]
+                 | F64_MAX             [macro]
+                 | F64_COPYSIGN        [macro]
+
+                 | I32_WRAP_I64        [macro]
+                 | I32_TRUNC_F32_S     [macro]
+                 | I32_TRUNC_F32_U     [macro]
+                 | I32_TRUNC_F64_S     [macro]
+                 | I32_TRUNC_F64_U     [macro]
+
+                 | I64_EXTEND_I32_S    [macro]
+                 | I64_EXTEND_I32_U    [macro]
+                 | I64_TRUNC_F32_S     [macro]
+                 | I64_TRUNC_F32_U     [macro]
+                 | I64_TRUNC_F64_S     [macro]
+                 | I64_TRUNC_F64_U     [macro]
+
+                 | F32_CONVERT_I32_S   [macro]
+                 | F32_CONVERT_I32_U   [macro]
+                 | F32_CONVERT_I64_S   [macro]
+                 | F32_CONVERT_I64_U   [macro]
+                 | F32_DEMOTE_F64      [macro]
+
+                 | F64_CONVERT_I32_S   [macro]
+                 | F64_CONVERT_I32_U   [macro]
+                 | F64_CONVERT_I64_S   [macro]
+                 | F64_CONVERT_I64_U   [macro]
+                 | F64_PROMOTE_F32     [macro]
+
+                 | I32_REINTERPRET_F32 [macro]
+                 | I64_REINTERPRET_F64 [macro]
+                 | F32_REINTERPRET_I32 [macro]
+                 | F64_REINTERPRET_I64 [macro]
+
+                 | I32_EXTEND_8_S      [macro]
+                 | I32_EXTEND_16_S     [macro]
+                 | I64_EXTEND_8_S      [macro]
+                 | I64_EXTEND_16_S     [macro]
+                 | I64_EXTEND_32_S     [macro]
+```
+
+```k
+endmodule
+```
+
+module BINARY_PARSER [private]
+  imports WASM
+  imports BINARY_PARSER_DATA
+
+  syntax ParseResult ::= ModuleDecl
+                       | ParseError(String)
+
+
+  syntax ModuleDecl ::= parseModule(Bytes)  [function, total]
+                      | parseMagic(Bytes)   [function, total]
+                      | parseVersion(Bytes) [function, total]
+
+endmodule

From c4ce869cd46ab2c31683ddd96809a764f5339bdd Mon Sep 17 00:00:00 2001
From: Stephen Skeirik <stephen.skeirik@runtimeverification.com>
Date: Mon, 6 Jan 2025 00:20:54 -0600
Subject: [PATCH 2/9] add partial counter contract

---
 tests/ulm/counter/rust/.gitignore             |   1 +
 tests/ulm/counter/rust/Cargo.lock             | 130 ++++++
 tests/ulm/counter/rust/Cargo.toml             |  26 ++
 tests/ulm/counter/rust/README.md              |  23 +
 tests/ulm/counter/rust/build.sh               |   7 +
 tests/ulm/counter/rust/src/address.rs         |  99 +++++
 tests/ulm/counter/rust/src/assertions.rs      |  15 +
 tests/ulm/counter/rust/src/contract.rs        |  37 ++
 .../counter/rust/src/contract_dispatcher.rs   |  75 ++++
 tests/ulm/counter/rust/src/decoder.rs         | 114 +++++
 tests/ulm/counter/rust/src/encoder.rs         | 102 +++++
 tests/ulm/counter/rust/src/lib.rs             |  10 +
 tests/ulm/counter/rust/src/predicate.rs       |   1 +
 tests/ulm/counter/rust/src/storage.rs         | 106 +++++
 tests/ulm/counter/rust/src/ulm.rs             | 287 ++++++++++++
 tests/ulm/counter/rust/src/unsigned.rs        | 407 ++++++++++++++++++
 16 files changed, 1440 insertions(+)
 create mode 100644 tests/ulm/counter/rust/.gitignore
 create mode 100644 tests/ulm/counter/rust/Cargo.lock
 create mode 100644 tests/ulm/counter/rust/Cargo.toml
 create mode 100644 tests/ulm/counter/rust/README.md
 create mode 100755 tests/ulm/counter/rust/build.sh
 create mode 100644 tests/ulm/counter/rust/src/address.rs
 create mode 100644 tests/ulm/counter/rust/src/assertions.rs
 create mode 100644 tests/ulm/counter/rust/src/contract.rs
 create mode 100644 tests/ulm/counter/rust/src/contract_dispatcher.rs
 create mode 100644 tests/ulm/counter/rust/src/decoder.rs
 create mode 100644 tests/ulm/counter/rust/src/encoder.rs
 create mode 100644 tests/ulm/counter/rust/src/lib.rs
 create mode 100644 tests/ulm/counter/rust/src/predicate.rs
 create mode 100644 tests/ulm/counter/rust/src/storage.rs
 create mode 100644 tests/ulm/counter/rust/src/ulm.rs
 create mode 100644 tests/ulm/counter/rust/src/unsigned.rs

diff --git a/tests/ulm/counter/rust/.gitignore b/tests/ulm/counter/rust/.gitignore
new file mode 100644
index 000000000..9f970225a
--- /dev/null
+++ b/tests/ulm/counter/rust/.gitignore
@@ -0,0 +1 @@
+target/
\ No newline at end of file
diff --git a/tests/ulm/counter/rust/Cargo.lock b/tests/ulm/counter/rust/Cargo.lock
new file mode 100644
index 000000000..f525d446c
--- /dev/null
+++ b/tests/ulm/counter/rust/Cargo.lock
@@ -0,0 +1,130 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "bumpalo"
+version = "3.16.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c"
+
+[[package]]
+name = "bytes"
+version = "1.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "325918d6fe32f23b19878fe4b34794ae41fc19ddbe53b10571a4874d44ffd39b"
+
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
+[[package]]
+name = "counter"
+version = "0.1.0"
+dependencies = [
+ "bytes",
+ "wasm-bindgen",
+]
+
+[[package]]
+name = "log"
+version = "0.4.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
+
+[[package]]
+name = "once_cell"
+version = "1.20.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.92"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.90"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83"
+
+[[package]]
+name = "wasm-bindgen"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a474f6281d1d70c17ae7aa6a613c87fce69a127e2624002df63dcb39d6cf6396"
+dependencies = [
+ "cfg-if",
+ "once_cell",
+ "wasm-bindgen-macro",
+]
+
+[[package]]
+name = "wasm-bindgen-backend"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f89bb38646b4f81674e8f5c3fb81b562be1fd936d84320f3264486418519c79"
+dependencies = [
+ "bumpalo",
+ "log",
+ "proc-macro2",
+ "quote",
+ "syn",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-macro"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2cc6181fd9a7492eef6fef1f33961e3695e4579b9872a6f7c83aee556666d4fe"
+dependencies = [
+ "quote",
+ "wasm-bindgen-macro-support",
+]
+
+[[package]]
+name = "wasm-bindgen-macro-support"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "30d7a95b763d3c45903ed6c81f156801839e5ee968bb07e534c44df0fcd330c2"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "wasm-bindgen-backend",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-shared"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "943aab3fdaaa029a6e0271b35ea10b72b943135afe9bffca82384098ad0e06a6"
diff --git a/tests/ulm/counter/rust/Cargo.toml b/tests/ulm/counter/rust/Cargo.toml
new file mode 100644
index 000000000..1ccaa009c
--- /dev/null
+++ b/tests/ulm/counter/rust/Cargo.toml
@@ -0,0 +1,26 @@
+[package]
+name = "counter"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+crate-type = ["cdylib"]
+
+[dependencies]
+wasm-bindgen = "0.2"
+bytes = "1.9"
+
+#[profile.dev]
+#panic = "abort"
+
+[profile.release]
+# this flag removes debug symbols
+strip = true
+# this flag and the one below optimizes for size, experiment with both and find the one that works better!
+# opt-level = "z"
+opt-level = "s"
+# the flags below instruct the compiler to try harder to do whole-program optimization
+lto = true
+codegen-units = 1
+# this flag tells the compiler to replace helpful debug behavior with calls to abort
+panic = "abort"
diff --git a/tests/ulm/counter/rust/README.md b/tests/ulm/counter/rust/README.md
new file mode 100644
index 000000000..3732105f1
--- /dev/null
+++ b/tests/ulm/counter/rust/README.md
@@ -0,0 +1,23 @@
+# Rust/Wasm ERC20 Contract
+
+This directory contains a Rust implementation of an ERC20 contract that is compiled into Wasm.
+
+As is the case with many chains that use Wasm contracts, we compile this Rust project as a library;
+that way, functions referenced in external libraries become host functions which can be provided via Wasm module imports.
+
+In order to reduce the size of the compiled Wasm library, we referred to this guide:
+
+https://github.com/johnthagen/min-sized-rust
+
+To build the contract with all of the size minimization options, first, ensure that a recent build of the Rust compiler is installed with the Wasm32 target, which can be done with:
+
+```sh
+rustup install nightly
+rustup target add wasm32-unknown-unknown --toolchain nightly
+```
+
+Then run the build script as follows:
+
+```sh
+build.sh
+```
diff --git a/tests/ulm/counter/rust/build.sh b/tests/ulm/counter/rust/build.sh
new file mode 100755
index 000000000..2032a2de5
--- /dev/null
+++ b/tests/ulm/counter/rust/build.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+LOC_FLAG="-Zlocation-detail=none" # removes debugging info from binary
+FMT_FLAG="-Zfmt-debug=none"       # removes formatter code from binary
+# the last two lines build stdlib for target with minimal panic handling and optimized for size
+RUSTFLAGS="$LOC_FLAG $FMT_FLAG" cargo +nightly build --release --target wasm32-unknown-unknown \
+-Z build-std=std,panic_abort                                                                   \
+-Z build-std-features="optimize_for_size,panic_immediate_abort"
diff --git a/tests/ulm/counter/rust/src/address.rs b/tests/ulm/counter/rust/src/address.rs
new file mode 100644
index 000000000..60e2baa6b
--- /dev/null
+++ b/tests/ulm/counter/rust/src/address.rs
@@ -0,0 +1,99 @@
+use bytes::Bytes;
+use core::cmp::Ordering;
+
+use crate::decoder::Decodable;
+use crate::encoder::{Encodable, EncodingType};
+use crate::unsigned::{U160, U256};
+
+#[derive(Debug)]
+pub struct Address {
+    value: U160,
+}
+
+impl Address {
+    fn new(value: U160) -> Self {
+        Address { value }
+    }
+
+    pub fn zero() -> Self {
+        Address::new(U160::from_u64(0))
+    }
+
+    pub fn is_zero(&self) -> bool {
+        self.value == U160::from_u64(0)
+    }
+
+    pub fn into_u160(self) -> U160 {
+      self.value
+    }
+    pub fn into_u256(self) -> U256 {
+        self.value.into()
+    }
+}
+
+impl From<U160> for Address
+{
+    fn from(value: U160) -> Self {
+        Address::new(value)
+    }
+}
+impl TryFrom<U256> for Address
+{
+    type Error = &'static str;
+    fn try_from(value: U256) -> Result<Self, Self::Error> {
+        Ok(Address::new(value.try_into()?))
+    }
+}
+impl From<Address> for U160
+{
+    fn from(value: Address) -> Self {
+        value.into_u160()
+    }
+}
+impl From<Address> for U256
+{
+    fn from(value: Address) -> Self {
+        value.into_u256()
+    }
+}
+
+impl Ord for Address {
+    fn cmp(&self, other: &Self) -> Ordering {
+        self.value.cmp(&other.value)
+    }
+}
+impl PartialOrd for Address {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+impl PartialEq for Address {
+    fn eq(&self, other: &Self) -> bool {
+        self.cmp(other) == Ordering::Equal
+    }
+}
+impl Eq for Address {}
+impl Clone for Address {
+    fn clone(&self) -> Self {
+        Address { value: self.value.clone() }
+    }
+}
+
+impl Encodable for Address
+{
+    fn encode(&self) -> (EncodingType, Bytes) {
+        self.value.encode()
+    }
+}
+impl Decodable for Address
+{
+    fn encoding_type() -> EncodingType {
+        U160::encoding_type()
+    }
+    fn head_size() -> usize {
+        U160::head_size()
+    }
+    fn decode(bytes: Bytes) -> Self {
+        Address::new(U160::decode(bytes))
+    }
+}
diff --git a/tests/ulm/counter/rust/src/assertions.rs b/tests/ulm/counter/rust/src/assertions.rs
new file mode 100644
index 000000000..e83a5a14c
--- /dev/null
+++ b/tests/ulm/counter/rust/src/assertions.rs
@@ -0,0 +1,15 @@
+
+use crate::ulm;
+
+pub fn fail(msg: &str) -> ! {
+  ulm::failWrapper(msg);
+}
+
+#[macro_export]
+macro_rules! require {
+  ( $cond:expr , $msg:expr ) => {
+      if ! $cond {
+          fail($msg);
+      }
+  }
+}
diff --git a/tests/ulm/counter/rust/src/contract.rs b/tests/ulm/counter/rust/src/contract.rs
new file mode 100644
index 000000000..6e8bef6b1
--- /dev/null
+++ b/tests/ulm/counter/rust/src/contract.rs
@@ -0,0 +1,37 @@
+use std::cell::RefCell;
+use std::rc::Rc;
+
+use crate::storage::{SingleChunkStorage, SingleChunkStorageBuilder};
+use crate::ulm::Ulm;
+use crate::unsigned::U256;
+
+pub struct Contract {
+  api: Rc<RefCell<dyn Ulm>>
+}
+
+impl Contract {
+    pub fn new(api: Rc<RefCell<dyn Ulm>>) -> Self {
+        Contract { api }
+    }
+
+    // ---------------------------
+
+    fn s_counter<'a>(&self) -> SingleChunkStorage<'a, U256> {
+        SingleChunkStorageBuilder::new(self.api.clone(), &("counter".to_string())).build()
+    }
+
+    // ---------------------------
+
+    pub fn init(&self) {
+        self.s_counter().set(U256::from_u64(0));
+    }
+
+    pub fn inc_counter(&self) -> bool {
+        self.s_counter().set(self.s_counter().get() + U256::from_u64(1));
+        true
+    }
+
+    pub fn get_counter(&self) -> U256 {
+        self.s_counter().get()
+    }
+}
diff --git a/tests/ulm/counter/rust/src/contract_dispatcher.rs b/tests/ulm/counter/rust/src/contract_dispatcher.rs
new file mode 100644
index 000000000..4e7e294a2
--- /dev/null
+++ b/tests/ulm/counter/rust/src/contract_dispatcher.rs
@@ -0,0 +1,75 @@
+use bytes::Bytes;
+use core::cell::RefCell;
+use std::rc::Rc;
+
+use crate::assertions::fail;
+use crate::decoder::Decoder;
+use crate::encoder::Encoder;
+use crate::contract::Contract;
+use crate::require;
+use crate::ulm;
+use crate::unsigned::U256;
+
+fn same_signature(api: &dyn ulm::Ulm, expected: &Bytes, signature: &str) -> bool {
+    expected == &Bytes::copy_from_slice(&ulm::endpoint_fingerprint(api, signature))
+}
+
+#[cfg(not(test))]
+#[no_mangle]
+#[allow(non_snake_case)]
+pub fn ulmDispatchCaller(init: bool) {
+    dispatch(ulm::impl_::UlmImpl::new(), init);
+}
+
+fn dispatch(api: Rc<RefCell<dyn ulm::Ulm>>, init: bool) {
+    let mut buffer = ulm::call_data(&*api.borrow());
+    if init {
+        initCaller(api, buffer);
+    } else {
+        require!(buffer.len() >= 4, "Buffer without function signature");
+        let arguments = buffer.split_off(4);
+        let signature = buffer;
+        if same_signature(&*api.borrow(), &signature, "incCounter()") {
+            incCaller(api, arguments);
+        } else if same_signature(&*api.borrow(), &signature, "getCounter()") {
+            getCaller(api, arguments);
+        } else {
+            fail("Unknown endpoint");
+        }
+    }
+}
+
+#[allow(non_snake_case)]
+fn initCaller(api: Rc<RefCell<dyn ulm::Ulm>>, arguments: Bytes) {
+    let decoder: Decoder<()> = Decoder::from_buffer(arguments);
+    decoder.check_done();
+
+    let contract = Contract::new(api.clone());
+    contract.init();
+}
+
+#[allow(non_snake_case)]
+fn incCaller(api: Rc<RefCell<dyn ulm::Ulm>>, arguments: Bytes) {
+    let decoder: Decoder<()> = Decoder::from_buffer(arguments);
+    decoder.check_done();
+
+    let contract = Contract::new(api.clone());
+    let result = contract.inc_counter();
+
+    let mut encoder = Encoder::new();
+    encoder.add(&U256::from_bool(result));
+    ulm::set_output(&mut *api.borrow_mut(), &encoder.encode());
+}
+
+#[allow(non_snake_case)]
+fn getCaller(api: Rc<RefCell<dyn ulm::Ulm>>, arguments: Bytes) {
+    let decoder: Decoder<()> = Decoder::from_buffer(arguments);
+    decoder.check_done();
+
+    let contract = Contract::new(api.clone());
+    let counter = contract.get_counter();
+
+    let mut encoder = Encoder::new();
+    encoder.add(&counter);
+    ulm::set_output(&mut *api.borrow_mut(), &encoder.encode());
+}
diff --git a/tests/ulm/counter/rust/src/decoder.rs b/tests/ulm/counter/rust/src/decoder.rs
new file mode 100644
index 000000000..5bff0462e
--- /dev/null
+++ b/tests/ulm/counter/rust/src/decoder.rs
@@ -0,0 +1,114 @@
+// Decodes values according to the solidity ABI:
+// https://docs.soliditylang.org/en/latest/abi-spec.html
+//
+// To decode, first implement the Decodable trait for the types you want to
+// decode. Then create the decoder. Note that, if you want to decode n values,
+// you have to provide the types for all n values in a tuple-based list that
+// ends with ().
+//
+// let decoder: Decoder<(Type_1, (Type_2, (..., (Type_n, ())...)))>
+//
+// Then you can decode the actual values. Note that decoding a value provides
+// a new decoder, which you must use in order to decode the subsequent values.
+//
+// let (value_1, decoder) = decoder.decode();
+// let (value_2, decoder) = decoder.decode();
+// ...
+// let (value_n, decoder) = decoder.decode();
+//
+// At the end, it's good practice to check that you have decoded everything
+// you wanted. The following will not compile if decoding didn't finish.
+//
+// decoder.check_done();
+
+use bytes::{Bytes, Buf};
+use core::marker::PhantomData;
+
+use crate::assertions::fail;
+use crate::require;
+use crate::unsigned::U256;
+use crate::encoder::EncodingType;
+
+pub trait Decodable {
+    fn encoding_type() -> EncodingType;
+    fn head_size() -> usize;
+    fn decode(bytes: Bytes) -> Self;
+}
+
+impl Decodable for String {
+    fn encoding_type() -> EncodingType {
+        EncodingType::VariableSize
+    }
+    fn head_size() -> usize {
+        32
+    }
+    fn decode(bytes: Bytes) -> Self {
+        let decoded = String::from_utf8(bytes.chunk().to_vec());
+        match decoded {
+            Ok(v) => v,
+            Err(_) => fail("utf8 decoding error"),
+        }
+    }
+}
+
+pub struct Decoder<'a, T> {
+    phantom: PhantomData<&'a T>,
+    buffer: Bytes,
+    next_value_head: usize,
+}
+
+impl<'a, T> Decoder<'a, T> {
+    pub fn from_buffer(buffer: Bytes) -> Decoder<'a, T> {
+        Decoder {
+            phantom: PhantomData,
+            buffer,
+            next_value_head: 0,
+        }
+    }
+}
+
+impl<'a> Decoder<'a, ()> {
+    pub fn check_done(&self) {
+    }
+}
+
+impl<'a, S, T> Decoder<'a, (S, T)>
+    where S:Decodable
+{
+    pub fn decode(self) -> (S, Decoder<'a, T>) {
+        let head_size =
+            match S::encoding_type() {
+                EncodingType::VariableSize => 32,
+                EncodingType::FixedSize => S::head_size(),
+            };
+        let current_value_head = self.next_value_head;
+        let next_value_head = current_value_head + head_size;
+        let head = self.buffer.slice(current_value_head .. next_value_head);
+        let encoded_value =
+            match S::encoding_type() {
+                EncodingType::FixedSize => head,
+                EncodingType::VariableSize => {
+                    let value_start_u256 = U256::decode(head);
+                    let value_start: usize = match value_start_u256.try_into() {
+                        Ok(v) => v,
+                        Err(s) => fail(s),
+                    };
+                    require!(value_start + 32 <= self.buffer.len(), "Value index out of range");
+                    let value_length_u256 = U256::decode(self.buffer.slice(value_start .. value_start + 32));
+                    let value_length: usize = match value_length_u256.try_into() {
+                        Ok(v) => v,
+                        Err(s) => fail(s),
+                    };
+                    require!(value_start + 32 + value_length < self.buffer.len(), "Value end out of range");
+                    self.buffer.slice(value_start + 32 .. value_start + 32 + value_length)
+                },
+            };
+        let decoded_value = S::decode(encoded_value);
+        let decoder = Decoder::<T> {
+            phantom: PhantomData,
+            buffer: self.buffer,
+            next_value_head,
+        };
+        (decoded_value, decoder)
+    }
+}
diff --git a/tests/ulm/counter/rust/src/encoder.rs b/tests/ulm/counter/rust/src/encoder.rs
new file mode 100644
index 000000000..82f0879f7
--- /dev/null
+++ b/tests/ulm/counter/rust/src/encoder.rs
@@ -0,0 +1,102 @@
+// Encodes values according to the solidity ABI:
+// https://docs.soliditylang.org/en/latest/abi-spec.html
+//
+// To encode, first implement the Encodable trait for the types you want to
+// encode. Then do something like this:
+//
+// let mut encoder = Encoder::new();
+// encoder.add(value_1);
+// encoder.add(value_2);
+// ...
+// encoder.add(value_n);
+// let encoded = encoder.encode();
+
+use bytes::{Bytes, BytesMut, BufMut, Buf};
+
+use crate::unsigned::U256;
+
+pub enum EncodingType {
+    FixedSize = 1,
+    VariableSize = 2,
+}
+
+pub trait Encodable {
+    fn encode(&self) -> (EncodingType, Bytes);
+}
+
+impl Encodable for String {
+    fn encode(&self) -> (EncodingType, Bytes) {
+        let bytes = self.as_bytes();
+        let total_bytes_length = 32 + ((bytes.len() + 31) / 32) * 32;
+        let mut result = BytesMut::with_capacity(total_bytes_length);
+        let (_, len_bytes) = U256::from_u64(bytes.len() as u64).encode();
+
+        result.put(len_bytes);
+        result.put(bytes);
+        for _ in result.len() .. total_bytes_length {
+            result.put_u8(0_u8);
+        }
+
+        (EncodingType::VariableSize, result.freeze())
+    }
+}
+
+pub struct Encoder {
+    objects: Vec<(EncodingType, Bytes)>,
+}
+
+impl Encoder {
+    pub fn new() -> Self {
+        Encoder { objects: Vec::new() }
+    }
+
+    pub fn add(&mut self, value: &dyn Encodable) {
+        self.objects.push(value.encode());
+    }
+
+    pub fn encode(&self) -> Bytes {
+        let head_size = self.head_size();
+        let tail_size = self.tail_size();
+        let mut prefix = BytesMut::with_capacity(head_size + tail_size);
+        let mut suffix = BytesMut::with_capacity(tail_size);
+        for (encoding_type, bytes) in self.objects.iter() {
+            match encoding_type {
+                EncodingType::FixedSize => prefix.extend_from_slice(bytes),
+                EncodingType::VariableSize => {
+                    let before_size = head_size + suffix.len();
+                    let (_, prefix_chunk) = U256::from_u64(before_size as u64).encode();
+                    prefix.put(prefix_chunk);
+                    suffix.put(bytes.chunk());
+                },
+            }
+        }
+        prefix.put(suffix);
+        prefix.freeze()
+    }
+
+    fn head_size(&self) -> usize {
+        let mut size = 0_usize;
+        for (encoding_type, bytes) in self.objects.iter() {
+            let current_size =
+                match encoding_type {
+                    EncodingType::FixedSize => bytes.len(),
+                    EncodingType::VariableSize => 32,
+                };
+            size += current_size;
+        }
+        size
+    }
+
+    fn tail_size(&self) -> usize {
+        let mut size = 0_usize;
+        for (encoding_type, bytes) in self.objects.iter() {
+            let current_size =
+                match encoding_type {
+                    EncodingType::FixedSize => 0,
+                    EncodingType::VariableSize => bytes.len(),
+                };
+            size += current_size;
+        }
+        size
+    }
+}
diff --git a/tests/ulm/counter/rust/src/lib.rs b/tests/ulm/counter/rust/src/lib.rs
new file mode 100644
index 000000000..4c34fbfc7
--- /dev/null
+++ b/tests/ulm/counter/rust/src/lib.rs
@@ -0,0 +1,10 @@
+mod address;
+mod assertions;
+mod decoder;
+mod encoder;
+mod contract;
+mod contract_dispatcher;
+mod predicate;
+mod storage;
+mod unsigned;
+mod ulm;
diff --git a/tests/ulm/counter/rust/src/predicate.rs b/tests/ulm/counter/rust/src/predicate.rs
new file mode 100644
index 000000000..9fdd9b735
--- /dev/null
+++ b/tests/ulm/counter/rust/src/predicate.rs
@@ -0,0 +1 @@
+pub trait Satisfied {}
diff --git a/tests/ulm/counter/rust/src/storage.rs b/tests/ulm/counter/rust/src/storage.rs
new file mode 100644
index 000000000..9332d5876
--- /dev/null
+++ b/tests/ulm/counter/rust/src/storage.rs
@@ -0,0 +1,106 @@
+// SingleChunkStorage is a class which makes it easy to work with storage
+// for objects that fit in 32 bytes. Accessing storage will crash (fail) if
+// the stored bytes cannot be converted to the value type.
+//
+// Let's say you want to access a storage object under the name N, with
+// key (K1, K2, ..., Kn) and with type T. You need the following:
+// * K1 ..., Kn must implement Encodable
+// * T must implement TryFrom<U256> and Into<U256>
+//
+// Then you can build the storage object like this:
+//
+// let mut builder = SingleChunkStorageBuilder::<MyValueType>::new(api, hooks_api, &("Storage name".to_string()))
+// builder.add_arg(K1);
+// builder.add_arg(K2);
+// ...
+// builder.add_arg(Kn);
+// let mut storage = builder.build();
+//
+// In order to set the storage value, do this:
+//
+// storage.set(&my_value);
+//
+// In order to get the stored value, do this:
+//
+// let my_value = storage.get();
+
+use core::marker::PhantomData;
+use std::cell::RefCell;
+use std::convert::TryFrom;
+use std::convert::Into;
+use std::rc::Rc;
+
+use crate::assertions::fail;
+use crate::encoder::Encodable;
+use crate::encoder::Encoder;
+use crate::unsigned::U256;
+use crate::ulm;
+
+pub struct SingleChunkStorage<'a, ValueType>
+    where
+        ValueType: Into<U256> + TryFrom<U256>,
+{
+    phantom_value: PhantomData<&'a ValueType>,
+    api: Rc<RefCell<dyn ulm::Ulm>>,
+    fingerprint: U256,
+}
+
+impl<'a, ValueType> SingleChunkStorage<'a, ValueType>
+    where
+        ValueType: Into<U256> + TryFrom<U256>,
+{
+    pub fn new(api: Rc<RefCell<dyn ulm::Ulm>>, fingerprint: U256) -> Self {
+        SingleChunkStorage::<ValueType> { phantom_value: PhantomData, api, fingerprint }
+    }
+
+    pub fn set(&mut self, value: ValueType) {
+        let converted: U256 = value.into();
+        ulm::set_account_storage(&mut *self.api.borrow_mut(), &self.fingerprint, &converted);
+    }
+
+    pub fn get(&self) -> ValueType {
+        let u256 = ulm::get_account_storage(&*self.api.borrow(), &self.fingerprint);
+        match u256.try_into() {
+            Ok(v) => v,
+            Err(_) => fail("Conversion from U256 failed for storage"),
+        }
+    }
+}
+
+pub struct SingleChunkStorageBuilder<'a, ValueType>
+    where
+        ValueType: Into<U256> + TryFrom<U256>,
+{
+    phantom_value: PhantomData<&'a ValueType>,
+    api: Rc<RefCell<dyn ulm::Ulm>>,
+    encoder: Encoder,
+}
+
+impl<'a, ValueType> SingleChunkStorageBuilder<'a, ValueType>
+    where
+        ValueType: Into<U256> + TryFrom<U256>,
+{
+    pub fn new(api: Rc<RefCell<dyn ulm::Ulm>>, name: &String) -> Self {
+        let mut encoder = Encoder::new();
+        encoder.add(name);
+        Self::from_encoder(api, encoder)
+    }
+
+    fn from_encoder(api: Rc<RefCell<dyn ulm::Ulm>>, encoder: Encoder) -> Self {
+        SingleChunkStorageBuilder::<ValueType> {
+            phantom_value: PhantomData,
+            api,
+            encoder,
+        }
+    }
+
+    pub fn add_arg(&mut self, arg: &dyn Encodable) {
+        self.encoder.add(arg);
+    }
+
+    pub fn build(self) -> SingleChunkStorage<'a, ValueType> {
+        let bytes = self.encoder.encode();
+        let fingerprint = ulm::keccak_hash_int(&*self.api.borrow(), &bytes);
+        SingleChunkStorage::new(self.api, fingerprint)
+    }
+}
diff --git a/tests/ulm/counter/rust/src/ulm.rs b/tests/ulm/counter/rust/src/ulm.rs
new file mode 100644
index 000000000..16f2aa567
--- /dev/null
+++ b/tests/ulm/counter/rust/src/ulm.rs
@@ -0,0 +1,287 @@
+use bytes::{Bytes, Buf};
+
+use crate::address::Address;
+use crate::unsigned::{U160, U256};
+
+#[cfg(test)]
+pub mod overrides {
+    #[no_mangle]
+    pub extern "C" fn fail(_msg: *const u8, _msg_len: usize) -> ! {
+        panic!("fail called");
+    }
+}
+
+#[cfg(test)]
+pub use mock::failWrapper;
+#[cfg(not(test))]
+pub use impl_::failWrapper;
+
+pub trait Ulm {
+    fn log3(&self, data1: &[u8; 32], data2: &[u8; 32], data3: &[u8; 32], bytes: &[u8]);
+    fn caller(&self, result: &mut [u8; 20]);
+
+    fn call_data_length(&self) -> u32;
+    fn call_data(&self, result: &mut [u8]);
+
+    fn get_account_storage(&self, key: &[u8; 32], value: &mut [u8; 32]);
+    fn set_account_storage(&mut self, key: &[u8; 32], value: &[u8; 32]);
+
+    fn set_output(&mut self, bytes: &[u8]);
+
+    fn keccak_hash(&self, value: &[u8], result: &mut [u8; 32]);
+}
+
+#[cfg(not(test))]
+pub mod impl_ {
+    use core::cell::RefCell;
+    use std::rc::Rc;
+
+    use crate::ulm::Ulm;
+
+    extern "C" {
+        // data1, data2 and data3 must have a length of exactly 32.
+        #[allow(non_snake_case)]
+        pub fn Log3(data1: *const u8, data2: *const u8, data3: *const u8, bytes: *const u8, bytes_length: usize);
+
+        // result must have a length of exactly 20.
+        #[allow(non_snake_case)]
+        pub fn Caller(result: *mut u8);
+
+        #[allow(non_snake_case)]
+        pub fn CallDataLength() -> u32;
+        // result must have a length of at least CallDataLength()
+        #[allow(non_snake_case)]
+        pub fn CallData(result: *mut u8);
+
+        // key and value must have a length of exactly 32.
+        #[allow(non_snake_case)]
+        pub fn GetAccountStorage(key: *const u8, value: *mut u8);
+
+        // key and value must have a length of exactly 32.
+        #[allow(non_snake_case)]
+        pub fn SetAccountStorage(key: *const u8, value: *const u8);
+
+
+        #[allow(non_snake_case)]
+        pub fn setOutput(bytes: *const u8, bytes_length: usize);
+
+        #[allow(dead_code)]
+        pub fn fail(msg: *const u8, msg_len: usize) -> !;
+
+        // result must have a length of exactly 32.
+        pub fn keccakHash(msg: *const u8, msg_len: usize, result: *mut u8);
+
+    }
+
+    #[allow(non_snake_case)]
+    pub fn failWrapper(msg: &str) -> ! {
+        let msg_bytes = msg.as_bytes();
+        unsafe { fail(msg_bytes.as_ptr(), msg_bytes.len()); }
+    }
+
+    pub struct UlmImpl {}
+
+    impl UlmImpl {
+      pub fn new() -> Rc<RefCell<Self>> {
+          Rc::new(RefCell::new(UlmImpl {}))
+      }
+    }
+
+    impl Ulm for UlmImpl {
+        fn log3(&self, data1: &[u8; 32], data2: &[u8; 32], data3: &[u8; 32], bytes: &[u8]) {
+            unsafe { Log3(data1.as_ptr(), data2.as_ptr(), data3.as_ptr(), bytes.as_ptr(), bytes.len()); }
+        }
+        fn caller(&self, result: &mut [u8; 20]) {
+            unsafe { Caller(result.as_mut_ptr()); }
+        }
+
+        fn call_data_length(&self) -> u32 {
+            unsafe { CallDataLength() }
+        }
+        fn call_data(&self, result: &mut [u8]) {
+            let required_len = self.call_data_length();
+            if result.len() < required_len.try_into().unwrap() {
+                failWrapper("call_data: buffer too small.");
+            }
+            unsafe { CallData(result.as_mut_ptr()); }
+        }
+
+        fn get_account_storage(&self, key: &[u8; 32], value: &mut [u8; 32]) {
+            unsafe { GetAccountStorage(key.as_ptr(), value.as_mut_ptr()); }
+        }
+
+        fn set_account_storage(&mut self, key: &[u8; 32], value: &[u8; 32]) {
+            unsafe { SetAccountStorage(key.as_ptr(), value.as_ptr()); }
+        }
+
+        fn set_output(&mut self, bytes: &[u8]) {
+            unsafe { setOutput(bytes.as_ptr(), bytes.len()); }
+        }
+
+        fn keccak_hash(&self, value: &[u8], result: &mut [u8; 32]) {
+            unsafe { keccakHash(value.as_ptr(), value.len(), result.as_mut_ptr()); }
+        }
+    }
+}
+
+#[cfg(test)]
+pub mod mock {
+    use bytes::{Bytes, Buf};
+    use std::cell::RefCell;
+    use std::collections::HashMap;
+    use std::rc::Rc;
+
+    use crate::address::Address;
+    use crate::assertions::fail;
+    use crate::require;
+    use crate::ulm::Ulm;
+    use crate::unsigned::U160;
+
+    #[allow(non_snake_case)]
+    pub fn failWrapper(msg: &str) -> ! {
+        panic!("{}", msg);
+    }
+
+    pub struct UlmMock {
+        storage: HashMap<Bytes, Bytes>,
+        caller: [u8; 20],
+        call_data: Bytes,
+    }
+
+    impl UlmMock {
+        pub fn new() -> Rc<RefCell<Self>> {
+            Rc::new(RefCell::new(UlmMock {
+                storage: HashMap::new(),
+                caller: [0_u8; 20],
+                call_data: Bytes::new(),
+            }))
+        }
+        pub fn set_caller(&mut self, caller: Address) {
+            let caller_nr: U160 = caller.into();
+            caller_nr.copy_to_array_le(&mut self.caller);
+        }
+    }
+
+    impl Ulm for UlmMock {
+        fn log3(&self, _data1: &[u8; 32], _data2: &[u8; 32], _data3: &[u8; 32], _bytes: &[u8]) {}
+
+        fn caller(&self, result: &mut [u8; 20]) {
+            *result = self.caller;
+        }
+
+        fn call_data_length(&self) -> u32 {
+            self.call_data.len().try_into().unwrap()
+        }
+        fn call_data(&self, result: &mut [u8]) {
+            let required_len = self.call_data_length();
+            require!(result.len() >= required_len.try_into().unwrap(), "call_data: buffer too small.");
+            require!(result.len() <= required_len.try_into().unwrap(), "call_data mock: buffer too large.");
+            result.copy_from_slice(self.call_data.chunk());
+        }
+
+        fn get_account_storage(&self, key: &[u8; 32], value: &mut [u8; 32]) {
+            let bytes_key = Bytes::copy_from_slice(key);
+            match self.storage.get(&bytes_key) {
+                Some(v) => {
+                    let bytes_value = v.chunk();
+                    require!(bytes_value.len() == 32, "unexpected value length in storage");
+                    value.copy_from_slice(bytes_value);
+                },
+                None => {
+                    for i in 0 .. value.len() {
+                        value[i] = 0;
+                    }
+                },
+            }
+        }
+
+        fn set_account_storage(&mut self, key: &[u8; 32], value: &[u8; 32]) {
+            let bytes_key = Bytes::copy_from_slice(key);
+            let bytes_value = Bytes::copy_from_slice(value);
+            self.storage.insert(bytes_key, bytes_value);
+        }
+
+        fn set_output(&mut self, bytes: &[u8]) {
+            self.call_data = Bytes::copy_from_slice(bytes);
+        }
+
+        fn keccak_hash(&self, value: &[u8], result: &mut [u8; 32]) {
+            for i in 1 .. result.len() {
+                result[i] = 0;
+            }
+            let mut assimetry: u16 = 1;
+            for i in 0 .. value.len() {
+                let assimetric_value: u16 = (value[i] as u16) * assimetry;
+                result[i % 32] ^= assimetric_value as u8;
+                assimetry = (assimetry * 3) & 0xff;
+            }
+        }
+    }
+}
+
+pub fn log3(api: &dyn Ulm, signature: &str, data2: &U256, data3: &U256, bytes: Bytes) {
+    let signature_fingerprint = keccak_hash_int(api, &Bytes::copy_from_slice(signature.as_bytes()));
+    let mut data1_bytes = [0_u8; 32];
+    signature_fingerprint.copy_to_array_le(&mut data1_bytes);
+
+    let mut data2_bytes = [0_u8; 32];
+    data2.copy_to_array_le(&mut data2_bytes);
+    let mut data3_bytes = [0_u8; 32];
+    data3.copy_to_array_le(&mut data3_bytes);
+    let bytes_bytes = bytes.chunk();
+
+    api.log3(&data1_bytes, &data2_bytes, &data3_bytes, &bytes_bytes);
+}
+
+pub fn caller(api: &dyn Ulm) -> Address {
+    let mut result = [0_u8; 20];
+    api.caller(&mut result);
+    U160::from_array_le(result).into()
+}
+
+pub fn call_data(api: &dyn Ulm) -> Bytes {
+    let length: usize = api.call_data_length().try_into().unwrap();
+    let mut buf : Vec<u8> = vec![0; length];
+    api.call_data(buf.as_mut_slice());
+    Bytes::copy_from_slice(buf.as_slice())
+}
+
+pub fn get_account_storage(api: &dyn Ulm, key: &U256) -> U256 {
+    let mut key_bytes = [0_u8; 32];
+    key.copy_to_array_le(&mut key_bytes);
+
+    let mut value_bytes = [0_u8; 32];
+    api.get_account_storage(&key_bytes, &mut value_bytes);
+
+    U256::from_array_le(value_bytes)
+}
+
+pub fn set_account_storage(api: &mut dyn Ulm, key: &U256, value: &U256) {
+    let mut key_bytes = [0_u8; 32];
+    key.copy_to_array_le(&mut key_bytes);
+
+    let mut value_bytes = [0_u8; 32];
+    value.copy_to_array_le(&mut value_bytes);
+
+    api.set_account_storage(&key_bytes, &value_bytes);
+}
+
+pub fn set_output(api: &mut dyn Ulm, bytes: &Bytes) {
+    api.set_output(bytes.chunk());
+}
+
+pub fn keccak_hash(api: &dyn Ulm, value: &Bytes) -> [u8; 32] {
+    let mut fingerprint = [0_u8; 32];
+    api.keccak_hash(value.chunk(), &mut fingerprint);
+    fingerprint
+}
+
+pub fn keccak_hash_int(api: &dyn Ulm, value: &Bytes) -> U256 {
+    let fingerprint = keccak_hash(api, value);
+    U256::from_array_le(fingerprint)
+}
+
+pub fn endpoint_fingerprint(api: &dyn Ulm, value: &str) -> [u8; 4] {
+    let fingerprint = keccak_hash(api, &Bytes::copy_from_slice(value.as_bytes()));
+    [fingerprint[0], fingerprint[1], fingerprint[2], fingerprint[3], ]
+}
\ No newline at end of file
diff --git a/tests/ulm/counter/rust/src/unsigned.rs b/tests/ulm/counter/rust/src/unsigned.rs
new file mode 100644
index 000000000..431768b6e
--- /dev/null
+++ b/tests/ulm/counter/rust/src/unsigned.rs
@@ -0,0 +1,407 @@
+// This is a suboptimal implementation of an unsigned int, which is small and
+// therefore useful for testing the wasm semantics. A proper implementation
+// should probably use something like ruint2::Uint<..., ...> or uint256::Uint256.
+
+use bytes::{Bytes, Buf};
+use core::cmp::Ordering;
+use core::ops::Add;
+use core::ops::Sub;
+
+use crate::assertions::fail;
+use crate::require;
+use crate::encoder::{Encodable, EncodingType, EncodingType::FixedSize};
+use crate::decoder::Decodable;
+use crate::predicate::{Satisfied};
+
+#[derive(Debug)]
+pub struct Unsigned<const N: usize> {
+    chunks: [u8; N],
+}
+
+// pub type U72  = Unsigned<9>;
+// pub type U80  = Unsigned<10>;
+// pub type U88  = Unsigned<11>;
+// pub type U96  = Unsigned<12>;
+// pub type U104 = Unsigned<13>;
+// pub type U112 = Unsigned<14>;
+// pub type U120 = Unsigned<15>;
+// pub type U128 = Unsigned<16>;
+// pub type U136 = Unsigned<17>;
+// pub type U144 = Unsigned<18>;
+// pub type U152 = Unsigned<19>;
+pub type U160 = Unsigned<20>;
+// pub type U168 = Unsigned<21>;
+// pub type U176 = Unsigned<22>;
+// pub type U184 = Unsigned<23>;
+// pub type U192 = Unsigned<24>;
+// pub type U200 = Unsigned<25>;
+// pub type U208 = Unsigned<26>;
+// pub type U216 = Unsigned<27>;
+// pub type U224 = Unsigned<28>;
+// pub type U232 = Unsigned<29>;
+// pub type U240 = Unsigned<30>;
+// pub type U248 = Unsigned<31>;
+pub type U256 = Unsigned<32>;
+
+impl<const N: usize> Unsigned<N> {
+    pub fn try_from_unsigned<const M: usize>(value: &Unsigned<M>) -> Result<Unsigned<N>, &'static str> {
+        let mut chunks = [0_u8; N];
+        if M <= N {
+            for i in 0 .. M {
+                chunks[i] = value.chunks[i];
+            }
+        } else {
+            for i in 0 .. N {
+                chunks[i] = value.chunks[i];
+            }
+            for i in N .. M {
+                if value.chunks[i] != 0 {
+                    return Err("Value too large to cast");
+                }
+            }
+        }
+        Ok (Unsigned { chunks })
+    }
+
+    pub fn from_array_le(chunks: [u8; N]) -> Unsigned<N> {
+        Unsigned { chunks }
+    }
+
+    pub fn from_u64(value: u64) -> Unsigned<N> {
+        if 8 <= N {
+            let mut chunks = [0_u8; N];
+            let mut to_process = value;
+            for i in 0 .. 8 {
+                chunks[i] = (to_process & 0xff) as u8;
+                to_process = to_process >> 8;
+            }
+            require!(to_process == 0, "Unprocessed bits in value.");
+            Unsigned { chunks }
+        } else {
+            match Unsigned::try_from_unsigned(&Unsigned::<8>::from_u64(value)) {
+                Ok(v) => v,
+                Err(msg) => fail(msg),
+            }
+        }
+    }
+    pub fn from_bool(value:bool) -> Self {
+        Self::from_u64(if value {0} else {1})
+    }
+    pub fn from_u8(value:u8) -> Self {
+        Self::from_u64(value as u64)
+    }
+    pub fn from_u16(value:u16) -> Self {
+        Self::from_u64(value as u64)
+    }
+    pub fn from_u32(value:u32) -> Self {
+        Self::from_u64(value as u64)
+    }
+
+    pub fn copy_to_array_le(&self, chunks: &mut [u8; N]) {
+        chunks.copy_from_slice(&self.chunks);
+    }
+
+    pub fn try_to_u64(&self) -> Result<u64, &'static str> {
+        let useful_length =
+            if 8 < N {
+                for i in 8 .. N {
+                    if self.chunks[i] != 0 {
+                        return Err("Overflow when converting to u64");
+                    }
+                }
+                8
+            } else {
+                N
+            };
+        let mut value = 0_u64;
+        for i in (0 .. useful_length).rev() {
+            value = value << 8;
+            value += self.chunks[i] as u64;
+        }
+        Ok(value)
+    }
+}
+
+impl<const N: usize> TryFrom<&Unsigned<N>> for u64 {
+    type Error = &'static str;
+    fn try_from(value: &Unsigned<N>) -> Result<Self, Self::Error> {
+        value.try_to_u64()
+    }
+}
+impl<const N: usize> TryFrom<Unsigned<N>> for u64 {
+    type Error = &'static str;
+    fn try_from(value: Unsigned<N>) -> Result<Self, Self::Error> {
+        (&value).try_into()
+    }
+}
+impl<const N: usize> TryFrom<&Unsigned<N>> for usize {
+    type Error = &'static str;
+    fn try_from(value: &Unsigned<N>) -> Result<Self, Self::Error> {
+        let value_u64: u64 = value.try_into()?;
+        match value_u64.try_into() {
+            Ok(v) => Ok(v),
+            Err(_) => Err("Error converting u64 to usize")
+        }
+    }
+}
+impl<const N: usize> TryFrom<Unsigned<N>> for usize {
+    type Error = &'static str;
+    fn try_from(value: Unsigned<N>) -> Result<Self, Self::Error> {
+        (&value).try_into()
+    }
+}
+impl<const N: usize, const M: usize> TryFrom<&Unsigned<N>> for Unsigned<M> {
+    type Error = &'static str;
+    fn try_from(value: &Unsigned<N>) -> Result<Self, Self::Error> {
+        Unsigned::try_from_unsigned(value)
+    }
+}
+
+#[macro_export]
+macro_rules! try_from_u256 {
+    ( $size:expr ) => {
+        impl TryFrom<U256> for Unsigned<$size>
+        {
+            type Error = &'static str;
+            fn try_from(value: U256) -> Result<Self, Self::Error> {
+                (&value).try_into()
+            }
+        }
+        impl From<Unsigned<$size>> for U256
+            where SmallerThan32<$size>: Satisfied
+        {
+            fn from(value: Unsigned<$size>) -> Self {
+                (&value).try_into().unwrap()
+            }
+        }
+    }
+}
+try_from_u256!(1);
+try_from_u256!(2);
+try_from_u256!(3);
+try_from_u256!(4);
+try_from_u256!(5);
+try_from_u256!(6);
+try_from_u256!(7);
+try_from_u256!(8);
+try_from_u256!(9);
+try_from_u256!(10);
+try_from_u256!(11);
+try_from_u256!(12);
+try_from_u256!(13);
+try_from_u256!(14);
+try_from_u256!(15);
+try_from_u256!(16);
+try_from_u256!(17);
+try_from_u256!(18);
+try_from_u256!(19);
+try_from_u256!(20);
+try_from_u256!(21);
+try_from_u256!(22);
+try_from_u256!(23);
+try_from_u256!(24);
+try_from_u256!(25);
+try_from_u256!(26);
+try_from_u256!(27);
+try_from_u256!(28);
+try_from_u256!(29);
+try_from_u256!(30);
+try_from_u256!(31);
+
+impl<const N: usize> Add for &Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn add(self, other: &Unsigned<N>) -> Self::Output {
+        let mut chunks = [0_u8; N];
+        let mut carry = 0_u16;
+        for i in 0..N {
+            let value = (self.chunks[i] as u16) + (other.chunks[i] as u16) + carry;
+            carry = value >> 8;
+            chunks[i] = (value & 0xff) as u8;
+        }
+        require!(carry == 0, "Addition overflow");
+        Unsigned { chunks }
+    }
+}
+impl<const N: usize> Add for Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn add(self, other: Unsigned<N>) -> Self::Output {
+        &self + &other
+    }
+}
+impl<const N: usize> Add<Unsigned<N>> for &Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn add(self, other: Unsigned<N>) -> Self::Output {
+        self + &other
+    }
+}
+impl<const N: usize> Add<&Unsigned<N>> for Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn add(self, other: &Unsigned<N>) -> Self::Output {
+        &self + other
+    }
+}
+
+impl<const N: usize> Sub for &Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn sub(self, other: &Unsigned<N>) -> Self::Output {
+        let mut chunks = [0_u8; N];
+        let mut carry = 0_u16;
+        for i in 0..N {
+            let self_chunk = self.chunks[i] as u16;
+            let to_remove = other.chunks[i] as u16 + carry;
+            let remove_from =
+                if self_chunk >= to_remove {
+                    carry = 0;
+                    self_chunk
+                } else {
+                    carry = 1;
+                    self_chunk + 0x100
+                };
+            require!(remove_from >= to_remove, "Unexpected value in subtraction");
+            let result = remove_from - to_remove;
+            require!(result <= 0xff, "Unexpected value in subtraction");
+            chunks[i] = result as u8;
+        }
+        require!(carry == 0, "Subtraction overflow");
+        Unsigned { chunks }
+    }
+}
+impl<const N: usize> Sub for Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn sub(self, other: Unsigned<N>) -> Self::Output {
+        &self - &other
+    }
+}
+impl<const N: usize> Sub<Unsigned<N>> for &Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn sub(self, other: Unsigned<N>) -> Self::Output {
+        self - &other
+    }
+}
+impl<const N: usize> Sub<&Unsigned<N>> for Unsigned<N> {
+    type Output = Unsigned<N>;
+    fn sub(self, other: &Unsigned<N>) -> Self::Output {
+        &self - other
+    }
+}
+
+impl<const N: usize> Ord for Unsigned<N> {
+    fn cmp(&self, other: &Self) -> Ordering {
+        for i in (0..N).rev() {
+            if self.chunks[i] < other.chunks[i] {
+                return Ordering::Less;
+            }
+            if self.chunks[i] > other.chunks[i] {
+                return Ordering::Greater;
+            }
+        }
+        Ordering::Equal
+    }
+}
+impl<const N: usize> PartialOrd for Unsigned<N> {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+impl<const N: usize> PartialEq for Unsigned<N> {
+    fn eq(&self, other: &Self) -> bool {
+        self.cmp(other) == Ordering::Equal
+    }
+}
+impl<const N: usize> Eq for Unsigned<N> {}
+impl<const N: usize> Clone for Unsigned<N> {
+    fn clone(&self) -> Self {
+        Unsigned { chunks: self.chunks.clone() }
+    }
+}
+
+impl Encodable for U256
+{
+    fn encode(&self) -> (EncodingType, Bytes) {
+        let mut encoded = [0_u8; 32];
+        for i in 0 .. 32 {
+            encoded[i] = self.chunks[31 - i];
+        }
+        (FixedSize, Bytes::copy_from_slice(&encoded))
+    }
+}
+impl Decodable for U256
+{
+    fn encoding_type() -> EncodingType {
+        FixedSize
+    }
+    fn head_size() -> usize {
+        32
+    }
+    fn decode(bytes: Bytes) -> Self {
+        let encoded = bytes.chunk();
+        require!(32 == encoded.len(), "Wrong length to decode");
+        let mut value: U256 = U256::from_u64(0);
+        for i in 0 .. 32 {
+            value.chunks[31 - i] = encoded[i];
+        }
+        value
+    }
+}
+impl<const N: usize> Encodable for Unsigned<N>
+where
+    SmallerThan32<N>: Satisfied
+{
+    fn encode(&self) -> (EncodingType, Bytes) {
+        match U256::try_from_unsigned(self) {
+            Ok(v) => v.encode(),
+            Err(msg) => fail(msg),
+        }
+    }
+}
+impl<const N: usize> Decodable for Unsigned<N>
+where
+    SmallerThan32<N>: Satisfied
+{
+    fn encoding_type() -> EncodingType {
+        U256::encoding_type()
+    }
+    fn head_size() -> usize {
+        U256::head_size()
+    }
+    fn decode(bytes: Bytes) -> Self {
+        let value_u256 = U256::decode(bytes);
+        match Unsigned::<N>::try_from_unsigned(&value_u256) {
+            Ok(v) => v,
+            Err(msg) => fail(msg),
+        }
+    }
+}
+
+pub enum SmallerThan32<const EXPRESSION: usize> {}
+impl Satisfied for SmallerThan32<1> {}
+impl Satisfied for SmallerThan32<2> {}
+impl Satisfied for SmallerThan32<3> {}
+impl Satisfied for SmallerThan32<4> {}
+impl Satisfied for SmallerThan32<5> {}
+impl Satisfied for SmallerThan32<6> {}
+impl Satisfied for SmallerThan32<7> {}
+impl Satisfied for SmallerThan32<8> {}
+impl Satisfied for SmallerThan32<9> {}
+impl Satisfied for SmallerThan32<10> {}
+impl Satisfied for SmallerThan32<11> {}
+impl Satisfied for SmallerThan32<12> {}
+impl Satisfied for SmallerThan32<13> {}
+impl Satisfied for SmallerThan32<14> {}
+impl Satisfied for SmallerThan32<15> {}
+impl Satisfied for SmallerThan32<16> {}
+impl Satisfied for SmallerThan32<17> {}
+impl Satisfied for SmallerThan32<18> {}
+impl Satisfied for SmallerThan32<19> {}
+impl Satisfied for SmallerThan32<20> {}
+impl Satisfied for SmallerThan32<21> {}
+impl Satisfied for SmallerThan32<22> {}
+impl Satisfied for SmallerThan32<23> {}
+impl Satisfied for SmallerThan32<24> {}
+impl Satisfied for SmallerThan32<25> {}
+impl Satisfied for SmallerThan32<26> {}
+impl Satisfied for SmallerThan32<27> {}
+impl Satisfied for SmallerThan32<28> {}
+impl Satisfied for SmallerThan32<29> {}
+impl Satisfied for SmallerThan32<30> {}
+impl Satisfied for SmallerThan32<31> {}

From 9545c019347d77f61237323f08f1e4752ebb7aed Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@pi2.network>
Date: Wed, 8 Jan 2025 19:37:23 +0200
Subject: [PATCH 3/9] Finish instruction codes and fix syntax

---
 .../kdist/wasm-semantics/binary-parser.md     | 817 ++++++++++++------
 1 file changed, 547 insertions(+), 270 deletions(-)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
index 69d7ba6b4..3b2995aa5 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -4,7 +4,7 @@ This file defines a Wasm binary parser.
 To begin, we define constant macros which drive the parser process.
 
 ```k
-module BINARY_PARSER_DATA
+module BINARY-PARSER-DATA
   imports BYTES
 ```
 
@@ -13,84 +13,84 @@ module BINARY_PARSER_DATA
 Every Wasm module starts with a 4-byte header and a 4-byte version.
 
 ```k
-  syntax Bytes ::= MAGIC   [macro] rule MAGIC   => b"x00x61x73x6D"
-                 | VERSION [macro] rule VERSION => b"x01x00x00x00"
+  syntax Bytes ::= "MAGIC"   [macro] rule MAGIC   => b"\x00\x61\x73\x6D"
+  syntax Bytes ::= "VERSION" [macro] rule VERSION => b"\x01\x00\x00\x00"
 ```
 
 After that, a Wasm module is an ordered list of sections, each prefixed with a section id.
 
 ```k
-                 | CUSTOM_SEC [macro] rule CUSTOM_SEC => b"x00"
-                 | TYPE_SEC   [macro] rule TYPE_SEC   => b"x01"
-                 | IMPORT_SEC [macro] rule IMPORT_SEC => b"x02"
-                 | FUNC_SEC   [macro] rule FUNC_SEC   => b"x03"
-                 | TABLE_SEC  [macro] rule TABLE_SEC  => b"x04"
-                 | MEMORY_SEC [macro] rule MEMORY_SEC => b"x05"
-                 | GLOBAL_SEC [macro] rule GLOBAL_SEC => b"x06"
-                 | EXPORT_SEC [macro] rule EXPORT_SEC => b"x07"
-                 | START_SEC  [macro] rule START_SEC  => b"x08"
-                 | ELT_SEC    [macro] rule ELT_SEC    => b"x09"
-                 | CODE_SEC   [macro] rule CODE_SEC   => b"x0a"
-                 | DAT_SEC    [macro] rule DAT_SEC    => b"x0b"
-                 | CNT_SEC    [macro] rule CNT_SEC    => b"x0c"
+  syntax Bytes ::= "CUSTOM_SEC" [macro] rule CUSTOM_SEC => b"\x00"
+  syntax Bytes ::= "TYPE_SEC"   [macro] rule TYPE_SEC   => b"\x01"
+  syntax Bytes ::= "IMPORT_SEC" [macro] rule IMPORT_SEC => b"\x02"
+  syntax Bytes ::= "FUNC_SEC"   [macro] rule FUNC_SEC   => b"\x03"
+  syntax Bytes ::= "TABLE_SEC"  [macro] rule TABLE_SEC  => b"\x04"
+  syntax Bytes ::= "MEMORY_SEC" [macro] rule MEMORY_SEC => b"\x05"
+  syntax Bytes ::= "GLOBAL_SEC" [macro] rule GLOBAL_SEC => b"\x06"
+  syntax Bytes ::= "EXPORT_SEC" [macro] rule EXPORT_SEC => b"\x07"
+  syntax Bytes ::= "START_SEC"  [macro] rule START_SEC  => b"\x08"
+  syntax Bytes ::= "ELT_SEC"    [macro] rule ELT_SEC    => b"\x09"
+  syntax Bytes ::= "CODE_SEC"   [macro] rule CODE_SEC   => b"x0a"
+  syntax Bytes ::= "DAT_SEC"    [macro] rule DAT_SEC    => b"x0b"
+  syntax Bytes ::= "CNT_SEC"    [macro] rule CNT_SEC    => b"x0c"
 ```
 
 In the import/export sections, different kinds of imports/exports are tagged.
 
 ```k
-                 | IMPORT_FUNC [macro] rule IMPORT_FUNC => b"x00"
-                 | IMPORT_TBLT [macro] rule IMPORT_TBLT => b"x01"
-                 | IMPORT_MEMT [macro] rule IMPORT_MEMT => b"x02"
-                 | IMPORT_GLBT [macro] rule IMPORT_GLBT => b"x03"
-                 | EXPORT_FUNC [macro] rule EXPORT_FUNC => b"x00"
-                 | EXPORT_TBLT [macro] rule EXPORT_TBLT => b"x01"
-                 | EXPORT_MEMT [macro] rule EXPORT_MEMT => b"x02"
-                 | EXPORT_GLBT [macro] rule EXPORT_GLBT => b"x03"
+  syntax Bytes ::= "IMPORT_FUNC" [macro] rule IMPORT_FUNC => b"\x00"
+  syntax Bytes ::= "IMPORT_TBLT" [macro] rule IMPORT_TBLT => b"\x01"
+  syntax Bytes ::= "IMPORT_MEMT" [macro] rule IMPORT_MEMT => b"\x02"
+  syntax Bytes ::= "IMPORT_GLBT" [macro] rule IMPORT_GLBT => b"\x03"
+  syntax Bytes ::= "EXPORT_FUNC" [macro] rule EXPORT_FUNC => b"\x00"
+  syntax Bytes ::= "EXPORT_TBLT" [macro] rule EXPORT_TBLT => b"\x01"
+  syntax Bytes ::= "EXPORT_MEMT" [macro] rule EXPORT_MEMT => b"\x02"
+  syntax Bytes ::= "EXPORT_GLBT" [macro] rule EXPORT_GLBT => b"\x03"
 ```
 
 _Element_ sections have various possible formats which are stored in a 3-bit code.
 The possible code words are explained in the table below:
 
-Bit # | Constraint | 0 State         | 1 State              |
+Bit # | "C"onstraint | "0" State         | "1" State              |
 ----- | ---------- | --------------- | -------------------- |
-0     | None       | active          | passive/declarative  |
-1     | Bit[0]=0   | has table index | zero table index     |
-1     | Bit[0]=1   | passive         | declarative          |
-2     | None       | elts by ref     | elts by value        |
+0     | "N"one       | active          | passive/declarative  |
+1     | "B"it[0]=0   | has table index | zero table index     |
+1     | "B"it[0]=1   | passive         | declarative          |
+2     | "N"one       | elts by ref     | elts by value        |
 
 ```k
-                 | ELTS_ACTIVE_ZERO_BY_REF [macro] // 000
-                 | ELTS_PASSIVE_BY_REF     [macro] // 001
-                 | ELTS_ACTIVE_IDX_BY_REF  [macro] // 010
-                 | ELTS_DECL_BY_REF        [macro] // 011
-                 | ELTS_ACTIVE_ZERO_BY_VAL [macro] // 100
-                 | ELTS_PASSIVE_BY_VAL     [macro] // 101
-                 | ELTS_ACTIVE_IDX_BY_VAL  [macro] // 110
-                 | ELTS_DECL_BY_VAL        [macro] // 110
-
-  rule ELTS_ACTIVE_ZERO_BY_REF => b"x00"
-  rule ELTS_PASSIVE_BY_REF     => b"x01"
-  rule ELTS_ACTIVE_IDX_BY_REF  => b"x02"
-  rule ELTS_DECL_BY_REF        => b"x03"
-  rule ELTS_ACTIVE_ZERO_BY_VAL => b"x04"
-  rule ELTS_PASSIVE_BY_VAL     => b"x05"
-  rule ELTS_ACTIVE_IDX_BY_VAL  => b"x06"
-  rule ELTS_DECL_BY_VAL        => b"x07"
+  syntax Bytes ::= "ELTS_ACTIVE_ZERO_BY_REF" [macro] // 000
+  syntax Bytes ::= "ELTS_PASSIVE_BY_REF"     [macro] // 001
+  syntax Bytes ::= "ELTS_ACTIVE_IDX_BY_REF"  [macro] // 010
+  syntax Bytes ::= "ELTS_DECL_BY_REF"        [macro] // 011
+  syntax Bytes ::= "ELTS_ACTIVE_ZERO_BY_VAL" [macro] // 100
+  syntax Bytes ::= "ELTS_PASSIVE_BY_VAL"     [macro] // 101
+  syntax Bytes ::= "ELTS_ACTIVE_IDX_BY_VAL"  [macro] // 110
+  syntax Bytes ::= "ELTS_DECL_BY_VAL"        [macro] // 110
+
+  rule ELTS_ACTIVE_ZERO_BY_REF => b"\x00"
+  rule ELTS_PASSIVE_BY_REF     => b"\x01"
+  rule ELTS_ACTIVE_IDX_BY_REF  => b"\x02"
+  rule ELTS_DECL_BY_REF        => b"\x03"
+  rule ELTS_ACTIVE_ZERO_BY_VAL => b"\x04"
+  rule ELTS_PASSIVE_BY_VAL     => b"\x05"
+  rule ELTS_ACTIVE_IDX_BY_VAL  => b"\x06"
+  rule ELTS_DECL_BY_VAL        => b"\x07"
 ```
 
 The special _element kind_ constant is used to describe possible element kinds.
 Currently, only one element kind is supported.
 
 ```k
-                 | ELT_KIND [macro] rule ELT_KIND => b"x00"
+  syntax Bytes ::= "ELT_KIND" [macro] rule ELT_KIND => b"\x00"
 ```
 
 _Data_ sections are tagged based on their kind.
 
 ```k
-                 | DATA_ACTIVE_ZERO [macro] rule DATA_ACTIVE_ZERO  => b"x00"
-                 | DATA_PASSIVE     [macro] rule DATA_PASSIVE_ZERO => b"x01"
-                 | DATA_ACTIVE_IDX  [macro] rule DATA_ACTIVE_IDX   => b"x02"
+  syntax Bytes ::= "DATA_ACTIVE_ZERO" [macro] rule DATA_ACTIVE_ZERO  => b"\x00"
+  syntax Bytes ::= "DATA_PASSIVE"     [macro] rule DATA_PASSIVE => b"\x01"
+  syntax Bytes ::= "DATA_ACTIVE_IDX"  [macro] rule DATA_ACTIVE_IDX   => b"\x02"
 ```
 
 Each value _type_ is tagged by a unique integer.
@@ -98,30 +98,30 @@ There are two special types: functions and empty types.
 These have special use requirements as we will see later.
 
 ```k
-                 | TYPE_I32     [macro] rule TYPE_I32     => b"x7F"
-                 | TYPE_I64     [macro] rule TYPE_I64     => b"x7E"
-                 | TYPE_F32     [macro] rule TYPE_F32     => b"x7D"
-                 | TYPE_F64     [macro] rule TYPE_F64     => b"x7C"
-                 | TYPE_VEC     [macro] rule TYPE_VEC     => b"x7B"
-                 | TYPE_FUN_REF [macro] rule TYPE_FUN_REF => b"x70"
-                 | TYPE_EXT_REF [macro] rule TYPE_EXT_REF => b"x64"
-                 | TYPE_FUN     [macro] rule TYPE_FUN     => b"x60"
-                 | TYPE_EMPTY   [macro] rule TYPE_EMPTY   => b"x40"
+  syntax Bytes ::= "TYPE_I32"     [macro] rule TYPE_I32     => b"\x7F"
+  syntax Bytes ::= "TYPE_I64"     [macro] rule TYPE_I64     => b"\x7E"
+  syntax Bytes ::= "TYPE_F32"     [macro] rule TYPE_F32     => b"\x7D"
+  syntax Bytes ::= "TYPE_F64"     [macro] rule TYPE_F64     => b"\x7C"
+  syntax Bytes ::= "TYPE_VEC"     [macro] rule TYPE_VEC     => b"\x7B"
+  syntax Bytes ::= "TYPE_FUN_REF" [macro] rule TYPE_FUN_REF => b"\x70"
+  syntax Bytes ::= "TYPE_EXT_REF" [macro] rule TYPE_EXT_REF => b"\x64"
+  syntax Bytes ::= "TYPE_FUN"     [macro] rule TYPE_FUN     => b"\x60"
+  syntax Bytes ::= "TYPE_EMPTY"   [macro] rule TYPE_EMPTY   => b"\x40"
 ```
 
 _Limits_ are used to encode the minimum size of memories and tables;
 a separate form that also specifies a maximum size is available.
 
 ```k
-                 | LIMITS     [macro] rule LIMITS     => b"x00"
-                 | LIMITS_MAX [macro] rule LIMITS_MAX => b"x01"
+  syntax Bytes ::= "LIMITS"     [macro] rule LIMITS     => b"\x00"
+  syntax Bytes ::= "LIMITS_MAX" [macro] rule LIMITS_MAX => b"\x01"
 ```
 
 _Globals_ may be declared as mutable or immutable.
 
 ```k
-                 | GLOBAL_CNST [macro] rule GLOBAL_CNST => b"x00"
-                 | GLOBAL_VAR  [macro] rule GLOBAL_VAR  => b"x01"
+  syntax Bytes ::= "GLOBAL_CNST" [macro] rule GLOBAL_CNST => b"\x00"
+  syntax Bytes ::= "GLOBAL_VAR"  [macro] rule GLOBAL_VAR  => b"\x01"
 ```
 
 ## Wasm Instruction Parser Tags
@@ -130,234 +130,511 @@ Wasm _control instructions_ are encoded with the follow tags.
 Note that `ELSE` instructions must appear in conjunction with `IF` instructions.
 
 ```k
-  syntax Bytes ::= UNREACHABLE   [macro] rule UNREACHABLE   => b"x00"
-                 | NOP           [macro] rule NOP           => b"x01"
-                 | BLOCK         [macro] rule BLOCK         => b"x02"
-                 | LOOP          [macro] rule LOOP          => b"x03"
-                 | IF            [macro] rule IF            => b"x04"
-                 | ELSE          [macro] rule ELSE          => b"x05"
-                 | BR            [macro] rule BR            => b"x0C"
-                 | BR_IF         [macro] rule BR_IF         => b"x0D"
-                 | BR_TABLE      [macro] rule BR_TABLE      => b"x0E"
-                 | RETURN        [macro] rule RETURN        => b"x0F"
-                 | CALL          [macro] rule CALL          => b"x10"
-                 | CALL_INDIRECT [macro] rule CALL_INDIRECT => b"x11"
+  syntax Bytes ::= "UNREACHABLE"   [macro] rule UNREACHABLE   => b"\x00"
+  syntax Bytes ::= "NOP"           [macro] rule NOP           => b"\x01"
+  syntax Bytes ::= "BLOCK"         [macro] rule BLOCK         => b"\x02"
+  syntax Bytes ::= "LOOP"          [macro] rule LOOP          => b"\x03"
+  syntax Bytes ::= "IF"            [macro] rule IF            => b"\x04"
+  syntax Bytes ::= "ELSE"          [macro] rule ELSE          => b"\x05"
+  syntax Bytes ::= "BR"            [macro] rule BR            => b"\x0C"
+  syntax Bytes ::= "BR_IF"         [macro] rule BR_IF         => b"\x0D"
+  syntax Bytes ::= "BR_TABLE"      [macro] rule BR_TABLE      => b"\x0E"
+  syntax Bytes ::= "RETURN"        [macro] rule RETURN        => b"\x0F"
+  syntax Bytes ::= "CALL"          [macro] rule CALL          => b"\x10"
+  syntax Bytes ::= "CALL_INDIRECT" [macro] rule CALL_INDIRECT => b"\x11"
 ```
 
 _Reference instructions_ are encoded with the following tags:
 
 ```k
-  syntax Bytes ::= REF_NULL   [macro] rule REF_NULL   => b"xD0"
-                 | REF_ISNULL [macro] rule REF_ISNULL => b"xD1"
-                 | REF_FUNC   [macro] rule REF_FUNC   => b"xD2"
+  syntax Bytes ::= "REF_NULL"   [macro] rule REF_NULL   => b"\xD0"
+  syntax Bytes ::= "REF_ISNULL" [macro] rule REF_ISNULL => b"\xD1"
+  syntax Bytes ::= "REF_FUNC"   [macro] rule REF_FUNC   => b"\xD2"
 ```
 
 _Variable instructions_ are encoded with the following tags:
 
 ```k
-  syntax Bytes ::= LOCAL_GET  [macro] rule LOCAL_GET  => b"x20"
-                 | LOCAL_SET  [macro] rule LOCAL_SET  => b"x21"
-                 | LOCAL_TEE  [macro] rule LOCAL_TEE  => b"x22"
-                 | GLOBAL_GET [macro] rule GLOBAL_GET => b"x23"
-                 | GLOBAL_SET [macro] rule GLOBAL_SET => b"x24"
+  syntax Bytes ::= "LOCAL_GET"  [macro] rule LOCAL_GET  => b"\x20"
+  syntax Bytes ::= "LOCAL_SET"  [macro] rule LOCAL_SET  => b"\x21"
+  syntax Bytes ::= "LOCAL_TEE"  [macro] rule LOCAL_TEE  => b"\x22"
+  syntax Bytes ::= "GLOBAL_GET" [macro] rule GLOBAL_GET => b"\x23"
+  syntax Bytes ::= "GLOBAL_SET" [macro] rule GLOBAL_SET => b"\x24"
 ```
 
 _Table instructions_ are encoded with the following tags:
 
 ```k
-  syntax Bytes ::= TABLE_GET  [macro] rule TABLE_GET  => b"x25"
-                 | TABLE_SET  [macro] rule TABLE_SET  => b"x26"
-                 | TABLE_INIT [macro] rule TABLE_INIT => b"xFCx0C"
-                 | ELEM_DROP  [macro] rule ELEM_DROP  => b"xFCx0D"
-                 | TABLE_COPY [macro] rule TABLE_COPY => b"xFCx0E"
-                 | TABLE_GROW [macro] rule TABLE_GROW => b"xFCx0F"
-                 | TABLE_SIZE [macro] rule TABLE_SIZE => b"xFCx10"
-                 | TABLE_FILL [macro] rule TABLE_FILL => b"xFCx11"
+  syntax Bytes ::= "TABLE_GET"  [macro] rule TABLE_GET  => b"\x25"
+  syntax Bytes ::= "TABLE_SET"  [macro] rule TABLE_SET  => b"\x26"
+  syntax Bytes ::= "TABLE_INIT" [macro] rule TABLE_INIT => b"\xFC\x0C"
+  syntax Bytes ::= "ELEM_DROP"  [macro] rule ELEM_DROP  => b"\xFC\x0D"
+  syntax Bytes ::= "TABLE_COPY" [macro] rule TABLE_COPY => b"\xFC\x0E"
+  syntax Bytes ::= "TABLE_GROW" [macro] rule TABLE_GROW => b"\xFC\x0F"
+  syntax Bytes ::= "TABLE_SIZE" [macro] rule TABLE_SIZE => b"\xFC\x10"
+  syntax Bytes ::= "TABLE_FILL" [macro] rule TABLE_FILL => b"\xFC\x11"
 ```
 
 _Memory instructions_ are encoded with the following tags:
 
 ```k
-                 | I32_LOAD      [macro] rule I32_LOAD      => b"x28"
-                 | I64_LOAD      [macro] rule I64_LOAD      => b"x29"
-                 | F32_LOAD      [macro] rule F32_LOAD      => b"x2A"
-                 | F64_LOAD      [macro] rule F64_LOAD      => b"x2B"
-                 | I32_LOAD_8_S  [macro] rule I32_LOAD_8_S  => b"x2C"
-                 | I32_LOAD_8_U  [macro] rule I32_LOAD_8_U  => b"x2D"
-                 | I32_LOAD_16_S [macro] rule I32_LOAD_16_S => b"x2E"
-                 | I32_LOAD_16_U [macro] rule I32_LOAD_16_U => b"x2F"
-                 | I64_LOAD_8_S  [macro] rule I64_LOAD_8_S  => b"x30"
-                 | I64_LOAD_8_U  [macro] rule I64_LOAD_8_U  => b"x31"
-                 | I64_LOAD_16_S [macro] rule I64_LOAD_16_S => b"x32"
-                 | I64_LOAD_16_U [macro] rule I64_LOAD_16_U => b"x33"
-                 | I64_LOAD_32_S [macro] rule I64_LOAD_32_S => b"x34"
-                 | I64_LOAD_32_U [macro] rule I64_LOAD_32_U => b"x35"
-                 | I32_STORE     [macro] rule I32_STORE     => b"x36"
-                 | I64_STORE     [macro] rule I64_STORE     => b"x37"
-                 | F32_STORE     [macro] rule F32_STORE     => b"x38"
-                 | F64_STORE     [macro] rule F64_STORE     => b"x39"
-                 | I32_STORE_8   [macro] rule I32_STORE_8   => b"x3A"
-                 | I32_STORE_16  [macro] rule I32_STORE_16  => b"x3B"
-                 | I64_STORE_8   [macro] rule I64_STORE_8   => b"x3C"
-                 | I64_STORE_16  [macro] rule I64_STORE_16  => b"x3D"
-                 | I64_STORE_32  [macro] rule I64_STORE_32  => b"x3E"
-                 | MEM_SIZE      [macro] rule MEM_SIZE      => b"x3F"
-                 | MEM_GROW      [macro] rule MEM_GROW      => b"x40"
-                 | MEM_INIT      [macro] rule MEM_INIT      => b"xFCx08"
-                 | DATA_DROP     [macro] rule DATA_DROP     => b"xFCx09"
-                 | MEM_COPY      [macro] rule MEM_COPY      => b"xFCx0A"
-                 | MEM_FILL      [macro] rule MEM_FILL      => b"xFCx0B"
+  syntax Bytes ::= "I32_LOAD"      [macro] rule I32_LOAD      => b"\x28"
+  syntax Bytes ::= "I64_LOAD"      [macro] rule I64_LOAD      => b"\x29"
+  syntax Bytes ::= "F32_LOAD"      [macro] rule F32_LOAD      => b"\x2A"
+  syntax Bytes ::= "F64_LOAD"      [macro] rule F64_LOAD      => b"\x2B"
+  syntax Bytes ::= "I32_LOAD_8_S"  [macro] rule I32_LOAD_8_S  => b"\x2C"
+  syntax Bytes ::= "I32_LOAD_8_U"  [macro] rule I32_LOAD_8_U  => b"\x2D"
+  syntax Bytes ::= "I32_LOAD_16_S" [macro] rule I32_LOAD_16_S => b"\x2E"
+  syntax Bytes ::= "I32_LOAD_16_U" [macro] rule I32_LOAD_16_U => b"\x2F"
+  syntax Bytes ::= "I64_LOAD_8_S"  [macro] rule I64_LOAD_8_S  => b"\x30"
+  syntax Bytes ::= "I64_LOAD_8_U"  [macro] rule I64_LOAD_8_U  => b"\x31"
+  syntax Bytes ::= "I64_LOAD_16_S" [macro] rule I64_LOAD_16_S => b"\x32"
+  syntax Bytes ::= "I64_LOAD_16_U" [macro] rule I64_LOAD_16_U => b"\x33"
+  syntax Bytes ::= "I64_LOAD_32_S" [macro] rule I64_LOAD_32_S => b"\x34"
+  syntax Bytes ::= "I64_LOAD_32_U" [macro] rule I64_LOAD_32_U => b"\x35"
+  syntax Bytes ::= "I32_STORE"     [macro] rule I32_STORE     => b"\x36"
+  syntax Bytes ::= "I64_STORE"     [macro] rule I64_STORE     => b"\x37"
+  syntax Bytes ::= "F32_STORE"     [macro] rule F32_STORE     => b"\x38"
+  syntax Bytes ::= "F64_STORE"     [macro] rule F64_STORE     => b"\x39"
+  syntax Bytes ::= "I32_STORE_8"   [macro] rule I32_STORE_8   => b"\x3A"
+  syntax Bytes ::= "I32_STORE_16"  [macro] rule I32_STORE_16  => b"\x3B"
+  syntax Bytes ::= "I64_STORE_8"   [macro] rule I64_STORE_8   => b"\x3C"
+  syntax Bytes ::= "I64_STORE_16"  [macro] rule I64_STORE_16  => b"\x3D"
+  syntax Bytes ::= "I64_STORE_32"  [macro] rule I64_STORE_32  => b"\x3E"
+  syntax Bytes ::= "MEM_SIZE"      [macro] rule MEM_SIZE      => b"\x3F"
+  syntax Bytes ::= "MEM_GROW"      [macro] rule MEM_GROW      => b"\x40"
+  syntax Bytes ::= "MEM_INIT"      [macro] rule MEM_INIT      => b"\xFC\x08"
+  syntax Bytes ::= "DATA_DROP"     [macro] rule DATA_DROP     => b"\xFC\x09"
+  syntax Bytes ::= "MEM_COPY"      [macro] rule MEM_COPY      => b"\xFC\x0A"
+  syntax Bytes ::= "MEM_FILL"      [macro] rule MEM_FILL      => b"\xFC\x0B"
 ```
 
 _Numeric instructions_ have the following tags:
 
 ```k
-                 | I32_CONST           [macro] rule I32_CONST => b"x41"
-                 | I64_CONST           [macro] rule I64_CONST => b"x42"
-                 | F32_CONST           [macro] rule F32_CONST => b"x43"
-                 | F64_CONST           [macro] rule F64_CONST => b"x44"
-
-                 | I32_EQZ             [macro] rule I32_EQZ  => b"x45"
-                 | I32_EQ              [macro] rule I32_EQ   => b"x46"
-                 | I32_NE              [macro] rule I32_NE   => b"x47"
-                 | I32_LT_S            [macro] rule I32_LT_S => b"x48"
-                 | I32_LT_U            [macro] rule I32_LT_U => b"x49"
-                 | I32_GT_S            [macro] rule I32_GT_S => b"x4A"
-                 | I32_GT_U            [macro] rule I32_GT_U => b"x4B"
-                 | I32_LE_S            [macro] rule I32_LE_S => b"x4C"
-                 | I32_LE_U            [macro] rule I32_LE_U => b"x4D"
-                 | I32_GE_S            [macro] rule I32_GE_S => b"x4E"
-                 | I32_GE_U            [macro] rule I32_GE_U => b"x4F"
-
-                 | I64_EQZ             [macro] rule I64_EQZ  => b"x50"
-                 | I64_EQ              [macro] rule I64_EQ   => b"x51"
-                 | I64_NE              [macro] rule I64_NE   => b"x52"
-                 | I64_LT_S            [macro] rule I64_LT_S => b"x53"
-                 | I64_LT_U            [macro] rule I64_LT_U => b"x54"
-                 | I64_GT_S            [macro] rule I64_GT_S => b"x55"
-                 | I64_GT_U            [macro] rule I64_GT_U => b"x56"
-                 | I64_LE_S            [macro] rule I64_LE_S => b"x57"
-                 | I64_LE_U            [macro] rule I64_LE_U => b"x58"
-                 | I64_GE_S            [macro] rule I64_GE_S => b"x59"
-                 | I64_GE_U            [macro] rule I64_GE_U => b"x5A"
-
-                 | F32_EQ              [macro] rule F32_EQ => b"x5B"
-                 | F32_NE              [macro] rule F32_NE => b"x5C"
-                 | F32_LT              [macro] rule F32_LT => b"x5D"
-                 | F32_GT              [macro] rule F32_GT => b"x5E"
-                 | F32_LE              [macro] rule F32_LE => b"x5F"
-                 | F32_GE              [macro] rule F32_GE => b"x60"
-
-                 | F64_EQ              [macro] rule F64_EQ => b"x61"
-                 | F64_NE              [macro] rule F64_NE => b"x62"
-                 | F64_LT              [macro] rule F64_LT => b"x63"
-                 | F64_GT              [macro] rule F64_GT => b"x64"
-                 | F64_LE              [macro] rule F64_LE => b"x65"
-                 | F64_GE              [macro] rule F64_GE => b"x66"
-
-                 | I32_CLZ             [macro]
-                 | I32_CTZ             [macro]
-                 | I32_POPCNT          [macro]
-                 | I32_ADD             [macro]
-                 | I32_SUB             [macro]
-                 | I32_MUL             [macro]
-                 | I32_DIV_S           [macro]
-                 | I32_DIV_U           [macro]
-                 | I32_REM_S           [macro]
-                 | I32_REM_U           [macro]
-                 | I32_AND             [macro]
-                 | I32_OR              [macro]
-                 | I32_XOR             [macro]
-                 | I32_SHL             [macro]
-                 | I32_SHR_S           [macro]
-                 | I32_SHR_U           [macro]
-                 | I32_ROTL            [macro]
-                 | I32_ROTR            [macro]
-
-                 | I64_CLZ             [macro]
-                 | I64_CTZ             [macro]
-                 | I64_POPCNT          [macro]
-                 | I64_ADD             [macro]
-                 | I64_SUB             [macro]
-                 | I64_MUL             [macro]
-                 | I64_DIV_S           [macro]
-                 | I64_DIV_U           [macro]
-                 | I64_REM_S           [macro]
-                 | I64_REM_U           [macro]
-                 | I64_AND             [macro]
-                 | I64_OR              [macro]
-                 | I64_XOR             [macro]
-                 | I64_SHL             [macro]
-                 | I64_SHR_S           [macro]
-                 | I64_SHR_U           [macro]
-                 | I64_ROTL            [macro]
-                 | I64_ROTR            [macro]
-
-                 | F32_ABS             [macro]
-                 | F32_NEG             [macro]
-                 | F32_CEIL            [macro]
-                 | F32_FLOOR           [macro]
-                 | F32_TRUNC           [macro]
-                 | F32_NEARSET         [macro]
-                 | F32_SQRT            [macro]
-                 | F32_ADD             [macro]
-                 | F32_SUB             [macro]
-                 | F32_MUL             [macro]
-                 | F32_DIV             [macro]
-                 | F32_MIN             [macro]
-                 | F32_MAX             [macro]
-                 | F32_COPYSIGN        [macro]
-
-                 | F64_ABS             [macro]
-                 | F64_NEG             [macro]
-                 | F64_CEIL            [macro]
-                 | F64_FLOOR           [macro]
-                 | F64_TRUNC           [macro]
-                 | F64_NEARSET         [macro]
-                 | F64_SQRT            [macro]
-                 | F64_ADD             [macro]
-                 | F64_SUB             [macro]
-                 | F64_MUL             [macro]
-                 | F64_DIV             [macro]
-                 | F64_MIN             [macro]
-                 | F64_MAX             [macro]
-                 | F64_COPYSIGN        [macro]
-
-                 | I32_WRAP_I64        [macro]
-                 | I32_TRUNC_F32_S     [macro]
-                 | I32_TRUNC_F32_U     [macro]
-                 | I32_TRUNC_F64_S     [macro]
-                 | I32_TRUNC_F64_U     [macro]
-
-                 | I64_EXTEND_I32_S    [macro]
-                 | I64_EXTEND_I32_U    [macro]
-                 | I64_TRUNC_F32_S     [macro]
-                 | I64_TRUNC_F32_U     [macro]
-                 | I64_TRUNC_F64_S     [macro]
-                 | I64_TRUNC_F64_U     [macro]
-
-                 | F32_CONVERT_I32_S   [macro]
-                 | F32_CONVERT_I32_U   [macro]
-                 | F32_CONVERT_I64_S   [macro]
-                 | F32_CONVERT_I64_U   [macro]
-                 | F32_DEMOTE_F64      [macro]
-
-                 | F64_CONVERT_I32_S   [macro]
-                 | F64_CONVERT_I32_U   [macro]
-                 | F64_CONVERT_I64_S   [macro]
-                 | F64_CONVERT_I64_U   [macro]
-                 | F64_PROMOTE_F32     [macro]
-
-                 | I32_REINTERPRET_F32 [macro]
-                 | I64_REINTERPRET_F64 [macro]
-                 | F32_REINTERPRET_I32 [macro]
-                 | F64_REINTERPRET_I64 [macro]
-
-                 | I32_EXTEND_8_S      [macro]
-                 | I32_EXTEND_16_S     [macro]
-                 | I64_EXTEND_8_S      [macro]
-                 | I64_EXTEND_16_S     [macro]
-                 | I64_EXTEND_32_S     [macro]
+  syntax Bytes ::= "I32_CONST"           [macro] rule I32_CONST => b"\x41"
+  syntax Bytes ::= "I64_CONST"           [macro] rule I64_CONST => b"\x42"
+  syntax Bytes ::= "F32_CONST"           [macro] rule F32_CONST => b"\x43"
+  syntax Bytes ::= "F64_CONST"           [macro] rule F64_CONST => b"\x44"
+
+  syntax Bytes ::= "I32_EQZ"             [macro] rule I32_EQZ  => b"\x45"
+  syntax Bytes ::= "I32_EQ"              [macro] rule I32_EQ   => b"\x46"
+  syntax Bytes ::= "I32_NE"              [macro] rule I32_NE   => b"\x47"
+  syntax Bytes ::= "I32_LT_S"            [macro] rule I32_LT_S => b"\x48"
+  syntax Bytes ::= "I32_LT_U"            [macro] rule I32_LT_U => b"\x49"
+  syntax Bytes ::= "I32_GT_S"            [macro] rule I32_GT_S => b"\x4A"
+  syntax Bytes ::= "I32_GT_U"            [macro] rule I32_GT_U => b"\x4B"
+  syntax Bytes ::= "I32_LE_S"            [macro] rule I32_LE_S => b"\x4C"
+  syntax Bytes ::= "I32_LE_U"            [macro] rule I32_LE_U => b"\x4D"
+  syntax Bytes ::= "I32_GE_S"            [macro] rule I32_GE_S => b"\x4E"
+  syntax Bytes ::= "I32_GE_U"            [macro] rule I32_GE_U => b"\x4F"
+
+  syntax Bytes ::= "I64_EQZ"             [macro] rule I64_EQZ  => b"\x50"
+  syntax Bytes ::= "I64_EQ"              [macro] rule I64_EQ   => b"\x51"
+  syntax Bytes ::= "I64_NE"              [macro] rule I64_NE   => b"\x52"
+  syntax Bytes ::= "I64_LT_S"            [macro] rule I64_LT_S => b"\x53"
+  syntax Bytes ::= "I64_LT_U"            [macro] rule I64_LT_U => b"\x54"
+  syntax Bytes ::= "I64_GT_S"            [macro] rule I64_GT_S => b"\x55"
+  syntax Bytes ::= "I64_GT_U"            [macro] rule I64_GT_U => b"\x56"
+  syntax Bytes ::= "I64_LE_S"            [macro] rule I64_LE_S => b"\x57"
+  syntax Bytes ::= "I64_LE_U"            [macro] rule I64_LE_U => b"\x58"
+  syntax Bytes ::= "I64_GE_S"            [macro] rule I64_GE_S => b"\x59"
+  syntax Bytes ::= "I64_GE_U"            [macro] rule I64_GE_U => b"\x5A"
+
+  syntax Bytes ::= "F32_EQ"              [macro] rule F32_EQ => b"\x5B"
+  syntax Bytes ::= "F32_NE"              [macro] rule F32_NE => b"\x5C"
+  syntax Bytes ::= "F32_LT"              [macro] rule F32_LT => b"\x5D"
+  syntax Bytes ::= "F32_GT"              [macro] rule F32_GT => b"\x5E"
+  syntax Bytes ::= "F32_LE"              [macro] rule F32_LE => b"\x5F"
+  syntax Bytes ::= "F32_GE"              [macro] rule F32_GE => b"\x60"
+
+  syntax Bytes ::= "F64_EQ"              [macro] rule F64_EQ => b"\x61"
+  syntax Bytes ::= "F64_NE"              [macro] rule F64_NE => b"\x62"
+  syntax Bytes ::= "F64_LT"              [macro] rule F64_LT => b"\x63"
+  syntax Bytes ::= "F64_GT"              [macro] rule F64_GT => b"\x64"
+  syntax Bytes ::= "F64_LE"              [macro] rule F64_LE => b"\x65"
+  syntax Bytes ::= "F64_GE"              [macro] rule F64_GE => b"\x66"
+
+  syntax Bytes ::= "I32_CLZ"             [macro] rule I32_CLZ => b"\x67"
+  syntax Bytes ::= "I32_CTZ"             [macro] rule I32_CTZ => b"\x68"
+  syntax Bytes ::= "I32_POPCNT"          [macro] rule I32_POPCNT => b"\x69"
+  syntax Bytes ::= "I32_ADD"             [macro] rule I32_ADD => b"\x6A"
+  syntax Bytes ::= "I32_SUB"             [macro] rule I32_SUB => b"\x6B"
+  syntax Bytes ::= "I32_MUL"             [macro] rule I32_MUL => b"\x6C"
+  syntax Bytes ::= "I32_DIV_S"           [macro] rule I32_DIV_S => b"\x6D"
+  syntax Bytes ::= "I32_DIV_U"           [macro] rule I32_DIV_U => b"\x6E"
+  syntax Bytes ::= "I32_REM_S"           [macro] rule I32_REM_S => b"\x6F"
+  syntax Bytes ::= "I32_REM_U"           [macro] rule I32_REM_U => b"\x70"
+  syntax Bytes ::= "I32_AND"             [macro] rule I32_AND => b"\x71"
+  syntax Bytes ::= "I32_OR"              [macro] rule I32_OR => b"\x72"
+  syntax Bytes ::= "I32_XOR"             [macro] rule I32_XOR => b"\x73"
+  syntax Bytes ::= "I32_SHL"             [macro] rule I32_SHL => b"\x74"
+  syntax Bytes ::= "I32_SHR_S"           [macro] rule I32_SHR_S => b"\x75"
+  syntax Bytes ::= "I32_SHR_U"           [macro] rule I32_SHR_U => b"\x76"
+  syntax Bytes ::= "I32_ROTL"            [macro] rule I32_ROTL => b"\x77"
+  syntax Bytes ::= "I32_ROTR"            [macro] rule I32_ROTR => b"\x78"
+
+  syntax Bytes ::= "I64_CLZ"             [macro] rule I64_CLZ => b"\x79"
+  syntax Bytes ::= "I64_CTZ"             [macro] rule I64_CTZ => b"\x7A"
+  syntax Bytes ::= "I64_POPCNT"          [macro] rule I64_POPCNT => b"\x7B"
+  syntax Bytes ::= "I64_ADD"             [macro] rule I64_ADD => b"\x7C"
+  syntax Bytes ::= "I64_SUB"             [macro] rule I64_SUB => b"\x7D"
+  syntax Bytes ::= "I64_MUL"             [macro] rule I64_MUL => b"\x7E"
+  syntax Bytes ::= "I64_DIV_S"           [macro] rule I64_DIV_S => b"\x7F"
+  syntax Bytes ::= "I64_DIV_U"           [macro] rule I64_DIV_U => b"\x80"
+  syntax Bytes ::= "I64_REM_S"           [macro] rule I64_REM_S => b"\x81"
+  syntax Bytes ::= "I64_REM_U"           [macro] rule I64_REM_U => b"\x82"
+  syntax Bytes ::= "I64_AND"             [macro] rule I64_AND => b"\x83"
+  syntax Bytes ::= "I64_OR"              [macro] rule I64_OR => b"\x84"
+  syntax Bytes ::= "I64_XOR"             [macro] rule I64_XOR => b"\x85"
+  syntax Bytes ::= "I64_SHL"             [macro] rule I64_SHL => b"\x86"
+  syntax Bytes ::= "I64_SHR_S"           [macro] rule I64_SHR_S => b"\x87"
+  syntax Bytes ::= "I64_SHR_U"           [macro] rule I64_SHR_U => b"\x88"
+  syntax Bytes ::= "I64_ROTL"            [macro] rule I64_ROTL => b"\x89"
+  syntax Bytes ::= "I64_ROTR"            [macro] rule I64_ROTR => b"\x8A"
+
+  syntax Bytes ::= "F32_ABS"             [macro] rule F32_ABS => b"\x8B"
+  syntax Bytes ::= "F32_NEG"             [macro] rule F32_NEG => b"\x8C"
+  syntax Bytes ::= "F32_CEIL"            [macro] rule F32_CEIL => b"\x8D"
+  syntax Bytes ::= "F32_FLOOR"           [macro] rule F32_FLOOR => b"\x8E"
+  syntax Bytes ::= "F32_TRUNC"           [macro] rule F32_TRUNC => b"\x8F"
+  syntax Bytes ::= "F32_NEAREST"         [macro] rule F32_NEAREST => b"\x90"
+  syntax Bytes ::= "F32_SQRT"            [macro] rule F32_SQRT => b"\x91"
+  syntax Bytes ::= "F32_ADD"             [macro] rule F32_ADD => b"\x92"
+  syntax Bytes ::= "F32_SUB"             [macro] rule F32_SUB => b"\x93"
+  syntax Bytes ::= "F32_MUL"             [macro] rule F32_MUL => b"\x94"
+  syntax Bytes ::= "F32_DIV"             [macro] rule F32_DIV => b"\x95"
+  syntax Bytes ::= "F32_MIN"             [macro] rule F32_MIN => b"\x96"
+  syntax Bytes ::= "F32_MAX"             [macro] rule F32_MAX => b"\x97"
+  syntax Bytes ::= "F32_COPYSIGN"        [macro] rule F32_COPYSIGN => b"\x98"
+
+  syntax Bytes ::= "F64_ABS"             [macro] rule F64_ABS => b"\x99"
+  syntax Bytes ::= "F64_NEG"             [macro] rule F64_NEG => b"\x9A"
+  syntax Bytes ::= "F64_CEIL"            [macro] rule F64_CEIL => b"\x9B"
+  syntax Bytes ::= "F64_FLOOR"           [macro] rule F64_FLOOR => b"\x9C"
+  syntax Bytes ::= "F64_TRUNC"           [macro] rule F64_TRUNC => b"\x9D"
+  syntax Bytes ::= "F64_NEAREST"         [macro] rule F64_NEAREST => b"\x9E"
+  syntax Bytes ::= "F64_SQRT"            [macro] rule F64_SQRT => b"\x9F"
+  syntax Bytes ::= "F64_ADD"             [macro] rule F64_ADD => b"\xA0"
+  syntax Bytes ::= "F64_SUB"             [macro] rule F64_SUB => b"\xA1"
+  syntax Bytes ::= "F64_MUL"             [macro] rule F64_MUL => b"\xA2"
+  syntax Bytes ::= "F64_DIV"             [macro] rule F64_DIV => b"\xA3"
+  syntax Bytes ::= "F64_MIN"             [macro] rule F64_MIN => b"\xA4"
+  syntax Bytes ::= "F64_MAX"             [macro] rule F64_MAX => b"\xA5"
+  syntax Bytes ::= "F64_COPYSIGN"        [macro] rule F64_COPYSIGN => b"\xA6"
+
+  syntax Bytes ::= "I32_WRAP_I64"        [macro] rule I32_WRAP_I64 => b"\xA7"
+  syntax Bytes ::= "I32_TRUNC_F32_S"     [macro] rule I32_TRUNC_F32_S => b"\xA8"
+  syntax Bytes ::= "I32_TRUNC_F32_U"     [macro] rule I32_TRUNC_F32_U => b"\xA9"
+  syntax Bytes ::= "I32_TRUNC_F64_S"     [macro] rule I32_TRUNC_F64_S => b"\xAA"
+  syntax Bytes ::= "I32_TRUNC_F64_U"     [macro] rule I32_TRUNC_F64_U => b"\xAB"
+
+  syntax Bytes ::= "I64_EXTEND_I32_S"    [macro] rule I64_EXTEND_I32_S => b"\xAC"
+  syntax Bytes ::= "I64_EXTEND_I32_U"    [macro] rule I64_EXTEND_I32_U => b"\xAD"
+  syntax Bytes ::= "I64_TRUNC_F32_S"     [macro] rule I64_TRUNC_F32_S => b"\xAE"
+  syntax Bytes ::= "I64_TRUNC_F32_U"     [macro] rule I64_TRUNC_F32_U => b"\xAF"
+  syntax Bytes ::= "I64_TRUNC_F64_S"     [macro] rule I64_TRUNC_F64_S => b"\xB0"
+  syntax Bytes ::= "I64_TRUNC_F64_U"     [macro] rule I64_TRUNC_F64_U => b"\xB1"
+
+  syntax Bytes ::= "F32_CONVERT_I32_S"   [macro] rule F32_CONVERT_I32_S => b"\xB2"
+  syntax Bytes ::= "F32_CONVERT_I32_U"   [macro] rule F32_CONVERT_I32_U => b"\xB3"
+  syntax Bytes ::= "F32_CONVERT_I64_S"   [macro] rule F32_CONVERT_I64_S => b"\xB4"
+  syntax Bytes ::= "F32_CONVERT_I64_U"   [macro] rule F32_CONVERT_I64_U => b"\xB5"
+  syntax Bytes ::= "F32_DEMOTE_F64"      [macro] rule F32_DEMOTE_F64 => b"\xB6"
+
+  syntax Bytes ::= "F64_CONVERT_I32_S"   [macro] rule F64_CONVERT_I32_S => b"\xB7"
+  syntax Bytes ::= "F64_CONVERT_I32_U"   [macro] rule F64_CONVERT_I32_U => b"\xB8"
+  syntax Bytes ::= "F64_CONVERT_I64_S"   [macro] rule F64_CONVERT_I64_S => b"\xB9"
+  syntax Bytes ::= "F64_CONVERT_I64_U"   [macro] rule F64_CONVERT_I64_U => b"\xBA"
+  syntax Bytes ::= "F64_PROMOTE_F32"     [macro] rule F64_PROMOTE_F32 => b"\xBB"
+
+  syntax Bytes ::= "I32_REINTERPRET_F32" [macro] rule I32_REINTERPRET_F32 => b"\xBC"
+  syntax Bytes ::= "I64_REINTERPRET_F64" [macro] rule I64_REINTERPRET_F64 => b"\xBD"
+  syntax Bytes ::= "F32_REINTERPRET_I32" [macro] rule F32_REINTERPRET_I32 => b"\xBE"
+  syntax Bytes ::= "F64_REINTERPRET_I64" [macro] rule F64_REINTERPRET_I64 => b"\xBF"
+
+  syntax Bytes ::= "I32_EXTEND_8_S"      [macro] rule I32_EXTEND_8_S => b"\xC0"
+  syntax Bytes ::= "I32_EXTEND_16_S"     [macro] rule I32_EXTEND_16_S => b"\xC1"
+  syntax Bytes ::= "I64_EXTEND_8_S"      [macro] rule I64_EXTEND_8_S => b"\xC2"
+  syntax Bytes ::= "I64_EXTEND_16_S"     [macro] rule I64_EXTEND_16_S => b"\xC3"
+  syntax Bytes ::= "I64_EXTEND_32_S"     [macro] rule I64_EXTEND_32_S => b"\xC4"
+
+  syntax Bytes ::= "I32_TRUNC_SAT_F32_S" [macro] rule I32_TRUNC_SAT_F32_S => b"\xFC\x00"
+  syntax Bytes ::= "I32_TRUNC_SAT_F32_U" [macro] rule I32_TRUNC_SAT_F32_U => b"\xFC\x01"
+  syntax Bytes ::= "I32_TRUNC_SAT_F64_S" [macro] rule I32_TRUNC_SAT_F64_S => b"\xFC\x02"
+  syntax Bytes ::= "I32_TRUNC_SAT_F64_U" [macro] rule I32_TRUNC_SAT_F64_U => b"\xFC\x03"
+  syntax Bytes ::= "I64_TRUNC_SAT_F32_S" [macro] rule I64_TRUNC_SAT_F32_S => b"\xFC\x04"
+  syntax Bytes ::= "I64_TRUNC_SAT_F32_U" [macro] rule I64_TRUNC_SAT_F32_U => b"\xFC\x05"
+  syntax Bytes ::= "I64_TRUNC_SAT_F64_S" [macro] rule I64_TRUNC_SAT_F64_S => b"\xFC\x06"
+  syntax Bytes ::= "I64_TRUNC_SAT_F64_U" [macro] rule I64_TRUNC_SAT_F64_U => b"\xFC\x07"
+```
+
+_Vector instructions_ have the following tags:
+
+```k
+
+  syntax Bytes ::= "V128_LOAD" [macro] rule V128_LOAD => b"\xFD\x00"
+  syntax Bytes ::= "V128_LOAD_8X8_S" [macro] rule V128_LOAD_8X8_S => b"\xFD\x01"
+  syntax Bytes ::= "V128_LOAD_8X8_U" [macro] rule V128_LOAD_8X8_U => b"\xFD\x02"
+  syntax Bytes ::= "V128_LOAD_16X4_S" [macro] rule V128_LOAD_16X4_S => b"\xFD\x03"
+  syntax Bytes ::= "V128_LOAD_16X4_U" [macro] rule V128_LOAD_16X4_U => b"\xFD\x04"
+  syntax Bytes ::= "V128_LOAD_32X2_S" [macro] rule V128_LOAD_32X2_S => b"\xFD\x05"
+  syntax Bytes ::= "V128_LOAD_32X2_U" [macro] rule V128_LOAD_32X2_U => b"\xFD\x06"
+  syntax Bytes ::= "V128_LOAD_8_SPLAT" [macro] rule V128_LOAD_8_SPLAT => b"\xFD\x07"
+  syntax Bytes ::= "V128_LOAD_16_SPLAT" [macro] rule V128_LOAD_16_SPLAT => b"\xFD\x08"
+  syntax Bytes ::= "V128_LOAD_32_SPLAT" [macro] rule V128_LOAD_32_SPLAT => b"\xFD\x09"
+  syntax Bytes ::= "V128_LOAD_64_SPLAT" [macro] rule V128_LOAD_64_SPLAT => b"\xFD\x0A"
+  syntax Bytes ::= "V128_LOAD_32_ZERO" [macro] rule V128_LOAD_32_ZERO => b"\xFD\x5C"
+  syntax Bytes ::= "V128_LOAD_64_ZERO" [macro] rule V128_LOAD_64_ZERO => b"\xFD\x5D"
+  syntax Bytes ::= "V128_STORE" [macro] rule V128_STORE => b"\xFD\x0B"
+  syntax Bytes ::= "V128_LOAD_8_LANE" [macro] rule V128_LOAD_8_LANE => b"\xFD\x54"
+  syntax Bytes ::= "V128_LOAD_16_LANE" [macro] rule V128_LOAD_16_LANE => b"\xFD\x55"
+  syntax Bytes ::= "V128_LOAD_32_LANE" [macro] rule V128_LOAD_32_LANE => b"\xFD\x56"
+  syntax Bytes ::= "V128_LOAD_64_LANE" [macro] rule V128_LOAD_64_LANE => b"\xFD\x57"
+  syntax Bytes ::= "V128_STORE_8_LANE" [macro] rule V128_STORE_8_LANE => b"\xFD\x58"
+  syntax Bytes ::= "V128_STORE_16_LANE" [macro] rule V128_STORE_16_LANE => b"\xFD\x59"
+  syntax Bytes ::= "V128_STORE_32_LANE" [macro] rule V128_STORE_32_LANE => b"\xFD\x5A"
+  syntax Bytes ::= "V128_STORE_64_LANE" [macro] rule V128_STORE_64_LANE => b"\xFD\x5B"
+
+  syntax Bytes ::= "V128_CONST_BYTES" [macro] rule V128_CONST_BYTES => b"\xFD\x0C"
+
+  syntax Bytes ::= "I8X16_SHUFFLE" [macro] rule I8X16_SHUFFLE => b"\xFD\x0D"
+
+  syntax Bytes ::= "I8X16_EXTRACT_LANE_S" [macro] rule I8X16_EXTRACT_LANE_S => b"\xFD\x15"
+  syntax Bytes ::= "I8X16_EXTRACT_LANE_U" [macro] rule I8X16_EXTRACT_LANE_U => b"\xFD\x16"
+  syntax Bytes ::= "I8X16_REPLACE_LANE" [macro] rule I8X16_REPLACE_LANE => b"\xFD\x17"
+  syntax Bytes ::= "I16X8_EXTRACT_LANE_S" [macro] rule I16X8_EXTRACT_LANE_S => b"\xFD\x18"
+  syntax Bytes ::= "I16X8_EXTRACT_LANE_U" [macro] rule I16X8_EXTRACT_LANE_U => b"\xFD\x19"
+  syntax Bytes ::= "I16X8_REPLACE_LANE" [macro] rule I16X8_REPLACE_LANE => b"\xFD\x1A"
+  syntax Bytes ::= "I32X4_EXTRACT_LANE" [macro] rule I32X4_EXTRACT_LANE => b"\xFD\x1B"
+  syntax Bytes ::= "I32X4_REPLACE_LANE" [macro] rule I32X4_REPLACE_LANE => b"\xFD\x1C"
+  syntax Bytes ::= "I64X2_EXTRACT_LANE" [macro] rule I64X2_EXTRACT_LANE => b"\xFD\x1D"
+  syntax Bytes ::= "I64X2_REPLACE_LANE" [macro] rule I64X2_REPLACE_LANE => b"\xFD\x1E"
+  syntax Bytes ::= "F32X4_EXTRACT_LANE" [macro] rule F32X4_EXTRACT_LANE => b"\xFD\x1F"
+  syntax Bytes ::= "F32X4_REPLACE_LANE" [macro] rule F32X4_REPLACE_LANE => b"\xFD\x20"
+  syntax Bytes ::= "F64X2_EXTRACT_LANE" [macro] rule F64X2_EXTRACT_LANE => b"\xFD\x21"
+  syntax Bytes ::= "F64X2_REPLACE_LANE" [macro] rule F64X2_REPLACE_LANE => b"\xFD\x22"
+
+  syntax Bytes ::= "I8X16_SWIZZLE" [macro] rule I8X16_SWIZZLE => b"\xFD\x0E"
+  syntax Bytes ::= "I8X16_SPLAT" [macro] rule I8X16_SPLAT => b"\xFD\x0F"
+  syntax Bytes ::= "I16X8_SPLAT" [macro] rule I16X8_SPLAT => b"\xFD\x10"
+  syntax Bytes ::= "I32X4_SPLAT" [macro] rule I32X4_SPLAT => b"\xFD\x11"
+  syntax Bytes ::= "I64X2_SPLAT" [macro] rule I64X2_SPLAT => b"\xFD\x12"
+  syntax Bytes ::= "F32X4_SPLAT" [macro] rule F32X4_SPLAT => b"\xFD\x13"
+  syntax Bytes ::= "F64X2_SPLAT" [macro] rule F64X2_SPLAT => b"\xFD\x14"
+
+  syntax Bytes ::= "I8X16_EQ" [macro] rule I8X16_EQ => b"\xFD\x23"
+  syntax Bytes ::= "I8X16_NE" [macro] rule I8X16_NE => b"\xFD\x24"
+  syntax Bytes ::= "I8X16_LT_S" [macro] rule I8X16_LT_S => b"\xFD\x25"
+  syntax Bytes ::= "I8X16_LT_U" [macro] rule I8X16_LT_U => b"\xFD\x26"
+  syntax Bytes ::= "I8X16_GT_S" [macro] rule I8X16_GT_S => b"\xFD\x27"
+  syntax Bytes ::= "I8X16_GT_U" [macro] rule I8X16_GT_U => b"\xFD\x28"
+  syntax Bytes ::= "I8X16_LE_S" [macro] rule I8X16_LE_S => b"\xFD\x29"
+  syntax Bytes ::= "I8X16_LE_U" [macro] rule I8X16_LE_U => b"\xFD\x2A"
+  syntax Bytes ::= "I8X16_GE_S" [macro] rule I8X16_GE_S => b"\xFD\x2B"
+  syntax Bytes ::= "I8X16_GE_U" [macro] rule I8X16_GE_U => b"\xFD\x2C"
+
+  syntax Bytes ::= "I16X8_EQ" [macro] rule I16X8_EQ => b"\xFD\x2D"
+  syntax Bytes ::= "I16X8_NE" [macro] rule I16X8_NE => b"\xFD\x2E"
+  syntax Bytes ::= "I16X8_LT_S" [macro] rule I16X8_LT_S => b"\xFD\x2F"
+  syntax Bytes ::= "I16X8_LT_U" [macro] rule I16X8_LT_U => b"\xFD\x30"
+  syntax Bytes ::= "I16X8_GT_S" [macro] rule I16X8_GT_S => b"\xFD\x31"
+  syntax Bytes ::= "I16X8_GT_U" [macro] rule I16X8_GT_U => b"\xFD\x32"
+  syntax Bytes ::= "I16X8_LE_S" [macro] rule I16X8_LE_S => b"\xFD\x33"
+  syntax Bytes ::= "I16X8_LE_U" [macro] rule I16X8_LE_U => b"\xFD\x34"
+  syntax Bytes ::= "I16X8_GE_S" [macro] rule I16X8_GE_S => b"\xFD\x35"
+  syntax Bytes ::= "I16X8_GE_U" [macro] rule I16X8_GE_U => b"\xFD\x36"
+
+  syntax Bytes ::= "I32X4_EQ" [macro] rule I32X4_EQ => b"\xFD\x37"
+  syntax Bytes ::= "I32X4_NE" [macro] rule I32X4_NE => b"\xFD\x38"
+  syntax Bytes ::= "I32X4_LT_S" [macro] rule I32X4_LT_S => b"\xFD\x39"
+  syntax Bytes ::= "I32X4_LT_U" [macro] rule I32X4_LT_U => b"\xFD\x3A"
+  syntax Bytes ::= "I32X4_GT_S" [macro] rule I32X4_GT_S => b"\xFD\x3B"
+  syntax Bytes ::= "I32X4_GT_U" [macro] rule I32X4_GT_U => b"\xFD\x3C"
+  syntax Bytes ::= "I32X4_LE_S" [macro] rule I32X4_LE_S => b"\xFD\x3D"
+  syntax Bytes ::= "I32X4_LE_U" [macro] rule I32X4_LE_U => b"\xFD\x3E"
+  syntax Bytes ::= "I32X4_GE_S" [macro] rule I32X4_GE_S => b"\xFD\x3F"
+  syntax Bytes ::= "I32X4_GE_U" [macro] rule I32X4_GE_U => b"\xFD\x40"
+
+  syntax Bytes ::= "I64X2_EQ" [macro] rule I64X2_EQ => b"\xFD\xD6X01"
+  syntax Bytes ::= "I64X2_NE" [macro] rule I64X2_NE => b"\xFD\xD7X01"
+  syntax Bytes ::= "I64X2_LT_S" [macro] rule I64X2_LT_S => b"\xFD\xD8X01"
+  syntax Bytes ::= "I64X2_GT_S" [macro] rule I64X2_GT_S => b"\xFD\xD9X01"
+  syntax Bytes ::= "I64X2_LE_S" [macro] rule I64X2_LE_S => b"\xFD\xDA\x01"
+  syntax Bytes ::= "I64X2_GE_S" [macro] rule I64X2_GE_S => b"\xFD\xDB\x01"
+
+  syntax Bytes ::= "F32X4_EQ" [macro] rule F32X4_EQ => b"\xFD\x41"
+  syntax Bytes ::= "F32X4_NE" [macro] rule F32X4_NE => b"\xFD\x42"
+  syntax Bytes ::= "F32X4_LT" [macro] rule F32X4_LT => b"\xFD\x43"
+  syntax Bytes ::= "F32X4_GT" [macro] rule F32X4_GT => b"\xFD\x44"
+  syntax Bytes ::= "F32X4_LE" [macro] rule F32X4_LE => b"\xFD\x45"
+  syntax Bytes ::= "F32X4_GE" [macro] rule F32X4_GE => b"\xFD\x46"
+
+  syntax Bytes ::= "F64X2_EQ" [macro] rule F64X2_EQ => b"\xFD\x47"
+  syntax Bytes ::= "F64X2_NE" [macro] rule F64X2_NE => b"\xFD\x48"
+  syntax Bytes ::= "F64X2_LT" [macro] rule F64X2_LT => b"\xFD\x49"
+  syntax Bytes ::= "F64X2_GT" [macro] rule F64X2_GT => b"\xFD\x4A"
+  syntax Bytes ::= "F64X2_LE" [macro] rule F64X2_LE => b"\xFD\x4B"
+  syntax Bytes ::= "F64X2_GE" [macro] rule F64X2_GE => b"\xFD\x4C"
+
+  syntax Bytes ::= "V128_NOT" [macro] rule V128_NOT => b"\xFD\x4D"
+  syntax Bytes ::= "V128_AND" [macro] rule V128_AND => b"\xFD\x4E"
+  syntax Bytes ::= "V128_ANDNOT" [macro] rule V128_ANDNOT => b"\xFD\x4F"
+  syntax Bytes ::= "V128_OR" [macro] rule V128_OR => b"\xFD\x50"
+  syntax Bytes ::= "V128_XOR" [macro] rule V128_XOR => b"\xFD\x51"
+  syntax Bytes ::= "V128_BITSELECT" [macro] rule V128_BITSELECT => b"\xFD\x52"
+  syntax Bytes ::= "V128_ANY_TRUE" [macro] rule V128_ANY_TRUE => b"\xFD\x53"
+
+  syntax Bytes ::= "I8X16_ABS" [macro] rule I8X16_ABS => b"\xFD\x60"
+  syntax Bytes ::= "I8X16_NEG" [macro] rule I8X16_NEG => b"\xFD\x61"
+  syntax Bytes ::= "I8X16_POPCNT" [macro] rule I8X16_POPCNT => b"\xFD\x62"
+  syntax Bytes ::= "I8X16_ALL_TRUE" [macro] rule I8X16_ALL_TRUE => b"\xFD\x63"
+  syntax Bytes ::= "I8X16_BITMASK" [macro] rule I8X16_BITMASK => b"\xFD\x64"
+  syntax Bytes ::= "I8X16_NARROW_I16X8_S" [macro] rule I8X16_NARROW_I16X8_S => b"\xFD\x65"
+  syntax Bytes ::= "I8X16_NARROW_I16X8_U" [macro] rule I8X16_NARROW_I16X8_U => b"\xFD\x66"
+  syntax Bytes ::= "I8X16_SHL" [macro] rule I8X16_SHL => b"\xFD\x6B"
+  syntax Bytes ::= "I8X16_SHR_S" [macro] rule I8X16_SHR_S => b"\xFD\x6C"
+  syntax Bytes ::= "I8X16_SHR_U" [macro] rule I8X16_SHR_U => b"\xFD\x6D"
+  syntax Bytes ::= "I8X16_ADD" [macro] rule I8X16_ADD => b"\xFD\x6E"
+  syntax Bytes ::= "I8X16_ADD_SAT_S" [macro] rule I8X16_ADD_SAT_S => b"\xFD\x6F"
+  syntax Bytes ::= "I8X16_ADD_SAT_U" [macro] rule I8X16_ADD_SAT_U => b"\xFD\x70"
+  syntax Bytes ::= "I8X16_SUB" [macro] rule I8X16_SUB => b"\xFD\x71"
+  syntax Bytes ::= "I8X16_SUB_SAT_S" [macro] rule I8X16_SUB_SAT_S => b"\xFD\x72"
+  syntax Bytes ::= "I8X16_SUB_SAT_U" [macro] rule I8X16_SUB_SAT_U => b"\xFD\x73"
+  syntax Bytes ::= "I8X16_MIN_S" [macro] rule I8X16_MIN_S => b"\xFD\x76"
+  syntax Bytes ::= "I8X16_MIN_U" [macro] rule I8X16_MIN_U => b"\xFD\x77"
+  syntax Bytes ::= "I8X16_MAX_S" [macro] rule I8X16_MAX_S => b"\xFD\x78"
+  syntax Bytes ::= "I8X16_MAX_U" [macro] rule I8X16_MAX_U => b"\xFD\x79"
+  syntax Bytes ::= "I8X16_AVGR_U" [macro] rule I8X16_AVGR_U => b"\xFD\x7B"
+
+  syntax Bytes ::= "I16X8_EXTADD_PAIRWISE_I8X16_S" [macro] rule I16X8_EXTADD_PAIRWISE_I8X16_S => b"\xFD\x7C"
+  syntax Bytes ::= "I16X8_EXTADD_PAIRWISE_I8X16_U" [macro] rule I16X8_EXTADD_PAIRWISE_I8X16_U => b"\xFD\x7D"
+  syntax Bytes ::= "I16X8_ABS" [macro] rule I16X8_ABS => b"\xFD\x80\x01"
+  syntax Bytes ::= "I16X8_NEG" [macro] rule I16X8_NEG => b"\xFD\x81\x01"
+  syntax Bytes ::= "I16X8_Q15MULR_SAT_S" [macro] rule I16X8_Q15MULR_SAT_S => b"\xFD\x82\x01"
+  syntax Bytes ::= "I16X8_ALL_TRUE" [macro] rule I16X8_ALL_TRUE => b"\xFD\x83\x01"
+  syntax Bytes ::= "I16X8_BITMASK" [macro] rule I16X8_BITMASK => b"\xFD\x84\x01"
+  syntax Bytes ::= "I16X8_NARROW_I32X4_S" [macro] rule I16X8_NARROW_I32X4_S => b"\xFD\x85\x01"
+  syntax Bytes ::= "I16X8_NARROW_I32X4_U" [macro] rule I16X8_NARROW_I32X4_U => b"\xFD\x86\x01"
+  syntax Bytes ::= "I16X8_EXTEND_LOW_I8X16_S" [macro] rule I16X8_EXTEND_LOW_I8X16_S => b"\xFD\x87\x01"
+  syntax Bytes ::= "I16X8_EXTEND_HIGH_I8X16_S" [macro] rule I16X8_EXTEND_HIGH_I8X16_S => b"\xFD\x88\x01"
+  syntax Bytes ::= "I16X8_EXTEND_LOW_I8X16_U" [macro] rule I16X8_EXTEND_LOW_I8X16_U => b"\xFD\x89\x01"
+  syntax Bytes ::= "I16X8_EXTEND_HIGH_I8X16_U" [macro] rule I16X8_EXTEND_HIGH_I8X16_U => b"\xFD\x8A\x01"
+  syntax Bytes ::= "I16X8_SHL" [macro] rule I16X8_SHL => b"\xFD\x8B\x01"
+  syntax Bytes ::= "I16X8_SHR_S" [macro] rule I16X8_SHR_S => b"\xFD\x8C\x01"
+  syntax Bytes ::= "I16X8_SHR_U" [macro] rule I16X8_SHR_U => b"\xFD\x8D\x01"
+  syntax Bytes ::= "I16X8_ADD" [macro] rule I16X8_ADD => b"\xFD\x8E\x01"
+  syntax Bytes ::= "I16X8_ADD_SAT_S" [macro] rule I16X8_ADD_SAT_S => b"\xFD\x8F\x01"
+  syntax Bytes ::= "I16X8_ADD_SAT_U" [macro] rule I16X8_ADD_SAT_U => b"\xFD\x90\x01"
+  syntax Bytes ::= "I16X8_SUB" [macro] rule I16X8_SUB => b"\xFD\x91\x01"
+  syntax Bytes ::= "I16X8_SUB_SAT_S" [macro] rule I16X8_SUB_SAT_S => b"\xFD\x92\x01"
+  syntax Bytes ::= "I16X8_SUB_SAT_U" [macro] rule I16X8_SUB_SAT_U => b"\xFD\x93\x01"
+  syntax Bytes ::= "I16X8_MUL" [macro] rule I16X8_MUL => b"\xFD\x95\x01"
+  syntax Bytes ::= "I16X8_MIN_S" [macro] rule I16X8_MIN_S => b"\xFD\x96\x01"
+  syntax Bytes ::= "I16X8_MIN_U" [macro] rule I16X8_MIN_U => b"\xFD\x97\x01"
+  syntax Bytes ::= "I16X8_MAX_S" [macro] rule I16X8_MAX_S => b"\xFD\x98\x01"
+  syntax Bytes ::= "I16X8_MAX_U" [macro] rule I16X8_MAX_U => b"\xFD\x99\x01"
+  syntax Bytes ::= "I16X8_AVGR_U" [macro] rule I16X8_AVGR_U => b"\xFD\x9B\x01"
+  syntax Bytes ::= "I16X8_EXTMUL_LOW_I8X16_S" [macro] rule I16X8_EXTMUL_LOW_I8X16_S => b"\xFD\x9C\x01"
+  syntax Bytes ::= "I16X8_EXTMUL_HIGH_I8X16_S" [macro] rule I16X8_EXTMUL_HIGH_I8X16_S => b"\xFD\x9D\x01"
+  syntax Bytes ::= "I16X8_EXTMUL_LOW_I8X16_U" [macro] rule I16X8_EXTMUL_LOW_I8X16_U => b"\xFD\x9E\x01"
+  syntax Bytes ::= "I16X8_EXTMUL_HIGH_I8X16_U" [macro] rule I16X8_EXTMUL_HIGH_I8X16_U => b"\xFD\x9F\x01"
+
+  syntax Bytes ::= "I32X4_EXTADD_PAIRWISE_I16X8_S" [macro] rule I32X4_EXTADD_PAIRWISE_I16X8_S => b"\xFD\x7E"
+  syntax Bytes ::= "I32X4_EXTADD_PAIRWISE_I16X8_U" [macro] rule I32X4_EXTADD_PAIRWISE_I16X8_U => b"\xFD\x7F"
+  syntax Bytes ::= "I32X4_ABS" [macro] rule I32X4_ABS => b"\xFD\xA0\x01"
+  syntax Bytes ::= "I32X4_NEG" [macro] rule I32X4_NEG => b"\xFD\xA1\x01"
+  syntax Bytes ::= "I32X4_ALL_TRUE" [macro] rule I32X4_ALL_TRUE => b"\xFD\xA3\x01"
+  syntax Bytes ::= "I32X4_BITMASK" [macro] rule I32X4_BITMASK => b"\xFD\xA4\x01"
+  syntax Bytes ::= "I32X4_EXTEND_LOW_I16X8_S" [macro] rule I32X4_EXTEND_LOW_I16X8_S => b"\xFD\xA7\x01"
+  syntax Bytes ::= "I32X4_EXTEND_HIGH_I16X8_S" [macro] rule I32X4_EXTEND_HIGH_I16X8_S => b"\xFD\xA8\x01"
+  syntax Bytes ::= "I32X4_EXTEND_LOW_I16X8_U" [macro] rule I32X4_EXTEND_LOW_I16X8_U => b"\xFD\xA9\x01"
+  syntax Bytes ::= "I32X4_EXTEND_HIGH_I16X8_U" [macro] rule I32X4_EXTEND_HIGH_I16X8_U => b"\xFD\xAA\x01"
+  syntax Bytes ::= "I32X4_SHL" [macro] rule I32X4_SHL => b"\xFD\xAB\x01"
+  syntax Bytes ::= "I32X4_SHR_S" [macro] rule I32X4_SHR_S => b"\xFD\xAC\x01"
+  syntax Bytes ::= "I32X4_SHR_U" [macro] rule I32X4_SHR_U => b"\xFD\xAD\x01"
+  syntax Bytes ::= "I32X4_ADD" [macro] rule I32X4_ADD => b"\xFD\xAE\x01"
+  syntax Bytes ::= "I32X4_SUB" [macro] rule I32X4_SUB => b"\xFD\xB1\x01"
+  syntax Bytes ::= "I32X4_MUL" [macro] rule I32X4_MUL => b"\xFD\xB5\x01"
+  syntax Bytes ::= "I32X4_MIN_S" [macro] rule I32X4_MIN_S => b"\xFD\xB6\x01"
+  syntax Bytes ::= "I32X4_MIN_U" [macro] rule I32X4_MIN_U => b"\xFD\xB7\x01"
+  syntax Bytes ::= "I32X4_MAX_S" [macro] rule I32X4_MAX_S => b"\xFD\xB8\x01"
+  syntax Bytes ::= "I32X4_MAX_U" [macro] rule I32X4_MAX_U => b"\xFD\xB9\x01"
+  syntax Bytes ::= "I32X4_DOT_I16X8" [macro] rule I32X4_DOT_I16X8 => b"\xFD\xBA\x01"
+  syntax Bytes ::= "I32X4_EXTMUL_LOW_I16X8_S" [macro] rule I32X4_EXTMUL_LOW_I16X8_S => b"\xFD\xBC\x01"
+  syntax Bytes ::= "I32X4_EXTMUL_HIGH_I16X8_S" [macro] rule I32X4_EXTMUL_HIGH_I16X8_S => b"\xFD\xBD\x01"
+  syntax Bytes ::= "I32X4_EXTMUL_LOW_I16X8_U" [macro] rule I32X4_EXTMUL_LOW_I16X8_U => b"\xFD\xBE\x01"
+  syntax Bytes ::= "I32X4_EXTMUL_HIGH_I16X8_U" [macro] rule I32X4_EXTMUL_HIGH_I16X8_U => b"\xFD\xBF\x01"
+
+  syntax Bytes ::= "I64X2_ABS" [macro] rule I64X2_ABS => b"\xFD\xC0\x01"
+  syntax Bytes ::= "I64X2_NEG" [macro] rule I64X2_NEG => b"\xFD\xC1\x01"
+  syntax Bytes ::= "I64X2_ALL_TRUE" [macro] rule I64X2_ALL_TRUE => b"\xFD\xC3\x01"
+  syntax Bytes ::= "I64X2_BITMASK" [macro] rule I64X2_BITMASK => b"\xFD\xC4\x01"
+  syntax Bytes ::= "I64X2_EXTEND_LOW_I32X4_S" [macro] rule I64X2_EXTEND_LOW_I32X4_S => b"\xFD\xC7\x01"
+  syntax Bytes ::= "I64X2_EXTEND_HIGH_I32X4_S" [macro] rule I64X2_EXTEND_HIGH_I32X4_S => b"\xFD\xC8\x01"
+  syntax Bytes ::= "I64X2_EXTEND_LOW_I32X4_U" [macro] rule I64X2_EXTEND_LOW_I32X4_U => b"\xFD\xC9\x01"
+  syntax Bytes ::= "I64X2_EXTEND_HIGH_I32X4_U" [macro] rule I64X2_EXTEND_HIGH_I32X4_U => b"\xFD\xCA\x01"
+  syntax Bytes ::= "I64X2_SHL" [macro] rule I64X2_SHL => b"\xFD\xCB\x01"
+  syntax Bytes ::= "I64X2_SHR_S" [macro] rule I64X2_SHR_S => b"\xFD\xCC\x01"
+  syntax Bytes ::= "I64X2_SHR_U" [macro] rule I64X2_SHR_U => b"\xFD\xCD\x01"
+  syntax Bytes ::= "I64X2_ADD" [macro] rule I64X2_ADD => b"\xFD\xCE\x01"
+  syntax Bytes ::= "I64X2_SUB" [macro] rule I64X2_SUB => b"\xFD\xD1\x01"
+  syntax Bytes ::= "I64X2_MUL" [macro] rule I64X2_MUL => b"\xFD\xD5\x01"
+  syntax Bytes ::= "I64X2_EXTMUL_LOW_I32X4_S" [macro] rule I64X2_EXTMUL_LOW_I32X4_S => b"\xFD\xDC\x01"
+  syntax Bytes ::= "I64X2_EXTMUL_HIGH_I32X4_S" [macro] rule I64X2_EXTMUL_HIGH_I32X4_S => b"\xFD\xDD\x01"
+  syntax Bytes ::= "I64X2_EXTMUL_LOW_I32X4_U" [macro] rule I64X2_EXTMUL_LOW_I32X4_U => b"\xFD\xDE\x01"
+  syntax Bytes ::= "I64X2_EXTMUL_HIGH_I32X4_U" [macro] rule I64X2_EXTMUL_HIGH_I32X4_U => b"\xFD\xDF\x01"
+
+  syntax Bytes ::= "F32X4_CEIL" [macro] rule F32X4_CEIL => b"\xFD\x67"
+  syntax Bytes ::= "F32X4_FLOOR" [macro] rule F32X4_FLOOR => b"\xFD\x68"
+  syntax Bytes ::= "F32X4_TRUNC" [macro] rule F32X4_TRUNC => b"\xFD\x69"
+  syntax Bytes ::= "F32X4_NEAREST" [macro] rule F32X4_NEAREST => b"\xFD\x6A"
+  syntax Bytes ::= "F32X4_ABS" [macro] rule F32X4_ABS => b"\xFD\xE0\x01"
+  syntax Bytes ::= "F32X4_NEG" [macro] rule F32X4_NEG => b"\xFD\xE1\x01"
+  syntax Bytes ::= "F32X4_SQRT" [macro] rule F32X4_SQRT => b"\xFD\xE3\x01"
+  syntax Bytes ::= "F32X4_ADD" [macro] rule F32X4_ADD => b"\xFD\xE4\x01"
+  syntax Bytes ::= "F32X4_SUB" [macro] rule F32X4_SUB => b"\xFD\xE5\x01"
+  syntax Bytes ::= "F32X4_MUL" [macro] rule F32X4_MUL => b"\xFD\xE6\x01"
+  syntax Bytes ::= "F32X4_DIV" [macro] rule F32X4_DIV => b"\xFD\xE7\x01"
+  syntax Bytes ::= "F32X4_MIN" [macro] rule F32X4_MIN => b"\xFD\xE8\x01"
+  syntax Bytes ::= "F32X4_MAX" [macro] rule F32X4_MAX => b"\xFD\xE9\x01"
+  syntax Bytes ::= "F32X4_PMIN" [macro] rule F32X4_PMIN => b"\xFD\xEA\x01"
+  syntax Bytes ::= "F32X4_PMAX" [macro] rule F32X4_PMAX => b"\xFD\xEB\x01"
+
+  syntax Bytes ::= "F64X2_CEIL" [macro] rule F64X2_CEIL => b"\xFD\x74"
+  syntax Bytes ::= "F64X2_FLOOR" [macro] rule F64X2_FLOOR => b"\xFD\x75"
+  syntax Bytes ::= "F64X2_TRUNC" [macro] rule F64X2_TRUNC => b"\xFD\x7A"
+  syntax Bytes ::= "F64X2_NEAREST" [macro] rule F64X2_NEAREST => b"\xFD\x94\x01"
+  syntax Bytes ::= "F64X2_ABS" [macro] rule F64X2_ABS => b"\xFD\xEC\x01"
+  syntax Bytes ::= "F64X2_NEG" [macro] rule F64X2_NEG => b"\xFD\xED\x01"
+  syntax Bytes ::= "F64X2_SQRT" [macro] rule F64X2_SQRT => b"\xFD\xEF\x01"
+  syntax Bytes ::= "F64X2_ADD" [macro] rule F64X2_ADD => b"\xFD\xF0\x01"
+  syntax Bytes ::= "F64X2_SUB" [macro] rule F64X2_SUB => b"\xFD\xF1\x01"
+  syntax Bytes ::= "F64X2_MUL" [macro] rule F64X2_MUL => b"\xFD\xF2\x01"
+  syntax Bytes ::= "F64X2_DIV" [macro] rule F64X2_DIV => b"\xFD\xF3\x01"
+  syntax Bytes ::= "F64X2_MIN" [macro] rule F64X2_MIN => b"\xFD\xF4\x01"
+  syntax Bytes ::= "F64X2_MAX" [macro] rule F64X2_MAX => b"\xFD\xF5\x01"
+  syntax Bytes ::= "F64X2_PMIN" [macro] rule F64X2_PMIN => b"\xFD\xF6\x01"
+  syntax Bytes ::= "F64X2_PMAX" [macro] rule F64X2_PMAX => b"\xFD\xF7\x01"
+
+  syntax Bytes ::= "I32X4_TRUNC_SAT_F32X4_S" [macro] rule I32X4_TRUNC_SAT_F32X4_S => b"\xFD\xF8\x01"
+  syntax Bytes ::= "I32X4_TRUNC_SAT_F32X4_U" [macro] rule I32X4_TRUNC_SAT_F32X4_U => b"\xFD\xF9\x01"
+  syntax Bytes ::= "F32X4_CONVERT_I32X4_S" [macro] rule F32X4_CONVERT_I32X4_S => b"\xFD\xFA\x01"
+  syntax Bytes ::= "F32X4_CONVERT_I32X4_U" [macro] rule F32X4_CONVERT_I32X4_U => b"\xFD\xFB\x01"
+  syntax Bytes ::= "I32X4_TRUNC_SAT_F64X2_S_ZERO" [macro] rule I32X4_TRUNC_SAT_F64X2_S_ZERO => b"\xFD\xFC\x01"
+  syntax Bytes ::= "I32X4_TRUNC_SAT_F64X2_U_ZERO" [macro] rule I32X4_TRUNC_SAT_F64X2_U_ZERO => b"\xFD\xFD\x01"
+  syntax Bytes ::= "F64X2_CONVERT_LOW_I32X4_S" [macro] rule F64X2_CONVERT_LOW_I32X4_S => b"\xFD\xFE\x01"
+  syntax Bytes ::= "F64X2_CONVERT_LOW_I32X4_U" [macro] rule F64X2_CONVERT_LOW_I32X4_U => b"\xFD\xFF\x01"
+  syntax Bytes ::= "F32X4_DEMOTE_F64X2_ZERO" [macro] rule F32X4_DEMOTE_F64X2_ZERO => b"\xFD\x5E"
+  syntax Bytes ::= "F64X2_PROMOTE_LOW_F32X4" [macro] rule F64X2_PROMOTE_LOW_F32X4 => b"\xFD\x5F"
+```
+
+_Expression_ encoding
+
+```k
+
+ syntax Bytes ::= "END" [macro] rule END => b"\x0B"
+
 ```
 
 ```k
@@ -368,12 +645,12 @@ module BINARY_PARSER [private]
   imports WASM
   imports BINARY_PARSER_DATA
 
-  syntax ParseResult ::= ModuleDecl
-                       | ParseError(String)
+  syntax ParseResult ::= "M"oduleDecl
+        syntax Bytes ::= "P"arseError(String)
 
 
   syntax ModuleDecl ::= parseModule(Bytes)  [function, total]
-                      | parseMagic(Bytes)   [function, total]
-                      | parseVersion(Bytes) [function, total]
+       syntax Bytes ::= parseMagic(Bytes)   [function, total]
+       syntax Bytes ::= parseVersion(Bytes) [function, total]
 
 endmodule

From ade86df7b57db5095278c3d2da29d69fab4bcce8 Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@pi2.network>
Date: Thu, 9 Jan 2025 15:39:14 +0200
Subject: [PATCH 4/9] Add link to doc

---
 pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
index 3b2995aa5..19ffb99f3 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -1,6 +1,7 @@
 # Wasm Binary Parser
 
-This file defines a Wasm binary parser.
+This file defines a Wasm binary parser based on this
+[spec](https://webassembly.github.io/spec/core/binary/index.html).
 To begin, we define constant macros which drive the parser process.
 
 ```k

From c9a471f9035b8605a2a652880064eb98d28abfba Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@pi2.network>
Date: Thu, 9 Jan 2025 15:47:59 +0200
Subject: [PATCH 5/9] Fix counter instructions

---
 tests/ulm/counter/rust/README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/ulm/counter/rust/README.md b/tests/ulm/counter/rust/README.md
index 3732105f1..3fd59657d 100644
--- a/tests/ulm/counter/rust/README.md
+++ b/tests/ulm/counter/rust/README.md
@@ -14,10 +14,11 @@ To build the contract with all of the size minimization options, first, ensure t
 ```sh
 rustup install nightly
 rustup target add wasm32-unknown-unknown --toolchain nightly
+rustup component add rust-src --toolchain nightly-x86_64-unknown-linux-gnu
 ```
 
 Then run the build script as follows:
 
 ```sh
-build.sh
+./build.sh
 ```

From ea3e28bdd05617c24bb20e3d629251172bc84cf6 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Mon, 13 Jan 2025 20:32:24 +0200
Subject: [PATCH 6/9] Update
 pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md

Co-authored-by: Stephen Skeirik <stephen.skeirik@pi2.network>
---
 pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
index 19ffb99f3..cf49bf369 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -105,7 +105,7 @@ These have special use requirements as we will see later.
   syntax Bytes ::= "TYPE_F64"     [macro] rule TYPE_F64     => b"\x7C"
   syntax Bytes ::= "TYPE_VEC"     [macro] rule TYPE_VEC     => b"\x7B"
   syntax Bytes ::= "TYPE_FUN_REF" [macro] rule TYPE_FUN_REF => b"\x70"
-  syntax Bytes ::= "TYPE_EXT_REF" [macro] rule TYPE_EXT_REF => b"\x64"
+  syntax Bytes ::= "TYPE_EXT_REF" [macro] rule TYPE_EXT_REF => b"\x6F"
   syntax Bytes ::= "TYPE_FUN"     [macro] rule TYPE_FUN     => b"\x60"
   syntax Bytes ::= "TYPE_EMPTY"   [macro] rule TYPE_EMPTY   => b"\x40"
 ```

From 8c3f4a242e29ae0dfe42747f2ba9bb56ae17816b Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Mon, 13 Jan 2025 20:34:04 +0200
Subject: [PATCH 7/9] Apply suggestions from code review

Co-authored-by: Stephen Skeirik <stephen.skeirik@pi2.network>
---
 .../pykwasm/kdist/wasm-semantics/binary-parser.md | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
index cf49bf369..c96a26a45 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -152,7 +152,10 @@ _Reference instructions_ are encoded with the following tags:
   syntax Bytes ::= "REF_ISNULL" [macro] rule REF_ISNULL => b"\xD1"
   syntax Bytes ::= "REF_FUNC"   [macro] rule REF_FUNC   => b"\xD2"
 ```
-
+```k
+  syntax Bytes ::= "DROP"           [macro] rule DROP           => b"\x1A"
+  syntax Bytes ::= "SELECT"         [macro] rule SELECT         => b"\x1B"
+  syntax Bytes ::= "SELECT_GENERIC" [macro] rule SELECT_GENERIC => b"\x1C"
 _Variable instructions_ are encoded with the following tags:
 
 ```k
@@ -457,10 +460,10 @@ _Vector instructions_ have the following tags:
   syntax Bytes ::= "I32X4_GE_S" [macro] rule I32X4_GE_S => b"\xFD\x3F"
   syntax Bytes ::= "I32X4_GE_U" [macro] rule I32X4_GE_U => b"\xFD\x40"
 
-  syntax Bytes ::= "I64X2_EQ" [macro] rule I64X2_EQ => b"\xFD\xD6X01"
-  syntax Bytes ::= "I64X2_NE" [macro] rule I64X2_NE => b"\xFD\xD7X01"
-  syntax Bytes ::= "I64X2_LT_S" [macro] rule I64X2_LT_S => b"\xFD\xD8X01"
-  syntax Bytes ::= "I64X2_GT_S" [macro] rule I64X2_GT_S => b"\xFD\xD9X01"
+  syntax Bytes ::= "I64X2_EQ" [macro] rule I64X2_EQ => b"\xFD\xD6\x01"
+  syntax Bytes ::= "I64X2_NE" [macro] rule I64X2_NE => b"\xFD\xD7\x01"
+  syntax Bytes ::= "I64X2_LT_S" [macro] rule I64X2_LT_S => b"\xFD\xD8\x01"
+  syntax Bytes ::= "I64X2_GT_S" [macro] rule I64X2_GT_S => b"\xFD\xD9\x01"
   syntax Bytes ::= "I64X2_LE_S" [macro] rule I64X2_LE_S => b"\xFD\xDA\x01"
   syntax Bytes ::= "I64X2_GE_S" [macro] rule I64X2_GE_S => b"\xFD\xDB\x01"
 
@@ -561,7 +564,7 @@ _Vector instructions_ have the following tags:
   syntax Bytes ::= "I32X4_MIN_U" [macro] rule I32X4_MIN_U => b"\xFD\xB7\x01"
   syntax Bytes ::= "I32X4_MAX_S" [macro] rule I32X4_MAX_S => b"\xFD\xB8\x01"
   syntax Bytes ::= "I32X4_MAX_U" [macro] rule I32X4_MAX_U => b"\xFD\xB9\x01"
-  syntax Bytes ::= "I32X4_DOT_I16X8" [macro] rule I32X4_DOT_I16X8 => b"\xFD\xBA\x01"
+  syntax Bytes ::= "I32X4_DOT_I16X8_S" [macro] rule I32X4_DOT_I16X8_S => b"\xFD\xBA\x01"
   syntax Bytes ::= "I32X4_EXTMUL_LOW_I16X8_S" [macro] rule I32X4_EXTMUL_LOW_I16X8_S => b"\xFD\xBC\x01"
   syntax Bytes ::= "I32X4_EXTMUL_HIGH_I16X8_S" [macro] rule I32X4_EXTMUL_HIGH_I16X8_S => b"\xFD\xBD\x01"
   syntax Bytes ::= "I32X4_EXTMUL_LOW_I16X8_U" [macro] rule I32X4_EXTMUL_LOW_I16X8_U => b"\xFD\xBE\x01"

From b65fa2796ba28457481bc8ed9a5a6534805c5ca5 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Mon, 13 Jan 2025 20:34:34 +0200
Subject: [PATCH 8/9] Update tests/ulm/counter/rust/README.md

Co-authored-by: Stephen Skeirik <stephen.skeirik@pi2.network>
---
 tests/ulm/counter/rust/README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/ulm/counter/rust/README.md b/tests/ulm/counter/rust/README.md
index 3fd59657d..4d59810cd 100644
--- a/tests/ulm/counter/rust/README.md
+++ b/tests/ulm/counter/rust/README.md
@@ -1,6 +1,6 @@
-# Rust/Wasm ERC20 Contract
+# Rust/Wasm Counter Contract
 
-This directory contains a Rust implementation of an ERC20 contract that is compiled into Wasm.
+This directory contains a Rust implementation of an Counter contract that is compiled into Wasm.
 
 As is the case with many chains that use Wasm contracts, we compile this Rust project as a library;
 that way, functions referenced in external libraries become host functions which can be provided via Wasm module imports.

From 37f496672cbbdc7ce544d62f2b8ff022cce3b88d Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@pi2.network>
Date: Mon, 13 Jan 2025 20:42:08 +0200
Subject: [PATCH 9/9] Fix review suggestions

---
 pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
index c96a26a45..c3abd1951 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/binary-parser.md
@@ -152,10 +152,13 @@ _Reference instructions_ are encoded with the following tags:
   syntax Bytes ::= "REF_ISNULL" [macro] rule REF_ISNULL => b"\xD1"
   syntax Bytes ::= "REF_FUNC"   [macro] rule REF_FUNC   => b"\xD2"
 ```
+
 ```k
   syntax Bytes ::= "DROP"           [macro] rule DROP           => b"\x1A"
   syntax Bytes ::= "SELECT"         [macro] rule SELECT         => b"\x1B"
   syntax Bytes ::= "SELECT_GENERIC" [macro] rule SELECT_GENERIC => b"\x1C"
+```
+
 _Variable instructions_ are encoded with the following tags:
 
 ```k