From 1c11f3cee7591c23f7109f79400be0b45a261444 Mon Sep 17 00:00:00 2001
From: Stephen Skeirik <stephen.skeirik@runtimeverification.com>
Date: Fri, 6 Dec 2024 19:35:50 -0500
Subject: [PATCH] fix decoding

---
 .../pykwasm/kdist/wasm-semantics/ulm-wasm.md  | 29 +++++--------------
 1 file changed, 8 insertions(+), 21 deletions(-)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
index 5fd99da41..d6f7b6c72 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
@@ -4,10 +4,8 @@ requires "ulm.k"
 ```
 
 ```k
-module ULM-WASM-COMMON-SYNTAX
-   imports WASM-COMMON-SYNTAX
-   imports BOOL-SYNTAX
-   imports INT-SYNTAX
+module ULM-WASM-SYNTAX
+    imports WASM
 ```
 
 Program Encoding
@@ -18,13 +16,12 @@ The ULM-integrated WASM VM has two possible program encodings:
 1.  In the local test VM case, a direct encoding is used.
 
     ```local
-    syntax PgmEncoding ::= Stmts
+    syntax PgmEncoding ::= ModuleDecl
     ```
 
 2.  In the remote ULM-integrated VM case, a byte encoding is used.
 
     ```remote
-    imports BYTES-SYNTAX
     syntax PgmEncoding ::= Bytes
     ```
 
@@ -32,17 +29,9 @@ The ULM-integrated WASM VM has two possible program encodings:
 endmodule
 ```
 
-```k
-module ULM-WASM-SYNTAX
-    imports ULM-WASM-COMMON-SYNTAX
-    imports WASM-SYNTAX
-endmodule
-```
-
 ```k
 module ULM-WASM
-    imports ULM-WASM-COMMON-SYNTAX
-    imports WASM
+    imports ULM-WASM-SYNTAX
     imports ULM
 ```
 
@@ -54,9 +43,9 @@ The WASM VM must decode the input program:
 1.  In local test VM case, the decoding function is just identity.
 
     ```local
-    syntax Stmts ::= decodePgm(Stmts) [function, total]
-    // ------------------------------------------------
-    rule decodePgm(Stmts) => Stmts
+    syntax ModuleDecl ::= decodePgm(ModuleDecl) [function, total]
+    // ----------------------------------------------------------
+    rule decodePgm(Mod) => Mod
     ```
 
 2.  In the remote ULM-integrated VM case, a specialized, hooked byte decoder is used.
@@ -96,9 +85,7 @@ The embedder loads the module to be executed and then resolves the entrypoint fu
 ```k
     rule <k> PGM:PgmEncoding => #resolveCurModuleFuncExport(FUNCNAME) </k>
          <entry> FUNCNAME </entry>
-         <instrs> .K
-               => sequenceStmts(text2abstract(decodePgm(PGM)))
-         </instrs>
+         <instrs> .K => decodePgm(PGM) </instrs>
 ```
 
 Note that entrypoint resolution must occur _after_ the Wasm module has been loaded.