@@ -819,14 +819,14 @@ Reference Instructions
819
819
S; F; (\I32 .\CONST ~s)~(\I32 .\CONST ~n)~(\ARRAYNEWDATA ~x~y) &\stepto & \TRAP
820
820
\\&&
821
821
\begin {array}[t]{@{}r@{~}l@{}}
822
- (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft}^n \\
822
+ (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft} \\
823
823
\land & s + n\cdot |\X {ft}|/8 > |S.\SDATAS [F.\AMODULE .\MIDATAS [y]].\DIDATA |)
824
824
\end {array} \\
825
825
\\[ 1 ex]
826
826
S; F; (\I32 .\CONST ~s)~(\I32 .\CONST ~n)~(\ARRAYNEWDATA ~x~y) &\stepto & (t.\CONST ~c)^n~(\ARRAYNEWFIXED ~x~n)
827
827
\\&&
828
828
\begin {array}[t]{@{}r@{~}l@{}}
829
- (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft}^n \\
829
+ (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft} \\
830
830
\land & t = \unpacktype (\X {ft}) \\
831
831
\land & \concat ((\bytes _{\X {ft}}(c))^n) = S.\SDATAS [F.\AMODULE .\MIDATAS [y]].\DIDATA [s \slice n\cdot |\X {ft}|/8 ] \\
832
832
\end {array} \\
@@ -1065,7 +1065,7 @@ Reference Instructions
1065
1065
1066
1066
12. Assert: due to :ref: `validation <valid-array.fill >`, the :ref: `array instance <syntax-arrayinst >` :math: `S.\SARRAYS [a]` exists.
1067
1067
1068
- 13. If :math: `d + n` is larger than or equal to the length of :math: `S.\SARRAYS [a].\AIFIELDS `, then:
1068
+ 13. If :math: `d + n` is larger than the length of :math: `S.\SARRAYS [a].\AIFIELDS `, then:
1069
1069
1070
1070
a. Trap.
1071
1071
@@ -1102,13 +1102,13 @@ Reference Instructions
1102
1102
(\iff d + n > |S.\SARRAYS [a].\AIFIELDS |)
1103
1103
\\[ 1 ex]
1104
1104
S; (\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~\val ~(\I32 .\CONST ~0 )~(\ARRAYFILL ~x)
1105
- \quad\stepto\quad S; \epsilon
1105
+ \quad\stepto\quad \epsilon
1106
1106
\\ \qquad
1107
1107
(\otherwise )
1108
1108
\\[ 1 ex]
1109
1109
S; (\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~\val ~(\I32 .\CONST ~n+1 )~(\ARRAYFILL ~x)
1110
1110
\quad\stepto
1111
- \\ \quad S;
1111
+ \\ \quad
1112
1112
\begin {array}[t]{@{}l@{}}
1113
1113
(\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~\val ~(\ARRAYSET ~x) \\
1114
1114
(\REFARRAYADDR ~a)~(\I32 .\CONST ~d+1 )~\val ~(\I32 .\CONST ~n)~(\ARRAYFILL ~x) \\
@@ -1175,11 +1175,11 @@ Reference Instructions
1175
1175
1176
1176
23. Assert: due to :ref: `validation <valid-array.copy >`, the :ref: `array instance <syntax-arrayinst >` :math: `S.\SARRAYS [a_2 ]` exists.
1177
1177
1178
- 24. If :math: `d + n` is larger than or equal to the length of :math: `S.\SARRAYS [a_1 ].\AIFIELDS `, then:
1178
+ 24. If :math: `d + n` is larger than the length of :math: `S.\SARRAYS [a_1 ].\AIFIELDS `, then:
1179
1179
1180
1180
a. Trap.
1181
1181
1182
- 25. If :math: `s + n` is larger than or equal to the length of :math: `S.\SARRAYS [a_2 ].\AIFIELDS `, then:
1182
+ 25. If :math: `s + n` is larger than the length of :math: `S.\SARRAYS [a_2 ].\AIFIELDS `, then:
1183
1183
1184
1184
a. Trap.
1185
1185
@@ -1252,7 +1252,7 @@ Reference Instructions
1252
1252
(\iff d + n > |S.\SARRAYS [a_1 ].\AIFIELDS | \vee s + n > |S.\SARRAYS [a_2 ].\AIFIELDS |)
1253
1253
\\[ 1 ex]
1254
1254
S; F; (\REFARRAYADDR ~a_1 )~(\I32 .\CONST ~d)~(\REFARRAYADDR ~a_2 )~(\I32 .\CONST ~s)~(\I32 .\CONST ~0 )~(\ARRAYCOPY ~x~y)
1255
- \quad\stepto\quad S; \epsilon
1255
+ \quad\stepto\quad \epsilon
1256
1256
\\ \qquad
1257
1257
(\otherwise )
1258
1258
\\[ 1 ex]
@@ -1391,13 +1391,13 @@ Where:
1391
1391
\end {array}
1392
1392
\\[ 1 ex]
1393
1393
S; F; (\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~0 )~(\ARRAYINITDATA ~x~y)
1394
- \quad\stepto\quad S; F; \epsilon
1394
+ \quad\stepto\quad \epsilon
1395
1395
\\ \qquad
1396
1396
(\otherwise )
1397
1397
\\[ 1 ex]
1398
1398
S; F; (\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~n+1 )~(\ARRAYINITDATA ~x~y)
1399
1399
\quad\stepto
1400
- \\ \quad S; F;
1400
+ \\ \quad
1401
1401
\begin {array}[t]{@{}l@{}}
1402
1402
(\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~(t.\CONST ~c)~(\ARRAYSET ~x) \\
1403
1403
(\REFARRAYADDR ~a)~(\I32 .\CONST ~d+1 )~(\I32 .\CONST ~s+|\X {ft}|/8 )~(\I32 .\CONST ~n)~(\ARRAYINITDATA ~x~y) \\
@@ -1497,13 +1497,13 @@ Where:
1497
1497
\end {array}
1498
1498
\\[ 1 ex]
1499
1499
S; F; (\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~0 )~(\ARRAYINITELEM ~x~y)
1500
- \quad\stepto\quad S; F; \epsilon
1500
+ \quad\stepto\quad \epsilon
1501
1501
\\ \qquad
1502
1502
(\otherwise )
1503
1503
\\[ 1 ex]
1504
1504
S; F; (\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~n+1 )~(\ARRAYINITELEM ~x~y)
1505
1505
\quad\stepto
1506
- \\ \quad S; F;
1506
+ \\ \quad
1507
1507
\begin {array}[t]{@{}l@{}}
1508
1508
(\REFARRAYADDR ~a)~(\I32 .\CONST ~d)~\REF ~(\ARRAYSET ~x) \\
1509
1509
(\REFARRAYADDR ~a)~(\I32 .\CONST ~d+1 )~(\I32 .\CONST ~s+1 )~(\I32 .\CONST ~n)~(\ARRAYINITELEM ~x~y) \\
@@ -1538,7 +1538,7 @@ Where:
1538
1538
1539
1539
.. math ::
1540
1540
\begin {array}{lcl@{\qquad }l}
1541
- (\REFNULL \X {ht})~\ANYCONVERTEXTERN &\stepto & (\REFNULL ~\ANY ) \\
1541
+ (\REFNULL ~ \X {ht})~\ANYCONVERTEXTERN &\stepto & (\REFNULL ~\ANY ) \\
1542
1542
(\REFEXTERN ~\reff )~\ANYCONVERTEXTERN &\stepto & \reff \\
1543
1543
\end {array}
1544
1544
@@ -1564,8 +1564,8 @@ Where:
1564
1564
1565
1565
.. math ::
1566
1566
\begin {array}{lcl@{\qquad }l}
1567
- (\REFNULL \X {ht})~\EXTERNCONVERTANY &\stepto & (\REFNULL ~\EXTERN ) \\
1568
- \reff ~\EXTERNCONVERTANY &\stepto & (\REFEXTERN ~\reff ) & (\iff \reff \neq (\REFNULL \X {ht})) \\
1567
+ (\REFNULL ~ \X {ht})~\EXTERNCONVERTANY &\stepto & (\REFNULL ~\EXTERN ) \\
1568
+ \reff ~\EXTERNCONVERTANY &\stepto & (\REFEXTERN ~\reff ) & (\iff \reff \neq (\REFNULL ~ \X {ht})) \\
1569
1569
\end {array}
1570
1570
1571
1571
@@ -4376,8 +4376,8 @@ Control Instructions
4376
4376
.. math ::
4377
4377
\begin {array}{lcl@{\qquad }l}
4378
4378
S; F; \reff ~(\BRONCAST ~l~\X {rt}_1 ~\X {rt}_2 ) &\stepto & \reff ~(\BR ~l)
4379
- & (\iff S \vdashval \reff : \X {rt}
4380
- \land \vdashreftypematch \X {rt} \matchesreftype \insttype _{F.\AMODULE }(\X {rt}_2 )) \\
4379
+ & (\iff S \vdashval \reff : \X {rt}}
4380
+ \land {} \vdashreftypematch \X {rt} \matchesreftype \insttype _{F.\AMODULE }(\X {rt}_2 )) \\
4381
4381
S; F; \reff ~(\BRONCAST ~l~\X {rt}_1 ~\X {rt}_2 ) &\stepto & \reff
4382
4382
& (\otherwise ) \\
4383
4383
\end {array}
@@ -4412,7 +4412,7 @@ Control Instructions
4412
4412
\begin {array}{lcl@{\qquad }l}
4413
4413
S; F; \reff ~(\BRONCASTFAIL ~l~\X {rt}_1 ~\X {rt}_2 ) &\stepto & \reff
4414
4414
& (\iff S \vdashval \reff : \X {rt}
4415
- \land \vdashreftypematch \X {rt} \matchesreftype \insttype _{F.\AMODULE }(\X {rt}_2 )) \\
4415
+ \land {} \vdashreftypematch \X {rt} \matchesreftype \insttype _{F.\AMODULE }(\X {rt}_2 )) \\
4416
4416
S; F; \reff ~(\BRONCASTFAIL ~l~\X {rt}_1 ~\X {rt}_2 ) &\stepto & \reff ~(\BR ~l)
4417
4417
& (\otherwise ) \\
4418
4418
\end {array}
0 commit comments