[spec] Address comments by Luke (#752)

Author: rossberg

document/core/intro/introduction.rst

@@ -5,7 +5,7 @@ WebAssembly (abbreviated Wasm [#wasm]_) is a *safe, portable, low-level code for
 designed for efficient execution and compact representation.
 Its main goal is to enable high performance applications on the Web, but it does not make any Web-specific assumptions or provide Web-specific features, so it can be employed in other environments as well.
 
-WebAssembly is an open standard developed by a `W3C Community Group <https://www.w3.org/community/webassembly/>`_ that includes representatives of all major browser vendors.
+WebAssembly is an open standard developed by a `W3C Community Group <https://www.w3.org/community/webassembly/>`_.
 
 This document describes version |release| of the :ref:`core <scope>` WebAssembly standard.
 It is intended that it will be superseded by new incremental releases with additional features in the future.

document/core/syntax/conventions.rst

@@ -41,9 +41,13 @@ The following conventions are adopted in defining grammar rules for abstract syn
 
 
 
+.. _notation-epsilon:
+.. _notation-length:
+.. _notation-index:
 .. _notation-slice:
 .. _notation-replace:
 .. _notation-record:
+.. _notation-project:
 .. _notation-concat:
 .. _notation-compose:
 

document/core/syntax/types.rst

@@ -49,7 +49,7 @@ Result Types
 ~~~~~~~~~~~~
 
 *Result types* classify the result of :ref:`executing <exec-instr>` :ref:`instructions <syntax-instr>` or :ref:`blocks <syntax-instr-control>`,
-which is a sequence of values.
+which is a sequence of values written with brackets.
 
 .. math::
    \begin{array}{llll}
@@ -71,7 +71,7 @@ Function Types
 ~~~~~~~~~~~~~~
 
 *Function types* classify the signature of :ref:`functions <syntax-func>`,
-mapping a vector of parameters to a vector of results.
+mapping a vector of parameters to a vector of results, written as follows.
 
 .. math::
    \begin{array}{llll}

document/core/text/modules.rst

@@ -476,9 +476,8 @@ When omitted, :math:`\T{0}` is assumed.
 .. math::
    \begin{array}{llclll}
    \production{element segment} & \Telem_I &::=&
-     \text{(}~\text{elem}~~(x{:}\Ttableidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
-       \Rightarrow\quad \{ \ETABLE~x', \EOFFSET~e, \EINIT~y^\ast \} \\
-       &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\
+     \text{(}~\text{elem}~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
+       \Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\
    \end{array}
 
 .. note::
@@ -498,6 +497,16 @@ As an abbreviation, a single instruction may occur in place of the offset:
      \text{(}~\text{offset}~~\Tinstr~\text{)}
    \end{array}
 
+Also, the table index can be omitted, defaulting to :math:`0`.
+
+.. math::
+   \begin{array}{llclll}
+   \production{element segment} &
+    \text{(}~\text{elem}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
+       &\equiv&
+     \text{(}~\text{elem}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
+   \end{array}
+
 As another abbreviation, element segments may also be specified inline with :ref:`table <text-table>` definitions; see the respective section.
 
 
@@ -518,9 +527,8 @@ The data is written as a :ref:`string <text-string>`, which may be split up into
 .. math::
    \begin{array}{llclll}
    \production{data segment} & \Tdata_I &::=&
-     \text{(}~\text{data}~~(x{:}\Tmemidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad
-       \Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\
-       &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\[1ex]
+     \text{(}~\text{data}~~x{:}\Tmemidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad
+       \Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\[1ex]
    \production{data string} & \Tdatastring &::=&
      (b^\ast{:}\Tstring)^\ast \quad\Rightarrow\quad \concat((b^\ast)^\ast) \\
    \end{array}
@@ -542,6 +550,16 @@ As an abbreviation, a single instruction may occur in place of the offset:
      \text{(}~\text{offset}~~\Tinstr~\text{)}
    \end{array}
 
+Also, the memory index can be omitted, defaulting to :math:`0`.
+
+.. math::
+   \begin{array}{llclll}
+   \production{data segment} &
+    \text{(}~\text{data}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
+       &\equiv&
+     \text{(}~\text{data}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
+   \end{array}
+
 As another abbreviation, data segments may also be specified inline with :ref:`memory <text-mem>` definitions; see the respective section.
 
 

document/core/valid/conventions.rst

@@ -40,14 +40,14 @@ which collects relevant information about the surrounding :ref:`module <syntax-m
 * *Globals*: the list of globals declared in the current module, represented by their global type.
 * *Locals*: the list of locals declared in the current function (including parameters), represented by their value type.
 * *Labels*: the stack of labels accessible from the current position, represented by their result type.
-* *Return*: the return type of the current function, represented as a result type.
+* *Return*: the return type of the current function, represented as an optional result type that is absent when no return is allowed, as in free-standing expressions.
 
 In other words, a context contains a sequence of suitable :ref:`types <syntax-type>` for each :ref:`index space <syntax-index>`,
 describing each defined entry in that space.
 Locals, labels and return type are only used for validating :ref:`instructions <syntax-instr>` in :ref:`function bodies <syntax-func>`, and are left empty elsewhere.
 The label stack is the only part of the context that changes as validation of an instruction sequence proceeds.
 
-It is convenient to define contexts as :ref:`records <notation-record>` :math:`C` with abstract syntax:
+More concretely, contexts are defined as :ref:`records <notation-record>` :math:`C` with abstract syntax:
 
 .. math::
    \begin{array}{llll}
@@ -64,22 +64,18 @@ It is convenient to define contexts as :ref:`records <notation-record>` :math:`C
      \end{array}
    \end{array}
 
-.. note::
-   The fields of a context are not defined as :ref:`vectors <syntax-vec>`,
-   since their lengths are not bounded by the maximum vector size.
+.. _notation-extend:
 
-In addition to field access :math:`C.\K{field}` the following notation is adopted for manipulating contexts:
+In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts:
 
 * When spelling out a context, empty fields are omitted.
 
 * :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence.
 
 .. note::
-   This notation is defined to *prepend* not *append*.
-   It is only used in situations where the original :math:`C.\K{field}` is either empty
-   or :math:`\K{field}` is :math:`\K{labels}`.
-   In the latter case adding to the front is desired
-   because the :ref:`label index <syntax-labelidx>` space is indexed relatively, that is, in reverse order of addition.
+   We use :ref:`indexing notation <notation-index>` like :math:`C.\CLABELS[i]` to look up indices in their respective :ref:`index space <syntax-index>` in the context.
+   Context extension notation :math:`C,\K{field}\,A` is primarily used to locally extend *relative* index spaces, such as :ref:`label indices <syntax-labelidx>`.
+   Accordingly, the notation is defined to append at the *front* of the respective sequence, introducing a new relative index :math:`0` and shifting the existing ones.
 
 
 .. _valid-notation-textual:

document/core/valid/instructions.rst

@@ -314,7 +314,7 @@ Memory Instructions
 
 * The memory :math:`C.\CMEMS[0]` must be defined in the context.
 
-* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width <syntax-valtype>` of :math:`t` divided by :math:`8`.
 
 * Then the instruction is valid with type :math:`[\I32] \to [t]`.
 
@@ -354,7 +354,7 @@ Memory Instructions
 
 * The memory :math:`C.\CMEMS[0]` must be defined in the context.
 
-* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`width <syntax-valtype>` of :math:`t` divided by :math:`8`.
+* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width <syntax-valtype>` of :math:`t` divided by :math:`8`.
 
 * Then the instruction is valid with type :math:`[\I32~t] \to []`.
 
@@ -483,6 +483,8 @@ Control Instructions
    }
 
 .. note::
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others.
+
    The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the block was entered.
    This may be generalized in future versions of WebAssembly.
 
@@ -507,6 +509,8 @@ Control Instructions
    }
 
 .. note::
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others.
+
    The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the loop was entered.
    This may be generalized in future versions of WebAssembly.
 
@@ -536,6 +540,8 @@ Control Instructions
    }
 
 .. note::
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others.
+
    The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the conditional was entered.
    This may be generalized in future versions of WebAssembly.
 
@@ -559,6 +565,8 @@ Control Instructions
    }
 
 .. note::
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+
    The |BR| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
 
@@ -580,6 +588,9 @@ Control Instructions
      C \vdashinstr \BRIF~l : [t^?~\I32] \to [t^?]
    }
 
+.. note::
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+
 
 .. _valid-br_table:
 
@@ -608,6 +619,8 @@ Control Instructions
    }
 
 .. note::
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l_i]` performs a relative lookup as expected.
+
    The |BRTABLE| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
 
@@ -616,7 +629,7 @@ Control Instructions
 :math:`\RETURN`
 ...............
 
-* The return type :math:`C.\CRETURN` must not be empty in the context.
+* The return type :math:`C.\CRETURN` must not be absent in the context.
 
 * Let :math:`[t^?]` be the :ref:`result type <syntax-resulttype>` of :math:`C.\CRETURN`.
 
@@ -632,8 +645,8 @@ Control Instructions
 .. note::
    The |RETURN| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
-   :math:`C.\CRETURN` is empty (:math:`\epsilon`) when validating an :ref:`expression <valid-expr>` that is not a function body.
-   This differs from it being set to the empty result type (:math:`[]`),
+   :math:`C.\CRETURN` is absent (set to :math:`\epsilon`) when validating an :ref:`expression <valid-expr>` that is not a function body.
+   This differs from it being set to the empty result type (:math:`[\epsilon]`),
    which is the case for functions not returning anything.
 
 
@@ -773,7 +786,7 @@ Constant Expressions
    \frac{
      (C \vdashinstrconst \instr \const)^\ast
    }{
-     C \vdashexprconst \instr~\END \const
+     C \vdashexprconst \instr^\ast~\END \const
    }
 
 .. math::
@@ -789,4 +802,7 @@ Constant Expressions
    }
 
 .. note::
+   Currently, constant expressions occurring as initializers of :ref:`globals <syntax-global>` are further constrained in that contained |GETGLOBAL| instructions are only allowed to refer to *imported* globals.
+   This is enforced in the :ref:`validation rule for modules <valid-module>` by constraining the context :math:`C` accordingly.
+
    The definition of constant expression may be extended in future versions of WebAssembly.