Skip to content

Commit db886b8

Browse files
rossbergrossberg
committed
[spec] Unbreak all_true again
1 parent 8e4f613 commit db886b8

File tree

12 files changed

+64
-238
lines changed

12 files changed

+64
-238
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -478,7 +478,7 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non
478478
Instruction(2.0, r'\I8X16.\VABS', r'\hex{FD}~~\hex{60}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'),
479479
Instruction(2.0, r'\I8X16.\VNEG', r'\hex{FD}~~\hex{61}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ineg'),
480480
Instruction(2.0, r'\I8X16.\VPOPCNT', r'\hex{FD}~~\hex{62}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-ipopcnt'),
481-
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'),
481+
Instruction(2.0, r'\I8X16.\VALLTRUE', r'\hex{FD}~~\hex{63}', r'[\V128] \to [\I32]', r'valid-vtestop', r'exec-vtestop'),
482482
Instruction(2.0, r'\I8X16.\VBITMASK', r'\hex{FD}~~\hex{64}', r'[\V128] \to [\I32]', r'valid-vbitmask', r'exec-vbitmask', r'op-ivbitmask'),
483483
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'),
484484
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'),

‎document/core/exec/numerics.rst‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -583,16 +583,16 @@ The integer result of predicates -- i.e., :ref:`tests <syntax-testop>` and :ref:
583583
\end{array}
584584
585585
586-
.. _op-iall_true:
586+
.. _op-inez:
587587

588-
:math:`\ialltrue_N(i)`
589-
......................
588+
:math:`\inez_N(i)`
589+
..................
590590

591591
* Return :math:`0` if :math:`i` is zero, :math:`1` otherwise.
592592

593593
.. math::
594594
\begin{array}{@{}lcll}
595-
\ialltrue_N(i) &=& \tobool(i \neq 0)
595+
\inez_N(i) &=& \tobool(i \neq 0)
596596
\end{array}
597597
598598

‎document/core/util/macros.def‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1597,7 +1597,7 @@
15971597
.. |ictz| mathdef:: \xref{exec/numerics}{op-ictz}{\F{ictz}}
15981598
.. |ipopcnt| mathdef:: \xref{exec/numerics}{op-ipopcnt}{\F{ipopcnt}}
15991599
.. |ieqz| mathdef:: \xref{exec/numerics}{op-ieqz}{\F{ieqz}}
1600-
.. |ialltrue| mathdef:: \xref{exec/numerics}{op-iall_true}{\F{iall\_true}}
1600+
.. |inez| mathdef:: \xref{exec/numerics}{op-inez}{\F{inez}}
16011601
.. |ieq| mathdef:: \xref{exec/numerics}{op-ieq}{\F{ieq}}
16021602
.. |ine| mathdef:: \xref{exec/numerics}{op-ine}{\F{ine}}
16031603
.. |ilt| mathdef:: \xref{exec/numerics}{op-ilt}{\F{ilt}}

‎specification/wasm-3.0/3.1-numerics.scalar.spectec‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ def $ibitselect_(N, iN(N), iN(N), iN(N)) : iN(N)
132132
def $irelaxed_laneselect_(N, iN(N), iN(N), iN(N)) : iN(N)*
133133

134134
def $ieqz_(N, iN(N)) : u32
135-
def $iall_true_(N, iN(N)) : u32 hint(show $iall__true_(%1,%2))
135+
def $inez_(N, iN(N)) : u32
136136

137137
def $ieq_(N, iN(N), iN(N)) : u32
138138
def $ine_(N, iN(N), iN(N)) : u32
@@ -217,7 +217,7 @@ def $irelaxed_laneselect_ hint(builtin)
217217

218218
def $ieqz_(N, i_1) = $bool(i_1 = 0)
219219

220-
def $iall_true_(N, i_1) = $bool(i_1 =/= 0)
220+
def $inez_(N, i_1) = $bool(i_1 =/= 0)
221221

222222

223223
def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2)

‎specification/wasm-3.0/3.2-numerics.vector.spectec‎

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -62,9 +62,6 @@ def $fvbinop_(shape, def $f_(N, fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128))
6262
def $ivternopnd_(shape, def $f_(N, iN(N), iN(N), iN(N)) : iN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
6363
def $fvternop_(shape, def $f_(N, fN(N), fN(N), fN(N)) : fN(N)*, vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
6464

65-
def $ivtestop_(shape, def $f_(N, iN(N)) : u32, vec_(V128)) : u32
66-
def $fvtestop_(shape, def $f_(N, fN(N)) : u32, vec_(V128)) : u32
67-
6865
def $ivrelop_(shape, def $f_(N, iN(N), iN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128)
6966
def $ivrelopsx_(shape, def $f_(N, sx, iN(N), iN(N)) : u32, sx, vec_(V128), vec_(V128)) : vec_(V128)
7067
def $fvrelop_(shape, def $f_(N, fN(N), fN(N)) : u32, vec_(V128), vec_(V128)) : vec_(V128)
@@ -120,15 +117,6 @@ def $fvternop_(Fnn X M, def $f_, v_1, v_2, v_3) = $inv_lanes_(Fnn X M, c*)*
120117
-- if c** = $setproduct_(lane_(Fnn), $f_($sizenn(Fnn), c_1, c_2, c_3)*)
121118

122119

123-
def $ivtestop_(Jnn X M, def $f_, v_1) = $prod(c*)
124-
-- if c_1* = $lanes_(Jnn X M, v_1)
125-
-- if c* = $f_($lsizenn(Jnn), c_1)*
126-
127-
def $fvtestop_(Fnn X M, def $f_, v_1) = $prod(c*)
128-
-- if c_1* = $lanes_(Fnn X M, v_1)
129-
-- if c* = $f_($sizenn(Fnn), c_1)*
130-
131-
132120
def $ivrelop_(Jnn X M, def $f_, v_1, v_2) = $inv_lanes_(Jnn X M, c*)
133121
-- if c_1* = $lanes_(Jnn X M, v_1)
134122
-- if c_2* = $lanes_(Jnn X M, v_2)
@@ -187,8 +175,6 @@ def $vbinop_(shape, vbinop_(shape), vec_(V128), vec_(V128)) : vec_(V128)*
187175
hint(show %2#$_(%1,%3,%4))
188176
def $vternop_(shape, vternop_(shape), vec_(V128), vec_(V128), vec_(V128)) : vec_(V128)*
189177
hint(show %2#$_(%1,%3,%4,%5))
190-
def $vtestop_(shape, vtestop_(shape), vec_(V128)) : u32
191-
hint(show %2#$_(%1,%3))
192178
def $vrelop_(shape, vrelop_(shape), vec_(V128), vec_(V128)) : vec_(V128)
193179
hint(show %2#$_(%1,%3,%4))
194180

@@ -265,8 +251,6 @@ def $vternop_(Jnn X M, RELAXED_LANESELECT, v_1, v_2, v_3) = $ivternopnd_(Jnn X M
265251
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)
266252
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)
267253

268-
def $vtestop_(Jnn X M, ALL_TRUE, v) = $ivtestop_(Jnn X M, $iall_true_, v)
269-
270254
def $vrelop_(Jnn X M, EQ, v_1, v_2) = $ivrelop_(Jnn X M, $ieq_, v_1, v_2)
271255
def $vrelop_(Jnn X M, NE, v_1, v_2) = $ivrelop_(Jnn X M, $ine_, v_1, v_2)
272256
def $vrelop_(Jnn X M, LT sx, v_1, v_2) = $ivrelopsx_(Jnn X M, $ilt_, sx, v_1, v_2)

‎specification/wasm-3.0/4.3-execution.instructions.spectec‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -992,7 +992,7 @@ rule Step_pure/vvternop:
992992

993993
rule Step_pure/vvtestop:
994994
(VCONST V128 c_1) (VVTESTOP V128 ANY_TRUE) ~> (CONST I32 c)
995-
-- if c = $ine_($vsize(V128), c_1, 0)
995+
-- if c = $inez_($vsize(V128), c_1)
996996

997997

998998
rule Step_pure/vunop-val:
@@ -1023,8 +1023,9 @@ rule Step_pure/vternop-trap:
10231023

10241024

10251025
rule Step_pure/vtestop:
1026-
(VCONST V128 c_1) (VTESTOP sh vtestop) ~> (CONST I32 i)
1027-
-- if i = $vtestop_(sh, vtestop, c_1)
1026+
(VCONST V128 c_1) (VTESTOP (Jnn X M) ALL_TRUE) ~> (CONST I32 c)
1027+
-- if i* = $lanes_(Jnn X M, c_1)
1028+
-- if c = $prod(($inez_($jsizenn(Jnn), i)*))
10281029

10291030

10301031
rule Step_pure/vrelop:

‎spectec/doc/example/output/NanoWasm.pdf‎

0 Bytes
Binary file not shown.

‎spectec/test-frontend/TEST.md‎

Lines changed: 7 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -4609,9 +4609,9 @@ def $ieqz_(N : N, iN : iN(N)) : u32
46094609
def $ieqz_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 = 0)))
46104610

46114611
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
4612-
def $iall_true_(N : N, iN : iN(N)) : u32
4612+
def $inez_(N : N, iN : iN(N)) : u32
46134613
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
4614-
def $iall_true_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
4614+
def $inez_{N : N, i_1 : iN(N)}(N, i_1) = `%`_u32($bool((i_1!`%`_iN.0 =/= 0)))
46154615

46164616
;; ../../../../specification/wasm-3.0/3.1-numerics.scalar.spectec
46174617
def $ieq_(N : N, iN : iN(N), iN : iN(N)) : u32
@@ -5036,20 +5036,6 @@ def $fvternop_(shape : shape, def $f_(N : N, fN : fN(N), fN : fN(N), fN : fN(N))
50365036
-- if (c_3*{c_3 <- `c_3*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_3))
50375037
-- 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*`}))
50385038

5039-
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
5040-
def $ivtestop_(shape : shape, def $f_(N : N, iN : iN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
5041-
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
5042-
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*`}))
5043-
-- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), v_1))
5044-
-- if (c*{c <- `c*`} = $f_($lsizenn((Jnn : Jnn <: lanetype)), c_1)*{c_1 <- `c_1*`})
5045-
5046-
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
5047-
def $fvtestop_(shape : shape, def $f_(N : N, fN : fN(N)) : u32, vec_ : vec_(V128_Vnn)) : u32
5048-
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
5049-
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*`}))
5050-
-- if (c_1*{c_1 <- `c_1*`} = $lanes_(`%X%`_shape((Fnn : Fnn <: lanetype), `%`_dim(M)), v_1))
5051-
-- if (c*{c <- `c*`} = $f_($sizenn((Fnn : Fnn <: numtype)), c_1)*{c_1 <- `c_1*`})
5052-
50535039
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
50545040
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)
50555041
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
@@ -5208,11 +5194,6 @@ def $vternop_(shape : shape, vternop_ : vternop_(shape), vec_ : vec_(V128_Vnn),
52085194
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
52095195
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)
52105196

5211-
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
5212-
def $vtestop_(shape : shape, vtestop_ : vtestop_(shape), vec_ : vec_(V128_Vnn)) : u32
5213-
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
5214-
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)
5215-
52165197
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
52175198
def $vrelop_(shape : shape, vrelop_ : vrelop_(shape), vec_ : vec_(V128_Vnn), vec_ : vec_(V128_Vnn)) : vec_(V128_Vnn)
52185199
;; ../../../../specification/wasm-3.0/3.2-numerics.vector.spectec
@@ -6221,7 +6202,7 @@ relation Step_pure: `%~>%`(instr*, instr*)
62216202
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
62226203
rule vvtestop{c_1 : vec_(V128_Vnn), c : num_(I32_numtype)}:
62236204
`%~>%`([VCONST_instr(V128_vectype, c_1) VVTESTOP_instr(V128_vectype, ANY_TRUE_vvtestop)], [CONST_instr(I32_numtype, c)])
6224-
-- if (c = $ine_($vsize(V128_vectype), c_1, `%`_iN(0)))
6205+
-- if (c = $inez_($vsize(V128_vectype), c_1))
62256206

62266207
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
62276208
rule `vunop-val`{c_1 : vec_(V128_Vnn), sh : shape, vunop : vunop_(sh), c : vec_(V128_Vnn)}:
@@ -6254,9 +6235,10 @@ relation Step_pure: `%~>%`(instr*, instr*)
62546235
-- if ($vternop_(sh, vternop, c_1, c_2, c_3) = [])
62556236

62566237
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
6257-
rule vtestop{c_1 : vec_(V128_Vnn), sh : shape, vtestop : vtestop_(sh), i : num_(I32_numtype)}:
6258-
`%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(sh, vtestop)], [CONST_instr(I32_numtype, i)])
6259-
-- if (i = $vtestop_(sh, vtestop, c_1))
6238+
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))))*}:
6239+
`%~>%`([VCONST_instr(V128_vectype, c_1) VTESTOP_instr(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), ALL_TRUE_vtestop_)], [CONST_instr(I32_numtype, c)])
6240+
-- if (i*{i <- `i*`} = $lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c_1))
6241+
-- if (c!`%`_num_.0 = $prod($inez_($jsizenn(Jnn), i)!`%`_u32.0*{i <- `i*`}))
62606242

62616243
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
62626244
rule vrelop{c_1 : vec_(V128_Vnn), c_2 : vec_(V128_Vnn), sh : shape, vrelop : vrelop_(sh), c : vec_(V128_Vnn)}:

‎spectec/test-latex/TEST.md‎

Lines changed: 7 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -8106,7 +8106,7 @@ $$
81068106

81078107
$$
81088108
\begin{array}[t]{@{}lcl@{}l@{}}
8109-
{{\mathrm{iall\_true}}}_{N}(i_1) & = & \mathbb{B}(i_1 \neq 0) \\
8109+
{{\mathrm{inez}}}_{N}(i_1) & = & \mathbb{B}(i_1 \neq 0) \\
81108110
\end{array}
81118111
$$
81128112

@@ -8462,28 +8462,6 @@ $$
84628462

84638463
\vspace{1ex}
84648464

8465-
$$
8466-
\begin{array}[t]{@{}lcl@{}l@{}}
8467-
{{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1) & = & {\Pi}\, {c^\ast} & \quad
8468-
\begin{array}[t]{@{}l@{}}
8469-
\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v_1) \\
8470-
{\land}~ {c^\ast} = {{{\mathrm{f}}}_{N}(c_1)^\ast} \\
8471-
\end{array} \\
8472-
\end{array}
8473-
$$
8474-
8475-
$$
8476-
\begin{array}[t]{@{}lcl@{}l@{}}
8477-
{{\mathrm{fvtestop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}({\mathrm{f}}, v_1) & = & {\Pi}\, {c^\ast} & \quad
8478-
\begin{array}[t]{@{}l@{}}
8479-
\mbox{if}~ {c_1^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}}(v_1) \\
8480-
{\land}~ {c^\ast} = {{{\mathrm{f}}}_{N}(c_1)^\ast} \\
8481-
\end{array} \\
8482-
\end{array}
8483-
$$
8484-
8485-
\vspace{1ex}
8486-
84878465
$$
84888466
\begin{array}[t]{@{}lcl@{}l@{}}
84898467
{{\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
@@ -8651,12 +8629,6 @@ $$
86518629
\end{array}
86528630
$$
86538631

8654-
$$
8655-
\begin{array}[t]{@{}lcl@{}l@{}}
8656-
{\mathsf{all\_true}}{{}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(v)} & = & {{\mathrm{ivtestop}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}({\mathrm{iall}}_{{\mathit{true}}}, v) \\
8657-
\end{array}
8658-
$$
8659-
86608632
$$
86618633
\begin{array}[t]{@{}lcl@{}l@{}}
86628634
{\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) \\
@@ -10743,7 +10715,7 @@ $$
1074310715

1074410716
$$
1074510717
\begin{array}[t]{@{}lrcl@{}l@{}}
10746-
{[\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) \\
10718+
{[\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) \\
1074710719
\end{array}
1074810720
$$
1074910721

@@ -10778,7 +10750,11 @@ $$
1077810750

1077910751
$$
1078010752
\begin{array}[t]{@{}lrcl@{}l@{}}
10781-
{[\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)} \\
10753+
{[\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
10754+
\begin{array}[t]{@{}l@{}}
10755+
\mbox{if}~ {i^\ast} = {{\mathrm{lanes}}}_{{{\mathsf{i}}{N}}{\mathsf{x}}{M}}(c_1) \\
10756+
{\land}~ c = {\Pi}\, ({{{\mathrm{inez}}}_{N}(i)^\ast}) \\
10757+
\end{array} \\
1078210758
\end{array}
1078310759
$$
1078410760

0 commit comments

Comments
 (0)