[spec] Specify instantiate (#114)

Incorporate active/passive segments into instantiation. While doing so, drop the notion of segment types as well as initelem/initdata administrative instructions and express the latter in terms of table.init and memory.init instructions. Adjust interpreter accordingly.

Author: rossberg

document/core/appendix/index-rules.rst

@@ -25,10 +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 : \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:`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`

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

@@ -321,7 +321,7 @@ Element Section
 ~~~~~~~~~~~~~~~
 
 The *element section* has the id 9.
-It decodes into a vector of :ref:`element segments <syntax-elem>` that represent the |MELEM| component of a :ref:`module <syntax-module>`.
+It decodes into a vector of :ref:`element segments <syntax-elem>` that represent the |MELEMS| component of a :ref:`module <syntax-module>`.
 
 .. math::
    \begin{array}{llclll}
@@ -354,7 +354,7 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
    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>`
+   imported in a single module, so all valid :ref:`active <syntax-elem>`
    element segments have a |ETABLE| value of :math:`0`.
 
    Additional element kinds may be added in future versions of WebAssembly.
@@ -429,7 +429,7 @@ Data Section
 ~~~~~~~~~~~~
 
 The *data section* has the id 11.
-It decodes into a vector of :ref:`data segments <syntax-data>` that represent the |MDATA| component of a :ref:`module <syntax-module>`.
+It decodes into a vector of :ref:`data segments <syntax-data>` that represent the |MDATAS| component of a :ref:`module <syntax-module>`.
 
 .. math::
    \begin{array}{llclll}
@@ -450,7 +450,7 @@ It decodes into a vector of :ref:`data segments <syntax-data>` that represent th
    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
+   imported in a single module, so all valid :ref:`active <syntax-data>` data
    segments have a |DMEM| value of :math:`0`.
 
 
@@ -543,8 +543,8 @@ Furthermore, it must be present if any :math:`data index <syntax-dataidx>` occur
        \MTABLES~\table^\ast, \\
        \MMEMS~\mem^\ast, \\
        \MGLOBALS~\global^\ast, \\
-       \MELEM~\elem^\ast, \\
-       \MDATA~\data^m, \\
+       \MELEMS~\elem^\ast, \\
+       \MDATAS~\data^m, \\
        \MSTART~\start^?, \\
        \MIMPORTS~\import^\ast, \\
        \MEXPORTS~\export^\ast ~\} \\