From ac3809160170fac8ca5a6c0b16b9730e0cdfb698 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 10 Feb 2026 10:12:15 +0100
Subject: [PATCH 01/10] [spec] Fix state for expression evaluation

---
 document/core/exec/modules.rst                |  8 ++++
 .../wasm-3.0/4.4-execution.modules.spectec    | 26 ++++++++-----
 .../wasm-latest/4.4-execution.modules.spectec | 26 ++++++++-----
 spectec/test-frontend/TEST.md                 | 38 +++++++++++++------
 4 files changed, 68 insertions(+), 30 deletions(-)

diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst
index 30cbc0a6e1..4303854465 100644
--- a/document/core/exec/modules.rst
+++ b/document/core/exec/modules.rst
@@ -182,6 +182,14 @@ $${definition: instantiate}
 
 where:
 
+.. _eval-exprs:
+
+$${definition-prose: evalexprs}
+
+$${definition: evalexprs}
+
+and:
+
 .. _eval-globals:
 
 $${definition-prose: evalglobals}
diff --git a/specification/wasm-3.0/4.4-execution.modules.spectec b/specification/wasm-3.0/4.4-execution.modules.spectec
index cd21223365..a28c4f4c93 100644
--- a/specification/wasm-3.0/4.4-execution.modules.spectec
+++ b/specification/wasm-3.0/4.4-execution.modules.spectec
@@ -157,17 +157,24 @@ def $runelem_(x, ELEM rt e^n (ACTIVE y instr*)) =
   instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT y x) (ELEM.DROP x)
 
 ;; TODO(2, rossberg): replace with something more uniform
+def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%)))
+def $evalexprs(z, eps) = (z, eps)
+def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
+  ----
+  -- Eval_expr: z; expr ~>* z'; ref
+  -- if (z'', ref'*) = $evalexprs(z', expr'*)
+
 def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%)))
 def $evalglobals(z, eps, eps) = (z, eps)
-def $evalglobals(z, gt gt'*, expr expr'*) = (z', val val'*)
+def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
   ----
-  -- Eval_expr: z; expr ~>* z; val
-  -- if z = s; f
+  -- Eval_expr: z; expr ~>* z'; val
+  -- if z' = s; f
   -- if (s', a) = $allocglobal(s, gt, val)
-  -- if (z', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
+  -- if (z'', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
 
 def $instantiate(store, module, externaddr*) : config
-def $instantiate(s, module, externaddr*) = s'; {MODULE moduleinst}; instr_E* instr_D* instr_S?
+def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E* instr_D* instr_S?
   ---- ----
   -- Module_ok: |- module : xt_I* -> xt_E*
   -- (Externaddr_ok: s |- externaddr : xt_I)*
@@ -184,11 +191,12 @@ def $instantiate(s, module, externaddr*) = s'; {MODULE moduleinst}; instr_E* ins
       GLOBALS $globalsxa(externaddr*),
       FUNCS $funcsxa(externaddr*) ($(|s.FUNCS|+i_F))^(i_F<|func*|) \
     }
-  -- if z = s; {MODULE moduleinst_0}  ;; TODO(2, rossberg): inline
+  -- if z = s; {MODULE moduleinst_0}
   -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*)
-  -- (Eval_expr : z'; expr_T ~>* z'; ref_T)*
-  -- (Eval_expr : z'; expr_E ~>* z'; ref_E)**
-  -- if (s', moduleinst) = $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*)
+  -- if (z'', ref_T*) = $evalexprs(z', expr_T*)
+  -- if (z''', ref_E*) = $evalexprs(z'', expr_E*)
+  -- if z''' = s'''; f
+  -- if (s'''', moduleinst) = $allocmodule(s''', module, externaddr*, val_G*, ref_T*, (ref_E*)*)
   -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|))
   -- if instr_E* = $concat_(instr, $runelem_(i_E, elem*[i_E])^(i_E<|elem*|))
   -- if instr_S? = (CALL x)?
diff --git a/specification/wasm-latest/4.4-execution.modules.spectec b/specification/wasm-latest/4.4-execution.modules.spectec
index cd21223365..a28c4f4c93 100644
--- a/specification/wasm-latest/4.4-execution.modules.spectec
+++ b/specification/wasm-latest/4.4-execution.modules.spectec
@@ -157,17 +157,24 @@ def $runelem_(x, ELEM rt e^n (ACTIVE y instr*)) =
   instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT y x) (ELEM.DROP x)
 
 ;; TODO(2, rossberg): replace with something more uniform
+def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%)))
+def $evalexprs(z, eps) = (z, eps)
+def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
+  ----
+  -- Eval_expr: z; expr ~>* z'; ref
+  -- if (z'', ref'*) = $evalexprs(z', expr'*)
+
 def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%)))
 def $evalglobals(z, eps, eps) = (z, eps)
-def $evalglobals(z, gt gt'*, expr expr'*) = (z', val val'*)
+def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
   ----
-  -- Eval_expr: z; expr ~>* z; val
-  -- if z = s; f
+  -- Eval_expr: z; expr ~>* z'; val
+  -- if z' = s; f
   -- if (s', a) = $allocglobal(s, gt, val)
-  -- if (z', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
+  -- if (z'', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
 
 def $instantiate(store, module, externaddr*) : config
-def $instantiate(s, module, externaddr*) = s'; {MODULE moduleinst}; instr_E* instr_D* instr_S?
+def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E* instr_D* instr_S?
   ---- ----
   -- Module_ok: |- module : xt_I* -> xt_E*
   -- (Externaddr_ok: s |- externaddr : xt_I)*
@@ -184,11 +191,12 @@ def $instantiate(s, module, externaddr*) = s'; {MODULE moduleinst}; instr_E* ins
       GLOBALS $globalsxa(externaddr*),
       FUNCS $funcsxa(externaddr*) ($(|s.FUNCS|+i_F))^(i_F<|func*|) \
     }
-  -- if z = s; {MODULE moduleinst_0}  ;; TODO(2, rossberg): inline
+  -- if z = s; {MODULE moduleinst_0}
   -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*)
-  -- (Eval_expr : z'; expr_T ~>* z'; ref_T)*
-  -- (Eval_expr : z'; expr_E ~>* z'; ref_E)**
-  -- if (s', moduleinst) = $allocmodule(s, module, externaddr*, val_G*, ref_T*, (ref_E*)*)
+  -- if (z'', ref_T*) = $evalexprs(z', expr_T*)
+  -- if (z''', ref_E*) = $evalexprs(z'', expr_E*)
+  -- if z''' = s'''; f
+  -- if (s'''', moduleinst) = $allocmodule(s''', module, externaddr*, val_G*, ref_T*, (ref_E*)*)
   -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|))
   -- if instr_E* = $concat_(instr, $runelem_(i_E, elem*[i_E])^(i_E<|elem*|))
   -- if instr_S? = (CALL x)?
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index ce89b29558..e03efd12f1 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -7285,36 +7285,50 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr*
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.94
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.75
+def $evalexprs(state : state, expr*) : (state, ref*)
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34
+  def $evalexprs{z : state}(z, []) = (z, [])
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-165.46
+  def $evalexprs{z : state, expr : expr, `expr'*` : expr*, z'' : state, ref : ref, `ref'*` : ref*, z' : state}(z, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [ref] ++ ref'*{ref' <- `ref'*`})
+    -- Eval_expr: `%;%~>*%;%`(z, expr, z', [(ref : ref <: val)])
+    -- if ((z'', ref'*{ref' <- `ref'*`}) = $evalexprs(z', expr'*{expr' <- `expr'*`}))
+}
+
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
+rec {
+
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.94
 def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
-  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.41
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.41
   def $evalglobals{z : state}(z, [], []) = (z, [])
-  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:162.1-167.81
-  def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z' : state, val : val, `val'*` : val*, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z', [val] ++ val'*{val' <- `val'*`})
-    -- Eval_expr: `%;%~>*%;%`(z, expr, z, [val])
-    -- if (z = `%;%`_state(s, f))
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-174.82
+  def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z'' : state, val : val, `val'*` : val*, z' : state, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [val] ++ val'*{val' <- `val'*`})
+    -- Eval_expr: `%;%~>*%;%`(z, expr, z', [val])
+    -- if (z' = `%;%`_state(s, f))
     -- if ((s', a) = $allocglobal(s, gt, val))
-    -- if ((z', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`}))
+    -- if ((z'', val'*{val' <- `val'*`}) = $evalglobals(`%;%`_state(s', f[MODULE_frame.GLOBALS_moduleinst =++ [a]]), gt'*{gt' <- `gt'*`}, expr'*{expr' <- `expr'*`}))
 }
 
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 def $instantiate(store : store, module : module, externaddr*) : config
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
-  def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `globaltype*` : globaltype*, `expr_G*` : expr*, `tabletype*` : tabletype*, `expr_T*` : expr*, `byte**` : byte**, `datamode*` : datamode*, `reftype*` : reftype*, `expr_E**` : expr**, `elemmode*` : elemmode*, `x?` : idx?, moduleinst_0 : moduleinst, `i_F*` : nat*, z : state, z' : state, `val_G*` : val*, `ref_T*` : ref*, `ref_E**` : ref**, `i_D*` : nat*, `i_E*` : nat*}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`}))
+  def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `globaltype*` : globaltype*, `expr_G*` : expr*, `tabletype*` : tabletype*, `expr_T*` : expr*, `byte**` : byte**, `datamode*` : datamode*, `reftype*` : reftype*, `expr_E*` : expr*, `elemmode*` : elemmode*, `x?` : idx?, moduleinst_0 : moduleinst, `i_F*` : nat*, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E*` : ref*, s''' : store, f : frame, `i_D*` : nat*, `i_E*` : nat*}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`}))
     -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`}))
     -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`}
     -- if (module = MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}))
     -- if (global*{global <- `global*`} = GLOBAL_global(globaltype, expr_G)*{expr_G <- `expr_G*`, globaltype <- `globaltype*`})
     -- if (table*{table <- `table*`} = TABLE_table(tabletype, expr_T)*{expr_T <- `expr_T*`, tabletype <- `tabletype*`})
     -- if (data*{data <- `data*`} = DATA_data(byte*{byte <- `byte*`}, datamode)*{`byte*` <- `byte**`, datamode <- `datamode*`})
-    -- if (elem*{elem <- `elem*`} = ELEM_elem(reftype, expr_E*{expr_E <- `expr_E*`}, elemmode)*{elemmode <- `elemmode*`, `expr_E*` <- `expr_E**`, reftype <- `reftype*`})
+    -- if (elem*{elem <- `elem*`} = ELEM_elem(reftype, expr_E*{expr_E <- `expr_E*`}, elemmode)*{elemmode <- `elemmode*`, reftype <- `reftype*`})
     -- if (start?{start <- `start?`} = START_start(x)?{x <- `x?`})
     -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){i_F <- `i_F*`}, DATAS [], ELEMS [], EXPORTS []})
     -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0}))
     -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`}))
-    -- (Eval_expr: `%;%~>*%;%`(z', expr_T, z', [(ref_T : ref <: val)]))*{expr_T <- `expr_T*`, ref_T <- `ref_T*`}
-    -- (Eval_expr: `%;%~>*%;%`(z', expr_E, z', [(ref_E : ref <: val)]))*{expr_E <- `expr_E*`, ref_E <- `ref_E*`}*{`expr_E*` <- `expr_E**`, `ref_E*` <- `ref_E**`}
-    -- if ((s', moduleinst) = $allocmodule(s, module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}))
+    -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`}))
+    -- if ((z''', ref_E*{ref_E <- `ref_E*`}) = $evalexprs(z'', expr_E*{expr_E <- `expr_E*`}))
+    -- if (z''' = `%;%`_state(s''', f))
+    -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{}))
     -- if (instr_D*{instr_D <- `instr_D*`} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data <- `data*`}[i_D])^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}))
     -- if (instr_E*{instr_E <- `instr_E*`} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem <- `elem*`}[i_E])^(i_E<|elem*{elem <- `elem*`}|){i_E <- `i_E*`}))
     -- if (instr_S?{instr_S <- `instr_S?`} = CALL_instr(x)?{x <- `x?`})

From d1de6b19c8fe5569733b0022a2e65a2ec17f473b Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 13 Feb 2026 08:01:24 +0100
Subject: [PATCH 02/10] Fix fix

---
 specification/wasm-3.0/4.4-execution.modules.spectec | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/specification/wasm-3.0/4.4-execution.modules.spectec b/specification/wasm-3.0/4.4-execution.modules.spectec
index a28c4f4c93..587e9528a1 100644
--- a/specification/wasm-3.0/4.4-execution.modules.spectec
+++ b/specification/wasm-3.0/4.4-execution.modules.spectec
@@ -164,6 +164,13 @@ def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
   -- Eval_expr: z; expr ~>* z'; ref
   -- if (z'', ref'*) = $evalexprs(z', expr'*)
 
+def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%)))
+def $evalexprss(z, eps) = (z, eps)
+def $evalexprss(z, expr* expr'**) = (z'', ref* ref'**)
+  ----
+  -- if (z', ref*) = $evalexprs(z, expr*)
+  -- if (z'', ref'**) = $evalexprss(z', expr'**)
+
 def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%)))
 def $evalglobals(z, eps, eps) = (z, eps)
 def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
@@ -194,7 +201,7 @@ def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E*
   -- if z = s; {MODULE moduleinst_0}
   -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*)
   -- if (z'', ref_T*) = $evalexprs(z', expr_T*)
-  -- if (z''', ref_E*) = $evalexprs(z'', expr_E*)
+  -- if (z''', ref_E**) = $evalexprss(z'', expr_E**)
   -- if z''' = s'''; f
   -- if (s'''', moduleinst) = $allocmodule(s''', module, externaddr*, val_G*, ref_T*, (ref_E*)*)
   -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|))

From cb2670249eb0a5335cf9d380287ab51a0a53915d Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 13 Feb 2026 08:45:14 +0100
Subject: [PATCH 03/10] Carry over previous commit to wasm-latest

---
 .../wasm-latest/4.4-execution.modules.spectec |  9 ++++++-
 spectec/test-frontend/TEST.md                 | 27 ++++++++++++++-----
 2 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/specification/wasm-latest/4.4-execution.modules.spectec b/specification/wasm-latest/4.4-execution.modules.spectec
index a28c4f4c93..587e9528a1 100644
--- a/specification/wasm-latest/4.4-execution.modules.spectec
+++ b/specification/wasm-latest/4.4-execution.modules.spectec
@@ -164,6 +164,13 @@ def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
   -- Eval_expr: z; expr ~>* z'; ref
   -- if (z'', ref'*) = $evalexprs(z', expr'*)
 
+def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%)))
+def $evalexprss(z, eps) = (z, eps)
+def $evalexprss(z, expr* expr'**) = (z'', ref* ref'**)
+  ----
+  -- if (z', ref*) = $evalexprs(z, expr*)
+  -- if (z'', ref'**) = $evalexprss(z', expr'**)
+
 def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%)))
 def $evalglobals(z, eps, eps) = (z, eps)
 def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
@@ -194,7 +201,7 @@ def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E*
   -- if z = s; {MODULE moduleinst_0}
   -- if (z', val_G*) = $evalglobals(z, globaltype*, expr_G*)
   -- if (z'', ref_T*) = $evalexprs(z', expr_T*)
-  -- if (z''', ref_E*) = $evalexprs(z'', expr_E*)
+  -- if (z''', ref_E**) = $evalexprss(z'', expr_E**)
   -- if z''' = s'''; f
   -- if (s'''', moduleinst) = $allocmodule(s''', module, externaddr*, val_G*, ref_T*, (ref_E*)*)
   -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|))
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index e03efd12f1..55ef118794 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -7298,11 +7298,24 @@ def $evalexprs(state : state, expr*) : (state, ref*)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.94
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.79
+def $evalexprss(state : state, expr**) : (state, ref**)
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35
+  def $evalexprss{z : state}(z, []) = (z, [])
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-172.49
+  def $evalexprss{z : state, `expr*` : expr*, `expr'**` : expr**, z'' : state, `ref*` : ref*, `ref'**` : ref**, z' : state}(z, [expr*{expr <- `expr*`}] ++ expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`}) = (z'', [ref*{ref <- `ref*`}] ++ ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`})
+    -- if ((z', ref*{ref <- `ref*`}) = $evalexprs(z, expr*{expr <- `expr*`}))
+    -- if ((z'', ref'*{ref' <- `ref'*`}*{`ref'*` <- `ref'**`}) = $evalexprss(z', expr'*{expr' <- `expr'*`}*{`expr'*` <- `expr'**`}))
+}
+
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
+rec {
+
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.94
 def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
-  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.41
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41
   def $evalglobals{z : state}(z, [], []) = (z, [])
-  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:169.1-174.82
+  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:176.1-181.82
   def $evalglobals{z : state, gt : globaltype, `gt'*` : globaltype*, expr : expr, `expr'*` : expr*, z'' : state, val : val, `val'*` : val*, z' : state, s : store, f : frame, s' : store, a : addr}(z, [gt] ++ gt'*{gt' <- `gt'*`}, [expr] ++ expr'*{expr' <- `expr'*`}) = (z'', [val] ++ val'*{val' <- `val'*`})
     -- Eval_expr: `%;%~>*%;%`(z, expr, z', [val])
     -- if (z' = `%;%`_state(s, f))
@@ -7313,22 +7326,22 @@ def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 def $instantiate(store : store, module : module, externaddr*) : config
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
-  def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `globaltype*` : globaltype*, `expr_G*` : expr*, `tabletype*` : tabletype*, `expr_T*` : expr*, `byte**` : byte**, `datamode*` : datamode*, `reftype*` : reftype*, `expr_E*` : expr*, `elemmode*` : elemmode*, `x?` : idx?, moduleinst_0 : moduleinst, `i_F*` : nat*, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E*` : ref*, s''' : store, f : frame, `i_D*` : nat*, `i_E*` : nat*}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`}))
+  def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `globaltype*` : globaltype*, `expr_G*` : expr*, `tabletype*` : tabletype*, `expr_T*` : expr*, `byte**` : byte**, `datamode*` : datamode*, `reftype*` : reftype*, `expr_E**` : expr**, `elemmode*` : elemmode*, `x?` : idx?, moduleinst_0 : moduleinst, `i_F*` : nat*, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E**` : ref**, s''' : store, f : frame, `i_D*` : nat*, `i_E*` : nat*}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`}))
     -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`}))
     -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`}
     -- if (module = MODULE_module(type*{type <- `type*`}, import*{import <- `import*`}, tag*{tag <- `tag*`}, global*{global <- `global*`}, mem*{mem <- `mem*`}, table*{table <- `table*`}, func*{func <- `func*`}, data*{data <- `data*`}, elem*{elem <- `elem*`}, start?{start <- `start?`}, export*{export <- `export*`}))
     -- if (global*{global <- `global*`} = GLOBAL_global(globaltype, expr_G)*{expr_G <- `expr_G*`, globaltype <- `globaltype*`})
     -- if (table*{table <- `table*`} = TABLE_table(tabletype, expr_T)*{expr_T <- `expr_T*`, tabletype <- `tabletype*`})
     -- if (data*{data <- `data*`} = DATA_data(byte*{byte <- `byte*`}, datamode)*{`byte*` <- `byte**`, datamode <- `datamode*`})
-    -- if (elem*{elem <- `elem*`} = ELEM_elem(reftype, expr_E*{expr_E <- `expr_E*`}, elemmode)*{elemmode <- `elemmode*`, reftype <- `reftype*`})
+    -- if (elem*{elem <- `elem*`} = ELEM_elem(reftype, expr_E*{expr_E <- `expr_E*`}, elemmode)*{elemmode <- `elemmode*`, `expr_E*` <- `expr_E**`, reftype <- `reftype*`})
     -- if (start?{start <- `start?`} = START_start(x)?{x <- `x?`})
     -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){i_F <- `i_F*`}, DATAS [], ELEMS [], EXPORTS []})
     -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0}))
     -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`}))
     -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`}))
-    -- if ((z''', ref_E*{ref_E <- `ref_E*`}) = $evalexprs(z'', expr_E*{expr_E <- `expr_E*`}))
+    -- if ((z''', ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}) = $evalexprss(z'', expr_E*{expr_E <- `expr_E*`}*{`expr_E*` <- `expr_E**`}))
     -- if (z''' = `%;%`_state(s''', f))
-    -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{}))
+    -- if ((s'''', moduleinst) = $allocmodule(s''', module, externaddr*{externaddr <- `externaddr*`}, val_G*{val_G <- `val_G*`}, ref_T*{ref_T <- `ref_T*`}, ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}))
     -- if (instr_D*{instr_D <- `instr_D*`} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data <- `data*`}[i_D])^(i_D<|data*{data <- `data*`}|){i_D <- `i_D*`}))
     -- if (instr_E*{instr_E <- `instr_E*`} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem <- `elem*`}[i_E])^(i_E<|elem*{elem <- `elem*`}|){i_E <- `i_E*`}))
     -- if (instr_S?{instr_S <- `instr_S?`} = CALL_instr(x)?{x <- `x?`})

From 6e4743101ac33c78d1d0a41557793e174d5c3a12 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Mon, 23 Feb 2026 10:49:18 +0900
Subject: [PATCH 04/10] HARDCODE: Consider last two args of Eval_expr as output

---
 spectec/src/il2al/animate.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml
index 8d70ddf832..ab9177a39f 100644
--- a/spectec/src/il2al/animate.ml
+++ b/spectec/src/il2al/animate.ml
@@ -243,7 +243,7 @@ let large_enough_subsets xs =
   let min = if n >= 2 then n-1 else n in
   List.filter ( fun ys -> min <= List.length ys ) yss
 
-let (@@) f g x = f x @ g x
+let (@@@) f g x = f x @ g x
 
 let is_not_lhs e = match e.it with
 | LenE _ | IterE (_, (ListN (_, Some _), _)) | DotE _ -> true
@@ -261,7 +261,7 @@ let is_call e = match e.it with
 
 let subset_selector e =
   if is_not_lhs e then (fun _ -> [])
-  else if is_call e then singletons @@ group_arg e
+  else if is_call e then singletons @@@ group_arg e
   else if is_atomic_lhs e then wrap
   else large_enough_subsets
 
@@ -292,13 +292,22 @@ let rec rows_of_prem vars len i p =
   | LetPr (_, _, targets) ->
     let covering_vars = List.filter_map (index_of len vars) targets in
     [ Assign targets, p, [i] @ covering_vars ]
+  | RulePr (id, _, { it = TupE args; _ }) when id.it = "Eval_expr" ->
+    (* HARDCODE: The output of the relation Eval_expr (%;%~>*%;%) is last two *)
+    let args', l = Util.Lib.List.split_last args in
+    let _, l' = Util.Lib.List.split_last args' in
+    let frees = (union (free_exp false l) (free_exp false l')).varid |> Set.elements in
+    [
+      Condition, p, [i];
+      Assign frees, p, [i] @ List.filter_map (index_of len vars) frees
+    ]
   | RulePr (_, _, { it = TupE args; _ }) ->
     (* Assumpton: the only possible assigned-value is the last arg (i.e. ... |- lhs ) *)
     let _, l = Util.Lib.List.split_last args in
-    let frees = (free_exp_list l) in
+    let frees = free_exp_list l in
     [
       Condition, p, [i];
-      Assign frees, p, [i] @ List.filter_map (index_of len vars) (free_exp_list l)
+      Assign frees, p, [i] @ List.filter_map (index_of len vars) frees
     ]
   | IterPr (p', iterexp) ->
     let p_r = rewrite_iterexp iterexp p' in

From 65b3a06cfab3f29d43449da045bad9e41484b206 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Mon, 23 Feb 2026 14:56:28 +0900
Subject: [PATCH 05/10] Identify all of the state name as z during
 interpretation

---
 spectec/src/il2al/transpile.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/spectec/src/il2al/transpile.ml b/spectec/src/il2al/transpile.ml
index d0c4d4a29b..88893398f7 100644
--- a/spectec/src/il2al/transpile.ml
+++ b/spectec/src/il2al/transpile.ml
@@ -946,6 +946,7 @@ let hide_state_expr expr =
       | CallE (f, args) -> CallE (f, hide_state_args args)
       | TupE [ s; e ] when is_store s -> e.it
       | TupE [ z; e ] when is_state z -> e.it
+      | VarE id when is_state expr && String.starts_with ~prefix:"z" id -> VarE "z"
       | e -> e
     in
     { expr with it = expr' }

From 997914ca4bcec8754b1f5b7ef47f412b987be8be Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Tue, 24 Feb 2026 09:52:24 +0900
Subject: [PATCH 06/10] Remove hardcode for animation of evalglobals and
 generalize

---
 spectec/src/il2al/animate.ml | 36 +++++++++++++++++++-----------------
 1 file changed, 19 insertions(+), 17 deletions(-)

diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml
index ab9177a39f..fd93d24a9d 100644
--- a/spectec/src/il2al/animate.ml
+++ b/spectec/src/il2al/animate.ml
@@ -292,23 +292,25 @@ let rec rows_of_prem vars len i p =
   | LetPr (_, _, targets) ->
     let covering_vars = List.filter_map (index_of len vars) targets in
     [ Assign targets, p, [i] @ covering_vars ]
-  | RulePr (id, _, { it = TupE args; _ }) when id.it = "Eval_expr" ->
-    (* HARDCODE: The output of the relation Eval_expr (%;%~>*%;%) is last two *)
-    let args', l = Util.Lib.List.split_last args in
-    let _, l' = Util.Lib.List.split_last args' in
-    let frees = (union (free_exp false l) (free_exp false l')).varid |> Set.elements in
-    [
-      Condition, p, [i];
-      Assign frees, p, [i] @ List.filter_map (index_of len vars) frees
-    ]
   | RulePr (_, _, { it = TupE args; _ }) ->
-    (* Assumpton: the only possible assigned-value is the last arg (i.e. ... |- lhs ) *)
-    let _, l = Util.Lib.List.split_last args in
-    let frees = free_exp_list l in
-    [
-      Condition, p, [i];
-      Assign frees, p, [i] @ List.filter_map (index_of len vars) frees
-    ]
+    (* Assumption:
+     * The only possible set of output variable
+     * is the last arg (i.e. ... |- lhs )
+     * or the last two args (i.e. ... ~>* z; v) *)
+    let assign_last n =
+      if List.length args <= n then [] else
+      let outs, ins = Lib.List.split n (List.rev args) in
+      let free_exps es = es |> List.map (free_exp false) |> List.fold_left union empty in
+      let free_set = free_exps outs in
+      let bound_set = free_exps ins in
+      if not (disjoint free_set bound_set) then [] else
+      let frees = free_set.varid |> Set.elements in
+      [ Assign frees, p, [i] @ List.filter_map (index_of len vars) frees ]
+    in
+
+    [ Condition, p, [i] ]
+      @ assign_last 1
+      @ assign_last 2
   | IterPr (p', iterexp) ->
     let p_r = rewrite_iterexp iterexp p' in
     let to_iter (tag, p, coverings) = tag, IterPr (recover_iterexp iterexp p, iterexp) $ p.at, coverings in
@@ -350,7 +352,7 @@ let animate_prems known_vars prems =
       Error.error (over_region (List.map at unhandled_prems)) "prose translation" "There might be a cyclic binding"
     else
       snd !best'
-  | Some x -> x
+  | Some prems -> prems
 
 (* Animate rule *)
 let animate_rule r = match r.it with

From 888045cfd686c40044e0938a91931c65e6074b5f Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 24 Feb 2026 09:23:57 +0100
Subject: [PATCH 07/10] Tweak macros

---
 .../wasm-3.0/4.4-execution.modules.spectec    |   7 ++++---
 spectec/doc/example/output/NanoWasm.pdf       | Bin 245512 -> 245512 bytes
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/specification/wasm-3.0/4.4-execution.modules.spectec b/specification/wasm-3.0/4.4-execution.modules.spectec
index 587e9528a1..58c112c0f2 100644
--- a/specification/wasm-3.0/4.4-execution.modules.spectec
+++ b/specification/wasm-3.0/4.4-execution.modules.spectec
@@ -157,21 +157,21 @@ def $runelem_(x, ELEM rt e^n (ACTIVE y instr*)) =
   instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT y x) (ELEM.DROP x)
 
 ;; TODO(2, rossberg): replace with something more uniform
-def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%)))
+def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%))) hint(macro none)
 def $evalexprs(z, eps) = (z, eps)
 def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
   ----
   -- Eval_expr: z; expr ~>* z'; ref
   -- if (z'', ref'*) = $evalexprs(z', expr'*)
 
-def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%)))
+def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%))) hint(macro none)
 def $evalexprss(z, eps) = (z, eps)
 def $evalexprss(z, expr* expr'**) = (z'', ref* ref'**)
   ----
   -- if (z', ref*) = $evalexprs(z, expr*)
   -- if (z'', ref'**) = $evalexprss(z', expr'**)
 
-def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%)))
+def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%))) hint(macro none)
 def $evalglobals(z, eps, eps) = (z, eps)
 def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
   ----
@@ -180,6 +180,7 @@ def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
   -- if (s', a) = $allocglobal(s, gt, val)
   -- if (z'', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
 
+
 def $instantiate(store, module, externaddr*) : config
 def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E* instr_D* instr_S?
   ---- ----
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 94f31ae26f2ebe7167f38c2af4ef1c31ace19afb..18166833ae045941b8dfe262f7ec4023444936f7 100644
GIT binary patch
delta 112
zcmeD9$Jg<Xuc3vpg=q`3$W~TMBV!|r>5^NS<si)MHd~ns*_<6+EexHE9nBq`T%F8}
iTn!yfEi7FOOw5c8ot+)c%-rl0YzQgY{$V$>1Tz2yIUXMX

delta 112
zcmeD9$Jg<Xuc3vpg=q`3$W~Sh6H6oW>5^NS<si)MHd~ns*__?XER0=^%$*DkEDQ{c
i%*>6Poy}ZbEG%4HOij#O98K*MYzQgY{$V$>1Tz5jc^%CF


From 3d72fae14f6a43a2dea0267c3550892a6ba14bf3 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 24 Feb 2026 09:31:02 +0100
Subject: [PATCH 08/10] Copy to latest

---
 specification/wasm-latest/4.4-execution.modules.spectec | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/specification/wasm-latest/4.4-execution.modules.spectec b/specification/wasm-latest/4.4-execution.modules.spectec
index 587e9528a1..91b2c9b3f7 100644
--- a/specification/wasm-latest/4.4-execution.modules.spectec
+++ b/specification/wasm-latest/4.4-execution.modules.spectec
@@ -157,21 +157,21 @@ def $runelem_(x, ELEM rt e^n (ACTIVE y instr*)) =
   instr* (CONST I32 0) (CONST I32 n) (TABLE.INIT y x) (ELEM.DROP x)
 
 ;; TODO(2, rossberg): replace with something more uniform
-def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%)))
+def $evalexprs(state, expr*) : (state, ref*) hint(show $evalexpr*#((%,%))) hint(macro none)
 def $evalexprs(z, eps) = (z, eps)
 def $evalexprs(z, expr expr'*) = (z'', ref ref'*)
   ----
   -- Eval_expr: z; expr ~>* z'; ref
   -- if (z'', ref'*) = $evalexprs(z', expr'*)
 
-def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%)))
+def $evalexprss(state, expr**) : (state, ref**) hint(show $evalexpr**#((%,%))) hint(macro none)
 def $evalexprss(z, eps) = (z, eps)
 def $evalexprss(z, expr* expr'**) = (z'', ref* ref'**)
   ----
   -- if (z', ref*) = $evalexprs(z, expr*)
   -- if (z'', ref'**) = $evalexprss(z', expr'**)
 
-def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%)))
+def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalglobal*#((%,%,%))) hint(macro none)
 def $evalglobals(z, eps, eps) = (z, eps)
 def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
   ----

From 95b2569e1672d322f7904c0d064266460b43533f Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 24 Feb 2026 09:50:03 +0100
Subject: [PATCH 09/10] Update test expect

---
 spectec/doc/example/output/NanoWasm.pdf | Bin 245512 -> 245512 bytes
 spectec/test-frontend/TEST.md           |   6 +++---
 spectec/test-middlend/TEST.md           |  18 +++++++++---------
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 18166833ae045941b8dfe262f7ec4023444936f7..a720e239bac6443a8a4e1faaf73e3ed9df060098 100644
GIT binary patch
delta 110
zcmeD9$Jg<Xuc3vpg=q`3=vEdJb0hQVl3SVO!L02zTbT>loGr|a9W4x<99@hIT?~zl
h&5TT(UEB;!EKN+z%?*v6%<U9x2r1eAVK=h`GXS*79RUCU

delta 110
zcmeD9$Jg<Xuc3vpg=q`3=vEdZV<U^{l3SVO!L02zTbT>loE=>)44sS}%^jUwoy?3}
h4IND_EL{vt%#014ogK~0-0T!=2r1eAVK=h`GXTyM9jyQW

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 4eca5c89d8..8466af4b89 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -7285,7 +7285,7 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr*
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.75
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92
 def $evalexprs(state : state, expr*) : (state, ref*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34
   def $evalexprs{z : state}(z, []) = (z, [])
@@ -7298,7 +7298,7 @@ def $evalexprs(state : state, expr*) : (state, ref*)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.79
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96
 def $evalexprss(state : state, expr**) : (state, ref**)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35
   def $evalexprss{z : state}(z, []) = (z, [])
@@ -7311,7 +7311,7 @@ def $evalexprss(state : state, expr**) : (state, ref**)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.94
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111
 def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41
   def $evalglobals{z : state}(z, [], []) = (z, [])
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 5de15e4faa..ce7873e553 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -7275,7 +7275,7 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr*
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.75
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92
 def $evalexprs(state : state, expr*) : (state, ref*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34
   def $evalexprs{z : state}(z, []) = (z, [])
@@ -7288,7 +7288,7 @@ def $evalexprs(state : state, expr*) : (state, ref*)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.79
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96
 def $evalexprss(state : state, expr**) : (state, ref**)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35
   def $evalexprss{z : state}(z, []) = (z, [])
@@ -7301,7 +7301,7 @@ def $evalexprss(state : state, expr**) : (state, ref**)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.94
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111
 def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41
   def $evalglobals{z : state}(z, [], []) = (z, [])
@@ -18667,7 +18667,7 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr*
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.75
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92
 def $evalexprs(state : state, expr*) : (state, ref*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34
   def $evalexprs{z : state}(z, []) = (z, [])
@@ -18680,7 +18680,7 @@ def $evalexprs(state : state, expr*) : (state, ref*)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.79
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96
 def $evalexprss(state : state, expr**) : (state, ref**)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35
   def $evalexprss{z : state}(z, []) = (z, [])
@@ -18693,7 +18693,7 @@ def $evalexprss(state : state, expr**) : (state, ref**)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.94
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111
 def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41
   def $evalglobals{z : state}(z, [], []) = (z, [])
@@ -30238,7 +30238,7 @@ def $runelem_(elemidx : elemidx, elem : elem) : instr*
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.75
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:160.1-160.92
 def $evalexprs(state : state, expr*) : (state, ref*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:161.1-161.34
   def $evalexprs{z : state}(z, []) = (z, [])
@@ -30251,7 +30251,7 @@ def $evalexprs(state : state, expr*) : (state, ref*)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.79
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:167.1-167.96
 def $evalexprss(state : state, expr**) : (state, ref**)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:168.1-168.35
   def $evalexprss{z : state}(z, []) = (z, [])
@@ -30264,7 +30264,7 @@ def $evalexprss(state : state, expr**) : (state, ref**)
 ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.94
+;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:174.1-174.111
 def $evalglobals(state : state, globaltype*, expr*) : (state, val*)
   ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec:175.1-175.41
   def $evalglobals{z : state}(z, [], []) = (z, [])

From 567626b2b944e95efdcc3ef0aa24802fbcdb216c Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 24 Feb 2026 09:52:53 +0100
Subject: [PATCH 10/10] Remove spurious diff

---
 specification/wasm-3.0/4.4-execution.modules.spectec | 1 -
 1 file changed, 1 deletion(-)

diff --git a/specification/wasm-3.0/4.4-execution.modules.spectec b/specification/wasm-3.0/4.4-execution.modules.spectec
index 58c112c0f2..91b2c9b3f7 100644
--- a/specification/wasm-3.0/4.4-execution.modules.spectec
+++ b/specification/wasm-3.0/4.4-execution.modules.spectec
@@ -180,7 +180,6 @@ def $evalglobals(z, gt gt'*, expr expr'*) = (z'', val val'*)
   -- if (s', a) = $allocglobal(s, gt, val)
   -- if (z'', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
 
-
 def $instantiate(store, module, externaddr*) : config
 def $instantiate(s, module, externaddr*) = s''''; {MODULE moduleinst}; instr_E* instr_D* instr_S?
   ---- ----