[spectext] Rename i8x16.any_true to v128.any_true

The renaming was accepted in #416. Interpreter was changed in #426. This
makes similar changes to the formal text.

Author: ngzhian

document/core/appendix/gen-index-instructions.py

@@ -404,9 +404,9 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\V128.\VOR', r'\hex{FD}~~80', r'[\V128~\V128] \to [\V128]', r'validation <valid-vsbinop>', r'execution <exec-vsbinop>', r'operator <op-ior>'),
     Instruction(r'\V128.\VXOR', r'\hex{FD}~~81', r'[\V128~\V128] \to [\V128]', r'validation <valid-vsbinop>', r'execution <exec-vsbinop>', r'operator <op-ixor>'),
     Instruction(r'\V128.\BITSELECT', r'\hex{FD}~~82', r'[\V128~\V128~\V128] \to [\V128]', r'validation <valid-vsternop>', r'execution <exec-vsternop>', r'operator <op-ibitselect>'),
+    Instruction(r'\V128.\ANYTRUE', r'\hex{FD}~~98', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I8X16.\VABS', r'\hex{FD}~~96', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-vunop>', r'operator <op-iabs>'),
     Instruction(r'\I8X16.\VNEG', r'\hex{FD}~~97', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-vunop>', r'operator <op-ineg>'),
-    Instruction(r'\I8X16.\ANYTRUE', r'\hex{FD}~~98', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I8X16.\ALLTRUE', r'\hex{FD}~~99', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I8X16.\BITMASK', r'\hex{FD}~~100', r'[\V128] \to [\I32]', r'validation <valid-simd-bitmask>', r'execution <exec-simd-bitmask>'),
     Instruction(r'\I8X16.\NARROW\K{\_i16x8\_s}', r'\hex{FD}~~101', r'[\V128~\V128] \to [\V128]', r'validation <valid-vbinop>', r'execution <exec-simd-narrow>'),
@@ -427,7 +427,6 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\I8X16.\AVGR\K{\_u}', r'\hex{FD}~~123', r'[\V128~\V128] \to [\V128]', r'validation <valid-vbinop>', r'execution <exec-vbinop>', r'operator <op-iavgr_u>'),
     Instruction(r'\I16X8.\VABS', r'\hex{FD}~~128', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-vunop>', r'operator <op-iabs>'),
     Instruction(r'\I16X8.\VNEG', r'\hex{FD}~~129', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-vunop>', r'operator <op-ineg>'),
-    Instruction(r'\I16X8.\ANYTRUE', r'\hex{FD}~~130', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I16X8.\ALLTRUE', r'\hex{FD}~~131', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I16X8.\BITMASK', r'\hex{FD}~~132', r'[\V128] \to [\I32]', r'validation <valid-simd-bitmask>', r'execution <exec-simd-bitmask>'),
     Instruction(r'\I16X8.\NARROW\K{\_i16x8\_s}', r'\hex{FD}~~133', r'[\V128~\V128] \to [\V128]', r'validation <valid-vbinop>', r'execution <exec-simd-narrow>'),
@@ -453,7 +452,6 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\I16X8.\AVGR\K{\_u}', r'\hex{FD}~~155', r'[\V128~\V128] \to [\V128]', r'validation <valid-vbinop>', r'execution <exec-vbinop>', r'operator <op-iavgr_u>'),
     Instruction(r'\I32X4.\VABS', r'\hex{FD}~~160', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-vunop>', r'operator <op-iabs>'),
     Instruction(r'\I32X4.\VNEG', r'\hex{FD}~~161', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-vunop>', r'operator <op-ineg>'),
-    Instruction(r'\I32X4.\ANYTRUE', r'\hex{FD}~~162', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I32X4.\ALLTRUE', r'\hex{FD}~~163', r'[\V128] \to [\I32]', r'validation <valid-vitestop>', r'execution <exec-vitestop>'),
     Instruction(r'\I32X4.\BITMASK', r'\hex{FD}~~164', r'[\V128] \to [\I32]', r'validation <valid-simd-bitmask>', r'execution <exec-simd-bitmask>'),
     Instruction(r'\I32X4.\WIDEN\K{\_low\_i16x8\_s}', r'\hex{FD}~~167', r'[\V128] \to [\V128]', r'validation <valid-vunop>', r'execution <exec-simd-widen>'),

document/core/appendix/index-instructions.rst

@@ -352,9 +352,9 @@ Instruction                                  Binary Opcode          Type
 :math:`\V128.\VOR`                           :math:`\hex{FD}~~80`   :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <validation <valid-vsbinop>>`               :ref:`execution <execution <exec-vsbinop>>`, :ref:`operator <operator <op-ior>>`        
 :math:`\V128.\VXOR`                          :math:`\hex{FD}~~81`   :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <validation <valid-vsbinop>>`               :ref:`execution <execution <exec-vsbinop>>`, :ref:`operator <operator <op-ixor>>`       
 :math:`\V128.\BITSELECT`                     :math:`\hex{FD}~~82`   :math:`[\V128~\V128~\V128] \to [\V128]`        :ref:`validation <validation <valid-vsternop>>`              :ref:`execution <execution <exec-vsternop>>`, :ref:`operator <operator <op-ibitselect>>`
+:math:`\V128.\ANYTRUE`                       :math:`\hex{FD}~~98`   :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I8X16.\VABS`                         :math:`\hex{FD}~~96`   :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-vunop>>`, :ref:`operator <operator <op-iabs>>`         
 :math:`\I8X16.\VNEG`                         :math:`\hex{FD}~~97`   :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-vunop>>`, :ref:`operator <operator <op-ineg>>`         
-:math:`\I8X16.\ANYTRUE`                      :math:`\hex{FD}~~98`   :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I8X16.\ALLTRUE`                      :math:`\hex{FD}~~99`   :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I8X16.\BITMASK`                      :math:`\hex{FD}~~100`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-simd-bitmask>>`          :ref:`execution <execution <exec-simd-bitmask>>`                                        
 :math:`\I8X16.\NARROW\K{\_i16x8\_s}`         :math:`\hex{FD}~~101`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <validation <valid-vbinop>>`                :ref:`execution <execution <exec-simd-narrow>>`                                         
@@ -375,7 +375,6 @@ Instruction                                  Binary Opcode          Type
 :math:`\I8X16.\AVGR\K{\_u}`                  :math:`\hex{FD}~~123`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <validation <valid-vbinop>>`                :ref:`execution <execution <exec-vbinop>>`, :ref:`operator <operator <op-iavgr_u>>`     
 :math:`\I16X8.\VABS`                         :math:`\hex{FD}~~128`  :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-vunop>>`, :ref:`operator <operator <op-iabs>>`         
 :math:`\I16X8.\VNEG`                         :math:`\hex{FD}~~129`  :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-vunop>>`, :ref:`operator <operator <op-ineg>>`         
-:math:`\I16X8.\ANYTRUE`                      :math:`\hex{FD}~~130`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I16X8.\ALLTRUE`                      :math:`\hex{FD}~~131`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I16X8.\BITMASK`                      :math:`\hex{FD}~~132`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-simd-bitmask>>`          :ref:`execution <execution <exec-simd-bitmask>>`                                        
 :math:`\I16X8.\NARROW\K{\_i16x8\_s}`         :math:`\hex{FD}~~133`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <validation <valid-vbinop>>`                :ref:`execution <execution <exec-simd-narrow>>`                                         
@@ -401,7 +400,6 @@ Instruction                                  Binary Opcode          Type
 :math:`\I16X8.\AVGR\K{\_u}`                  :math:`\hex{FD}~~155`  :math:`[\V128~\V128] \to [\V128]`              :ref:`validation <validation <valid-vbinop>>`                :ref:`execution <execution <exec-vbinop>>`, :ref:`operator <operator <op-iavgr_u>>`     
 :math:`\I32X4.\VABS`                         :math:`\hex{FD}~~160`  :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-vunop>>`, :ref:`operator <operator <op-iabs>>`         
 :math:`\I32X4.\VNEG`                         :math:`\hex{FD}~~161`  :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-vunop>>`, :ref:`operator <operator <op-ineg>>`         
-:math:`\I32X4.\ANYTRUE`                      :math:`\hex{FD}~~162`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I32X4.\ALLTRUE`                      :math:`\hex{FD}~~163`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-vitestop>>`              :ref:`execution <execution <exec-vitestop>>`                                            
 :math:`\I32X4.\BITMASK`                      :math:`\hex{FD}~~164`  :math:`[\V128] \to [\I32]`                     :ref:`validation <validation <valid-simd-bitmask>>`          :ref:`execution <execution <exec-simd-bitmask>>`                                        
 :math:`\I32X4.\WIDEN\K{\_low\_i16x8\_s}`     :math:`\hex{FD}~~167`  :math:`[\V128] \to [\V128]`                    :ref:`validation <validation <valid-vunop>>`                 :ref:`execution <execution <exec-simd-widen>>`                                          

document/core/binary/instructions.rst

@@ -572,7 +572,8 @@ All other SIMD instructions are plain opcodes without any immediates.
      \hex{FD}~~79{:}\Bu32 &\Rightarrow& \V128.\VANDNOT \\ &&|&
      \hex{FD}~~80{:}\Bu32 &\Rightarrow& \V128.\VOR \\ &&|&
      \hex{FD}~~81{:}\Bu32 &\Rightarrow& \V128.\VXOR \\ &&|&
-     \hex{FD}~~82{:}\Bu32 &\Rightarrow& \V128.\BITSELECT
+     \hex{FD}~~82{:}\Bu32 &\Rightarrow& \V128.\BITSELECT \\ &&|&
+     \hex{FD}~~98{:}\Bu32 &\Rightarrow& \V128.\ANYTRUE \\ &&|&
    \end{array}
 
 .. _binary-vitestop:
@@ -587,7 +588,6 @@ All other SIMD instructions are plain opcodes without any immediates.
    \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{simdhaslongerinstructionnames} \\[-2ex] &&|&
      \hex{FD}~~96{:}\Bu32 &\Rightarrow& \I8X16.\VABS \\ &&|&
      \hex{FD}~~97{:}\Bu32 &\Rightarrow& \I8X16.\VNEG \\ &&|&
-     \hex{FD}~~98{:}\Bu32 &\Rightarrow& \I8X16.\ANYTRUE \\ &&|&
      \hex{FD}~~99{:}\Bu32 &\Rightarrow& \I8X16.\ALLTRUE \\ &&|&
      \hex{FD}~~100{:}\Bu32 &\Rightarrow& \I8X16.\BITMASK \\ &&|&
      \hex{FD}~~101{:}\Bu32 &\Rightarrow& \I8X16.\NARROW\K{\_i16x8\_s} \\ &&|&
@@ -613,7 +613,6 @@ All other SIMD instructions are plain opcodes without any immediates.
    \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{simdhaslongerinstructionnames} \\[-2ex] &&|&
      \hex{FD}~~128{:}\Bu32 &\Rightarrow& \I16X8.\VABS \\ &&|&
      \hex{FD}~~129{:}\Bu32 &\Rightarrow& \I16X8.\VNEG \\ &&|&
-     \hex{FD}~~130{:}\Bu32 &\Rightarrow& \I16X8.\ANYTRUE \\ &&|&
      \hex{FD}~~131{:}\Bu32 &\Rightarrow& \I16X8.\ALLTRUE \\ &&|&
      \hex{FD}~~132{:}\Bu32 &\Rightarrow& \I16X8.\BITMASK \\ &&|&
      \hex{FD}~~133{:}\Bu32 &\Rightarrow& \I16X8.\NARROW\K{\_i32x4\_s} \\ &&|&
@@ -644,7 +643,6 @@ All other SIMD instructions are plain opcodes without any immediates.
    \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{simdhaslongerinstructionnames} \\[-2ex] &&|&
      \hex{FD}~~160{:}\Bu32 &\Rightarrow& \I32X4.\VABS \\ &&|&
      \hex{FD}~~161{:}\Bu32 &\Rightarrow& \I32X4.\VNEG \\ &&|&
-     \hex{FD}~~162{:}\Bu32 &\Rightarrow& \I32X4.\ANYTRUE \\ &&|&
      \hex{FD}~~163{:}\Bu32 &\Rightarrow& \I32X4.\ALLTRUE \\ &&|&
      \hex{FD}~~164{:}\Bu32 &\Rightarrow& \I32X4.\BITMASK \\ &&|&
      \hex{FD}~~167{:}\Bu32 &\Rightarrow& \I32X4.\WIDEN\K{\_low\_i16x8\_s} \\ &&|&

document/core/exec/instructions.rst

@@ -284,6 +284,26 @@ SIMD instructions are defined in terms of generic numeric operators applied lane
    \end{array}
 
 
+.. _exec-simd-any_true:
+
+:math:`\V128\K{.}\ANYTRUE`
+...........................
+
+1. Assert: due to :ref:`validation <valid-vitestop>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
+
+2. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
+
+3. Let :math:`i` be the result of computing :math:`\ine_{128}(c_1, 0)`.
+
+4. Push the value :math:`\I32.\CONST~i` onto the stack.
+
+.. math::
+   \begin{array}{lcl@{\qquad}l}
+   (\V128\K{.}\VCONST~c_1)~\V128\K{.}\ANYTRUE &\stepto& (\I32\K{.}\CONST~i)
+     & (\iff i = \ine_{128}(c_1, 0)) \\
+   \end{array}
+
+
 .. _exec-simd-swizzle:
 
 :math:`\K{i8x16.}\SWIZZLE`
@@ -561,26 +581,6 @@ SIMD instructions are defined in terms of generic numeric operators applied lane
    \end{array}
 
 
-.. _exec-simd-any_true:
-
-:math:`\shape\K{.}\ANYTRUE`
-...........................
-
-1. Assert: due to :ref:`validation <valid-vitestop>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
-
-2. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
-
-3. Let :math:`i` be the result of computing :math:`\ine_{128}(c_1, 0)`.
-
-4. Push the value :math:`\I32.\CONST~i` onto the stack.
-
-.. math::
-   \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~\shape\K{.}\ANYTRUE &\stepto& (\I32\K{.}\CONST~i)
-     & (\iff i = \ine_{128}(c_1, 0)) \\
-   \end{array}
-
-
 .. _exec-simd-bitmask:
 
 :math:`t\K{x}N\K{.}\BITMASK`

document/core/syntax/instructions.rst

@@ -211,6 +211,7 @@ SIMD instructions provide basic operations over :ref:`values <syntax-value>` of
      \K{v128.}\vsunop \\&&|&
      \K{v128.}\vsbinop \\&&|&
      \K{v128.}\vsternop \\&&|&
+     \K{v128.}\ANYTRUE \\&&|&
      \K{i8x16.}\SHUFFLE~\laneidx^{16} \\&&|&
      \K{i8x16.}\SWIZZLE \\&&|&
      \shape\K{.}\SPLAT \\&&|&
@@ -266,7 +267,6 @@ SIMD instructions provide basic operations over :ref:`values <syntax-value>` of
    \production{SIMD ternary operator} & \vsternop &::=&
      \K{bitselect} \\
    \production{SIMD test operator} & \vitestop &::=&
-     \K{any\_true} ~|~
      \K{all\_true} \\
    \production{SIMD integer relational operator} & \virelop &::=&
      \K{eq} ~|~

document/core/text/instructions.rst

@@ -606,7 +606,8 @@ SIMD const instructions have a mandatory :ref:`shape <syntax-simd-shape>` descri
      \text{v128.andnot} &\Rightarrow& \V128.\VANDNOT\\ &&|&
      \text{v128.or} &\Rightarrow& \V128.\VOR\\ &&|&
      \text{v128.xor} &\Rightarrow& \V128.\VXOR\\ &&|&
-     \text{v128.bitselect} &\Rightarrow& \V128.\BITSELECT
+     \text{v128.bitselect} &\Rightarrow& \V128.\BITSELECT\\ &&|&
+     \text{v128.any\_true} &\Rightarrow& \V128.\ANYTRUE
    \end{array}
 
 .. _text-vitestop:
@@ -621,7 +622,6 @@ SIMD const instructions have a mandatory :ref:`shape <syntax-simd-shape>` descri
    \phantom{\production{instruction}} & \phantom{\Tplaininstr_I} &\phantom{::=}& \phantom{averylonginstructionnameforsimdtext} && \phantom{simdhasreallylonginstructionnames} \\[-2ex] &&|&
      \text{i8x16.abs} &\Rightarrow& \I8X16.\VABS\\ &&|&
      \text{i8x16.neg} &\Rightarrow& \I8X16.\VNEG\\ &&|&
-     \text{i8x16.any\_true} &\Rightarrow& \I8X16.\ANYTRUE\\ &&|&
      \text{i8x16.all\_true} &\Rightarrow& \I8X16.\ALLTRUE\\ &&|&
      \text{i8x16.bitmask} &\Rightarrow& \I8X16.\BITMASK\\ &&|&
      \text{i8x16.narrow\_i16x8\_s} &\Rightarrow& \I8X16.\NARROW\K{\_i16x8\_s}\\ &&|&
@@ -647,7 +647,6 @@ SIMD const instructions have a mandatory :ref:`shape <syntax-simd-shape>` descri
    \phantom{\production{instruction}} & \phantom{\Tplaininstr_I} &\phantom{::=}& \phantom{averylonginstructionnameforsimdtext} && \phantom{simdhasreallylonginstructionnames} \\[-2ex] &&|&
      \text{i16x8.abs} &\Rightarrow& \I16X8.\VABS\\ &&|&
      \text{i16x8.neg} &\Rightarrow& \I16X8.\VNEG\\ &&|&
-     \text{i16x8.any\_true} &\Rightarrow& \I16X8.\ANYTRUE\\ &&|&
      \text{i16x8.all\_true} &\Rightarrow& \I16X8.\ALLTRUE\\ &&|&
      \text{i16x8.bitmask} &\Rightarrow& \I16X8.\BITMASK\\ &&|&
      \text{i16x8.narrow\_i32x4\_s} &\Rightarrow& \I16X8.\NARROW\K{\_i32x4\_s}\\ &&|&
@@ -678,7 +677,6 @@ SIMD const instructions have a mandatory :ref:`shape <syntax-simd-shape>` descri
    \phantom{\production{instruction}} & \phantom{\Tplaininstr_I} &\phantom{::=}& \phantom{averylonginstructionnameforsimdtext} && \phantom{simdhasreallylonginstructionnames} \\[-2ex] &&|&
      \text{i32x4.abs} &\Rightarrow& \I32X4.\VABS\\ &&|&
      \text{i32x4.neg} &\Rightarrow& \I32X4.\VNEG\\ &&|&
-     \text{i32x4.any\_true} &\Rightarrow& \I32X4.\ANYTRUE\\ &&|&
      \text{i32x4.all\_true} &\Rightarrow& \I32X4.\ALLTRUE\\ &&|&
      \text{i32x4.bitmask} &\Rightarrow& \I32X4.\BITMASK\\ &&|&
      \text{i32x4.widen\_low\_i16x8\_s} &\Rightarrow& \I32X4.\WIDEN\K{\_low\_i16x8\_s}\\ &&|&

document/core/valid/instructions.rst

@@ -240,6 +240,20 @@ We also define an auxiliary function to get number of packed numeric types in a
    }
 
 
+.. _valid-any-true:
+
+:math:`\V128\K{.}\ANYTRUE`
+............................
+
+* The instruction is valid with type :math:`[\V128] \to [\I32]`.
+
+.. math::
+   \frac{
+   }{
+     C \vdashinstr \V128\K{.}\ANYTRUE : [\V128] \to [\I32]
+   }
+
+
 .. _valid-simd-shuffle:
 
 :math:`\K{i8x16.}\SHUFFLE~\laneidx^{16}`