Merge pull request WebAssembly#247 from ioannad/merge-upstream-spec

Merge upstream spec

.github/workflows/main.yml

@@ -21,6 +21,17 @@ jobs:
       - run: opam install --yes ocamlbuild.0.14.0
       - run: cd interpreter && opam exec make all
 
+  ref-interpreter-js-library:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Setup OCaml
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: 4.12.x
+      - run: opam install --yes ocamlbuild.0.14.0 ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
+      - run: cd interpreter && opam exec make wast.js
+
   build-js-api-spec:
     runs-on: ubuntu-latest
     steps:
@@ -52,7 +63,7 @@ jobs:
       - 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
-      - run: pip install sphinx==4.0.0
+      - run: pip install sphinx==5.1.0
       - run: cd document/core && make all
       - uses: actions/upload-artifact@v2
         with:

document/README.md

@@ -3,9 +3,9 @@
 This directory contains the source code for the WebAssembly spec documents, as served from the [webassembly.github.io/spec](https://webassembly.github.io/spec) pages.
 It uses [Sphinx](http://www.sphinx-doc.org/) and [Bikeshed](https://github.com/tabatkins/bikeshed).
 
-To install Sphinx:
+To install Sphinx (and required library six):
 ```
-pip install sphinx
+pip install sphinx six
 ```
 
 To install Bikeshed, see the instructions [here](https://tabatkins.github.io/bikeshed/#installing).
@@ -42,7 +42,7 @@ pipenv shell
 Install Python dependencies:
 
 ```
-pipenv install Sphinx==4.0.0
+pipenv install Sphinx==4.0.0 six
 ```
 
 ### Checking out the repository

document/core/appendix/algorithm.rst

@@ -140,6 +140,8 @@ The type of the :ref:`label <syntax-label>` associated with a control frame is e
 
 Finally, the current frame can be marked as unreachable.
 In that case, all existing operand types are purged from the value stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_val` to take effect.
+Because every function has an implicit outermost label that corresponds to an implicit block frame,
+it is an invariant of the validation algorithm that there always is at least one frame on the control stack when validating an instruction, and hence, `ctrls[0]` is always defined.
 
 .. note::
    Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.

document/core/appendix/changes.rst

@@ -7,7 +7,7 @@ Change History
 Since the original release 1.0 of the WebAssembly specification, a number of proposals for extensions have been integrated.
 The following sections provide an overview of what has changed.
 
-Release 1.1
+Release 2.0
 ~~~~~~~~~~~
 
 .. index:: instruction, integer

document/core/appendix/custom.rst

@@ -36,7 +36,7 @@ Each subsection consists of a
 
 * a one-byte subsection *id*,
 * the |U32| *size* of the contents, in bytes,
-* the actual *contents*, whose structure is depended on the subsection id.
+* the actual *contents*, whose structure is dependent on the subsection id.
 
 .. math::
    \begin{array}{llcll}

document/core/appendix/embedding.rst

@@ -33,7 +33,7 @@ Failure of an interface operation is indicated by an auxiliary syntactic class:
 
 .. math::
    \begin{array}{llll}
-   \production{(error)} & \error &::=& \ERROR \\
+   \production{error} & \error &::=& \ERROR \\
    \end{array}
 
 In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific :ref:`implementation limitations <impl>` are reached.
@@ -50,7 +50,7 @@ Some operations state *pre-conditions* about their arguments or *post-conditions
 It is the embedder's responsibility to meet the pre-conditions.
 If it does, the post conditions are guaranteed by the semantics.
 
-In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects <syntax-runtime>` (:math:`store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses <syntax-addr>`):
+In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects <syntax-runtime>` (:math:`\store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses <syntax-addr>`):
 
 * Every runtime object passed as a parameter must be :ref:`valid <valid-store>` per an implicit pre-condition.
 
@@ -258,7 +258,7 @@ Functions
 :math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)`
 ...........................................................................
 
-1. Pre-condition: :math:`\functype` is :math:`valid <valid-functype>`.
+1. Pre-condition: :math:`\functype` is :ref:`valid <valid-functype>`.
 
 2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function <alloc-func>` in :math:`\store` with :ref:`function type <syntax-functype>` :math:`\functype` and host function code :math:`\hostfunc`.
 
@@ -326,7 +326,7 @@ Tables
 :math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr, \reff)`
 ..........................................................................
 
-1. Pre-condition: :math:`\tabletype` is :math:`valid <valid-tabletype>`.
+1. Pre-condition: :math:`\tabletype` is :ref:`valid <valid-tabletype>`.
 
 2. Let :math:`\tableaddr` be the result of :ref:`allocating a table <alloc-table>` in :math:`\store` with :ref:`table type <syntax-tabletype>` :math:`\tabletype` and initialization value :math:`\reff`.
 
@@ -345,7 +345,7 @@ Tables
 
 1. Return :math:`S.\STABLES[a].\TITYPE`.
 
-2. Post-condition: the returned :ref:`table type <syntax-tabletype>` is :math:`valid <valid-tabletype>`.
+2. Post-condition: the returned :ref:`table type <syntax-tabletype>` is :ref:`valid <valid-tabletype>`.
 
 .. math::
    \begin{array}{lclll}
@@ -438,7 +438,7 @@ Memories
 :math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)`
 ................................................................
 
-1. Pre-condition: :math:`\memtype` is :math:`valid <valid-memtype>`.
+1. Pre-condition: :math:`\memtype` is :ref:`valid <valid-memtype>`.
 
 2. Let :math:`\memaddr` be the result of :ref:`allocating a memory <alloc-mem>` in :math:`\store` with :ref:`memory type <syntax-memtype>` :math:`\memtype`.
 
@@ -457,7 +457,7 @@ Memories
 
 1. Return :math:`S.\SMEMS[a].\MITYPE`.
 
-2. Post-condition: the returned :ref:`memory type <syntax-memtype>` is :math:`valid <valid-memtype>`.
+2. Post-condition: the returned :ref:`memory type <syntax-memtype>` is :ref:`valid <valid-memtype>`.
 
 .. math::
    \begin{array}{lclll}
@@ -573,7 +573,7 @@ Globals
 :math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)`
 ............................................................................
 
-1. Pre-condition: :math:`\globaltype` is :math:`valid <valid-globaltype>`.
+1. Pre-condition: :math:`\globaltype` is :ref:`valid <valid-globaltype>`.
 
 2. Let :math:`\globaladdr` be the result of :ref:`allocating a global <alloc-global>` in :math:`\store` with :ref:`global type <syntax-globaltype>` :math:`\globaltype` and initialization value :math:`\val`.
 
@@ -592,7 +592,7 @@ Globals
 
 1. Return :math:`S.\SGLOBALS[a].\GITYPE`.
 
-2. Post-condition: the returned :ref:`global type <syntax-globaltype>` is :math:`valid <valid-globaltype>`.
+2. Post-condition: the returned :ref:`global type <syntax-globaltype>` is :ref:`valid <valid-globaltype>`.
 
 .. math::
    \begin{array}{lclll}