[interpreter] Use small-step semantics

document/core/appendix/index-rules.rst

@@ -25,8 +25,10 @@ Construct                                        Judgement
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`
 :ref:`Memory <valid-mem>`                        :math:`C \vdashmem \mem : \memtype`
 :ref:`Global <valid-global>`                     :math:`C \vdashglobal \global : \globaltype`
-:ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem \ok`
-:ref:`Data segment <valid-data>`                 :math:`C \vdashdata \data \ok`
+:ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem : \segtype`
+:ref:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode : \segtype`
+:ref:`Data segment <valid-data>`                 :math:`C \vdashdata \data : \segtype`
+:ref:`Data mode <valid-datamode>`                :math:`C \vdashdatamode \datamode : \segtype`
 :ref:`Start function <valid-start>`              :math:`C \vdashstart \start \ok`
 :ref:`Export <valid-export>`                     :math:`C \vdashexport \export : \externtype`
 :ref:`Export description <valid-exportdesc>`     :math:`C \vdashexportdesc \exportdesc : \externtype`

document/core/appendix/properties.rst

@@ -485,54 +485,6 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    }
 
 
-.. index:: element, table, table address, module instance, function index
-
-:math:`\INITELEM~\tableaddr~o~x^n`
-..................................
-
-* The :ref:`external table value <syntax-externval>` :math:`\EVTABLE~\tableaddr` must be :ref:`valid <valid-externval-table>` with some :ref:`external table type <syntax-externtype>` :math:`\ETTABLE~\limits~\FUNCREF`.
-
-* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN`.
-
-* The :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst` must be :ref:`valid <valid-moduleinst>` with some :ref:`context <context>` :math:`C`.
-
-* Each :ref:`function index <syntax-funcidx>` :math:`x_i` in :math:`x^n` must be defined in the context :math:`C`.
-
-* Then the instruction is valid.
-
-.. math::
-   \frac{
-     S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\FUNCREF
-     \qquad
-     o + n \leq \limits.\LMIN
-     \qquad
-     (C.\CFUNCS[x] = \functype)^n
-   }{
-     S; C \vdashadmininstr \INITELEM~\tableaddr~o~x^n \ok
-   }
-
-
-.. index:: data, memory, memory address, byte
-
-:math:`\INITDATA~\memaddr~o~b^n`
-................................
-
-* The :ref:`external memory value <syntax-externval>` :math:`\EVMEM~\memaddr` must be :ref:`valid <valid-externval-mem>` with some :ref:`external memory type <syntax-externtype>` :math:`\ETMEM~\limits`.
-
-* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN` divided by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.
-
-* Then the instruction is valid.
-
-.. math::
-   \frac{
-     S \vdashexternval \EVMEM~\memaddr : \ETMEM~\limits
-     \qquad
-     o + n \leq \limits.\LMIN \cdot 64\,\F{Ki}
-   }{
-     S; C \vdashadmininstr \INITDATA~\memaddr~o~b^n \ok
-   }
-
-
 .. index:: label, instruction, result type
 
 :math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END`

document/core/binary/modules.rst

@@ -314,6 +314,7 @@ It decodes into an optional :ref:`start function <syntax-start>` that represents
    single: element; segment
 .. _binary-elem:
 .. _binary-elemsec:
+.. _binary-elemkind:
 .. _binary-elemexpr:
 
 Element Section
@@ -327,28 +328,37 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
    \production{element section} & \Belemsec &::=&
      \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\
    \production{element segment} & \Belem &::=&
-     \hex{00}~~o{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETABLE~0, \EOFFSET~o, \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast \} \\ &&|&
-     \hex{01}~~\hex{00}~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast \} \\ &&|&
-     \hex{02}~~x{:}\Btableidx~~o{:}\Bexpr~~\hex{00}~~y^\ast{:}\Bvec(\Bfuncidx)
-       &\Rightarrow& \{ \ETABLE~x, \EOFFSET~o, \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast \} \\ &&|&
-     \hex{04}~~o{:}\Bexpr~e^\ast{:}\Bvec(\Belemexpr)
-       &\Rightarrow& \{ \ETABLE~0, \EOFFSET~o, \ETYPE~\FUNCREF, \EINIT~e^\ast \} \\ &&|&
-     \hex{05}~~\X{et}:\Belemtype~~e^\ast{:}\Bvec(\Belemexpr)
-       &\Rightarrow& \{ \ETYPE~et, \EINIT~e^\ast \} \\ &&|&
-     \hex{06}~~x{:}\Btableidx~~o{:}\Bexpr~~\X{et}:\Belemtype~~e^\ast{:}\Bvec(\Belemexpr)
-       &\Rightarrow& \{ \ETABLE~x, \EOFFSET~o, \ETYPE~et, \EINIT~e^\ast \} \\
-   \production{elemexpr} & \Belemexpr &::=&
+     \hex{00}~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
+       &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+     \hex{01}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
+       &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
+     \hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
+       &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
+     \hex{04}~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Belemexpr)
+       &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
+     \hex{05}~~\X{et}:\Belemtype~~\X{el}^\ast{:}\Bvec(\Belemexpr)
+       &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&
+     \hex{06}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemtype~~\X{el}^\ast{:}\Bvec(\Belemexpr)
+       &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\
+   \production{element kind} & \Belemkind &::=&
+     \hex{00} &\Rightarrow& \FUNCREF \\
+   \production{element expression} & \Belemexpr &::=&
      \hex{D0}~\hex{0B} &\Rightarrow& \REFNULL~\END \\ &&|&
      \hex{D2}~x{:}\Bfuncidx~\hex{0B} &\Rightarrow& (\REFFUNC~x)~\END \\
    \end{array}
 
 .. note::
+   The initial byte can be interpreted as a bitfield.
+   Bit 0 indicates a passive segment,
+   bit 1 indicates the presence of an explicit table index for an active segment,
+   bit 2 indicates the use of element type and element expressions instead of element kind and element indices.
+
    In the current version of WebAssembly, at most one table may be defined or
    imported in a single module, so all valid :ref:`active <syntax-active>`
    element segments have a |ETABLE| value of :math:`0`.
 
+   Additional element kinds may be added in future versions of WebAssembly.
+
 
 .. index:: ! code section, function, local, type index, function type
    pair: binary format; function
@@ -427,14 +437,18 @@ It decodes into a vector of :ref:`data segments <syntax-data>` that represent th
      \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg} \\
    \production{data segment} & \Bdata &::=&
      \hex{00}~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte)
-       &\Rightarrow& \{ \DMEM~0, \DOFFSET~e, \DINIT~b^\ast \} \\ &&|&
+       &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DACTIVE~\{ \DMEM~0, \DOFFSET~e \} \} \\ &&|&
      \hex{01}~~b^\ast{:}\Bvec(\Bbyte)
-       &\Rightarrow& \{ \DINIT~b^\ast \} \\ &&|&
+       &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DPASSIVE \} \\ &&|&
      \hex{02}~~x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte)
-       &\Rightarrow& \{ \DMEM~x, \DOFFSET~e, \DINIT~b^\ast \} \\
+       &\Rightarrow& \{ \DINIT~b^\ast, \DMODE~\DACTIVE~\{ \DMEM~x, \DOFFSET~e \} \} \\
    \end{array}
 
 .. note::
+   The initial byte can be interpreted as a bitfield.
+   Bit 0 indicates a passive segment,
+   bit 1 indicates the presence of an explicit memory index for an active segment.
+
    In the current version of WebAssembly, at most one memory may be defined or
    imported in a single module, so all valid :ref:`active <syntax-active>` data
    segments have a |DMEM| value of :math:`0`.

document/core/exec/instructions.rst

@@ -695,6 +695,9 @@ Memory Instructions
      (\iff n > 1) \\
    \end{array}
 
+.. note::
+   The use of the :math:`\vconst_t` meta function in the rules for this and the following instructions ensures that an overflowing index turns into a :ref:`trap <syntax-trap>`.
+
 
 .. _exec-memory.init:
 
@@ -711,11 +714,11 @@ Memory Instructions
 
 5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[\X{ma}]`.
 
-6. Assert: due to :ref:`validation <valid-data.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.
+6. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.
 
 7. Let :math:`\X{da}` be the :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.
 
-8. Assert: due to :ref:`validation <valid-data.init>`, :math:`S.\SDATA[\X{da}]` exists.
+8. Assert: due to :ref:`validation <valid-memory.init>`, :math:`S.\SDATA[\X{da}]` exists.
 
 9. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[\X{da}]`.
 
@@ -813,11 +816,11 @@ Memory Instructions
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-data.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.
+2. Assert: due to :ref:`validation <valid-data.drop>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.
 
 3. Let :math:`a` be the :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.
 
-4. Assert: due to :ref:`validation <valid-data.init>`, :math:`S.\SDATA[a]` exists.
+4. Assert: due to :ref:`validation <valid-data.drop>`, :math:`S.\SDATA[a]` exists.
 
 5. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[a]`.
 
@@ -941,7 +944,7 @@ Memory Instructions
    \begin{array}{lcl@{\qquad}l}
    S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\MEMORYCOPY &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
-     (\I32.\CONST~(dst+cnt-1))~(\I32.\CONST~(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\
+     (\vconst_\I32(dst+cnt-1))~(\vconst_\I32(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\
      (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\
      \end{array} \\
    \end{array}
@@ -1072,11 +1075,11 @@ Table Instructions
 
 5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[\X{ta}]`.
 
-6. Assert: due to :ref:`validation <valid-elem.init>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.
+6. Assert: due to :ref:`validation <valid-table.init>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.
 
 7. Let :math:`\X{ea}` be the :ref:`element address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[x]`.
 
-8. Assert: due to :ref:`validation <valid-elem.init>`, :math:`S.\SELEM[\X{ea}]` exists.
+8. Assert: due to :ref:`validation <valid-table.init>`, :math:`S.\SELEM[\X{ea}]` exists.
 
 9. Let :math:`\X{elem}^?` be the optional :ref:`element instance <syntax-eleminst>` :math:`S.\SELEM[\X{ea}]`.
 
@@ -1174,11 +1177,11 @@ Table Instructions
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-elem.init>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.
+2. Assert: due to :ref:`validation <valid-elem.drop>`, :math:`F.\AMODULE.\MIELEMS[x]` exists.
 
 3. Let :math:`a` be the :ref:`element address <syntax-elemaddr>` :math:`F.\AMODULE.\MIELEMS[x]`.
 
-4. Assert: due to :ref:`validation <valid-elem.init>`, :math:`S.\SELEM[a]` exists.
+4. Assert: due to :ref:`validation <valid-elem.drop>`, :math:`S.\SELEM[a]` exists.
 
 5. Let :math:`\X{elem}^?` be the optional :ref:`elem instance <syntax-eleminst>` :math:`S.\SELEM[a]`.