[spec] First go at specification

document/core/appendix/algorithm.rst

@@ -21,15 +21,49 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b
 Data Structures
 ~~~~~~~~~~~~~~~
 
+Types are representable as an enumeration.
+In addition to the plain types from the WebAssembly validation semantics, an extended notion of operand type includes a bottom type `Unknown` that is used as the type of :ref:`polymorphic <polymorphism>` operands.
+
+A simple subtyping check can be defined on these types.
+In addition, corresponding functions computing the join (least upper bound) and meet (greatest lower bound) of two types are used.
+Because there is no top type, a join does not exist in all cases.
+Similarly, a meet must always be defined on known value types that exclude the auxiliary bottom type `Unknown`,
+hence a meet does not exist in all cases either.
+A type error is encountered if a join or meet is required when it does not exist.
+
+.. code-block:: pseudo
+
+   type val_type = I32 | I64 | F32 | F64 | Anyref | Anyfunc | Anyeqref | Nullref
+   type opd_type = val_type | Unknown
+
+   func is_ref(t : opd_type) : bool =
+     return t = Anyref || t = Anyfunc || t = Anyeqref || t = Nullref
+
+   func matches(t1 : opd_type, t2 : opd_type) : bool =
+     return t1 = t2 || t1 = Unknown ||
+       (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref)
+
+   func join(t1 : opd_type, t2 : opd_type) : opd_type =
+     if (t1 = t2) return t1
+     if (matches(t1, t2)) return t2
+     if (matches(t2, t1)) return t1
+     error_if(not (is_ref(t1) && is_ref(t2)))
+     return Anyref
+
+   func meet(t1 : val_type, t2 : val_type) : val_type =
+     if (t1 = t2) return t1
+     if (matches(t1, t2)) return t1
+     if (matches(t2, t1)) return t2
+     error_if(not (is_ref(t1) && is_ref(t2)))
+     return Nullref
+
 The algorithm uses two separate stacks: the *operand stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
 the latter surrounding :ref:`structured control instructions <syntax-instr-control>` and their associated :ref:`blocks <syntax-instr-control>`.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64
-
-   type opd_stack = stack(val_type | Unknown)
+   type opd_stack = stack(opd_type)
 
    type ctrl_stack = stack(ctrl_frame)
    type ctrl_frame = {
@@ -58,20 +92,17 @@ However, these variables are not manipulated directly by the main checking funct
 
 .. code-block:: pseudo
 
-   func push_opd(type : val_type | Unknown) =
+   func push_opd(type : opd_type) =
      opds.push(type)
 
-   func pop_opd() : val_type | Unknown =
+   func pop_opd() : opd_type =
      if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
      error_if(opds.size() = ctrls[0].height)
      return opds.pop()
 
-   func pop_opd(expect : val_type | Unknown) : val_type | Unknown =
+   func pop_opd(expect : val_type) =
      let actual = pop_opd()
-     if (actual = Unknown) return expect
-     if (expect = Unknown) return actual
-     error_if(actual =/= expect)
-     return actual
+     error_if(not matches(actual, expect))
 
    func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t)
    func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t)
@@ -83,9 +114,8 @@ But first, a special case is handled where the block contains no known operands,
 That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically <polymorphism>`.
 In that case, an unknown type is returned.
 
-A second function for popping an operand takes an expected type, which the actual operand type is checked against.
-The types may differ in case one of them is Unknown.
-The more specific type is returned.
+A second function for popping an operand takes an expected (known) type, which the actual operand type is checked against.
+The types may differ by subtyping, inlcuding the case where the actual type is unknown.
 
 Finally, there are accumulative functions for pushing or popping multiple operand types.
 
@@ -150,14 +180,19 @@ Other instructions are checked in a similar manner.
          pop_opd(I32)
          push_opd(I32)
 
+       case (ref.eq)
+         pop_opd(Anyeqref)
+         pop_opd(Anyeqref)
+         push_opd(I32)
+
        case (drop)
          pop_opd()
 
        case (select)
          pop_opd(I32)
          let t1 = pop_opd()
-         let t2 = pop_opd(t1)
-         push_opd(t2)
+         let t2 = pop_opd()
+         push_opd(join(t1, t2))
 
        case (unreachable)
          unreachable()
@@ -193,10 +228,12 @@ Other instructions are checked in a similar manner.
 
        case (br_table n* m)
          error_if(ctrls.size() < m)
+         var ts = ctrls[m].label_types
          foreach (n in n*)
-           error_if(ctrls.size() < n || ctrls[n].label_types =/= ctrls[m].label_types)
+           error_if(ctrls.size() < n)
+           ts := meet(ts, ctrls[n].label_types)
          pop_opd(I32)
-         pop_opds(ctrls[m].label_types)
+         pop_opds(ts)
          unreachable()
 
 .. note::

document/core/appendix/index-instructions.rst

@@ -24,7 +24,7 @@ Instruction                          Binary Opcode     Type
 :math:`\BRTABLE~l^\ast~l`            :math:`\hex{0E}`  :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]`  :ref:`validation <valid-br_table>`        :ref:`execution <exec-br_table>`
 :math:`\RETURN`                      :math:`\hex{0F}`  :math:`[t_1^\ast~t^?] \to [t_2^\ast]`       :ref:`validation <valid-return>`          :ref:`execution <exec-return>`
 :math:`\CALL~x`                      :math:`\hex{10}`  :math:`[t_1^\ast] \to [t_2^\ast]`           :ref:`validation <valid-call>`            :ref:`execution <exec-call>`
-:math:`\CALLINDIRECT~x`              :math:`\hex{11}`  :math:`[t_1^\ast~\I32] \to [t_2^\ast]`      :ref:`validation <valid-call_indirect>`   :ref:`execution <exec-call_indirect>`
+:math:`\CALLINDIRECT~x~y`            :math:`\hex{11}`  :math:`[t_1^\ast~\I32] \to [t_2^\ast]`      :ref:`validation <valid-call_indirect>`   :ref:`execution <exec-call_indirect>`
 (reserved)                           :math:`\hex{12}`                                                  
 (reserved)                           :math:`\hex{13}`                                                  
 (reserved)                           :math:`\hex{14}`                                                  
@@ -44,8 +44,8 @@ Instruction                          Binary Opcode     Type
 :math:`\TEELOCAL~x`                  :math:`\hex{22}`  :math:`[t] \to [t]`                         :ref:`validation <valid-tee_local>`       :ref:`execution <exec-tee_local>`
 :math:`\GETGLOBAL~x`                 :math:`\hex{23}`  :math:`[] \to [t]`                          :ref:`validation <valid-get_global>`      :ref:`execution <exec-get_global>`
 :math:`\SETGLOBAL~x`                 :math:`\hex{24}`  :math:`[t] \to []`                          :ref:`validation <valid-set_global>`      :ref:`execution <exec-set_global>`
-(reserved)                           :math:`\hex{25}`                                                  
-(reserved)                           :math:`\hex{26}`                                                  
+:math:`\GETTABLE~x`                  :math:`\hex{25}`  :math:`[\I32] \to [t]`                      :ref:`validation <valid-get_table>`       :ref:`execution <exec-get_table>`
+:math:`\SETTABLE~x`                  :math:`\hex{26}`  :math:`[\I32~t] \to []`                     :ref:`validation <valid-set_table>`       :ref:`execution <exec-set_table>`
 (reserved)                           :math:`\hex{27}`                                                  
 :math:`\I32.\LOAD~\memarg`           :math:`\hex{28}`  :math:`[\I32] \to [\I32]`                   :ref:`validation <valid-load>`            :ref:`execution <exec-load>`
 :math:`\I64.\LOAD~\memarg`           :math:`\hex{29}`  :math:`[\I32] \to [\I64]`                   :ref:`validation <valid-load>`            :ref:`execution <exec-load>`
@@ -199,5 +199,24 @@ Instruction                          Binary Opcode     Type
 :math:`\I64.\REINTERPRET\K{/}\F64`   :math:`\hex{BD}`  :math:`[\F64] \to [\I64]`                   :ref:`validation <valid-cvtop>`           :ref:`execution <exec-cvtop>`, :ref:`operator <op-reinterpret>`
 :math:`\F32.\REINTERPRET\K{/}\I32`   :math:`\hex{BE}`  :math:`[\I32] \to [\F32]`                   :ref:`validation <valid-cvtop>`           :ref:`execution <exec-cvtop>`, :ref:`operator <op-reinterpret>`
 :math:`\F64.\REINTERPRET\K{/}\I64`   :math:`\hex{BF}`  :math:`[\I64] \to [\F64]`                   :ref:`validation <valid-cvtop>`           :ref:`execution <exec-cvtop>`, :ref:`operator <op-reinterpret>`
+(reserved)                           :math:`\hex{C0}`                                                  
+(reserved)                           :math:`\hex{C1}`                                                  
+(reserved)                           :math:`\hex{C2}`                                                  
+(reserved)                           :math:`\hex{C3}`                                                  
+(reserved)                           :math:`\hex{C4}`                                                  
+(reserved)                           :math:`\hex{C5}`                                                  
+(reserved)                           :math:`\hex{C6}`                                                  
+(reserved)                           :math:`\hex{C7}`                                                  
+(reserved)                           :math:`\hex{C8}`                                                  
+(reserved)                           :math:`\hex{C9}`                                                  
+(reserved)                           :math:`\hex{CA}`                                                  
+(reserved)                           :math:`\hex{CB}`                                                  
+(reserved)                           :math:`\hex{CC}`                                                  
+(reserved)                           :math:`\hex{CD}`                                                  
+(reserved)                           :math:`\hex{CE}`                                                  
+(reserved)                           :math:`\hex{CF}`                                                  
+:math:`\REFNULL`                     :math:`\hex{D0}`  :math:`[] \to [\NULLREF]`                   :ref:`validation <valid-ref_null>`        :ref:`execution <exec-ref_null>`
+:math:`\REFISNULL`                   :math:`\hex{D1}`  :math:`[\ANYREF] \to [\I32]`                :ref:`validation <valid-ref_isnull>`        :ref:`execution <exec-ref_isnull>`
+:math:`\REFEQ`                       :math:`\hex{D2}`  :math:`[\ANYEQREF~\ANYEQREF] \to [\I32]`    :ref:`validation <valid-ref_eq>`          :ref:`execution <exec-ref_eq>`
 ===================================  ================  ==========================================  ========================================  ===============================================================
 

document/core/appendix/index-rules.rst

@@ -71,14 +71,15 @@ Construct                                        Judgement
 ===============================================  ===============================================================================
 
 
-Import Matching
-~~~~~~~~~~~~~~~
+Matching
+~~~~~~~~
 
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
-:ref:`Limits <match-limits>`                     :math:`\vdashlimitsmatch \limits_1 \matches \limits_2`
-:ref:`External type <match-externtype>`          :math:`\vdashexterntypematch \externtype_1 \matches \externtype_2`
+:ref:`Value type <match-valtype>`                :math:`\vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
+:ref:`External type <match-externtype>`          :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
+:ref:`Limits <match-limits>`                     :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
 ===============================================  ===============================================================================
 
 

document/core/appendix/index-types.rst

@@ -8,17 +8,19 @@ Index of Types
 Category                                  Constructor                                         Binary Opcode
 ========================================  ===========================================  ===============================================================================
 :ref:`Type index <syntax-typeidx>`        :math:`x`                                    (positive number as |Bs32| or |Bu32|)
-:ref:`Value type <syntax-valtype>`        |I32|                                        :math:`\hex{7F}` (-1 as |Bs7|)
-:ref:`Value type <syntax-valtype>`        |I64|                                        :math:`\hex{7E}` (-2 as |Bs7|)
-:ref:`Value type <syntax-valtype>`        |F32|                                        :math:`\hex{7D}` (-3 as |Bs7|)
-:ref:`Value type <syntax-valtype>`        |F64|                                        :math:`\hex{7C}` (-4 as |Bs7|)
-(reserved)                                                                             :math:`\hex{7C}` .. :math:`\hex{71}`
-:ref:`Element type <syntax-elemtype>`     |ANYFUNC|                                    :math:`\hex{70}` (-16 as |Bs7|)
-(reserved)                                                                             :math:`\hex{6F}` .. :math:`\hex{61}`
+:ref:`Number type <syntax-numtype>`       |I32|                                        :math:`\hex{7F}` (-1 as |Bs7|)
+:ref:`Number type <syntax-numtype>`       |I64|                                        :math:`\hex{7E}` (-2 as |Bs7|)
+: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>`    |ANYFUNC|                                    :math:`\hex{70}` (-16 as |Bs7|)
+:ref:`Reference type <syntax-reftype>`    |ANYREF|                                     :math:`\hex{6F}` (-17 as |Bs7|)
+:ref:`Reference type <syntax-reftype>`    |ANYEQREF|                                   :math:`\hex{6E}` (-18 as |Bs7|)
+(reserved)                                                                             :math:`\hex{6D}` .. :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|)
-:ref:`Table type <syntax-tabletype>`      :math:`\limits~\elemtype`                    (none)
+:ref:`Table type <syntax-tabletype>`      :math:`\limits~\reftype`                     (none)
 :ref:`Memory type <syntax-memtype>`       :math:`\limits`                              (none)
 :ref:`Global type <syntax-globaltype>`    :math:`\mut~\valtype`                        (none)
 ========================================  ===========================================  ===============================================================================

document/core/binary/instructions.rst

@@ -54,17 +54,39 @@ Control Instructions
        &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|&
      \hex{0F} &\Rightarrow& \RETURN \\ &&|&
      \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|&
-     \hex{11}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \CALLINDIRECT~x \\
+     \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\
    \end{array}
 
 .. note::
    The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty.
 
+
+.. index:: reference instruction
+   pair: binary format; instruction
+.. _binary-instr-ref:
+
+Reference Instructions
+~~~~~~~~~~~~~~~~~~~~~~
+
+:ref:`Reference instructions <syntax-instr-ref>` are represented by single byte codes.
+
+.. _binary-ref_null:
+.. _binary-ref_isnull:
+.. _binary-ref_eq:
+
+.. math::
+   \begin{array}{llclll}
+   \production{instruction} & \Binstr &::=& \dots \\ &&|&
+     \hex{D0} &\Rightarrow& \REFNULL \\ &&|&
+     \hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
+     \hex{D2} &\Rightarrow& \REFEQ \\
+   \end{array}
+
 .. note::
-   In future versions of WebAssembly, the zero byte occurring in the encoding
-   of the |CALLINDIRECT| instruction may be used to index additional tables.
+   These opcode assignments are preliminary.
+
 
-.. index:: value type, polymorphism
+.. index:: parametric instruction, value type, polymorphism
    pair: binary format; instruction
 .. _binary-instr-parametric:
 
@@ -110,6 +132,29 @@ Variable Instructions
    \end{array}
 
 
+.. index:: table instruction, table index
+   pair: binary format; instruction
+.. _binary-instr-table:
+
+Table Instructions
+~~~~~~~~~~~~~~~~~~
+
+:ref:`Table instructions <syntax-instr-table>` are represented by single byte codes.
+
+.. _binary-get_table:
+.. _binary-set_table:
+
+.. math::
+   \begin{array}{llclll}
+   \production{instruction} & \Binstr &::=& \dots \\ &&|&
+     \hex{25}~~x{:}\Btableidx &\Rightarrow& \GETTABLE~x \\ &&|&
+     \hex{26}~~x{:}\Btableidx &\Rightarrow& \SETTABLE~x \\
+   \end{array}
+
+.. note::
+   These opcode assignments are preliminary.
+
+
 .. index:: memory instruction, memory index
    pair: binary format; instruction
 .. _binary-instr-memory: