diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index c3ffc2a324..8ffedcca31 100755 --- a/document/core/appendix/index-instructions.py +++ b/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') diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ccb27bfd31..74802d6deb 100644 --- a/document/core/exec/instructions.rst +++ b/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 `: .. 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 ` 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 `. +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 `. + +.. 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. diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index 85d3dbd00c..b76190f6f2 100644 --- a/document/core/exec/numerics.rst +++ b/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 diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 2ae99bdee8..1dcec42d2d 100644 --- a/document/core/util/macros.def +++ b/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}}