[spec] DataCount section, syntax, and validation (#80)

The data count section has a count that must match the number of data segments. If the data count section isn't present, then `memory.init` and `data.drop` cannot be used.

Fixes issue #73.

Author: binji

document/core/binary/modules.rst

@@ -84,22 +84,23 @@ In these cases, the empty result :math:`\epsilon` is interpreted as the empty ve
 
 The following section ids are used:
 
-==  ========================================
-Id  Section                                 
-==  ========================================
- 0  :ref:`custom section <binary-customsec>`
- 1  :ref:`type section <binary-typesec>`    
- 2  :ref:`import section <binary-importsec>`
- 3  :ref:`function section <binary-funcsec>`
- 4  :ref:`table section <binary-tablesec>`  
- 5  :ref:`memory section <binary-memsec>`   
- 6  :ref:`global section <binary-globalsec>`
- 7  :ref:`export section <binary-exportsec>`
- 8  :ref:`start section <binary-startsec>`  
- 9  :ref:`element section <binary-elemsec>` 
-10  :ref:`code section <binary-codesec>`    
-11  :ref:`data section <binary-datasec>`    
-==  ========================================
+==  ===============================================
+Id  Section                                        
+==  ===============================================
+ 0  :ref:`custom section <binary-customsec>`       
+ 1  :ref:`type section <binary-typesec>`           
+ 2  :ref:`import section <binary-importsec>`       
+ 3  :ref:`function section <binary-funcsec>`       
+ 4  :ref:`table section <binary-tablesec>`         
+ 5  :ref:`memory section <binary-memsec>`          
+ 6  :ref:`global section <binary-globalsec>`       
+ 7  :ref:`export section <binary-exportsec>`       
+ 8  :ref:`start section <binary-startsec>`         
+ 9  :ref:`element section <binary-elemsec>`        
+10  :ref:`code section <binary-codesec>`           
+11  :ref:`data section <binary-datasec>`           
+12  :ref:`data count section <binary-datacountsec>`
+==  ===============================================
 
 
 .. index:: ! custom section
@@ -433,6 +434,32 @@ It decodes into a vector of :ref:`data segments <syntax-data>` that represent th
    segments have a |DMEM| value of :math:`0`.
 
 
+.. index:: ! data count section, data count, data segment
+   pair: binary format; data count
+   pair: section; data count
+.. _binary-datacountsec:
+
+Data Count Section
+~~~~~~~~~~~~~~~~~~
+
+The *data count section* has the id 12.
+It decodes into an optional :ref:`u32 <syntax-uint>` that represents the number of :ref:`data segments <syntax-data>` in the :ref:`data section <binary-datasec>`. If this count does not match the length of the data segment vector, the module is malformed.
+
+.. math::
+   \begin{array}{llclll}
+   \production{data count section} & \Bdatacountsec &::=&
+     \X{n}^?{:}\Bsection_{12}(\Bu32) &\Rightarrow& \X{n}^? \\
+   \end{array}
+
+.. note::
+   The data count section is used to simplify single-pass validation. Since the
+   data section occurs after the code section, the :math:`\MEMORYINIT` and
+   :math:`\DATADROP` instructions would not be able to check whether the data
+   segment index is valid until the data section is read. The data count section
+   occurs before the code section, so a single-pass validator can use this count
+   instead of deferring validation.
+
+
 .. index:: module, section, type definition, function type, function, table, memory, global, element, data, start function, import, export, context, version
    pair: binary format; module
 .. _binary-magic:
@@ -450,6 +477,8 @@ The preamble is followed by a sequence of :ref:`sections <binary-section>`.
 while other sections must occur at most once and in the prescribed order.
 All sections can be empty.
 The lengths of vectors produced by the (possibly empty) :ref:`function <binary-funcsec>` and :ref:`code <binary-codesec>` section must match up.
+Similarly, the data count must match the length of the :ref:`data segment <binary-datasec>` vector.
+The :math:`\MEMORYINIT` and :math:`\DATADROP` instructions can only be used if the data count section is present.
 
 .. math::
    \begin{array}{llcllll}
@@ -479,9 +508,11 @@ The lengths of vectors produced by the (possibly empty) :ref:`function <binary-f
      \Bcustomsec^\ast \\ &&&
      \elem^\ast{:\,}\Belemsec \\ &&&
      \Bcustomsec^\ast \\ &&&
+     m^?{:\,}\Bdatacountsec \\ &&&
+     \Bcustomsec^\ast \\ &&&
      \X{code}^n{:\,}\Bcodesec \\ &&&
      \Bcustomsec^\ast \\ &&&
-     \data^\ast{:\,}\Bdatasec \\ &&&
+     \data^{\X{m'}}{:\,}\Bdatasec \\ &&&
      \Bcustomsec^\ast
      \quad\Rightarrow\quad \{~
        \begin{array}[t]{@{}l@{}}
@@ -491,10 +522,14 @@ The lengths of vectors produced by the (possibly empty) :ref:`function <binary-f
        \MMEMS~\mem^\ast, \\
        \MGLOBALS~\global^\ast, \\
        \MELEM~\elem^\ast, \\
-       \MDATA~\data^\ast, \\
+       \MDATA~\data^{\X{m'}}, \\
        \MSTART~\start^?, \\
        \MIMPORTS~\import^\ast, \\
        \MEXPORTS~\export^\ast ~\} \\
+      \end{array} \\ &&&
+     (\begin{array}[t]{@{}c@{~}l@{}}
+      \iff & m^? \neq \epsilon \\
+      \vee & \forall (t^\ast, e) \in \X{code}^n, \MEMORYINIT \notin e \wedge \DATADROP \notin e) \\
       \end{array} \\
    \end{array}
 
@@ -503,6 +538,14 @@ where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`,
 .. math::
    \func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} ) \\
 
+and where,
+
+.. math::
+   \begin{array}{lcl@{\qquad}l}
+   \X{m'} &=& m & (\iff m^? \neq \epsilon) \\
+   \X{m'} &=& 0 & (\otherwise)
+   \end{array}
+
 .. note::
    The version of the WebAssembly binary format may increase in the future
    if backward-incompatible changes have to be made to the format.

document/core/util/macros.def

@@ -503,6 +503,7 @@
 .. |Belemsec| mathdef:: \xref{binary/modules}{binary-elemsec}{\B{elemsec}}
 .. |Bdatasec| mathdef:: \xref{binary/modules}{binary-datasec}{\B{datasec}}
 .. |Bstartsec| mathdef:: \xref{binary/modules}{binary-startsec}{\B{startsec}}
+.. |Bdatacountsec| mathdef:: \xref{binary/modules}{binary-datacountsec}{\B{datacountsec}}
 
 .. |Bcustom| mathdef:: \xref{binary/modules}{binary-customsec}{\B{custom}}
 .. |Btype| mathdef:: \xref{binary/modules}{binary-typedef}{\B{type}}

document/core/valid/instructions.rst

@@ -357,7 +357,7 @@ Table Instructions
    \frac{
      C.\CELEM[x] = \segtype
    }{
-     C \vdashinstr \DATADROP~x : [] \to []
+     C \vdashinstr \ELEMDROP~x : [] \to []
    }
 
 
@@ -548,8 +548,6 @@ Memory Instructions
 
 * The data segment :math:`C.\CDATA[x]` must be defined in the context.
 
-* The :ref:`segment type <syntax-segtype>` :math:`C.\CDATA[x]` must be |SPASSIVE|.
-
 * Then the instruction is valid with type :math:`[] \to []`.
 
 .. math::