Merge pull request #99 from Wasm-DSL/bug.mm

Rename mm to moduleinst

spectec/spec/wasm-1.0/9-module.watsup

@@ -34,15 +34,15 @@ def $mems(externval externval'*) = $mems(externval'*)
 ;; Definitions
 
 def $allocfunc(store, moduleinst, func) : (store, funcaddr)
-def $allocfunc(s, mm, func) = (s[.FUNCS =.. fi], |s.FUNCS|)
-  -- if fi = { TYPE mm.TYPES[x], MODULE mm, CODE func }
+def $allocfunc(s, moduleinst, func) = (s[.FUNCS =.. fi], |s.FUNCS|)
+  -- if fi = { TYPE moduleinst.TYPES[x], MODULE moduleinst, CODE func }
   -- if func = FUNC x local* expr
 
 def $allocfuncs(store, moduleinst, func*) : (store, funcaddr*)
-def $allocfuncs(s, mm, eps) = (s, eps)
-def $allocfuncs(s, mm, func func'*) = (s_2, fa fa'*)
-  -- if (s_1, fa) = $allocfunc(s, mm, func)
-  -- if (s_2, fa'*) = $allocfuncs(s_1, mm, func'*)
+def $allocfuncs(s, moduleinst, eps) = (s, eps)
+def $allocfuncs(s, moduleinst, func func'*) = (s_2, fa fa'*)
+  -- if (s_1, fa) = $allocfunc(s, moduleinst, func)
+  -- if (s_2, fa'*) = $allocfuncs(s_1, moduleinst, func'*)
 
 def $allocglobal(store, globaltype, val) : (store, globaladdr)
 def $allocglobal(s, globaltype, val) = (s[.GLOBALS =.. gi], |s.GLOBALS|)
@@ -85,7 +85,7 @@ def $instexport(fa*, ga*, ta*, ma*, EXPORT name (MEM x)) = { NAME name, VALUE (M
 
 
 def $allocmodule(store, module, externval*, val*) : (store, moduleinst)
-def $allocmodule(s, module, externval*, val*) = (s_4, mm)
+def $allocmodule(s, module, externval*, val*) = (s_4, moduleinst)
   -- if module =
     MODULE
       (TYPE ft)*
@@ -107,15 +107,15 @@ def $allocmodule(s, module, externval*, val*) = (s_4, mm)
   -- if ta* = $(|s.TABLES|+i_table)^(i_table<n_table)
   -- if ma* = $(|s.MEMS|+i_mem)^(i_mem<n_mem)
   -- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
-  -- if mm = {
+  -- if moduleinst = {
       TYPES ft*,
       FUNCS fa_ex* fa*,
       GLOBALS ga_ex* ga*,
       TABLES ta_ex* ta*,
       MEMS ma_ex* ma*,
       EXPORTS xi*
     }
-  -- if (s_1, fa*) = $allocfuncs(s, mm, func^n_func)
+  -- if (s_1, fa*) = $allocfuncs(s, moduleinst, func^n_func)
   -- if (s_2, ga*) = $allocglobals(s_1, globaltype^n_global, val*)
   -- if (s_3, ta*) = $alloctables(s_2, tabletype^n_table)
   -- if (s_4, ma*) = $allocmems(s_3, memtype^n_mem)
@@ -126,16 +126,16 @@ def $allocmodule(s, module, externval*, val*) = (s_4, mm)
 ;;
 
 def $initelem(store, moduleinst, u32*, (funcaddr*)*) : store
-def $initelem(s, mm, eps, eps) = s
-def $initelem(s, mm, i i'*, (a*) (a'*)*) = s_2
-  -- if s_1 = s[.TABLES[mm.TABLES[0]].REFS[i:|a*|] = a*]
-  -- if s_2 = $initelem(s_1, mm, i'*, (a'*)*)
+def $initelem(s, moduleinst, eps, eps) = s
+def $initelem(s, moduleinst, i i'*, (a*) (a'*)*) = s_2
+  -- if s_1 = s[.TABLES[moduleinst.TABLES[0]].REFS[i:|a*|] = a*]
+  -- if s_2 = $initelem(s_1, moduleinst, i'*, (a'*)*)
 
 def $initdata(store, moduleinst, u32*, (byte*)*) : store
-def $initdata(s, mm, eps, eps) = s
-def $initdata(s, mm, i i'*, (b*) (b'*)*) = s_2
-  -- if s_1 = s[.MEMS[mm.MEMS[0]].BYTES[i:|b*|] = b*]
-  -- if s_2 = $initdata(s_1, mm, i'*, (b'*)*)
+def $initdata(s, moduleinst, eps, eps) = s
+def $initdata(s, moduleinst, i i'*, (b*) (b'*)*) = s_2
+  -- if s_1 = s[.MEMS[moduleinst.MEMS[0]].BYTES[i:|b*|] = b*]
+  -- if s_2 = $initdata(s_1, moduleinst, i'*, (b'*)*)
 
 def $instantiate(store, module, externval*) : config
 def $instantiate(s, module, externval*) = s_3; f; (CALL x')?
@@ -146,20 +146,20 @@ def $instantiate(s, module, externval*) = s_3; f; (CALL x')?
   -- if data* = (DATA expr_D b*)*
   -- if start? = (START x')?
   -- if n_F = |func*|
-  -- if mm_init = {
+  -- if moduleinst_init = {
       TYPES functype*,
       FUNCS $funcs(externval*) $(|s.FUNCS|+i_F)^(i_F<n_F),
       GLOBALS $globals(externval*)
     }
-  -- if f_init = { MODULE mm_init }
+  -- if f_init = { MODULE moduleinst_init }
   -- if z = s; f_init
   -- (Eval_expr : z; expr_G ~>* z; val)*
   -- (Eval_expr : z; expr_E ~>* z; (CONST I32 i_E))*
   -- (Eval_expr : z; expr_D ~>* z; (CONST I32 i_D))*
-  -- if (s_1, mm) = $allocmodule(s, module, externval*, val*)
-  -- if s_2 = $initelem(s_1, mm, i_E*, mm.FUNCS[x]**)
-  -- if s_3 = $initdata(s_2, mm, i_D*, b**)
-  -- if f = { MODULE mm }
+  -- if (s_1, moduleinst) = $allocmodule(s, module, externval*, val*)
+  -- if s_2 = $initelem(s_1, moduleinst, i_E*, moduleinst.FUNCS[x]**)
+  -- if s_3 = $initdata(s_2, moduleinst, i_D*, b**)
+  -- if f = { MODULE moduleinst }
 
 
 ;;

spectec/spec/wasm-2.0/9-module.watsup

@@ -34,15 +34,15 @@ def $mems(externval externval'*) = $mems(externval'*)
 ;; Definitions
 
 def $allocfunc(store, moduleinst, func) : (store, funcaddr)
-def $allocfunc(s, mm, func) = (s[.FUNCS =.. fi], |s.FUNCS|)
-  -- if fi = { TYPE mm.TYPES[x], MODULE mm, CODE func }
+def $allocfunc(s, moduleinst, func) = (s[.FUNCS =.. fi], |s.FUNCS|)
+  -- if fi = { TYPE moduleinst.TYPES[x], MODULE moduleinst, CODE func }
   -- if func = FUNC x local* expr
 
 def $allocfuncs(store, moduleinst, func*) : (store, funcaddr*)
-def $allocfuncs(s, mm, eps) = (s, eps)
-def $allocfuncs(s, mm, func func'*) = (s_2, fa fa'*)
-  -- if (s_1, fa) = $allocfunc(s, mm, func)
-  -- if (s_2, fa'*) = $allocfuncs(s_1, mm, func'*)
+def $allocfuncs(s, moduleinst, eps) = (s, eps)
+def $allocfuncs(s, moduleinst, func func'*) = (s_2, fa fa'*)
+  -- if (s_1, fa) = $allocfunc(s, moduleinst, func)
+  -- if (s_2, fa'*) = $allocfuncs(s_1, moduleinst, func'*)
 
 def $allocglobal(store, globaltype, val) : (store, globaladdr)
 def $allocglobal(s, globaltype, val) = (s[.GLOBALS =.. gi], |s.GLOBALS|)
@@ -105,7 +105,7 @@ def $instexport(fa*, ga*, ta*, ma*, EXPORT name (MEM x)) = { NAME name, VALUE (M
 
 
 def $allocmodule(store, module, externval*, val*, (ref*)*) : (store, moduleinst)
-def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, mm)
+def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, moduleinst)
   -- if module =
     MODULE
       (TYPE ft)*
@@ -129,7 +129,7 @@ def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, mm)
   -- if ea* = $(|s.ELEMS|+i_elem)^(i_elem<n_elem)
   -- if da* = $(|s.DATAS|+i_data)^(i_data<n_data)
   -- if xi* = $instexport(fa_ex* fa*, ga_ex* ga*, ta_ex* ta*, ma_ex* ma*, export)*
-  -- if mm = {
+  -- if moduleinst = {
       TYPES ft*,
       FUNCS fa_ex* fa*,
       GLOBALS ga_ex* ga*,
@@ -139,7 +139,7 @@ def $allocmodule(s, module, externval*, val*, (ref*)*) = (s_6, mm)
       DATAS da*,
       EXPORTS xi*
     }
-  -- if (s_1, fa*) = $allocfuncs(s, mm, func^n_func)
+  -- if (s_1, fa*) = $allocfuncs(s, moduleinst, func^n_func)
   -- if (s_2, ga*) = $allocglobals(s_1, globaltype^n_global, val*)
   -- if (s_3, ta*) = $alloctables(s_2, tabletype^n_table)
   -- if (s_4, ma*) = $allocmems(s_3, memtype^n_mem)
@@ -174,17 +174,17 @@ def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)?
   -- if n_F = |func*|
   -- if n_E = |elem*|
   -- if n_D = |data*|
-  -- if mm_init = {
+  -- if moduleinst_init = {
        TYPES functype*,
        FUNCS $funcs(externval*) $(|s.FUNCS|+i_F)^(i_F<n_F),
        GLOBALS $globals(externval*)
      }
-  -- if f_init = { MODULE mm_init }
+  -- if f_init = { MODULE moduleinst_init }
   -- if z = s; f_init
   -- (Eval_expr : z; expr_G ~>* z; val)*
   -- (Eval_expr : z; expr_E ~>* z; ref)**
-  -- if (s', mm) = $allocmodule(s, module, externval*, val*, (ref*)*)
-  -- if f = { MODULE mm }
+  -- if (s', moduleinst) = $allocmodule(s, module, externval*, val*, (ref*)*)
+  -- if f = { MODULE moduleinst }
   -- if instr_E* = $concat_(instr, $runelem(elem*[i], i)^(i<n_E))
   -- if instr_D* = $concat_(instr, $rundata(data*[j], j)^(j<n_D))
 

spectec/spec/wasm-3.0/9-module.watsup

@@ -19,9 +19,9 @@ def $allocfunc(s, deftype, funccode, moduleinst) = (s ++ {FUNCS funcinst}, |s.FU
 
 def $allocfuncs(store, deftype*, funccode*, moduleinst*) : (store, funcaddr*) hint(show $allocfunc*#((%,%,%,%)))
 def $allocfuncs(s, eps, eps, eps) = (s, eps)
-def $allocfuncs(s, dt dt'*, funccode funccode'*, mm mm'*) = (s_2, fa fa'*)
-  -- if (s_1, fa) = $allocfunc(s, dt, funccode, mm)
-  -- if (s_2, fa'*) = $allocfuncs(s_1, dt'*, funccode'*, mm'*)
+def $allocfuncs(s, dt dt'*, funccode funccode'*, moduleinst moduleinst'*) = (s_2, fa fa'*)
+  -- if (s_1, fa) = $allocfunc(s, dt, funccode, moduleinst)
+  -- if (s_2, fa'*) = $allocfuncs(s_1, dt'*, funccode'*, moduleinst'*)
 
 def $allocglobal(store, globaltype, val) : (store, globaladdr)
 def $allocglobal(s, globaltype, val) = (s ++ {GLOBALS globalinst}, |s.GLOBALS|)
@@ -160,7 +160,7 @@ def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* instr_S?
   -- if elem* = (ELEM reftype expr_E* elemmode)*
   -- if data* = (DATA byte* datamode)*
   -- if start? = (START x)?
-  ;; TODO: avoid this HACK and use mm directly, or built it fully incrementally
+  ;; TODO: avoid this HACK and use moduleinst directly, or built it fully incrementally
   -- if moduleinst_0 = {
       TYPES $alloctypes(type*),
       FUNCS $funcsxv(externval*) ($(|s.FUNCS|+i_F))^(i_F<|func*|),
@@ -170,9 +170,8 @@ def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* instr_S?
   -- (Eval_expr : z; expr_G ~>* z; val_G)*
   -- (Eval_expr : z; expr_T ~>* z; ref_T)*
   -- (Eval_expr : z; expr_E ~>* z; ref_E)**
-  ;; TODO: rename mm to moduleinst (causes stack overflow in interpreter!)
-  -- if (s', mm) = $allocmodule(s, module, externval*, val_G*, ref_T*, (ref_E*)*)
-  -- if f = {MODULE mm}  ;; TODO: inline
+  -- if (s', moduleinst) = $allocmodule(s, module, externval*, val_G*, ref_T*, (ref_E*)*)
+  -- if f = {MODULE moduleinst}  ;; TODO: inline
   -- if instr_E* = $concat_(instr, $runelem_(i_E, elem*[i_E])^(i_E<|elem*|))
   -- if instr_D* = $concat_(instr, $rundata_(i_D, data*[i_D])^(i_D<|data*|))
   -- if instr_S? = (CALL x)?

spectec/src/il2al/manual.ml

@@ -1,3 +1,4 @@
+open Util.Source
 open Al
 open Ast
 open Al_util
@@ -128,7 +129,7 @@ let return_instrs_of_instantiate config =
       frameE (Some (numE Z.zero), frame),
       listE ([ caseE (atom_of_name "FRAME_" "admininstr", []) ]), rhs
     );
-    returnI (Some (tupE [ store; varE "mm" ]))
+    returnI (Some (tupE [ store; accE (frame, DotP (atom_of_name "MODULE" "") $ no_region) ]))
   ]
 let return_instrs_of_invoke config =
   let _, frame, rhs = config in

spectec/test-frontend/TEST.md

@@ -5535,10 +5535,10 @@ rec {
 def $allocfuncs(store : store, deftype*, funccode*, moduleinst*) : (store, funcaddr*)
   ;; 9-module.watsup:21.1-21.45
   def $allocfuncs{s : store}(s, [], [], []) = (s, [])
-  ;; 9-module.watsup:22.1-24.63
-  def $allocfuncs{s : store, dt : deftype, dt'* : deftype*, funccode : funccode, funccode'* : funccode*, mm : moduleinst, mm'* : moduleinst*, s_2 : store, fa : funcaddr, fa'* : funcaddr*, s_1 : store}(s, [dt] :: dt'*{dt' : deftype}, [funccode] :: funccode'*{funccode' : funccode}, [mm] :: mm'*{mm' : moduleinst}) = (s_2, [fa] :: fa'*{fa' : funcaddr})
-    -- if ((s_1, fa) = $allocfunc(s, dt, funccode, mm))
-    -- if ((s_2, fa'*{fa' : funcaddr}) = $allocfuncs(s_1, dt'*{dt' : deftype}, funccode'*{funccode' : funccode}, mm'*{mm' : moduleinst}))
+  ;; 9-module.watsup:22.1-24.71
+  def $allocfuncs{s : store, dt : deftype, dt'* : deftype*, funccode : funccode, funccode'* : funccode*, moduleinst : moduleinst, moduleinst'* : moduleinst*, s_2 : store, fa : funcaddr, fa'* : funcaddr*, s_1 : store}(s, [dt] :: dt'*{dt' : deftype}, [funccode] :: funccode'*{funccode' : funccode}, [moduleinst] :: moduleinst'*{moduleinst' : moduleinst}) = (s_2, [fa] :: fa'*{fa' : funcaddr})
+    -- if ((s_1, fa) = $allocfunc(s, dt, funccode, moduleinst))
+    -- if ((s_2, fa'*{fa' : funcaddr}) = $allocfuncs(s_1, dt'*{dt' : deftype}, funccode'*{funccode' : funccode}, moduleinst'*{moduleinst' : moduleinst}))
 }
 
 ;; 9-module.watsup
@@ -5702,7 +5702,7 @@ def $rundata_(dataidx : dataidx, data : data) : instr*
 ;; 9-module.watsup
 def $instantiate(store : store, module : module, externval*) : config
   ;; 9-module.watsup
-  def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, mm : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr})
+  def $instantiate{s : store, module : module, externval* : externval*, s' : store, f : frame, instr_E* : instr*, instr_D* : instr*, instr_S? : instr?, type* : type*, import* : import*, func* : func*, global* : global*, table* : table*, mem* : mem*, elem* : elem*, data* : data*, start? : start?, export* : export*, globaltype* : globaltype*, expr_G* : expr*, tabletype* : tabletype*, expr_T* : expr*, reftype* : reftype*, expr_E** : expr**, elemmode* : elemmode*, byte** : byte**, datamode* : datamode*, x? : idx?, moduleinst_0 : moduleinst, i_F^|func*{func : func}| : nat^|func*{func : func}|, z : state, val_G* : val*, ref_T* : ref*, ref_E** : ref**, moduleinst : moduleinst, i_E^|elem*{elem : elem}| : nat^|elem*{elem : elem}|, i_D^|data*{data : data}| : nat^|data*{data : data}|}(s, module, externval*{externval : externval}) = `%;%`_config(`%;%`_state(s', f), instr_E*{instr_E : instr} :: instr_D*{instr_D : instr} :: instr_S?{instr_S : instr})
     -- if (module = MODULE_module(type*{type : type}, import*{import : import}, func*{func : func}, global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}, start?{start : start}, export*{export : export}))
     -- if (global*{global : global} = GLOBAL_global(globaltype, expr_G)*{expr_G : expr, globaltype : globaltype})
     -- if (table*{table : table} = TABLE_table(tabletype, expr_T)*{expr_T : expr, tabletype : tabletype})
@@ -5714,8 +5714,8 @@ def $instantiate(store : store, module : module, externval*) : config
     -- (Eval_expr: `%;%~>*%;%`(z, expr_G, z, [val_G]))*{expr_G : expr, val_G : val}
     -- (Eval_expr: `%;%~>*%;%`(z, expr_T, z, [(ref_T : ref <: val)]))*{expr_T : expr, ref_T : ref}
     -- (Eval_expr: `%;%~>*%;%`(z, expr_E, z, [(ref_E : ref <: val)]))*{expr_E : expr, ref_E : ref}*{expr_E : expr, ref_E : ref}
-    -- if ((s', mm) = $allocmodule(s, module, externval*{externval : externval}, val_G*{val_G : val}, ref_T*{ref_T : ref}, ref_E*{ref_E : ref}*{ref_E : ref}))
-    -- if (f = {LOCALS [], MODULE mm})
+    -- if ((s', moduleinst) = $allocmodule(s, module, externval*{externval : externval}, val_G*{val_G : val}, ref_T*{ref_T : ref}, ref_E*{ref_E : ref}*{ref_E : ref}))
+    -- if (f = {LOCALS [], MODULE moduleinst})
     -- if (instr_E*{instr_E : instr} = $concat_(syntax instr, $runelem_(`%`_elemidx(i_E), elem*{elem : elem}[i_E])^(i_E<|elem*{elem : elem}|){i_E : nat}))
     -- if (instr_D*{instr_D : instr} = $concat_(syntax instr, $rundata_(`%`_dataidx(i_D), data*{data : data}[i_D])^(i_D<|data*{data : data}|){i_D : nat}))
     -- if (instr_S?{instr_S : instr} = CALL_instr(x)?{x : funcidx})

spectec/test-latex/TEST.md

@@ -7904,9 +7904,9 @@ $$
 $$
 \begin{array}{@{}lcl@{}l@{}}
 {{{\mathrm{allocfunc}}^\ast}}{(s,\, \epsilon,\, \epsilon,\, \epsilon)} &=& (s,\, \epsilon) \\
-{{{\mathrm{allocfunc}}^\ast}}{(s,\, {\mathit{dt}}~{{\mathit{dt}'}^\ast},\, {\mathit{code}}~{{{\mathit{code}}'}^\ast},\, {\mathit{mm}}~{{\mathit{mm}'}^\ast})} &=& (s_2,\, {\mathit{fa}}~{{\mathit{fa}'}^\ast})
-  &\qquad \mbox{if}~(s_1,\, {\mathit{fa}}) = {\mathrm{allocfunc}}(s, {\mathit{dt}}, {\mathit{code}}, {\mathit{mm}}) \\
-  &&&\qquad {\land}~(s_2,\, {{\mathit{fa}'}^\ast}) = {{{\mathrm{allocfunc}}^\ast}}{(s_1,\, {{\mathit{dt}'}^\ast},\, {{{\mathit{code}}'}^\ast},\, {{\mathit{mm}'}^\ast})} \\
+{{{\mathrm{allocfunc}}^\ast}}{(s,\, {\mathit{dt}}~{{\mathit{dt}'}^\ast},\, {\mathit{code}}~{{{\mathit{code}}'}^\ast},\, {\mathit{moduleinst}}~{{\mathit{moduleinst}'}^\ast})} &=& (s_2,\, {\mathit{fa}}~{{\mathit{fa}'}^\ast})
+  &\qquad \mbox{if}~(s_1,\, {\mathit{fa}}) = {\mathrm{allocfunc}}(s, {\mathit{dt}}, {\mathit{code}}, {\mathit{moduleinst}}) \\
+  &&&\qquad {\land}~(s_2,\, {{\mathit{fa}'}^\ast}) = {{{\mathrm{allocfunc}}^\ast}}{(s_1,\, {{\mathit{dt}'}^\ast},\, {{{\mathit{code}}'}^\ast},\, {{\mathit{moduleinst}'}^\ast})} \\
 \end{array}
 $$
 
@@ -8094,9 +8094,9 @@ $$
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~(z ; {\mathit{expr}}_{\mathsf{g}} \hookrightarrow^\ast z ; {\mathit{val}}_{\mathsf{g}})^\ast} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~(z ; {\mathit{expr}}_{\mathsf{t}} \hookrightarrow^\ast z ; {\mathit{ref}}_{\mathsf{t}})^\ast} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{(z ; {\mathit{expr}}_{\mathsf{e}} \hookrightarrow^\ast z ; {\mathit{ref}}_{\mathsf{e}})^\ast}^\ast} \\
-   \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~({s'},\, {\mathit{mm}}) = {\mathrm{allocmodule}}(s, {\mathit{module}}, {{\mathit{externval}}^\ast}, {{\mathit{val}}_{\mathsf{g}}^\ast}, {{\mathit{ref}}_{\mathsf{t}}^\ast}, {({{\mathit{ref}}_{\mathsf{e}}^\ast})^\ast})} \\
+   \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~({s'},\, {\mathit{moduleinst}}) = {\mathrm{allocmodule}}(s, {\mathit{module}}, {{\mathit{externval}}^\ast}, {{\mathit{val}}_{\mathsf{g}}^\ast}, {{\mathit{ref}}_{\mathsf{t}}^\ast}, {({{\mathit{ref}}_{\mathsf{e}}^\ast})^\ast})} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~f = \{ \begin{array}[t]{@{}l@{}}
-\mathsf{module}~{\mathit{mm}} \}\end{array}} \\
+\mathsf{module}~{\mathit{moduleinst}} \}\end{array}} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{instr}}_{\mathsf{e}}^\ast} = {\mathrm{concat}}({{{\mathrm{runelem}}}_{i_{\mathsf{e}}}({{\mathit{elem}}^\ast}{}[i_{\mathsf{e}}])^{i_{\mathsf{e}}<{|{{\mathit{elem}}^\ast}|}}})} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{instr}}_{\mathsf{d}}^\ast} = {\mathrm{concat}}({{{\mathrm{rundata}}}_{i_{\mathsf{d}}}({{\mathit{data}}^\ast}{}[i_{\mathsf{d}}])^{i_{\mathsf{d}}<{|{{\mathit{data}}^\ast}|}}})} \\
    \multicolumn{4}{@{}l@{}}{\qquad\quad {\land}~{{\mathit{instr}}_{\mathsf{s}}^?} = {(\mathsf{call}~x)^?}} \\