Segment refactoring (#113)

Refactor segment representation in AST (in both spec and interpreter) by separating out a `segment_mode`.

Other changes in Spec:
- Various fixes to text format grammar of segments.
- Factor out elemkind in binary format.
- Add note about possible future extension of element kinds.
- Add note about interpretation of segment kinds as bitfields.
- Fix some cross references.

Other changes in Interpreter:
- Rename {table,memory}_segment to {elem,data}_segment.
- Some rename elem to elem_expr and global.value to global.ginit for consistency with spec.
- Decode the elem segment kind as vu32 to maintain backwards compat.
- Some code simplifications / beautifications.

Author: rossberg

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/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

@@ -667,7 +667,7 @@ Memory Instructions
 
 17. Execute the instruction :math:`\MEMORYFILL`.
 
-18. Push the value :math:`\vconst_\I32(i+1)` to the stack.
+18. Push the value :math:`\vconst_{\I32}(i+1)` to the stack.
 
 19. Push the value :math:`\val` to the stack.
 
@@ -688,7 +688,7 @@ Memory Instructions
    S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n)~(\MEMORYFILL) &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
      (\I32.\CONST~i)~\val~(\I32.\CONST~1)~(\MEMORYFILL) \\
-     (\vconst_\I32(i+1))~\val~(\I32.\CONST~(n-1))~(\MEMORYFILL) \\
+     (\vconst_{\I32}(i+1))~\val~(\I32.\CONST~(n-1))~(\MEMORYFILL) \\
      \end{array} \\
    \end{array}
    \\ \qquad
@@ -711,11 +711,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}]`.
 
@@ -763,9 +763,9 @@ Memory Instructions
 
 22. Execute the instruction :math:`\MEMORYINIT~x`.
 
-23. Push the value :math:`\vconst_\I32(dst+1)` to the stack.
+23. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
 
-24. Push the value :math:`\vconst_\I32(src+1)` to the stack.
+24. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
 
 25. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
 
@@ -792,7 +792,7 @@ Memory Instructions
    S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt))~(\MEMORYINIT~x) &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
      (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~(\MEMORYINIT~x) \\
-     (\vconst_\I32(dst+1))~(\vconst_\I32(src+1))~(\I32.\CONST~(cnt-1))~(\MEMORYINIT~x) \\
+     (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~(\MEMORYINIT~x) \\
      \end{array} \\
    \end{array}
    \\ \qquad
@@ -813,11 +813,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]`.
 
@@ -890,15 +890,15 @@ Memory Instructions
 
    d. Execute the instruction :math:`\MEMORYCOPY`.
 
-   e. Push the value :math:`\vconst_\I32(dst+1)` to the stack.
+   e. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
 
-   f. Push the value :math:`\vconst_\I32(src+1)` to the stack.
+   f. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
 
 10. Else:
 
-   a. Push the value :math:`\vconst_\I32(dst+cnt-1)` to the stack.
+   a. Push the value :math:`\vconst_{\I32}(dst+cnt-1)` to the stack.
 
-   b. Push the value :math:`\vconst_\I32(src+cnt-1)` to the stack.
+   b. Push the value :math:`\vconst_{\I32}(src+cnt-1)` to the stack.
 
    c. Push the value :math:`\I32.\CONST~1` to the stack.
 
@@ -932,7 +932,7 @@ Memory Instructions
    S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\MEMORYCOPY &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
      (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~\MEMORYCOPY \\
-     (\vconst_\I32(dst+1))~(\vconst_\I32(src+1))~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\
+     (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\
      \end{array} \\
    \end{array}
    \\ \qquad
@@ -1001,15 +1001,15 @@ Table Instructions
 
    d. Execute the instruction :math:`\TABLECOPY`.
 
-   e. Push the value :math:`\vconst_\I32(dst+1)` to the stack.
+   e. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
 
-   f. Push the value :math:`\vconst_\I32(src+1)` to the stack.
+   f. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
 
 10. Else:
 
-   a. Push the value :math:`\vconst_\I32(dst+cnt-1)` to the stack.
+   a. Push the value :math:`\vconst_{\I32}(dst+cnt-1)` to the stack.
 
-   b. Push the value :math:`\vconst_\I32(src+cnt-1)` to the stack.
+   b. Push the value :math:`\vconst_{\I32}(src+cnt-1)` to the stack.
 
    c. Push the value :math:`\I32.\CONST~1` to the stack.
 
@@ -1039,7 +1039,7 @@ Table Instructions
    S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\TABLECOPY &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
      (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~\TABLECOPY \\
-     (\vconst_\I32(dst+1))~(\vconst_\I32(src+1))~(\I32.\CONST~(cnt-1))~\TABLECOPY \\
+     (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~\TABLECOPY \\
      \end{array} \\
    \end{array}
    \\ \qquad
@@ -1072,11 +1072,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}]`.
 
@@ -1124,9 +1124,9 @@ Table Instructions
 
 22. Execute the instruction :math:`\TABLEINIT~x`.
 
-23. Push the value :math:`\vconst_\I32(dst+1)` to the stack.
+23. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack.
 
-24. Push the value :math:`\vconst_\I32(src+1)` to the stack.
+24. Push the value :math:`\vconst_{\I32}(src+1)` to the stack.
 
 25. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack.
 
@@ -1153,7 +1153,7 @@ Table Instructions
    S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~(\TABLEINIT~x) &\stepto& S; F;
      \begin{array}[t]{@{}l@{}}
      (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~(\TABLEINIT~x) \\
-     (\vconst_\I32(dst+1))~(\vconst_\I32(src+1))~(\I32.\CONST~(cnt-1))~(\TABLEINIT~x) \\
+     (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~(\TABLEINIT~x) \\
      \end{array} \\
    \end{array}
    \\ \qquad
@@ -1174,11 +1174,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]`.
 

document/core/exec/modules.rst

@@ -614,6 +614,8 @@ Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals),
 Instantiation
 ~~~~~~~~~~~~~
 
+.. todo:: Adjust for passive segments.
+
 Given a :ref:`store <syntax-store>` :math:`S`, a :ref:`module <syntax-module>` :math:`\module` is instantiated with a list of :ref:`external values <syntax-externval>` :math:`\externval^n` supplying the required imports as follows.
 
 Instantiation checks that the module is :ref:`valid <valid>` and the provided imports :ref:`match <match-externtype>` the declared types,
@@ -665,55 +667,51 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
 8. Push the frame :math:`F` to the stack.
 
-9. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM`, do:
-
-    a. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating <exec-expr>` the expression :math:`\elem_i.\EOFFSET`.
+9. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM` whose :ref:`mode <syntax-elemmode>` :math:`\elem_i.\EMODE` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{eoexpr}_i \}`, do:
 
-    b. Assert: due to :ref:`validation <valid-elem>`, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`.
+    a. Assert: due to :ref:`validation <valid-elem>`, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists.
 
-    c. Let :math:`\tableidx_i` be the :ref:`table index <syntax-tableidx>` :math:`\elem_i.\ETABLE`.
+    b. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` :math:`\moduleinst.\MITABLES[\tableidx_i]`.
 
-    d. Assert: due to :ref:`validation <valid-elem>`, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists.
+    c. Assert: due to :ref:`validation <valid-elem>`, :math:`S'.\STABLES[\tableaddr_i]` exists.
 
-    e. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` :math:`\moduleinst.\MITABLES[\tableidx_i]`.
+    d. Let :math:`\tableinst_i` be the :ref:`table instance <syntax-tableinst>` :math:`S'.\STABLES[\tableaddr_i]`.
 
-    f. Assert: due to :ref:`validation <valid-elem>`, :math:`S'.\STABLES[\tableaddr_i]` exists.
+    e. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating <exec-expr>` the expression :math:`\X{eoexpr}_i`.
 
-    g. Let :math:`\tableinst_i` be the :ref:`table instance <syntax-tableinst>` :math:`S'.\STABLES[\tableaddr_i]`.
+    f. Assert: due to :ref:`validation <valid-elem>`, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`.
 
-    h. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`.
+    g. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`.
 
-    i. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then:
+    h. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then:
 
        i. Fail.
 
-10. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATA`, do:
-
-    a. Let :math:`\X{doval}_i` be the result of :ref:`evaluating <exec-expr>` the expression :math:`\data_i.\DOFFSET`.
+10. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATA` whose :ref:`mode <syntax-datamode>` :math:`\data_i.\DMODE` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{doexpr}_i \}`, do:
 
-    b. Assert: due to :ref:`validation <valid-data>`, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`.
+    a. Assert: due to :ref:`validation <valid-data>`, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists.
 
-    c. Let :math:`\memidx_i` be the :ref:`memory index <syntax-memidx>` :math:`\data_i.\DMEM`.
+    b. Let :math:`\memaddr_i` be the :ref:`memory address <syntax-memaddr>` :math:`\moduleinst.\MIMEMS[\memidx_i]`.
 
-    d. Assert: due to :ref:`validation <valid-data>`, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists.
+    c. Assert: due to :ref:`validation <valid-data>`, :math:`S'.\SMEMS[\memaddr_i]` exists.
 
-    e. Let :math:`\memaddr_i` be the :ref:`memory address <syntax-memaddr>` :math:`\moduleinst.\MIMEMS[\memidx_i]`.
+    d. Let :math:`\meminst_i` be the :ref:`memory instance <syntax-meminst>` :math:`S'.\SMEMS[\memaddr_i]`.
 
-    f. Assert: due to :ref:`validation <valid-data>`, :math:`S'.\SMEMS[\memaddr_i]` exists.
+    e. Let :math:`\X{doval}_i` be the result of :ref:`evaluating <exec-expr>` the expression :math:`\data_i.\DOFFSET`.
 
-    g. Let :math:`\meminst_i` be the :ref:`memory instance <syntax-meminst>` :math:`S'.\SMEMS[\memaddr_i]`.
+    f. Assert: due to :ref:`validation <valid-data>`, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`.
 
-    h. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`.
+    g. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`.
 
-    i. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then:
+    h. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then:
 
        i. Fail.
 
 11. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
 
 12. Pop the frame from the stack.
 
-13. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM`, do:
+13. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEM` whose :ref:`mode <syntax-elemmode>` :math:`\elem_i.\EMODE` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{eoexpr}_i \}`, do:
 
     a. For each :ref:`function index <syntax-funcidx>` :math:`\funcidx_{ij}` in :math:`\elem_i.\EINIT` (starting with :math:`j = 0`), do:
 
@@ -723,7 +721,7 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
        iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\funcaddr_{ij}`.
 
-14. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATA`, do:
+14. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATA` whose :ref:`mode <syntax-datamode>` :math:`\data_i.\DMODE` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{doexpr}_i \}`, do:
 
     a. For each :ref:`byte <syntax-byte>` :math:`b_{ij}` in :math:`\data_i.\DINIT` (starting with :math:`j = 0`), do:
 

document/core/exec/runtime.rst

@@ -314,7 +314,7 @@ Element Instances
 ~~~~~~~~~~~~~~~~~
 
 An *element instance* is the runtime representation of an :ref:`element segment <syntax-elem>`.
-Like table instances, an element instance holds a vector of function elements.
+It holds a vector of function elements.
 
 .. math::
   \begin{array}{llll}