interpreter: accept folded GC allocator global initializers in the WAT decoder

The global-decl parser detected GC heap-allocating initializers
(struct.new / array.new*) by scanning only the top-level atoms of the
initializer sexpr, so the folded leaf form
(struct.new $s (i32.const 100)) slipped past the check, fell through to
the literal-folding shape match, and was rejected with 'global init
expression must be i32.const or i64.const'. The same allocation wrapped
in extended-const arithmetic was accepted, because the extended-const
scan does recurse into folded operands.

Generalize the recursive sexpr scan into initExprMentions and use it for
both the extended-const detection and a new initExprAllocates predicate,
so GC allocators are detected in both the flat form emitted by
wasm-tools print and the folded form.

Adds regression theorems in Examples/GlobalInitExpr exercising the exact
repro from the issue: the leaf and arithmetic-wrapped struct.new
initializers both decode and evaluate to a struct whose field reads back
as 100.

Fixes #109

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: mfornet

interpreter/Interpreter/Wasm/Decoder/Wat.lean

@@ -2189,18 +2189,33 @@ arithmetic ops (`i32.add`/`i32.sub`/`i32.mul`, i64 ditto). Recurses into
 folded operand forms (the flat form emitted by `wasm-tools print` is
 handled by the list case). -/
 mutual
-  /-- Scan a single sexpr; recurse into a `(…)` list via the list helper. -/
-  def initExprNeedsEval : Sexpr → Bool
-    | .atom a =>
-      a == "global.get"
-        || a ∈ #["i32.add", "i32.sub", "i32.mul", "i64.add", "i64.sub", "i64.mul"]
-    | .list ys => initExprNeedsEvalList ys
+  /-- Scan a single sexpr for an atom satisfying `p`; recurse into a `(…)`
+  list via the list helper (covers both the folded operand form and the flat
+  form emitted by `wasm-tools print`). -/
+  def initExprMentions (p : String → Bool) : Sexpr → Bool
+    | .atom a => p a
+    | .list ys => initExprMentionsList p ys
   /-- Scan a sequence of sexprs (the operands of a folded instruction). -/
-  def initExprNeedsEvalList : List Sexpr → Bool
+  def initExprMentionsList (p : String → Bool) : List Sexpr → Bool
     | [] => false
-    | y :: ys => initExprNeedsEval y || initExprNeedsEvalList ys
+    | y :: ys => initExprMentions p y || initExprMentionsList p ys
 end
 
+/-- Scan a single sexpr; recurse into a `(…)` list via the list helper. -/
+def initExprNeedsEval : Sexpr → Bool :=
+  initExprMentions fun a =>
+    a == "global.get"
+      || a ∈ #["i32.add", "i32.sub", "i32.mul", "i64.add", "i64.sub", "i64.mul"]
+
+/-- Whether a global-initializer sexpr mentions a GC heap-allocating constant
+instruction (`struct.new`/`array.new*`), in either the flat or the folded
+form. Such initializers cannot be folded to a literal at decode time. -/
+def initExprAllocates : Sexpr → Bool :=
+  initExprMentions fun a =>
+    a ∈ #["struct.new", "struct.new_default",
+          "array.new", "array.new_default", "array.new_fixed",
+          "array.new_data", "array.new_elem"]
+
 private def parseGlobalDecl (ctx : Ctx) (xs : List Sexpr) :
     Except Err Wasm.GlobalDecl := do
   let xs := match xs with
@@ -2228,12 +2243,7 @@ private def parseGlobalDecl (ctx : Ctx) (xs : List Sexpr) :
   -- GC heap-allocating initializers (`struct.new`/`array.new*`) cannot be
   -- folded to a single value at decode time; keep the const-expr program so
   -- `Module.runConstGlobals` can evaluate it at instantiation.
-  let needsExpr := xs.any fun
-    | .atom a => a == "struct.new" || a == "struct.new_default"
-        || a == "array.new" || a == "array.new_default" || a == "array.new_fixed"
-        || a == "array.new_data" || a == "array.new_elem"
-    | _ => false
-  if needsExpr then
+  if xs.any initExprAllocates then
     let prog ← parseInstrSeq ctx xs
     -- The value can't be folded at decode time; stash a placeholder `init`
     -- and let `Module.runConstGlobals` evaluate `initExpr` at instantiation.

interpreter/Interpreter/Wasm/Examples/GlobalInitExpr.lean

@@ -55,5 +55,59 @@ theorem getG_returns_42 :
       = [.i32 42] := by
   native_decide
 
+/-! ### GC allocator initializers (issue #109)
+
+    `struct.new` is a constant instruction, so a global may be initialised
+    with a plain `(struct.new $s (i32.const 100))`. The decoder used to
+    detect GC allocators only at the top level of the initializer sexpr, so
+    the folded leaf form was rejected while the same allocation wrapped in
+    extended-const arithmetic — caught by the (recursive) extended-const
+    scan — was accepted. Both forms must decode and evaluate to the same
+    module behaviour. -/
+
+/-- Leaf form: the initializer is a folded `struct.new` with a plain
+`i32.const` field value. -/
+def structGlobalLeafWat : String := "
+(module
+  (type $s (struct (field i32)))
+  (global $g (ref $s) (struct.new $s (i32.const 100)))
+  (func $f (export \"f\") (result i32)
+    (struct.get $s 0 (global.get $g))))
+"
+
+/-- Arithmetic form: the same allocation with the field value computed by an
+extended-const expression. -/
+def structGlobalArithWat : String := "
+(module
+  (type $s (struct (field i32)))
+  (global $g (ref $s) (struct.new $s (i32.add (i32.const 50) (i32.const 50))))
+  (func $f (export \"f\") (result i32)
+    (struct.get $s 0 (global.get $g))))
+"
+
+private def decodedLeaf : Wasm.Module := decodeOrDefault structGlobalLeafWat
+private def decodedArith : Wasm.Module := decodeOrDefault structGlobalArithWat
+
+/-- The leaf `struct.new` initializer decodes (rather than erroring) and is
+kept as a const-expr program for `runConstGlobals`. -/
+theorem leaf_struct_new_keeps_initExpr :
+    (decodedLeaf.globals[0]?.map (·.initExpr.isEmpty)).getD true = false := by
+  native_decide
+
+/-- End-to-end: reading the struct field of the leaf-initialised global
+returns `100`. -/
+theorem leaf_struct_new_returns_100 :
+    runValues 64 decodedLeaf 0
+      (decodedLeaf.runConstGlobals 64 (decodedLeaf.initialStore (α := Unit)) {}) []
+      = [.i32 100] := by
+  native_decide
+
+/-- The arithmetic-wrapped form evaluates to the same result. -/
+theorem arith_struct_new_returns_100 :
+    runValues 64 decodedArith 0
+      (decodedArith.runConstGlobals 64 (decodedArith.initialStore (α := Unit)) {}) []
+      = [.i32 100] := by
+  native_decide
+
 end GlobalInitExpr
 end Wasm