diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 0e98a786..647ad426 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -54,6 +54,8 @@ Construct Judgement :ref:`Table instance ` :math:`S \vdashtableinst \tableinst : \tabletype` :ref:`Memory instance ` :math:`S \vdashmeminst \meminst : \memtype` :ref:`Global instance ` :math:`S \vdashglobalinst \globalinst : \globaltype` +:ref:`Element instance ` :math:`S \vdasheleminst \eleminst \ok` +:ref:`Data instance ` :math:`S \vdashdatainst \datainst \ok` :ref:`Export instance ` :math:`S \vdashexportinst \exportinst \ok` :ref:`Module instance ` :math:`S \vdashmoduleinst \moduleinst : C` :ref:`Store ` :math:`\vdashstore \store \ok` @@ -95,6 +97,8 @@ Construct Judgement :ref:`Table instance ` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2` :ref:`Memory instance ` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2` :ref:`Global instance ` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2` +:ref:`Element instance ` :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2` +:ref:`Data instance ` :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2` :ref:`Store ` :math:`\vdashstoreextends \store_1 \extendsto \store_2` =============================================== =============================================================================== diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index e1f5d8c0..83437f8b 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -100,6 +100,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Each :ref:`global instance ` :math:`\globalinst_i` in :math:`S.\SGLOBALS` must be :ref:`valid ` with some :ref:`global type ` :math:`\globaltype_i`. +* Each :ref:`element instance ` :math:`\eleminst_i` in :math:`S.\SELEMS` must be :ref:`valid `. + +* Each :ref:`data instance ` :math:`\datainst_i` in :math:`S.\SDATAS` must be :ref:`valid `. + * Then the store is valid. .. math:: @@ -114,11 +118,17 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \qquad (S \vdashglobalinst \globalinst : \globaltype)^\ast \\ + (S \vdasheleminst \eleminst \ok)^\ast + \qquad + (S \vdashdatainst \datainst \ok)^\ast + \\ S = \{ \SFUNCS~\funcinst^\ast, \STABLES~\tableinst^\ast, \SMEMS~\meminst^\ast, - \SGLOBALS~\globalinst^\ast \} + \SGLOBALS~\globalinst^\ast, + \SELEMS~\eleminst^\ast, + \SDATAS~\datainst^\ast \} \end{array} }{ \vdashstore S \ok @@ -224,7 +234,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. math:: \frac{ - ((S \vdash \EVFUNC~\X{fa} : \ETFUNC~\functype)^?)^n + ((S \vdashexternval \EVFUNC~\X{fa} : \ETFUNC~\functype)^?)^n \qquad \vdashlimits \{\LMIN~n, \LMAX~m^?\} : 2^{32} }{ @@ -265,6 +275,41 @@ Module instances are classified by *module contexts*, which are regular :ref:`co } +.. index:: element instance, reference +.. _valid-eleminst: + +:ref:`Element Instances ` :math:`\{ \EIELEM~\X{fa}^\ast \}` +............................................................................ + +* For each :ref:`function address ` :math:`\X{fa}_i` in the table elements :math:`\X{fa}^\ast`: + + * The :ref:`external value ` :math:`\EVFUNC~\X{fa}` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETFUNC~\X{ft}`. + +* Then the element instance is valid. + +.. math:: + \frac{ + (S \vdashexternval \EVFUNC~\X{fa} : \ETFUNC~\functype)^\ast + }{ + S \vdasheleminst \{ \EIELEM~\X{fa}^\ast \} \ok + } + + +.. index:: data instance, byte +.. _valid-datainst: + +:ref:`Data Instances ` :math:`\{ \DIDATA~b^\ast \}` +.................................................................... + +* The data instance is valid. + +.. math:: + \frac{ + }{ + S \vdashdatainst \{ \DIDATA~b^\ast \} \ok + } + + .. index:: external type, export instance, name, external value .. _valid-exportinst: @@ -299,6 +344,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * For each :ref:`global address ` :math:`\globaladdr_i` in :math:`\moduleinst.\MIGLOBALS`, the :ref:`external value ` :math:`\EVGLOBAL~\globaladdr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETGLOBAL~\globaltype_i`. +* For each :ref:`element address ` :math:`\elemaddr_i` in :math:`\moduleinst.\MIELEMS`, the :ref:`element instance ` :math:`S.\SELEMS[\elemaddr_i]` must be :ref:`valid `. + +* For each :ref:`data address ` :math:`\dataaddr_i` in :math:`\moduleinst.\MIDATAS`, the :ref:`data instance ` :math:`S.\SDATAS[\dataaddr_i]` must be :ref:`valid `. + * Each :ref:`export instance ` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` must be :ref:`valid `. * For each :ref:`export instance ` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS`, the :ref:`name ` :math:`\exportinst_i.\EINAME` must be different from any other name occurring in :math:`\moduleinst.\MIEXPORTS`. @@ -327,6 +376,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \qquad (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast \\ + (S \vdasheleminst S.\SELEMS[\elemaddr] \ok)^\ast + \qquad + (S \vdashdatainst S.\SDATAS[\dataaddr] \ok)^\ast + \\ (S \vdashexportinst \exportinst \ok)^\ast \qquad (\exportinst.\EINAME)^\ast ~\mbox{disjoint} @@ -338,7 +391,9 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ - \MIGLOBALS & \globaladdr^\ast \\ + \MIGLOBALS & \globaladdr^\ast, \\ + \MIELEMS & \elemaddr^\ast, \\ + \MIDATAS & \dataaddr^\ast, \\ \MIEXPORTS & \exportinst^\ast ~\} : \{ \begin{array}[t]{@{}l@{~}l@{}} \CTYPES & \functype^\ast, \\ @@ -560,6 +615,10 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * The length of :math:`S.\SGLOBALS` must not shrink. +* The length of :math:`S.\SELEMS` must not shrink. + +* The length of :math:`S.\SDATAS` must not shrink. + * For each :ref:`function instance ` :math:`\funcinst_i` in the original :math:`S.\SFUNCS`, the new function instance must be an :ref:`extension ` of the old. * For each :ref:`table instance ` :math:`\tableinst_i` in the original :math:`S.\STABLES`, the new table instance must be an :ref:`extension ` of the old. @@ -568,21 +627,31 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * For each :ref:`global instance ` :math:`\globalinst_i` in the original :math:`S.\SGLOBALS`, the new global instance must be an :ref:`extension ` of the old. +* For each :ref:`element instance ` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new global instance must be an :ref:`extension ` of the old. + +* For each :ref:`data instance ` :math:`\datainst_i` in the original :math:`S.\SDATAS`, the new global instance must be an :ref:`extension ` of the old. + .. math:: \frac{ \begin{array}{@{}ccc@{}} S_1.\SFUNCS = \funcinst_1^\ast & S_2.\SFUNCS = {\funcinst'_1}^\ast~\funcinst_2^\ast & - (\funcinst_1 \extendsto \funcinst'_1)^\ast \\ + (\vdashfuncinstextends \funcinst_1 \extendsto \funcinst'_1)^\ast \\ S_1.\STABLES = \tableinst_1^\ast & S_2.\STABLES = {\tableinst'_1}^\ast~\tableinst_2^\ast & - (\tableinst_1 \extendsto \tableinst'_1)^\ast \\ + (\vdashtableinstextends \tableinst_1 \extendsto \tableinst'_1)^\ast \\ S_1.\SMEMS = \meminst_1^\ast & S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast & - (\meminst_1 \extendsto \meminst'_1)^\ast \\ + (\vdashmeminstextends \meminst_1 \extendsto \meminst'_1)^\ast \\ S_1.\SGLOBALS = \globalinst_1^\ast & S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast & - (\globalinst_1 \extendsto \globalinst'_1)^\ast \\ + (\vdashglobalinstextends \globalinst_1 \extendsto \globalinst'_1)^\ast \\ + S_1.\SELEMS = \eleminst_1^\ast & + S_2.\SELEMS = {\eleminst'_1}^\ast~\eleminst_2^\ast & + (\vdasheleminstextends \eleminst_1 \extendsto \eleminst'_1)^\ast \\ + S_1.\SDATAS = \datainst_1^\ast & + S_2.\SDATAS = {\datainst'_1}^\ast~\datainst_2^\ast & + (\vdashdatainstextends \datainst_1 \extendsto \datainst'_1)^\ast \\ \end{array} }{ \vdashstoreextends S_1 \extendsto S_2 @@ -660,6 +729,38 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' } +.. index:: element instance +.. _extend-eleminst: + +:ref:`Element Instance ` :math:`\eleminst` +........................................................... + +* The vector :math:`\eleminst.\EIELEM` must either remain unchanged or shrink to length :math:`0`. + +.. math:: + \frac{ + \X{fa}_1^\ast = \X{fa}_2^\ast \vee \X{fa}_2^\ast = \epsilon + }{ + \vdasheleminstextends \{\EIELEM~\X{fa}_1^\ast\} \extendsto \{\EIELEM~\X{fa}_2^\ast\} + } + + +.. index:: data instance +.. _extend-datainst: + +:ref:`Data Instance ` :math:`\datainst` +........................................................ + +* The vector :math:`\datainst.\DIDATA` must either remain unchanged or shrink to length :math:`0`. + +.. math:: + \frac{ + b_1^\ast = b_2^\ast \vee b_2^\ast = \epsilon + }{ + \vdashdatainstextends \{\DIDATA~b_1^\ast\} \extendsto \{\DIDATA~b_2^\ast\} + } + + .. index:: ! preservation, ! progress, soundness, configuration, thread, terminal configuration, instantiation, invocation, validity, module .. _soundness-statement: diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index eecf0f8d..590d8ff6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -635,11 +635,11 @@ Memory Instructions 2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIMEMS[0]` exists. -3. Let :math:`a` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. +3. Let :math:`\X{ma}` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. -4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[a]` exists. +4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[\X{ma}]` exists. -5. Let :math:`\X{mem}` be the :ref:`memory instance ` :math:`S.\SMEMS[a]`. +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. @@ -651,31 +651,25 @@ Memory Instructions 10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -11. Pop the value :math:`\I32.\CONST~i` from the stack. +11. Pop the value :math:`\I32.\CONST~d` from the stack. -12. If :math:`n = 0`, then: +12. If :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: - a. Return. - -13. If :math:`n = 1`, then: - - a. Push the value :math:`\I32.\CONST~i` to the stack. - - b. Push the value :math:`\val` to the stack. + a. Trap. - c. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. +13. If :math:`n = 0`, then: - d. Return. + a. Return. -14. Push the value :math:`\I32.\CONST~i` to the stack. +14. Push the value :math:`\I32.\CONST~d` to the stack. 15. Push the value :math:`\val` to the stack. -16. Push the value :math:`\I32.\CONST~1` to the stack. +16. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. -17. Execute the instruction :math:`\MEMORYFILL`. +17. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -18. Push the value :math:`\vconst_{\I32}(i+1)` to the stack. +18. Push the value :math:`\I32.\CONST~(d+1)` to the stack. 19. Push the value :math:`\val` to the stack. @@ -684,28 +678,28 @@ Memory Instructions 21. Execute the instruction :math:`\MEMORYFILL`. .. math:: + ~\\[-1ex] \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\MEMORYFILL) &\stepto& S; F; \epsilon - \end{array} \\ - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~1)~(\MEMORYFILL) &\stepto& S; F; - (\I32.\CONST~i)~\val~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ - \end{array} \\ - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n)~(\MEMORYFILL) &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~i)~\val~(\I32.\CONST~1)~(\MEMORYFILL) \\ - (\vconst_{\I32}(i+1))~\val~(\I32.\CONST~(n-1))~(\MEMORYFILL) \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff n > 1) \\ + S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n)~\MEMORYFILL + \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 + \quad\stepto\quad S; F; \epsilon + \\ \qquad + (\otherwise) + \\[1ex] + S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n+1)~\MEMORYFILL + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d)~\val~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32.\CONST~d+1)~\val~(\I32.\CONST~n)~\MEMORYFILL \\ + \end{array} + \\ \qquad + (\otherwise) \\ \end{array} -.. note:: - The use of the :math:`\vconst_t` meta function in the rules for this and the following instructions ensures that an overflowing index turns into a :ref:`trap `. - .. _exec-memory.init: @@ -726,9 +720,9 @@ Memory Instructions 7. Let :math:`\X{da}` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[x]`. -8. Assert: due to :ref:`validation `, :math:`S.\SDATA[\X{da}]` exists. +8. Assert: due to :ref:`validation `, :math:`S.\SDATAS[\X{da}]` exists. -9. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATA[\X{da}]`. +9. Let :math:`\X{data}` be the :ref:`data instance ` :math:`S.\SDATAS[\X{da}]`. 10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. @@ -742,74 +736,58 @@ Memory Instructions 15. Pop the value :math:`\I32.\CONST~dst` from the stack. -16. If :math:`cnt = 0`, then: - - a. Return. - -17. If :math:`cnt = 1`, then: - - a. Push the value :math:`\I32.\CONST~dst` to 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: - b. If `src` is larger than the length of :math:`\X{data}.\DIINIT`, then: - - i. Trap. + a. Trap. - c. Let :math:`b` be the byte :math:`\X{data}.\DIINIT[src]`. +17. If :math:`n = 0`, then: - d. Push the value :math:`\I32.\CONST~b` to the stack. + a. Return. - e. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. +18. Let :math:`b` be the byte :math:`\X{data}.\DIDATA[s]`. - f. Return. +19. Push the value :math:`\I32.\CONST~d` to the stack. -18. Push the value :math:`\I32.\CONST~dst` to the stack. +20. Push the value :math:`\I32.\CONST~b` to the stack. -19. Push the value :math:`\I32.\CONST~src` to the stack. +21. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. -20. Push the value :math:`\I32.\CONST~1` to the stack. +22. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -21. Execute the instruction :math:`\MEMORYINIT~x`. +23. Push the value :math:`\I32.\CONST~(d+1)` to the stack. -22. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack. +24. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. -23. Push the value :math:`\vconst_{\I32}(src+1)` to the stack. +25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -24. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack. +26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -25. Execute the instruction :math:`\MEMORYINIT~x`. +27. Execute the instruction :math:`\MEMORYINIT~x`. .. math:: ~\\[-1ex] \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~0)~(\MEMORYINIT~x) &\stepto& S; F; \epsilon - \end{array} - \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~(\MEMORYINIT~x) &\stepto& S; F; - (\I32.\CONST~dst)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ - \end{array} - \\ \qquad + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\MEMORYINIT~x) + \quad\stepto\quad S; F; \TRAP + \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & src < |S.\SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT| \\ - \wedge & b = S.\SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT[src]) \\ + (\iff & s + n > |S.\SDATAS[F.\AMODULE.\MIDATAS[x]].\DIDATA| \\ + \vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\ \end{array} \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt))~(\MEMORYINIT~x) &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~(\MEMORYINIT~x) \\ - (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~(\MEMORYINIT~x) \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff cnt > 1) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x) + \quad\stepto\quad S; F; \epsilon + \\ \qquad + (\otherwise) \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~(\MEMORYINIT~x) &\stepto& S; F; \TRAP - \end{array} - \\ \qquad - (\otherwise) \\ + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\MEMORYINIT~x) + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\MEMORYINIT~x) \\ + \end{array} + \\ \qquad + (\otherwise, \iff b = S.\SDATAS[F.\AMODULE.\MIDATAS[x]].\DIDATA[s]) \\ \end{array} @@ -824,9 +802,9 @@ Memory Instructions 3. Let :math:`a` be the :ref:`data address ` :math:`F.\AMODULE.\MIDATAS[x]`. -4. Assert: due to :ref:`validation `, :math:`S.\SDATA[a]` exists. +4. Assert: due to :ref:`validation `, :math:`S.\SDATAS[a]` exists. -5. Replace :math:`S.\SDATA[a]` with the :ref:`data instance ` :math:`\{\DIINIT~\epsilon\}`. +5. Replace :math:`S.\SDATAS[a]` with the :ref:`data instance ` :math:`\{\DIDATA~\epsilon\}`. .. math:: ~\\[-1ex] @@ -835,7 +813,7 @@ Memory Instructions S; F; (\DATADROP~x) &\stepto& S'; F; \epsilon \end{array} \\ \qquad - (\iff S' = S \with \SDATA[F.\AMODULE.\MIDATAS[x]] = \{ \DIINIT~\epsilon \}) \\ + (\iff S' = S \with \SDATAS[F.\AMODULE.\MIDATAS[x]] = \{ \DIDATA~\epsilon \}) \\ \end{array} @@ -844,101 +822,113 @@ Memory Instructions :math:`\MEMORYCOPY` ................... -1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIMEMS[0]` exists. + +3. Let :math:`\X{ma}` be the :ref:`memory address ` :math:`F.\AMODULE.\MIMEMS[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\SMEMS[\X{ma}]` exists. + +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. -2. Pop the value :math:`\I32.\CONST~cnt` from the stack. +7. Pop the value :math:`\I32.\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. -3. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +9. Pop the value :math:`\I32.\CONST~s` from the stack. -4. Pop the value :math:`\I32.\CONST~src` from the stack. +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -5. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +11. Pop the value :math:`\I32.\CONST~d` from the stack. -6. Pop the value :math:`\I32.\CONST~dst` from the stack. +12. If :math:`s + n` is larger than the length of :math:`\X{mem}.\MIDATA` or :math:`d + n` is larger than the length of :math:`\X{mem}.\MIDATA`, then: + + a. Trap. -7. If :math:`cnt = 0`, then: +13. If :math:`n = 0`, then: a. Return. -8. If :math:`cnt = 1`, then: +14. If :math:`d \leq s`, then: - a. Push the value :math:`\I32.\CONST~dst` to the stack. + a. Push the value :math:`\I32.\CONST~d` to the stack. - b. Push the value :math:`\I32.\CONST~src` to the stack. + b. Push the value :math:`\I32.\CONST~s` to the stack. c. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}`. d. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. - e. Return. + e. Assert: due to the earlier check against the memory size, :math:`d+1 < 2^{32}`. -9. If :math:`dst <= src`, then: + f. Push the value :math:`\I32.\CONST~(d+1)` to the stack. - a. Push the value :math:`\I32.\CONST~dst` to the stack. + g. Assert: due to the earlier check against the memory size, :math:`s+1 < 2^{32}`. - b. Push the value :math:`\I32.\CONST~src` to the stack. + h. Push the value :math:`\I32.\CONST~(s+1)` to the stack. - c. Push the value :math:`\I32.\CONST~1` to the stack. +15. Else: - d. Execute the instruction :math:`\MEMORYCOPY`. + a. Assert: due to the earlier check against the memory size, :math:`d+n-1 < 2^{32}`. - e. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack. + b. Push the value :math:`\I32.\CONST~(d+n-1)` to the stack. - f. Push the value :math:`\vconst_{\I32}(src+1)` to the stack. + c. Assert: due to the earlier check against the memory size, :math:`s+n-1 < 2^{32}`. -10. Else: + d. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - a. Push the value :math:`\vconst_{\I32}(dst+cnt-1)` to the stack. + e. Execute the instruction :math:`\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}`. - b. Push the value :math:`\vconst_{\I32}(src+cnt-1)` to the stack. + f. Execute the instruction :math:`\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}`. - c. Push the value :math:`\I32.\CONST~1` to the stack. + g. Push the value :math:`\I32.\CONST~d` to the stack. - d. Execute the instruction :math:`\MEMORYCOPY`. + h. Push the value :math:`\I32.\CONST~s` to the stack. - e. Push the value :math:`\I32.\CONST~dst` to the stack. +16. Push the value :math:`\I32.\CONST~(n-1)` to the stack. - f. Push the value :math:`\I32.\CONST~src` to the stack. - -11. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack. - -12. Execute the instruction :math:`\MEMORYCOPY`. +17. Execute the instruction :math:`\MEMORYCOPY`. .. math:: ~\\[-1ex] \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~0)~\MEMORYCOPY &\stepto& S; F; \epsilon - \end{array} + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY + \quad\stepto\quad S; F; \TRAP + \\ \qquad + \begin{array}[t]{@{}r@{~}l@{}} + (\iff & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ + \vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|) \\ + \end{array} \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~\MEMORYCOPY &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~dst) \\ - (\I32.\CONST~src)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ - (\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ - \end{array} \\ - \end{array} + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\MEMORYCOPY + \quad\stepto\quad S; F; \epsilon + \\ \qquad + (\otherwise) \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\MEMORYCOPY &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~\MEMORYCOPY \\ - (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff dst \leq src \wedge cnt > 1) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\MEMORYCOPY + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d) \\ + (\I32.\CONST~s)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~\MEMORYCOPY \\ + \end{array} + \\ \qquad + (\otherwise, \iff d \leq s) \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\MEMORYCOPY &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\vconst_{\I32}(dst+cnt-1))~(\vconst_{\I32}(src+cnt-1))~(\I32.\CONST~1)~\MEMORYCOPY \\ - (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt-1))~\MEMORYCOPY \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff dst > src \wedge cnt > 1) \\ + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\MEMORYCOPY + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d+n-1) \\ + (\I32.\CONST~s+n-1)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\ + (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\MEMORYCOPY \\ + \end{array} + \\ \qquad + (\otherwise, \iff d > s) \\ \end{array} @@ -955,97 +945,109 @@ Table Instructions :math:`\TABLECOPY` .................. -1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITABLES[0]` exists. + +3. Let :math:`\X{ta}` be the :ref:`table address ` :math:`F.\AMODULE.\MITABLES[0]`. + +4. Assert: due to :ref:`validation `, :math:`S.\STABLES[\X{ta}]` exists. -2. Pop the value :math:`\I32.\CONST~cnt` from the stack. +5. Let :math:`\X{tab}` be the :ref:`table instance ` :math:`S.\STABLES[\X{ta}]`. -3. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +6. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -4. Pop the value :math:`\I32.\CONST~src` from the stack. +7. Pop the value :math:`\I32.\CONST~n` from the stack. -5. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +8. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -6. Pop the value :math:`\I32.\CONST~dst` from the stack. +9. Pop the value :math:`\I32.\CONST~s` from the stack. -7. If :math:`cnt = 0`, then: +10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. + +11. Pop the value :math:`\I32.\CONST~d` from the stack. + +12. If :math:`s + n` is larger than the length of :math:`\X{tab}.\TIELEM` or :math:`d + n` is larger than the length of :math:`\X{tab}.\TIELEM`, then: + + a. Trap. + +13. If :math:`n = 0`, then: a. Return. -8. If :math:`cnt = 1`, then: +14. If :math:`d \leq s`, then: - a. Push the value :math:`\I32.\CONST~dst` to the stack. + a. Push the value :math:`\I32.\CONST~d` to the stack. - b. Push the value :math:`\I32.\CONST~src` to the stack. + b. Push the value :math:`\I32.\CONST~s` to the stack. c. Execute the instruction :math:`\TABLEGET`. d. Execute the instruction :math:`\TABLESET`. - e. Return. - -9. If :math:`dst <= src`, then: + e. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. - a. Push the value :math:`\I32.\CONST~dst` to the stack. + f. Push the value :math:`\I32.\CONST~(d+1)` to the stack. - b. Push the value :math:`\I32.\CONST~src` to the stack. + g. Assert: due to the earlier check against the table size, :math:`s+1 < 2^{32}`. - c. Push the value :math:`\I32.\CONST~1` to the stack. + h. Push the value :math:`\I32.\CONST~(s+1)` to the stack. - d. Execute the instruction :math:`\TABLECOPY`. +15. Else: - e. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack. + a. Assert: due to the earlier check against the table size, :math:`d+n-1 < 2^{32}`. - f. Push the value :math:`\vconst_{\I32}(src+1)` to the stack. + b. Push the value :math:`\I32.\CONST~(d+n-1)` to the stack. -10. Else: + c. Assert: due to the earlier check against the table size, :math:`s+n-1 < 2^{32}`. - a. Push the value :math:`\vconst_{\I32}(dst+cnt-1)` to the stack. + d. Push the value :math:`\I32.\CONST~(s+n-1)` to the stack. - b. Push the value :math:`\vconst_{\I32}(src+cnt-1)` to the stack. - - c. Push the value :math:`\I32.\CONST~1` to the stack. + c. Execute the instruction :math:`\TABLEGET`. - d. Execute the instruction :math:`\TABLECOPY`. + f. Execute the instruction :math:`\TABLESET`. - e. Push the value :math:`\I32.\CONST~dst` to the stack. + g. Push the value :math:`\I32.\CONST~d` to the stack. - f. Push the value :math:`\I32.\CONST~src` to the stack. + h. Push the value :math:`\I32.\CONST~s` to the stack. -11. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack. +16. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -12. Execute the instruction :math:`\TABLECOPY`. +17. Execute the instruction :math:`\TABLECOPY`. .. math:: ~\\[-1ex] \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~0)~\TABLECOPY &\stepto& S; F; \epsilon - \end{array} + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\TABLECOPY + \quad\stepto\quad S; F; \TRAP + \\ \qquad + \begin{array}[t]{@{}r@{~}l@{}} + (\iff & s + n > |S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM| \\ + \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[0]].\TIELEM|) \\ + \end{array} \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~\TABLECOPY &\stepto& S; F; - (\I32.\CONST~dst)~(\I32.\CONST~src)~\TABLEGET~\TABLESET \\ - \end{array} + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\TABLECOPY + \quad\stepto\quad S; F; \epsilon + \\ \qquad + (\otherwise) \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\TABLECOPY &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~\TABLECOPY \\ - (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~\TABLECOPY \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff dst <= src \wedge cnt > 1) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\TABLECOPY + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d)~(\I32.\CONST~s)~\TABLEGET~\TABLESET \\ + (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~\TABLECOPY \\ + \end{array} + \\ \qquad + (\otherwise, \iff d \leq s) \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~\TABLECOPY &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~(dst+cnt-1))~(\I32.\CONST~(src+cnt-1))~(\I32.\CONST~1)~\TABLECOPY \\ - (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~(cnt-1))~\TABLECOPY \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff dst > src \wedge cnt > 1) \\ + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\TABLECOPY + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~\TABLEGET~\TABLESET \\ + (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~\TABLECOPY \\ + \end{array} + \\ \qquad + (\otherwise, \iff d > s) \\ \end{array} @@ -1068,90 +1070,74 @@ Table Instructions 7. Let :math:`\X{ea}` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[x]`. -8. Assert: due to :ref:`validation `, :math:`S.\SELEM[\X{ea}]` exists. +8. Assert: due to :ref:`validation `, :math:`S.\SELEMS[\X{ea}]` exists. -9. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEM[\X{ea}]`. +9. Let :math:`\X{elem}` be the :ref:`element instance ` :math:`S.\SELEMS[\X{ea}]`. 10. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -11. Pop the value :math:`\I32.\CONST~cnt` from the stack. +11. 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. Pop the value :math:`\I32.\CONST~src` from the stack. +13. 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. Pop the value :math:`\I32.\CONST~dst` from the stack. - -16. If :math:`cnt = 0`, then: - - a. Return. - -17. If :math:`cnt = 1`, then: +15. Pop the value :math:`\I32.\CONST~d` from the stack. - a. Push the value :math:`\I32.\CONST~dst` to 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: - b. If `src` is larger than the length of :math:`\X{elem}.\EIINIT`, then: - - i. Trap. + a. Trap. - c. Let :math:`\funcelem` be the :ref:`function element ` :math:`\X{elem}.\EIINIT[src]`. +17. If :math:`n = 0`, then: - d. Push the value :math:`\funcelem` to the stack. + a. Return. - e. Execute the instruction :math:`\TABLESET`. +18. Let :math:`\funcelem` be the :ref:`function element ` :math:`\X{elem}.\EIELEM[s]`. - f. Return. +19. Push the value :math:`\I32.\CONST~d` to the stack. -18. Push the value :math:`\I32.\CONST~dst` to the stack. +20. Push the value :math:`\funcelem` to the stack. -19. Push the value :math:`\I32.\CONST~src` to the stack. +21. Execute the instruction :math:`\TABLESET`. -20. Push the value :math:`\I32.\CONST~1` to the stack. +22. Assert: due to the earlier check against the table size, :math:`d+1 < 2^{32}`. -21. Execute the instruction :math:`\TABLEINIT~x`. +23. Push the value :math:`\I32.\CONST~(d+1)` to the stack. -22. Push the value :math:`\vconst_{\I32}(dst+1)` to the stack. +24. Assert: due to the earlier check against the segment size, :math:`s+1 < 2^{32}`. -23. Push the value :math:`\vconst_{\I32}(src+1)` to the stack. +25. Push the value :math:`\I32.\CONST~(s+1)` to the stack. -24. Push the value :math:`\I32.\CONST~(cnt-1)` to the stack. +26. Push the value :math:`\I32.\CONST~(n-1)` to the stack. -25. Execute the instruction :math:`\TABLEINIT~x`. +27. Execute the instruction :math:`\TABLEINIT~x`. .. math:: ~\\[-1ex] \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~0)~(\TABLEINIT~x) &\stepto& S; F; \epsilon - \end{array} - \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~(\TABLEINIT~x) &\stepto& S; F; - (\I32.\CONST~dst)~\funcelem~(\TABLESET~x) \\ - \end{array} - \\ \qquad + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLEINIT~x) + \quad\stepto\quad S; F; \TRAP + \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & src < |S.\SELEM[F.\AMODULE.\MIELEMS[x]].\EIINIT| \\ - \wedge & \funcelem = S.\SELEM[F.\AMODULE.\MIELEMS[x]].\EIINIT[src]) \\ + (\iff & s + n > |S.\SELEMS[F.\AMODULE.\MIELEMS[x]].\EIELEM| \\ + \vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\ \end{array} \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~(\TABLEINIT~x) &\stepto& S; F; - \begin{array}[t]{@{}l@{}} - (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~1)~(\TABLEINIT~x) \\ - (\vconst_{\I32}(dst+1))~(\vconst_{\I32}(src+1))~(\I32.\CONST~(cnt-1))~(\TABLEINIT~x) \\ - \end{array} \\ - \end{array} - \\ \qquad - (\iff cnt > 1) + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x) + \quad\stepto\quad S; F; \epsilon + \\ \qquad + (\otherwise) \\[1ex] - \begin{array}{lcl@{\qquad}l} - S; F; (\I32.\CONST~dst)~(\I32.\CONST~src)~(\I32.\CONST~cnt)~(\TABLEINIT~x) &\stepto& S; F; \TRAP - \end{array} - \\ \qquad - (\otherwise) \\ + S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x) + \quad\stepto\quad S; F; + \begin{array}[t]{@{}l@{}} + (\I32.\CONST~d)~\funcelem~(\TABLESET~x) \\ + (\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x) \\ + \end{array} + \\ \qquad + (\otherwise, \iff \funcelem = S.\SELEMS[F.\AMODULE.\MIELEMS[x]].\EIELEM[s]) \\ \end{array} @@ -1166,9 +1152,9 @@ Table Instructions 3. Let :math:`a` be the :ref:`element address ` :math:`F.\AMODULE.\MIELEMS[x]`. -4. Assert: due to :ref:`validation `, :math:`S.\SELEM[a]` exists. +4. Assert: due to :ref:`validation `, :math:`S.\SELEMS[a]` exists. -5. Replace :math:`S.\SELEM[a]` with the :ref:`element instance ` :math:`\{\EIINIT~\epsilon\}`. +5. Replace :math:`S.\SELEMS[a]` with the :ref:`element instance ` :math:`\{\EIELEM~\epsilon\}`. .. math:: ~\\[-1ex] @@ -1177,7 +1163,7 @@ Table Instructions S; F; (\ELEMDROP~x) &\stepto& S'; F; \epsilon \end{array} \\ \qquad - (\iff S' = S \with \SELEM[F.\AMODULE.\MIELEMS[x]] = \{ \EIINIT~\epsilon \}) \\ + (\iff S' = S \with \SELEMS[F.\AMODULE.\MIELEMS[x]] = \{ \EIELEM~\epsilon \}) \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 005d6822..b0b51849 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -381,9 +381,9 @@ New instances of :ref:`functions `, :ref:`tables ` in :math:`S`. -3. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIINIT~\funcelem^\ast \}`. +3. Let :math:`\eleminst` be the :ref:`element instance ` :math:`\{ \EIELEM~\funcelem^\ast \}`. -4. Append :math:`\eleminst` to the |SELEM| of :math:`S`. +4. Append :math:`\eleminst` to the |SELEMS| of :math:`S`. 5. Return :math:`a`. @@ -391,9 +391,9 @@ New instances of :ref:`functions `, :ref:`tables `, :ref:`tables ` in :math:`S`. -3. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \DIINIT~\bytes \}`. +3. Let :math:`\datainst` be the :ref:`data instance ` :math:`\{ \DIDATA~\bytes \}`. -4. Append :math:`\datainst` to the |SDATA| of :math:`S`. +4. Append :math:`\datainst` to the |SDATAS| of :math:`S`. 5. Return :math:`a`. @@ -417,9 +417,9 @@ New instances of :ref:`functions `, :ref:`tables `. - -.. math:: - \begin{array}{lcl@{\qquad}l} - \vconst_t(x) &=& (t\K{.}\CONST~x) - & (\iff x~\mbox{is well-formed for}~t) \\ - \vconst_t(x) &=& \TRAP - & (\otherwise) \\ - \end{array} - .. index:: ! result, value, trap pair: abstract syntax; result @@ -87,8 +74,8 @@ Syntactically, the store is defined as a :ref:`record ` listing \STABLES & \tableinst^\ast, \\ \SMEMS & \meminst^\ast, \\ \SGLOBALS & \globalinst^\ast, \\ - \SELEM & \eleminst^\ast, \\ - \SDATA & \datainst^\ast ~\} \\ + \SELEMS & \eleminst^\ast, \\ + \SDATAS & \datainst^\ast ~\} \\ \end{array} \end{array} @@ -318,7 +305,7 @@ It holds a vector of function elements. .. math:: \begin{array}{llll} \production{(element instance)} & \eleminst &::=& - \{ \EIINIT~\vec(\funcelem) \} \\ + \{ \EIELEM~\vec(\funcelem) \} \\ \end{array} @@ -336,7 +323,7 @@ It holds a vector of :ref:`bytes `. .. math:: \begin{array}{llll} \production{(data instance)} & \datainst &::=& - \{ \DIINIT~\vec(\byte) \} \\ + \{ \DIDATA~\vec(\byte) \} \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index d16319b7..86acdc98 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -854,9 +854,9 @@ .. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}} .. |GIMUT| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{mut}} -.. |EIINIT| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{init}} +.. |EIELEM| mathdef:: \xref{exec/runtime}{syntax-eleminst}{\K{elem}} -.. |DIINIT| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{init}} +.. |DIDATA| mathdef:: \xref{exec/runtime}{syntax-datainst}{\K{data}} .. |EINAME| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{name}} .. |EIVALUE| mathdef:: \xref{exec/runtime}{syntax-exportinst}{\K{value}} @@ -899,7 +899,6 @@ .. |evtables| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{tables}} .. |evmems| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{mems}} .. |evglobals| mathdef:: \xref{exec/runtime}{syntax-externval}{\F{globals}} -.. |vconst| mathdef:: \xref{exec/runtime}{syntax-val}{\F{const}} .. Store, terminals @@ -908,8 +907,8 @@ .. |STABLES| mathdef:: \xref{exec/runtime}{syntax-store}{\K{tables}} .. |SMEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{mems}} .. |SGLOBALS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{globals}} -.. |SELEM| mathdef:: \xref{exec/runtime}{syntax-store}{\K{elem}} -.. |SDATA| mathdef:: \xref{exec/runtime}{syntax-store}{\K{data}} +.. |SELEMS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{elems}} +.. |SDATAS| mathdef:: \xref{exec/runtime}{syntax-store}{\K{datas}} .. Store, non-terminals @@ -1067,6 +1066,8 @@ .. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash} .. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash} .. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash} +.. |vdasheleminst| mathdef:: \xref{appendix/properties}{valid-eleminst}{\vdash} +.. |vdashdatainst| mathdef:: \xref{appendix/properties}{valid-datainst}{\vdash} .. |vdashexportinst| mathdef:: \xref{appendix/properties}{valid-exportinst}{\vdash} .. |vdashmoduleinst| mathdef:: \xref{appendix/properties}{valid-moduleinst}{\vdash} @@ -1079,6 +1080,8 @@ .. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash} .. |vdashmeminstextends| mathdef:: \xref{appendix/properties}{extend-meminst}{\vdash} .. |vdashglobalinstextends| mathdef:: \xref{appendix/properties}{extend-globalinst}{\vdash} +.. |vdasheleminstextends| mathdef:: \xref{appendix/properties}{extend-eleminst}{\vdash} +.. |vdashdatainstextends| mathdef:: \xref{appendix/properties}{extend-datainst}{\vdash} .. |vdashstoreextends| mathdef:: \xref{appendix/properties}{extend-store}{\vdash}