[spec] Unbreak all_true again
diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py
index 76dc60d..5822150 100755
--- a/document/core/appendix/index-instructions.py
+++ b/document/core/appendix/index-instructions.py
@@ -478,7 +478,7 @@
Instruction(2.0, r'\I8X16.\VABS', r'\hex{FD}~~\hex{60}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'),
Instruction(2.0, r'\I8X16.\VNEG', r'\hex{FD}~~\hex{61}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ineg'),
Instruction(2.0, r'\I8X16.\VPOPCNT', r'\hex{FD}~~\hex{62}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ipopcnt'),
- Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop', r'op-iall_true'),
+ Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop'),
Instruction(2.0, r'\I8X16.\VBITMASK', r'\hex{FD}~~\hex{64}', r'[\V128] \to [\I32]', r'valid-vbitmask', r'exec-vbitmask', r'op-ivbitmask'),
Instruction(2.0, r'\I8X16.\VNARROW\K{\_i16x8\_s}', r'\hex{FD}~~\hex{65}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vnarrow', r'op-vnarrow'),
Instruction(2.0, r'\I8X16.\VNARROW\K{\_i16x8\_u}', r'\hex{FD}~~\hex{66}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vnarrow', r'op-vnarrow'),
diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst
index a2886f8..ce0e42f 100644
--- a/document/core/exec/numerics.rst
+++ b/document/core/exec/numerics.rst
@@ -583,16 +583,16 @@
\end{array}
-.. _op-iall_true:
+.. _op-inez:
-:math:`\ialltrue_N(i)`
-......................
+:math:`\inez_N(i)`
+..................
* Return :math:`0` if :math:`i` is zero, :math:`1` otherwise.
.. math::
\begin{array}{@{}lcll}
- \ialltrue_N(i) &=& \tobool(i \neq 0)
+ \inez_N(i) &=& \tobool(i \neq 0)
\end{array}
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 7caefba..4af4c09 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -1583,7 +1583,7 @@
.. |ictz| mathdef:: \xref{exec/numerics}{op-ictz}{\F{ictz}}
.. |ipopcnt| mathdef:: \xref{exec/numerics}{op-ipopcnt}{\F{ipopcnt}}
.. |ieqz| mathdef:: \xref{exec/numerics}{op-ieqz}{\F{ieqz}}
-.. |ialltrue| mathdef:: \xref{exec/numerics}{op-iall_true}{\F{iall\_true}}
+.. |inez| mathdef:: \xref{exec/numerics}{op-inez}{\F{inez}}
.. |ieq| mathdef:: \xref{exec/numerics}{op-ieq}{\F{ieq}}
.. |ine| mathdef:: \xref{exec/numerics}{op-ine}{\F{ine}}
.. |ilt| mathdef:: \xref{exec/numerics}{op-ilt}{\F{ilt}}
diff --git a/specification/wasm-3.0/3.1-numerics.scalar.spectec b/specification/wasm-3.0/3.1-numerics.scalar.spectec
index f277a74..832c219 100644
--- a/specification/wasm-3.0/3.1-numerics.scalar.spectec
+++ b/specification/wasm-3.0/3.1-numerics.scalar.spectec
@@ -132,7 +132,7 @@
def $irelaxed_laneselect_(N, iN(N), iN(N), iN(N)) : iN(N)*
def $ieqz_(N, iN(N)) : u32
-def $iall_true_(N, iN(N)) : u32 hint(show $iall__true_(%1,%2))
+def $inez_(N, iN(N)) : u32
def $ieq_(N, iN(N), iN(N)) : u32
def $ine_(N, iN(N), iN(N)) : u32
@@ -217,7 +217,7 @@
def $ieqz_(N, i_1) = $bool(i_1 = 0)
-def $iall_true_(N, i_1) = $bool(i_1 =/= 0)
+def $inez_(N, i_1) = $bool(i_1 =/= 0)
def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2)
diff --git a/specification/wasm-3.0/3.2-numerics.vector.spectec b/specification/wasm-3.0/3.2-numerics.vector.spectec
index e476af0..c88b9da 100644
--- a/specification/wasm-3.0/3.2-numerics.vector.spectec
+++ b/specification/wasm-3.0/3.2-numerics.vector.spectec
@@ -62,9 +62,6 @@
def $ivternopnd_(shape, def $f_(N, iN(N), iN(N), iN(N)) : iN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
def $fvternop_(shape, def $f_(N, fN(N), fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
-def $ivtestop_(shape, def $f_(N, iN(N)) : u32, vec_(V128)) : u32
-def $fvtestop_(shape, def $f_(N, fN(N)) : u32, vec_(V128)) : u32
-
def $ivrelop_(shape, def $f_(N, iN(N), iN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128)
def $ivrelopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : u32, sx, vec_(V128), vec_(V128)) : vec_(V128)
def $fvrelop_(shape, def $f_(N, fN(N), fN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128)
@@ -120,15 +117,6 @@
-- if c** = $setproduct_(lane_(Fnn), $f_($sizenn(Fnn), c_1, c_2, c_3)*)
-def $ivtestop_(Jnn X M, def $f_, v_1) = $prod(c*)
- -- if c_1* = $lanes_(Jnn X M, v_1)
- -- if c* = $f_($lsizenn(Jnn), c_1)*
-
-def $fvtestop_(Fnn X M, def $f_, v_1) = $prod(c*)
- -- if c_1* = $lanes_(Fnn X M, v_1)
- -- if c* = $f_($sizenn(Fnn), c_1)*
-
-
def $ivrelop_(Jnn X M, def $f_, v_1, v_2) = $inv_lanes_(Jnn X M, c*)
-- if c_1* = $lanes_(Jnn X M, v_1)
-- if c_2* = $lanes_(Jnn X M, v_2)
@@ -187,8 +175,6 @@
hint(show %2#$_(%1,%3,%4))
def $vternop_(shape, vternop_(shape), vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
hint(show %2#$_(%1,%3,%4,%5))
-def $vtestop_(shape, vtestop_(shape), vec_(V128)) : u32
- hint(show %2#$_(%1,%3))
def $vrelop_(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
hint(show %2#$_(%1,%3,%4))
@@ -265,8 +251,6 @@
def $vternop_(Fnn X M, RELAXED_MADD, v_1, v_2, v_3) = $fvternop_(Fnn X M, $frelaxed_madd_, v_1, v_2, v_3)
def $vternop_(Fnn X M, RELAXED_NMADD, v_1, v_2, v_3) = $fvternop_(Fnn X M, $frelaxed_nmadd_, v_1, v_2, v_3)
-def $vtestop_(Jnn X M, ALL_TRUE, v) = $ivtestop_(Jnn X M, $iall_true_, v)
-
def $vrelop_(Jnn X M, EQ, v_1, v_2) = $ivrelop_(Jnn X M, $ieq_, v_1, v_2)
def $vrelop_(Jnn X M, NE, v_1, v_2) = $ivrelop_(Jnn X M, $ine_, v_1, v_2)
def $vrelop_(Jnn X M, LT sx, v_1, v_2) = $ivrelopsx_(Jnn X M, $ilt_, sx, v_1, v_2)
diff --git a/specification/wasm-3.0/4.3-execution.instructions.spectec b/specification/wasm-3.0/4.3-execution.instructions.spectec
index 5c7a706..bde165a 100644
--- a/specification/wasm-3.0/4.3-execution.instructions.spectec
+++ b/specification/wasm-3.0/4.3-execution.instructions.spectec
@@ -992,7 +992,7 @@
rule Step_pure/vvtestop:
(VCONST V128 c_1) (VVTESTOP V128 ANY_TRUE) ~> (CONST I32 c)
- -- if c = $ine_($vsize(V128), c_1, 0)
+ -- if c = $inez_($vsize(V128), c_1)
rule Step_pure/vunop-val:
@@ -1023,8 +1023,9 @@
rule Step_pure/vtestop:
- (VCONST V128 c_1) (VTESTOP sh vtestop) ~> (CONST I32 i)
- -- if i = $vtestop_(sh, vtestop, c_1)
+ (VCONST V128 c_1) (VTESTOP (Jnn X M) ALL_TRUE) ~> (CONST I32 c)
+ -- if i* = $lanes_(Jnn X M, c_1)
+ -- if c = $prod(($inez_($jsizenn(Jnn), i)*))
rule Step_pure/vrelop:
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 9847f49..9a2d1cc 100644
--- a/spectec/doc/example/output/NanoWasm.pdf
+++ b/spectec/doc/example/output/NanoWasm.pdf
Binary files differ
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index dbd1b24..59f6ed4 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -4609,9 +4609,9 @@
def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
-def $iall_true_(N : N, iN : iN(N)) : u32
+def $inez_(N : N, iN : iN(N)) : u32
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
- def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
+ def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32
@@ -5037,20 +5037,6 @@
-- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`}))
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`})
@@ -5209,11 +5195,6 @@
def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v)
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2)
@@ -6221,7 +6202,7 @@
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}:
`%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)])
- -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0)))
+ -- if (c = $inez_($vsize(V128_vectype), c_1))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}:
@@ -6254,9 +6235,10 @@
-- if ($vternop_(sh, vternop, c_1, c_2, c_3) = [])
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
- rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}:
- `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)])
- -- if (i = $vtestop_(sh, vtestop, c_1))
+ rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}:
+ `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)])
+ -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1))
+ -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`}))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 168b37b..d2141f7 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -8110,7 +8110,7 @@
$$
\begin{array}[t]{@{}lcl@{}l@{}}
-{{\mathrm{iall\_true}}}_{N}(i_1) & = & \mathbb{B}(i_1 \neq 0) \\
+{{\mathrm{inez}}}_{N}(i_1) & = & \mathbb{B}(i_1 \neq 0) \\
\end{array}
$$
@@ -8468,28 +8468,6 @@
$$
\begin{array}[t]{@{}lcl@{}l@{}}
-{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1) & = & {\Pi}\, {c^\ast} & \quad
-\begin{array}[t]{@{}l@{}}
-\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1) \\
-{\land}~ {c^\ast} = {{{\mathrm{f}}}_{N}(c_1)^\ast} \\
-\end{array} \\
-\end{array}
-$$
-
-$$
-\begin{array}[t]{@{}lcl@{}l@{}}
-{{\mathrm{fvtestop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1) & = & {\Pi}\, {c^\ast} & \quad
-\begin{array}[t]{@{}l@{}}
-\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}(v_1) \\
-{\land}~ {c^\ast} = {{{\mathrm{f}}}_{N}(c_1)^\ast} \\
-\end{array} \\
-\end{array}
-$$
-
-\vspace{1ex}
-
-$$
-\begin{array}[t]{@{}lcl@{}l@{}}
{{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1, v_2) & = & {{{{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}^{{-1}}}}{({c^\ast})} & \quad
\begin{array}[t]{@{}l@{}}
\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1) \\
@@ -8657,12 +8635,6 @@
$$
\begin{array}[t]{@{}lcl@{}l@{}}
-{\mathsf{all\_true}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v)} & = & {{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{iall}}_{{\mathit{true}}}, v) \\
-\end{array}
-$$
-
-$$
-\begin{array}[t]{@{}lcl@{}l@{}}
{\mathsf{eq}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1, v_2)} & = & {{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{ieq}}, v_1, v_2) \\
{\mathsf{ne}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1, v_2)} & = & {{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{ine}}, v_1, v_2) \\
{{\mathsf{lt}}{\mathsf{\_}}{{\mathit{sx}}}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1, v_2)} & = & {{\mathrm{ivrelopsx}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{ilt}}, {\mathit{sx}}, v_1, v_2) \\
@@ -10747,7 +10719,7 @@
$$
\begin{array}[t]{@{}lrcl@{}l@{}}
-{[\textsc{\scriptsize E{-}vvtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~(\mathsf{v{\scriptstyle 128}} {.} \mathsf{any\_true}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c) & \quad \mbox{if}~ c = {{\mathrm{ine}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1, 0) \\
+{[\textsc{\scriptsize E{-}vvtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~(\mathsf{v{\scriptstyle 128}} {.} \mathsf{any\_true}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c) & \quad \mbox{if}~ c = {{\mathrm{inez}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1) \\
\end{array}
$$
@@ -10782,7 +10754,11 @@
$$
\begin{array}[t]{@{}lrcl@{}l@{}}
-{[\textsc{\scriptsize E{-}vtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~({\mathit{sh}} {.} {\mathit{vtestop}}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i) & \quad \mbox{if}~ i = {{\mathit{vtestop}}}{{}_{{\mathit{sh}}}(c_1)} \\
+{[\textsc{\scriptsize E{-}vtestop}]} \quad & (\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)~({{\mathsf{i}}{N}}{\mathsf{x}}{M} {.} \mathsf{all\_true}) & \hookrightarrow & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c) & \quad
+\begin{array}[t]{@{}l@{}}
+\mbox{if}~ {i^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(c_1) \\
+{\land}~ c = {\Pi}\, ({{{\mathrm{inez}}}_{N}(i)^\ast}) \\
+\end{array} \\
\end{array}
$$
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 411691d..167b1ba 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -4599,9 +4599,9 @@
def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
-def $iall_true_(N : N, iN : iN(N)) : u32
+def $inez_(N : N, iN : iN(N)) : u32
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
- def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
+ def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32
@@ -5027,20 +5027,6 @@
-- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`}))
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`})
@@ -5199,11 +5185,6 @@
def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v)
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2)
@@ -6211,7 +6192,7 @@
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}:
`%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)])
- -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0)))
+ -- if (c = $inez_($vsize(V128_vectype), c_1))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}:
@@ -6244,9 +6225,10 @@
-- if ($vternop_(sh, vternop, c_1, c_2, c_3) = [])
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
- rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}:
- `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)])
- -- if (i = $vtestop_(sh, vtestop, c_1))
+ rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}:
+ `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)])
+ -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1))
+ -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`}))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:
@@ -15948,9 +15930,9 @@
def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
-def $iall_true_(N : N, iN : iN(N)) : u32
+def $inez_(N : N, iN : iN(N)) : u32
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
- def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
+ def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32
@@ -16376,20 +16358,6 @@
-- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`}))
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`})
@@ -16548,11 +16516,6 @@
def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v)
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2)
@@ -17562,7 +17525,7 @@
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}:
`%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)])
- -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0)))
+ -- if (c = $inez_($vsize(V128_vectype), c_1))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}:
@@ -17595,9 +17558,10 @@
-- if ($vternop_(sh, vternop, c_1, c_2, c_3) = [])
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
- rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}:
- `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)])
- -- if (i = $vtestop_(sh, vtestop, c_1))
+ rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}:
+ `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)])
+ -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1))
+ -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`}))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:
@@ -27423,9 +27387,9 @@
def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
-def $iall_true_(N : N, iN : iN(N)) : u32
+def $inez_(N : N, iN : iN(N)) : u32
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
- def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
+ def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32
@@ -27851,20 +27815,6 @@
-- if (c*{c <- `c*`}*{`c*` <- `c**`} = $setproduct_(syntax lane_((Fnn : Fnn <: lanetype)), $f_($sizenn((Fnn : Fnn <: numtype)), c_1, c_2, c_3)*{c_1 <- `c_1*`, c_2 <- `c_2*`, c_3 <- `c_3*`}))
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $ivtestop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $fvtestop_{Fnn : Fnn, M : M, def $f_(N : N, fN : fN(N)) : u32, v_1 : vec_(V128_Vnn), `c*` : u32*, `c_1*` : lane_($lanetype(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $f_, v_1) = `%`_u32($prod(c!`%`_u32.0*{c <- `c*`}))
- -- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1))
- -- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`})
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_(shape : shape, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $ivrelop_{Jnn : Jnn, M : M, def $f_(N : N, iN : iN(N), iN : iN(N)) : u32, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), `c*` : iN($lsizenn((Jnn : Jnn <: lanetype)))*, `c_1*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*, `c_2*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $f_, v_1, v_2) = $inv_lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c*{c <- `c*`})
@@ -28023,11 +27973,6 @@
def $vternop_{Fnn : Fnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn), v_3 : vec_(V128_Vnn)}(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), RELAXED_NMADD_vternop_, v_1, v_2, v_3) = $fvternop_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), def $frelaxed_nmadd_, v_1, v_2, v_3)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
-def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32
- ;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
- def $vtestop_{Jnn : Jnn, M : M, v : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_, v) = $ivtestop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $iall_true_, v)
-
-;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
def $vrelop_{Jnn : Jnn, M : M, v_1 : vec_(V128_Vnn), v_2 : vec_(V128_Vnn)}(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), EQ_vrelop_, v_1, v_2) = $ivrelop_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), def $ieq_, v_1, v_2)
@@ -29052,7 +28997,7 @@
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}:
`%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)])
- -- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0)))
+ -- if (c = $inez_($vsize(V128_vectype), c_1))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}:
@@ -29088,9 +29033,10 @@
-- if ($vternop_(sh, vternop, c_1, c_2, c_3) = [])
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
- rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}:
- `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)])
- -- if (i = $vtestop_(sh, vtestop, c_1))
+ rule vtestop{c_1 : vec_(V128_Vnn), Jnn : Jnn, M : M, c : num_(I32_numtype), `i*` : lane_($lanetype(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M))))*}:
+ `%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)])
+ -- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1))
+ -- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`}))
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index adf3fc7..03a8738 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -18740,7 +18740,7 @@
#. Pop the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)` from the stack.
-#. Let :math:`c` be :math:`{{\mathrm{ine}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1, 0)`.
+#. Let :math:`c` be :math:`{{\mathrm{inez}}}_{{|\mathsf{v{\scriptstyle 128}}|}}(c_1)`.
#. Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c)` to the stack.
@@ -18808,17 +18808,19 @@
#. Push the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c)` to the stack.
-:math:`{\mathit{sh}} {.} {\mathit{vtestop}}`
-............................................
+:math:`{{\mathsf{i}}{N}}{\mathsf{x}}{M} {.} \mathsf{all\_true}`
+...............................................................
1. Assert: Due to validation, a value of vector type :math:`\mathsf{v{\scriptstyle 128}}` is on the top of the stack.
#. Pop the value :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{const}~c_1)` from the stack.
-#. Let :math:`i` be :math:`{{\mathit{vtestop}}}{{}_{{\mathit{sh}}}(c_1)}`.
+#. Let :math:`{i^\ast}` be :math:`{{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(c_1)`.
-#. Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i)` to the stack.
+#. Let :math:`c` be :math:`{\Pi}\, {{{\mathrm{inez}}}_{N}(i)^\ast}`.
+
+#. Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c)` to the stack.
:math:`{\mathit{sh}} {.} {\mathit{vrelop}}`
@@ -23964,8 +23966,8 @@
1. Return :math:`\mathbb{B}(i_1 = 0)`.
-:math:`{{\mathrm{iall\_true}}}_{N}(i_1)`
-........................................
+:math:`{{\mathrm{inez}}}_{N}(i_1)`
+..................................
1. Return :math:`\mathbb{B}(i_1 \neq 0)`.
@@ -24613,40 +24615,6 @@
#. Return :math:`{{{{{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}^{{-1}}}}{({c^\ast})}^\ast}`.
-:math:`{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1)`
-...................................................................................
-
-
-1. Let :math:`{c_1^\ast}` be :math:`{{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1)`.
-
-#. Let :math:`{c^\ast}` be :math:`\epsilon`.
-
-#. For each :math:`c_1` in :math:`{c_1^\ast}`, do:
-
- a. Let :math:`c` be :math:`{{\mathrm{f}}}_{N}(c_1)`.
-
- #. Append :math:`c` to :math:`{c^\ast}`.
-
-#. Return :math:`{\Pi}\, {c^\ast}`.
-
-
-:math:`{{\mathrm{fvtestop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1)`
-...................................................................................
-
-
-1. Let :math:`{c_1^\ast}` be :math:`{{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}(v_1)`.
-
-#. Let :math:`{c^\ast}` be :math:`\epsilon`.
-
-#. For each :math:`c_1` in :math:`{c_1^\ast}`, do:
-
- a. Let :math:`c` be :math:`{{\mathrm{f}}}_{N}(c_1)`.
-
- #. Append :math:`c` to :math:`{c^\ast}`.
-
-#. Return :math:`{\Pi}\, {c^\ast}`.
-
-
:math:`{{\mathrm{ivrelop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1, v_2)`
.......................................................................................
@@ -24989,13 +24957,6 @@
#. Return :math:`{{\mathrm{fvternop}}}_{{{\mathit{lanetype}}}{\mathsf{x}}{M}}({\mathrm{frelaxed}}_{{\mathit{nmadd}}}, v_1, v_2, v_3)`.
-:math:`{\mathsf{all\_true}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v)}`
-......................................................................
-
-
-1. Return :math:`{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{iall}}_{{\mathit{true}}}, v)`.
-
-
:math:`{{\mathit{vrelop}}}{{}_{{{\mathit{lanetype}}}{\mathsf{x}}{M}}(v_1, v_2)}`
................................................................................
@@ -29296,7 +29257,7 @@
Step_pure/vvtestop V128 ANY_TRUE
1. Assert: Due to validation, a value of value type V128 is on the top of the stack.
2. Pop the value (V128.CONST c_1) from the stack.
-3. Let c be $ine_($vsize(V128), c_1, 0).
+3. Let c be $inez_($vsize(V128), c_1).
4. Push the value (I32.CONST c) to the stack.
Step_pure/vunop sh vunop
@@ -29329,11 +29290,12 @@
8. Let c be an element of $vternop_(sh, vternop, c_1, c_2, c_3).
9. Push the value (V128.CONST c) to the stack.
-Step_pure/vtestop sh vtestop
+Step_pure/vtestop Jnn X M ALL_TRUE
1. Assert: Due to validation, a value of value type V128 is on the top of the stack.
2. Pop the value (V128.CONST c_1) from the stack.
-3. Let i be $vtestop_(sh, vtestop, c_1).
-4. Push the value (I32.CONST i) to the stack.
+3. Let i* be $lanes_(Jnn X M, c_1).
+4. Let c be $prod($inez_($jsizenn(Jnn), i)*).
+5. Push the value (I32.CONST c) to the stack.
Step_pure/vrelop sh vrelop
1. Assert: Due to validation, a value of value type V128 is on the top of the stack.
@@ -31752,7 +31714,7 @@
ieqz_ N i_1
1. Return $bool((i_1 = 0)).
-iall_true_ N i_1
+inez_ N i_1
1. Return $bool((i_1 =/= 0)).
ieq_ N i_1 i_2
@@ -32062,22 +32024,6 @@
4. Let c** be $setproduct_(`lane_((Fnn : Fnn <: lanetype)), $f_($sizenn(Fnn), c_1, c_2, c_3)*).
5. Return $inv_lanes_(Fnn X M, c*)*.
-ivtestop_ Jnn X M $f_ v_1
-1. Let c_1* be $lanes_(Jnn X M, v_1).
-2. Let c* be [].
-3. For each c_1 in c_1*, do:
- a. Let c be $f_($lsizenn(Jnn), c_1).
- b. Append c to the c*.
-4. Return $prod(c*).
-
-fvtestop_ Fnn X M $f_ v_1
-1. Let c_1* be $lanes_(Fnn X M, v_1).
-2. Let c* be [].
-3. For each c_1 in c_1*, do:
- a. Let c be $f_($sizenn(Fnn), c_1).
- b. Append c to the c*.
-4. Return $prod(c*).
-
ivrelop_ Jnn X M $f_ v_1 v_2
1. Let c_1* be $lanes_(Jnn X M, v_1).
2. Let c_2* be $lanes_(Jnn X M, v_2).
@@ -32242,9 +32188,6 @@
4. Assert: Due to validation, (vternop_ = RELAXED_NMADD).
5. Return $fvternop_(lanetype X M, $frelaxed_nmadd_, v_1, v_2, v_3).
-vtestop_ Jnn X M ALL_TRUE v
-1. Return $ivtestop_(Jnn X M, $iall_true_, v).
-
vrelop_ lanetype X M vrelop_ v_1 v_2
1. If lanetype is Jnn, then:
a. If (vrelop_ = EQ), then:
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index 617e983..bfcc596 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -1625,7 +1625,6 @@
warning: definition `fvbinop_` was never spliced
warning: definition `fvrelop_` was never spliced
warning: definition `fvternop_` was never spliced
-warning: definition `fvtestop_` was never spliced
warning: definition `fvunop_` was never spliced
warning: definition `fzero` was never spliced
warning: definition `global` was never spliced
@@ -1641,7 +1640,6 @@
warning: definition `iabs_` was never spliced
warning: definition `iadd_` was never spliced
warning: definition `iadd_sat_` was never spliced
-warning: definition `iall_true_` was never spliced
warning: definition `iand_` was never spliced
warning: definition `iandnot_` was never spliced
warning: definition `iavgr_` was never spliced
@@ -1665,6 +1663,7 @@
warning: definition `imul_` was never spliced
warning: definition `ine_` was never spliced
warning: definition `ineg_` was never spliced
+warning: definition `inez_` was never spliced
warning: definition `inot_` was never spliced
warning: definition `inst_globaltype` was never spliced
warning: definition `inst_memtype` was never spliced
@@ -1724,7 +1723,6 @@
warning: definition `ivshufflop_` was never spliced
warning: definition `ivswizzlop_` was never spliced
warning: definition `ivternopnd_` was never spliced
-warning: definition `ivtestop_` was never spliced
warning: definition `ivunop_` was never spliced
warning: definition `ixor_` was never spliced
warning: definition `jsize` was never spliced
@@ -1862,7 +1860,6 @@
warning: definition `vsizenn` was never spliced
warning: definition `vswizzlop_` was never spliced
warning: definition `vternop_` was never spliced
-warning: definition `vtestop_` was never spliced
warning: definition `vunop_` was never spliced
warning: definition `vunpack` was never spliced
warning: definition `vvbinop_` was never spliced
@@ -2472,7 +2469,6 @@
warning: definition prose `fvbinop_` was never spliced
warning: definition prose `fvrelop_` was never spliced
warning: definition prose `fvternop_` was never spliced
-warning: definition prose `fvtestop_` was never spliced
warning: definition prose `fvunop_` was never spliced
warning: definition prose `fzero` was never spliced
warning: definition prose `global` was never spliced
@@ -2488,7 +2484,6 @@
warning: definition prose `iabs_` was never spliced
warning: definition prose `iadd_` was never spliced
warning: definition prose `iadd_sat_` was never spliced
-warning: definition prose `iall_true_` was never spliced
warning: definition prose `idiv_` was never spliced
warning: definition prose `ieq_` was never spliced
warning: definition prose `ieqz_` was never spliced
@@ -2503,6 +2498,7 @@
warning: definition prose `imul_` was never spliced
warning: definition prose `ine_` was never spliced
warning: definition prose `ineg_` was never spliced
+warning: definition prose `inez_` was never spliced
warning: definition prose `inst_globaltype` was never spliced
warning: definition prose `inst_memtype` was never spliced
warning: definition prose `inst_reftype` was never spliced
@@ -2539,7 +2535,6 @@
warning: definition prose `ivshufflop_` was never spliced
warning: definition prose `ivswizzlop_` was never spliced
warning: definition prose `ivternopnd_` was never spliced
-warning: definition prose `ivtestop_` was never spliced
warning: definition prose `ivunop_` was never spliced
warning: definition prose `jsize` was never spliced
warning: definition prose `jsizenn` was never spliced
@@ -2666,7 +2661,6 @@
warning: definition prose `vsizenn` was never spliced
warning: definition prose `vswizzlop_` was never spliced
warning: definition prose `vternop_` was never spliced
-warning: definition prose `vtestop_` was never spliced
warning: definition prose `vunop_` was never spliced
warning: definition prose `vunpack` was never spliced
warning: definition prose `vvbinop_` was never spliced
