@@ -513,31 +513,31 @@ Most other vector instructions are defined in terms of numeric operators that ar
513
513
514
514
1. Assert: due to :ref: `validation <valid-vec-replace_lane >`, :math: `x < \dim (\shape )`.
515
515
516
- 2. Let :math: `t_ 1 ` be the type :math: `\unpacked (\shape )`.
516
+ 2. Let :math: `t_ 2 ` be the type :math: `\unpacked (\shape )`.
517
517
518
518
3. Assert: due to :ref: `validation <valid-vec-replace_lane >`, a value of :ref: `value type <syntax-valtype >` :math: `t_1 ` is on the top of the stack.
519
519
520
- 4. Pop the value :math: `t_ 1 .\CONST ~c_ 1 ` from the stack.
520
+ 4. Pop the value :math: `t_ 2 .\CONST ~c_ 2 ` from the stack.
521
521
522
522
5. Assert: due to :ref: `validation <valid-vec-replace_lane >`, a value of :ref: `value type <syntax-valtype >` |V128 | is on the top of the stack.
523
523
524
- 6. Pop the value :math: `\V128 .\VCONST ~c_ 2 ` from the stack.
524
+ 6. Pop the value :math: `\V128 .\VCONST ~c_ 1 ` from the stack.
525
525
526
- 7. Let :math: `i^\ast ` be the result of computing :math: `\lanes _{\shape }(c_ 2 )`.
526
+ 7. Let :math: `i^\ast ` be the result of computing :math: `\lanes _{\shape }(c_ 1 )`.
527
527
528
- 8. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 1 )`.
528
+ 8. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 2 )`.
529
529
530
530
9. Push :math: `\V128 .\VCONST ~c` on the stack.
531
531
532
532
.. math ::
533
533
\begin {array}{l}
534
534
\begin {array}{lcl@{\qquad }l}
535
- (t_ 1 \ K {.}\CONST ~c_1 )~(\V 128 \ K {.}\VCONST ~c_2 )~(\shape\K {.}\REPLACELANE ~x) &\stepto & (\V128 \K {.}\VCONST ~c)
535
+ (\V 128 \ K {.}\VCONST ~c_1 )~(t_ 2 \ K {.}\CONST ~c_2 )~(\shape\K {.}\REPLACELANE ~x) &\stepto & (\V128 \K {.}\VCONST ~c)
536
536
\end {array}
537
537
\\ \qquad
538
538
\begin {array}[t]{@{}r@{~}l@{}}
539
- (\iff & i^\ast = \lanes _{\shape }(c_ 2 ) \\
540
- \wedge & c = \lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 1 ))
539
+ (\iff & i^\ast = \lanes _{\shape }(c_ 1 ) \\
540
+ \wedge & c = \lanes ^{-1 }_{\shape }(i^\ast \with [x] = c_ 2 ))
541
541
\end {array}
542
542
\end {array}
543
543
@@ -837,8 +837,8 @@ where:
837
837
\end {array}
838
838
839
839
840
- :math: `t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx\K {\_zero}`
841
- ...............................................................
840
+ :math: `t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx ^? \K {\_zero}`
841
+ .................................................................
842
842
843
843
1. Assert: due to :ref: `syntax <syntax-instr-vec >`, :math: `N = 2 \cdot M`.
844
844
@@ -848,7 +848,7 @@ where:
848
848
849
849
4. Let :math: `i^\ast ` be the result of computing :math: `\lanes _{t_1 \K {x}M}(c_1 )`.
850
850
851
- 5. Let :math: `j^\ast ` be the result of computing :math: `\vcvtop ^{\sx }_{|t_1 |,|t_2 |}(i^\ast )`.
851
+ 5. Let :math: `j^\ast ` be the result of computing :math: `\vcvtop ^{\sx ^? }_{|t_1 |,|t_2 |}(i^\ast )`.
852
852
853
853
6. Let :math: `k^\ast ` be the concatenation of the two sequences :math: `j^\ast ` and :math: `0 ^M`.
854
854
@@ -859,11 +859,11 @@ where:
859
859
.. math ::
860
860
\begin {array}{l}
861
861
\begin {array}{lcl@{\qquad }l}
862
- (\V128 \K {.}\VCONST ~c_1 )~t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx\K {\_zero} &\stepto & (\V128 \K {.}\VCONST ~c) \\
862
+ (\V128 \K {.}\VCONST ~c_1 )~t_2 \K {x}N\K {.}\vcvtop\K {\_ }t_1 \K {x}M\K {\_ }\sx ^? \K {\_zero} &\stepto & (\V128 \K {.}\VCONST ~c) \\
863
863
\end {array}
864
864
\\ \qquad
865
865
\begin {array}[t]{@{}r@{~}l@{}}
866
- (\iff & c = \lanes ^{-1 }_{t_2 \K {x}N}(\vcvtop ^{\sx }_{|t_1 |,|t_2 |}(\lanes _{t_1 \K {x}M}(c_1 ))~0 ^M))
866
+ (\iff & c = \lanes ^{-1 }_{t_2 \K {x}N}(\vcvtop ^{\sx ^? }_{|t_1 |,|t_2 |}(\lanes _{t_1 \K {x}M}(c_1 ))~0 ^M))
867
867
\end {array}
868
868
\end {array}
869
869
@@ -942,7 +942,7 @@ where:
942
942
943
943
10. Let :math: `k_2 ^\ast ` be the result of computing :math: `\extend ^{\sx }_{|t_1 |,|t_2 |}(j_2 ^\ast )`.
944
944
945
- 11. Let :math: `k^\ast ` be the result of computing :math: `\imul _{t_2 \K {x}N }(k_1 ^\ast , k_2 ^\ast )`.
945
+ 11. Let :math: `k^\ast ` be the result of computing :math: `\imul _{| t_2 | }(k_1 ^\ast , k_2 ^\ast )`.
946
946
947
947
12. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{t_2 \K {x}N}(k^\ast )`.
948
948
@@ -956,7 +956,7 @@ where:
956
956
\begin {array}[t]{@{}r@{~}l@{}}
957
957
(\iff & i^\ast = \lanes _{t_1 \K {x}M}(c_1 )[\half (0 , N) \slice N] \\
958
958
\wedge & j^\ast = \lanes _{t_1 \K {x}M}(c_2 )[\half (0 , N) \slice N] \\
959
- \wedge & c = \lanes ^{-1 }_{t_2 \K {x}N}(\imul _{t_2 \K {x}N }(\extend ^{\sx }_{|t_1 |,|t_2 |}(i^\ast ), \extend ^{\sx }_{|t_1 |,|t_2 |}(j^\ast ))))
959
+ \wedge & c = \lanes ^{-1 }_{t_2 \K {x}N}(\imul _{| t_2 | }(\extend ^{\sx }_{|t_1 |,|t_2 |}(i^\ast ), \extend ^{\sx }_{|t_1 |,|t_2 |}(j^\ast ))))
960
960
\end {array}
961
961
962
962
where:
@@ -983,7 +983,7 @@ where:
983
983
984
984
5. Let :math: `(j_1 ~j_2 )^\ast ` be the result of computing :math: `\extend ^{\sx }_{|t_1 |,|t_2 |}(i^\ast )`.
985
985
986
- 6. Let :math: `k^\ast ` be the result of computing :math: `\iadd _{N }(j_1 , j_2 )^\ast `.
986
+ 6. Let :math: `k^\ast ` be the result of computing :math: `\iadd _{|t_ 2 | }(j_1 , j_2 )^\ast `.
987
987
988
988
7. Let :math: `c` be the result of computing :math: `\lanes ^{-1 }_{t_2 \K {x}N}(k^\ast )`.
989
989
@@ -997,7 +997,7 @@ where:
997
997
\\ \qquad
998
998
\begin {array}[t]{@{}r@{~}l@{}}
999
999
(\iff & (i_1 ~i_2 )^\ast = \extend ^{\sx }_{|t_1 |,|t_2 |}(\lanes _{t_1 \K {x}M}(c_1 )) \\
1000
- \wedge & j^\ast = \iadd _{N }(i_1 , i_2 )^\ast \\
1000
+ \wedge & j^\ast = \iadd _{|t_ 2 | }(i_1 , i_2 )^\ast \\
1001
1001
\wedge & c = \lanes ^{-1 }_{t_2 \K {x}N}(j^\ast ))
1002
1002
\end {array}
1003
1003
\end {array}
0 commit comments