From ace09470a6aab8e31710c6835a70a344cbec051b Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 6 Nov 2024 14:58:53 -0800 Subject: [PATCH] Memory64 spec tweaks and fixes from @rossberg (#98) - Removed unnecessary/mismatching lookup of table/memory type in execution prose - Added missing result type lookup in formal rule for table.size and memory.size - Fixed computation of -1 result value for table.grow and table.size to work for i64 - Some fixes around specification of text format for inline elements/data shorthand - Fixed matching rules for tabletype/memtype to enforce same address type Split out from https://github.com/WebAssembly/spec/pull/1839 --- document/core/binary/types.rst | 6 +- document/core/exec/instructions.rst | 420 ++++++++++++--------------- document/core/syntax/types.rst | 13 +- document/core/text/modules.rst | 29 +- document/core/valid/instructions.rst | 8 +- document/core/valid/matching.rst | 8 +- 6 files changed, 217 insertions(+), 267 deletions(-) diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index d5501ec48..3ab538a09 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -251,7 +251,7 @@ Additional shorthands are recognized for unary recursions and sub types without Limits ~~~~~~ -:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present, and the corresponding :ref:`address type `. +:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present, and a flag for the :ref:`address type `. .. math:: \begin{array}{llclll} @@ -275,7 +275,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{memory type} & \Bmemtype &::=& - (\X{at}, \X{lim}){:}\Blimits &\Rightarrow& \X{at}~~\X{lim} \\ + (\X{at},\X{lim}){:}\Blimits &\Rightarrow& \X{at}~\X{lim} \\ \end{array} @@ -291,7 +291,7 @@ Table Types .. math:: \begin{array}{llclll} \production{table type} & \Btabletype &::=& - \X{et}{:}\Breftype~~(\X{at}, \X{lim}){:}\Blimits &\Rightarrow& \X{at}~~\X{lim}~\X{et} \\ + \X{et}{:}\Breftype~~(\X{at},\X{lim}){:}\Blimits &\Rightarrow& \X{at}~\X{lim}~\X{et} \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3a23b045e..d6a16b84a 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2725,19 +2725,17 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: +8. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -10. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. +9. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. -11. Push the value :math:`\val` to the stack. +10. Push the value :math:`\val` to the stack. .. math:: ~\\[-1ex] @@ -2770,21 +2768,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +6. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -8. Pop the value :math:`\val` from the stack. +7. Pop the value :math:`\val` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: +10. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -12. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. +11. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. .. math:: ~\\[-1ex] @@ -2829,7 +2825,10 @@ Table Instructions S; F; (\TABLESIZE~x) &\stepto& S; F; (\X{at}.\CONST~\X{sz}) \end{array} \\ \qquad - (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\ + \begin{array}[t]{@{}r@{~}l@{}} + (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz} \\ + \wedge S.\STABLES[F.\AMODULE.\MITABLES[x]].\TITYPE = \X{at}~\X{lim}~t) + \end{array} \\ \end{array} @@ -2849,21 +2848,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. +6. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -9. Pop the value :math:`\X{at}.\CONST~n` from the stack. +8. Pop the value :math:`t.\CONST~n` from the stack. -10. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +9. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -11. Pop the value :math:`\val` from the stack. +10. Pop the value :math:`\val` from the stack. -12. Let :math:`\X{err}` be the :math:`\X{at}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +11. Let :math:`\X{err}` be the value :math:`2^{|\X{at}|}-1`, for which :math:`\signed_{|\X{at}|}(\X{err})` is :math:`-1`. -13. Either: +12. Either: a. If :ref:`growing ` :math:`\X{tab}` by :math:`n` entries with initialization value :math:`\val` succeeds, then: @@ -2873,7 +2870,7 @@ Table Instructions i. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. -14. Or: +13. Or: a. push the value :math:`\X{at}.\CONST~\X{err}` to the stack. @@ -2891,7 +2888,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; \val~(\X{at}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{32}^{-1}(-1)) + S; F; \val~(\X{at}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{|\X{at}|}^{-1}(-1)) \end{array} \end{array} @@ -2919,21 +2916,19 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Pop the value :math:`\X{at}.\CONST~n` from the stack. -8. Pop the value :math:`\X{at}.\CONST~n` from the stack. +8. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -9. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. - -10. Pop the value :math:`\val` from the stack. +9. Pop the value :math:`\val` from the stack. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`address type ` :math:`\X{at}` is on the top of the stack. -12. Pop the value :math:`\X{at}.\CONST~i` from the stack. +11. Pop the value :math:`\X{at}.\CONST~i` from the stack. -13. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: +12. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. @@ -3004,25 +2999,19 @@ Table Instructions 9. Let :math:`\X{tab}_y` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_y]`. -10. Let :math:`\X{at}_x~\limits_x` be the :ref:`table type ` :math:`\X{tab}_x.\TITYPE`. - -11. Let :math:`\X{at}_y~\limits_y` be the :ref:`table type ` :math:`\X{tab}_y.\TITYPE`. - -12. Let :math:`\X{at}_n` be the :ref:`minimum ` of :math:`\X{at}_x` and :math:`\X{at}_y`. +10. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_n` is on the top of the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_n` is on the top of the stack. +11. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. -14. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. +12. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_s` is on the top of the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_y` is on the top of the stack. +13. Pop the value :math:`\X{at}_s.\CONST~s` from the stack. -16. Pop the value :math:`\X{at}_y.\CONST~s` from the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_d` is on the top of the stack. -17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_x` is on the top of the stack. +15. Pop the value :math:`\X{at}_d.\CONST~d` from the stack. -18. Pop the value :math:`\X{at}_x.\CONST~d` from the stack. - -19. If :math:`s + n` is larger than the length of :math:`\X{tab}_y.\TIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}_x.\TIELEM`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{tab}_y.\TIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}_x.\TIELEM`, then: a. Trap. @@ -3032,9 +3021,9 @@ Table Instructions 21. If :math:`d \leq s`, then: - a. Push the value :math:`\X{at}_x.\CONST~d` to the stack. + a. Push the value :math:`\X{at}_d.\CONST~d` to the stack. - b. Push the value :math:`\X{at}_y.\CONST~s` to the stack. + b. Push the value :math:`\X{at}_s.\CONST~s` to the stack. c. Execute the instruction :math:`\TABLEGET~y`. @@ -3042,29 +3031,29 @@ Table Instructions e. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\X{at}_x.\CONST~(d+1)` to the stack. + f. Push the value :math:`\X{at}_d.\CONST~(d+1)` to the stack. g. Assert: due to the earlier check against the table size, :math:`s+1 < 2^{32}`. - h. Push the value :math:`\X{at}_y.\CONST~(s+1)` to the stack. + h. Push the value :math:`\X{at}_s.\CONST~(s+1)` to the stack. 22. Else: a. Assert: due to the earlier check against the table size, :math:`d+n-1 < 2^{32}`. - b. Push the value :math:`\X{at}_x.\CONST~(d+n-1)` to the stack. + b. Push the value :math:`\X{at}_d.\CONST~(d+n-1)` to the stack. c. Assert: due to the earlier check against the table size, :math:`s+n-1 < 2^{32}`. - d. Push the value :math:`\X{at}_y.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{at}_s.\CONST~(s+n-1)` to the stack. c. Execute the instruction :math:`\TABLEGET~y`. f. Execute the instruction :math:`\TABLESET~x`. - g. Push the value :math:`\X{at}_x.\CONST~d` to the stack. + g. Push the value :math:`\X{at}_d.\CONST~d` to the stack. - h. Push the value :math:`\X{at}_y.\CONST~s` to the stack. + h. Push the value :math:`\X{at}_s.\CONST~s` to the stack. 23. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. @@ -3073,7 +3062,7 @@ Table Instructions .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3081,27 +3070,27 @@ Table Instructions \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~0)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~0)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\X{at}_x.\CONST~d+1)~(\X{at}_y.\CONST~s+1)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ + (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\X{at}_d.\CONST~d+1)~(\X{at}_s.\CONST~s+1)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\X{at}_x.\CONST~d+n)~(\X{at}_y.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\X{at}_x.\CONST~d)~(\X{at}_y.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ + (\X{at}_d.\CONST~d+n)~(\X{at}_s.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\X{at}_d.\CONST~d)~(\X{at}_s.\CONST~s)~(\X{at}_n.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -3123,55 +3112,53 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. - -7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. -8. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. +7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. -9. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. +8. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. -10. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. +9. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\I32` is on the top of the stack. -12. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -14. Pop the value :math:`\I32.\CONST~s` from the stack. +13. Pop the value :math:`\I32.\CONST~s` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -16. Pop the value :math:`\X{at}.\CONST~d` from the stack. +15. Pop the value :math:`\X{at}.\CONST~d` from the stack. -17. If :math:`s + n` is larger than the length of :math:`\X{elem}.\EIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{elem}.\EIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -18. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -19. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. +18. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. -20. Push the value :math:`\X{at}.\CONST~d` to the stack. +19. Push the value :math:`\X{at}.\CONST~d` to the stack. -21. Push the value :math:`\val` to the stack. +20. Push the value :math:`\val` to the stack. -22. Execute the instruction :math:`\TABLESET~x`. +21. Execute the instruction :math:`\TABLESET~x`. -23. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. +22. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. -24. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. +23. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. -25. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. +24. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. -26. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -27. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -28. Execute the instruction :math:`\TABLEINIT~x~y`. +27. Execute the instruction :math:`\TABLEINIT~x~y`. .. math:: ~\\[-1ex] @@ -3260,35 +3247,33 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -10. If :math:`N` is not part of the instruction, then: +9. If :math:`N` is not part of the instruction, then: a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. -11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -12. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -13. If :math:`N` and :math:`\sx` are part of the instruction, then: +12. If :math:`N` and :math:`\sx` are part of the instruction, then: a. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. b. Let :math:`c` be the result of computing :math:`\extend^{\sx}_{N,|t|}(n)`. -14. Else: +13. Else: a. Let :math:`c` be the constant for which :math:`\bytes_t(c) = b^\ast`. -15. Push the value :math:`t.\CONST~c` to the stack. +14. Push the value :math:`t.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3337,29 +3322,27 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -10. If :math:`\X{ea} + M \cdot N /8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. If :math:`\X{ea} + M \cdot N /8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice M \cdot N /8]`. +10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice M \cdot N /8]`. -12. Let :math:`m_k` be the integer for which :math:`\bytes_{\iM}(m_k) = b^\ast[k \cdot M/8 \slice M/8]`. +11. Let :math:`m_k` be the integer for which :math:`\bytes_{\iM}(m_k) = b^\ast[k \cdot M/8 \slice M/8]`. -13. Let :math:`W` be the integer :math:`M \cdot 2`. +12. Let :math:`W` be the integer :math:`M \cdot 2`. -14. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. +13. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. -15. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. +14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. -16. Push the value :math:`\V128.\CONST~c` to the stack. +15. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3400,27 +3383,25 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -12. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. +11. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. -13. Let :math:`L` be the integer :math:`128 / N`. +12. Let :math:`L` be the integer :math:`128 / N`. -14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. +13. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. -15. Push the value :math:`\V128.\CONST~c` to the stack. +14. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3459,25 +3440,23 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Pop the value :math:`\X{at}.\CONST~i` from the stack. -8. Pop the value :math:`\X{at}.\CONST~i` from the stack. +8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. - -10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -12. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. +11. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. -13. Let :math:`c` be the result of computing :math:`\extendu_{N,128}(n)`. +12. Let :math:`c` be the result of computing :math:`\extendu_{N,128}(n)`. -14. Push the value :math:`\V128.\CONST~c` to the stack. +13. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3516,33 +3495,31 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -8. Pop the value :math:`\V128.\CONST~v` from the stack. +7. Pop the value :math:`\V128.\CONST~v` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -13. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +12. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -14. Let :math:`r` be the constant for which :math:`\bytes_{\iN}(r) = b^\ast`. +13. Let :math:`r` be the constant for which :math:`\bytes_{\iN}(r) = b^\ast`. -15. Let :math:`L` be :math:`128 / N`. +14. Let :math:`L` be :math:`128 / N`. -16. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. +15. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. -17. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [y] = r)`. +16. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [y] = r)`. -18. Push the value :math:`\V128.\CONST~c` to the stack. +17. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] @@ -3583,37 +3560,35 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t` is on the top of the stack. -8. Pop the value :math:`t.\CONST~c` from the stack. +7. Pop the value :math:`t.\CONST~c` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -12. If :math:`N` is not part of the instruction, then: +11. If :math:`N` is not part of the instruction, then: a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. -13. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -14. If :math:`N` is part of the instruction, then: +13. If :math:`N` is part of the instruction, then: a. Let :math:`n` be the result of computing :math:`\wrap_{|t|,N}(c)`. b. Let :math:`b^\ast` be the byte sequence :math:`\bytes_{\iN}(n)`. -15. Else: +14. Else: a. Let :math:`b^\ast` be the byte sequence :math:`\bytes_t(c)`. -16. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. +15. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. .. math:: ~\\[-1ex] @@ -3661,29 +3636,27 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\V128` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\V128` is on the top of the stack. -8. Pop the value :math:`\V128.\CONST~c` from the stack. +7. Pop the value :math:`\V128.\CONST~c` from the stack. -9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -10. Pop the value :math:`\X{at}.\CONST~i` from the stack. +9. Pop the value :math:`\X{at}.\CONST~i` from the stack. -11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -13. Let :math:`L` be :math:`128/N`. +12. Let :math:`L` be :math:`128/N`. -14. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. +13. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. -15. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[y])`. +14. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[y])`. -16. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. +15. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. .. math:: ~\\[-1ex] @@ -3734,7 +3707,10 @@ Memory Instructions S; F; (\MEMORYSIZE~x) &\stepto& S; F; (\X{at}.\CONST~\X{sz}) \end{array} \\ \qquad - (\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| = \X{sz}\cdot64\,\F{Ki}) \\ + \begin{array}[t]{@{}r@{~}l@{}} + (\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| = \X{sz}\cdot64\,\F{Ki} \\ + \wedge S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MITYPE = \X{at}~\X{lim}) + \end{array} \\ \end{array} @@ -3754,17 +3730,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size `. +6. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size `. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +7. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -9. Pop the value :math:`\X{at}.\CONST~n` from the stack. +8. Pop the value :math:`\X{at}.\CONST~n` from the stack. -10. Let :math:`\X{err}` be the :math:`\X{at}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +9. Let :math:`\X{err}` be the :math:`\X{at}` value :math:`2^{|\X{at}|}-1`, for which :math:`\signed_{|\X{at}|}(\X{err})` is :math:`-1`. -11. Either: +10. Either: a. If :ref:`growing ` :math:`\X{mem}` by :math:`n` :ref:`pages ` succeeds, then: @@ -3774,7 +3748,7 @@ Memory Instructions i. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. -12. Or: +11. Or: a. Push the value :math:`\X{at}.\CONST~\X{err}` to the stack. @@ -3792,7 +3766,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\X{at}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{32}^{-1}(-1)) + S; F; (\X{at}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{at}.\CONST~\signed_{|\X{at}|}^{-1}(-1)) \end{array} \end{array} @@ -3820,17 +3794,15 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. 7. Pop the value :math:`\X{at}.\CONST~n` from the stack. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Assert: due to :ref:`validation `, a value is on the top of the stack. 9. Pop the value :math:`\val` from the stack. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`address type ` :math:`\X{at}` is on the top of the stack. 11. Pop the value :math:`\X{at}.\CONST~d` from the stack. @@ -3906,33 +3878,27 @@ Memory Instructions 9. Let :math:`\X{mem}_s` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{sa}]`. -10. Let :math:`\X{at}_d~\limits_d` be the :ref:`memory type ` :math:`\X{mem}_d.\MITYPE`. +10. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_n` is on the top of the stack. -11. Let :math:`\X{at}_s~\limits_s` be the :ref:`memory type ` :math:`\X{mem}_s.\MITYPE`. +11. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. -12. Let :math:`\X{at}_n` be the :ref:`minimum ` of :math:`\X{at}_s` and :math:`\X{at}_d`. +12. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_s` is on the top of the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_n` is on the top of the stack. +13. Pop the value :math:`\X{at}_s.\CONST~s` from the stack. -14. Pop the value :math:`\X{at}_n.\CONST~n` from the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}_d` is on the top of the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_s` is on the top of the stack. +15. Pop the value :math:`\X{at}_d.\CONST~d` from the stack. -16. Pop the value :math:`\X{at}_s.\CONST~s` from the stack. - -17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}_d` is on the top of the stack. - -18. Pop the value :math:`\X{at}_d.\CONST~d` from the stack. - -19. If :math:`s + n` is larger than the length of :math:`\X{mem}_s.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}_d.\MIDATA`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{mem}_s.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}_d.\MIDATA`, then: a. Trap. -20. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -21. If :math:`d \leq s`, then: +18. If :math:`d \leq s`, then: a. Push the value :math:`\X{at}_d.\CONST~d` to the stack. @@ -3950,7 +3916,7 @@ Memory Instructions h. Push the value :math:`\X{at}_s.\CONST~(s+1)` to the stack. -22. Else: +19. Else: a. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`. @@ -3968,9 +3934,9 @@ Memory Instructions h. Push the value :math:`\X{at}_s.\CONST~s` to the stack. -23. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. +20. Push the value :math:`\X{at}_n.\CONST~(n-1)` to the stack. -24. Execute the instruction :math:`\MEMORYCOPY~x~y`. +21. Execute the instruction :math:`\MEMORYCOPY~x~y`. .. math:: ~\\[-1ex] @@ -4029,55 +3995,53 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{at}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. - -7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. -8. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. +7. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. -9. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. +8. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. -10. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. +9. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. -11. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -12. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Pop the value :math:`\I32.\CONST~n` from the stack. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -14. Pop the value :math:`\I32.\CONST~s` from the stack. +13. Pop the value :math:`\I32.\CONST~s` from the stack. -15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{at}` is on the top of the stack. +14. Assert: due to :ref:`validation `, a value of some :ref:`address type ` :math:`\X{at}` is on the top of the stack. -16. Pop the value :math:`\X{at}.\CONST~d` from the stack. +15. Pop the value :math:`\X{at}.\CONST~d` from the stack. -17. If :math:`s + n` is larger than the length of :math:`\X{data}.\DIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +16. If :math:`s + n` is larger than the length of :math:`\X{data}.\DIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -18. If :math:`n = 0`, then: +17. If :math:`n = 0`, then: a. Return. -19. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. +18. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. -20. Push the value :math:`\X{at}.\CONST~d` to the stack. +19. Push the value :math:`\X{at}.\CONST~d` to the stack. -21. Push the value :math:`\I32.\CONST~b` to the stack. +20. Push the value :math:`\I32.\CONST~b` to the stack. -22. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. +21. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. -23. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. +22. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -24. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. +23. Push the value :math:`\X{at}.\CONST~(d+1)` to the stack. -25. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. +24. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. -26. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -27. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -28. Execute the instruction :math:`\MEMORYINIT~x~y`. +27. Execute the instruction :math:`\MEMORYINIT~x~y`. .. math:: ~\\[-1ex] diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 5e17179f2..2da8a265f 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -366,7 +366,7 @@ The syntax of sub types is :ref:`generalized ` for the purp Address Type ~~~~~~~~~~~~ -*Address types* classify the values that can be used to index into +*Address types* are a subset of :ref:`number types ` that classify the values that can be used as offsets into :ref:`memories ` and :ref:`tables `. .. math:: @@ -380,13 +380,12 @@ Address Type Conventions ........... -The *minimum* of two address types is defined as |I32| if either of the types are -|I32|, and |I64| otherwise. +The *minimum* of two address types is defined as the address type whose :ref:`bit width ` is the minimum of the two. .. math:: \begin{array}{llll} - \atmin(\I64, \I64) &=& \I64 \\ - \atmin(\X{at}_1, \X{at}_2) &=& \I32 & (\otherwise) \\ + \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_1 & (\iff |\X{at}_1| \leq |\X{at}_2|) \\ + \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_2 & (\otherwise) \\ \end{array} @@ -424,7 +423,7 @@ Memory Types .. math:: \begin{array}{llrl} \production{memory type} & \memtype &::=& - ~\addrtype~\limits \\ + \addrtype~\limits \\ \end{array} The limits constrain the minimum and optionally the maximum size of a memory. @@ -445,7 +444,7 @@ Table Types .. math:: \begin{array}{llrl} \production{table type} & \tabletype &::=& - ~\addrtype~\limits ~\reftype \\ + \addrtype~\limits~\reftype \\ \end{array} Like memories, tables are constrained by limits for their minimum and optionally maximum size. diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 3178332dd..73bb7182b 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -307,21 +307,12 @@ An :ref:`element segment ` can be given inline with a table definitio .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~\expr^n{:}\Tvec(\Telemexpr)~\text{)}~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)} \\ & \qquad - \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\Telemexpr)~\text{)} + \text{(}~\text{table}~~\Tid^?~~\Taddrtype^?~~\Treftype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{table}~~\Tid'~~\Taddrtype^?~~n~~n~~\Treftype~\text{)} \\ & \qquad + \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\Taddrtype'\text{.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\text{(}~\text{ref.func}~~\Tfuncidx~\text{)})~\text{)} \\ & \qquad\qquad - (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh) \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \production{module field} & - \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)} \\ & \qquad - \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\text{(}~\text{ref.func}~~\Tfuncidx~\text{)})~\text{)} - \\ & \qquad\qquad - (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh) \\ + (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad + \iff \Taddrtype? \neq \epsilon \wedge \Taddrtype' = \Taddrtype^? \vee \Taddrtype^? = \epsilon \wedge \Taddrtype' = \text{i32}) \\ \end{array} Tables can be defined as :ref:`imports ` or :ref:`exports ` inline: @@ -378,13 +369,13 @@ A :ref:`data segment ` can be given inline with a memory definition, .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{memory}~~\Tid^?~~\X{at}^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{memory}~~\Tid'~~\X{at}^?~~m~~m~\text{)} \\ & \qquad - \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{at}'\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\Taddrtype^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{memory}~~\Tid'~~\Taddrtype^?~~m~~m~\text{)} \\ & \qquad + \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\Taddrtype'\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} \\ & \qquad\qquad (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad - \iff \X{at}^? \neq \epsilon \wedge \X{at}' = \X{at}^? \vee \X{at}^? = \epsilon \wedge \X{at}' = \text{i32}, \\ & \qquad\qquad - m = \F{ceil}(n / 64\,\F{Ki})), \\ + \iff \Taddrtype? \neq \epsilon \wedge \Taddrtype' = \Taddrtype^? \vee \Taddrtype^? = \epsilon \wedge \Taddrtype' = \text{i32}, \\ & \qquad\qquad + m = \F{ceil}(n / 64\,\F{Ki})) \\ \end{array} Memories can be defined as :ref:`imports ` or :ref:`exports ` inline: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 01e09d93c..602540d97 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1496,11 +1496,11 @@ Table Instructions * Let :math:`\X{at}_2~\limits_2~t_2` be the :ref:`table type ` :math:`C.\CTABLES[y]`. -* Let :math:`\X{at}` be the :ref:`minimum ` of :math:`\X{at}_1` and :math:`\X{at}_2` - * The :ref:`reference type ` :math:`t_2` must :ref:`match ` :math:`t_1`. -* Then the instruction is valid with type :math:`[\X{at}_1~\X{at}_2~\atmin(\X{at}_1, \X{at}_2)] \to []`. +* Let :math:`\X{at}` be the :ref:`minimum ` of :math:`\X{at}_1` and :math:`\X{at}_2` + +* Then the instruction is valid with type :math:`[\X{at}_1~\X{at}_2~\X{at}] \to []`. .. math:: \frac{ @@ -1890,7 +1890,7 @@ Memory Instructions * Let :math:`\X{at}` be the :ref:`minimum ` of :math:`\X{at}_x` and :math:`\X{at}_y` -* Then the instruction is valid with type :math:`[\X{at}_x~\X{at}_y~\atmin(\X{at}_x, \X{at}_y)] \to []`. +* Then the instruction is valid with type :math:`[\X{at}_x~\X{at}_y~\X{at}] \to []`. .. math:: \frac{ diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 75ff8c08e..12457adf8 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -513,15 +513,13 @@ A :ref:`table type ` :math:`(\addrtype_1~\limits_1~\reftype_1) .. math:: ~\\[-1ex] \frac{ - C \vdashnumtypematch \addrtype_1 \matchesnumtype \addrtype_2 - \qquad C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 \qquad C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2 \qquad C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1 }{ - C \vdashtabletypematch \addrtype_1~\limits_1~\reftype_1 \matchestabletype \addrtype_2~\limits_2~\reftype_2 + C \vdashtabletypematch \addrtype~\limits_1~\reftype_1 \matchestabletype \addrtype~\limits_2~\reftype_2 } @@ -541,11 +539,9 @@ A :ref:`memory type ` :math:`(\addrtype_1~\limits_1)` matches :m .. math:: ~\\[-1ex] \frac{ - C \vdashnumtypematch \addrtype_1 \matchesnumtype \addrtype_2 - \qquad C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 }{ - C \vdashmemtypematch \limits_1 \matchesmemtype \limits_2 + C \vdashmemtypematch \addrtype~\limits_1 \matchesmemtype \addrtype~\limits_2 }