diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
index e2e327194..693828104 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
@@ -83,7 +83,7 @@ infer that this must be the top configuration, so it will wrap it in
 A special configuration cell is added in the local case to support VM initialization.
 
 ```local
-        <entry> $ENTRY:String </entry>
+        <entry> $ENTRY:WasmString </entry>
 ```
 
 
@@ -91,13 +91,95 @@ A special configuration cell is added in the local case to support VM initializa
       </ulmWasm>
 ```
 
+Implementing all unresolved imports as hooks
+--------------------------------------------
+
+```k
+
+    syntax String ::= wasmString2StringStripped ( WasmString ) [function]
+                    | #stripQuotes ( String ) [function]
+ // ----------------------------------------------------
+    rule wasmString2StringStripped(WS) => #stripQuotes(#parseWasmString(WS))
+
+    rule #stripQuotes(S) => replaceAll(S, "\"", "")
+
+    syntax IdentifierToken ::= String2Identifier(String) [function, total, hook(STRING.string2token)]
+
+```
+
+First, we create an empty module for any import referencing a non-existing module.
+
+```k
+
+    rule
+        <instrs> #import(MOD, _, _) ... </instrs>
+        <moduleRegistry> MR:Map => MR [ MOD <- NEXT ] </moduleRegistry>
+        <nextModuleIdx> NEXT => NEXT +Int 1 </nextModuleIdx>
+        <moduleInstances> ( .Bag => <moduleInst> <modIdx> NEXT </modIdx> ... </moduleInst>) ... </moduleInstances>
+        requires notBool MOD in_keys(MR)
+
+```
+
+Next, for each import referencing a non-existing function, we add a function
+that just invokes a (non-wasm) `hostCall` instruction.
+
+```k
+
+    syntax Instr ::= hostCall(String, String, FuncType)
+ // ---------------------------------------------------
+    rule
+        <instrs>
+            (  .K
+            => allocfunc
+                ( HOSTMOD, NEXTADDR, TYPE, [ .ValTypes ]
+                , hostCall
+                    ( wasmString2StringStripped(MOD)
+                    , wasmString2StringStripped(NAME)
+                    , TYPE
+                    )
+                  .Instrs
+                , #meta
+                    (... id: String2Identifier
+                        ( "$auto-alloc:"
+                        +String #parseWasmString(MOD)
+                        +String ":"
+                        +String #parseWasmString(NAME)
+                        )
+                    , localIds: .Map
+                    )
+                )
+            )
+            ~> #import(MOD, NAME, #funcDesc(... type: TIDX))
+            ...
+        </instrs>
+        <curModIdx> CUR </curModIdx>
+        <moduleInst>
+            <modIdx> CUR </modIdx>
+            <types> ... TIDX |-> TYPE ... </types>
+            ...
+        </moduleInst>
+        <nextFuncAddr> NEXTADDR => NEXTADDR +Int 1 </nextFuncAddr>
+        <moduleRegistry> ... MOD |-> HOSTMOD ... </moduleRegistry>
+        <moduleInst>
+            <modIdx> HOSTMOD </modIdx>
+            <exports> EXPORTS => EXPORTS [NAME <- NEXTFUNC ] </exports>
+            <funcAddrs> FS => setExtend(FS, NEXTFUNC, NEXTADDR, -1) </funcAddrs>
+            <nextFuncIdx> NEXTFUNC => NEXTFUNC +Int 1 </nextFuncIdx>
+            <nextTypeIdx> NEXTTYPE => NEXTTYPE +Int 1 </nextTypeIdx>
+            <types> TYPES => TYPES [ NEXTTYPE <- TYPE ] </types>
+            ...
+        </moduleInst>
+    requires notBool NAME in_keys(EXPORTS)
+
+```
+
 Obtaining the Entrypoint
 ------------------------
 
 In the standalone semantics, the Wasm VM obtains an entrypoint from the configuration.
 
 ```local
-    syntax String ::= #getEntryPoint() [function, total]
+    syntax WasmString ::= #getEntryPoint() [function, total]
     rule #getEntryPoint() => FUNCNAME
          [[ <entry> FUNCNAME </entry> ]]
 ```
@@ -105,8 +187,8 @@ In the standalone semantics, the Wasm VM obtains an entrypoint from the configur
 In the remote semantics, the Wasm VM has a fixed entrypoint.
 
 ```remote
-    syntax String ::= #getEntryPoint() [function, total]
-    rule #getEntryPoint() => "ulmDispatchCaller"
+    syntax WasmString ::= #getEntryPoint() [function, total]
+    rule #getEntryPoint() => #token("\"ulmDispatchCaller\"", "WasmStringToken")
 ```
 
 Passing Control
@@ -123,8 +205,8 @@ Note that entrypoint resolution must occur _after_ the Wasm module has been load
 This is ensured by requiring that the `<instrs>` cell is empty during resolution.
 
 ```k
-    syntax Initializer ::= #resolveCurModuleFuncExport(String)
-                         | #resolveModuleFuncExport(Int, String)
+    syntax Initializer ::= #resolveCurModuleFuncExport(WasmString)
+                         | #resolveModuleFuncExport(Int, WasmString)
                          | #resolveFunc(Int, ListInt)
     // ----------------------------------------------
     rule <k> #resolveCurModuleFuncExport(FUNCNAME) => #resolveModuleFuncExport(MODIDX, FUNCNAME) </k>