[spec] Fix definition of lane ops + better xrefs (#1700)

document/core/appendix/index-instructions.py

@@ -54,8 +54,7 @@ def RefWrap(s, kind):
 
 def Instruction(name, opcode, type=None, validation=None, execution=None, operator=None):
     if operator:
-        execution_str = ', '.join([RefWrap(execution, 'execution'),
-                                   RefWrap(operator, 'operator')])
+        execution_str = RefWrap(execution, 'execution') + ' (' + RefWrap(operator, 'operator') + ')'
     else:
         execution_str = RefWrap(execution, 'execution')
 

document/core/exec/instructions.rst

@@ -20,16 +20,15 @@ The mapping of numeric instructions to their underlying operators is expressed b
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \X{op}_{\IN}(i_1,\dots,i_k) &=& \F{i}\X{op}_N(i_1,\dots,i_k) \\
-   \X{op}_{\FN}(z_1,\dots,z_k) &=& \F{f}\X{op}_N(z_1,\dots,z_k) \\
-   \X{op}_{\VN}(i_1,\dots,i_k) &=& \F{i}\X{op}_N(i_1,\dots,i_k) \\
+   \X{op}_{\IN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\
+   \X{op}_{\FN}(z_1,\dots,z_k) &=& \xref{exec/numerics}{float-ops}{\F{f}\X{op}}_N(z_1,\dots,z_k) \\
    \end{array}
 
 And for :ref:`conversion operators <exec-cvtop>`:
 
 .. math::
    \begin{array}{lll@{\qquad}l}
-   \X{cvtop}^{\sx^?}_{t_1,t_2}(c) &=& \X{cvtop}^{\sx^?}_{|t_1|,|t_2|}(c) \\
+   \cvtop^{\sx^?}_{t_1,t_2}(c) &=& \xref{exec/numerics}{convert-ops}{\X{cvtop}}^{\sx^?}_{|t_1|,|t_2|}(c) \\
    \end{array}
 
 Where the underlying operators are partial, the corresponding instruction will :ref:`trap <trap>` when the result is not defined.
@@ -64,9 +63,9 @@ Where the underlying operators are non-deterministic, because they may return on
 
 2. Pop the value :math:`t.\CONST~c_1` from the stack.
 
-3. If :math:`\unop_t(c_1)` is defined, then:
+3. If :math:`\unopF_t(c_1)` is defined, then:
 
-   a. Let :math:`c` be a possible result of computing :math:`\unop_t(c_1)`.
+   a. Let :math:`c` be a possible result of computing :math:`\unopF_t(c_1)`.
 
    b. Push the value :math:`t.\CONST~c` to the stack.
 
@@ -77,9 +76,9 @@ Where the underlying operators are non-deterministic, because they may return on
 .. math::
    \begin{array}{lcl@{\qquad}l}
    (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& (t\K{.}\CONST~c)
-     & (\iff c \in \unop_t(c_1)) \\
+     & (\iff c \in \unopF_t(c_1)) \\
    (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& \TRAP
-     & (\iff \unop_{t}(c_1) = \{\})
+     & (\iff \unopF_{t}(c_1) = \{\})
    \end{array}
 
 
@@ -94,9 +93,9 @@ Where the underlying operators are non-deterministic, because they may return on
 
 3. Pop the value :math:`t.\CONST~c_1` from the stack.
 
-4. If :math:`\binop_t(c_1, c_2)` is defined, then:
+4. If :math:`\binopF_t(c_1, c_2)` is defined, then:
 
-   a. Let :math:`c` be a possible result of computing :math:`\binop_t(c_1, c_2)`.
+   a. Let :math:`c` be a possible result of computing :math:`\binopF_t(c_1, c_2)`.
 
    b. Push the value :math:`t.\CONST~c` to the stack.
 
@@ -107,9 +106,9 @@ Where the underlying operators are non-deterministic, because they may return on
 .. math::
    \begin{array}{lcl@{\qquad}l}
    (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& (t\K{.}\CONST~c)
-     & (\iff c \in \binop_t(c_1,c_2)) \\
+     & (\iff c \in \binopF_t(c_1,c_2)) \\
    (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& \TRAP
-     & (\iff \binop_{t}(c_1,c_2) = \{\})
+     & (\iff \binopF_{t}(c_1,c_2) = \{\})
    \end{array}
 
 
@@ -122,14 +121,14 @@ Where the underlying operators are non-deterministic, because they may return on
 
 2. Pop the value :math:`t.\CONST~c_1` from the stack.
 
-3. Let :math:`c` be the result of computing :math:`\testop_t(c_1)`.
+3. Let :math:`c` be the result of computing :math:`\testopF_t(c_1)`.
 
 4. Push the value :math:`\I32.\CONST~c` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
    (t\K{.}\CONST~c_1)~t\K{.}\testop &\stepto& (\I32\K{.}\CONST~c)
-     & (\iff c = \testop_t(c_1)) \\
+     & (\iff c = \testopF_t(c_1)) \\
    \end{array}
 
 
@@ -144,14 +143,14 @@ Where the underlying operators are non-deterministic, because they may return on
 
 3. Pop the value :math:`t.\CONST~c_1` from the stack.
 
-4. Let :math:`c` be the result of computing :math:`\relop_t(c_1, c_2)`.
+4. Let :math:`c` be the result of computing :math:`\relopF_t(c_1, c_2)`.
 
 5. Push the value :math:`\I32.\CONST~c` to the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
    (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\relop &\stepto& (\I32\K{.}\CONST~c)
-     & (\iff c = \relop_t(c_1,c_2)) \\
+     & (\iff c = \relopF_t(c_1,c_2)) \\
    \end{array}
 
 
@@ -256,20 +255,27 @@ Reference Instructions
 Vector Instructions
 ~~~~~~~~~~~~~~~~~~~
 
-Most vector instructions are defined in terms of generic numeric operators applied lane-wise based on the :ref:`shape <syntax-vec-shape>`.
+Vector instructions that operate bitwise are handled as integer operations of respective width.
 
 .. math::
    \begin{array}{lll@{\qquad}l}
+   \X{op}_{\VN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\
+   \end{array}
+
+Most other vector instructions are defined in terms of numeric operators that are applied lane-wise according to the given :ref:`shape <syntax-vec-shape>`.
+
+.. math::
+   \begin{array}{llll}
    \X{op}_{t\K{x}N}(n_1,\dots,n_k) &=&
-     \lanes^{-1}_{t\K{x}N}(op_t(\lanes_{t\K{x}N}(n_1) ~\dots~ \lanes_{t\K{x}N}(n_k))
+     \lanes^{-1}_{t\K{x}N}(\xref{exec/instructions}{exec-instr-numeric}{\X{op}}_t(i_1,\dots,i_k)^\ast) & \qquad(\iff i_1^\ast = \lanes_{t\K{x}N}(n_1) \land \dots \land i_k^\ast = \lanes_{t\K{x}N}(n_k) \\
    \end{array}
 
 .. note::
-   For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`i_1, i_2`
-   invokes :math:`\ADD_{\K{i32x4}}(i_1, i_2)`, which maps to
-   :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1^+, i_2^+))`,
-   where :math:`i_1^+` and :math:`i_2^+` are sequences resulting from invoking
-   :math:`\lanes_{\K{i32x4}}(i_1)` and :math:`\lanes_{\K{i32x4}}(i_2)`
+   For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`v_1, v_2`
+   invokes :math:`\ADD_{\K{i32x4}}(v_1, v_2)`, which maps to
+   :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1, i_2)^\ast)`,
+   where :math:`i_1^\ast` and :math:`i_2^\ast` are sequences resulting from invoking
+   :math:`\lanes_{\K{i32x4}}(v_1)` and :math:`\lanes_{\K{i32x4}}(v_2)`
    respectively.
 
 

document/core/exec/numerics.rst

@@ -169,24 +169,25 @@ where :math:`M = \significand(N)` and :math:`E = \exponent(N)`.
 Vectors
 .......
 
-Numeric vectors have the same underlying representation as an |i128|.
-They can also be interpreted as a sequence of numeric values packed into a |V128| with a particular |shape|.
+Numeric vectors of type |VN| have the same underlying representation as an |IN|.
+They can also be interpreted as a sequence of numeric values packed into a |VN| with a particular |shape| :math:`t\K{x}M`,
+provided that :math:`N = |t|\cdot M`.
 
 .. math::
    \begin{array}{l}
    \begin{array}{lll@{\qquad}l}
-   \lanes_{t\K{x}N}(c) &=&
-     c_0~\dots~c_{N-1} \\
+   \lanes_{t\K{x}M}(c) &=&
+     c_0~\dots~c_{M-1} \\
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}l@{~}l@{~}l}
-     (\where & B &=& |t| / 8 \\
-     \wedge & b^{16} &=& \bytes_{\i128}(c) \\
-     \wedge & c_i &=& \bytes_{t}^{-1}(b^{16}[i \cdot B \slice B]))
+     (\where & w &=& |t| / 8 \\
+     \wedge & b^\ast &=& \bytes_{\IN}(c) \\
+     \wedge & c_i &=& \bytes_{t}^{-1}(b^\ast[i \cdot w \slice w]))
      \end{array}
    \end{array}
 
-These functions are bijections, so they are invertible.
+This function is a bijection on |IN|, hence it is invertible.
 
 
 .. index:: byte, little endian, memory

document/core/util/macros.def

@@ -500,6 +500,12 @@
 .. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}}
 .. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}}
 
+.. |unopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{unop}}
+.. |binopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{binop}}
+.. |testopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{testop}}
+.. |relopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{relop}}
+.. |cvtopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{cvtop}}
+
 .. |iunop| mathdef:: \xref{syntax/instructions}{syntax-iunop}{\X{iunop}}
 .. |ibinop| mathdef:: \xref{syntax/instructions}{syntax-ibinop}{\X{ibinop}}
 .. |itestop| mathdef:: \xref{syntax/instructions}{syntax-itestop}{\X{itestop}}