[spec] Add concrete ref types

document/core/appendix/index-rules.rst

@@ -13,13 +13,13 @@ Typing of Static Constructs
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
-:ref:`Limits <valid-limits>`                     :math:`\vdashlimits \limits : k`
-:ref:`Function type <valid-functype>`            :math:`\vdashfunctype \functype \ok`
-:ref:`Block type <valid-blocktype>`              :math:`\vdashblocktype \blocktype \ok`
-:ref:`Table type <valid-tabletype>`              :math:`\vdashtabletype \tabletype \ok`
-:ref:`Memory type <valid-memtype>`               :math:`\vdashmemtype \memtype \ok`
-:ref:`Global type <valid-globaltype>`            :math:`\vdashglobaltype \globaltype \ok`
-:ref:`External type <valid-externtype>`          :math:`\vdashexterntype \externtype \ok`
+:ref:`Limits <valid-limits>`                     :math:`C \vdashlimits \limits : k`
+:ref:`Function type <valid-functype>`            :math:`C \vdashfunctype \functype \ok`
+:ref:`Block type <valid-blocktype>`              :math:`C \vdashblocktype \blocktype \ok`
+:ref:`Table type <valid-tabletype>`              :math:`C \vdashtabletype \tabletype \ok`
+:ref:`Memory type <valid-memtype>`               :math:`C \vdashmemtype \memtype \ok`
+:ref:`Global type <valid-globaltype>`            :math:`C \vdashglobaltype \globaltype \ok`
+:ref:`External type <valid-externtype>`          :math:`C \vdashexterntype \externtype \ok`
 :ref:`Instruction <valid-instr>`                 :math:`S;C \vdashinstr \instr : \functype`
 :ref:`Instruction sequence <valid-instr-seq>`    :math:`S;C \vdashinstrseq \instr^\ast : \functype`
 :ref:`Expression <valid-expr>`                   :math:`C \vdashexpr \expr : \resulttype`
@@ -83,8 +83,17 @@ Matching
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
-:ref:`External type <match-externtype>`          :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
-:ref:`Limits <match-limits>`                     :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
+:ref:`Number type <match-numtype>`               :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2`
+:ref:`Heap type <match-heaptype>`                :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2`
+:ref:`Reference type <match-reftype>`            :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2`
+:ref:`Value type <match-valtype>`                :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
+:ref:`Result type <match-resulttype>`            :math:`C \vdashresulttypematch \resulttype_1 \matchesresulttype \resulttype_2`
+:ref:`Function type <match-functype>`            :math:`C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2`
+:ref:`Table type <match-tabletype>`              :math:`C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2`
+:ref:`Memory type <match-memtype>`               :math:`C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2`
+:ref:`Global type <match-globaltype>`            :math:`C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2`
+:ref:`External type <match-externtype>`          :math:`C \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
+:ref:`Limits <match-limits>`                     :math:`C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
 ===============================================  ===============================================================================
 
 

document/core/appendix/index-types.rst

@@ -13,9 +13,12 @@ Category                                  Constructor
 :ref:`Number type <syntax-numtype>`       |F32|                                        :math:`\hex{7D}` (-3 as |Bs7|)
 :ref:`Number type <syntax-numtype>`       |F64|                                        :math:`\hex{7C}` (-4 as |Bs7|)
 (reserved)                                                                             :math:`\hex{7B}` .. :math:`\hex{71}`
-:ref:`Reference type <syntax-reftype>`    |FUNCREF|                                    :math:`\hex{70}` (-16 as |Bs7|)
-:ref:`Reference type <syntax-reftype>`    |EXTERNREF|                                  :math:`\hex{6F}` (-17 as |Bs7|)
-(reserved)                                                                             :math:`\hex{6E}` .. :math:`\hex{61}`
+:ref:`Heap type <syntax-heaptype>`        |FUNC|                                       :math:`\hex{70}` (-16 as |Bs7|)
+:ref:`Heap type <syntax-heaptype>`        |EXTERN|                                     :math:`\hex{6F}` (-17 as |Bs7|)
+(reserved)                                                                             :math:`\hex{6E}` .. :math:`\hex{6D}`
+:ref:`Reference type <syntax-reftype>`    |REF| |NULL|                                 :math:`\hex{6C}` (-20 as |Bs7|)
+:ref:`Reference type <syntax-reftype>`    |REF|                                        :math:`\hex{6B}` (-21 as |Bs7|)
+(reserved)                                                                             :math:`\hex{6A}` .. :math:`\hex{61}`
 :ref:`Function type <syntax-functype>`    :math:`[\valtype^\ast] \to [\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 (reserved)                                                                             :math:`\hex{5F}` .. :math:`\hex{41}`
 :ref:`Result type <syntax-resulttype>`    :math:`[\epsilon]`                           :math:`\hex{40}` (-64 as |Bs7|)

document/core/appendix/properties.rst

@@ -4,6 +4,10 @@
 Soundness
 ---------
 
+.. todo:: need to operate wrt semantic types
+.. todo:: define "S \vdash t ok"
+.. todo:: ensure wf of guessed valtypes
+
 The :ref:`type system <type-system>` of WebAssembly is *sound*, implying both *type safety* and *memory safety* with respect to the WebAssembly semantics. For example:
 
 * All types declared and derived during validation are respected at run time;
@@ -50,7 +54,7 @@ Results
 :ref:`Results <syntax-result>` :math:`\TRAP`
 ............................................
 
-* The result is valid with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types <syntax-valtype>`.
+* The result is valid with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`valid <valid-valtype>` :ref:`value types <syntax-valtype>`.
 
 .. math::
    \frac{
@@ -221,6 +225,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\limits~t`.
 
+.. todo:: reftypematch needs C
+
 .. math::
    \frac{
      \vdashtabletype \limits~t \ok
@@ -229,7 +235,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
      \qquad
      (S \vdash \reff : t')^n
      \qquad
-     (\vdashreftypematch t' \matchesvaltype t)^n
+     (C \vdashreftypematch t' \matchesvaltype t)^n
    }{
      S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t
    }
@@ -297,11 +303,13 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * Then the table instance is valid.
 
+.. todo:: reftypematch needs C
+
 .. math::
    \frac{
      (S \vdash \reff : t')^\ast
      \qquad
-     (\vdashreftypematch t' \matchesvaltype t)^\ast
+     (C \vdashreftypematch t' \matchesvaltype t)^\ast
    }{
      S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok
    }

document/core/binary/instructions.rst

@@ -88,7 +88,7 @@ Reference Instructions
 .. math::
    \begin{array}{llclll}
    \production{instruction} & \Binstr &::=& \dots \\ &&|&
-     \hex{D0}~~t{:}\Breftype &\Rightarrow& \REFNULL~t \\ &&|&
+     \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|&
      \hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
      \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\
    \end{array}

document/core/binary/types.rst

@@ -29,20 +29,40 @@ Number Types
    \end{array}
 
 
+.. index:: heap type
+   pair: binary format; heap type
+.. _binary-heaptype:
+
+Heap Types
+~~~~~~~~~~
+
+:ref:`Heap types <syntax-reftype>` are encoded as either a single byte, or as a :ref:`type index <binary-typeidx>` encoded as a positive :ref:`signed integer <binary-sint>`.
+
+.. math::
+   \begin{array}{llclll@{\qquad\qquad}l}
+   \production{heap type} & \Bheaptype &::=&
+     \hex{6F} &\Rightarrow& \EXTERN \\ &&|&
+     \hex{70} &\Rightarrow& \FUNC \\ &&|&
+     x{:}\Bs33 &\Rightarrow& x & (\iff x \geq 0) \\
+   \end{array}
+
+
 .. index:: reference type
    pair: binary format; reference type
 .. _binary-reftype:
 
 Reference Types
 ~~~~~~~~~~~~~~~
 
-:ref:`Reference types <syntax-reftype>` are also encoded by a single byte.
+:ref:`Reference types <syntax-reftype>` are either encoded by a single byte followed by a :ref:`heap type <binary-heaptype>`, or, as a short form, directly as a non-index heap type.
 
 .. math::
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{reference type} & \Breftype &::=&
-     \hex{70} &\Rightarrow& \FUNCREF \\ &&|&
-     \hex{6F} &\Rightarrow& \EXTERNREF \\
+     \hex{6B}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|&
+     \hex{6C}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|&
+     \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|&
+     \hex{70} &\Rightarrow& \FUNCREF \\
    \end{array}
 
 

document/core/exec/modules.rst

@@ -3,7 +3,7 @@ Modules
 
 For modules, the execution semantics primarily defines :ref:`instantiation <exec-instantiation>`, which :ref:`allocates <alloc>` instances for a module and its contained definitions, initializes :ref:`tables <syntax-table>` and :ref:`memories <syntax-mem>` from contained :ref:`element <syntax-elem>` and :ref:`data <syntax-data>` segments, and invokes the :ref:`start function <syntax-start>` if present. It also includes :ref:`invocation <exec-invocation>` of exported functions.
 
-Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports <exec-import>` and :ref:`allocating <alloc>` instances.
+Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports <match-externtype>` and :ref:`allocating <alloc>` instances.
 
 
 .. index:: external value, external type, validation, import, store

document/core/exec/runtime.rst

@@ -13,6 +13,7 @@ Runtime Structure
 .. _syntax-ref:
 .. _syntax-ref.extern:
 .. _syntax-val:
+.. _syntax-null:
 
 Values
 ~~~~~~

document/core/syntax/instructions.rst

@@ -434,7 +434,7 @@ Forward branches require operands according to the output of the targeted block'
 Backward branches require operands according to the input of the targeted block's type, i.e., represent the values consumed by the restarted block.
 
 The |CALL| instruction invokes another :ref:`function <syntax-func>`, consuming the necessary arguments from the stack and returning the result values of the call.
-The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table <syntax-table>` that is denoted by a :ref:`table index <syntax-tableidx>` and must have type |FUNCREF|.
+The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table <syntax-table>` that is denoted by a :ref:`table index <syntax-tableidx>` and must contain :ref:`function references <syntax-reftype>`.
 Since it may contain functions of heterogeneous type,
 the callee is dynamically checked against the :ref:`function type <syntax-functype>` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap <trap>` if it does not match.
 

document/core/syntax/modules.rst

@@ -273,7 +273,7 @@ The |EOFFSET| is given by a :ref:`constant <valid-constant>` :ref:`expression <s
 Element segments are referenced through :ref:`element indices <syntax-elemidx>`.
 
 .. note::
-   In the current version of WebAssembly, only tables of element type |FUNCREF| can be initialized with an element segment.
+   In the current version of WebAssembly, only tables whose elements are :ref:`function references <syntax-reftype>` can be initialized with an element segment.
    This limitation may be lifted in the future.
 
 

document/core/syntax/types.rst

@@ -41,34 +41,58 @@ Conventions
   That is, :math:`|\I32| = |\F32| = 32` and :math:`|\I64| = |\F64| = 64`.
 
 
-.. index:: ! reference type, reference, table, function, function type, null
+.. index:: ! heap type, store, type index
+   pair: abstract syntax; heap type
+.. _syntax-heaptype:
+
+Heap Types
+~~~~~~~~~~
+
+*Heap types* classify objects in the runtime :ref:`store <store>`.
+
+.. math::
+   \begin{array}{llll}
+   \production{heap type} & \heaptype &::=&
+     \FUNC ~|~ \EXTERN ~|~ \typeidx \\
+   \end{array}
+
+The type |FUNC| denotes the infinite union of all types of :ref:`functions <syntax-func>`, regardless of their concrete :ref:`function types <syntax-functype>`.
+
+The type |EXTERN| denotes the infinite union of all objects owned by the :ref:`embedder <embedder>` and that can be passed into WebAssembly under this type.
+
+A *concrete* heap type consists of a :ref:`type index <syntax-typeidx>` and classifies an object of the respective :ref:`type <syntax-type>` defined in the module.
+
+
+.. index:: ! reference type, heap type, reference, table, function, function type, null
    pair: abstract syntax; reference type
    pair: reference; type
 .. _syntax-reftype:
 
 Reference Types
 ~~~~~~~~~~~~~~~
 
-*Reference types* classify first-class references to objects in the runtime :ref:`store <store>`.
+*Reference types* classify :ref:`values <syntax-value>` that are first-class references to objects in the runtime :ref:`store <store>`.
 
 .. math::
    \begin{array}{llll}
    \production{reference type} & \reftype &::=&
-     \FUNCREF ~|~ \EXTERNREF \\
+     \REF~\NULL^?~\heaptype \\
    \end{array}
 
-The type |FUNCREF| denotes the infinite union of all references to :ref:`functions <syntax-func>`, regardless of their :ref:`function types <syntax-functype>`.
+A reference type is characterised by the :ref:`heap type <syntax-heaptype>` it points to.
 
-The type |EXTERNREF| denotes the infinite union of all references to objects owned by the :ref:`embedder <embedder>` and that can be passed into WebAssembly under this type.
+In addition, a reference type of the form :math:`\REF \NULL \X{ht}` is *nullable*, meaning that it can either be a proper reference to :math:`\X{ht}` or :ref:`null <syntax-null>`.
+Other references are *non-null*.
 
 Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed.
 Values of reference type can be stored in :ref:`tables <syntax-table>`.
 
 
-.. index:: ! value type, number type, reference type
+.. index:: ! value type, number type, reference type, ! bottom type
    pair: abstract syntax; value type
    pair: value; type
 .. _syntax-valtype:
+.. _syntax-bottype:
 
 Value Types
 ~~~~~~~~~~~

document/core/text/instructions.rst

@@ -70,7 +70,7 @@ However, the special case of a type use that is syntactically empty or consists
    \begin{array}[t]{@{}c@{}} ::= \\ | \\ \end{array}
    &
    \begin{array}[t]{@{}lcll@{}}
-     (t{:}\Tresult)^? &\Rightarrow& t^? \\
+     (t{:}\Tresult_I)^? &\Rightarrow& t^? \\
      x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\
    \end{array} \\
    \production{block instruction} & \Tblockinstr_I &::=&
@@ -128,9 +128,9 @@ The :math:`\text{else}` keyword of an :math:`\text{if}` instruction can be omitt
 .. math::
    \begin{array}{llclll}
    \production{block instruction} &
-     \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end}
+     \text{if}~~\Tlabel~~\Tblocktype_I~~\Tinstr^\ast~~\text{end}
        &\equiv&
-     \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{else}~~\text{end}
+     \text{if}~~\Tlabel~~\Tblocktype_I~~\Tinstr^\ast~~\text{else}~~\text{end}
    \end{array}
 
 Also, for backwards compatibility, the table index to :math:`\text{call\_indirect}` can be omitted, defaulting to :math:`0`.
@@ -178,7 +178,7 @@ Parametric Instructions
    \begin{array}{llclll}
    \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
      \text{drop} &\Rightarrow& \DROP \\ &&|&
-     \text{select}~((t{:}\Tresult)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\
+     \text{select}~((t{:}\Tresult_I)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\
    \end{array}