[spec] Fix minor errors and inconsistencies

document/core/appendix/properties.rst

@@ -237,7 +237,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 :ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}`
 ......................................................................................
 
-* The :ref:`memory type <syntax-memtype>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-memtype>`.
+* The :ref:`memory type <syntax-memtype>` :math:`\limits` must be :ref:`valid <valid-memtype>`.
 
 * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.
 

document/core/exec/instructions.rst

@@ -1256,7 +1256,7 @@ Table Instructions
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; F; \TABLESIZE~x &\stepto& S; F; (\I32.\CONST~\X{sz})
+   S; F; (\TABLESIZE~x) &\stepto& S; F; (\I32.\CONST~\X{sz})
    \end{array}
    \\ \qquad
      (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\
@@ -1288,19 +1288,21 @@ Table Instructions
 
 10. Pop the value :math:`\val` from the stack.
 
-11. Either, try :ref:`growing <grow-table>` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`:
+11. Let :math:`\X{err}` be the |i32| value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`.
+
+12. Either, try :ref:`growing <grow-table>` :math:`\X{table}` by :math:`n` entries with initialization value :math:`\val`:
 
    a. If it succeeds, push the value :math:`\I32.\CONST~\X{sz}` to the stack.
 
-   b. Else, push the value :math:`\I32.\CONST~(-1)` to the stack.
+   b. Else, push the value :math:`\I32.\CONST~\X{err}` to the stack.
 
-12. Or, push the value :math:`\I32.\CONST~(-1)` to the stack.
+13. Or, push the value :math:`\I32.\CONST~\X{err}` to the stack.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; F; \val~(\I32.\CONST~n)~\TABLEGROW~x &\stepto& S'; F; (\I32.\CONST~\X{sz})
+   S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\I32.\CONST~\X{sz})
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -1310,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~{-1})
+   S; F; (\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1))
    \end{array}
    \end{array}
 
@@ -1511,7 +1513,7 @@ Table Instructions
      \quad\stepto
      \\ \qquad S; F;
        \begin{array}[t]{@{}l@{}}
-       (\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~(\TABLEGET~y)~(\TABLESET~x) \\
+       (\I32.\CONST~d+n)~(\I32.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\
        (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\
        \end{array}
      \\ \qquad
@@ -1722,7 +1724,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(t.\LOAD({N}\K{\_}\sx)^?~\memarg) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~\memarg) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -1783,7 +1785,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~\memarg) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~\memarg) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -1840,7 +1842,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_splat}~\memarg) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~\memarg) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -1895,7 +1897,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(\V128.\LOAD{N}\K{\_zero}~\memarg) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~\memarg) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -1957,7 +1959,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -2034,7 +2036,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(t.\CONST~c)~(t.\STORE{N}^?~\memarg) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~\memarg) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -2091,7 +2093,7 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~k)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP
+   S; F; (\I32.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~\memarg~x) &\stepto& S; F; \TRAP
    \end{array}
    \\ \qquad
      (\otherwise) \\
@@ -2368,8 +2370,8 @@ Memory Instructions
      \quad\stepto
      \\ \qquad S; F;
        \begin{array}[t]{@{}l@{}}
-       (\I32.\CONST~d+n-1) \\
-       (\I32.\CONST~s+n-1)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\
+       (\I32.\CONST~d+n) \\
+       (\I32.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\
        (\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\
        (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY \\
        \end{array}
@@ -2679,7 +2681,7 @@ Control Instructions
 :math:`\BRTABLE~l^\ast~l_N`
 ...........................
 
-1. Assert: due to :ref:`validation <valid-br-table>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-br_table>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
 
 2. Pop the value :math:`\I32.\CONST~i` from the stack.
 
@@ -2858,22 +2860,22 @@ Exiting :math:`\instr^\ast` with label :math:`L`
 
 When the end of a block is reached without a jump or trap aborting it, then the following steps are performed.
 
-1. Let :math:`m` be the number of values on the top of the stack.
+1. Let :math:`n` be the number of values on the top of the stack.
 
-2. Pop the values :math:`\val^m` from the stack.
+2. Pop the values :math:`\val^n` from the stack.
 
-3. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack.
+3. Assert: due to :ref:`validation <valid-instr-seq>`, the label :math:`L` is now on the top of the stack and has arity :math:`n`.
 
 4. Pop the label from the stack.
 
-5. Push :math:`\val^m` back to the stack.
+5. Push :math:`\val^n` back to the stack.
 
 6. Jump to the position after the |END| of the :ref:`structured control instruction <syntax-instr-control>` associated with the label :math:`L`.
 
 .. math::
    ~\\[-1ex]
    \begin{array}{lcl@{\qquad}l}
-   \LABEL_n\{\instr^\ast\}~\val^m~\END &\stepto& \val^m
+   \LABEL_n\{\instr^\ast\}~\val^n~\END &\stepto& \val^n
    \end{array}
 
 .. note::

document/core/exec/runtime.rst

@@ -30,18 +30,18 @@ or *external references* pointing to an uninterpreted form of :ref:`extern addre
 
 .. math::
    \begin{array}{llcl}
-   \production{(number)} & \num &::=&
+   \production{number} & \num &::=&
      \I32.\CONST~\i32 \\&&|&
      \I64.\CONST~\i64 \\&&|&
      \F32.\CONST~\f32 \\&&|&
      \F64.\CONST~\f64 \\
-   \production{(vector)} & \vecc &::=&
+   \production{vector} & \vecc &::=&
      \V128.\CONST~\i128 \\
-   \production{(reference)} & \reff &::=&
+   \production{reference} & \reff &::=&
      \REFNULL~t \\&&|&
      \REFFUNCADDR~\funcaddr \\&&|&
      \REFEXTERNADDR~\externaddr \\
-   \production{(value)} & \val &::=&
+   \production{value} & \val &::=&
      \num ~|~ \vecc ~|~ \reff \\
    \end{array}
 
@@ -79,7 +79,7 @@ It is either a sequence of :ref:`values <syntax-val>` or a :ref:`trap <syntax-tr
 
 .. math::
    \begin{array}{llcl}
-   \production{(result)} & \result &::=&
+   \production{result} & \result &::=&
      \val^\ast \\&&|&
      \TRAP
    \end{array}
@@ -101,7 +101,7 @@ Syntactically, the store is defined as a :ref:`record <notation-record>` listing
 
 .. math::
    \begin{array}{llll}
-   \production{(store)} & \store &::=& \{~
+   \production{store} & \store &::=& \{~
      \begin{array}[t]{l@{~}ll}
      \SFUNCS & \funcinst^\ast, \\
      \STABLES & \tableinst^\ast, \\
@@ -157,21 +157,21 @@ In addition, an :ref:`embedder <embedder>` may supply an uninterpreted set of *h
 
 .. math::
    \begin{array}{llll}
-   \production{(address)} & \addr &::=&
+   \production{address} & \addr &::=&
      0 ~|~ 1 ~|~ 2 ~|~ \dots \\
-   \production{(function address)} & \funcaddr &::=&
+   \production{function address} & \funcaddr &::=&
      \addr \\
-   \production{(table address)} & \tableaddr &::=&
+   \production{table address} & \tableaddr &::=&
      \addr \\
-   \production{(memory address)} & \memaddr &::=&
+   \production{memory address} & \memaddr &::=&
      \addr \\
-   \production{(global address)} & \globaladdr &::=&
+   \production{global address} & \globaladdr &::=&
      \addr \\
-   \production{(element address)} & \elemaddr &::=&
+   \production{element address} & \elemaddr &::=&
      \addr \\
-   \production{(data address)} & \dataaddr &::=&
+   \production{data address} & \dataaddr &::=&
      \addr \\
-   \production{(extern address)} & \externaddr &::=&
+   \production{extern address} & \externaddr &::=&
      \addr \\
    \end{array}
 
@@ -204,7 +204,7 @@ and collects runtime representations of all entities that are imported, defined,
 
 .. math::
    \begin{array}{llll}
-   \production{(module instance)} & \moduleinst &::=& \{
+   \production{module instance} & \moduleinst &::=& \{
      \begin{array}[t]{l@{~}ll}
      \MITYPES & \functype^\ast, \\
      \MIFUNCS & \funcaddr^\ast, \\
@@ -238,10 +238,10 @@ The module instance is used to resolve references to other definitions during ex
 
 .. math::
    \begin{array}{llll}
-   \production{(function instance)} & \funcinst &::=&
+   \production{function instance} & \funcinst &::=&
      \{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \} \\ &&|&
      \{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \} \\
-   \production{(host function)} & \hostfunc &::=& \dots \\
+   \production{host function} & \hostfunc &::=& \dots \\
    \end{array}
 
 A *host function* is a function expressed outside WebAssembly but passed to a :ref:`module <syntax-module>` as an :ref:`import <syntax-import>`.
@@ -268,7 +268,7 @@ It records its :ref:`type <syntax-tabletype>` and holds a vector of :ref:`refere
 
 .. math::
    \begin{array}{llll}
-   \production{(table instance)} & \tableinst &::=&
+   \production{table instance} & \tableinst &::=&
      \{ \TITYPE~\tabletype, \TIELEM~\vec(\reff) \} \\
    \end{array}
 
@@ -292,7 +292,7 @@ It records its :ref:`type <syntax-memtype>` and holds a vector of :ref:`bytes <s
 
 .. math::
    \begin{array}{llll}
-   \production{(memory instance)} & \meminst &::=&
+   \production{memory instance} & \meminst &::=&
      \{ \MITYPE~\memtype, \MIDATA~\vec(\byte) \} \\
    \end{array}
 
@@ -316,7 +316,7 @@ It records its :ref:`type <syntax-globaltype>` and holds an individual :ref:`val
 
 .. math::
    \begin{array}{llll}
-   \production{(global instance)} & \globalinst &::=&
+   \production{global instance} & \globalinst &::=&
      \{ \GITYPE~\globaltype, \GIVALUE~\val \} \\
    \end{array}
 
@@ -338,7 +338,7 @@ It holds a vector of references and their common :ref:`type <syntax-reftype>`.
 
 .. math::
   \begin{array}{llll}
-  \production{(element instance)} & \eleminst &::=&
+  \production{element instance} & \eleminst &::=&
     \{ \EITYPE~\reftype, \EIELEM~\vec(\reff) \} \\
   \end{array}
 
@@ -356,7 +356,7 @@ It holds a vector of :ref:`bytes <syntax-byte>`.
 
 .. math::
   \begin{array}{llll}
-  \production{(data instance)} & \datainst &::=&
+  \production{data instance} & \datainst &::=&
     \{ \DIDATA~\vec(\byte) \} \\
   \end{array}
 
@@ -374,7 +374,7 @@ It defines the export's :ref:`name <syntax-name>` and the associated :ref:`exter
 
 .. math::
    \begin{array}{llll}
-   \production{(export instance)} & \exportinst &::=&
+   \production{export instance} & \exportinst &::=&
      \{ \EINAME~\name, \EIVALUE~\externval \} \\
    \end{array}
 
@@ -392,7 +392,7 @@ It is an :ref:`address <syntax-addr>` denoting either a :ref:`function instance
 
 .. math::
    \begin{array}{llcl}
-   \production{(external value)} & \externval &::=&
+   \production{external value} & \externval &::=&
      \EVFUNC~\funcaddr \\&&|&
      \EVTABLE~\tableaddr \\&&|&
      \EVMEM~\memaddr \\&&|&
@@ -456,7 +456,7 @@ Labels carry an argument arity :math:`n` and their associated branch *target*, w
 
 .. math::
    \begin{array}{llll}
-   \production{(label)} & \label &::=&
+   \production{label} & \label &::=&
      \LABEL_n\{\instr^\ast\} \\
    \end{array}
 
@@ -485,9 +485,9 @@ and a reference to the function's own :ref:`module instance <syntax-moduleinst>`
 
 .. math::
    \begin{array}{llll}
-   \production{(activation)} & \X{activation} &::=&
+   \production{activation} & \X{activation} &::=&
      \FRAME_n\{\frame\} \\
-   \production{(frame)} & \frame &::=&
+   \production{frame} & \frame &::=&
      \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\
    \end{array}
 
@@ -529,7 +529,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
 
 .. math::
    \begin{array}{llcl}
-   \production{(administrative instruction)} & \instr &::=&
+   \production{administrative instruction} & \instr &::=&
      \dots \\ &&|&
      \TRAP \\ &&|&
      \REFFUNCADDR~\funcaddr \\ &&|&
@@ -590,9 +590,9 @@ In order to specify the reduction of :ref:`branches <syntax-instr-control>`, the
 
 .. math::
    \begin{array}{llll}
-   \production{(block contexts)} & \XB^0 &::=&
+   \production{block contexts} & \XB^0 &::=&
      \val^\ast~[\_]~\instr^\ast \\
-   \production{(block contexts)} & \XB^{k+1} &::=&
+   \production{block contexts} & \XB^{k+1} &::=&
      \val^\ast~\LABEL_n\{\instr^\ast\}~\XB^k~\END~\instr^\ast \\
    \end{array}
 
@@ -624,9 +624,9 @@ that operates relative to a current :ref:`frame <syntax-frame>` referring to the
 
 .. math::
    \begin{array}{llcl}
-   \production{(configuration)} & \config &::=&
+   \production{configuration} & \config &::=&
      \store; \thread \\
-   \production{(thread)} & \thread &::=&
+   \production{thread} & \thread &::=&
      \frame; \instr^\ast \\
    \end{array}
 
@@ -645,7 +645,7 @@ Finally, the following definition of *evaluation context* and associated structu
 
 .. math::
    \begin{array}{llll}
-   \production{(evaluation contexts)} & E &::=&
+   \production{evaluation contexts} & E &::=&
      [\_] ~|~
      \val^\ast~E~\instr^\ast ~|~
      \LABEL_n\{\instr^\ast\}~E~\END \\