Merge from upstream spec

.github/workflows/main.yml

@@ -19,7 +19,11 @@ jobs:
         with:
           ocaml-compiler: 4.12.x
       - run: opam install --yes ocamlbuild.0.14.0
-      - run: cd interpreter && opam exec make all
+      - name: Setup Node.js
+        uses: actions/setup-node@v1
+        with:
+          node-version: 18.x
+      - run: cd interpreter && opam exec make JS=node all
 
   ref-interpreter-js-library:
     runs-on: ubuntu-latest
@@ -60,6 +64,9 @@ jobs:
       - uses: actions/checkout@v2
         with:
           submodules: "recursive"
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16
       - run: pip install bikeshed && bikeshed update
       - run: pip install six
       - run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended

document/core/appendix/gen-index-instructions.py

@@ -427,10 +427,10 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\V128.\LOAD\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{55}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'),
     Instruction(r'\V128.\LOAD\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{56}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'),
     Instruction(r'\V128.\LOAD\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{57}', r'[\I32~\V128] \to [\V128]', r'valid-load-lane', r'exec-load-lane'),
-    Instruction(r'\V128.\STORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to [\V128]', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{8\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{58}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
+    Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
     Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
     Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
     Instruction(r'\F32X4.\VDEMOTE\K{\_f64x2\_zero}', r'\hex{FD}~~\hex{5E}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-demote'),

document/core/appendix/index-instructions.rst

@@ -367,10 +367,10 @@ Instruction                                        Binary Opcode
 :math:`\V128.\LOAD\K{16\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{55}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-load-lane>`            :ref:`execution <exec-load-lane>`                                 
 :math:`\V128.\LOAD\K{32\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{56}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-load-lane>`            :ref:`execution <exec-load-lane>`                                 
 :math:`\V128.\LOAD\K{64\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{57}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-load-lane>`            :ref:`execution <exec-load-lane>`                                 
-:math:`\V128.\STORE\K{8\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{58}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
-:math:`\V128.\STORE\K{16\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{59}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
-:math:`\V128.\STORE\K{32\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5A}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
-:math:`\V128.\STORE\K{64\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5B}`            :math:`[\I32~\V128] \to [\V128]`               :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{8\_lane}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{58}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{16\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{59}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{32\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5A}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
+:math:`\V128.\STORE\K{64\_lane}~\memarg~\laneidx`  :math:`\hex{FD}~~\hex{5B}`            :math:`[\I32~\V128] \to []`                    :ref:`validation <valid-store-lane>`           :ref:`execution <exec-store-lane>`                                
 :math:`\V128.\LOAD\K{32\_zero}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{5C}`            :math:`[\I32] \to [\V128]`                     :ref:`validation <valid-load-zero>`            :ref:`execution <exec-load-zero>`                                 
 :math:`\V128.\LOAD\K{64\_zero}~\memarg~\laneidx`   :math:`\hex{FD}~~\hex{5D}`            :math:`[\I32] \to [\V128]`                     :ref:`validation <valid-load-zero>`            :ref:`execution <exec-load-zero>`                                 
 :math:`\F32X4.\VDEMOTE\K{\_f64x2\_zero}`           :math:`\hex{FD}~~\hex{5E}`            :math:`[\V128] \to [\V128]`                    :ref:`validation <valid-vcvtop>`               :ref:`execution <exec-vcvtop>`, :ref:`operator <op-demote>`       

document/core/conf.py

@@ -297,7 +297,8 @@
   'pointsize': '10pt',
 
    # Additional stuff for the LaTeX preamble.
-   'preamble': '',
+   # Don't type-set cross references with emphasis.
+   'preamble': '\\renewcommand\\sphinxcrossref[1]{#1}\n',
 
    # Latex figure (float) alignment
   'figure_align': 'htbp',

document/core/exec/instructions.rst

@@ -394,7 +394,7 @@ Most vector instructions are defined in terms of generic numeric operators appli
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\V128\K{.}\SWIZZLE &\stepto& (\V128\K{.}\VCONST~c')
+   (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\I8X16\K{.}\SWIZZLE &\stepto& (\V128\K{.}\VCONST~c')
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -431,7 +431,7 @@ Most vector instructions are defined in terms of generic numeric operators appli
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\V128\K{.}\SHUFFLE~x^\ast &\stepto& (\V128\K{.}\VCONST~c)
+   (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\I8X16\K{.}\SHUFFLE~x^\ast &\stepto& (\V128\K{.}\VCONST~c)
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -1312,7 +1312,7 @@ Table Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
+   S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
    \end{array}
    \end{array}
 
@@ -2244,7 +2244,7 @@ Memory Instructions
    S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n)~\MEMORYFILL
      \quad\stepto\quad S; F; \TRAP
      \\ \qquad
-     (\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|)
+     (\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|)
    \\[1ex]
    S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~0)~\MEMORYFILL
      \quad\stepto\quad S; F; \epsilon
@@ -2451,7 +2451,7 @@ Memory Instructions
      \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & s + n > |S.\SDATAS[F.\AMODULE.\MIDATAS[x]].\DIDATA| \\
-      \vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\[1ex]
+      \vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|) \\[1ex]
      \end{array}
    \\[1ex]
    S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x)
@@ -3143,15 +3143,13 @@ Invocation of :ref:`function address <syntax-funcaddr>` :math:`a`
 
 7. Pop the values :math:`\val^n` from the stack.
 
-8. Let :math:`\val_0^\ast` be the list of zero values of types :math:`t^\ast`.
-
-9. Let :math:`F` be the :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`.
+8. Let :math:`F` be the :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~f.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`.
 
-10. Push the activation of :math:`F` with arity :math:`m` to the stack.
+9. Push the activation of :math:`F` with arity :math:`m` to the stack.
 
-11. Let :math:`L` be the :ref:`label <syntax-label>` whose arity is :math:`m` and whose continuation is the end of the function.
+10. Let :math:`L` be the :ref:`label <syntax-label>` whose arity is :math:`m` and whose continuation is the end of the function.
 
-12. :ref:`Enter <exec-instr-seq-enter>` the instruction sequence :math:`\instr^\ast` with label :math:`L`.
+11. :ref:`Enter <exec-instr-seq-enter>` the instruction sequence :math:`\instr^\ast` with label :math:`L`.
 
 .. math::
    ~\\[-1ex]

document/core/exec/modules.rst

@@ -495,8 +495,7 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
 
    a. Let :math:`\limits_i~t_i` be the :ref:`table type <syntax-tabletype>` :math:`\table_i.\TTYPE`.
 
-   b. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` :math:`\table_i.\TTYPE`
-   with initialization value :math:`\REFNULL~t_i`.
+   b. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` :math:`\table_i.\TTYPE` with initialization value :math:`\REFNULL~t_i`.
 
 4. For each :ref:`memory <syntax-mem>` :math:`\mem_i` in :math:`\module.\MMEMS`, do:
 

document/core/exec/runtime.rst

@@ -510,17 +510,15 @@ Intuitively, :math:`\instr^\ast` is the *continuation* to execute when the branc
 
    When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.
 
-Activations and Frames
-......................
+Activation Frames
+.................
 
 Activation frames carry the return arity :math:`n` of the respective function,
 hold the values of its :ref:`locals <syntax-local>` (including arguments) in the order corresponding to their static :ref:`local indices <syntax-localidx>`,
 and a reference to the function's own :ref:`module instance <syntax-moduleinst>`:
 
 .. math::
    \begin{array}{llll}
-   \production{activation} & \X{activation} &::=&
-     \FRAME_n\{\frame\} \\
    \production{frame} & \frame &::=&
      \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\
    \end{array}

document/core/static/custom.css

@@ -44,6 +44,8 @@ div.admonition p.admonition-title {
 div.math {
   background-color: #F0F0F0;
   padding: 3px 0 3px 0;
+  overflow-x: auto;
+  overflow-y: hidden;
 }
 
 div.relations {

document/core/syntax/conventions.rst

@@ -20,7 +20,7 @@ Grammar Notation
 
 The following conventions are adopted in defining grammar rules for abstract syntax.
 
-* Terminal symbols (atoms) are written in sans-serif font: :math:`\K{i32}, \K{end}`.
+* Terminal symbols (atoms) are written in sans-serif font or in symbolic form: :math:`\K{i32}, \K{end}, {\to}, [, ]`.
 
 * Nonterminal symbols are written in italic font: :math:`\X{valtype}, \X{instr}`.
 

document/core/syntax/instructions.rst

@@ -45,7 +45,7 @@ These operations closely match respective operations available in hardware.
    \production{signedness} & \sx &::=&
      \K{u} ~|~ \K{s} \\
    \production{instruction} & \instr &::=&
-     \K{i}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-int}{\iX{\X{nn}}} ~|~
+     \K{i}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-int}{\uX{\X{nn}}} ~|~
      \K{f}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-float}{\fX{\X{nn}}} \\&&|&
      \K{i}\X{nn}\K{.}\iunop ~|~
      \K{f}\X{nn}\K{.}\funop \\&&|&

document/core/text/instructions.rst

@@ -34,6 +34,8 @@ The following grammar handles the corresponding update to the :ref:`identifier c
    \production{label} & \Tlabel_I &::=&
      v{:}\Tid &\Rightarrow& \{\ILABELS~v\} \compose I
        & (\iff v \notin I.\ILABELS) \\ &&|&
+     v{:}\Tid &\Rightarrow& \{\ILABELS~v\} \compose (I \with \ILABELS[i] = \epsilon)
+       & (\iff I.\ILABELS[i] = v) \\ &&|&
      \epsilon &\Rightarrow& \{\ILABELS~(\epsilon)\} \compose I \\
    \end{array}
 
@@ -42,6 +44,9 @@ The following grammar handles the corresponding update to the :ref:`identifier c
    This effectively shifts all existing labels up by one,
    mirroring the fact that control instructions are indexed relatively not absolutely.
 
+   If a label with the same name already exists,
+   then it is shadowed and the earlier label becomes inaccessible.
+
 
 .. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism, tag index, exception instructions
    pair: text format; instruction
@@ -175,7 +180,7 @@ Reference Instructions
    \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|&
      \text{ref.null}~~t{:}\Theaptype &\Rightarrow& \REFNULL~t \\ &&|&
      \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|&
-     \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|&
+     \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\
    \end{array}
 
 
@@ -901,7 +906,7 @@ Vector constant instructions have a mandatory :ref:`shape <syntax-vec-shape>` de
      \text{f64x2.convert\_low\_i32x4\_s} &\Rightarrow& \F64X2.\VCONVERT\K{\_low\_i32x4\_s}\\  &&|&
      \text{f64x2.convert\_low\_i32x4\_u} &\Rightarrow& \F64X2.\VCONVERT\K{\_low\_i32x4\_u}\\ &&|&
      \text{f32x4.demote\_f64x2\_zero} &\Rightarrow& \F32X4.\VDEMOTE\K{\_f64x2\_zero}\\ &&|&
-     \text{f64x2.promote\_low\_f32x4} &\Rightarrow& \F64X2.\VPROMOTE\K{\_low\_f32x4}\\ &&|&
+     \text{f64x2.promote\_low\_f32x4} &\Rightarrow& \F64X2.\VPROMOTE\K{\_low\_f32x4}\\
    \end{array}
 
 

document/core/text/lexical.rst

@@ -48,7 +48,7 @@ The character stream in the source text is divided, from left to right, into a s
      \text{(} ~|~ \text{)} ~|~ \Treserved \\
    \production{keyword} & \Tkeyword &::=&
      (\text{a} ~|~ \dots ~|~ \text{z})~\Tidchar^\ast
-     \qquad (\mbox{if occurring as a literal terminal in the grammar}) \\
+     \qquad (\iff~\mbox{occurring as a literal terminal in the grammar}) \\
    \production{reserved} & \Treserved &::=&
      (\Tidchar ~|~ \Tstring)^+ \\
    \end{array}

document/core/text/modules.rst

@@ -112,7 +112,7 @@ If inline declarations are given, then their types must match the referenced :re
         \end{array} \\
    \end{array}
 
-The synthesized attribute of a |Ttypeuse| is a pair consisting of both the used :ref:`type index <syntax-typeidx>` and the updated :ref:`identifier context <text-context>` including possible parameter identifiers.
+The synthesized attribute of a |Ttypeuse| is a pair consisting of both the used :ref:`type index <syntax-typeidx>` and the local :ref:`identifier context <text-context>` containing possible parameter identifiers.
 The following auxiliary function extracts optional identifiers from parameters:
 
 .. math::
@@ -206,7 +206,7 @@ Function definitions can bind a symbolic :ref:`function identifier <text-id>`, a
      \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~~
      (t{:}\Tlocal)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad
        \Rightarrow\quad \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\X{in}^\ast~\END \} \\ &&& \qquad\qquad\qquad
-       (\iff I'' = I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex]
+       (\iff I'' = I \compose I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex]
    \production{local} & \Tlocal &::=&
      \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype~\text{)}
        \quad\Rightarrow\quad t \\