[spec] Fix state for expression evaluation

Author: rossberg

specification/wasm-3.0/4.4-execution.modules.spectec

@@ -161,8 +161,7 @@ def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalgloba
 def $evalglobals(z, eps, eps) = (z, eps)
 def $evalglobals(z, gt gt'*, expr expr'*) = (z', val val'*)
   ----
-  -- Eval_expr: z; expr ~>* z; val
-  -- if z = s; f
+  -- Eval_expr: z; expr ~>* s; f; val
   -- if (s', a) = $allocglobal(s, gt, val)
   -- if (z', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)
 

specification/wasm-latest/4.4-execution.modules.spectec

@@ -161,8 +161,7 @@ def $evalglobals(state, globaltype*, expr*) : (state, val*) hint(show $evalgloba
 def $evalglobals(z, eps, eps) = (z, eps)
 def $evalglobals(z, gt gt'*, expr expr'*) = (z', val val'*)
   ----
-  -- Eval_expr: z; expr ~>* z; val
-  -- if z = s; f
+  -- Eval_expr: z; expr ~>* s; f; val
   -- if (s', a) = $allocglobal(s, gt, val)
   -- if (z', val'*) = $evalglobals((s'; f[.MODULE.GLOBALS =++ a]), gt'*, expr'*)