Rebase on bulk proposal (WebAssembly#65)

Lots of merge conflicts to resolve. I hope I didn't screw up...

README.md

@@ -9,7 +9,9 @@ It is meant for discussion, prototype specification and implementation of a prop
 
 * See the [modified spec](https://webassembly.github.io/reference-types/core/) for details.
 
-Original `README` from upstream repository follows...
+The repository is now based on the [bulk operations proposal](proposals/bulk-memory-operations/Overview.md) and includes all respective changes.
+
+Original README from upstream repository follows...
 
 # spec
 

document/core/appendix/index-rules.rst

@@ -27,7 +27,9 @@ Construct                                        Judgement
 :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:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode \ok`
 :ref:`Data segment <valid-data>`                 :math:`C \vdashdata \data \ok`
+:ref:`Data mode <valid-datamode>`                :math:`C \vdashdatamode \datamode \ok`
 :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`
@@ -52,6 +54,8 @@ Construct                                        Judgement
 :ref:`Table instance <valid-tableinst>`          :math:`S \vdashtableinst \tableinst : \tabletype`
 :ref:`Memory instance <valid-meminst>`           :math:`S \vdashmeminst \meminst : \memtype`
 :ref:`Global instance <valid-globalinst>`        :math:`S \vdashglobalinst \globalinst : \globaltype`
+:ref:`Element instance <valid-eleminst>`         :math:`S \vdasheleminst \eleminst \ok`
+:ref:`Data instance <valid-datainst>`            :math:`S \vdashdatainst \datainst \ok`
 :ref:`Export instance <valid-exportinst>`        :math:`S \vdashexportinst \exportinst \ok`
 :ref:`Module instance <valid-moduleinst>`        :math:`S \vdashmoduleinst \moduleinst : C`
 :ref:`Store <valid-store>`                       :math:`\vdashstore \store \ok`
@@ -97,6 +101,8 @@ Construct                                        Judgement
 :ref:`Table instance <extend-tableinst>`         :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2`
 :ref:`Memory instance <extend-meminst>`          :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2`
 :ref:`Global instance <extend-globalinst>`       :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2`
+:ref:`Element instance <extend-eleminst>`         :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2`
+:ref:`Data instance <extend-datainst>`           :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2`
 :ref:`Store <extend-store>`                      :math:`\vdashstoreextends \store_1 \extendsto \store_2`
 ===============================================  ===============================================================================
 

document/core/appendix/properties.rst

@@ -87,6 +87,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * Each :ref:`global instance <syntax-globalinst>` :math:`\globalinst_i` in :math:`S.\SGLOBALS` must be :ref:`valid <valid-globalinst>` with some  :ref:`global type <syntax-globaltype>` :math:`\globaltype_i`.
 
+* Each :ref:`element instance <syntax-eleminst>` :math:`\eleminst_i` in :math:`S.\SELEMS` must be :ref:`valid <valid-eleminst>`.
+
+* Each :ref:`data instance <syntax-datainst>` :math:`\datainst_i` in :math:`S.\SDATAS` must be :ref:`valid <valid-datainst>`.
+
 * Then the store is valid.
 
 .. math::
@@ -101,11 +105,17 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
      \qquad
      (S \vdashglobalinst \globalinst : \globaltype)^\ast
      \\
+     (S \vdasheleminst \eleminst \ok)^\ast
+     \qquad
+     (S \vdashdatainst \datainst \ok)^\ast
+     \\
      S = \{
        \SFUNCS~\funcinst^\ast,
        \STABLES~\tableinst^\ast,
        \SMEMS~\meminst^\ast,
-       \SGLOBALS~\globalinst^\ast \}
+       \SGLOBALS~\globalinst^\ast,
+       \SELEMS~\eleminst^\ast,
+       \SDATAS~\datainst^\ast \}
      \end{array}
    }{
      \vdashstore S \ok
@@ -203,7 +213,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`.
 
-* For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the table elements :math:`\reff^n`:
+* For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the table's elements :math:`\reff^n`:
 
   * The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with some :ref:`reference type <syntax-reftype>` :math:`t'_i`.
 
@@ -273,6 +283,47 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
    }
 
 
+.. index:: element instance, reference
+.. _valid-eleminst:
+
+.. todo:: TODO: adjust elem instances
+
+:ref:`Element Instances <syntax-eleminst>` :math:`\{ \EIELEM~\X{fa}^\ast \}`
+............................................................................
+
+* For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the elements :math:`\reff^n`:
+
+  * The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with some :ref:`reference type <syntax-reftype>` :math:`t'_i`.
+
+  * The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.
+
+* Then the table instance is valid.
+
+.. math::
+   \frac{
+     (S \vdash \reff : t')^\ast
+     \qquad
+     (\vdashreftypematch t' \matchesvaltype t)^n
+   }{
+     S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok
+   }
+
+
+.. index:: data instance, byte
+.. _valid-datainst:
+
+:ref:`Data Instances <syntax-eleminst>` :math:`\{ \DIDATA~b^\ast \}`
+....................................................................
+
+* The data instance is valid.
+
+.. math::
+   \frac{
+   }{
+     S \vdashdatainst \{ \DIDATA~b^\ast \} \ok
+   }
+
+
 .. index:: external type, export instance, name, external value
 .. _valid-exportinst:
 
@@ -307,6 +358,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * For each :ref:`global address <syntax-globaladdr>` :math:`\globaladdr_i` in :math:`\moduleinst.\MIGLOBALS`, the :ref:`external value <syntax-externval>` :math:`\EVGLOBAL~\globaladdr_i` must be :ref:`valid <valid-externval-global>` with some :ref:`external type <syntax-externtype>` :math:`\ETGLOBAL~\globaltype_i`.
 
+* For each :ref:`element address <syntax-elemaddr>` :math:`\elemaddr_i` in :math:`\moduleinst.\MIELEMS`, the :ref:`element instance <syntax-eleminst>` :math:`S.\SELEMS[\elemaddr_i]` must be :ref:`valid <valid-eleminst>`.
+
+* 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>`.
+
 * Each :ref:`export instance <syntax-exportinst>` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` must be :ref:`valid <valid-exportinst>`.
 
 * For each :ref:`export instance <syntax-exportinst>` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS`, the :ref:`name <syntax-name>` :math:`\exportinst_i.\EINAME` must be different from any other name occurring in :math:`\moduleinst.\MIEXPORTS`.
@@ -335,6 +390,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
      \qquad
      (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast
      \\
+     (S \vdasheleminst S.\SELEMS[\elemaddr] \ok)^\ast
+     \qquad
+     (S \vdashdatainst S.\SDATAS[\dataaddr] \ok)^\ast
+     \\
      (S \vdashexportinst \exportinst \ok)^\ast
      \qquad
      (\exportinst.\EINAME)^\ast ~\mbox{disjoint}
@@ -346,7 +405,9 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
        \MIFUNCS & \funcaddr^\ast, \\
        \MITABLES & \tableaddr^\ast, \\
        \MIMEMS & \memaddr^\ast, \\
-       \MIGLOBALS & \globaladdr^\ast \\
+       \MIGLOBALS & \globaladdr^\ast, \\
+       \MIELEMS & \elemaddr^\ast, \\
+       \MIDATAS & \dataaddr^\ast, \\
        \MIEXPORTS & \exportinst^\ast ~\} : \{
          \begin{array}[t]{@{}l@{~}l@{}}
          \CTYPES & \functype^\ast, \\
@@ -524,54 +585,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`
@@ -647,6 +660,10 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
 
 * The length of :math:`S.\SGLOBALS` must not shrink.
 
+* The length of :math:`S.\SELEMS` must not shrink.
+
+* The length of :math:`S.\SDATAS` must not shrink.
+
 * For each :ref:`function instance <syntax-funcinst>` :math:`\funcinst_i` in the original :math:`S.\SFUNCS`, the new function instance must be an :ref:`extension <extend-funcinst>` of the old.
 
 * For each :ref:`table instance <syntax-tableinst>` :math:`\tableinst_i` in the original :math:`S.\STABLES`, the new table instance must be an :ref:`extension <extend-tableinst>` of the old.
@@ -655,21 +672,31 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
 
 * For each :ref:`global instance <syntax-globalinst>` :math:`\globalinst_i` in the original :math:`S.\SGLOBALS`, the new global instance must be an :ref:`extension <extend-globalinst>` of the old.
 
+* For each :ref:`element instance <syntax-eleminst>` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new global instance must be an :ref:`extension <extend-eleminst>` of the old.
+
+* For each :ref:`data instance <syntax-datainst>` :math:`\datainst_i` in the original :math:`S.\SDATAS`, the new global instance must be an :ref:`extension <extend-datainst>` of the old.
+
 .. math::
    \frac{
      \begin{array}{@{}ccc@{}}
      S_1.\SFUNCS = \funcinst_1^\ast &
      S_2.\SFUNCS = {\funcinst'_1}^\ast~\funcinst_2^\ast &
-     (\funcinst_1 \extendsto \funcinst'_1)^\ast \\
+     (\vdashfuncinstextends \funcinst_1 \extendsto \funcinst'_1)^\ast \\
      S_1.\STABLES = \tableinst_1^\ast &
      S_2.\STABLES = {\tableinst'_1}^\ast~\tableinst_2^\ast &
-     (\tableinst_1 \extendsto \tableinst'_1)^\ast \\
+     (\vdashtableinstextends \tableinst_1 \extendsto \tableinst'_1)^\ast \\
      S_1.\SMEMS = \meminst_1^\ast &
      S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast &
-     (\meminst_1 \extendsto \meminst'_1)^\ast \\
+     (\vdashmeminstextends \meminst_1 \extendsto \meminst'_1)^\ast \\
      S_1.\SGLOBALS = \globalinst_1^\ast &
      S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast &
-     (\globalinst_1 \extendsto \globalinst'_1)^\ast \\
+     (\vdashglobalinstextends \globalinst_1 \extendsto \globalinst'_1)^\ast \\
+     S_1.\SELEMS = \eleminst_1^\ast &
+     S_2.\SELEMS = {\eleminst'_1}^\ast~\eleminst_2^\ast &
+     (\vdasheleminstextends \eleminst_1 \extendsto \eleminst'_1)^\ast \\
+     S_1.\SDATAS = \datainst_1^\ast &
+     S_2.\SDATAS = {\datainst'_1}^\ast~\datainst_2^\ast &
+     (\vdashdatainstextends \datainst_1 \extendsto \datainst'_1)^\ast \\
      \end{array}
    }{
      \vdashstoreextends S_1 \extendsto S_2
@@ -747,6 +774,38 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
    }
 
 
+.. index:: element instance
+.. _extend-eleminst:
+
+:ref:`Element Instance <syntax-eleminst>` :math:`\eleminst`
+...........................................................
+
+* The vector :math:`\eleminst.\EIELEM` must either remain unchanged or shrink to length :math:`0`.
+
+.. math::
+   \frac{
+     \X{fa}_1^\ast = \X{fa}_2^\ast \vee \X{fa}_2^\ast = \epsilon
+   }{
+     \vdasheleminstextends \{\EIELEM~\X{fa}_1^\ast\} \extendsto \{\EIELEM~\X{fa}_2^\ast\}
+   }
+
+
+.. index:: data instance
+.. _extend-datainst:
+
+:ref:`Data Instance <syntax-datainst>` :math:`\datainst`
+........................................................
+
+* The vector :math:`\datainst.\DIDATA` must either remain unchanged or shrink to length :math:`0`.
+
+.. math::
+   \frac{
+     b_1^\ast = b_2^\ast \vee b_2^\ast = \epsilon
+   }{
+     \vdashdatainstextends \{\DIDATA~b_1^\ast\} \extendsto \{\DIDATA~b_2^\ast\}
+   }
+
+
 
 .. index:: ! preservation, ! progress, soundness, configuration, thread, terminal configuration, instantiation, invocation, validity, module
 .. _soundness-statement:

document/core/binary/conventions.rst

@@ -59,6 +59,9 @@ In order to distinguish symbols of the binary syntax from symbols of the abstrac
 
 * Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases.
 
+* If the same meta variable or non-terminal symbol appears multiple times in a production (in the syntax or in an attribute), then all those occurrences must have the same instantiation.
+  (This is a shorthand for a side condition requiring multiple different variables to be equal.)
+
 .. note::
    For example, the :ref:`binary grammar <binary-valtype>` for :ref:`value types <syntax-valtype>` is given as follows:
 

document/core/binary/instructions.rst

@@ -135,17 +135,19 @@ Variable Instructions
 .. index:: table instruction, table index
    pair: binary format; instruction
 .. _binary-instr-table:
-
-Table Instructions
-~~~~~~~~~~~~~~~~~~
-
-:ref:`Table instructions <syntax-instr-table>` are represented by either single byte or two byte codes.
-
 .. _binary-table.get:
 .. _binary-table.set:
 .. _binary-table.size:
 .. _binary-table.grow:
 .. _binary-table.fill:
+.. _binary-table.copy:
+.. _binary-table.init:
+.. _binary-elem.drop:
+
+Table Instructions
+~~~~~~~~~~~~~~~~~~
+
+:ref:`Table instructions <syntax-instr-table>` are represented by either single byte or two byte codes.
 
 .. math::
    \begin{array}{llclll}
@@ -155,6 +157,9 @@ Table Instructions
      \hex{FC}~\hex{0F}~~x{:}\Btableidx &\Rightarrow& \TABLEGROW~x \\ &&|&
      \hex{FC}~\hex{10}~~x{:}\Btableidx &\Rightarrow& \TABLESIZE~x \\ &&|&
      \hex{FC}~\hex{11}~~x{:}\Btableidx &\Rightarrow& \TABLEFILL~x \\
+     \hex{FC}~\hex{0C}~~\hex{00}~x{:}\Belemidx &\Rightarrow& \TABLEINIT~x \\ &&|&
+     \hex{FC}~\hex{0D}~~x{:}\Belemidx &\Rightarrow& \ELEMDROP~x \\ &&|&
+     \hex{FC}~\hex{0E}~~\hex{00}~~\hex{00} &\Rightarrow& \TABLECOPY \\
    \end{array}
 
 
@@ -174,6 +179,10 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
 .. _binary-storen:
 .. _binary-memory.size:
 .. _binary-memory.grow:
+.. _binary-memory.fill:
+.. _binary-memory.copy:
+.. _binary-memory.init:
+.. _binary-data.drop:
 
 .. math::
    \begin{array}{llclll}
@@ -204,11 +213,15 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
      \hex{3D}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{16}~m \\ &&|&
      \hex{3E}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{32}~m \\ &&|&
      \hex{3F}~~\hex{00} &\Rightarrow& \MEMORYSIZE \\ &&|&
-     \hex{40}~~\hex{00} &\Rightarrow& \MEMORYGROW \\
+     \hex{40}~~\hex{00} &\Rightarrow& \MEMORYGROW \\ &&|&
+     \hex{FC}~\hex{08}~~\hex{00}~x{:}\Bdataidx &\Rightarrow& \MEMORYINIT~x \\ &&|&
+     \hex{FC}~\hex{09}~~x{:}\Bdataidx &\Rightarrow& \DATADROP~x \\ &&|&
+     \hex{FC}~\hex{0A}~~\hex{00}~~\hex{00} &\Rightarrow& \MEMORYCOPY \\ &&|&
+     \hex{FC}~\hex{0B}~~\hex{00} &\Rightarrow& \MEMORYFILL \\
    \end{array}
 
 .. note::
-   In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |MEMORYSIZE| and |MEMORYGROW| instructions may be used to index additional memories.
+   In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |MEMORYSIZE|, |MEMORYGROW|, |MEMORYCOPY|, and |MEMORYFILL| instructions may be used to index additional memories.
 
 
 .. index:: numeric instruction