Context extension notation

Author: rossberg

document/core/valid/conventions.rst

@@ -69,14 +69,12 @@ In addition to field access written :math:`C.\K{field}` the following notation i
 * When spelling out a context, empty fields are omitted.
   Likewise, the |CRETURN| field may be omitted when it is |NORETURN|.
 
-* :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.
+* The notation :math:`\K{field}\,A^\ast, C` 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
+   The notation for context extension 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.
+   It is reversed from usual conventions because it *prepends* not *appends*, in accordance with the use of relative indexing to look up a label in the context's label list.
 
 
 .. _valid-notation-textual:

document/core/valid/instructions.rst

@@ -477,7 +477,7 @@ Control Instructions
 
 .. math::
    \frac{
-     C,\CLABELS\,[t^?] \vdashinstrseq \instr^\ast : [] \to [t^?]
+     \CLABELS\,[t^?], C \vdashinstrseq \instr^\ast : [] \to [t^?]
    }{
      C \vdashinstr \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?]
    }
@@ -501,7 +501,7 @@ Control Instructions
 
 .. math::
    \frac{
-     C,\CLABELS\,[] \vdashinstrseq \instr^\ast : [] \to [t^?]
+     \CLABELS\,[], C \vdashinstrseq \instr^\ast : [] \to [t^?]
    }{
      C \vdashinstr \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?]
    }
@@ -528,9 +528,9 @@ Control Instructions
 
 .. math::
    \frac{
-     C,\CLABELS\,[t^?] \vdashinstrseq \instr_1^\ast : [] \to [t^?]
+     \CLABELS\,[t^?], C \vdashinstrseq \instr_1^\ast : [] \to [t^?]
      \qquad
-     C,\CLABELS\,[t^?] \vdashinstrseq \instr_2^\ast : [] \to [t^?]
+     \CLABELS\,[t^?], C \vdashinstrseq \instr_2^\ast : [] \to [t^?]
    }{
      C \vdashinstr \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?]
    }
@@ -787,4 +787,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.

document/core/valid/modules.rst

@@ -42,7 +42,7 @@ Functions :math:`\func` are classified by :ref:`function types <syntax-functype>
    \frac{
      C.\CTYPES[x] = [t_1^\ast] \to [t_2^?]
      \qquad
-     C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdashexpr \expr : [t_2^?]
+     \CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?], C \vdashexpr \expr : [t_2^?]
    }{
      C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?]
    }
@@ -454,16 +454,16 @@ Instead, the context :math:`C` for validation of the module's content is constru
   * :math:`C.\CTYPES` is :math:`\module.\MTYPES`,
 
   * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`,
-    with the import's :ref:`external types <syntax-extentype>` :math:`\X{it}^\ast` and the internal :math:`function types <syntax-functype>` :math:`\X{ft}^\ast` as determined below,
+    with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :math:`function types <syntax-functype>` :math:`\X{ft}^\ast` as determined below,
 
   * :math:`C.\CTABLES` is :math:`\ettables(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`,
-    with the import's :ref:`external types <syntax-extentype>` :math:`\X{it}^\ast` and the internal :math:`table types <syntax-tabletype>` :math:`\X{tt}^\ast` as determined below,
+    with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :math:`table types <syntax-tabletype>` :math:`\X{tt}^\ast` as determined below,
 
   * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`,
-    with the import's :ref:`external types <syntax-extentype>` :math:`\X{it}^\ast` and the internal :math:`memory types <syntax-memtype>` :math:`\X{mt}^\ast` as determined below,
+    with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :math:`memory types <syntax-memtype>` :math:`\X{mt}^\ast` as determined below,
 
   * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`,
-    with the import's :ref:`external types <syntax-extentype>` :math:`\X{it}^\ast` and the internal :math:`global types <syntax-globaltype>` :math:`\X{gt}^\ast` as determined below,
+    with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :math:`global types <syntax-globaltype>` :math:`\X{gt}^\ast` as determined below,
 
   * :math:`C.\CLOCALS` is empty,