Merge upstream

LICENSE

@@ -2,9 +2,10 @@ Please see the LICENSE file in each top-level directory for the terms applicable
 
 The relevant directories and licenses are:
 
-document/    - W3C Software and Document Notice and License
-spectec/     - Apache License 2.0
-interpreter/ - Apache License 2.0
-test/        - Apache License 2.0
-proposals/   - Creative Commons Universal 1.0 International License (CC0)
-papers/      - Creative Commons Attribution 4.0 International License (CC BY 4.0)
+document/       - W3C Software and Document Notice and License
+specification/  - W3C Software and Document Notice and License
+spectec/        - Apache License 2.0
+interpreter/    - Apache License 2.0
+test/           - Apache License 2.0
+proposals/      - Creative Commons Universal 1.0 International License (CC0)
+papers/         - Creative Commons Attribution 4.0 International License (CC BY 4.0)

document/core/exec/instructions.rst

@@ -1176,10 +1176,10 @@ Expressions
 
 An :ref:`expression <syntax-expr>` is *evaluated* relative to a :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>` pointing to its containing :ref:`module instance <syntax-moduleinst>`.
 
-$${rule-prose: Eval_expr}
+$${rule-prose-ignore: Eval_expr}
 
-$${rule: Eval_expr}
+$${rule-ignore: Eval_expr}
 
-.. note::
-   Evaluation iterates this reduction rule until reaching a value.
-   Expressions constituting :ref:`function <syntax-func>` bodies are executed during function :ref:`invocation <exec-invoke>`.
+Expression evaluation iterates single-step reduction until reaching a sequence of resulting :ref:`values <syntax-val>`.
+
+Expressions constituting :ref:`function <syntax-func>` bodies are executed during function :ref:`invocation <exec-invoke>`.

document/core/exec/numerics.rst

@@ -1051,17 +1051,17 @@ then its sign is non-deterministic and the :ref:`payload <syntax-payload>` is co
 
 * Otherwise the payload is picked non-deterministically among all :ref:`arithmetic NaNs <arithmetic-nan>`; that is, its most significant bit is :math:`1` and all others are unspecified.
 
-* In the :ref:`deterministic profile <profile-deterministic>`, however, a positive canonical NaNs is reliably produced in the latter case.
+* In the :ref:`deterministic profile <profile-deterministic>`, only positive canonical NaN outputs are produced.
 
 The non-deterministic result is expressed by the following auxiliary function producing a set of allowed outputs from a set of inputs:
 
 .. math::
    \begin{array}{llcl@{\qquad}l}
    & \nans_N\{z^\ast\} &=& \{ + \NAN(\canon_N) \} \\
    \exprofiles{\PROFDET} & \nans_N\{z^\ast\} &=& \{ + \NAN(n), - \NAN(n) ~|~ n = \canon_N \}
-     & (\iff \{z^\ast\} \subseteq \{ + \NAN(\canon_N), - \NAN(\canon_N) \} \\
+     & (\iff \forall \,{\pm \NAN(n)} \in z^\ast,~ n = \canon_N) \\
    \exprofiles{\PROFDET} & \nans_N\{z^\ast\} &=& \{ + \NAN(n), - \NAN(n) ~|~ n \geq \canon_N \}
-     & (\iff \{z^\ast\} \not\subseteq \{ + \NAN(\canon_N), - \NAN(\canon_N) \} \\
+     & (\iff \exists \,{\pm \NAN(n)} \in z^\ast,~ n \neq \canon_N) \\
    \end{array}
 
 
@@ -2221,7 +2221,7 @@ where :math:`f`, :math:`\sx_1`, :math:`\sx_2`, :math:`h`, and :math:`k` are inst
    \VEXTMUL{\K\_}\LOW{\K\_}\sx & \ivmul & \sx & \sx & 0 & M_2 \\
    \VEXTMUL{\K\_}\HIGH{\K\_}\sx & \ivmul & \sx & \sx & M_2 & M_2 \\
    \VDOT{\K\_}\S & \ivdot & \S & \S & 0 & M_1 \\
-   \VRELAXEDDOT{\K\_}\S & \ivdotsat & \S & \relaxed(R_{\F{idot}})[ \S, \U ] & 0 & M_1 \\
+   \VRELAXEDDOT{\K\_}\S & \ivrelaxeddot & \S & \relaxed(R_{\F{idot}})[ \S, \U ] & 0 & M_1 \\
    \end{array}
 
 .. note::
@@ -2533,16 +2533,21 @@ where:
    it behaves like regular :math:`\ivswizzle`.
 
 
-.. _op-irelaxed_dot:
+.. _op-ivrelaxed_dot:
 .. _op-irelaxed_dot_add:
 
-:math:`\VRELAXEDDOT(i_1, i_2)`
-..............................
+:math:`\ivrelaxeddot_N(i_1^{2m}, i_2^{2m})`
+...........................................
 
 The implementation-specific behaviour of this operation is determined by the global parameter :math:`R_{\F{idot}} \in \{0, 1\}`.
-It also affects the behaviour of :math:`\VRELAXEDDOTADD`.
+It also affects the behaviour of :math:`\VRELAXEDDOT` and :math:`\VRELAXEDDOTADD` specified :ref:`above <op-vextbinop>`.
+
+* Return :math:`\relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ]`.
 
-Its definition is part of the definition of :math:`\vextbinop` specified :ref:`above <op-vextbinop>`.
+.. math::
+   \begin{array}{@{}lcll}
+   \ivrelaxeddot_N(i_1^{2m}, i_2^{2m}) &=& \relaxed(R_{\F{idot}})[ \ivdot_N(i_1^{2m}, i_2^{2m}), \ivdotsat_N(i_1^{2m}, i_2^{2m}) ] \\
+   \end{array}
 
 .. note::
    Relaxed dot product is implementation-dependent when the second operand is negative in a signed intepretation.

document/core/syntax/modules.rst

@@ -111,7 +111,7 @@ Conventions
 * For every index space ${-:abcidx}, the notation ${-:$abcidx(A)} denotes the set of indices from that index space occurring free in ${:A}. Sometimes this set is reinterpreted as the :ref:`list <syntax-list>` of its elements.
 
 .. note::
-   For example, if ${:instr*} is ${instr*: (DATA.DROP 1) (MEMORY.INIT 2 3)}, then ${:$dataidx_instrs(instr*) = 1 3}, or equivalently, the set ${:`{1, 3}}.
+   For example, if ${:instr*} is ${instr*: (DATA.DROP 1) (MEMORY.INIT 2 3)}, then ${:$dataidx(instr*) = 1 3}, or equivalently, the set ${:`{1, 3}}.
 
 
 .. index:: ! type definition, type index, function type, aggregate type

document/core/util/macros.def

@@ -1711,7 +1711,7 @@
 .. |frelaxedmin| mathdef:: \xref{exec/numerics}{op-frelaxed_min}{\F{frelaxed\_min}}
 .. |frelaxedmax| mathdef:: \xref{exec/numerics}{op-frelaxed_max}{\F{frelaxed\_max}}
 .. |irelaxedq15mulrs| mathdef:: \xref{exec/numerics}{op-irelaxed_q15mulr_s}{\F{irelaxed\_q15mulr\_s}}
-.. |irelaxeddot| mathdef:: \xref{exec/numerics}{op-irelaxed_dot}{\F{irelaxed\_dot}}
+.. |ivrelaxeddot| mathdef:: \xref{exec/numerics}{op-ivrelaxed_dot}{\F{ivrelaxed\_dot}}
 
 
 .. Numerics, meta functions

document/core/valid/instructions.rst

@@ -1364,8 +1364,6 @@ $${rule-prose: Instrs_ok}
 
 $${rule: Instrs_ok/empty}
 
-$${rule: Instrs_ok/instr}
-
 $${rule: Instrs_ok/seq}
 
 $${rule: Instrs_ok/sub}

document/core/valid/matching.rst

@@ -131,7 +131,7 @@ Field Types
 
 $${rule-prose: Fieldtype_sub}
 
-$${rule: {Fieldtype_sub/*}}
+$${rule: {Fieldtype_sub/var}}
 
 
 $${rule-prose: Storagetype_sub}
@@ -208,7 +208,7 @@ Global Types
 
 $${rule-prose: Globaltype_sub}
 
-$${rule: {Globaltype_sub/*}}
+$${rule: {Globaltype_sub/var}}
 
 
 .. index:: memory type, limits