From d8608557cee853458b78fa48267d6c7b4ef04355 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Thu, 20 Jul 2023 11:50:48 -0700 Subject: [PATCH 1/4] Execution prose for bulk array operations Add execution prose for array.fill, array.copy, array.init_data, and array.init_elem. As a drive by consistency fix, also remove unnecessary parentheses around values in the prose for other GC instructions. These parentheses do not appear in the prose for any other instruction. --- document/core/exec/instructions.rst | 354 +++++++++++++++++++++++++--- 1 file changed, 327 insertions(+), 27 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index dffae6da0..f39f3d65e 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -382,7 +382,7 @@ Reference Instructions 1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` |I32| is on the top of the stack. -2. Pop the value :math:`(\I32.\CONST~i)` from the stack. +2. Pop the value :math:`\I32.\CONST~i` from the stack. 3. Let :math:`j` be the result of computing :math:`\wrap_{32,31}(i)`. @@ -409,11 +409,11 @@ Reference Instructions 4. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`scalar reference `. -5. Let :math:`(\REFI31~i)` be the reference value :math:`\reff`. +5. Let :math:`\REFI31~i` be the reference value :math:`\reff`. 6. Let :math:`j` be the result of computing :math:`\extend^{\sx}_{31,32}(i)`. -7. Push the value :math:`(\I32.\CONST~j)` to the stack. +7. Push the value :math:`\I32.\CONST~j` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} @@ -546,7 +546,7 @@ Reference Instructions 9. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`structure reference `. -10. Let :math:`(\REFSTRUCTADDR~a)` be the reference value :math:`\reff`. +10. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. 11. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`i + 1` fields. @@ -599,7 +599,7 @@ Reference Instructions 11. Assert: due to :ref:`validation `, a :math:`\reff` is a :ref:`structure reference `. -12. Let :math:`(\REFSTRUCTADDR~a)` be the reference value :math:`\reff`. +12. Let :math:`\REFSTRUCTADDR~a` be the reference value :math:`\reff`. 13. Assert: due to :ref:`validation `, the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]` exists and has at least :math:`i + 1` fields. @@ -636,7 +636,7 @@ Reference Instructions 5. Assert: due to :ref:`validation `, a :ref:`value ` of type :math:`\I32` is on the top of the stack. -6. Pop the value :math:`(\I32.\CONST~n)` from the stack. +6. Pop the value :math:`\I32.\CONST~n` from the stack. 7. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. @@ -681,7 +681,7 @@ Reference Instructions 5. Assert: due to :ref:`validation `, a :ref:`value ` of type :math:`\I32` is on the top of the stack. -6. Pop the value :math:`(\I32.\CONST~n)` from the stack. +6. Pop the value :math:`\I32.\CONST~n` from the stack. 7. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. @@ -784,9 +784,9 @@ Reference Instructions 9. Assert: due to :ref:`validation `, two :ref:`values ` of type :math:`\I32` are on the top of the stack. -10. Pop the value :math:`(\I32.\CONST~n)` from the stack. +10. Pop the value :math:`\I32.\CONST~n` from the stack. -11. Pop the value :math:`(\I32.\CONST~s)` from the stack. +11. Pop the value :math:`\I32.\CONST~s` from the stack. 12. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. @@ -804,7 +804,7 @@ Reference Instructions a. Let :math:`c_i` be the constant for which :math:`\bytes_{\X{ft}}(k_i)` is :math:`{b'}^n`. - b. Push the value :math:`(t.\CONST~c_i)` to the stack. + b. Push the value :math:`t.\CONST~c_i` to the stack. 18. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. @@ -853,9 +853,9 @@ Reference Instructions 9. Assert: due to :ref:`validation `, two :ref:`values ` of type :math:`\I32` are on the top of the stack. -10. Pop the value :math:`(\I32.\CONST~n)` from the stack. +10. Pop the value :math:`\I32.\CONST~n` from the stack. -11. Pop the value :math:`(\I32.\CONST~s)` from the stack. +11. Pop the value :math:`\I32.\CONST~s` from the stack. 12. If the sum of :math:`s` and :math:`n` is larger than the length of :math:`\eleminst.\EIELEM`, then: @@ -900,7 +900,7 @@ Reference Instructions 5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -6. Pop the value :math:`(\I32.\CONST~i)` from the stack. +6. Pop the value :math:`\I32.\CONST~i` from the stack. 7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. @@ -910,9 +910,9 @@ Reference Instructions a. Trap. -10. Assert: due to :ref:`validation `, a :math:`\reff` is an :ref:`array reference `. +10. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -11. Let :math:`(\REFARRAYADDR~a)` be the reference value :math:`\reff`. +11. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. 12. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. @@ -961,7 +961,7 @@ Reference Instructions 7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. -8. Pop the value :math:`(\I32.\CONST~i)` from the stack. +8. Pop the value :math:`\I32.\CONST~i` from the stack. 9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. @@ -971,9 +971,9 @@ Reference Instructions a. Trap. -12. Assert: due to :ref:`validation `, a :math:`\reff` is an :ref:`array reference `. +12. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -13. Let :math:`(\REFARRAYADDR~a)` be the reference value :math:`\reff`. +13. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. 14. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. @@ -1010,9 +1010,9 @@ Reference Instructions a. Trap. -4. Assert: due to :ref:`validation `, a :math:`\reff` is an :ref:`array reference `. +4. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. -5. Let :math:`(\REFARRAYADDR~a)` be the reference value :math:`\reff`. +5. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. 6. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. @@ -1032,7 +1032,59 @@ Reference Instructions :math:`\ARRAYFILL~x` .................... -.. todo:: Prose +1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +2. Pop the value :math:`n` from the stack. + +3. Assert: due to :ref:`validation `, a :ref:`value ` is on the top of the stack. + +4. Pop the value :math:`\val` from the stack. + +5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +6. Pop the value :math:`d` from the stack. + +7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. + +8. Pop the value :math:`\reff` from the stack. + +9. If :math:`\reff` is :math:`\REFNULL~t`, then: + + a. Trap. + +10. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. + +11. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. + +12. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. + +13. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: + + a. Trap. + +14. If :math:`n = 0`, then: + + a. Return. + +15. Push the value :math:`\REFARRAYADDR~a` to the stack. + +16. Push the value :math:`\I32.\CONST~d` to the stack. + +17. Push the value :math:`\val` to the stack. + +18. Execute the instruction :math:`\ARRAYSET~x`. + +19. Push the value :math:`\REFARRAYADDR~a` to the stack. + +20. Assert: due to the earlier check against the array size, :math:`d+1 < 2^{32}`. + +21. Push the value :math:`\I32.\CONST~(d+1)` to the stack. + +22. Push the value :math:`\val` to the stack. + +23. Push the value :math:`\I32.\CONST~(n-1)` to the stack. + +24. Execute the instruction :math:`\ARRAYFILL~x`. .. math:: ~\\[-1ex] @@ -1066,10 +1118,116 @@ Reference Instructions :math:`\ARRAYCOPY~x~y` ...................... -.. todo:: Prose - .. todo:: Handle packed fields correctly via array.get_u instead of array.get +1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +2. Pop the value :math:`n` from the stack. + +3. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +4. Pop the value :math:`s` from the stack. + +5. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~y)` is on the top of the stack. + +6. Pop the value :math:`\reff_2` from the stack. + +7. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`\I32` is on the top of the stack. + +8. Pop the value :math:`d` from the stack. + +9. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. + +10. Pop the value :math:`\reff_1` from the stack. + +11. If :math:`\reff_1` is :math:`\REFNULL~t`, then: + + a. Trap. + +12. Assert: due to :ref:`validation `, :math:`\reff_1` is an :ref:`array reference `. + +13. Let :math:`\REFARRAYADDR~a_1` be the reference value :math:`\reff_1`. + +14. If :math:`\reff_2` is :math:`\REFNULL~t`, then: + + a. Trap. + +15. Assert: due to :ref:`validation `, :math:`\reff_2` is an :ref:`array reference `. + +16. Let :math:`\REFARRAYADDR~a_2` be the reference value :math:`\reff_2`. + +17. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_1]` exists. + +18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a_2]` exists. + +19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_1].\AIFIELDS`, then: + + a. Trap. + +20. If :math:`s + n` is larger than or equal to the length of :math:`S.\SARRAYS[a_2].\AIFIELDS`, then: + + a. Trap. + +21. If :math:`n = 0`, then: + + a. Return. + +22. If :math:`d \leq s`, then: + + a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. + + b. Push the value :math:`\I32.\CONST~d` to the stack. + + c. Push the value :math:`\REFARRAYADDR~a_2` to the stack. + + d. Push the value :math:`\I32.\CONST~s` to the stack. + + e. Execute the instruction :math:`\ARRAYGET~y`. + + f. Execute the instruction :math:`\ARRAYSET~x`. + + g. Push the value :math:`\REFARRAYADDR~a_1` to the stack. + + h. Assert: due to the earlier check against the array size, :math:`d+1 < 2^{32}`. + + i. Push the value :math:`\I32.\CONST~(d+1)` to the stack. + + j. Push the value :math:`\REFARRAYADDR~a_2` to the stack. + + k. Assert: due to the earlier check against the array size, :math:`s+1 < 2^{32}`. + + l. Push the value :math:`\I32.\CONST~(s+1)` to the stack. + +23. Else: + + a. Push the value :math:`\REFARRAYADDR~a_1` to the stack. + + b. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`. + + c. Push the value :math:`\I32.\CONST~(d+n-1)` to the stack. + + d. Push the value :math:`\REFARRAYADDR~a_2` to the stack. + + e. Assert: due to the earlier check against the memory size, :math:`s+n-1 < 2^{32}`. + + f. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. + + g. Execute the instruction :math:`\ARRAYGET~y`. + + h. Execute the instruction :math:`\ARRAYSET~x`. + + i. Push the value :math:`\REFARRAYADDR~a_1` to the stack. + + j. Push the value :math:`\I32.\CONST~d` to the stack. + + k. Push the value :math:`\REFARRAYADDR~a_2` to the stack. + + l. Push the value :math:`\I32.\CONST~s` to the stack. + +24. Push the value :math:`\I32.\CONST~(n-1)` to the stack. + +25. Execute the instruction :math:`\ARRAYCOPY~x~y`. + .. math:: ~\\[-1ex] \begin{array}{l} @@ -1118,7 +1276,81 @@ Reference Instructions :math:`\ARRAYINITDATA~x~y` .......................... -.. todo:: Prose +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. + +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. + +3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. + +4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) + +5. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. + +6. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. + +7. Assert: due to :ref:`validation `, the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]` exists. + +8. Let :math:`\datainst` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. + +9. Assert: due to :ref:`validation `, three values of type :math:`\I32` are on the top of the stack. + +10. Pop the value :math:`\I32.\CONST~n` from the stack. + +11. Pop the value :math:`\I32.\CONST~s` from the stack. + +12. Pop the value :math:`\I32.\CONST~d` from the stack. + +13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. + +14. Pop the value :math:`\reff` from the stack. + +15. If :math:`\reff` is :math:`\REFNULL~t`, then: + + a. Trap. + +16. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. + +17. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. + +18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. + +19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: + + a. Trap. + +20. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}`. + +21. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: + + a. Trap. + +22. If :math:`n = 0`, then: + + a. Return. + +23. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice z]`. + +24. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. + +25. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(k_i)` is :math:`b^\ast`. + +26. Push the value :math:`\REFARRAYADDR~a` to the stack. + +27. Push the value :math:`\I32.\CONST~d` to the stack. + +28. Push the value :math:`t.\CONST~c` to the stack. + +29. Execute the instruction :math:`\ARRAYSET~x`. + +30. Push the value :math:`\REFARRAYADDR~a` to the stack. + +31. Push the value :math:`\I32.\CONST~(d+1)` to the stack. + +32. Push the value :math:`\I32.\CONST~(s+z)` to the stack. + +33. Push the value :math:`\I32.\CONST~(n-1)` to the stack. + +34. Execute the instruction :math:`\ARRAYINITDATA~x~y`. .. math:: ~\\[-1ex] @@ -1140,7 +1372,7 @@ Reference Instructions \quad\stepto \\ \quad S; F; \begin{array}[t]{@{}l@{}} - (\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST c)~(\ARRAYSET~x) \\ + (\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST~c)~(\ARRAYSET~x) \\ (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+|\X{ft}|)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \\ \end{array} \\ \qquad @@ -1159,7 +1391,75 @@ Reference Instructions :math:`\ARRAYINITELEM~x~y` .......................... -.. todo:: Prose +1. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. + +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. + +3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. + +4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) + +5. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. + +6. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. + +7. Assert: due to :ref:`validation `, the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]` exists. + +8. Let :math:`\eleminst` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. + +9. Assert: due to :ref:`validation `, three values of type :math:`\I32` are on the top of the stack. + +10. Pop the value :math:`\I32.\CONST~n` from the stack. + +11. Pop the value :math:`\I32.\CONST~s` from the stack. + +12. Pop the value :math:`\I32.\CONST~d` from the stack. + +13. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~x)` is on the top of the stack. + +14. Pop the value :math:`\reff` from the stack. + +15. If :math:`\reff` is :math:`\REFNULL~t`, then: + + a. Trap. + +16. Assert: due to :ref:`validation `, :math:`\reff` is an :ref:`array reference `. + +17. Let :math:`\REFARRAYADDR~a` be the reference value :math:`\reff`. + +18. Assert: due to :ref:`validation `, the :ref:`array instance ` :math:`S.\SARRAYS[a]` exists. + +19. If :math:`d + n` is larger than or equal to the length of :math:`S.\SARRAYS[a].\AIFIELDS`, then: + + a. Trap. + +20. If :math:`s + n` is larger than or equal to the length of :math:`\eleminst.\EIELEM`, then: + + a. Trap. + +21. If :math:`n = 0`, then: + + a. Return. + +22. Let :math:`\reff'` be the :ref:`reference value ` :math:`\eleminst.\EIELEM[s]`. + +23. Push the value :math:`\REFARRAYADDR~a` to the stack. + +24. Push the value :math:`\I32.\CONST~d` to the stack. + +25. Push the value :math:`\reff'` to the stack. + +26. Execute the instruction :math:`\ARRAYSET~x`. + +27. Push the value :math:`\REFARRAYADDR~a` to the stack. + +28. Push the value :math:`\I32.\CONST~(d+1)` to the stack. + +29. Push the value :math:`\I32.\CONST~(s+1)` to the stack. + +30. Push the value :math:`\I32.\CONST~(n-1)` to the stack. + +31. Execute the instruction :math:`\ARRAYINITELEM~x~y`. .. math:: ~\\[-1ex] @@ -1220,7 +1520,7 @@ Reference Instructions 3. Assert: due to :ref:`validation `, a :math:`\reff` is an :ref:`external reference `. -4. Let :math:`(\REFEXTERN~\reff')` be the reference value :math:`\reff`. +4. Let :math:`\REFEXTERN~\reff'` be the reference value :math:`\reff`. 5. Push the reference value :math:`\reff'` to the stack. From 19784234dccaf1b3a82dac947ee9ff8cd17c7375 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Sat, 22 Jul 2023 11:47:24 -0700 Subject: [PATCH 2/4] type expansion and byte width --- document/core/exec/instructions.rst | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index f39f3d65e..75cbeb859 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -790,7 +790,7 @@ Reference Instructions 12. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. -13. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}`. +13. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. 14. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: @@ -815,7 +815,7 @@ Reference Instructions \\&& \begin{array}[t]{@{}r@{~}l@{}} (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ - \land & s + n\cdot|\X{ft}| > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|) + \land & s + n\cdot|\X{ft}|/8 > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|) \end{array} \\ \\[1ex] S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& (t.\CONST~c)^n~(\ARRAYNEWFIXED~x~n) @@ -823,7 +823,7 @@ Reference Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ \land & t = \unpacktype(\X{ft}) \\ - \land & (\bytes_{\X{ft}}(c))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|] \\ + \land & (\bytes_{\X{ft}}(c))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|/8] \\ \end{array} \\ \end{array} @@ -1280,9 +1280,9 @@ Reference Instructions 2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) +4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. 5. Assert: due to :ref:`validation `, the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]` exists. @@ -1318,7 +1318,7 @@ Reference Instructions a. Trap. -20. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}`. +20. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. 21. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: @@ -1360,7 +1360,7 @@ Reference Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & d + n > |S.\SARRAYS[a].\AIFIELDS| \\ \vee & (F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \land - s + n\cdot|\X{ft}| > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|)) + s + n\cdot|\X{ft}|/8 > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|)) \end{array} \\[1ex] S; F; (\REFARRAYADDR~a)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\ARRAYINITDATA~x~y) @@ -1373,13 +1373,13 @@ Reference Instructions \\ \quad S; F; \begin{array}[t]{@{}l@{}} (\REFARRAYADDR~a)~(\I32.\CONST~d)~(t.\CONST~c)~(\ARRAYSET~x) \\ - (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+|\X{ft}|)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \\ + (\REFARRAYADDR~a)~(\I32.\CONST~d+1)~(\I32.\CONST~s+|\X{ft}|/8)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\otherwise, \iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\ \land & t = \unpacktype(\X{ft}) \\ - \land & \bytes_{\X{ft}}(c) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice |\X{ft}|] + \land & \bytes_{\X{ft}}(c) = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice |\X{ft}|/8] \end{array} \\[1ex] S; F; (\REFNULL~t)~(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYINITDATA~x~y) \quad\stepto\quad \TRAP @@ -1395,9 +1395,9 @@ Reference Instructions 2. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. -3. Assert: due to :ref:`validation `, :math:`\deftype` is an :ref:`array type `. +3. Assert: due to :ref:`validation `, the :ref:`expansion ` of :math:`\deftype` is an :ref:`array type `. -4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) +4. Let :math:`\TARRAY~\X{ft}` be the :ref:`expanded ` :ref:`array type ` :math:`\deftype`. 5. Assert: due to :ref:`validation `, the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]` exists. From ba832340dede252f7fbfbd5c7b0090f7bc7129ff Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Sat, 22 Jul 2023 12:06:56 -0700 Subject: [PATCH 3/4] assert that bit width and bytes_ft are defined --- document/core/exec/instructions.rst | 40 +++++++++++++++++------------ 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 75cbeb859..3126d05d0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -802,9 +802,11 @@ Reference Instructions 17. For each consecutive subsequence :math:`{b'}^n` of :math:`b^\ast`: - a. Let :math:`c_i` be the constant for which :math:`\bytes_{\X{ft}}(k_i)` is :math:`{b'}^n`. + a. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. - b. Push the value :math:`t.\CONST~c_i` to the stack. + b. Let :math:`c_i` be the constant for which :math:`\bytes_{\X{ft}}(c_i)` is :math:`{b'}^n`. + + c. Push the value :math:`t.\CONST~c_i` to the stack. 18. Execute the instruction :math:`(\ARRAYNEWFIXED~x~n)`. @@ -1318,39 +1320,43 @@ Reference Instructions a. Trap. -20. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. +20. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. + +21. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}` divided by eight. -21. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: +22. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: a. Trap. -22. If :math:`n = 0`, then: +23. If :math:`n = 0`, then: a. Return. -23. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice z]`. +24. Let :math:`b^\ast` be the :ref:`byte ` sequence :math:`\datainst.\DIDATA[s \slice z]`. + +25. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. -24. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. +26. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. -25. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(k_i)` is :math:`b^\ast`. +27. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(c)` is :math:`b^\ast`. -26. Push the value :math:`\REFARRAYADDR~a` to the stack. +28. Push the value :math:`\REFARRAYADDR~a` to the stack. -27. Push the value :math:`\I32.\CONST~d` to the stack. +29. Push the value :math:`\I32.\CONST~d` to the stack. -28. Push the value :math:`t.\CONST~c` to the stack. +30. Push the value :math:`t.\CONST~c` to the stack. -29. Execute the instruction :math:`\ARRAYSET~x`. +31. Execute the instruction :math:`\ARRAYSET~x`. -30. Push the value :math:`\REFARRAYADDR~a` to the stack. +32. Push the value :math:`\REFARRAYADDR~a` to the stack. -31. Push the value :math:`\I32.\CONST~(d+1)` to the stack. +33. Push the value :math:`\I32.\CONST~(d+1)` to the stack. -32. Push the value :math:`\I32.\CONST~(s+z)` to the stack. +34. Push the value :math:`\I32.\CONST~(s+z)` to the stack. -33. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +35. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -34. Execute the instruction :math:`\ARRAYINITDATA~x~y`. +36. Execute the instruction :math:`\ARRAYINITDATA~x~y`. .. math:: ~\\[-1ex] From ecd98b8634e2d2a267fca98f27be29e81ba891cd Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Sat, 22 Jul 2023 12:19:23 -0700 Subject: [PATCH 4/4] fix link --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3126d05d0..90ab494dc 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1336,7 +1336,7 @@ Reference Instructions 25. Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\X{ft})`. -26. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. +26. Assert: due to :ref:`validation `, :math:`\bytes_{\X{ft}}` is defined. 27. Let :math:`c` be the constant for which :math:`\bytes_{\X{ft}}(c)` is :math:`b^\ast`.