diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index db83ae26be..b2995f2f15 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -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 ` (:math:`store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses `): +In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects ` (:math:`\store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses `): * Every runtime object passed as a parameter must be :ref:`valid ` 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 `. +1. Pre-condition: :math:`\functype` is :ref:`valid `. 2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function ` in :math:`\store` with :ref:`function type ` :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 `. +1. Pre-condition: :math:`\tabletype` is :ref:`valid `. 2. Let :math:`\tableaddr` be the result of :ref:`allocating a table ` in :math:`\store` with :ref:`table type ` :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 ` is :math:`valid `. +2. Post-condition: the returned :ref:`table type ` is :ref:`valid `. .. 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 `. +1. Pre-condition: :math:`\memtype` is :ref:`valid `. 2. Let :math:`\memaddr` be the result of :ref:`allocating a memory ` in :math:`\store` with :ref:`memory type ` :math:`\memtype`. @@ -457,7 +457,7 @@ Memories 1. Return :math:`S.\SMEMS[a].\MITYPE`. -2. Post-condition: the returned :ref:`memory type ` is :math:`valid `. +2. Post-condition: the returned :ref:`memory type ` is :ref:`valid `. .. math:: \begin{array}{lclll} @@ -551,7 +551,7 @@ Globals :math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)` ............................................................................ -1. Pre-condition: :math:`\globaltype` is :math:`valid `. +1. Pre-condition: :math:`\globaltype` is :ref:`valid `. 2. Let :math:`\globaladdr` be the result of :ref:`allocating a global ` in :math:`\store` with :ref:`global type ` :math:`\globaltype` and initialization value :math:`\val`. @@ -570,7 +570,7 @@ Globals 1. Return :math:`S.\SGLOBALS[a].\GITYPE`. -2. Post-condition: the returned :ref:`global type ` is :math:`valid `. +2. Post-condition: the returned :ref:`global type ` is :ref:`valid `. .. math:: \begin{array}{lclll} diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index da3658c8fb..72251114e8 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -483,7 +483,7 @@ Finally, :ref:`frames ` are classified with *frame contexts*, whic * Each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` must be :ref:`valid ` with some :ref:`value type ` :math:`t_i`. -* Let :math:`t^\ast` the concatenation of all :math:`t_i` in order. +* Let :math:`t^\ast` be the concatenation of all :math:`t_i` in order. * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`value types ` :math:`t^\ast` prepended to the |CLOCALS| vector. @@ -543,7 +543,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera :math:`\REFFUNCADDR~\funcaddr` .............................. -* The :ref:`external function value ` :math:`\EVFUNC~\funcaddr` must be :ref:`valid ` with :ref:`external function type ` :math:`\ETFUNC \functype`. +* The :ref:`external function value ` :math:`\EVFUNC~\funcaddr` must be :ref:`valid ` with :ref:`external function type ` :math:`\ETFUNC~\functype`. * Then the instruction is valid with type :math:`[] \to [\FUNCREF]`. diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index f20bd0749c..e9c72b61a5 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -559,7 +559,7 @@ Furthermore, it must be present if any :ref:`data index ` occurs where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`, .. math:: - \func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} ) \\ + \func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} \\ .. note:: The version of the WebAssembly binary format may increase in the future diff --git a/document/core/exec/conventions.rst b/document/core/exec/conventions.rst index 807239b044..d9b998a923 100644 --- a/document/core/exec/conventions.rst +++ b/document/core/exec/conventions.rst @@ -92,7 +92,7 @@ and a sequence of |CONST| instructions can be interpreted as an operand "stack" (\I32.\CONST~n_1)~(\I32.\CONST~n_2)~\I32.\ADD \quad\stepto\quad (\I32.\CONST~(n_1 + n_2) \mod 2^{32}) Per this rule, two |CONST| instructions and the |ADD| instruction itself are removed from the instruction stream and replaced with one new |CONST| instruction. - This can be interpreted as popping two value off the stack and pushing the result. + This can be interpreted as popping two values off the stack and pushing the result. When no result is produced, an instruction reduces to the empty sequence: diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6ab846d281..194c39851e 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -400,7 +400,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \begin{array}[t]{@{}r@{~}l@{}} (\iff & i^\ast = \lanes_{i8x16}(c_2) \\ \wedge & c^\ast = \lanes_{i8x16}(c_1)~0^{240} \\ - \wedge & c' = \lanes^{-1}_{i8x16}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ]) + \wedge & c' = \lanes^{-1}_{i8x16}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])) \end{array} \end{array} @@ -436,7 +436,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & i^\ast = \lanes_{i8x16}(c_1)~\lanes_{i8x16}(c_2) \\ - \wedge & c = \lanes^{-1}_{i8x16}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]]) + \wedge & c = \lanes^{-1}_{i8x16}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])) \end{array} \end{array} @@ -494,7 +494,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & t_2 = \unpacked(t_1\K{x}N) \\ - \wedge & c_2 = \extend^{sx^?}_{t_1,t_2}(\lanes_{t_1\K{x}N}(c_1)[x]) + \wedge & c_2 = \extend^{sx^?}_{t_1,t_2}(\lanes_{t_1\K{x}N}(c_1)[x])) \end{array} \end{array} @@ -529,8 +529,8 @@ Most vector instructions are defined in terms of generic numeric operators appli \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & i^\ast = \lanes_{\shape}(c_2)) \\ - \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_1) + (\iff & i^\ast = \lanes_{\shape}(c_2) \\ + \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_1)) \end{array} \end{array} @@ -673,7 +673,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & i_1^\ast = \lanes_{\shape}(c) \\ - \wedge & i = \bool(\bigwedge(i_1 \neq 0)^\ast) + \wedge & i = \bool(\bigwedge(i_1 \neq 0)^\ast)) \end{array} \end{array} @@ -735,7 +735,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \begin{array}[t]{@{}r@{~}l@{}} (\iff & d_1^M = \narrow^{\sx}_{|t_1|,|t_2|}( \lanes_{t_1\K{x}M}(c_1)) \\ \wedge & d_2^M = \narrow^{\sx}_{|t_1|,|t_2|}( \lanes_{t_1\K{x}M}(c_2)) \\ - \wedge & c = \lanes^{-1}_{t_2\K{x}N}(d_1^M~d_2^M) + \wedge & c = \lanes^{-1}_{t_2\K{x}N}(d_1^M~d_2^M)) \end{array} \end{array} @@ -762,7 +762,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))) + (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)))) \end{array} \end{array} @@ -795,7 +795,7 @@ Most vector instructions are defined in terms of generic numeric operators appli \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx^?}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)[\half(0, N) \slice N])) + (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx^?}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)[\half(0, N) \slice N]))) \end{array} \end{array} @@ -830,7 +830,7 @@ where: \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M) + (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M)) \end{array} \end{array} @@ -840,7 +840,7 @@ where: :math:`\K{i32x4.}\DOT\K{\_i16x8\_s}` .................................... -1. Assert: due to :ref:`validation `, two values of :ref:`value type ` |V128| is on the top of the stack. +1. Assert: due to :ref:`validation `, two values of :ref:`value type ` |V128| are on the top of the stack. 2. Pop the value :math:`\V128.\VCONST~c_2` from the stack. @@ -863,7 +863,7 @@ where: \begin{array}[t]{@{}r@{~}l@{}} (\iff & (i_1~i_2)^\ast = \imul_{32}(\extends_{16,32}(\lanes_{\I16X8}(c_1)), \extends_{16,32}(\lanes_{\I16X8}(c_2))) \\ \wedge & j^\ast = \iadd_{32}(i_1, i_2)^\ast \\ - \wedge & c = \lanes^{-1}_{\I32X4}(j^\ast) + \wedge & c = \lanes^{-1}_{\I32X4}(j^\ast)) \end{array} \end{array} @@ -873,7 +873,7 @@ where: :math:`t_2\K{x}N\K{.}\EXTMUL\K{\_}\half\K{\_}t_1\K{x}M\K{\_}\sx` ................................................................ -1. Assert: due to :ref:`validation `, two values of :ref:`value type ` |V128| is on the top of the stack. +1. Assert: due to :ref:`validation `, two values of :ref:`value type ` |V128| are on the top of the stack. 2. Pop the value :math:`\V128.\VCONST~c_2` from the stack. @@ -903,7 +903,7 @@ where: \begin{array}[t]{@{}r@{~}l@{}} (\iff & i^\ast = \lanes_{t_1\K{x}M}(c_1)[\half(0, N) \slice N] \\ \wedge & j^\ast = \lanes_{t_1\K{x}M}(c_2)[\half(0, N) \slice N] \\ - \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{t_2\K{x}N}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast))) + \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{t_2\K{x}N}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast)))) \end{array} where: @@ -941,7 +941,7 @@ where: \begin{array}[t]{@{}r@{~}l@{}} (\iff & (i_1~i_2)^\ast = \extend^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)) \\ \wedge & j^\ast = \iadd_{N}(i_1, i_2)^\ast \\ - \wedge & c = \lanes^{-1}_{t_2\K{x}N}(j^\ast) + \wedge & c = \lanes^{-1}_{t_2\K{x}N}(j^\ast)) \end{array} \end{array} @@ -1777,9 +1777,9 @@ Memory Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + M \cdot N / 8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & \bytes_{\iM}(m_k) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} + k \cdot M/8 \slice M/8]) \\ + \wedge & \bytes_{\iM}(m_k) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} + k \cdot M/8 \slice M/8] \\ \wedge & W = M \cdot 2 \\ - \wedge & c = \lanes^{-1}_{\X{i}W\K{x}N}(\extend^{\sx}_{M,W}(m_0) \dots \extend^{\sx}_{M,W}(m_{N-1})) + \wedge & c = \lanes^{-1}_{\X{i}W\K{x}N}(\extend^{\sx}_{M,W}(m_0) \dots \extend^{\sx}_{M,W}(m_{N-1}))) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -1835,8 +1835,8 @@ Memory Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8]) \\ - \wedge & c = \lanes^{-1}_{\iN\K{x}L}(n^L) + \wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] \\ + \wedge & c = \lanes^{-1}_{\iN\K{x}L}(n^L)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -1890,8 +1890,8 @@ Memory Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8]) \\ - \wedge & c = \extendu_{N,128}(n) + \wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] \\ + \wedge & c = \extendu_{N,128}(n)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -1951,9 +1951,9 @@ Memory Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & \bytes_{\iN}(r) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8]) \\ + \wedge & \bytes_{\iN}(r) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] \\ \wedge & L = 128/N \\ - \wedge & c = \lanes^{-1}_{\K{i}N\K{x}L}(\lanes_{\K{i}N\K{x}L}(v) \with [x] = r) + \wedge & c = \lanes^{-1}_{\K{i}N\K{x}L}(\lanes_{\K{i}N\K{x}L}(v) \with [x] = r)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -2030,7 +2030,7 @@ Memory Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ - \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\wrap_{|t|,N}(c)) \\[1ex] + \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\wrap_{|t|,N}(c))) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -2087,7 +2087,7 @@ Memory Instructions (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ \wedge & L = 128/N \\ - \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\lanes_{\K{i}N\K{x}L}(c)[x]) + \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\lanes_{\K{i}N\K{x}L}(c)[x])) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index eb2faa05f6..0e8c9d50a0 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -386,7 +386,7 @@ Growing :ref:`tables ` \wedge & \X{len} < 2^{32} \\ \wedge & \limits~t = \tableinst.\TITYPE \\ \wedge & \limits' = \limits \with \LMIN = \X{len} \\ - \wedge & \vdashlimits \limits' \ok \\ + \wedge & \vdashlimits \limits' \ok) \\ \end{array} \\ \end{array} @@ -424,7 +424,7 @@ Growing :ref:`memories ` \wedge & \X{len} \leq 2^{16} \\ \wedge & \limits = \meminst.\MITYPE \\ \wedge & \limits' = \limits \with \LMIN = \X{len} \\ - \wedge & \vdashlimits \limits' \ok \\ + \wedge & \vdashlimits \limits' \ok) \\ \end{array} \\ \end{array} @@ -462,7 +462,7 @@ and list of :ref:`reference ` vectors for the module's :ref:`element 6. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEMS`, do: - a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` a :ref:`element instance ` of :ref:`reference type ` :math:`\elem_i.\ETYPE` with contents :math:`(\reff^\ast)^\ast[i]`. + a. Let :math:`\elemaddr_i` be the :ref:`element address ` resulting from :ref:`allocating ` an :ref:`element instance ` of :ref:`reference type ` :math:`\elem_i.\ETYPE` with contents :math:`(\reff^\ast)^\ast[i]`. 7. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATAS`, do: diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index 3019844475..c7050b17d0 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -197,7 +197,7 @@ Numeric vectors have the same underlying representation as an |i128|. They can a \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\where & B = |t| / 8 \\ - \wedge & b^{16} = bytes_{\i128}(c) \\ + \wedge & b^{16} = \bytes_{\i128}(c) \\ \wedge & c_i = \bytes_{t}^{-1}(b^{16}[i \cdot B \slice B])) \end{array} \end{array} @@ -746,7 +746,7 @@ The integer result of predicates -- i.e., :ref:`tests ` and :ref: * Let :math:`j` be the :ref:`signed interpretation ` of :math:`i`. -* If :math:`j` greater than or equal to :math:`0`, then return :math:`i`. +* If :math:`j` is greater than or equal to :math:`0`, then return :math:`i`. * Else return the negation of `j`, modulo :math:`2^N`. @@ -1060,13 +1060,13 @@ This non-deterministic result is expressed by the following auxiliary function p * Else if both :math:`z_1` and :math:`z_2` are infinities of equal sign, then return that infinity. -* Else if one of :math:`z_1` or :math:`z_2` is an infinity, then return that infinity. +* Else if either :math:`z_1` or :math:`z_2` is an infinity, then return that infinity. * Else if both :math:`z_1` and :math:`z_2` are zeroes of opposite sign, then return positive zero. * Else if both :math:`z_1` and :math:`z_2` are zeroes of equal sign, then return that zero. -* Else if one of :math:`z_1` or :math:`z_2` is a zero, then return the other operand. +* Else if either :math:`z_1` or :math:`z_2` is a zero, then return the other operand. * Else if both :math:`z_1` and :math:`z_2` are values with the same magnitude but opposite signs, then return positive zero. @@ -1149,9 +1149,9 @@ This non-deterministic result is expressed by the following auxiliary function p * Else if both :math:`z_1` and :math:`z_2` are infinities of opposite sign, then return negative infinity. -* Else if one of :math:`z_1` or :math:`z_2` is an infinity and the other a value with equal sign, then return positive infinity. +* Else if either :math:`z_1` or :math:`z_2` is an infinity and the other a value with equal sign, then return positive infinity. -* Else if one of :math:`z_1` or :math:`z_2` is an infinity and the other a value with opposite sign, then return negative infinity. +* Else if either :math:`z_1` or :math:`z_2` is an infinity and the other a value with opposite sign, then return negative infinity. * Else if both :math:`z_1` and :math:`z_2` are zeroes of equal sign, then return positive zero. @@ -1235,9 +1235,9 @@ This non-deterministic result is expressed by the following auxiliary function p * If either :math:`z_1` or :math:`z_2` is a NaN, then return an element of :math:`\nans_N\{z_1, z_2\}`. -* Else if one of :math:`z_1` or :math:`z_2` is a negative infinity, then return negative infinity. +* Else if either :math:`z_1` or :math:`z_2` is a negative infinity, then return negative infinity. -* Else if one of :math:`z_1` or :math:`z_2` is a positive infinity, then return the other value. +* Else if either :math:`z_1` or :math:`z_2` is a positive infinity, then return the other value. * Else if both :math:`z_1` and :math:`z_2` are zeroes of opposite signs, then return negative zero. @@ -1264,9 +1264,9 @@ This non-deterministic result is expressed by the following auxiliary function p * If either :math:`z_1` or :math:`z_2` is a NaN, then return an element of :math:`\nans_N\{z_1, z_2\}`. -* Else if one of :math:`z_1` or :math:`z_2` is a positive infinity, then return positive infinity. +* Else if either :math:`z_1` or :math:`z_2` is a positive infinity, then return positive infinity. -* Else if one of :math:`z_1` or :math:`z_2` is a negative infinity, then return the other value. +* Else if either :math:`z_1` or :math:`z_2` is a negative infinity, then return the other value. * Else if both :math:`z_1` and :math:`z_2` are zeroes of opposite signs, then return positive zero. diff --git a/document/core/intro/overview.rst b/document/core/intro/overview.rst index b9e858cccc..5a4760baf4 100644 --- a/document/core/intro/overview.rst +++ b/document/core/intro/overview.rst @@ -26,7 +26,7 @@ This language is structured around the following concepts. In addition to these basic number types, there is a single 128 bit wide vector type representing different types of packed data. The supported representations are 4 32-bit, or 2 64-bit - |IEEE754|_ numbers, or different widths of packed integer values + |IEEE754|_ numbers, or different widths of packed integer values, specifically 2 64-bit integers, 4 32-bit integers, 8 16-bit integers, or 16 8-bit integers. diff --git a/document/core/syntax/conventions.rst b/document/core/syntax/conventions.rst index 979d6bc4e3..9e5dca1820 100644 --- a/document/core/syntax/conventions.rst +++ b/document/core/syntax/conventions.rst @@ -107,9 +107,9 @@ The following notation is adopted for manipulating such records: The update notation for sequences and records generalizes recursively to nested components accessed by "paths" :math:`\X{pth} ::= ([\dots] \;| \;.\K{field})^+`: -* :math:`s \with [i]\,\X{pth} = A` is short for :math:`s \with [i] = (s[i] \with \X{pth} = A)`. +* :math:`s \with [i]\,\X{pth} = A` is short for :math:`s \with [i] = (s[i] \with \X{pth} = A)`, -* :math:`r \with \K{field}\,\X{pth} = A` is short for :math:`r \with \K{field} = (r.\K{field} \with \X{pth} = A)`. +* :math:`r \with \K{field}\,\X{pth} = A` is short for :math:`r \with \K{field} = (r.\K{field} \with \X{pth} = A)`, where :math:`r \with~.\K{field} = A` is shortened to :math:`r \with \K{field} = A`. diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 5b869b33f7..6ebb400d98 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -428,7 +428,7 @@ Instructions in this group are concerned with accessing :ref:`references ` results if any of the accessed memory bytes lies outside the address range implied by the memory's current size. .. note:: - Future version of WebAssembly might provide memory instructions with 64 bit address ranges. + Future versions of WebAssembly might provide memory instructions with 64 bit address ranges. The |MEMORYSIZE| instruction returns the current size of a memory. The |MEMORYGROW| instruction grows memory by a given delta and returns the previous size, or :math:`-1` if enough memory cannot be allocated. diff --git a/document/core/text/conventions.rst b/document/core/text/conventions.rst index ddcd8e7809..12c8b7dfc8 100644 --- a/document/core/text/conventions.rst +++ b/document/core/text/conventions.rst @@ -110,7 +110,7 @@ Contexts The text format allows the use of symbolic :ref:`identifiers ` in place of :ref:`indices `. To resolve these identifiers into concrete indices, -some grammar production are indexed by an *identifier context* :math:`I` as a synthesized attribute that records the declared identifiers in each :ref:`index space `. +some grammar productions are indexed by an *identifier context* :math:`I` as a synthesized attribute that records the declared identifiers in each :ref:`index space `. In addition, the context records the types defined in the module, so that :ref:`parameter ` indices can be computed for :ref:`functions `. It is convenient to define identifier contexts as :ref:`records ` :math:`I` with abstract syntax as follows: diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index b85f513280..0964dfdaa1 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -120,7 +120,7 @@ The following auxiliary function extracts optional identifiers from parameters: Both productions overlap for the case that the function type is :math:`[] \to []`. However, in that case, they also produce the same results, so that the choice is immaterial. - The :ref:`well-formedness ` condition on :math:`I'` ensures that the parameters do not contain duplicate identifier. + The :ref:`well-formedness ` condition on :math:`I'` ensures that the parameters do not contain duplicate identifiers. .. _text-typeuse-abbrev: @@ -356,7 +356,7 @@ Memory definitions can bind a symbolic :ref:`memory identifier `. Abbreviations ............. -A :ref:`data segment ` can be given inline with a memory definition, in which case its offset is :math:`0` the :ref:`limits ` of the :ref:`memory type ` are inferred from the length of the data, rounded up to :ref:`page size `: +A :ref:`data segment ` can be given inline with a memory definition, in which case its offset is :math:`0` and the :ref:`limits ` of the :ref:`memory type ` are inferred from the length of the data, rounded up to :ref:`page size `: .. math:: \begin{array}{llclll} @@ -365,7 +365,7 @@ A :ref:`data segment ` can be given inline with a memory definition, \text{(}~\text{memory}~~\Tid'~~m~~m~\text{)} \\ & \qquad \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} \\ & \qquad\qquad - (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, m = \F{ceil}(n / 64\F{Ki})) \\ + (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, m = \F{ceil}(n / 64\,\F{Ki})) \\ \end{array} Memories can be defined as :ref:`imports ` or :ref:`exports ` inline: diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index b6a49b0cd3..ae219e44a2 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -150,7 +150,7 @@ and there is one respective rule for each relevant construct :math:`A` of the ab C \vdash \I32.\ADD : [\I32~\I32] \to [\I32] } - The instruction is always valid with type :math:`[\I32~\I32] \to [\I32`] + The instruction is always valid with type :math:`[\I32~\I32] \to [\I32]` (saying that it consumes two |I32| values and produces one), independent of any side conditions. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 131551416c..a6d6b007ab 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1033,7 +1033,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 \cdot M }{ - C \vdashinstr \K{v128.}\K{.}\LOAD{N}\K{x}M\_\sx~\memarg : [\I32] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~\memarg : [\I32] \to [\V128] } @@ -1578,7 +1578,7 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`stack type ` :math:`[] \to [{t'}^\ast]`. -* For each :ref:`operand type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. +* For each :ref:`operand type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. * Then the expression is valid with :ref:`result type ` :math:`[t^\ast]`. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index ed17d795cb..5b13ae7fc5 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -147,7 +147,7 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` with some :ref:`result type ` :math:`[t]`. diff --git a/document/js-api/index.bs b/document/js-api/index.bs index 20c2c6e5cb..40267eb85d 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -585,7 +585,7 @@ interface Module {
- The Module(|bytes|) constructor, when invoked, performs the follwing steps: + The Module(|bytes|) constructor, when invoked, performs the following steps: 1. Let |stableBytes| be a [=get a copy of the buffer source|copy of the bytes held by the buffer=] |bytes|. 1. [=Compile a WebAssembly module|Compile the WebAssembly module=] |stableBytes| and store the result as |module|. @@ -778,7 +778,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address 1. Let |ref| be [=DefaultValue=](|elementType|). 1. Otherwise, 1. Let |ref| be ? [=ToWebAssemblyValue=](|value|, |elementType|). - 1. Let |type| be the [=table type=] {[=table type|min=] |initial|, [=table type|ma𝗑=] |maximum|} |elementType|. + 1. Let |type| be the [=table type=] {[=table type|min=] |initial|, [=table type|max=] |maximum|} |elementType|. 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |tableaddr|) be [=table_alloc=](|store|, |type|, |ref|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. @@ -1147,7 +1147,7 @@ WebAssembly defines the following Error classes: CompileError When the [=namespace object=] for the {{WebAssembly}} namespace is [=create a namespace object|created=], the following steps must be run: -1. Let |namespaceObject| the [=namespace object=]. +1. Let |namespaceObject| be the [=namespace object=]. 1. [=list/iterate|For each=] |error| of « "CompileError", "LinkError", "RuntimeError" », 1. Let |constructor| be a new object, implementing the [=NativeError Object Structure=], with NativeError set to |error|. 1. ! [$CreateMethodProperty$](|namespaceObject|, |error|, |constructor|). @@ -1241,4 +1241,4 @@ In practice, an implementation may run out of resources for valid modules below

This section is non-normative.

-This document defines a host environment for WebAssembly. It enables a WebAssembly instance to [=import=] JavaScript objects and functions from an [=read the imports|import object=], but otherwise provides no access to the embedding environment. Thus a WebAssembly instance is bounds to the same constraints as JavaScript. +This document defines a host environment for WebAssembly. It enables a WebAssembly instance to [=import=] JavaScript objects and functions from an [=read the imports|import object=], but otherwise provides no access to the embedding environment. Thus a WebAssembly instance is bound to the same constraints as JavaScript. diff --git a/document/web-api/index.bs b/document/web-api/index.bs index 51f92a5a77..6022221296 100644 --- a/document/web-api/index.bs +++ b/document/web-api/index.bs @@ -125,7 +125,7 @@ Note: This algorithm accepts a {{Response}} object, or a 1. If |response| is not [=CORS-same-origin=], [=reject=] |returnValue| with a {{TypeError}} and abort these substeps. 1. If |response|'s [=response/status=] is not an [=ok status=], [=reject=] |returnValue| with a {{TypeError}} and abort these substeps. - 1. [=Consume body|consume=] |response|'s body as an {{ArrayBuffer}}, and let |bodyPromise| be the result. + 1. [=Consume body|Consume=] |response|'s body as an {{ArrayBuffer}}, and let |bodyPromise| be the result. Note: Although it is specified here that the response is consumed entirely before compilation proceeds, that is purely for ease of specification; implementations are likely to instead perform processing in a streaming fashion. The difference is unobservable, and thus the simpler model is specified. @@ -145,7 +145,7 @@ Web user agents must augment the {{Module}} interface with the [DataCloneError" {{DOMException}} + 1. If |forStorage| is true, throw a "DataCloneError" {{DOMException}}. 1. Set |serialized|.\[[Bytes]] to the [=sub-serialization=] of |value|.\[[Bytes]]. @@ -184,7 +184,7 @@ example) even though the exact format of implementation-dependent stack trace strings does not always match, the locations are easily understandable and the same across browsers. -To achieve the same goal of a common representations for WebAssembly constructs, the +To achieve the same goal of a common representation for WebAssembly constructs, the following conventions are adopted. A WebAssembly location is a reference to a particular instruction in the binary, and may be