From f196f3a40f8ffbf97ed2e2d36eff8562f4d433c1 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 12 Jun 2024 13:41:01 -0700 Subject: [PATCH 1/8] [spec] Update syntax spec for memory64 I updated `instructions.rst` and make a start on `types.rst` but could use some help on how to parameterize `limits` on the index type. --- document/core/binary/instructions.rst | 2 +- document/core/binary/types.rst | 12 ++++--- document/core/exec/instructions.rst | 46 +++++++++++++++------------ document/core/syntax/instructions.rst | 5 +-- document/core/syntax/types.rst | 25 +++++++++++++-- document/core/text/modules.rst | 10 +++--- document/core/text/types.rst | 30 +++++++++++++++-- document/core/util/macros.def | 2 ++ document/core/valid/instructions.rst | 10 +++--- 9 files changed, 99 insertions(+), 43 deletions(-) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index f054013e6..284c7719e 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -278,7 +278,7 @@ Each variant of :ref:`memory instruction ` is encoded with .. math:: \begin{array}{llcllll} \production{memory argument} & \Bmemarg &::=& - a{:}\Bu32~~o{:}\Bu32 &\Rightarrow& 0~\{ \ALIGN~a,~\OFFSET~o \} + a{:}\Bu32~~o{:}\Bu64 &\Rightarrow& 0~\{ \ALIGN~a,~\OFFSET~o \} & (\iff a < 2^6) \\ &&|& a{:}\Bu32~~x{:}\memidx~~o{:}\Bu32 &\Rightarrow& x~\{ \ALIGN~(a - 2^6),~\OFFSET~o \} & (\iff 2^6 \leq a < 2^7) \\ diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 700cc2dbd..e2e3a199c 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -249,13 +249,15 @@ 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. +:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present, and the corresponsing index type. .. math:: \begin{array}{llclll} \production{limits} & \Blimits &::=& - \hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|& - \hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\ + \hex{00}~~n{:}\Bu64 &\Rightarrow& (\I32, \{ \LMIN~n, \LMAX~\epsilon \}) \\ &&|& + \hex{01}~~n{:}\Bu64~~m{:}\Bu64 &\Rightarrow& (\I32, \{ \LMIN~n, \LMAX~m \}) \\ &&|& + \hex{04}~~n{:}\Bu64 &\Rightarrow& (\I64, \{ \LMIN~n, \LMAX~\epsilon \}) \\ &&|& + \hex{05}~~n{:}\Bu64~~m{:}\Bu64 &\Rightarrow& (\I64, \{ \LMIN~n, \LMAX~m \}) \end{array} @@ -271,7 +273,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{memory type} & \Bmemtype &::=& - \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\ + (\X{it}, \X{lim}){:}\Blimits &\Rightarrow& \X{it}~~\X{lim} \\ \end{array} @@ -287,7 +289,7 @@ Table Types .. math:: \begin{array}{llclll} \production{table type} & \Btabletype &::=& - \X{et}{:}\Breftype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ + \X{et}{:}\Breftype~~(\X{it}, \X{lim}){:}\Blimits &\Rightarrow& \X{it}~~\X{lim}~\X{et} \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index fdd0941b6..224e77483 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3682,31 +3682,37 @@ Memory Instructions 9. Let :math:`\X{mem}_s` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{sa}]`. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +10. Let :math:`\X{it}_d~\limits` be the :math:`\X{mem}_d.\MITYPE`. -11. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Let :math:`\X{it}_s~\limits` be the :math:`\X{mem}_s.\MITYPE`. -12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +12. Let :math:`\X{it}_{min}` be ....? -13. Pop the value :math:`\I32.\CONST~s` from the stack. +13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_{min}` is on the top of the stack. -14. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +14. Pop the value :math:`\X{it}_{min}.\CONST~n` from the stack. -15. Pop the value :math:`\I32.\CONST~d` from the stack. +15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_s` is on the top of the stack. + +16. Pop the value :math:`\X{it}_s.\CONST~s` from the stack. + +17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_d` is on the top of the stack. -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: +18. Pop the value :math:`\X{it}_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: a. Trap. -17. If :math:`n = 0`, then: +20. If :math:`n = 0`, then: a. Return. -18. If :math:`d \leq s`, then: +21. If :math:`d \leq s`, then: - a. Push the value :math:`\I32.\CONST~d` to the stack. + a. Push the value :math:`\X{it}.\CONST~d` to the stack. - b. Push the value :math:`\I32.\CONST~s` to the stack. + b. Push the value :math:`\X{it}.\CONST~s` to the stack. c. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`. @@ -3714,33 +3720,33 @@ Memory Instructions e. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\I32.\CONST~(d+1)` to the stack. + f. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. g. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. - h. Push the value :math:`\I32.\CONST~(s+1)` to the stack. + h. Push the value :math:`\X{it}.\CONST~(s+1)` to the stack. -19. Else: +22. Else: a. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`. - b. Push the value :math:`\I32.\CONST~(d+n-1)` to the stack. + b. Push the value :math:`\X{it}.\CONST~(d+n-1)` to the stack. c. Assert: due to the earlier check against the memory size, :math:`s+n-1 < 2^{32}`. - d. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{it}.\CONST~(s+n-1)` to the stack. e. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`. f. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. - g. Push the value :math:`\I32.\CONST~d` to the stack. + g. Push the value :math:`\X{it}.\CONST~d` to the stack. - h. Push the value :math:`\I32.\CONST~s` to the stack. + h. Push the value :math:`\X{it}.\CONST~s` to the stack. -20. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +23. Push the value :math:`\X{it}_{min}.\CONST~(n-1)` to the stack. -21. Execute the instruction :math:`\MEMORYCOPY~x~y`. +24. Execute the instruction :math:`\MEMORYCOPY~x~y`. .. math:: ~\\[-1ex] diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 4b3bb0863..ae4523119 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -650,7 +650,7 @@ Instructions in this group are concerned with linear :ref:`memory `. .. math:: \begin{array}{llrl} \production{memory immediate} & \memarg &::=& - \{ \OFFSET~\u32, \ALIGN~\u32 \} \\ + \{ \OFFSET~\u64, \ALIGN~\u32 \} \\ \production{lane width} & \X{ww} &::=& 8 ~|~ 16 ~|~ 32 ~|~ 64 \\ \production{instruction} & \instr &::=& @@ -696,9 +696,6 @@ The static address offset is added to the dynamic address operand, yielding a 33 All values are read and written in |LittleEndian|_ byte order. A :ref:`trap ` results if any of the accessed memory bytes lies outside the address range implied by the memory's current size. -.. note:: - Future versions of WebAssembly might provide memory instructions with 64 bit address ranges. - The |MEMORYSIZE| instruction returns the current size of a memory. The |MEMORYGROW| instruction grows a memory by a given delta and returns the previous size, or :math:`-1` if enough memory cannot be allocated. Both instructions operate in units of :ref:`page size `. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 406eebde7..de441cd65 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -349,6 +349,25 @@ In a :ref:`module `, each member of a recursive type is assigned The syntax of sub types is :ref:`generalized ` for the purpose of specifying :ref:`validation ` and :ref:`execution `. +.. _index:: ! index type + pair: abstract syntax; index type + single: memory; index type + single: table; index type +.. _syntax-idxtype: + +Index Type +~~~~~~~~~~ + +*Index types* classify the values that can be used to index into +:ref:`memories ` and :ref:`tables `. + +.. math:: + \begin{array}{llll} + \production{index type} & \idxtype &::=& + \I32 ~|~ \I64 \\ + \end{array} + + .. index:: ! limits, memory type, table type pair: abstract syntax; limits single: memory; limits @@ -363,7 +382,7 @@ Limits .. math:: \begin{array}{llrl} \production{limits} & \limits &::=& - \{ \LMIN~\u32, \LMAX~\u32^? \} \\ + \{ \LMIN~\u64, \LMAX~\u64^? \} \\ \end{array} If no maximum is given, the respective storage can grow to any size. @@ -383,7 +402,7 @@ Memory Types .. math:: \begin{array}{llrl} \production{memory type} & \memtype &::=& - \limits \\ + ~\idxtype~\limits \\ \end{array} The limits constrain the minimum and optionally the maximum size of a memory. @@ -404,7 +423,7 @@ Table Types .. math:: \begin{array}{llrl} \production{table type} & \tabletype &::=& - \limits~\reftype \\ + ~\idxtype~\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 591ca2e0a..b5412ba34 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -365,11 +365,13 @@ A :ref:`data segment ` can be given inline with a memory definition, .. math:: \begin{array}{llclll} \production{module field} & - \text{(}~\text{memory}~~\Tid^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad - \text{(}~\text{memory}~~\Tid'~~m~~m~\text{)} \\ & \qquad - \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\X{it}^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad + \text{(}~\text{memory}~~\Tid'~~\X{it}^?~~m~~m~\text{)} \\ & \qquad + \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{it}'~\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} \\ & \qquad\qquad - (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, m = \F{ceil}(n / 64\,\F{Ki})) \\ + (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad + \iff it^? \neq \epsilon \wedge \X{it}' = \X{it}^? \vee \X{it}^? = \epsilon \wedge \X{it}' = \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/text/types.rst b/document/core/text/types.rst index 731af495a..6833f3e2a 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -282,6 +282,32 @@ Similarly, final sub types with no super-types can omit the |Tsub| keyword and a \end{array} +.. index:: index type + pair: text format; index type +.. _text-idxtype: + +Index Type +~~~~~~~~~~ + +.. math:: + \begin{array}{llclll} + \production{index type} & \Tidxtype &::=& + \text{i32} &\Rightarrow& \I32 \\ &&|& + \text{i64} &\Rightarrow& \I64 \\ + \end{array} + +Abbreviations +............. + +The index type can be omited, in which case it defaults :math:`\I32`: + +.. math:: + \begin{array}{llclll} + \production{index type} & + \text{} &\equiv& \text{i32} + \end{array} + + .. index:: limits pair: text format; limits .. _text-limits: @@ -307,7 +333,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{memory type} & \Tmemtype_I &::=& - \X{lim}{:}\Tlimits &\Rightarrow& \X{lim} \\ + \X{it}{:}\Tidxtype~~\X{lim}{:}\Tlimits &\Rightarrow& \X{it}~\X{lim} \\ \end{array} @@ -321,7 +347,7 @@ Table Types .. math:: \begin{array}{llclll} \production{table type} & \Ttabletype_I &::=& - \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{lim}~\X{et} \\ + \X{it}{:}\Tidxtype~~\X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{it}~\X{lim}~\X{et} \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 84cb8ffb0..b666f5b69 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -269,6 +269,7 @@ .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} +.. |idxtype| mathdef:: \xref{syntax/types}{syntax-idxtype}{\X{idxtype}} .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}} .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}} @@ -913,6 +914,7 @@ .. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}} .. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}} +.. |Tidxtype| mathdef:: \xref{text/types}{text-idxtype}{\T{idxtype}} .. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}} .. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 139b5a584..528476068 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1753,15 +1753,17 @@ Memory Instructions * The memory :math:`C.\CMEMS[y]` must be defined in the context. -* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. + +* Then the instruction is valid with type :math:`[it~it~it] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it1}~\limits1 \qquad - C.\CMEMS[x] = \memtype + C.\CMEMS[y] = \X{it2}~\limits2 }{ - C \vdashinstr \MEMORYCOPY~x~y : [\I32~\I32~\I32] \to [] + C \vdashinstr \MEMORYCOPY~x~y : [\X{it}~\X{it}~\X{it}] \to [] } From d5e1a957af00205c7c5ec4d0b64a3c42284d42cd Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Mon, 24 Jun 2024 13:33:40 -0700 Subject: [PATCH 2/8] feedback --- document/core/binary/instructions.rst | 2 +- document/core/exec/instructions.rst | 28 +++++++++++++-------------- document/core/syntax/types.rst | 4 ++++ document/core/text/modules.rst | 2 +- document/core/valid/instructions.rst | 14 +++++++++----- 5 files changed, 29 insertions(+), 21 deletions(-) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 284c7719e..e54aabc3f 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -280,7 +280,7 @@ Each variant of :ref:`memory instruction ` is encoded with \production{memory argument} & \Bmemarg &::=& a{:}\Bu32~~o{:}\Bu64 &\Rightarrow& 0~\{ \ALIGN~a,~\OFFSET~o \} & (\iff a < 2^6) \\ &&|& - a{:}\Bu32~~x{:}\memidx~~o{:}\Bu32 &\Rightarrow& x~\{ \ALIGN~(a - 2^6),~\OFFSET~o \} + a{:}\Bu32~~x{:}\memidx~~o{:}\Bu64 &\Rightarrow& x~\{ \ALIGN~(a - 2^6),~\OFFSET~o \} & (\iff 2^6 \leq a < 2^7) \\ \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{28}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD~m \\ &&|& diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 224e77483..0383497ef 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3682,15 +3682,15 @@ Memory Instructions 9. Let :math:`\X{mem}_s` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{sa}]`. -10. Let :math:`\X{it}_d~\limits` be the :math:`\X{mem}_d.\MITYPE`. +10. Let :math:`\X{it}_d~\limits_d` be the :math:`\X{mem}_d.\MITYPE`. -11. Let :math:`\X{it}_s~\limits` be the :math:`\X{mem}_s.\MITYPE`. +11. Let :math:`\X{it}_s~\limits_s` be the :math:`\X{mem}_s.\MITYPE`. -12. Let :math:`\X{it}_{min}` be ....? +12. Let :math:`\X{it}_n` be the :ref:`minimum ` of :math:`\X{it}_s` and :math:`\X{it}_d`. -13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_{min}` is on the top of the stack. +13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_n` is on the top of the stack. -14. Pop the value :math:`\X{it}_{min}.\CONST~n` from the stack. +14. Pop the value :math:`\X{it}_n.\CONST~n` from the stack. 15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_s` is on the top of the stack. @@ -3710,9 +3710,9 @@ Memory Instructions 21. If :math:`d \leq s`, then: - a. Push the value :math:`\X{it}.\CONST~d` to the stack. + a. Push the value :math:`\X{it}_d.\CONST~d` to the stack. - b. Push the value :math:`\X{it}.\CONST~s` to the stack. + b. Push the value :math:`\X{it}_s.\CONST~s` to the stack. c. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`. @@ -3720,31 +3720,31 @@ Memory Instructions e. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. + f. Push the value :math:`\X{it}_d.\CONST~(d+1)` to the stack. g. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. - h. Push the value :math:`\X{it}.\CONST~(s+1)` to the stack. + h. Push the value :math:`\X{it}_s.\CONST~(s+1)` to the stack. 22. Else: a. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`. - b. Push the value :math:`\X{it}.\CONST~(d+n-1)` to the stack. + b. Push the value :math:`\X{it}_d.\CONST~(d+n-1)` to the stack. c. Assert: due to the earlier check against the memory size, :math:`s+n-1 < 2^{32}`. - d. Push the value :math:`\X{it}.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{it}_s.\CONST~(s+n-1)` to the stack. e. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}`. f. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}`. - g. Push the value :math:`\X{it}.\CONST~d` to the stack. + g. Push the value :math:`\X{it}_d.\CONST~d` to the stack. - h. Push the value :math:`\X{it}.\CONST~s` to the stack. + h. Push the value :math:`\X{it}_s.\CONST~s` to the stack. -23. Push the value :math:`\X{it}_{min}.\CONST~(n-1)` to the stack. +23. Push the value :math:`\X{it}.\CONST~(n-1)` to the stack. 24. Execute the instruction :math:`\MEMORYCOPY~x~y`. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index de441cd65..e84c10e06 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -367,6 +367,10 @@ Index Type \I32 ~|~ \I64 \\ \end{array} +.. _aux-idxtype-min: + +The minimum of two index types is defined as |I32| if either of the types are +|I32| and |I64| otherwise. .. index:: ! limits, memory type, table type pair: abstract syntax; limits diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index b5412ba34..541f960f0 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -367,7 +367,7 @@ A :ref:`data segment ` can be given inline with a memory definition, \production{module field} & \text{(}~\text{memory}~~\Tid^?~~\X{it}^?~~\text{(}~\text{data}~~b^n{:}\Tdatastring~\text{)}~~\text{)} \quad\equiv \\ & \qquad \text{(}~\text{memory}~~\Tid'~~\X{it}^?~~m~~m~\text{)} \\ & \qquad - \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{it}'~\text{.const}~~\text{0}~\text{)}~~\Tdatastring~\text{)} + \text{(}~\text{data}~~\text{(}~\text{memory}~~\Tid'~\text{)}~~\text{(}~\X{it}'\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 it^? \neq \epsilon \wedge \X{it}' = \X{it}^? \vee \X{it}^? = \epsilon \wedge \X{it}' = \text{i32}, \\ & \qquad\qquad diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 528476068..7e26a2006 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1753,17 +1753,21 @@ Memory Instructions * The memory :math:`C.\CMEMS[y]` must be defined in the context. -* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. +* Let :math:`\X{it}_x~\limits_x` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. -* Then the instruction is valid with type :math:`[it~it~it] \to []`. +* Let :math:`\X{it}_y~\limits_y` be the :ref:`memory type ` :math:`C.\CMEMS[y]`. + +* Let :math:`\X{it}` be the :ref:`minimum ` of :math:`\X{it}_x` and :math:`\X{it}_y` + +* Then the instruction is valid with type :math:`[\X{it}_x~\X{it}_y~\X{it}] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \X{it1}~\limits1 + C.\CMEMS[x] = \X{it}_x~\limits_y \qquad - C.\CMEMS[y] = \X{it2}~\limits2 + C.\CMEMS[y] = \X{it}_y~\limits_y }{ - C \vdashinstr \MEMORYCOPY~x~y : [\X{it}~\X{it}~\X{it}] \to [] + C \vdashinstr \MEMORYCOPY~x~y : [\X{it}_x~\X{it}_y~\X{it}] \to [] } From b925e4a8473477cd6e571f82952fa00f7f1f4e85 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Mon, 24 Jun 2024 16:18:29 -0700 Subject: [PATCH 3/8] validation rules --- document/core/valid/instructions.rst | 155 ++++++++++++++++----------- 1 file changed, 90 insertions(+), 65 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 7e26a2006..1cfe236d4 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1328,15 +1328,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[\I32] \to [t]`. +* Then the instruction is valid with type :math:`[\X{it}] \to [t]`. .. math:: \frac{ - C.\CTABLES[x] = \limits~t + C.\CTABLES[x] = \X{it}~\limits~t }{ - C \vdashinstr \TABLEGET~x : [\I32] \to [t] + C \vdashinstr \TABLEGET~x : [\X{it}] \to [t] } @@ -1347,15 +1347,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[\I32~t] \to []`. +* Then the instruction is valid with type :math:`[\X{it}~t] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \limits~t + C.\CTABLES[x] = \X{it}~\limits~t }{ - C \vdashinstr \TABLESET~x : [\I32~t] \to [] + C \vdashinstr \TABLESET~x : [\X{it}~t] \to [] } @@ -1366,13 +1366,13 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Then the instruction is valid with type :math:`[] \to [\I32]`. +* Then the instruction is valid with type :math:`[] \to [\X{it}]`. .. math:: \frac{ - C.\CTABLES[x] = \tabletype + C.\CTABLES[x] = \X{it}~\limits~t }{ - C \vdashinstr \TABLESIZE~x : [] \to [\I32] + C \vdashinstr \TABLESIZE~x : [] \to [\X{it}] } @@ -1383,15 +1383,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[t~\I32] \to [\I32]`. +* Then the instruction is valid with type :math:`[t~\X{it}] \to [\X{it}]`. .. math:: \frac{ - C.\CTABLES[x] = \limits~t + C.\CTABLES[x] = \X{it}~\limits~t }{ - C \vdashinstr \TABLEGROW~x : [t~\I32] \to [\I32] + C \vdashinstr \TABLEGROW~x : [t~\X{it}] \to [\X{it}] } @@ -1402,15 +1402,15 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* Then the instruction is valid with type :math:`[\I32~t~\I32] \to []`. +* Then the instruction is valid with type :math:`[\X{it}~t~\X{it}] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \limits~t + C.\CTABLES[x] = \X{it}~\limits~t }{ - C \vdashinstr \TABLEFILL~x : [\I32~t~\I32] \to [] + C \vdashinstr \TABLEFILL~x : [\X{it}~t~\X{it}] \to [] } @@ -1421,25 +1421,27 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits_1~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}_1~\limits_1~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The table :math:`C.\CTABLES[y]` must be defined in the context. -* Let :math:`\limits_2~t_2` be the :ref:`table type ` :math:`C.\CTABLES[y]`. +* Let :math:`\X{it}_2~\limits_2~t_2` be the :ref:`table type ` :math:`C.\CTABLES[y]`. + +* Let :math:`\X{it}` be the :ref:`minimum ` of :math:`\X{it}_1` and :math:`\X{it}_2` * The :ref:`reference type ` :math:`t_2` must :ref:`match ` :math:`t_1`. -* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. +* Then the instruction is valid with type :math:`[\X{it}_1~\X{it}_2~\X{it}] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \limits_1~t_1 + C.\CTABLES[x] = \X{it}~\limits_1~t_1 \qquad - C.\CTABLES[y] = \limits_2~t_2 + C.\CTABLES[y] = \X{it}~\limits_2~t_2 \qquad C \vdashreftypematch t_2 \matchesvaltype t_1 }{ - C \vdashinstr \TABLECOPY~x~y : [\I32~\I32~\I32] \to [] + C \vdashinstr \TABLECOPY~x~y : [\X{it}_1~\X{it}_2~\X{it}] \to [] } @@ -1450,7 +1452,7 @@ Table Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t_1` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The element segment :math:`C.\CELEMS[y]` must be defined in the context. @@ -1458,17 +1460,17 @@ Table Instructions * The :ref:`reference type ` :math:`t_2` must :ref:`match ` :math:`t_1`. -* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. +* Then the instruction is valid with type :math:`[\X{it}~\I32~\I32] \to []`. .. math:: \frac{ - C.\CTABLES[x] = \limits~t_1 + C.\CTABLES[x] = \X{it}~\limits~t_1 \qquad C.\CELEMS[y] = t_2 \qquad C \vdashreftypematch t_2 \matchesvaltype t_1 }{ - C \vdashinstr \TABLEINIT~x~y : [\I32~\I32~\I32] \to [] + C \vdashinstr \TABLEINIT~x~y : [\X{it}~\I32~\I32] \to [] } @@ -1505,17 +1507,19 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. -* Then the instruction is valid with type :math:`[\I32] \to [t]`. +* Then the instruction is valid with type :math:`[\X{it}] \to [t]`. .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ - C \vdashinstr t\K{.load}~x~\memarg : [\I32] \to [t] + C \vdashinstr t\K{.load}~x~\memarg : [\X{it}] \to [t] } @@ -1526,9 +1530,11 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\I32] \to [t]`. +* Then the instruction is valid with type :math:`[\X{it}] \to [t]`. .. math:: \frac{ @@ -1536,7 +1542,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr t\K{.load}N\K{\_}\sx~x~\memarg : [\I32] \to [t] + C \vdashinstr t\K{.load}N\K{\_}\sx~x~\memarg : [\X{it}] \to [t] } @@ -1545,9 +1551,11 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. -* Then the instruction is valid with type :math:`[\I32~t] \to []`. +* Then the instruction is valid with type :math:`[\X{it}~t] \to []`. .. math:: \frac{ @@ -1555,7 +1563,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ - C \vdashinstr t\K{.store}~x~\memarg : [\I32~t] \to [] + C \vdashinstr t\K{.store}~x~\memarg : [\X{it}~t] \to [] } @@ -1568,7 +1576,7 @@ Memory Instructions * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\I32~t] \to []`. +* Then the instruction is valid with type :math:`[\X{it}~t] \to []`. .. math:: \frac{ @@ -1576,7 +1584,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr t\K{.store}N~x~\memarg : [\I32~t] \to [] + C \vdashinstr t\K{.store}N~x~\memarg : [\X{it}~t] \to [] } @@ -1587,9 +1595,11 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8 \cdot M`. -* Then the instruction is valid with type :math:`[\I32] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`. .. math:: \frac{ @@ -1597,7 +1607,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 \cdot M }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg : [\I32] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg : [\X{it}] \to [\V128] } @@ -1608,9 +1618,11 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\I32] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`. .. math:: \frac{ @@ -1618,7 +1630,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{\_splat}~x~\memarg : [\I32] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{\_splat}~x~\memarg : [\X{it}] \to [\V128] } @@ -1629,9 +1641,11 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. -* Then the instruction is valid with type :math:`[\I32] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`. .. math:: \frac{ @@ -1639,7 +1653,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{\_zero}~x~\memarg : [\I32] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{\_zero}~x~\memarg : [\X{it}] \to [\V128] } @@ -1650,11 +1664,13 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. * The lane index :math:`\laneidx` must be smaller than :math:`128/N`. -* Then the instruction is valid with type :math:`[\I32~\V128] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{it}~\V128] \to [\V128]`. .. math:: \frac{ @@ -1664,7 +1680,7 @@ Memory Instructions \qquad \laneidx < 128/N }{ - C \vdashinstr \K{v128.}\LOAD{N}\K{\_lane}~x~\memarg~\laneidx : [\I32~\V128] \to [\V128] + C \vdashinstr \K{v128.}\LOAD{N}\K{\_lane}~x~\memarg~\laneidx : [\X{it}~\V128] \to [\V128] } @@ -1675,11 +1691,12 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`. * The lane index :math:`\laneidx` must be smaller than :math:`128/N`. -* Then the instruction is valid with type :math:`[\I32~\V128] \to [\V128]`. +* Then the instruction is valid with type :math:`[\X{it}~\V128] \to [\V128]`. .. math:: \frac{ @@ -1689,7 +1706,7 @@ Memory Instructions \qquad \laneidx < 128/N }{ - C \vdashinstr \K{v128.}\STORE{N}\K{\_lane}~x~\memarg~\laneidx : [\I32~\V128] \to [] + C \vdashinstr \K{v128.}\STORE{N}\K{\_lane}~x~\memarg~\laneidx : [\X{it}~\V128] \to [] } @@ -1700,13 +1717,15 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Then the instruction is valid with type :math:`[] \to [\I32]`. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + +* Then the instruction is valid with type :math:`[] \to [\X{it}]`. .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits }{ - C \vdashinstr \MEMORYSIZE~x : [] \to [\I32] + C \vdashinstr \MEMORYSIZE~x : [] \to [\X{it}] } @@ -1717,13 +1736,15 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Then the instruction is valid with type :math:`[\I32] \to [\I32]`. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + +* Then the instruction is valid with type :math:`[\X{it}] \to [\X{it}]`. .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits }{ - C \vdashinstr \MEMORYGROW~x : [\I32] \to [\I32] + C \vdashinstr \MEMORYGROW~x : [\X{it}] \to [\X{it}] } @@ -1734,13 +1755,15 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. -* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + +* Then the instruction is valid with type :math:`[\X{it}~\I32~\X{it}] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits }{ - C \vdashinstr \MEMORYFILL~x : [\I32~\I32~\I32] \to [] + C \vdashinstr \MEMORYFILL~x : [\X{it}~\I32~\X{it}] \to [] } @@ -1778,17 +1801,19 @@ Memory Instructions * The memory :math:`C.\CMEMS[x]` must be defined in the context. +* Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`C.\CMEMS[x]`. + * The data segment :math:`C.\CDATAS[y]` must be defined in the context. -* Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`. +* Then the instruction is valid with type :math:`[\X{it}~\I32~\I32] \to []`. .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad C.\CDATAS[y] = {\ok} }{ - C \vdashinstr \MEMORYINIT~x~y : [\I32~\I32~\I32] \to [] + C \vdashinstr \MEMORYINIT~x~y : [\X{it}~\I32~\I32] \to [] } @@ -2222,7 +2247,7 @@ Control Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The :ref:`reference type ` :math:`t` must :ref:`match ` type :math:`\REF~\NULL~\FUNC`. @@ -2234,13 +2259,13 @@ Control Instructions .. math:: \frac{ - C.\CTABLES[x] = \limits~t + C.\CTABLES[x] = \X{it}~\limits~t \qquad C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC \qquad \expanddt(C.\CTYPES[y]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] }{ - C \vdashinstr \CALLINDIRECT~x~y : [t_1^\ast~\I32] \to [t_2^\ast] + C \vdashinstr \CALLINDIRECT~x~y : [t_1^\ast~\X{it}] \to [t_2^\ast] } @@ -2311,7 +2336,7 @@ Control Instructions * The table :math:`C.\CTABLES[x]` must be defined in the context. -* Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. +* Let :math:`\X{it}~\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. * The :ref:`reference type ` :math:`t` must :ref:`match ` type :math:`\REF~\NULL~\FUNC`. @@ -2325,7 +2350,7 @@ Control Instructions .. math:: \frac{ - C.\CTABLES[x] = \limits~t + C.\CTABLES[x] = \X{it}~\limits~t \qquad C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC \qquad From 2472d29799766dca797f545a72c73c365a467efa Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Tue, 25 Jun 2024 16:38:30 -0700 Subject: [PATCH 4/8] feedback --- document/core/exec/instructions.rst | 2 +- document/core/syntax/types.rst | 14 ++++++++++++-- document/core/util/macros.def | 1 + document/core/valid/instructions.rst | 8 ++++---- 4 files changed, 18 insertions(+), 7 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 0383497ef..3d23eb22d 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3744,7 +3744,7 @@ Memory Instructions h. Push the value :math:`\X{it}_s.\CONST~s` to the stack. -23. Push the value :math:`\X{it}.\CONST~(n-1)` to the stack. +23. Push the value :math:`\X{it}_n.\CONST~(n-1)` to the stack. 24. Execute the instruction :math:`\MEMORYCOPY~x~y`. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index e84c10e06..838ff87eb 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -369,8 +369,18 @@ Index Type .. _aux-idxtype-min: -The minimum of two index types is defined as |I32| if either of the types are -|I32| and |I64| otherwise. +Conventions +........... + +The *minimum* of two index types is defined as |I32| if either of the types are +|I32|, and |I64| otherwise. + +.. math:: + \begin{array}{llll} + \itmin(\I64, \I64) &=& \I64 \\ + \itmin(\X{it}_1, \X{it}_2) &=& \I32 & (\otherwise) \\ + \end{array} + .. index:: ! limits, memory type, table type pair: abstract syntax; limits diff --git a/document/core/util/macros.def b/document/core/util/macros.def index b666f5b69..dd17dcf9f 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -293,6 +293,7 @@ .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}} +.. |itmin| mathdef:: \xref{syntax/types}{aux-idxtype-min}{\F{itmin}} .. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}} .. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 1cfe236d4..516165f1c 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1431,7 +1431,7 @@ Table Instructions * The :ref:`reference type ` :math:`t_2` must :ref:`match ` :math:`t_1`. -* Then the instruction is valid with type :math:`[\X{it}_1~\X{it}_2~\X{it}] \to []`. +* Then the instruction is valid with type :math:`[\X{it}_1~\X{it}_2~\itmin(\X{it}_1, \X{it}_2)] \to []`. .. math:: \frac{ @@ -1441,7 +1441,7 @@ Table Instructions \qquad C \vdashreftypematch t_2 \matchesvaltype t_1 }{ - C \vdashinstr \TABLECOPY~x~y : [\X{it}_1~\X{it}_2~\X{it}] \to [] + C \vdashinstr \TABLECOPY~x~y : [\X{it}_1~\X{it}_2~\itmin(\X{it}_1, \X{it}_2)] \to [] } @@ -1782,7 +1782,7 @@ Memory Instructions * Let :math:`\X{it}` be the :ref:`minimum ` of :math:`\X{it}_x` and :math:`\X{it}_y` -* Then the instruction is valid with type :math:`[\X{it}_x~\X{it}_y~\X{it}] \to []`. +* Then the instruction is valid with type :math:`[\X{it}_x~\X{it}_y~\itmin(\X{it}_x, \X{it}_y)] \to []`. .. math:: \frac{ @@ -1790,7 +1790,7 @@ Memory Instructions \qquad C.\CMEMS[y] = \X{it}_y~\limits_y }{ - C \vdashinstr \MEMORYCOPY~x~y : [\X{it}_x~\X{it}_y~\X{it}] \to [] + C \vdashinstr \MEMORYCOPY~x~y : [\X{it}_x~\X{it}_y~\itmin(\X{it}_x, \X{it}_y)] \to [] } From 223b6c834b30d4e2146b5f9490c1675fbfe2f8b6 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Wed, 26 Jun 2024 15:14:04 -0700 Subject: [PATCH 5/8] exec spec --- document/core/exec/instructions.rst | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3d23eb22d..5e3ac9057 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3751,12 +3751,15 @@ Memory Instructions .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY~x~y + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}.\CONST~n)~\MEMORYCOPY~x~y \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| \\ - \vee & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MIDATA|) \\[1ex] + (\iff & (d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| \\ + \vee & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MIDATA|) \\ + \land & \X{it}_x~\limits_x = S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MITYPE \\[1ex] + \land & \X{it}_y~\limits_y = S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MITYPE \\[1ex] + \land & \X{it} = \itmin(\X{it}_x,\X{it}_y)) \end{array} \\[1ex] S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\MEMORYCOPY~x~y From f124d363c7b90633fc6f5dfb8dee3fe4c84f28e5 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Fri, 28 Jun 2024 10:08:47 -0700 Subject: [PATCH 6/8] feedback --- document/core/exec/instructions.rst | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 5e3ac9057..bde8f20a0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3756,10 +3756,7 @@ Memory Instructions \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & (d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| \\ - \vee & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MIDATA|) \\ - \land & \X{it}_x~\limits_x = S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MITYPE \\[1ex] - \land & \X{it}_y~\limits_y = S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MITYPE \\[1ex] - \land & \X{it} = \itmin(\X{it}_x,\X{it}_y)) + \vee & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MIDATA|)) \\ \end{array} \\[1ex] S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\MEMORYCOPY~x~y From 4c4bf1883a451f2cc329b767f93968d08e4f8315 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Fri, 28 Jun 2024 10:53:15 -0700 Subject: [PATCH 7/8] exec rules --- document/core/exec/instructions.rst | 546 +++++++++++++++------------- 1 file changed, 293 insertions(+), 253 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index bde8f20a0..ed7b0e5bd 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2541,28 +2541,30 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. -7. Pop the value :math:`\I32.\CONST~i` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. + +8. Pop the value :math:`\X{it}.\CONST~i` from the stack. -8. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: +9. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -9. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. +10. Let :math:`\val` be the value :math:`\X{tab}.\TIELEM[i]`. -10. Push the value :math:`\val` to the stack. +11. Push the value :math:`\val` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \val + S; F; (\X{it}.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \val \end{array} \\ \qquad (\iff S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \val) \\ \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(\TABLEGET~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2584,30 +2586,32 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. -7. Pop the value :math:`\val` from the stack. +7. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Pop the value :math:`\val` from the stack. -9. Pop the value :math:`\I32.\CONST~i` from the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -10. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: +10. Pop the value :math:`\X{it}.\CONST~i` from the stack. + +11. If :math:`i` is not smaller than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -11. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. +12. Replace the element :math:`\X{tab}.\TIELEM[i]` with :math:`\val`. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\TABLESET~x) &\stepto& S'; F; \epsilon + S; F; (\X{it}.\CONST~i)~\val~(\TABLESET~x) &\stepto& S'; F; \epsilon \end{array} \\ \qquad (\iff S' = S \with \STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \val) \\ \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\TABLESET~x) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~\val~(\TABLESET~x) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -2629,14 +2633,16 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{sz}` be the length of :math:`\X{tab}.\TIELEM`. +6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. -7. Push the value :math:`\I32.\CONST~\X{sz}` to the stack. +7. Let :math:`\X{sz}` be the length of :math:`\X{tab}.\TIELEM`. + +8. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\TABLESIZE~x) &\stepto& S; F; (\I32.\CONST~\X{sz}) + S; F; (\TABLESIZE~x) &\stepto& S; F; (\X{it}.\CONST~\X{sz}) \end{array} \\ \qquad (\iff |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM| = \X{sz}) \\ @@ -2658,37 +2664,39 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. +6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +7. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. -8. Pop the value :math:`\I32.\CONST~n` from the stack. +8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -9. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +9. Pop the value :math:`\X{it}.\CONST~n` from the stack. -10. Pop the value :math:`\val` from the stack. +10. 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. -11. Let :math:`\X{err}` be the |i32| value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +12. Let :math:`\X{err}` be the :math:`\X{it}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. -12. Either: +13. Either: a. If :ref:`growing ` :math:`\X{tab}` by :math:`n` entries with initialization value :math:`\val` succeeds, then: - i. Push the value :math:`\I32.\CONST~\X{sz}` to the stack. + i. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. b. Else: - i. Push the value :math:`\I32.\CONST~\X{err}` to the stack. + i. Push the value :math:`\X{it}.\CONST~\X{err}` to the stack. -13. Or: +14. Or: - a. push the value :math:`\I32.\CONST~\X{err}` to the stack. + a. push the value :math:`\X{it}.\CONST~\X{err}` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\I32.\CONST~\X{sz}) + S; F; \val~(\X{it}.\CONST~n)~(\TABLEGROW~x) &\stepto& S'; F; (\X{it}.\CONST~\X{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -2698,7 +2706,7 @@ Table Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; \val~(\I32.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1)) + S; F; \val~(\X{it}.\CONST~n)~(\TABLEGROW~x) &\stepto& S; F; (\X{it}.\CONST~\signed_{32}^{-1}(-1)) \end{array} \end{array} @@ -2726,60 +2734,62 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. -7. Pop the value :math:`\I32.\CONST~n` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -8. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. +8. Pop the value :math:`\X{it}.\CONST~n` from the stack. -9. Pop the value :math:`\val` from the stack. +9. Assert: due to :ref:`validation `, a :ref:`reference value ` 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. +10. Pop the value :math:`\val` from the stack. + +11. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -11. Pop the value :math:`\I32.\CONST~i` from the stack. +12. Pop the value :math:`\X{it}.\CONST~i` from the stack. -12. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: +13. If :math:`i + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: a. Trap. -12. If :math:`n` is :math:`0`, then: +13. If :math:`n` is :math:`0`, then: a. Return. -13. Push the value :math:`\I32.\CONST~i` to the stack. +14. Push the value :math:`\X{it}.\CONST~i` to the stack. -14. Push the value :math:`\val` to the stack. +15. Push the value :math:`\val` to the stack. -15. Execute the instruction :math:`\TABLESET~x`. +16. Execute the instruction :math:`\TABLESET~x`. -16. Push the value :math:`\I32.\CONST~(i+1)` to the stack. +17. Push the value :math:`\X{it}.\CONST~(i+1)` to the stack. -17. Push the value :math:`\val` to the stack. +18. Push the value :math:`\val` to the stack. -18. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +19. Push the value :math:`\X{it}.\CONST~(n-1)` to the stack. -19. Execute the instruction :math:`\TABLEFILL~x`. +20. Execute the instruction :math:`\TABLEFILL~x`. .. math:: \begin{array}{l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n)~(\TABLEFILL~x) + S; F; (\X{it}.\CONST~i)~\val~(\X{it}.\CONST~n)~(\TABLEFILL~x) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & i + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~x) + S; F; (\X{it}.\CONST~i)~\val~(\X{it}.\CONST~0)~(\TABLEFILL~x) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n+1)~(\TABLEFILL~x) + S; F; (\X{it}.\CONST~i)~\val~(\X{it}.\CONST~n+1)~(\TABLEFILL~x) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~i)~\val~(\TABLESET~x) \\ - (\I32.\CONST~i+1)~\val~(\I32.\CONST~n)~(\TABLEFILL~x) \\ + (\X{it}.\CONST~i)~\val~(\TABLESET~x) \\ + (\X{it}.\CONST~i+1)~\val~(\X{it}.\CONST~n)~(\TABLEFILL~x) \\ \end{array} \\ \qquad (\otherwise) \\ @@ -2809,31 +2819,37 @@ Table Instructions 9. Let :math:`\X{tab}_y` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_y]`. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +10. Let :math:`\X{it}_x~\limits_x` be the :math:`\X{tab}_x.\TITYPE`. -11. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Let :math:`\X{it}_y~\limits_y` be the :math:`\X{tab}_y.\TITYPE`. + +12. Let :math:`\X{it}_n` be the :ref:`minimum ` of :math:`\X{it}_s` and :math:`\X{it}_d`. -12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +13. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_n` is on the top of the stack. + +14. Pop the value :math:`\X{it}_n.\CONST~n` 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{it}_y` is on the top of the stack. -14. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +16. Pop the value :math:`\X{it}_y.\CONST~s` from the stack. -15. Pop the value :math:`\I32.\CONST~d` from the stack. +17. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}_x` is on the top of the stack. -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: +18. Pop the value :math:`\X{it}_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: a. Trap. -17. If :math:`n = 0`, then: +20. If :math:`n = 0`, then: a. Return. -18. If :math:`d \leq s`, then: +21. If :math:`d \leq s`, then: - a. Push the value :math:`\I32.\CONST~d` to the stack. + a. Push the value :math:`\X{it}_x.\CONST~d` to the stack. - b. Push the value :math:`\I32.\CONST~s` to the stack. + b. Push the value :math:`\X{it}_y.\CONST~s` to the stack. c. Execute the instruction :math:`\TABLEGET~y`. @@ -2841,38 +2857,38 @@ Table Instructions e. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. - f. Push the value :math:`\I32.\CONST~(d+1)` to the stack. + f. Push the value :math:`\X{it}_x.\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:`\I32.\CONST~(s+1)` to the stack. + h. Push the value :math:`\X{it}_y.\CONST~(s+1)` to the stack. -19. Else: +22. Else: a. Assert: due to the earlier check against the table size, :math:`d+n-1 < 2^{32}`. - b. Push the value :math:`\I32.\CONST~(d+n-1)` to the stack. + b. Push the value :math:`\X{it}_x.\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:`\I32.\CONST~(s+n-1)` to the stack. + d. Push the value :math:`\X{it}_y.\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:`\I32.\CONST~d` to the stack. + g. Push the value :math:`\X{it}_x.\CONST~d` to the stack. - h. Push the value :math:`\I32.\CONST~s` to the stack. + h. Push the value :math:`\X{it}_y.\CONST~s` to the stack. -20. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +23. Push the value :math:`\X{it}_n.\CONST~(n-1)` to the stack. -21. Execute the instruction :math:`\TABLECOPY~x~y`. +24. Execute the instruction :math:`\TABLECOPY~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -2880,27 +2896,27 @@ Table Instructions \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLECOPY~x~y) + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~0)~(\TABLECOPY~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d)~(\I32.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\ + (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\X{it}_x.\CONST~d+1)~(\X{it}_y.\CONST~s+1)~(\X{it}_n.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLECOPY~x~y) + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~(\TABLECOPY~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n)~(\I32.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ - (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\ + (\X{it}_x.\CONST~d+n)~(\X{it}_y.\CONST~s+n)~(\TABLEGET~y)~(\TABLESET~x) \\ + (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~(\TABLECOPY~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -2922,58 +2938,60 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. +6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. -7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. +7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. -8. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. +8. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[y]`. -9. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. +9. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +10. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. -11. Pop the value :math:`\I32.\CONST~n` from the stack. +11. Assert: due to :ref:`validation `, a value of :ref:`value type ` 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. +12. Pop the value :math:`\I32.\CONST~n` from the stack. -13. Pop the value :math:`\I32.\CONST~s` from the stack. +13. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -14. 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. -15. Pop the value :math:`\I32.\CONST~d` from the stack. +15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -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: +16. Pop the value :math:`\X{it}.\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: a. Trap. -17. If :math:`n = 0`, then: +18. If :math:`n = 0`, then: a. Return. -18. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. +19. Let :math:`\val` be the :ref:`reference value ` :math:`\X{elem}.\EIELEM[s]`. -19. Push the value :math:`\I32.\CONST~d` to the stack. +20. Push the value :math:`\X{it}.\CONST~d` to the stack. -20. Push the value :math:`\val` to the stack. +21. Push the value :math:`\val` to the stack. -21. Execute the instruction :math:`\TABLESET~x`. +22. Execute the instruction :math:`\TABLESET~x`. -22. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. +23. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. -23. Push the value :math:`\I32.\CONST~(d+1)` to the stack. +24. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. -24. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. +25. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. -25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +26. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +27. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -27. Execute the instruction :math:`\TABLEINIT~x~y`. +28. Execute the instruction :math:`\TABLEINIT~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x~y) + S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -2981,17 +2999,17 @@ Table Instructions \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex] \end{array} \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x~y) + S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x~y) + S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d)~\val~(\TABLESET~x) \\ - (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \\ + (\X{it}.\CONST~d)~\val~(\TABLESET~x) \\ + (\X{it}.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff \val = S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM[s]) \\ @@ -3057,39 +3075,41 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\I32.\CONST~i` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Pop the value :math:`\X{it}.\CONST~i` from the stack. -9. If :math:`N` is not part of the instruction, then: +9. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. + +10. 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`. -10. 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. -11. 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]`. -12. If :math:`N` and :math:`\sx` are part of the instruction, then: +13. 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)`. -13. Else: +14. Else: a. Let :math:`c` be the constant for which :math:`\bytes_t(c) = b^\ast`. -14. Push the value :math:`t.\CONST~c` to the stack. +15. Push the value :math:`t.\CONST~c` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(t.\LOAD~x~\memarg) &\stepto& S; F; (t.\CONST~c) + S; F; (\X{it}.\CONST~i)~(t.\LOAD~x~\memarg) &\stepto& S; F; (t.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3099,7 +3119,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(t.\LOAD{N}\K{\_}\sx~x~\memarg) &\stepto& + S; F; (\X{it}.\CONST~i)~(t.\LOAD{N}\K{\_}\sx~x~\memarg) &\stepto& S; F; (t.\CONST~\extend^{\sx}_{N,|t|}(n)) \end{array} \\ \qquad @@ -3110,7 +3130,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(t.\LOAD({N}\K{\_}\sx)^?~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3132,33 +3152,35 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\I32.\CONST~i` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Pop the value :math:`\X{it}.\CONST~i` from the stack. -9. If :math:`\X{ea} + M \cdot N /8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +9. 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: a. Trap. -10. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice M \cdot N /8]`. +11. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice M \cdot N /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]`. +12. Let :math:`m_k` be the integer for which :math:`\bytes_{\iM}(m_k) = b^\ast[k \cdot M/8 \slice M/8]`. -12. Let :math:`W` be the integer :math:`M \cdot 2`. +13. Let :math:`W` be the integer :math:`M \cdot 2`. -13. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. +14. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. -14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. +15. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. -15. Push the value :math:`\V128.\CONST~c` to the stack. +16. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\LOAD{M}\K{x}N\_\sx~x~\memarg) &\stepto& + S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{M}\K{x}N\_\sx~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad @@ -3171,7 +3193,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{M}\K{x}N\K{\_}\sx~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3193,31 +3215,33 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\I32.\CONST~i` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. + +8. Pop the value :math:`\X{it}.\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`. -9. 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. -10. 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]`. -11. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. +12. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. -12. Let :math:`L` be the integer :math:`128 / N`. +13. Let :math:`L` be the integer :math:`128 / N`. -13. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. +14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. -14. Push the value :math:`\V128.\CONST~c` to the stack. +15. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) + S; F; (\X{it}.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3228,7 +3252,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{N}\K{\_splat}~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3250,29 +3274,31 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\I32.\CONST~i` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -8. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +8. Pop the value :math:`\X{it}.\CONST~i` from the stack. -9. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +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: a. Trap. -10. 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]`. -11. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. +12. Let :math:`n` be the integer for which :math:`\bytes_{\iN}(n) = b^\ast`. -12. Let :math:`c` be the result of computing :math:`\extendu_{N,128}(n)`. +13. Let :math:`c` be the result of computing :math:`\extendu_{N,128}(n)`. -13. Push the value :math:`\V128.\CONST~c` to the stack. +14. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) + S; F; (\X{it}.\CONST~i)~(\V128\K{.}\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3283,7 +3309,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(\V128.\LOAD{N}\K{\_zero}~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3305,37 +3331,39 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\V128.\CONST~v` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Pop the value :math:`\V128.\CONST~v` from the stack. -9. Pop the value :math:`\I32.\CONST~i` from the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Pop the value :math:`\X{it}.\CONST~i` from the stack. -11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +11. 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: a. Trap. -12. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. +13. Let :math:`b^\ast` be the byte sequence :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]`. -13. Let :math:`r` be the constant for which :math:`\bytes_{\iN}(r) = b^\ast`. +14. Let :math:`r` be the constant for which :math:`\bytes_{\iN}(r) = b^\ast`. -14. Let :math:`L` be :math:`128 / N`. +15. Let :math:`L` be :math:`128 / N`. -15. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. +16. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. -16. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [y] = r)`. +17. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [y] = r)`. -17. Push the value :math:`\V128.\CONST~c` to the stack. +18. Push the value :math:`\V128.\CONST~c` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\CONST~v)~(\V128\K{.}\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; (\V128.\CONST~c) + S; F; (\X{it}.\CONST~i)~(\V128.\CONST~v)~(\V128\K{.}\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; (\V128.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3347,7 +3375,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(\V128.\CONST~v)~(\V128.\LOAD{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3370,41 +3398,43 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t` is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`t.\CONST~c` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t` is on the top of the stack. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Pop the value :math:`t.\CONST~c` from the stack. -9. Pop the value :math:`\I32.\CONST~i` from the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. + +10. Pop the value :math:`\X{it}.\CONST~i` from the stack. -10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +11. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. -11. If :math:`N` is not part of the instruction, then: +12. 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`. -12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +13. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: a. Trap. -13. If :math:`N` is part of the instruction, then: +14. 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)`. -14. Else: +15. Else: a. Let :math:`b^\ast` be the byte sequence :math:`\bytes_t(c)`. -15. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. +16. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE~x~\memarg) &\stepto& S'; F; \epsilon + S; F; (\X{it}.\CONST~i)~(t.\CONST~c)~(t.\STORE~x~\memarg) &\stepto& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3414,7 +3444,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}~x~\memarg) &\stepto& S'; F; \epsilon + S; F; (\X{it}.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}~x~\memarg) &\stepto& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3424,7 +3454,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~x~\memarg) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(t.\CONST~c)~(t.\STORE{N}^?~x~\memarg) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3446,33 +3476,35 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\V128` is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\V128.\CONST~c` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\V128` is on the top of the stack. -8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Pop the value :math:`\V128.\CONST~c` from the stack. -9. Pop the value :math:`\I32.\CONST~i` from the stack. +9. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -10. Let :math:`\X{ea}` be the integer :math:`i + \memarg.\OFFSET`. +10. Pop the value :math:`\X{it}.\CONST~i` from the stack. -11. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: +11. 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: a. Trap. -12. Let :math:`L` be :math:`128/N`. +13. Let :math:`L` be :math:`128/N`. -13. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. +14. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. -14. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[y])`. +15. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[y])`. -15. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. +16. Replace the bytes :math:`\X{mem}.\MIDATA[\X{ea} \slice N/8]` with :math:`b^\ast`. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S'; F; \epsilon + S; F; (\X{it}.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3483,7 +3515,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP + S; F; (\X{it}.\CONST~i)~(\V128.\CONST~c)~(\V128.\STORE{N}\K{\_lane}~x~\memarg~y) &\stepto& S; F; \TRAP \end{array} \\ \qquad (\otherwise) \\ @@ -3505,14 +3537,16 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{sz}` be the length of :math:`\X{mem}.\MIDATA` divided by the :ref:`page size `. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. + +7. Let :math:`\X{sz}` be the length of :math:`\X{mem}.\MIDATA` divided by the :ref:`page size `. -7. Push the value :math:`\I32.\CONST~\X{sz}` to the stack. +8. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\MEMORYSIZE~x) &\stepto& S; F; (\I32.\CONST~\X{sz}) + S; F; (\MEMORYSIZE~x) &\stepto& S; F; (\X{it}.\CONST~\X{sz}) \end{array} \\ \qquad (\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA| = \X{sz}\cdot64\,\F{Ki}) \\ @@ -3534,33 +3568,35 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size `. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +7. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size `. -8. Pop the value :math:`\I32.\CONST~n` from the stack. +8. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -9. Let :math:`\X{err}` be the |i32| value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. +9. Pop the value :math:`\X{it}.\CONST~n` from the stack. -10. Either: +10. Let :math:`\X{err}` be the :math:`\X{it}` value :math:`2^{32}-1`, for which :math:`\signed_{32}(\X{err})` is :math:`-1`. + +11. Either: a. If :ref:`growing ` :math:`\X{mem}` by :math:`n` :ref:`pages ` succeeds, then: - i. Push the value :math:`\I32.\CONST~\X{sz}` to the stack. + i. Push the value :math:`\X{it}.\CONST~\X{sz}` to the stack. b. Else: - i. Push the value :math:`\I32.\CONST~\X{err}` to the stack. + i. Push the value :math:`\X{it}.\CONST~\X{err}` to the stack. -11. Or: +12. Or: - a. Push the value :math:`\I32.\CONST~\X{err}` to the stack. + a. Push the value :math:`\X{it}.\CONST~\X{err}` to the stack. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\MEMORYGROW~x) &\stepto& S'; F; (\I32.\CONST~\X{sz}) + S; F; (\X{it}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S'; F; (\X{it}.\CONST~\X{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3570,7 +3606,7 @@ Memory Instructions \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\I32.\CONST~\signed_{32}^{-1}(-1)) + S; F; (\X{it}.\CONST~n)~(\MEMORYGROW~x) &\stepto& S; F; (\X{it}.\CONST~\signed_{32}^{-1}(-1)) \end{array} \end{array} @@ -3598,17 +3634,19 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Pop the value :math:`\I32.\CONST~n` from the stack. +7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. + +7. Pop the value :math:`\X{it}.\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. 9. Pop the value :math:`\val` from the stack. -10. 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 ` :math:`\X{it}` is on the top of the stack. -11. Pop the value :math:`\I32.\CONST~d` from the stack. +11. Pop the value :math:`\X{it}.\CONST~d` from the stack. 12. If :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: @@ -3622,37 +3660,37 @@ Memory Instructions 15. Push the value :math:`\val` to the stack. -16. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. +16. Execute the instruction :math:`\X{it}\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. 17. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -18. Push the value :math:`\I32.\CONST~(d+1)` to the stack. +18. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. 19. Push the value :math:`\val` to the stack. -20. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +20. Push the value :math:`\X{it}.\CONST~(n-1)` to the stack. 21. Execute the instruction :math:`\MEMORYFILL~x`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n)~\MEMORYFILL~x + S; F; (\X{it}.\CONST~d)~\val~(\X{it}.\CONST~n)~\MEMORYFILL~x \quad\stepto\quad S; F; \TRAP \\ \qquad (\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\[1ex] - S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~0)~\MEMORYFILL~x + S; F; (\X{it}.\CONST~d)~\val~(\X{it}.\CONST~0)~\MEMORYFILL~x \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n+1)~\MEMORYFILL~x + S; F; (\X{it}.\CONST~d)~\val~(\X{it}.\CONST~n+1)~\MEMORYFILL~x \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d)~\val~(\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\I32.\CONST~d+1)~\val~(\I32.\CONST~n)~\MEMORYFILL~x \\ + (\X{it}.\CONST~d)~\val~(\X{it}\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{it}.\CONST~d+1)~\val~(\X{it}.\CONST~n)~\MEMORYFILL~x \\ \end{array} \\ \qquad (\otherwise) \\ @@ -3751,7 +3789,7 @@ Memory Instructions .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}.\CONST~n)~\MEMORYCOPY~x~y + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~\MEMORYCOPY~x~y \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3759,31 +3797,31 @@ Memory Instructions \vee & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[y]].\MIDATA|)) \\ \end{array} \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\MEMORYCOPY~x~y + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~0)~\MEMORYCOPY~x~y \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\MEMORYCOPY~x~y + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~\MEMORYCOPY~x~y \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d) \\ - (\I32.\CONST~s)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{it}_x.\CONST~d) \\ + (\X{it}_y.\CONST~s)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~\MEMORYCOPY~x~y \\ + (\X{it}_x.\CONST~d+1)~(\X{it}_y.\CONST~s+1)~(\X{it}_n.\CONST~n)~\MEMORYCOPY~x~y \\ \end{array} \\ \qquad (\otherwise, \iff d \leq s) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\MEMORYCOPY~x~y + S; F; (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n+1)~\MEMORYCOPY~x~y \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d+n) \\ - (\I32.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{it}_x.\CONST~d+n) \\ + (\X{it}_y.\CONST~s+n)~(\I32\K{.}\LOAD\K{8\_u}~y~\{ \OFFSET~0, \ALIGN~0 \}) \\ (\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY~x~y \\ + (\X{it}_x.\CONST~d)~(\X{it}_y.\CONST~s)~(\X{it}_n.\CONST~n)~\MEMORYCOPY~x~y \\ \end{array} \\ \qquad (\otherwise, \iff d > s) \\ @@ -3805,58 +3843,60 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. +6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. -7. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. +7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. -8. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. +8. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[y]`. -9. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. +9. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. -10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +10. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. -11. Pop the value :math:`\I32.\CONST~n` from the stack. +11. 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. -12. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +13. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -13. Pop the value :math:`\I32.\CONST~s` from the stack. +14. Pop the value :math:`\I32.\CONST~s` from the stack. -14. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +15. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. -15. Pop the value :math:`\I32.\CONST~d` from the stack. +16. Pop the value :math:`\X{it}.\CONST~d` from the stack. -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: +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: a. Trap. -17. If :math:`n = 0`, then: +18. If :math:`n = 0`, then: a. Return. -18. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. +19. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. -19. Push the value :math:`\I32.\CONST~d` to the stack. +20. Push the value :math:`\X{it}.\CONST~d` to the stack. -20. Push the value :math:`\I32.\CONST~b` to the stack. +21. Push the value :math:`\I32.\CONST~b` to the stack. -21. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. +22. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. -22. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. +23. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -23. Push the value :math:`\I32.\CONST~(d+1)` to the stack. +24. Push the value :math:`\X{it}.\CONST~(d+1)` to the stack. -24. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. +25. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. -25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. +26. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. +27. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -27. Execute the instruction :math:`\MEMORYINIT~x~y`. +28. Execute the instruction :math:`\MEMORYINIT~x~y`. .. math:: ~\\[-1ex] \begin{array}{l} - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) + S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) \quad\stepto\quad S; F; \TRAP \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3864,17 +3904,17 @@ Memory Instructions \vee & s + n > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\MIDATA|) \\[1ex] \end{array} \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x~y) + S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x~y) \quad\stepto\quad S; F; \epsilon \\ \qquad (\otherwise) \\[1ex] - S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\MEMORYINIT~x~y) + S; F; (\X{it}.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\MEMORYINIT~x~y) \quad\stepto \\ \qquad S; F; \begin{array}[t]{@{}l@{}} - (\I32.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) \\ + (\X{it}.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~x~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\X{it}.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\MEMORYINIT~x~y) \\ \end{array} \\ \qquad (\otherwise, \iff b = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s]) \\ From e8045b6f510f5b2e9afd70c0c39bd7e9bd38a4b8 Mon Sep 17 00:00:00 2001 From: Sam Clegg Date: Mon, 1 Jul 2024 14:33:55 -0700 Subject: [PATCH 8/8] feedback --- document/core/exec/instructions.rst | 42 ++++++++++++++-------------- document/core/valid/instructions.rst | 16 +++++------ 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ed7b0e5bd..4743e18b7 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2541,7 +2541,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -2586,7 +2586,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. +6. Let :math:`\X{it}~\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. @@ -2633,7 +2633,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. 7. Let :math:`\X{sz}` be the length of :math:`\X{tab}.\TIELEM`. @@ -2664,7 +2664,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. 7. Let :math:`\X{sz}` be the length of :math:`S.\STABLES[a]`. @@ -2734,7 +2734,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -2819,9 +2819,9 @@ Table Instructions 9. Let :math:`\X{tab}_y` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}_y]`. -10. Let :math:`\X{it}_x~\limits_x` be the :math:`\X{tab}_x.\TITYPE`. +10. Let :math:`\X{it}_x~\limits_x` be the :ref:`table type ` :math:`\X{tab}_x.\TITYPE`. -11. Let :math:`\X{it}_y~\limits_y` be the :math:`\X{tab}_y.\TITYPE`. +11. Let :math:`\X{it}_y~\limits_y` be the :ref:`table type ` :math:`\X{tab}_y.\TITYPE`. 12. Let :math:`\X{it}_n` be the :ref:`minimum ` of :math:`\X{it}_s` and :math:`\X{it}_d`. @@ -2938,7 +2938,7 @@ Table Instructions 5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{tab}.\TITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`table type ` :math:`\X{tab}.\TITYPE`. 7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIELEMS[y]` exists. @@ -3075,7 +3075,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -3152,7 +3152,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -3215,7 +3215,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -3274,7 +3274,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -3331,7 +3331,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\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. @@ -3398,7 +3398,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\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. @@ -3476,7 +3476,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\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. @@ -3537,7 +3537,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Let :math:`\X{sz}` be the length of :math:`\X{mem}.\MIDATA` divided by the :ref:`page size `. @@ -3568,7 +3568,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\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 `. @@ -3634,7 +3634,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`\X{it}` is on the top of the stack. @@ -3720,9 +3720,9 @@ Memory Instructions 9. Let :math:`\X{mem}_s` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{sa}]`. -10. Let :math:`\X{it}_d~\limits_d` be the :math:`\X{mem}_d.\MITYPE`. +10. Let :math:`\X{it}_d~\limits_d` be the :ref:`memory type ` :math:`\X{mem}_d.\MITYPE`. -11. Let :math:`\X{it}_s~\limits_s` be the :math:`\X{mem}_s.\MITYPE`. +11. Let :math:`\X{it}_s~\limits_s` be the :ref:`memory type ` :math:`\X{mem}_s.\MITYPE`. 12. Let :math:`\X{it}_n` be the :ref:`minimum ` of :math:`\X{it}_s` and :math:`\X{it}_d`. @@ -3843,7 +3843,7 @@ Memory Instructions 5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[\X{ma}]`. -6. Let :math:`\X{it}~\limits` be the :math:`\X{mem}.\MITYPE`. +6. Let :math:`\X{it}~\limits` be the :ref:`memory type ` :math:`\X{mem}.\MITYPE`. 7. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIDATAS[y]` exists. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 516165f1c..fc83e1d7b 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1538,7 +1538,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ @@ -1559,7 +1559,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ @@ -1580,7 +1580,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ @@ -1603,7 +1603,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq N/8 \cdot M }{ @@ -1626,7 +1626,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ @@ -1649,7 +1649,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ @@ -1674,7 +1674,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} < N/8 \qquad @@ -1700,7 +1700,7 @@ Memory Instructions .. math:: \frac{ - C.\CMEMS[x] = \memtype + C.\CMEMS[x] = \X{it}~\limits \qquad 2^{\memarg.\ALIGN} < N/8 \qquad