decoder: remove dead stub-immediate path, fix stale docstrings (#127)

* decoder: remove dead stub-immediate path, fix stale docstrings

`stubImmediateCount` unconditionally returns `none` (all GC ops are decoded for
real now), which makes the `some n => consumeStubAtoms …` branch that calls it
statically unreachable and `consumeStubAtoms` dead. This removes both and folds
the branch to its only reachable arm (`.ok rest`), keeping the live
`consumeBrOnCastImmediates` case untouched — behaviour is unchanged.

It also refreshes several comments that no longer match the decoder: the
top-of-file and `parseModule` docstrings (type/table/memory/global/elem/data/tag
content is fully parsed now, not discarded), the `parsePlainOp` catch-all
(floats and SIMD are modelled; the fallback only stubs still-unmodelled proposals
like atomics), and the `isMemOp` comments (memory ops emit real load/stores).

* decoder+array: correct import docstrings, generalize slice callee bridge

Address code-review findings on the decoder cleanup and the new slice corpus:

- Wat.lean: the module-header and `parseModule` docstrings claimed non-func
  imports are "dropped"; they are in fact parsed into `globals`/`tables`/`memory`
  and recorded in `importedGlobals`/`importedTables`/`importedMemories`. Reword to
  match. Also remove the now-unreachable `br_on_cast` arm in the `parsePlainOp`
  fallback (handled by an explicit arm) and its orphaned `consumeBrOnCastImmediates`.

- Array trunk: add chunk-generic `unSliceBodyTerminates`; `isEmptyBodyTerminates`
  and the new symmetric `lenBodyTerminates` are one-line instances, so the `len`
  callee bridge no longer hand-rolls the `of_returns_wp` glue. Drop the now-unused
  op-specific `lenBodyWp`/`isEmptyBodyWp` (subsumed by the generic `unBodyReturnsWp`).

- RustArray/Spec.lean: bridges first, internal specs reuse them at `initialStore`
  (matching RustArrayTests) instead of duplicating the callee term.

- Add `open_slice_export` macro factoring the uniform export-proof head; apply to
  all six slice export proofs.

Verified: codelib and programs both `lake build` clean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Marcelo Fornet <mfornet94@gmail.com>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: 3 people

codelib/CodeLib/RustStd/Array/Basic.lean

@@ -15,10 +15,11 @@ exact shape the integer trunk `CodeLib/RustStd/UInt.lean` already abstracts as
 `UnChunk` (over any `UIntWasm` type; here `UInt32`, whose `toV` is `.i32`).
 So a length-only op needs *no new chunk shape*: its chunk is a `UnChunk` instance
 (`Len.len_chunk`, `IsEmpty.isEmpty_chunk`) and its called monomorphized body is
-discharged by the trunk's `unBodyReturnsWp` (`Len.lenBodyWp`,
-`IsEmpty.isEmptyBodyWp`) — the same `unBodyReturnsWp` reads the length from an
-**arbitrary** local `i` (slices carry the length in the second fat-pointer field,
-e.g. param local `1`), so nothing slice-specific is needed there.
+discharged by the shared `unSliceBodyTerminates` below (instantiated per op as
+`Len.lenBodyTerminates`, `IsEmpty.isEmptyBodyTerminates`), which feeds the chunk
+through the integer trunk's `unBodyReturnsWp`. That reads the length from the
+slice's second fat-pointer field (param local `1`), so nothing beyond the chunk
+is needed per op.
 
 The one genuinely new unit here is `fatPtrLoadWp`: unlike a scalar, a slice
 crosses the C ABI **spilled to linear memory**, so the export wrapper must read
@@ -106,4 +107,56 @@ macro_rules
           List.reverseAux, List.map, List.length_cons, List.length_nil]
        rw [fatPtrLoadWp 0 $p $dataPtr $len [] (by simp) $hfat]))
 
+/-- Open a memory-resident slice *export* proof: apply the entry lemma, unfold the
+wrapper `def`s, and marshal the fat pointer back from memory with `load_fat_ptr` —
+the uniform three-line head every slice export shares before it `call`s its body.
+`fdef`/`fbody` are the wrapper's `Function`/`Program` defs; the remaining operands
+match `load_fat_ptr`. Leaves the goal just past the fat-pointer read, with the
+per-export tail (`wp_call_tw`, result rewriting) still explicit since it varies. -/
+syntax "open_slice_export " ident ", " ident " at "
+  term ", " term ", " term " using " term : tactic
+
+macro_rules
+  | `(tactic| open_slice_export $fdef, $fbody at $p, $dataPtr, $len using $hfat) =>
+    `(tactic|
+      (apply TerminatesWith.of_wp_entry_for (f := $fdef) rfl
+       unfold $fdef $fbody
+       load_fat_ptr $p, $dataPtr, $len using $hfat))
+
+/-! ## Generic length-only slice callee
+
+A length-only slice primitive compiles at opt-0 to a two-param leaf body
+`[.localGet 1] ++ frag ++ [.ret]`: the fat pointer is passed as `(dataPtr, len)`
+(local `0`, local `1`), the body reads the length from local `1`, and `frag` is a
+`UnChunk` transforming it. `len` (`frag = []`, `op = id`) and `is_empty`
+(`frag = [.const 0, .eq, .const 1, .and]`, `op = isEmptyValue`) are both this
+shape, so one chunk-generic `TerminatesWith` bridge serves them — and any future
+unary slice primitive — instead of a per-op copy of the `of_returns_wp` glue. -/
+
+/-- Callee bridge for a length-only slice body: any module function `id` whose
+body is `[.localGet 1] ++ frag ++ [.ret]` for a `UnChunk frag op` terminates,
+when called with stack `(len, dataPtr, …rest)`, returning `op len` on top of
+`rest`. Instantiate at a concrete chunk (`len_chunk`, `isEmpty_chunk`) to obtain
+that primitive's leaf-call fact; the `of_returns_wp`/`unBodyReturnsWp` glue lives
+here once. -/
+theorem unSliceBodyTerminates {α} {env : HostEnv α} {m : Module} {id : Nat}
+    {f : Function} {frag : Program} {op : UInt32 → UInt32} (chunk : UnChunk frag op)
+    (st : Store α) (dataPtr len : UInt32) (rest : List Value)
+    (hf : m.funcs[id - m.imports.length]? = some f)
+    (hbody : f.body = [.localGet 1] ++ frag ++ [.ret])
+    (hnp : f.numParams = 2)
+    (hres : f.results.length = 1)
+    (hImp : m.imports[id]? = none := by rfl) :
+    TerminatesWith env m id st (.i32 len :: .i32 dataPtr :: rest)
+      (fun st' vs => vs = .i32 (op len) :: rest ∧ framePost st st') := by
+  refine (TerminatesWith.of_returns_wp (f := f) (rs := [.i32 (op len)])
+      (P := framePost st) hf hres.symm ?_ hImp).mono ?_
+  · rw [hbody]
+    simp only [Function.toLocals, hnp]
+    exact unBodyReturnsWp chunk st 1 len [] rfl
+  · intro st' vs h
+    refine ⟨?_, h.2⟩
+    rw [h.1, hnp]
+    simp
+
 end Wasm.RustStd.Array

codelib/CodeLib/RustStd/Array/IsEmpty.lean

@@ -3,8 +3,8 @@ import CodeLib.RustStd.Array.Basic
 /-! `&[T]::is_empty` — a zero-length test masked to a Rust bool, computed from the
 slice length component. The reusable unit is the unary chunk (a `UnChunk` over
 `UInt32`) for the fragment `[.const 0, .eq, .const 1, .and]`; the called body
-(`isEmptyBodyWp`) derives from it through the integer trunk's `unBodyReturnsWp`,
-and an inlined occurrence reuses the chunk directly. -/
+(`isEmptyBodyTerminates`) derives from it through the trunk's
+`unSliceBodyTerminates`, and an inlined occurrence reuses the chunk directly. -/
 
 namespace Wasm.RustStd.Array
 
@@ -28,32 +28,21 @@ theorem isEmptyValue_and_one (len : UInt32) :
 /-- The reusable chunk: with the slice length on the stack, the fragment
 `[.const 0, .eq, .const 1, .and]` computes `isEmptyValue len`. The single
 stack-form unit for `is_empty` (a `UnChunk` over `UInt32`): it feeds the called
-body via the trunk's `unBodyReturnsWp`, and is `rw`-able directly at an inlined
-`is_empty` once the length is on the stack. -/
+body via the trunk's `unSliceBodyTerminates`, and is `rw`-able directly at an
+inlined `is_empty` once the length is on the stack. -/
 theorem isEmpty_chunk : UnChunk (T := UInt32) [.const 0, .eq, .const 1, .and] isEmptyValue := by
   intro α m env Q st P L rest len vs
   simp only [toV_u32, List.cons_append, List.nil_append, wp_const_cons, wp_eq_cons, wp_and_cons]
   unfold isEmptyValue
   by_cases h : len = 0 <;> simp [h]
 
-/-- Function-body theorem for the generated `&[T]::is_empty` primitive body
-`[localGet i, .const 0, .eq, .const 1, .and, .ret]`, reusing the integer trunk's
-`unBodyReturnsWp` with `isEmpty_chunk`. This is the *called* shape; an inlined
-`is_empty` reuses `isEmpty_chunk` directly (opt-0 only ever emits the call). -/
-theorem isEmptyBodyWp {α} {m : Module} {env : HostEnv α} (st : Store α)
-    {P L : List Value} (i : Nat) (len : UInt32) (vs : List Value)
-    (hlen : (⟨P, L, vs⟩ : Locals).get i = some (.i32 len)) :
-    wp m [.localGet i, .const 0, .eq, .const 1, .and, .ret]
-      (Returns (.i32 (isEmptyValue len) :: vs) (framePost st)) st ⟨P, L, vs⟩ env :=
-  unBodyReturnsWp isEmpty_chunk st i len vs hlen
-
 /-- Reusable *callee* fact for a generated leaf `is_empty` body. Any module
 function `id` whose body is the canonical `[localGet 1, const 0, eq, const 1, and,
 ret]` (the slice length sits in param local `1`, the second fat-pointer field)
 terminates, when called with stack `(len, dataPtr, …rest)`, returning
-`isEmptyValue len` on top of `rest`. Each corpus' leaf `is_empty` call bridge is
-this lemma at its concrete `func…Def`, so the `of_returns_wp`/`isEmptyBodyWp` glue
-lives here once instead of being restated per corpus. -/
+`isEmptyValue len` on top of `rest`. This is the trunk's `unSliceBodyTerminates`
+at `isEmpty_chunk`; each corpus' leaf `is_empty` call bridge is this lemma at its
+concrete `func…Def`. -/
 theorem isEmptyBodyTerminates {α} {env : HostEnv α} {m : Module} {id : Nat}
     {f : Function} (st : Store α) (dataPtr len : UInt32) (rest : List Value)
     (hf : m.funcs[id - m.imports.length]? = some f)
@@ -62,15 +51,7 @@ theorem isEmptyBodyTerminates {α} {env : HostEnv α} {m : Module} {id : Nat}
     (hres : f.results.length = 1)
     (hImp : m.imports[id]? = none := by rfl) :
     TerminatesWith env m id st (.i32 len :: .i32 dataPtr :: rest)
-      (fun st' vs => vs = .i32 (isEmptyValue len) :: rest ∧ framePost st st') := by
-  refine (TerminatesWith.of_returns_wp (f := f) (rs := [.i32 (isEmptyValue len)])
-      (P := framePost st) hf hres.symm ?_ hImp).mono ?_
-  · rw [hbody]
-    simp only [Function.toLocals, hnp]
-    exact isEmptyBodyWp st 1 len [] rfl
-  · intro st' vs h
-    refine ⟨?_, h.2⟩
-    rw [h.1, hnp]
-    simp
+      (fun st' vs => vs = .i32 (isEmptyValue len) :: rest ∧ framePost st st') :=
+  unSliceBodyTerminates isEmpty_chunk st dataPtr len rest hf hbody hnp hres hImp
 
 end Wasm.RustStd.Array

codelib/CodeLib/RustStd/Array/Len.lean

@@ -3,8 +3,8 @@ import CodeLib.RustStd.Array.Basic
 /-! `&[T]::len` — the slice length is the `i32` length component of the fat
 pointer; the monomorphized primitive body just returns it. The reusable unit is
 the degenerate unary chunk (`frag = []`, `op = id`) over the length, which feeds
-the called body through the integer trunk's `unBodyReturnsWp`. The *inlined*
-read is just `wp_localGet_cons`, so it needs no slice-specific lemma. -/
+the called body through the trunk's `unSliceBodyTerminates`. The *inlined* read
+is just `wp_localGet_cons`, so it needs no slice-specific lemma. -/
 
 namespace Wasm.RustStd.Array
 
@@ -13,20 +13,26 @@ open Wasm Wasm.RustStd
 /-- The reusable chunk: with the length on the stack, the empty fragment leaves
 it unchanged — `len` is the identity length-only op. The `frag = []`, `op = id`
 case of the trunk's `UnChunk` (at `UInt32`, whose `toV` is `.i32`); feeds
-`lenBodyWp` via `unBodyReturnsWp`. -/
+`lenBodyTerminates` via `unSliceBodyTerminates`. -/
 theorem len_chunk : UnChunk (T := UInt32) [] (id : UInt32 → UInt32) := by
   intro α m env Q st P L rest len vs
   simp
 
-/-- Function-body theorem for the generated `&[T]::len` primitive body
-`[localGet i, .ret]`, reusing the integer trunk's `unBodyReturnsWp` with
-`len_chunk`. Serves the *called* shape; the *inlined* shape is just
-`wp_localGet_cons`. -/
-theorem lenBodyWp {α} {m : Module} {env : HostEnv α} (st : Store α)
-    {P L : List Value} (i : Nat) (len : UInt32) (vs : List Value)
-    (hlen : (⟨P, L, vs⟩ : Locals).get i = some (.i32 len)) :
-    wp m [.localGet i, .ret]
-      (Returns (.i32 len :: vs) (framePost st)) st ⟨P, L, vs⟩ env :=
-  unBodyReturnsWp len_chunk st i len vs hlen
+/-- Reusable *callee* fact for a generated leaf `len` body. Any module function
+`id` whose body is the canonical `[localGet 1, ret]` (the slice length sits in
+param local `1`, the second fat-pointer field) terminates, when called with stack
+`(len, dataPtr, …rest)`, returning `len` on top of `rest`. This is the trunk's
+`unSliceBodyTerminates` at `len_chunk` (`op = id`); each corpus' leaf `len` call
+bridge is this lemma at its concrete `func…Def`. -/
+theorem lenBodyTerminates {α} {env : HostEnv α} {m : Module} {id : Nat}
+    {f : Function} (st : Store α) (dataPtr len : UInt32) (rest : List Value)
+    (hf : m.funcs[id - m.imports.length]? = some f)
+    (hbody : f.body = [.localGet 1, .ret])
+    (hnp : f.numParams = 2)
+    (hres : f.results.length = 1)
+    (hImp : m.imports[id]? = none := by rfl) :
+    TerminatesWith env m id st (.i32 len :: .i32 dataPtr :: rest)
+      (fun st' vs => vs = .i32 len :: rest ∧ framePost st st') :=
+  unSliceBodyTerminates len_chunk st dataPtr len rest hf hbody hnp hres hImp
 
 end Wasm.RustStd.Array

interpreter/Interpreter/Wasm/Decoder/Wat.lean

@@ -9,10 +9,12 @@ A small parser for the WebAssembly text format, targeting Wasm's AST.
 Supported:
 * `(module ...)` with any number of `(func ...)` definitions.
 * `(type ...)`, `(export ...)`, `(import ...)`, `(table ...)`, `(memory ...)`,
-  `(global ...)`, `(elem ...)`, `(data ...)`, `(start ...)` — recognized at the
-  module level. Only `func` and `export` contribute to the resulting
-  `Wasm.Module`; the rest are accepted to allow round-tripping the spec
-  testsuite, but their content is discarded.
+  `(global ...)`, `(elem ...)`, `(data ...)`, `(tag ...)`, `(start ...)` —
+  recognized at the module level and fully parsed into the resulting
+  `Wasm.Module`. Non-func imports (`(import … (memory|global|table …))`)
+  are parsed too: each becomes a placeholder decl at the low end of its
+  index space and is recorded in `importedGlobals`/`importedTables`/
+  `importedMemories` for later host substitution.
 * Func headers may include `(type N)`, `(param ...)*`, `(result ...)*`,
   `(local ...)*` in any order, with grouped or singleton declarations.
 * Linear instruction stream and folded operand expressions
@@ -26,8 +28,10 @@ Supported:
 * Numeric indices and symbolic identifiers (`$L`).
 * `(;0;)` block comments and `;;` line comments are stripped during tokenization.
 
-Features Wasm does not model (memory loads/stores, `memory.*`, globals,
-`call_indirect`, tables) are accepted lexically but lowered to
+Memory loads/stores, `memory.*`, globals, `call_indirect`, tables,
+floats, and SIMD are all modelled and decode to real instructions.
+Instructions from proposals the interpreter still doesn't model (e.g.
+atomics/threads) are accepted lexically but lowered to
 `Wasm.Instruction.unreachable` so the surrounding function still
 type-checks. `local.tee i` is desugared to `[local.set i; local.get i]`. -/
 
@@ -672,13 +676,14 @@ private def parsePlainOp : String → Except Err Wasm.Instruction
   | "i31.get_u"    => .ok (.gc .i31GetU)
   | "ref.eq"       => .ok (.gc .refEq)
   | op          =>
-    -- Accept instructions from proposals the interpreter doesn't model
-    -- (floats, SIMD, reference types, tables, GC, exceptions, tail calls)
-    -- by lowering them to `unreachable`. This lets modules whose
-    -- *signatures* or unrelated functions touch these features still
-    -- decode; any function that actually executes such an instruction
-    -- traps with "unreachable" instead of failing to decode at all,
-    -- which would cascade to every assert in the file.
+    -- Fallback for mnemonics not matched above (and not caught by
+    -- `simdOp?`): still-unmodelled proposals such as atomics/threads and
+    -- relaxed SIMD, plus stray leftovers from partly-modelled proposals
+    -- (reference types, tables, GC, exceptions, tail calls). Lower them to
+    -- `unreachable` so modules whose *signatures* or unrelated functions
+    -- touch these features still decode; a function that actually executes
+    -- such an instruction traps with "unreachable" instead of failing to
+    -- decode at all, which would cascade to every assert in the file.
     if op.startsWith "f32." || op.startsWith "f64." || op.startsWith "v128."
        || op.startsWith "i8x16." || op.startsWith "i16x8." || op.startsWith "i32x4."
        || op.startsWith "i64x2." || op.startsWith "f32x4." || op.startsWith "f64x2."
@@ -695,9 +700,9 @@ private def parsePlainOp : String → Except Err Wasm.Instruction
     else
       .error s!"unsupported instruction: {op}"
 
-/-- Memory ops that take an offset immediate. We accept them lexically
-(`offset=`/`align=` attributes parsed and discarded) but emit
-`unreachable` for the instruction itself. -/
+/-- Memory ops that take an offset immediate, mapped to their natural
+alignment (byte width). `offset=`/`align=` attributes are parsed off the
+token stream; `memOpToInstruction` then emits the real load/store. -/
 private def isMemOp (op : String) : Option Nat :=
   match op with
   | "i32.load"     => some 4
@@ -714,10 +719,8 @@ private def isMemOp (op : String) : Option Nat :=
   | "i64.store8"   => some 1
   | "i64.store16"  => some 2
   | "i64.store32"  => some 4
-  -- Float and SIMD memory ops are lexically accepted (their offset=/
-  -- align= attributes parsed and discarded), but `memOpToInstruction`
-  -- lowers them to `unreachable` since the interpreter doesn't model
-  -- those value types.
+  -- Float and SIMD memory ops (their offset=/align= attributes parsed the
+  -- same way); `memOpToInstruction` emits the matching real load/store.
   | "f32.load" | "f32.store" => some 4
   | "f64.load" | "f64.store" => some 8
   | "v128.load" | "v128.store" => some 16
@@ -766,24 +769,6 @@ private def consumeMemAttrs (natAlign : Nat) (toks : List Sexpr)
     | xs => .ok (offset, xs)
   loop 0 toks
 
-/-- Number of atom immediates a *lowered* (treated-as-`unreachable`) op
-consumes. Used to keep the linear/folded parsers in sync with the token
-stream when we accept-and-stub instructions from proposals the
-interpreter doesn't model. Returns `none` for ops we don't pretend to
-support. -/
-private def stubImmediateCount (_op : String) : Option Nat :=
-  -- `br_on_cast`/`br_on_cast_fail` take label + from_type + to_type and are
-  -- handled separately by `consumeBrOnCastImmediates`; all other GC ops are
-  -- now decoded to real instructions.
-  none
-
-/-- Drop the first `n` atom tokens from `toks`. Errors if a non-atom is
-encountered or the stream is too short. -/
-private partial def consumeStubAtoms (op : String) : Nat → List Sexpr → Except Err (List Sexpr)
-  | 0, ts => .ok ts
-  | k+1, .atom _ :: ts => consumeStubAtoms op k ts
-  | _+1, _ => .error s!"{op}: expected immediate atom"
-
 /-! ## SIMD mnemonic table
 
 Shape-prefixed mnemonics (`i8x16.add`, `f64x2.pmin`, …) decode through
@@ -1022,17 +1007,6 @@ private def looksLikeLabel (s : String) : Bool :=
   else
     s.toList.all (fun c => c.isDigit || c = '_')
 
-/-- Consume the label immediate and the two type-immediates of a
-`br_on_cast` / `br_on_cast_fail`. The label is a single atom; each type
-is either an atom (e.g. `anyref`) or a `(ref …)` list. -/
-private def consumeBrOnCastImmediates (op : String)
-    : List Sexpr → Except Err (List Sexpr)
-  | .atom _ :: t1 :: t2 :: rest =>
-    match t1, t2 with
-    | .atom _, .atom _ | .atom _, .list _
-    | .list _, .atom _ | .list _, .list _ => .ok rest
-  | _ => .error s!"{op}: expected label + 2 type immediates"
-
 /-- Parse the *optional* table-index immediate carried by `table.get` /
 `table.size` in flat (post-`wasm-tools print`) form. The index is `$name`
 or a numeric literal when present and defaults to table `0` when omitted;
@@ -1374,15 +1348,12 @@ private partial def parseInstr (ctx : Ctx) (toks : List Sexpr)
         | none =>
         match parsePlainOp op with
         | .error e => .error e
-        | .ok i => do
-          -- For ops we lowered to `unreachable`, consume any textual
-          -- immediates so the token stream stays aligned.
-          let rest' ← if op == "br_on_cast" || op == "br_on_cast_fail" then
-            consumeBrOnCastImmediates op rest
-          else match stubImmediateCount op with
-            | some n => consumeStubAtoms op n rest
-            | none   => .ok rest
-          .ok ([i], rest')
+        -- Ops reaching this fallback are lowered to `unreachable` and carry
+        -- no immediates we track, so the token stream stays aligned with
+        -- `rest` untouched. (Ops that *do* carry immediates — including
+        -- `br_on_cast`/`br_on_cast_fail` — are handled by explicit arms above
+        -- and never fall through here.)
+        | .ok i => .ok ([i], rest)
 
 private partial def parseFolded (ctx : Ctx) (xs : List Sexpr)
     : Except Err (List Wasm.Instruction) :=
@@ -2849,14 +2820,16 @@ private def collectImports (types : Array TypeEntry) (fields : List Sexpr)
     | _ => pure ()
   return (imports, idOf)
 
-/-- Walk a `(module ...)` form. `(func …)`, `(export …)`, `(global …)`,
-`(memory …)`, `(data …)`, `(start …)`, and `(import "mod" "name"
-(func …))` all contribute to the resulting `Wasm.Module`. Function
-imports occupy the low end of the unified function index space (indices
-`0 … N-1`); in-module function indices are shifted up by
-`imports.length`. Other recognised fields (`type`, `table`, `elem`, non-
-func imports) are accepted lexically so the spec testsuite still loads,
-but their content is discarded. -/
+/-- Walk a `(module ...)` form. `(type …)`, `(func …)`, `(export …)`,
+`(global …)`, `(table …)`, `(memory …)`, `(elem …)`, `(data …)`,
+`(tag …)`, `(start …)`, and `(import "mod" "name" (…))` — for func and
+non-func imports alike — all contribute to the resulting `Wasm.Module`.
+Function imports occupy the low end of the unified function index space
+(indices `0 … N-1`); in-module function indices are shifted up by
+`imports.length`. Non-func imports (`(import … (memory|global|table …))`)
+are collected by `collectEntityImports` into placeholder decls at the low
+end of the global/table/memory index spaces and recorded in
+`importedGlobals`/`importedTables`/`importedMemories`. -/
 def parseModule (xs : List Sexpr) : Except Err Wasm.Module := do
   let mut rest := xs
   match rest with