Exact func externtype types

document/core/appendix/index-rules.rst

@@ -52,7 +52,7 @@ Construct                                        Judgement
 :ref:`Global <valid-global>`                     :math:`C \vdashglobal \global : \globaltype`
 :ref:`Memory <valid-mem>`                        :math:`C \vdashmem \mem : \memtype`
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`
-:ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \deftype`
+:ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \exactdeftype`
 :ref:`Local <valid-local>`                       :math:`C \vdashlocal \local : \localtype`
 :ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem : \reftype`
 :ref:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode : \reftype`

document/core/appendix/properties.rst

@@ -435,7 +435,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
 * Under :ref:`context <context>` :math:`C`:
 
-  * The :ref:`function <syntax-func>` :math:`\func` must be :ref:`valid <valid-func>` with some :ref:`defined type <syntax-deftype>` :math:`\deftype'`.
+  * The :ref:`function <syntax-func>` :math:`\func` must be :ref:`valid <valid-func>` with some :ref:`exact defined type <syntax-exactdeftype>` :math:`\EXACT~\deftype'`.
 
   * The :ref:`defined type <syntax-deftype>` :math:`\deftype'` must :ref:`match <match-deftype>` :math:`\deftype`.
 
@@ -448,7 +448,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
      \qquad
      S \vdashmoduleinst \moduleinst : C
      \\
-     C \vdashfunc \func : \deftype'
+     C \vdashfunc \func : \EXACT~\deftype'
      \qquad
      C \vdashdeftypematch \deftype' \subdeftypematch \deftype
      \end{array}
@@ -707,7 +707,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
 * For each :ref:`table address <syntax-tableaddr>` :math:`\tableaddr_i` in :math:`\moduleinst.\MITABLES`, the :ref:`external address <syntax-externaddr>` :math:`\XATABLE~\tableaddr_i` must be :ref:`valid <valid-externaddr-table>` with some :ref:`external type <syntax-externtype>` :math:`\XTTABLE~\tabletype_i`.
 
-* For each :ref:`function address <syntax-funcaddr>` :math:`\funcaddr_i` in :math:`\moduleinst.\MIFUNCS`, the :ref:`external address <syntax-externaddr>` :math:`\XAFUNC~\funcaddr_i` must be :ref:`valid <valid-externaddr-func>` with some :ref:`external type <syntax-externtype>` :math:`\XTFUNC~\deftype_{\K{F}i}`.
+* For each :ref:`function address <syntax-funcaddr>` :math:`\funcaddr_i` in :math:`\moduleinst.\MIFUNCS`, the :ref:`external address <syntax-externaddr>` :math:`\XAFUNC~\funcaddr_i` must be :ref:`valid <valid-externaddr-func>` with some :ref:`external type <syntax-externtype>` :math:`\XTFUNC~\exactdeftype_i`.
 
 * For each :ref:`data address <syntax-dataaddr>` :math:`\dataaddr_i` in :math:`\moduleinst.\MIDATAS`, the :ref:`data instance <syntax-datainst>` :math:`S.\SDATAS[\dataaddr_i]` must be :ref:`valid <valid-datainst>` with :math:`\X{ok}_i`.
 
@@ -727,7 +727,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
 * Let :math:`\tabletype^\ast` be the concatenation of all :math:`\tabletype_i` in order.
 
-* Let :math:`\deftype_{\K{F}}^\ast` be the concatenation of all :math:`\deftype_{\K{F}i}` in order.
+* Let :math:`\exactdeftype^\ast` be the concatenation of all :math:`\exactdeftype_i` in order.
 
 * Let :math:`\reftype^\ast` be the concatenation of all :math:`\reftype_i` in order.
 
@@ -738,7 +738,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 * Let :math:`x^\ast` be the sequence of :ref:`function indices <syntax-funcidx>` from :math:`0` to :math:`k-1` for some :math:`k` that is smaller than or equal to the number of functions in the instance.
 
 * Then the module instance is valid with :ref:`context <context>`
-  :math:`\{\CTYPES~\deftype^\ast,` :math:`\CTAGS~\tagtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CFUNCS~\deftype_{\K{F}}^\ast,` :math:`\CDATAS~\X{ok}^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CREFS~x^\ast\}`.
+  :math:`\{\CTYPES~\deftype^\ast,` :math:`\CTAGS~\tagtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CFUNCS~\exactdeftype^\ast,` :math:`\CDATAS~\X{ok}^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CREFS~x^\ast\}`.
 
 .. math::
    ~\\[-1ex]
@@ -750,7 +750,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
      \\
      (S \vdashexternaddr \XAGLOBAL~\globaladdr : \XTGLOBAL~\globaltype)^\ast
      \qquad
-     (S \vdashexternaddr \XAFUNC~\funcaddr : \XTFUNC~\deftype_{\K{F}})^\ast
+     (S \vdashexternaddr \XAFUNC~\funcaddr : \XTFUNC~\exactdeftype)^\ast
      \\
      (S \vdashexternaddr \XAMEM~\memaddr : \XTMEM~\memtype)^\ast
      \qquad
@@ -784,7 +784,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
          \CGLOBALS & \globaltype^\ast, \\
          \CMEMS & \memtype^\ast, \\
          \CTABLES & \tabletype^\ast, \\
-         \CFUNCS & \deftype_{\K{F}}^\ast, \\
+         \CFUNCS & \exactdeftype^\ast, \\
          \CDATAS & \X{ok}^\ast, \\
          \CELEMS & \reftype^\ast, \\
          \CREFS & 0 \dots k-1 ~\}
@@ -824,6 +824,8 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
        \\\
        (S; C \vdashglobaltype \globaltype \OKglobaltype)^\ast
        \qquad
+       \exactdeftype^\ast = (\exact^?~\deftype')^\ast
+       \qquad
        (S; C \vdashdeftype \deftype' \OKdeftype)^\ast
        \\
        (S; C \vdashmemtype \memtype \OKmemtype)^\ast
@@ -839,7 +841,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
          \CGLOBALS & \globaltype^\ast, \\
          \CMEMS & \memtype^\ast, \\
          \CTABLES & \tabletype^\ast, \\
-         \CFUNCS & {\deftype'}^\ast, \\
+         \CFUNCS & \exactdeftype^\ast, \\
          \CELEMS & \reftype^\ast, \\
          \CDATAS & {\X{ok}}^\ast ~\}
          \end{array}

document/core/syntax/types.rst

@@ -73,14 +73,16 @@ $${definition-ignore: vsize}
 .. index:: ! type use, type index
    pair: abstract syntax; type use
 .. _syntax-typeuse:
+.. _syntax-exacttypeuse:
 
 Type Uses
 ~~~~~~~~~
 
 A *type use* is the use site of a :ref:`type index <syntax-typeidx>` referencing a :ref:`composite type <syntax-comptype>` :ref:`defined <syntax-type>` in a :ref:`module <syntax-module>`.
 It classifies objects of the respective type.
+In some contexts, a type use may be annotated with :ref:`exactness <syntax-exact>`.
 
-$${syntax: {typeuse/syn}}
+$${syntax: {typeuse/syn exacttypeuse}}
 
 The syntax of type uses is :ref:`extended <syntax-typeuse-ext>` with additional forms for the purpose of specifying :ref:`validation <valid>` and :ref:`execution <exec>`.
 
@@ -110,8 +112,8 @@ That is, both type hierarchies are inhabited by an isomorphic set of values, but
 $${syntax: {absheaptype/syn heaptype}}
 
 A heap type is either *abstract* or *concrete*.
-A concrete heap type consists of a :ref:`type use <syntax-typeuse>` that classifies an object of the respective :ref:`type <syntax-type>` defined in a module.
-A concrete heap type may be *exact*, in which case it classifies objects of precisely the respective :ref:`type <syntax-type>` and not any other type that may :ref:`match <match-heaptype>` it.
+A concrete heap type consists of an :ref:`exact type use <syntax-exacttypeuse>` that classifies an object of the respective :ref:`type <syntax-type>` defined in a module.
+When the type use is annotated with ${:EXACT}, it classifies objects of precisely the respective :ref:`type <syntax-type>` and not any other type that may :ref:`match <match-heaptype>` it.
 Abstract types are denoted by individual keywords.
 
 The type ${:FUNC} denotes the common supertype of all :ref:`function types <syntax-functype>`, regardless of their concrete definition.
@@ -473,7 +475,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:`exact type use <syntax-exacttypeuse>` 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/util/macros.def

@@ -309,6 +309,7 @@
 .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}}
 .. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}}
 .. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}}
+.. |exactdeftype| mathdef:: \xref{valid/conventions}{syntax-exactdeftype}{\X{exactdeftype}}
 
 .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
 .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
@@ -327,6 +328,7 @@
 .. |init| mathdef:: \xref{valid/conventions}{syntax-init}{\X{init}}
 
 .. |typeuse| mathdef:: \xref{syntax/types}{syntax-typeuse}{\X{typeuse}}
+.. |exacttypeuse| mathdef:: \xref{syntax/types}{syntax-exacttypeuse}{\X{exacttypeuse}}
 
 .. |instrtype| mathdef:: \xref{valid/conventions}{syntax-instrtype}{\X{instrtype}}
 .. |localtype| mathdef:: \xref{valid/conventions}{syntax-localtype}{\X{localtype}}

document/core/valid/conventions.rst

@@ -94,14 +94,16 @@ Convention
 .. index:: ! defined type, recursive type
    pair: abstract syntax; defined type
 .. _syntax-deftype:
+.. _syntax-exactdeftype:
 
 Defined Types
 ~~~~~~~~~~~~~
 
 *Defined types* denote the individual types defined in a :ref:`module <syntax-module>`.
 Each such type is represented as a projection from the :ref:`recursive type <syntax-rectype>` group it originates from, indexed by its position in that group.
+For the purpose of typing :ref:`functions <syntax-func>`, a defined type may be annotated with :ref:`exactness <syntax-exact>`.
 
-$${syntax: deftype}
+$${syntax: {deftype exactdeftype}}
 
 Defined types do not occur in the :ref:`binary <binary>` or :ref:`text <text>` format,
 but are formed by :ref:`rolling up <aux-roll-deftype>` the :ref:`recursive types <syntax-reftype>` defined in a module.
@@ -225,7 +227,7 @@ Validity of an individual definition is specified relative to a *context*,
 which collects relevant information about the surrounding :ref:`module <syntax-module>` and the definitions in scope:
 
 * *Types*: the list of :ref:`types <syntax-type>` defined in the current module.
-* *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 (possibly :ref:`exact <syntax-exact>`) :ref:`defined type <syntax-deftype>` 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>`.
@@ -281,7 +283,7 @@ The following conventions are adopted in stating these rules.
 
   .. note::
      For example, if ${:A} is a :ref:`function <syntax-func>`,
-     then ${:T} is a :ref:`defined function type <syntax-deftype>`;
+     then ${:T} is an :ref:`exact defined type <syntax-exactdeftype>`;
      for an ${:A} that is a :ref:`global <syntax-global>`,
      ${:T} is a :ref:`global type <syntax-globaltype>`;
      and so on.

document/core/valid/modules.rst

@@ -102,7 +102,7 @@ $${rule: Table_ok}
 Functions
 ~~~~~~~~~
 
-Functions ${:func} are classified by :ref:`defined types <syntax-deftype>` that :ref:`expand <aux-expand-deftype>` to :ref:`function types <syntax-functype>` of the form ${comptype: FUNC t_1* -> t_2*}.
+Functions ${:func} are classified by :ref:`exact defined types <syntax-exactdeftype>` that :ref:`expand <aux-expand-deftype>` to :ref:`function types <syntax-functype>` of the form ${comptype: FUNC t_1* -> t_2*}.
 
 $${rule-prose: Func_ok}
 

interpreter/syntax/ast.ml

@@ -413,12 +413,12 @@ let exporttype_of (m : module_) (ex : export) : exporttype =
         let Table (tt, _) = t.it in tt) m.it.tables in
       ExternTableT (Lib.List32.nth tts x.it)
     | FuncX x ->
-      let dts = funcs xts @ List.map (fun f ->
+      let uts = funcs xts @ List.map (fun f ->
         let Func (y, _, _) = f.it in
         (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs
       in
-      let (exact, dt) = Lib.List32.nth dts x.it in
-      ExternFuncT (exact, dt)
+      let (exact, ut) = Lib.List32.nth uts x.it in
+      ExternFuncT (exact, ut)
   in ExportT (name, subst_externtype (subst_of dts) xt)
 
 let moduletype_of (m : module_) : moduletype =

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

@@ -34,16 +34,20 @@ syntax rectype hint(desc "recursive type")  ;; forward decl
 syntax deftype hint(desc "defined type") =
   | _DEF rectype n hint(show %.%)
 
+syntax exactdeftype hint(desc "exact defined type") = exact? deftype
+
 syntax typeuse/syn hint(desc "type use") =
   | _IDX typeidx | ...
 syntax typeuse/sem =
   | ... | deftype | REC n hint(show REC.%)
 
+syntax exacttypeuse hint(desc "exact type use") = exact? typeuse
+
 syntax typevar hint(desc "type variable") =
   | _IDX typeidx | REC n hint(show REC.%)
 
 syntax heaptype hint(desc "heap type") =
-  | absheaptype | _HT exact? typeuse hint(show % %)
+  | absheaptype | _HT exacttypeuse hint(show %)
 
 syntax reftype hint(desc "reference type") =
   | REF null? heaptype
@@ -143,7 +147,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 exacttypeuse
 
 syntax moduletype hint(desc "module type") =
   externtype* -> externtype* hint(macro "toM")
@@ -158,6 +162,7 @@ var at : addrtype
 ;; var bt : blocktype  ;; defined below
 var ct : comptype
 var dt : deftype
+var edt : exactdeftype
 var et : elemtype
 var ft : fieldtype
 var gt : globaltype
@@ -317,7 +322,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*) : exactdeftype*  hint(show $funcs(%))   hint(macro "funcsxt")
 
 def $tagsxt(eps) = eps
 def $tagsxt((TAG jt) xt*) = jt $tagsxt(xt*)
@@ -336,7 +341,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 edt) xt*) = edt $funcsxt(xt*)
 def $funcsxt(externtype xt*) = $funcsxt(xt*)  -- otherwise
 
 
@@ -438,7 +443,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 tu'), tv*, tu*) = FUNC $subst_typeuse(tu', tv*, tu*)
+def $subst_externtype((FUNC exact? tu'), tv*, tu*) = FUNC exact? $subst_typeuse(tu', tv*, tu*)
 
 def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)*
 
@@ -595,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 exact? typeuse) = $free_typeuse(typeuse)
 
 def $free_moduletype(externtype_1* -> externtype_2*) =
   $free_list($free_externtype(externtype_1)*) ++

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

@@ -27,7 +27,7 @@ syntax context/syn 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 exactdeftype*     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

@@ -178,7 +178,7 @@ def $before(typeuse, i) = true  -- otherwise
 def $unrollht_(context, heaptype) : subtype
 def $unrollht_(C, _HT EXACT? deftype) = $unrolldt(deftype)
 def $unrollht_(C, _HT EXACT? _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
-def $unrollht_(C, _HT EXACT? REC i) = C.RECS[i]
+def $unrollht_(C, _HT EXACT? (REC i)) = C.RECS[i]
 
 rule Subtype_ok2:
   C |- SUB FINAL? typeuse* desctype : OK(i)
@@ -268,6 +268,6 @@ rule Externtype_ok/table:
   -- Tabletype_ok: C |- tabletype : OK
 
 rule Externtype_ok/func:
-  C |- FUNC typeuse : OK
+  C |- FUNC 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

@@ -278,5 +278,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 exactdeftype_1 <: FUNC exactdeftype_2
+  -- Heaptype_sub: C |- _HT exactdeftype_1 <: _HT exactdeftype_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] = 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] = 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 edt))
+  -- if C.FUNCS[x] = edt
   -- if x <- C.REFS
 
 rule Instr_ok/ref.i31: