diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md
index 1ed01b680..2cd20e5f1 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md
@@ -24,7 +24,7 @@ module WASM-AUXIL
          <instrs> #clearConfig => .K ...    </instrs>
          <curModIdx>         _ => .Int      </curModIdx>
          <valstack>          _ => .ValStack </valstack>
-         <locals>            _ => .Map      </locals>
+         <locals>            _ => .List     </locals>
          <moduleInstances>   _ => .Bag      </moduleInstances>
          <moduleIds>         _ => .Map      </moduleIds>
          <nextModuleIdx>     _ => 0         </nextModuleIdx>
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
index 59c0fb6f9..52c4a445c 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
@@ -430,7 +430,8 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca
 
 ```k
     rule <instrs> #assertLocal INDEX VALUE _ => .K ... </instrs>
-         <locals> ... INDEX |-> VALUE ... </locals>
+         <locals> LOCALS </locals>
+      requires LOCALS[INDEX] ==K VALUE
 
     rule <instrs> #assertGlobal TFIDX VALUE _ => .K ... </instrs>
          <curModIdx> CUR </curModIdx>
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
index 4d23c2dda..2d2684a58 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
@@ -1174,7 +1174,6 @@ They are currently supported in KWasm text files, but may be deprecated.
 
     rule #t2aInstr<C>(#block(VT:VecType, IS:Instrs, BLOCKINFO)) => #block(VT, #t2aInstrs<C>(IS), BLOCKINFO)
 
-    rule #t2aInstr<_>(init_local I V) => init_local I V
     rule #t2aInstr<_>(init_locals VS) => init_locals VS
 ```
 
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
index a0d4e8bfd..d0afb4e72 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
@@ -164,10 +164,9 @@ Internal Syntax
 module WASM-INTERNAL-SYNTAX
     imports WASM-DATA-INTERNAL-SYNTAX
 
-    syntax Instr ::=  "init_local"  Int Val
-                   |  "init_locals"     ValStack
-                   | "#init_locals" Int ValStack
- // --------------------------------------------
+    syntax Instr ::=  "init_locals" ValStack
+                   | "#init_locals" ValStack
+ // ----------------------------------------
 
     syntax Int ::= #pageSize()      [function, total]
     syntax Int ::= #maxMemorySize() [function, total]
@@ -202,8 +201,8 @@ module WASM
         <instrs> .K </instrs>
         <valstack> .ValStack </valstack>
         <curFrame>
-          <locals>    .Map </locals>
-          <curModIdx> .Int </curModIdx>
+          <locals>    .List </locals>
+          <curModIdx> .Int  </curModIdx>
         </curFrame>
         <moduleRegistry> .Map </moduleRegistry>
         <moduleIds> .Map </moduleIds>
@@ -549,17 +548,15 @@ Variable Operators
 The various `init_local` variants assist in setting up the `locals` cell.
 
 ```k
-    rule <instrs> init_local INDEX VALUE => .K ... </instrs>
-         <locals> LOCALS => LOCALS [ INDEX <- VALUE ] </locals>
-
-    rule <instrs> init_locals VALUES => #init_locals 0 VALUES ... </instrs>
+    rule <instrs> init_locals VALUES => #init_locals VALUES ... </instrs>
+         <locals> _ => .List </locals>
 
-    rule <instrs> #init_locals _ .ValStack => .K ... </instrs>
-    rule <instrs> #init_locals N (VALUE : VALSTACK)
-               => init_local N VALUE
-               ~> #init_locals (N +Int 1) VALSTACK
+    rule <instrs> #init_locals .ValStack => .K ... </instrs>
+    rule <instrs> #init_locals (VALUE : VALSTACK)
+               => #init_locals VALSTACK
                ...
           </instrs>
+         <locals> ... .List => ListItem(VALUE) </locals>
 ```
 
 The `*_local` instructions are defined here.
@@ -570,18 +567,18 @@ The `*_local` instructions are defined here.
                    | "#local.tee" "(" Int ")" [klabel(aLocal.tee), symbol]
  // ----------------------------------------------------------------------
     rule <instrs> #local.get(I) => .K ... </instrs>
-         <valstack> VALSTACK => VALUE : VALSTACK </valstack>
-         <locals> ... I |-> VALUE ... </locals>
+         <valstack> VALSTACK => {LOCALS [ I ]}:>Val : VALSTACK </valstack>
+         <locals> LOCALS </locals>
 
     rule <instrs> #local.set(I) => .K ... </instrs>
          <valstack> VALUE : VALSTACK => VALSTACK </valstack>
          <locals> LOCALS => LOCALS[I <- VALUE] </locals>
-        requires I in_keys(LOCALS)
+        requires I >=Int 0 andBool I <Int size(LOCALS)
 
     rule <instrs> #local.tee(I) => .K ... </instrs>
          <valstack> VALUE : _VALSTACK </valstack>
          <locals> LOCALS => LOCALS[I <- VALUE] </locals>
-        requires I in_keys(LOCALS)
+        requires I >=Int 0 andBool I <Int size(LOCALS)
 ```
 
 ### Globals
@@ -1164,8 +1161,8 @@ Similar to labels, they sit on the instruction stack (the `<instrs>` cell), and
 Unlike labels, only one frame can be "broken" through at a time.
 
 ```k
-    syntax Frame ::= "frame" Int ValTypes ValStack Map
- // --------------------------------------------------
+    syntax Frame ::= "frame" Int ValTypes ValStack List
+ // ---------------------------------------------------
     rule <instrs> frame MODIDX' TRANGE VALSTACK' LOCAL' => .K ... </instrs>
          <valstack> VALSTACK => #take(lengthValTypes(TRANGE), VALSTACK) ++ VALSTACK' </valstack>
          <locals> _ => LOCAL' </locals>
@@ -1187,7 +1184,7 @@ The `#take` function will return the parameter stack in the reversed order, then
                ...
          </instrs>
          <valstack>  VALSTACK => .ValStack </valstack>
-         <locals> LOCAL => .Map </locals>
+         <locals> LOCAL </locals>
          <curModIdx> MODIDX => MODIDX' </curModIdx>
          <funcDef>
            <fAddr>    FADDR                     </fAddr>
diff --git a/tests/success-llvm.out b/tests/success-llvm.out
index 0eae581e8..bdfd25dfa 100644
--- a/tests/success-llvm.out
+++ b/tests/success-llvm.out
@@ -11,7 +11,7 @@
     </valstack>
     <curFrame>
       <locals>
-        .Map
+        .List
       </locals>
       <curModIdx>
         .Int