Refactor type uses

Wasm-DSL · Mar 27, 2024 · be5b1bf · be5b1bf
1 parent 7d9746e
commit be5b1bf
Show file tree

Hide file tree

Showing 16 changed files with 1,506 additions and 1,402 deletions.
diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup
@@ -139,8 +139,18 @@ syntax absheaptype/syn hint(desc "abstract heap type") =
   | ...
 syntax absheaptype/sem =
   | ... | BOT
-syntax heaptype/syn hint(desc "heap type") =
-  | absheaptype | _IDX typeidx | ...
+
+syntax rectype hint(desc "recursive type")  ;; forward decl
+syntax deftype hint(desc "defined type") =
+  | DEF rectype nat hint(show %.%)
+
+syntax typeuse/syn hint(desc "type use") =
+  | _IDX typeidx | ...
+syntax typeuse/sem =
+  | ... | deftype | REC n
+
+syntax heaptype hint(desc "heap type") =
+  | absheaptype | typeuse
 
 syntax reftype hint(desc "reference type") =
   | REF nul heaptype
@@ -189,19 +199,11 @@ syntax comptype hint(desc "composite type") =
   | FUNC functype
 
 syntax subtype/syn hint(desc "sub type") =
-  | SUB fin typeidx* comptype | ...
-syntax subtype/sem =
-  | ... | SUBD fin heaptype* comptype  hint(show SUB % % %)
+  | SUB fin typeuse* comptype
 
 syntax rectype hint(desc "recursive type") =
   | REC list(subtype)
 
-syntax deftype hint(desc "defined type") =
-  | DEF rectype nat hint(show %.%)
-
-syntax heaptype/sem =
-  | ... | deftype | REC n
-
 
 ;; External types
 
@@ -248,6 +250,8 @@ var xt : externtype
 var yt : fieldtype     ;; TODO: better choice?
 var zt : storagetype
 
+var tu : typeuse
+
 
 ;;
 ;; Operators
@@ -431,11 +435,11 @@ syntax instr/br hint(desc "branch instruction") = ...
 
 syntax instr/call hint(desc "function instruction") = ...
   | CALL funcidx
-  | CALL_REF typeidx?
+  | CALL_REF typeuse
   | CALL_INDIRECT tableidx typeidx
   | RETURN
   | RETURN_CALL funcidx
-  | RETURN_CALL_REF typeidx?
+  | RETURN_CALL_REF typeuse
   | RETURN_CALL_INDIRECT tableidx typeidx
   | ...
 

diff --git a/spectec/spec/wasm-3.0/2-syntax-aux.watsup b/spectec/spec/wasm-3.0/2-syntax-aux.watsup
@@ -136,90 +136,92 @@ def $idx(x) = _IDX x
 
 ;; Substitution
 
-def $subst_typevar(typevar, typevar*, heaptype*) : heaptype            hint(show %#`[%:=%])
+def $subst_typevar(typevar, typevar*, typeuse*) : typeuse             hint(show %#`[%:=%])
+def $subst_typeuse(typeuse, typevar*, typeuse*) : typeuse             hint(show %#`[%:=%])
 
-def $subst_numtype(numtype, typevar*, heaptype*) : numtype             hint(show %#`[%:=%])
-def $subst_vectype(vectype, typevar*, heaptype*) : vectype             hint(show %#`[%:=%])
-def $subst_heaptype(heaptype, typevar*, heaptype*) : heaptype          hint(show %#`[%:=%])
-def $subst_reftype(reftype, typevar*, heaptype*) : reftype             hint(show %#`[%:=%])
-def $subst_valtype(valtype, typevar*, heaptype*) : valtype             hint(show %#`[%:=%])
+def $subst_numtype(numtype, typevar*, typeuse*) : numtype             hint(show %#`[%:=%])
+def $subst_vectype(vectype, typevar*, typeuse*) : vectype             hint(show %#`[%:=%])
+def $subst_heaptype(heaptype, typevar*, typeuse*) : heaptype          hint(show %#`[%:=%])
+def $subst_reftype(reftype, typevar*, typeuse*) : reftype             hint(show %#`[%:=%])
+def $subst_valtype(valtype, typevar*, typeuse*) : valtype             hint(show %#`[%:=%])
 
-def $subst_packtype(packtype, typevar*, heaptype*) : packtype          hint(show %#`[%:=%])
-def $subst_storagetype(storagetype, typevar*, heaptype*) : storagetype hint(show %#`[%:=%])
-def $subst_fieldtype(fieldtype, typevar*, heaptype*) : fieldtype       hint(show %#`[%:=%])
+def $subst_packtype(packtype, typevar*, typeuse*) : packtype          hint(show %#`[%:=%])
+def $subst_storagetype(storagetype, typevar*, typeuse*) : storagetype hint(show %#`[%:=%])
+def $subst_fieldtype(fieldtype, typevar*, typeuse*) : fieldtype       hint(show %#`[%:=%])
 
-def $subst_comptype(comptype, typevar*, heaptype*) : comptype          hint(show %#`[%:=%])
-def $subst_subtype(subtype, typevar*, heaptype*) : subtype             hint(show %#`[%:=%])
-def $subst_rectype(rectype, typevar*, heaptype*) : rectype             hint(show %#`[%:=%])
-def $subst_deftype(deftype, typevar*, heaptype*) : deftype             hint(show %#`[%:=%])
+def $subst_comptype(comptype, typevar*, typeuse*) : comptype          hint(show %#`[%:=%])
+def $subst_subtype(subtype, typevar*, typeuse*) : subtype             hint(show %#`[%:=%])
+def $subst_rectype(rectype, typevar*, typeuse*) : rectype             hint(show %#`[%:=%])
+def $subst_deftype(deftype, typevar*, typeuse*) : deftype             hint(show %#`[%:=%])
 
-def $subst_globaltype(globaltype, typevar*, heaptype*) : globaltype    hint(show %#`[%:=%])
-def $subst_functype(functype, typevar*, heaptype*) : functype          hint(show %#`[%:=%])
-def $subst_tabletype(tabletype, typevar*, heaptype*) : tabletype       hint(show %#`[%:=%])
-def $subst_memtype(memtype, typevar*, heaptype*) : memtype             hint(show %#`[%:=%])
+def $subst_globaltype(globaltype, typevar*, typeuse*) : globaltype    hint(show %#`[%:=%])
+def $subst_functype(functype, typevar*, typeuse*) : functype          hint(show %#`[%:=%])
+def $subst_tabletype(tabletype, typevar*, typeuse*) : tabletype       hint(show %#`[%:=%])
+def $subst_memtype(memtype, typevar*, typeuse*) : memtype             hint(show %#`[%:=%])
 
-def $subst_externtype(externtype, typevar*, heaptype*) : externtype    hint(show %#`[%:=%])
+def $subst_externtype(externtype, typevar*, typeuse*) : externtype    hint(show %#`[%:=%])
 
 
 def $subst_typevar(xx, eps, eps) = xx
-def $subst_typevar(xx, xx_1 xx'*, ht_1 ht'*) = ht_1                            -- if xx = xx_1
-def $subst_typevar(xx, xx_1 xx'*, ht_1 ht'*) = $subst_typevar(xx, xx'*, ht'*)  -- otherwise
+def $subst_typevar(xx, xx_1 xx'*, tu_1 tu'*) = tu_1                            -- if xx = xx_1
+def $subst_typevar(xx, xx_1 xx'*, tu_1 tu'*) = $subst_typevar(xx, xx'*, tu'*)  -- otherwise
 
-def $subst_numtype(nt, xx*, ht*) = nt
-def $subst_vectype(vt, xx*, ht*) = vt
+def $subst_typeuse(xx', xx*, tu*) = $subst_typevar(xx', xx*, tu*)
+def $subst_typeuse(dt, xx*, tu*) = $subst_deftype(dt, xx*, tu*)
 
-def $subst_heaptype(xx', xx*, ht*) = $subst_typevar(xx', xx*, ht*)
-def $subst_heaptype(dt, xx*, ht*) = $subst_deftype(dt, xx*, ht*)
-def $subst_heaptype(ht', xx*, ht*) = ht'  -- otherwise
+def $subst_numtype(nt, xx*, tu*) = nt
+def $subst_vectype(vt, xx*, tu*) = vt
 
-def $subst_reftype((REF nul ht'), xx*, ht*) = REF nul $subst_heaptype(ht', xx*, ht*)
+def $subst_heaptype(xx', xx*, tu*) = $subst_typevar(xx', xx*, tu*)
+def $subst_heaptype(dt, xx*, tu*) = $subst_deftype(dt, xx*, tu*)
+def $subst_heaptype(ht, xx*, tu*) = ht  -- otherwise
 
-def $subst_valtype(nt, xx*, ht*) = $subst_numtype(nt, xx*, ht*)
-def $subst_valtype(vt, xx*, ht*) = $subst_vectype(vt, xx*, ht*)
-def $subst_valtype(rt, xx*, ht*) = $subst_reftype(rt, xx*, ht*)
-def $subst_valtype(BOT, xx*, ht*) = BOT
+def $subst_reftype((REF nul ht), xx*, tu*) = REF nul $subst_heaptype(ht, xx*, tu*)
 
-def $subst_packtype(pt, xx*, ht*) = pt
+def $subst_valtype(nt, xx*, tu*) = $subst_numtype(nt, xx*, tu*)
+def $subst_valtype(vt, xx*, tu*) = $subst_vectype(vt, xx*, tu*)
+def $subst_valtype(rt, xx*, tu*) = $subst_reftype(rt, xx*, tu*)
+def $subst_valtype(BOT, xx*, tu*) = BOT
 
-def $subst_storagetype(t, xx*, ht*) = $subst_valtype(t, xx*, ht*)
-def $subst_storagetype(pt, xx*, ht*) = $subst_packtype(pt, xx*, ht*)
+def $subst_packtype(pt, xx*, tu*) = pt
 
-def $subst_fieldtype((mut zt), xx*, ht*) = mut $subst_storagetype(zt, xx*, ht*)
+def $subst_storagetype(t, xx*, tu*) = $subst_valtype(t, xx*, tu*)
+def $subst_storagetype(pt, xx*, tu*) = $subst_packtype(pt, xx*, tu*)
 
-def $subst_comptype((STRUCT yt*), xx*, ht*) = STRUCT $subst_fieldtype(yt, xx*, ht*)*
-def $subst_comptype((ARRAY yt), xx*, ht*) = ARRAY $subst_fieldtype(yt, xx*, ht*)
-def $subst_comptype((FUNC ft), xx*, ht*) = FUNC $subst_functype(ft, xx*, ht*)
+def $subst_fieldtype((mut zt), xx*, tu*) = mut $subst_storagetype(zt, xx*, tu*)
 
-def $subst_subtype((SUB fin y* ct), xx*, ht*) =
-  SUBD fin $subst_heaptype(_IDX y, xx*, ht*)* $subst_comptype(ct, xx*, ht*)
-def $subst_subtype((SUBD fin ht'* ct), xx*, ht*) =
-  SUBD fin $subst_heaptype(ht', xx*, ht*)* $subst_comptype(ct, xx*, ht*)
+def $subst_comptype((STRUCT yt*), xx*, tu*) = STRUCT $subst_fieldtype(yt, xx*, tu*)*
+def $subst_comptype((ARRAY yt), xx*, tu*) = ARRAY $subst_fieldtype(yt, xx*, tu*)
+def $subst_comptype((FUNC ft), xx*, tu*) = FUNC $subst_functype(ft, xx*, tu*)
 
-def $subst_rectype((REC st*), xx*, ht*) = REC $subst_subtype(st, xx*, ht*)*
+def $subst_subtype((SUB fin tu'* ct), xx*, tu*) =
+  SUB fin $subst_typeuse(tu', xx*, tu*)* $subst_comptype(ct, xx*, tu*)
 
-def $subst_deftype((DEF qt i), xx*, ht*) = DEF $subst_rectype(qt, xx*, ht*) i
+def $subst_rectype((REC st*), xx*, tu*) = REC $subst_subtype(st, xx*, tu*)*
 
-def $subst_globaltype((mut t), xx*, ht*) = mut $subst_valtype(t, xx*, ht*)
-def $subst_functype((t_1* -> t_2*), xx*, ht*) = $subst_valtype(t_1, xx*, ht*)* -> $subst_valtype(t_2, xx*, ht*)*
-def $subst_memtype((lim I8), xx*, ht*) = lim I8
-def $subst_tabletype((lim rt), xx*, ht*) = lim $subst_reftype(rt, xx*, ht*)
+def $subst_deftype((DEF qt i), xx*, tu*) = DEF $subst_rectype(qt, xx*, tu*) i
 
-def $subst_externtype((FUNC dt), xx*, ht*) = FUNC $subst_deftype(dt, xx*, ht*)
-def $subst_externtype((GLOBAL gt), xx*, ht*) = GLOBAL $subst_globaltype(gt, xx*, ht*)
-def $subst_externtype((TABLE tt), xx*, ht*) = TABLE $subst_tabletype(tt, xx*, ht*)
-def $subst_externtype((MEM mt), xx*, ht*) = MEM $subst_memtype(mt, xx*, ht*)
+def $subst_globaltype((mut t), xx*, tu*) = mut $subst_valtype(t, xx*, tu*)
+def $subst_functype((t_1* -> t_2*), xx*, tu*) = $subst_valtype(t_1, xx*, tu*)* -> $subst_valtype(t_2, xx*, tu*)*
+def $subst_memtype((lim I8), xx*, tu*) = lim I8
+def $subst_tabletype((lim rt), xx*, tu*) = lim $subst_reftype(rt, xx*, tu*)
+
+def $subst_externtype((FUNC dt), xx*, tu*) = FUNC $subst_deftype(dt, xx*, tu*)
+def $subst_externtype((GLOBAL gt), xx*, tu*) = GLOBAL $subst_globaltype(gt, xx*, tu*)
+def $subst_externtype((TABLE tt), xx*, tu*) = TABLE $subst_tabletype(tt, xx*, tu*)
+def $subst_externtype((MEM mt), xx*, tu*) = MEM $subst_memtype(mt, xx*, tu*)
 
 
 def $subst_all_reftype(reftype, heaptype*) : reftype  hint(show %#`[:=%])
 def $subst_all_deftype(deftype, heaptype*) : deftype  hint(show %#`[:=%])
 
-def $subst_all_reftype(rt, ht^n) = $subst_reftype(rt, $idx(i)^(i<n), ht^n)
-def $subst_all_deftype(dt, ht^n) = $subst_deftype(dt, $idx(i)^(i<n), ht^n)
+def $subst_all_reftype(rt, tu^n) = $subst_reftype(rt, $idx(i)^(i<n), tu^n)
+def $subst_all_deftype(dt, tu^n) = $subst_deftype(dt, $idx(i)^(i<n), tu^n)
 
 def $subst_all_deftypes(deftype*, heaptype*) : deftype*  hint(show %#`[:=%])
 
-def $subst_all_deftypes(eps, ht*) = eps
-def $subst_all_deftypes(dt_1 dt*, ht*) = $subst_all_deftype(dt_1, ht*) $subst_all_deftypes(dt*, ht*)
+def $subst_all_deftypes(eps, tu*) = eps
+def $subst_all_deftypes(dt_1 dt*, tu*) = $subst_all_deftype(dt_1, tu*) $subst_all_deftypes(dt*, tu*)
 
 
 ;; Rolling and Unrolling
@@ -240,7 +242,7 @@ def $unrollrt(REC st^n) = REC ($subst_subtype(st, (REC i)^(i<n), (DEF qt i)^(i<n
 def $rolldt(x, qt) = (DEF (REC st^n) i)^(i<n)  -- if $rollrt(x, qt) = REC st^n
 def $unrolldt(DEF qt i) = st*[i]               -- if $unrollrt(qt) = REC st*
 
-def $expanddt(dt) = ct                         -- if $unrolldt(dt) = SUBD fin ht* ct
+def $expanddt(dt) = ct                         -- if $unrolldt(dt) = SUB fin tu* ct
 
 relation Expand: deftype ~~ comptype
 rule Expand: dt ~~ ct                          -- if $expanddt(dt) = ct

diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -156,15 +156,15 @@ rule Comptype_ok/func:
 
 
 rule Subtype_ok:
-  C |- SUB FINAL? typeidx* comptype : OK(x_0)
+  C |- SUB FINAL? $idx(typeidx)* comptype : OK(x_0)
   -- if |x*| <= 1
   -- (if x < x_0)*
-  -- (if $unrolldt(C.TYPES[x]) = SUB x'* comptype')*
+  -- (if $unrolldt(C.TYPES[x]) = SUB $idx(x')* comptype')*
 
   -- Comptype_ok: C |- comptype : OK
   -- (Comptype_sub: C |- comptype <: comptype')*
 
-def $before(heaptype, typeidx, nat) : bool   hint(show % << %,%)
+def $before(typeuse, typeidx, nat) : bool   hint(show % << %,%)
 def $before(deftype, x, i) = true
 def $before(_IDX typeidx, x, i) = typeidx < x
 def $before(REC j, x, i) = j < i
@@ -175,10 +175,10 @@ def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
 def $unrollht(C, REC i) = C.REC[i]
 
 rule Subtype_ok2:
-  C |- SUBD FINAL? heaptype* compttype : OK x i
-  -- if |heaptype*| <= 1
-  -- (if $before(heaptype, x, i))*
-  -- (if $unrollht(C, heaptype) = SUBD heaptype'* comptype')*
+  C |- SUB FINAL? typeuse* compttype : OK x i
+  -- if |typeuse*| <= 1
+  -- (if $before(typeuse, x, i))*
+  -- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
 
   -- Comptype_ok: C |- comptype : OK
   -- (Comptype_sub: C |- comptype <: comptype')*
@@ -328,8 +328,8 @@ rule Heaptype_sub/typeidx-r:
   -- Heaptype_sub: C |- heaptype <: C.TYPES[typeidx]
 
 rule Heaptype_sub/rec:
-  C |- REC i <: ht
-  -- if C.REC[i] = SUBD fin (ht_1* ht ht_2*) ct
+  C |- REC i <: tu
+  -- if C.REC[i] = SUB fin (tu_1* tu tu_2*) ct
 
 rule Heaptype_sub/none:
   C |- NONE <: heaptype
@@ -440,8 +440,8 @@ rule Deftype_sub/refl:
 
 rule Deftype_sub/super:
   C |- deftype_1 <: deftype_2
-  -- if $unrolldt(deftype_1) = SUBD fin (ht_1* ht ht_2*) ct
-  -- Heaptype_sub: C |- ht <: deftype_2
+  -- if $unrolldt(deftype_1) = SUB fin (tu_1* tu tu_2*) ct
+  -- Heaptype_sub: C |- tu <: deftype_2
 
 
 ;; External types
@@ -645,7 +645,7 @@ rule Instr_ok/call:
   -- Expand: C.FUNCS[x] ~~ FUNC (t_1* -> t_2*)
 
 rule Instr_ok/call_ref:
-  C |- CALL_REF x : t_1* (REF NULL $idx(x)) -> t_2*
+  C |- CALL_REF $idx(x) : t_1* (REF NULL $idx(x)) -> t_2*
   -- Expand: C.TYPES[x] ~~ FUNC (t_1* -> t_2*)
 
 rule Instr_ok/call_indirect:
@@ -669,7 +669,7 @@ rule Instr_ok/return_call:
 
 ;; TODO: enable t_2* <: C.RETURN
 rule Instr_ok/return_call_ref:
-  C |- RETURN_CALL_REF x : t_3* t_1* (REF NULL $idx(x)) -> t_4*
+  C |- RETURN_CALL_REF $idx(x) : t_3* t_1* (REF NULL $idx(x)) -> t_4*
   -- Expand: C.TYPES[x] ~~ FUNC (t_1* -> t_2*)
   -- if C.RETURN = (t'_2*)
   -- Resulttype_sub: C |- t_2* <: t'_2*

diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup
@@ -157,14 +157,14 @@ rule Step_read/br_on_cast_fail-fail:
 ;; Function instructions
 
 rule Step_read/call:
-  z; (CALL x)  ~>  (REF.FUNC_ADDR a) (CALL_REF)
+  z; (CALL x)  ~>  (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE)
   -- if $funcaddr(z)[x] = a
 
 rule Step_read/call_ref-null:
-  z; (REF.NULL ht) (CALL_REF x?)  ~>  TRAP
+  z; (REF.NULL ht) (CALL_REF tu)  ~>  TRAP
 
 rule Step_read/call_ref-func:
-  z; val^n (REF.FUNC_ADDR a) (CALL_REF x?)  ~>  (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
+  z; val^n (REF.FUNC_ADDR a) (CALL_REF tu)  ~>  (FRAME_ m `{f} (LABEL_ m `{eps} instr*))
 
   -- if $funcinst(z)[a] = fi
   -- Expand: fi.TYPE ~~ FUNC (t_1^n -> t_2^m)
@@ -173,25 +173,26 @@ rule Step_read/call_ref-func:
 
 
 rule Step_read/return_call:
-  z; (RETURN_CALL x)  ~>  (REF.FUNC_ADDR $funcaddr(z)[x]) (RETURN_CALL_REF)
+  z; (RETURN_CALL x)  ~>  (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE)
+  -- if $funcaddr(z)[x] = a
 
 
 rule Step_read/return_call_ref-label:
-  z; (LABEL_ k `{instr'*} val* (RETURN_CALL_REF x?) instr*)  ~>  val* (RETURN_CALL_REF x?)
+  z; (LABEL_ k `{instr'*} val* (RETURN_CALL_REF tu) instr*)  ~>  val* (RETURN_CALL_REF tu)
 
 rule Step_read/return_call_ref-frame-null:
-  z; (FRAME_ k `{f} val* (REF.NULL ht) (RETURN_CALL_REF x?) instr*)  ~>  TRAP
+  z; (FRAME_ k `{f} val* (REF.NULL ht) (RETURN_CALL_REF tu) instr*)  ~>  TRAP
 
 rule Step_read/return_call_ref-frame-addr:
-  z; (FRAME_ k `{f} val'* val^n (REF.FUNC_ADDR a) (RETURN_CALL_REF x?) instr*)  ~>  val^n (REF.FUNC_ADDR a) (CALL_REF x?)
+  z; (FRAME_ k `{f} val'* val^n (REF.FUNC_ADDR a) (RETURN_CALL_REF tu) instr*)  ~>  val^n (REF.FUNC_ADDR a) (CALL_REF tu)
   -- Expand: $funcinst(z)[a].TYPE ~~ FUNC (t_1^n -> t_2^m)
 
 
 rule Step_pure/call_indirect:
-  (CALL_INDIRECT x y)  ~>  (TABLE.GET x) (REF.CAST (REF NULL $idx(y))) (CALL_REF y)
+  (CALL_INDIRECT x y)  ~>  (TABLE.GET x) (REF.CAST (REF NULL $idx(y))) (CALL_REF $idx(y))
 
 rule Step_pure/return_call_indirect:
-  (RETURN_CALL_INDIRECT x y)  ~>  (TABLE.GET x) (REF.CAST (REF NULL $idx(y))) (RETURN_CALL_REF y)
+  (RETURN_CALL_INDIRECT x y)  ~>  (TABLE.GET x) (REF.CAST (REF NULL $idx(y))) (RETURN_CALL_REF $idx(y))
 
 
 rule Step_pure/frame-vals:
@@ -245,7 +246,7 @@ rule Step_pure/cvtop-trap:
 ;; Reference instructions
 
 rule Step_read/ref.null-idx:
-  z; (REF.NULL $($(_IDX x)))  ~>  (REF.NULL $type(z, x))
+  z; (REF.NULL $idx(x))  ~>  (REF.NULL $type(z, x))
 
 rule Step_read/ref.func:
   z; (REF.FUNC x)  ~>  (REF.FUNC_ADDR $funcaddr(z)[x])

diff --git a/spectec/spec/wasm-3.0/9-module.watsup b/spectec/spec/wasm-3.0/9-module.watsup
@@ -172,7 +172,7 @@ def $instantiate(s, module, externval*) = s'; f; instr_E* instr_D* (CALL x)?
 ;;
 
 def $invoke(store, funcaddr, val*) : config
-def $invoke(s, fa, val^n) = s; f; val^n (REF.FUNC_ADDR fa) (CALL_REF 0)
+def $invoke(s, fa, val^n) = s; f; val^n (REF.FUNC_ADDR fa) (CALL_REF $funcinst((s; f))[fa].TYPE)
   -- if f = { MODULE {} }
   -- if $funcinst((s; f))[fa].CODE = FUNC x local* expr
   -- Expand: s.FUNCS[fa].TYPE ~~ FUNC (t_1^n -> t_2*)
diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup
@@ -145,8 +145,8 @@ grammar Bcomptype : comptype =
   | 0x58 yt:Bfieldtype => ARRAY yt
 
 grammar Bsubtype : subtype =
-  | 0x50 x*:Bvec(Btypeidx) ct:Bcomptype => SUB x* ct
-  | 0x49 x*:Bvec(Btypeidx) ct:Bcomptype => SUB FINAL x* ct
+  | 0x50 x*:Bvec(Btypeidx) ct:Bcomptype => SUB $idx(x)* ct
+  | 0x49 x*:Bvec(Btypeidx) ct:Bcomptype => SUB FINAL $idx(x)* ct
   | ct:Bcomptype => SUB FINAL eps ct
 
 grammar Brectype : rectype =

diff --git a/spectec/src/backend-interpreter/builtin.ml b/spectec/src/backend-interpreter/builtin.ml
@@ -26,7 +26,7 @@ let builtin () =
     let dt =
       CaseV ("DEF", [
         CaseV ("REC", [
-          [| CaseV ("SUBD", [none "FINAL"; listV [||]; ftype]) |] |> listV
+          [| CaseV ("SUB", [none "FINAL"; listV [||]; ftype]) |] |> listV
         ]); numV Z.zero
       ]) in
     name, StrV [