change <memAddrs> and <mems> cells from Map to List (#5)

* change `<memAddrs>` and `<mems>` cells from Map to List * Adjusting checking bounds requires --------- Co-authored-by: Dwight Guth <[email protected]>
Pi-Squared-Inc · Aug 9, 2024 · 331b68d · 331b68d
1 parent 7113711
commit 331b68d
Show file tree

Hide file tree

Showing 4 changed files with 77 additions and 163 deletions.
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md
@@ -34,8 +34,7 @@ module WASM-AUXIL
            <funcs>           _ => .Bag      </funcs>
            <nextTabAddr>     _ => 0         </nextTabAddr>
            <tabs>            _ => .Bag      </tabs>
-           <nextMemAddr>     _ => 0         </nextMemAddr>
-           <mems>            _ => .Bag      </mems>
+           <mems>            _ => .List     </mems>
            <nextGlobAddr>    _ => 0         </nextGlobAddr>
            <globals>         _ => .Bag      </globals>
            <nextElemAddr>    _ => 0         </nextElemAddr>

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
@@ -570,37 +570,25 @@ This checks that the last allocated memory has the given size and max value.
          <moduleInst>
            <modIdx> CUR </modIdx>
            <memIds> IDS </memIds>
-           <memAddrs> #ContextLookup(IDS, TFIDX) |-> ADDR </memAddrs>
+           <memAddrs> ListItem(ADDR) </memAddrs>
            ...
          </moduleInst>
-         <mems>
-           <memInst>
-             <mAddr>   ADDR  </mAddr>
-             <mmax>    MAX   </mmax>
-             <msize>   SIZE  </msize>
-             ...
-           </memInst>
-           ...
-         </mems>
+         <mems> MEMS </mems>
+      requires ADDR <Int size(MEMS)
+        andBool #ContextLookup(IDS, TFIDX) ==K 0 andBool (#let memInst(MAX', SIZE', _) = MEMS[ADDR] #in MAX ==K MAX' andBool SIZE ==K SIZE')
 
     rule <instrs> #assertMemoryData (KEY , VAL) MSG => #assertMemoryData CUR (KEY, VAL) MSG ... </instrs>
          <curModIdx> CUR </curModIdx>
 
     rule <instrs> #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ... </instrs>
          <moduleInst>
            <modIdx> MODIDX </modIdx>
-           <memAddrs> 0 |-> ADDR </memAddrs>
+           <memAddrs> ListItem(ADDR) </memAddrs>
            ...
          </moduleInst>
-         <mems>
-           <memInst>
-             <mAddr> ADDR </mAddr>
-             <mdata> BM </mdata>
-             ...
-           </memInst>
-           ...
-         </mems>
-      requires #getRange(BM, KEY, 1) ==Int VAL
+         <mems> MEMS </mems>
+      requires ADDR <Int size(MEMS)
+        andBool (#let memInst(_, _, BM) = MEMS[ADDR] #in #getRange(BM, KEY, 1) ==Int VAL)
 ```
 
 ### Module Assertions