Exact func externtypes types

document/core/syntax/types.rst

@@ -473,7 +473,7 @@ External Types
 
 $${syntax: externtype}
 
-For functions, the :ref:`type use <syntax-typeuse>` has to refer to the definition of a :ref:`function type <syntax-functype>`.
+For functions, the :ref:`heap type <syntax-heaptype>` has to refer to the definition of a :ref:`function type <syntax-functype>`.
 
 .. note::
    Future versions of WebAssembly may have additional uses for tags, and may allow non-empty result types in the function types of tags.

document/core/valid/conventions.rst

@@ -225,7 +225,7 @@ which collects relevant information about the surrounding :ref:`module <syntax-m
 
 * *Types*: the list of :ref:`types <syntax-type>` defined in the current module.
 * *Recursive Types*: the list of :ref:`sub types <syntax-subtype>` in the current group of recursive types.
-* *Functions*: the list of :ref:`functions <syntax-func>` declared in the current module, represented by a :ref:`defined type <syntax-deftype>` that :ref:`expands <aux-expand-deftype>` to their :ref:`function type <syntax-functype>`.
+* *Functions*: the list of :ref:`functions <syntax-func>` declared in the current module, represented by a concrete :ref:`heap type <syntax-heaptype>` that :ref:`expands <aux-expand-deftype>` to their :ref:`function type <syntax-functype>`.
 * *Tables*: the list of :ref:`tables <syntax-table>` declared in the current module, represented by their :ref:`table type <syntax-tabletype>`.
 * *Memories*: the list of :ref:`memories <syntax-mem>` declared in the current module, represented by their :ref:`memory type <syntax-memtype>`.
 * *Globals*: the list of :ref:`globals <syntax-global>` declared in the current module, represented by their :ref:`global type <syntax-globaltype>`.

specification/wasm-latest/1.2-syntax.types.spectec

@@ -143,7 +143,7 @@ syntax datatype hint(desc "data type") = OK hint(macro "%data")
 syntax elemtype hint(desc "element type") = reftype
 
 syntax externtype hint(desc "external type") hint(macro "%" "XT%") =
-  | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC typeuse
+  | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC heaptype
 
 syntax moduletype hint(desc "module type") =
   externtype* -> externtype* hint(macro "toM")
@@ -317,7 +317,7 @@ def $tagsxt(externtype*) : tagtype*        hint(show $tags(%))    hint(macro "ta
 def $globalsxt(externtype*) : globaltype*  hint(show $globals(%)) hint(macro "globalsxt")
 def $memsxt(externtype*) : memtype*        hint(show $mems(%))    hint(macro "memsxt")
 def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))  hint(macro "tablesxt")
-def $funcsxt(externtype*) : deftype*       hint(show $funcs(%))   hint(macro "funcsxt")
+def $funcsxt(externtype*) : heaptype*      hint(show $funcs(%))   hint(macro "funcsxt")
 
 def $tagsxt(eps) = eps
 def $tagsxt((TAG jt) xt*) = jt $tagsxt(xt*)
@@ -336,7 +336,7 @@ def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*)
 def $tablesxt(externtype xt*) = $tablesxt(xt*)  -- otherwise
 
 def $funcsxt(eps) = eps
-def $funcsxt((FUNC dt) xt*) = dt $funcsxt(xt*)
+def $funcsxt((FUNC ht) xt*) = ht $funcsxt(xt*)
 def $funcsxt(externtype xt*) = $funcsxt(xt*)  -- otherwise
 
 
@@ -438,7 +438,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*)
 def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*)
 def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*)
 def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*)
-def $subst_externtype((FUNC dt), tv*, tu*) = FUNC $subst_deftype(dt, tv*, tu*)
+def $subst_externtype((FUNC ht), tv*, tu*) = FUNC $subst_heaptype(ht, tv*, tu*)
 
 def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)*
 
@@ -600,7 +600,7 @@ def $free_externtype(TAG tagtype) = $free_tagtype(tagtype)
 def $free_externtype(GLOBAL globaltype) = $free_globaltype(globaltype)
 def $free_externtype(MEM memtype) = $free_memtype(memtype)
 def $free_externtype(TABLE tabletype) = $free_tabletype(tabletype)
-def $free_externtype(FUNC typeuse) = $free_typeuse(typeuse)
+def $free_externtype(FUNC heaptype) = $free_heaptype(heaptype)
 
 def $free_moduletype(externtype_1* -> externtype_2*) =
   $free_list($free_externtype(externtype_1)*) ++

specification/wasm-latest/2.0-validation.contexts.spectec

@@ -28,7 +28,7 @@ syntax context hint(desc "context") hint(macro "%" "C%") =
     GLOBALS globaltype*     hint(desc "global"),
     MEMS memtype*           hint(desc "memory"),
     TABLES tabletype*       hint(desc "table"),
-    FUNCS deftype*          hint(desc "function"),
+    FUNCS heaptype*         hint(desc "function"),
     DATAS datatype*         hint(desc "data segment"),
     ELEMS elemtype*         hint(desc "element segment"),
     LOCALS localtype*       hint(desc "local"),

specification/wasm-latest/2.1-validation.types.spectec

@@ -261,6 +261,6 @@ rule Externtype_ok/table:
   -- Tabletype_ok: C |- tabletype : OK
 
 rule Externtype_ok/func:
-  C |- FUNC typeuse : OK
+  C |- FUNC (_HT exact? typeuse) : OK
   -- Typeuse_ok: C |- typeuse : OK
   -- Expand_use: typeuse ~~_C $($(FUNC t_1* -> t_2*))

specification/wasm-latest/2.2-validation.subtyping.spectec

@@ -260,5 +260,5 @@ rule Externtype_sub/table:
   -- Tabletype_sub: C |- tabletype_1 <: tabletype_2
 
 rule Externtype_sub/func:
-  C |- FUNC deftype_1 <: FUNC deftype_2
-  -- Deftype_sub: C |- deftype_1 <: deftype_2
+  C |- FUNC heaptype_1 <: FUNC heaptype_2
+  -- Heaptype_sub: C |- heaptype_1 <: heaptype_2

specification/wasm-latest/2.3-validation.instructions.spectec

@@ -120,7 +120,8 @@ rule Instr_ok/br_on_cast_fail:
 
 rule Instr_ok/call:
   C |- CALL x : t_1* -> t_2*
-  -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2*
+  -- if C.FUNCS[x] = _HT exact? dt
+  -- Expand: dt ~~ FUNC t_1* -> t_2*
 
 rule Instr_ok/call_ref:
   C |- CALL_REF (_IDX x) : t_1* (REF NULL (_HT _IDX x)) -> t_2*
@@ -140,7 +141,8 @@ rule Instr_ok/return:
 ;; TODO(3, rossberg): enable t_2* <: C.RETURN
 rule Instr_ok/return_call:
   C |- RETURN_CALL x : t_3* t_1* -> t_4*
-  -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2*
+  -- if C.FUNCS[x] = _HT exact? dt
+  -- Expand: dt ~~ FUNC t_1* -> t_2*
   -- if C.RETURN = (t'_2*)
   -- Resulttype_sub: C |- t_2* <: t'_2*
   -- Instrtype_ok: C |- t_3* -> t_4* : OK
@@ -210,8 +212,8 @@ rule Instr_ok/ref.null:
   -- Heaptype_ok: C |- ht : OK
 
 rule Instr_ok/ref.func:
-  C |- REF.FUNC x : eps -> (REF (_HT dt))
-  -- if C.FUNCS[x] = dt
+  C |- REF.FUNC x : eps -> (REF ht)
+  -- if C.FUNCS[x] = ht
   -- if x <- C.REFS
 
 rule Instr_ok/ref.i31:

specification/wasm-latest/2.4-validation.modules.spectec

@@ -90,7 +90,8 @@ rule Elemmode_ok/active:
 
 rule Start_ok:
   C |- START x : OK
-  -- Expand: C.FUNCS[x] ~~ FUNC eps -> eps
+  -- if C.FUNCS[x] = _HT exact? dt
+  -- Expand: dt ~~ FUNC eps -> eps
 
 
 ;; Im/exports
@@ -125,8 +126,8 @@ rule Externidx_ok/table:
   -- if C.TABLES[x] = tt
 
 rule Externidx_ok/func:
-  C |- FUNC x : FUNC dt
-  -- if C.FUNCS[x] = dt
+  C |- FUNC x : FUNC ht
+  -- if C.FUNCS[x] = ht
 
 
 ;; Modules
@@ -159,14 +160,15 @@ rule Module_ok:
   ----
   -- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*}
   ----
-  -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*}
+  -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS ht_I* ht*, REFS x*}
+  -- if ht* = (_HT EXACT dt)*
   -- if x* = $funcidx_nonfuncs(global* mem* table* elem*)
   ----
   -- if jt_I* = $tagsxt(xt_I*)
   -- if gt_I* = $globalsxt(xt_I*)
   -- if mt_I* = $memsxt(xt_I*)
   -- if tt_I* = $tablesxt(xt_I*)
-  -- if dt_I* = $funcsxt(xt_I*)
+  -- if ht_I* = $funcsxt(xt_I*)
 
 
 rule Types_ok/empty:

specification/wasm-latest/4.1-execution.values.spectec

@@ -102,7 +102,7 @@ rule Externaddr_ok/table:
   -- if s.TABLES[a] = tableinst
 
 rule Externaddr_ok/func:
-  s |- FUNC a : FUNC funcinst.TYPE
+  s |- FUNC a : FUNC (_HT EXACT funcinst.TYPE)
   -- if s.FUNCS[a] = funcinst
 
 rule Externaddr_ok/sub:

specification/wasm-latest/5.2-binary.types.spectec

@@ -100,7 +100,8 @@ grammar Btabletype : tabletype =
 
 
 grammar Bexterntype : externtype =
-  | 0x00 x:Btypeidx => FUNC (_IDX x)
+  | 0x00 x:Btypeidx => FUNC (_HT _IDX x)
+  | 0x20 x:Btypeidx => FUNC (_HT EXACT _IDX x)
   | 0x01 tt:Btabletype => TABLE tt
   | 0x02 mt:Bmemtype => MEM mt
   | 0x03 gt:Bglobaltype => GLOBAL gt

specification/wasm-latest/6.2-text.types.spectec

@@ -152,7 +152,8 @@ grammar Texterntype_(I) : (externtype, idctxt) =
   | "(" "global" id?:Tid? gt:Tglobaltype_(I) ")" => (GLOBAL gt, {GLOBALS (id?)})
   | "(" "memory" id?:Tid? mt:Tmemtype_(I) ")" => (MEM mt, {MEMS (id?)})
   | "(" "table" id?:Tid? tt:Ttabletype_(I) ")" => (TABLE tt, {TABLES (id?)})
-  | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC $($(_IDX x)), {FUNCS (id?)})
+  | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC $($(_HT _IDX x)), {FUNCS (id?)})
+  | "(" "func" id?:Tid? "(" "exact" (x,I'):Ttypeuse_(I) ")" ")" => (FUNC $($(_HT EXACT _IDX x)), {FUNCS (id?)})
 
 
 ;; Type uses