[spec] Simplify datacount side condition (#83)

* Add definition of free index sets
* Simplify datacount side condition
* Explain convention about multiple occurrences of meta variables

Author: rossberg

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/modules.rst

@@ -476,9 +476,11 @@ The preamble is followed by a sequence of :ref:`sections <binary-section>`.
 :ref:`Custom sections <binary-customsec>` may be inserted at any place in this sequence,
 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.
+
+Similarly, the optional data count must match the length of the :ref:`data segment <binary-datasec>` vector.
+Furthermore, it must be present if any :math:`data index <syntax-dataidx>` occurs in the code section.
 
 .. math::
    \begin{array}{llcllll}
@@ -512,7 +514,7 @@ The :math:`\MEMORYINIT` and :math:`\DATADROP` instructions can only be used if t
      \Bcustomsec^\ast \\ &&&
      \X{code}^n{:\,}\Bcodesec \\ &&&
      \Bcustomsec^\ast \\ &&&
-     \data^{\X{m'}}{:\,}\Bdatasec \\ &&&
+     \data^m{:\,}\Bdatasec \\ &&&
      \Bcustomsec^\ast
      \quad\Rightarrow\quad \{~
        \begin{array}[t]{@{}l@{}}
@@ -522,30 +524,19 @@ The :math:`\MEMORYINIT` and :math:`\DATADROP` instructions can only be used if t
        \MMEMS~\mem^\ast, \\
        \MGLOBALS~\global^\ast, \\
        \MELEM~\elem^\ast, \\
-       \MDATA~\data^{\X{m'}}, \\
+       \MDATA~\data^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} \\ &&&
+     (\iff m^? \neq \epsilon \vee \freedataidx(\X{code}^n) = \emptyset) \\
    \end{array}
 
 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/syntax/conventions.rst

@@ -41,6 +41,9 @@ The following conventions are adopted in defining grammar rules for abstract syn
 
 * Some productions are augmented with side conditions in parentheses, ":math:`(\iff \X{condition})`", that 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, then all those occurrences must have the same instantiation.
+  (This is a shorthand for a side condition requiring multiple different variables to be equal.)
+
 
 .. _notation-epsilon:
 .. _notation-length:
@@ -82,6 +85,7 @@ Moreover, the following conventions are employed:
   (similarly for :math:`x^\ast`, :math:`x^+`, :math:`x^?`).
   This implicitly expresses a form of mapping syntactic constructions over a sequence.
 
+
 Productions of the following form are interpreted as *records* that map a fixed set of fields :math:`\K{field}_i` to "values" :math:`A_i`, respectively:
 
 .. math::

document/core/syntax/modules.rst

@@ -81,22 +81,36 @@ Each class of definition has its own *index space*, as distinguished by the foll
 The index space for :ref:`functions <syntax-func>`, :ref:`tables <syntax-table>`, :ref:`memories <syntax-mem>` and :ref:`globals <syntax-global>` includes respective :ref:`imports <syntax-import>` declared in the same module.
 The indices of these imports precede the indices of other definitions in the same index space.
 
-Element indices reference :ref:`element segments <syntax-elem>`.
-
-Data indices reference :ref:`data segments <syntax-data>`.
+Element indices reference :ref:`element segments <syntax-elem>` and data indices reference :ref:`data segments <syntax-data>`.
 
 The index space for :ref:`locals <syntax-local>` is only accessible inside a :ref:`function <syntax-func>` and includes the parameters of that function, which precede the local variables.
 
 Label indices reference :ref:`structured control instructions <syntax-instr-control>` inside an instruction sequence.
 
 
+.. _free-typeidx:
+.. _free-funcidx:
+.. _free-tableidx:
+.. _free-memidx:
+.. _free-globalidx:
+.. _free-elemidx:
+.. _free-dataidx:
+.. _free-localidx:
+.. _free-labelidx:
+.. _free-index:
+
 Conventions
 ...........
 
 * The meta variable :math:`l` ranges over label indices.
 
 * The meta variables :math:`x, y` range over indices in any of the other index spaces.
 
+* The notation :math:`\F{idx}(A)` denotes the set of indices from index space :math:`\X{idx}` occurring free in :math:`A`.
+
+.. note::
+   For example, if :math:`\instr^\ast` is :math:`(\DATADROP~x) (\MEMORYINIT~y)`, then :math:`\freedataidx(\instr^\ast) = \{x, y\}`.
+
 
 .. index:: ! type definition, type index, function type
    pair: abstract syntax; type definition

document/core/text/conventions.rst

@@ -54,6 +54,8 @@ In order to distinguish symbols of the textual syntax from symbols of the abstra
 
 * 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.
+
 .. _text-syntactic:
 
 * A distinction is made between *lexical* and *syntactic* productions. For the latter, arbitrary :ref:`white space <text-space>` is allowed in any place where the grammar contains spaces. The productions defining :ref:`lexical syntax <text-lexical>` and the syntax of :Ref:`values <text-value>` are considered lexical, all others are syntactic.

document/core/util/macros.def

@@ -226,6 +226,19 @@
 .. |labelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\X{labelidx}}
 
 
+.. Indices, meta functions
+
+.. |freetypeidx| mathdef:: \xref{syntax/modules}{syntax-typeidx}{\F{typeidx}}
+.. |freefuncidx| mathdef:: \xref{syntax/modules}{syntax-funcidx}{\F{funcidx}}
+.. |freetableidx| mathdef:: \xref{syntax/modules}{syntax-tableidx}{\F{tableidx}}
+.. |freememidx| mathdef:: \xref{syntax/modules}{syntax-memidx}{\F{memidx}}
+.. |freeglobalidx| mathdef:: \xref{syntax/modules}{syntax-globalidx}{\F{globalidx}}
+.. |freeelemidx| mathdef:: \xref{syntax/modules}{syntax-elemidx}{\F{elemidx}}
+.. |freedataidx| mathdef:: \xref{syntax/modules}{syntax-dataidx}{\F{dataidx}}
+.. |freelocalidx| mathdef:: \xref{syntax/modules}{syntax-localidx}{\F{localidx}}
+.. |freelabelidx| mathdef:: \xref{syntax/modules}{syntax-labelidx}{\F{labelidx}}
+
+
 .. Modules, terminals
 
 .. |MTYPES| mathdef:: \xref{syntax/modules}{syntax-module}{\K{types}}