diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 9ffe84591..ec347147f 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -462,7 +462,7 @@ Reference Instructions S; F; \val^n~(\STRUCTNEW~x) &\stepto& S'; F; (\REFSTRUCTADDR~|S.\SSTRUCTS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & \X{si} = \{\SITYPE~F.\AMODULE.\MITYPES[x], \SIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\ \land & S' = S \with \SSTRUCTS = S.\SSTRUCTS~\X{si}) \end{array} \\ @@ -501,7 +501,7 @@ Reference Instructions F; (\STRUCTNEWDEFAULT~x) &\stepto& (\default_{\unpacktype(\X{ft})}))^n~(\STRUCTNEW~x) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n) + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n) \end{array} \\ \end{array} @@ -511,7 +511,7 @@ Reference Instructions S; F; (\STRUCTNEWDEFAULT~x) &\stepto& S'; F; (\REFSTRUCTADDR~|S.\SSTRUCTS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & \X{si} = \{\SITYPE~F.\AMODULE.\MITYPES[x], \SIFIELDS~(\packval_{\X{ft}}(\default_{\unpacktype(\X{ft})}))^n\} \\ \land & S' = S \with \SSTRUCTS = S.\SSTRUCTS~\X{si}) \end{array} \\ @@ -561,7 +561,7 @@ Reference Instructions S; F; (\REFSTRUCTADDR~a)~(\STRUCTGET\K{\_}\sx^?~x~i) &\stepto& \val & \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^\ast \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & \val = \unpackval^{\sx^?}_{\X{ft}^\ast[i]}(S.\SSTRUCTS[a].\SIFIELDS[i])) \end{array} \\ S; F; (\REFNULL~t)~(\STRUCTGET\K{\_}\sx^?~x~i) &\stepto& \TRAP @@ -612,7 +612,7 @@ Reference Instructions S; F; (\REFSTRUCTADDR~a)~\val~(\STRUCTSET~x~i) &\stepto& S'; \epsilon & \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^\ast \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & S' = S \with \SSTRUCTS[a].\SIFIELDS[i] = \packval_{\X{ft}^\ast[i]}(\val)) \end{array} \\ S; F; (\REFNULL~t)~\val~(\STRUCTSET~x~i) &\stepto& \TRAP @@ -657,7 +657,7 @@ Reference Instructions S; F; \val~(\I32.\CONST~n)~(\ARRAYNEW~x) &\stepto& S'; F; (\REFARRAYADDR~|S.\SARRAYS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\ \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai}) \end{array} \\ @@ -696,7 +696,7 @@ Reference Instructions F; (\I32.\CONST~n)~(\ARRAYNEWDEFAULT~x) &\stepto& (\default_{\unpacktype(\X{ft}}))^n~(\ARRAYNEWFIXED~x~n) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES.\MITYPES[x] = \TARRAY~\X{ft}) + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}) \end{array} \\ \end{array} @@ -706,7 +706,7 @@ Reference Instructions S; F; (\I32.\CONST~n)~(\ARRAYNEWDEFAULT~x) &\stepto& S'; F; (\REFARRAYADDR~|S.\SARRAYS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\default_{\unpacktype(\X{ft}}))^n\} \\ \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai}) \end{array} \\ @@ -751,7 +751,7 @@ Reference Instructions S; F; \val^n~(\ARRAYNEWFIXED~x~n) &\stepto& S'; F; (\REFARRAYADDR~|S.\SARRAYS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ \land & \X{ai} = \{\AITYPE~F.\AMODULE.\MITYPES[x], \AIFIELDS~(\packval_{\X{ft}}(\val))^n\} \\ \land & S' = S \with \SARRAYS = S.\SARRAYS~\X{ai}) \end{array} \\ @@ -814,14 +814,14 @@ Reference Instructions S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& \TRAP \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft}^n \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ \land & s + n\cdot|\X{ft}| > |S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA|) \end{array} \\ \\[1ex] S; F; (\I32.\CONST~s)~(\I32.\CONST~n)~(\ARRAYNEWDATA~x~y) &\stepto& (t.\CONST~c)^n~(\ARRAYNEWFIXED~x~n) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft}^n \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ \land & t = \unpacktype(\X{ft}) \\ \land & (\bytes_{\X{ft}}(c))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|] \\ \end{array} \\ @@ -931,7 +931,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \val & \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TARRAY~\X{ft} \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ \land & \val = \unpackval^{\sx^?}_{\X{ft}}(S.\SARRAYS[a].\AIFIELDS[i])) \end{array} \\ S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~(\ARRAYGET\K{\_}\sx^?~x) &\stepto& \val @@ -990,7 +990,7 @@ Reference Instructions S; F; (\REFARRAYADDR~a)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& S'; \epsilon & \begin{array}[t]{@{}r@{~}l@{}} - (\iff & F.\AMODULE.\MITYPES[x] = \TSTRUCT~\X{ft}^n \\ + (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ \land & S' = S \with \SARRAYS[a].\AIFIELDS[i] = \packval_{\X{ft}}(\val)) \end{array} \\ S; F; (\REFNULL~t)~(\I32.\CONST~i)~\val~(\ARRAYSET~x) &\stepto& \TRAP @@ -3589,9 +3589,9 @@ Control Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`\expand_{S;F}(\blocktype)` is defined. +2. Assert: due to :ref:`validation `, :math:`\fblocktype_{S;F}(\blocktype)` is defined. -3. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`instruction type ` :math:`\expand_{S;F}(\blocktype)`. +3. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`instruction type ` :math:`\fblocktype_{S;F}(\blocktype)`. 4. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the block. @@ -3606,7 +3606,7 @@ Control Instructions \begin{array}{lcl} S; F; \val^m~\BLOCK~\X{bt}~\instr^\ast~\END &\stepto& S; F; \LABEL_n\{\epsilon\}~\val^m~\instr^\ast~\END - \\&&\quad (\iff \expand_{S;F}(\X{bt}) = [t_1^m] \to [t_2^n]) + \\&&\quad (\iff \fblocktype_{S;F}(\X{bt}) = [t_1^m] \to [t_2^n]) \end{array} @@ -3617,9 +3617,9 @@ Control Instructions 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. Assert: due to :ref:`validation `, :math:`\expand_{S;F}(\blocktype)` is defined. +2. Assert: due to :ref:`validation `, :math:`\fblocktype_{S;F}(\blocktype)` is defined. -3. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`instruction type ` :math:`\expand_{S;F}(\blocktype)`. +3. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`instruction type ` :math:`\fblocktype_{S;F}(\blocktype)`. 4. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the start of the loop. @@ -3634,7 +3634,7 @@ Control Instructions \begin{array}{lcl} S; F; \val^m~\LOOP~\X{bt}~\instr^\ast~\END &\stepto& S; F; \LABEL_m\{\LOOP~\X{bt}~\instr^\ast~\END\}~\val^m~\instr^\ast~\END - \\&&\quad (\iff \expand_{S;F}(\X{bt}) = [t_1^m] \to [t_2^n]) + \\&&\quad (\iff \fblocktype_{S;F}(\X{bt}) = [t_1^m] \to [t_2^n]) \end{array} @@ -3978,9 +3978,9 @@ Control 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.\MITYPES[y]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITYPES[y]` is defined. -7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type ` :math:`F.\AMODULE.\MITYPES[y]`. +7. Let :math:`\X{dt}_{\F{expect}}` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[y]`. 8. Assert: due to :ref:`validation `, a value with :ref:`value type ` |I32| is on the top of the stack. @@ -4004,9 +4004,9 @@ Control Instructions 16. Let :math:`\X{f}` be the :ref:`function instance ` :math:`S.\SFUNCS[a]`. -17. Let :math:`\X{ft}_{\F{actual}}` be the :ref:`function type ` :math:`\X{f}.\FITYPE`. +17. Let :math:`\X{dt}_{\F{actual}}` be the :ref:`defined type ` :math:`\X{f}.\FITYPE`. -18. If :math:`\X{ft}_{\F{actual}}` and :math:`\X{ft}_{\F{expect}}` differ, then: +18. If :math:`\X{dt}_{\F{actual}}` does not :ref:`match ` :math:`\X{dt}_{\F{expect}}`, then: a. Trap. @@ -4022,7 +4022,7 @@ Control Instructions \begin{array}[t]{@{}r@{~}l@{}} (\iff & S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM[i] = \REFFUNCADDR~a \\ \wedge & S.\SFUNCS[a] = f \\ - \wedge & S \vdashfunctypematch F.\AMODULE.\MITYPES[y] \matchesfunctype f.\FITYPE) + \wedge & S \vdashdeftypematch F.\AMODULE.\MITYPES[y] \matchesdeftype f.\FITYPE) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -4099,9 +4099,9 @@ Control 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.\MITYPES[x]` exists. +6. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITYPES[x]` is defined. -7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type ` :math:`F.\AMODULE.\MITYPES[x]`. +7. Let :math:`\X{dt}_{\F{expect}}` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. 8. Assert: due to :ref:`validation `, a value with :ref:`value type ` |I32| is on the top of the stack. @@ -4121,9 +4121,9 @@ Control Instructions 14. Let :math:`\X{f}` be the :ref:`function instance ` :math:`S.\SFUNCS[a]`. -15. Let :math:`\X{ft}_{\F{actual}}` be the :ref:`function type ` :math:`\X{f}.\FITYPE`. +15. Let :math:`\X{dt}_{\F{actual}}` be the :ref:`defined type ` :math:`\X{f}.\FITYPE`. -16. If :math:`\X{ft}_{\F{actual}}` and :math:`\X{ft}_{\F{expect}}` differ, then: +16. If :math:`\X{dt}_{\F{actual}}` does not :ref:`match ` :math:`\X{dt}_{\F{expect}}`, then: a. Trap. @@ -4210,7 +4210,7 @@ Invocation of :ref:`function address ` :math:`a` 2. Let :math:`f` be the :ref:`function instance `, :math:`S.\SFUNCS[a]`. -3. Let :math:`[t_1^n] \toF [t_2^m]` be the :ref:`function type ` :math:`\X{f}.\FITYPE`. +3. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`structured type ` :math:`\expand(\X{f}.\FITYPE)`. 4. Let :math:`\local^\ast` be the list of :ref:`locals ` :math:`f.\FICODE.\FLOCALS`. @@ -4237,7 +4237,7 @@ Invocation of :ref:`function address ` :math:`a` \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & S.\SFUNCS[a] = f \\ - \wedge & S.f.\FITYPE = [t_1^n] \toF [t_2^m] \\ + \wedge & \expand(S.f.\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m] \\ \wedge & f.\FICODE = \{ \FTYPE~x, \FLOCALS~\{\LTYPE~t\}^k, \FBODY~\instr^\ast~\END \} \\ \wedge & F = \{ \AMODULE~f.\FIMODULE, ~\ALOCALS~\val^n~(\default_t)^k \}) \end{array} \\ @@ -4254,7 +4254,7 @@ Tail-invocation of :ref:`function address ` :math:`a` 1. Assert: due to :ref:`validation `, :math:`S.\SFUNCS[a]` exists. -2. Let :math:`[t_1^n] \toF [t_2^m]` be the :ref:`function type ` :math:`S.\SFUNCS[a].\FITYPE`. +2. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`structured type ` :math:`\expand(S.\SFUNCS[a].\FITYPE)`. 3. Assert: due to :ref:`validation `, there are at least :math:`n` values on the top of the stack. @@ -4279,7 +4279,7 @@ Tail-invocation of :ref:`function address ` :math:`a` \begin{array}{lcl@{\qquad}l} S; \FRAME_m\{F\}~B^\ast[\val^n~(\RETURNINVOKE~a)]~\END &\stepto& \val^n~(\INVOKE~a) - & (\iff S.\SFUNCS[a].\FITYPE = [t_1^n] \toF [t_2^m]) + & (\iff \expand(S.\SFUNCS[a].\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m]) \end{array} @@ -4336,7 +4336,8 @@ Furthermore, the resulting store must be :ref:`valid `, i.e., all d \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \toF [t_2^m], \FIHOSTCODE~\X{hf} \} \\ + (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTCODE~\X{hf} \} \\ + \wedge & \expand(\deftype) = \TFUNC~[t_1^n] \toF [t_2^m] \\ \wedge & (S'; \result) \in \X{hf}(S; \val^n)) \\ \end{array} \\ \begin{array}{lcl@{\qquad}l} @@ -4344,7 +4345,8 @@ Furthermore, the resulting store must be :ref:`valid `, i.e., all d \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \toF [t_2^m], \FIHOSTCODE~\X{hf} \} \\ + (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTCODE~\X{hf} \} \\ + \wedge & \expand(\deftype) = \TFUNC~[t_1^n] \toF [t_2^m] \\ \wedge & \bot \in \X{hf}(S; \val^n)) \\ \end{array} \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 6b20540e1..f0bb58ee1 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -21,11 +21,11 @@ New instances of :ref:`functions `, :ref:`tables ` to allocate and :math:`\moduleinst` its :ref:`module instance `. -2. Let :math:`\functype` be the :ref:`function type ` :math:`\moduleinst.\MITYPES[\func.\FTYPE]`. +2. Let :math:`\deftype` be the :ref:`defined type ` :math:`\moduleinst.\MITYPES[\func.\FTYPE]`. 3. Let :math:`a` be the first free :ref:`function address ` in :math:`S`. -4. Let :math:`\funcinst` be the :ref:`function instance ` :math:`\{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \}`. +4. Let :math:`\funcinst` be the :ref:`function instance ` :math:`\{ \FITYPE~\deftype, \FIMODULE~\moduleinst, \FICODE~\func \}`. 6. Append :math:`\funcinst` to the |SFUNCS| of :math:`S`. @@ -36,9 +36,9 @@ New instances of :ref:`functions `, :ref:`tables `, :ref:`tables ` ....................................... -1. Let :math:`\hostfunc` be the :ref:`host function ` to allocate and :math:`\functype` its :ref:`function type `. +1. Let :math:`\hostfunc` be the :ref:`host function ` to allocate and :math:`\deftype` its :ref:`defined type `. 2. Let :math:`a` be the first free :ref:`function address ` in :math:`S`. -3. Let :math:`\funcinst` be the :ref:`function instance ` :math:`\{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \}`. +3. Let :math:`\funcinst` be the :ref:`function instance ` :math:`\{ \FITYPE~\deftype, \FIHOSTCODE~\hostfunc \}`. 4. Append :math:`\funcinst` to the |SFUNCS| of :math:`S`. @@ -62,10 +62,10 @@ New instances of :ref:`functions `, :ref:`tables ` vectors for the module's :ref:`element where: +.. todo:: adjust deftypes + .. math:: \begin{array}{@{}rlll@{}} \table^\ast &=& \module.\MTABLES \\ @@ -663,7 +665,7 @@ The following steps are performed: 2. Let :math:`\funcinst` be the :ref:`function instance ` :math:`S.\SFUNCS[\funcaddr]`. -3. Let :math:`[t_1^n] \toF [t_2^m]` be the :ref:`function type ` :math:`\funcinst.\FITYPE`. +3. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`structured type ` :math:`\expand(\funcinst.\FITYPE)`. 4. If the length :math:`|\val^\ast|` of the provided argument values is different from the number :math:`n` of expected arguments, then: @@ -695,7 +697,7 @@ The values :math:`\val_{\F{res}}^m` are returned as the results of the invocatio ~\\[-1ex] \begin{array}{@{}lcl} \invoke(S, \funcaddr, \val^n) &=& S; F; \val^n~(\INVOKE~\funcaddr) \\ - &(\iff & S.\SFUNCS[\funcaddr].\FITYPE = [t_1^n] \toF [t_2^m] \\ + &(\iff & \expand(S.\SFUNCS[\funcaddr].\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m] \\ &\wedge& (S \vdashval \val : t_1)^n \\ &\wedge& F = \{ \AMODULE~\{\}, \ALOCALS~\epsilon \}) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index b3789f3d4..16cddfb5a 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -286,8 +286,8 @@ The module instance is used to resolve references to other definitions during ex .. math:: \begin{array}{llll} \production{function instance} & \funcinst &::=& - \{ \FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func \} \\ &&|& - \{ \FITYPE~\functype, \FIHOSTCODE~\hostfunc \} \\ + \{ \FITYPE~\deftype, \FIMODULE~\moduleinst, \FICODE~\func \} \\ &&|& + \{ \FITYPE~\deftype, \FIHOSTCODE~\hostfunc \} \\ \production{host function} & \hostfunc &::=& \dots \\ \end{array} @@ -462,7 +462,7 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]` -.. index:: ! structure instance, ! array instance, structure type, array type, ! field value, ! packed value +.. index:: ! structure instance, ! array instance, structure type, array type, defined type, ! field value, ! packed value pair: abstract syntax; field value pair: abstract syntax; packed value pair: abstract syntax; structure instance @@ -473,20 +473,21 @@ It filters out entries of a specific kind in an order-preserving fashion: .. _syntax-packedval: .. _syntax-structinst: .. _syntax-arrayinst: +.. _syntax-aggrinst: -Structure and Array Instances -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Aggregate Instances +~~~~~~~~~~~~~~~~~~~ A *structure instance* is the runtime representation of a heap object allocated from a :ref:`structure type `. Likewise, an *array instance* is the runtime representation of a heap object allocated from an :ref:`array type `. -Both record their respective type and hold a vector of the values of their *fields*. +Both record their respective :ref:`defined type ` and hold a vector of the values of their *fields*. .. math:: \begin{array}{llcl} \production{structure instance} & \structinst &::=& - \{ \SITYPE~\structtype, \SIFIELDS~\vec(\fieldval) \} \\ + \{ \SITYPE~\deftype, \SIFIELDS~\vec(\fieldval) \} \\ \production{array instance} & \arrayinst &::=& - \{ \AITYPE~\arraytype, \AIFIELDS~\vec(\fieldval) \} \\ + \{ \AITYPE~\deftype, \AIFIELDS~\vec(\fieldval) \} \\ \production{field value} & \fieldval &::=& \val ~|~ \packedval \\ \production{packed value} & \packedval &::=& @@ -595,7 +596,7 @@ Locals may be uninitialized, in which case they are empty. Locals are mutated by respective :ref:`variable instructions `. -.. _exec-expand: +.. _aux-fblocktype: Conventions ........... @@ -607,9 +608,9 @@ Conventions * The following auxiliary definition takes a :ref:`block type ` and looks up the :ref:`instruction type ` that it denotes in the current frame: .. math:: - \begin{array}{lll} - \expand_{S;F}(\typeidx) &=& F.\AMODULE.\MITYPES[\typeidx] \\ - \expand_{S;F}([\valtype^?]) &=& [] \to [\valtype^?] \\ + \begin{array}{llll} + \fblocktype_{S;F}(\typeidx) &=& \functype & (\iff \expand(F.\AMODULE.\MITYPES[\typeidx]) = \TFUNC~\functype) \\ + \fblocktype_{S;F}([\valtype^?]) &=& [] \to [\valtype^?] \\ \end{array} diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst index c21f2c44d..27543c71c 100644 --- a/document/core/exec/values.rst +++ b/document/core/exec/values.rst @@ -89,15 +89,19 @@ The following auxiliary typing rules specify this typing relation relative to a * Let :math:`\structinst` be the :ref:`structure instance ` :math:`S.\SSTRUCTS[a]`. -* Let :math:`\structtype` be the :ref:`structure type ` :math:`\structinst.\SITYPE`. +* Let :math:`\deftype` be the :ref:`defined type ` :math:`\structinst.\SITYPE`. -* Then the value is valid with :ref:`reference type ` :math:`(\REF~\structtype)`. +* The :ref:`expansion ` of :math:`\deftype` must be a :ref:`struct type `. + +* Then the value is valid with :ref:`reference type ` :math:`(\REF~\deftype)`. .. math:: \frac{ - \structtype = S.\SSTRUCTS[a].\SITYPE + \deftype = S.\SSTRUCTS[a].\SITYPE + \qquad + \expand(\deftype) = \TSTRUCT~\structtype }{ - S \vdashval \REFSTRUCTADDR~a : \REF~\structtype + S \vdashval \REFSTRUCTADDR~a : \REF~\deftype } @@ -110,15 +114,19 @@ The following auxiliary typing rules specify this typing relation relative to a * Let :math:`\arrayinst` be the :ref:`array instance ` :math:`S.\SARRAYS[a]`. -* Let :math:`\arraytype` be the :ref:`array type ` :math:`\arrayinst.\AITYPE`. +* Let :math:`\deftype` be the :ref:`defined type ` :math:`\arrayinst.\AITYPE`. + +* The :ref:`expansion ` of :math:`\deftype` must be an :ref:`array type `. * Then the value is valid with :ref:`reference type ` :math:`(\REF~\arraytype)`. .. math:: \frac{ - \arraytype = S.\SARRAYS[a].\AITYPE + \deftype = S.\SARRAYS[a].\AITYPE + \qquad + \expand(\deftype) = \TARRAY~\arraytype }{ - S \vdashval \REFARRAYADDR~a : \REF~\arraytype + S \vdashval \REFARRAYADDR~a : \REF~\deftype } @@ -129,15 +137,19 @@ The following auxiliary typing rules specify this typing relation relative to a * Let :math:`\funcinst` be the :ref:`function instance ` :math:`S.\SFUNCS[a]`. -* Let :math:`\functype` be the :ref:`function type ` :math:`\funcinst.\FITYPE`. +* Let :math:`\deftype` be the :ref:`defined type ` :math:`\funcinst.\FITYPE`. + +* The :ref:`expansion ` of :math:`\deftype` must be a :ref:`function type `. * Then the value is valid with :ref:`reference type ` :math:`(\REF~\functype)`. .. math:: \frac{ - \functype = S.\SFUNCS[a].\FITYPE + \deftype = S.\SFUNCS[a].\FITYPE + \qquad + \expand(\deftype) = \TFUNC~\functype }{ - S \vdashval \REFFUNCADDR~a : \REF~\functype + S \vdashval \REFFUNCADDR~a : \REF~\deftype } diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index 0a7e731a3..d8b0f5ae9 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -14,7 +14,7 @@ and provide initialization in the form of :ref:`data ` and :ref:`el .. math:: \begin{array}{llrll} \production{module} & \module &::=& \{ & - \MTYPES~\vec(\functype), \\&&&& + \MTYPES~\vec(\rectype), \\&&&& \MFUNCS~\vec(\func), \\&&&& \MTABLES~\vec(\table), \\&&&& \MMEMS~\vec(\mem), \\&&&& @@ -112,20 +112,15 @@ Conventions For example, if :math:`\instr^\ast` is :math:`(\DATADROP~x) (\MEMORYINIT~y)`, then :math:`\freedataidx(\instr^\ast) = \{x, y\}`, or equivalently, the vector :math:`x~y`. -.. index:: ! type definition, type index, function type +.. index:: ! type definition, type index, function type, aggregate type pair: abstract syntax; type definition .. _syntax-typedef: Types ~~~~~ -The |MTYPES| component of a module defines a vector of :ref:`function types `. - -All function types used in a module must be defined in this component. -They are referenced by :ref:`type indices `. - -.. note:: - Future versions of WebAssembly may add additional forms of type definitions. +The |MTYPES| component of a module defines a vector of :ref:`recursive types `, each of consisting of a list of :ref:`sub types ` referenced by individual :ref:`type indices `. +All :ref:`function ` or :ref:`aggregate ` types used in a module must be defined in this component. .. index:: ! function, ! local, function index, local index, type index, value type, expression, import diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 84de5c5e3..a32644612 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -187,6 +187,24 @@ Other references are *non-null*. Reference types are *opaque*, meaning that neither their size nor their bit pattern can be observed. Values of reference type can be stored in :ref:`tables `. +.. _aux-reftypediff: + +Convention +.......... + +* The *difference* :math:`\X{rt}_1\reftypediff\X{rt}_2` between two reference types is defined as follows: + + .. math:: + \begin{array}{lll} + (\REF~\NULL_1^?~\X{ht}_1) \reftypediff (\REF~\NULL~\X{ht}_2) &=& (\REF~\X{ht}_1) \\ + (\REF~\NULL_1^?~\X{ht}_1) \reftypediff (\REF~\X{ht}_2) &=& (\REF~\NULL_1^?~\X{ht}_1) \\ + \end{array} + +.. note:: + This definition computes an approximation of the reference type that is inhabited by all values from :math:`\X{rt}_1` except those from :math:`\X{rt}_2`. + Since the type system does not have general union types, + the definition only affects the presence of null and cannot express the absence of other values. + .. index:: ! value type, number type, vector type, reference type, ! bottom type pair: abstract syntax; value type @@ -302,25 +320,121 @@ They are also used to classify the inputs and outputs of :ref:`instructions ` and :ref:`aggregate types `. + +.. math:: + \begin{array}{llrl} + \production{structured type} & \strtype &::=& + \TFUNC~\functype ~|~ \TSTRUCT~\structtype ~|~ \TARRAY~\arraytype \\ + \end{array} + + +.. index:: ! recursive type, ! sub type, structured type, ! final, subtyping + pair: abstract syntax; recursive type + pair: abstract syntax; sub type +.. _syntax-rectype: +.. _syntax-subtype: + +Recursive Types +~~~~~~~~~~~~~~~ + +*Recursive types* denote a group of mutually recursive :ref:`structured types `, each of which can optionally declare a list of supertypes that it :ref:`matches `. +Each type can also be declared *final*, preventing further subtyping. +. +In a :ref:`module `, each member of a recursive type is assigned a separate :ref:`type index `. + +.. math:: + \begin{array}{llrl} + \production{recursive type} & \rectype &::=& + \TREC~\subtype^\ast \\ + \production{sub types} & \subtype &::=& + \TSUB~\TFINAL^?~\heaptype^\ast~\strtype \\ + \end{array} + + +.. index:: ! defined type, recursive type, ! unroll, ! expand pair: abstract syntax; defined type .. _syntax-deftype: Defined Types ~~~~~~~~~~~~~ -.. todo:: structured types, recrusive types, etc. +*Defined types* denote the individual types defined in a :ref:`module `. +Each such type is represented as a projection from the :ref:`recursive type ` group it originates from, indexed by its position in that group. -*Defined types* are the ones that can be defined in a :ref:`module `, assigning them a :ref:`type index `. .. math:: \begin{array}{llrl} \production{defined type} & \deftype &::=& - \functype \\ + \rectype.i \\ \end{array} -.. note:: - Future versions of WebAssembly may introduce additional forms of defined types. +Defined types do not occur in the :ref:`binary ` or :ref:`text ` format, +but are formed during :ref:`validation ` and :ref:`execution ` from the recursive types defined in each module. + +.. _aux-expand: +.. _aux-unroll: + +Conventions +........... + +* The following auxiliary function denotes the *unrolling* of a defined type: + + .. math:: + \begin{array}{lll} + \unroll((\subtype^\ast).i) &=& \subtype^\ast[i] \\ + \end{array} + +* The following auxiliary function denotes the *expansion* of a defined type: + + .. math:: + \begin{array}{llll} + \expand(\deftype) &=& \strtype & (\iff \unroll(\deftype) = \TSUB~\TFINAL^?~\X{ht}^?~\strtype) \\ + \end{array} .. index:: ! limits, memory type, table type @@ -384,9 +498,6 @@ Table Types Like memories, tables are constrained by limits for their minimum and optionally maximum size. The limits are given in numbers of entries. -.. note:: - In future versions of WebAssembly, additional element types may be introduced. - .. index:: ! global type, ! mutability, value type, global, mutability pair: abstract syntax; global type @@ -411,7 +522,7 @@ Global Types \end{array} -.. index:: ! external type, function type, table type, memory type, global type, import, external value +.. index:: ! external type, defined type, function type, table type, memory type, global type, import, external value pair: abstract syntax; external type pair: external; type .. _syntax-externtype: @@ -424,7 +535,7 @@ External Types .. math:: \begin{array}{llrl} \production{external types} & \externtype &::=& - \ETFUNC~\functype ~|~ + \ETFUNC~\deftype ~|~ \ETTABLE~\tabletype ~|~ \ETMEM~\memtype ~|~ \ETGLOBAL~\globaltype \\ diff --git a/document/core/util/macros.def b/document/core/util/macros.def index c854c7773..06e7b2638 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -228,7 +228,7 @@ .. |TARRAY| mathdef:: \xref{syntax/types}{syntax-strtype}{\K{array}} .. |TSUB| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{sub}} .. |TREC| mathdef:: \xref{syntax/types}{syntax-rectype}{\K{rec}} -.. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{filan}} +.. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{final}} .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} @@ -257,6 +257,7 @@ .. |structtype| mathdef:: \xref{syntax/types}{syntax-structtype}{\X{structtype}} .. |arraytype| mathdef:: \xref{syntax/types}{syntax-arraytype}{\X{arraytype}} .. |fieldtype| mathdef:: \xref{syntax/types}{syntax-fieldtype}{\X{fieldtype}} +.. |storagetype| mathdef:: \xref{syntax/types}{syntax-storagetype}{\X{storagetype}} .. |packedtype| mathdef:: \xref{syntax/types}{syntax-packedtype}{\X{packedtype}} .. |strtype| mathdef:: \xref{syntax/types}{syntax-strtype}{\X{strtype}} .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}} @@ -278,6 +279,11 @@ .. Types, meta functions +.. |reftypediff| mathdef:: \xref{syntax/types}{aux-reftypediff}{\setminus} + +.. |unroll| mathdef:: \xref{syntax/types}{aux-unroll}{\F{unroll}} +.. |expand| mathdef:: \xref{syntax/types}{aux-expand}{\F{expand}} + .. |packtype| mathdef:: \xref{syntax/types}{aux-packtype}{\F{pack}} .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}} @@ -999,6 +1005,10 @@ .. |matchesresulttype| mathdef:: \xref{valid/matching}{match-resulttype}{\leq} .. |matchesinstrtype| mathdef:: \xref{valid/matching}{match-instrtype}{\leq} .. |matchesfunctype| mathdef:: \xref{valid/matching}{match-functype}{\leq} +.. |matchesstructtype| mathdef:: \xref{valid/matching}{match-structtype}{\leq} +.. |matchesarraytype| mathdef:: \xref{valid/matching}{match-arraytype}{\leq} +.. |matchesstrtype| mathdef:: \xref{valid/matching}{match-strtype}{\leq} +.. |matchesdeftype| mathdef:: \xref{valid/matching}{match-deftype}{\leq} .. |matchestabletype| mathdef:: \xref{valid/matching}{match-tabletype}{\leq} .. |matchesmemtype| mathdef:: \xref{valid/matching}{match-memtype}{\leq} .. |matchesglobaltype| mathdef:: \xref{valid/matching}{match-globaltype}{\leq} @@ -1050,6 +1060,10 @@ .. |vdashresulttypematch| mathdef:: \xref{valid/matching}{match-resulttype}{\vdash} .. |vdashinstrtypematch| mathdef:: \xref{valid/matching}{match-instrtype}{\vdash} .. |vdashfunctypematch| mathdef:: \xref{valid/matching}{match-functype}{\vdash} +.. |vdashstructtypematch| mathdef:: \xref{valid/matching}{match-structtype}{\vdash} +.. |vdasharraytypematch| mathdef:: \xref{valid/matching}{match-arraytype}{\vdash} +.. |vdashstrtypematch| mathdef:: \xref{valid/matching}{match-strtype}{\vdash} +.. |vdashdeftypematch| mathdef:: \xref{valid/matching}{match-deftype}{\vdash} .. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash} .. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash} .. |vdashglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\vdash} @@ -1243,7 +1257,7 @@ .. Stack, meta functions -.. |expand| mathdef:: \xref{exec/runtime}{exec-expand}{\F{expand}} +.. |fblocktype| mathdef:: \xref{exec/runtime}{aux-fblocktype}{\F{instrtype}} .. Administrative Instructions, terminals diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 05581d4eb..f60adc76f 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -232,6 +232,439 @@ Reference Instructions C \vdashinstr \REFASNONNULL : [(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})] } +.. _valid-ref.eq: + +:math:`\REFEQ` +.............. + +* The instruction is valid with type :math:`[(\REF~\NULL~\EQT) (\REF~\NULL~\EQT)] \to [\I32]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \REFEQ : [(\REF~\NULL~\EQT)~(\REF~\NULL~\EQT)] \to [\I32] + } + +.. _valid-ref.test: + +:math:`\REFTEST~\X{rt}` +....................... + +* The :ref:`reference type ` :math:`\X{rt}` must be :ref:`valid `. + +* Then the instruction is valid with type :math:`[\X{rt}'] \to [\I32]` for any :ref:`valid ` :ref:`reference type ` :math:`\X{rt}'` for which :math:`\X{rt}` :ref:`matches ` :math:`\X{rt}'`. + +.. math:: + \frac{ + C \vdashreftype \X{rt} \ok + \qquad + C \vdashreftypematch \X{rt} \matchesreftype \X{rt}' + }{ + C \vdashinstr \REFTEST~\X{rt} : [\X{rt}'] \to [\I32] + } + +.. _valid-ref.cast: + +:math:`\REFCAST~\X{rt}` +....................... + +* The :ref:`reference type ` :math:`\X{rt}` must be :ref:`valid `. + +* Then the instruction is valid with type :math:`[\X{rt}'] \to [\X{rt}]` for any :ref:`valid ` :ref:`reference type ` :math:`\X{rt}'` for which :math:`\X{rt}` :ref:`matches ` :math:`\X{rt}'`. + +.. math:: + \frac{ + C \vdashreftype \X{rt} \ok + \qquad + C \vdashreftypematch \X{rt} \matchesreftype \X{rt}' + }{ + C \vdashinstr \REFCAST~\X{rt} : [\X{rt}'] \to [\X{rt}] + } + + +.. index:: aggregate reference + +Aggregate Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. _valid-struct.new: + +:math:`\STRUCTNEW~x` +.................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be a :ref:`structure type ` :math:`\TSTRUCT~\fieldtype^\ast`. + +* For each :ref:`field type ` :math:`\fieldtype_i` in :math:`\fieldtype^\ast`: + + - Let :math:`\fieldtype_i` be :math:`\mut~\storagetype_i`. + + - Let :math:`t_i` be the :ref:`value type ` :math:`\unpacktype(\storagetype_i)`. + +* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. + +* Then the instruction is valid with type :math:`[t^\ast] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TSTRUCT~(\mut~\X{st})^\ast + }{ + C \vdashinstr \STRUCTNEW~x : [(\unpacktype(\X{st}))^\ast] \to [(\REF~x)] + } + +.. _valid-struct.new_default: + +:math:`\STRUCTNEWDEFAULT~x` +........................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be a :ref:`structure type ` :math:`\TSTRUCT~\fieldtype^\ast`. + +* For each :ref:`field type ` :math:`\fieldtype_i` in :math:`\fieldtype^\ast`: + + - Let :math:`\fieldtype_i` be :math:`\mut~\storagetype_i`. + + - Let :math:`t_i` be the :ref:`value type ` :math:`\unpacktype(\storagetype_i)`. + + - The type :math:`t_i` must be :ref:`defaultable `. + +* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. + +* Then the instruction is valid with type :math:`[] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TSTRUCT~(\mut~\X{st})^\ast + \qquad + (C \vdashvaltypedefaultable \unpacktype(\X{st}) \defaultable)^\ast + }{ + C \vdashinstr \STRUCTNEWDEFAULT~x : [] \to [(\REF~x)] + } + +.. _valid-struct.get: +.. _valid-struct.get_u: +.. _valid-struct.get_s: + +:math:`\STRUCTGET\K{\_}\sx^?~x~i` +................................. + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be a :ref:`structure type ` :math:`\TSTRUCT~\fieldtype^\ast`. + +* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype^\ast[i]`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* The extension :math:`\sx` must be present if and only if :math:`\storagetype` is a :ref:`packed type `. + +* Then the instruction is valid with type :math:`[(\REF~\NULL~x)] \to [t]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast + \qquad + \X{ft}^\ast[i] = \mut~\X{st} + \qquad + \sx = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st}) + }{ + C \vdashinstr \STRUCTGET\K{\_}\sx^?~x~i : [(\REF~\NULL~x)] \to [\unpacktype(\X{st})] + } + +.. _valid-struct.set: + +:math:`\STRUCTSET~x~i` +...................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be a :ref:`structure type ` :math:`\TSTRUCT~\fieldtype^\ast`. + +* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype^\ast[i]`. + +* The prefix :math:`\mut` must be :math:`\MVAR`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* Then the instruction is valid with type :math:`[(\REF~\NULL~x)~t] \to []`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast + \qquad + \X{ft}^\ast[i] = \MVAR~\X{st} + }{ + C \vdashinstr \STRUCTSET~x~i : [(\REF~\NULL~x)~\unpacktype(\X{st})] \to [] + } + + +.. _valid-array.new: + +:math:`\ARRAYNEW~x` +................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let :math:`\fieldtype` be :math:`\mut~\storagetype`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* Then the instruction is valid with type :math:`[t~\I32] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + }{ + C \vdashinstr \ARRAYNEW~x : [\unpacktype(\X{st})~\I32] \to [(\REF~x)] + } + +.. _valid-array.new_default: + +:math:`\ARRAYNEWDEFAULT~x` +.......................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let :math:`\fieldtype` be :math:`\mut~\storagetype`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* The type :math:`t` must be :ref:`defaultable `. + +* Then the instruction is valid with type :math:`[\I32] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \qquad + C \vdashvaltypedefaultable \unpacktype(\X{st}) \defaultable + }{ + C \vdashinstr \ARRAYNEW~x : [\I32] \to [(\REF~x)] + } + +.. _valid-array.new_fixed: + +:math:`\ARRAYNEWFIXED~x~n` +.......................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let :math:`\fieldtype` be :math:`\mut~\storagetype`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* Then the instruction is valid with type :math:`[t^n] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + }{ + C \vdashinstr \ARRAYNEWFIXED~x~n : [\unpacktype(\X{st})^n] \to [(\REF~x)] + } + +.. _valid-array.new_elem: + +:math:`\ARRAYNEWELEM~x~y` +......................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let :math:`\fieldtype` be :math:`\mut~\storagetype`. + +* The :ref:`storage type ` :math:`\storagetype` must be a :ref:`reference type ` :math:`\X{rt}`. + +* The :ref:`element segment ` :math:`C.\CELEMS[y]` must exist. + +* Let :math:`\X{rt}'` be the :ref:`reference type ` :math:`C.\CELEMS[y]`. + +* The :ref:`reference type ` :math:`\X{rt}'` must :ref:`match ` :math:`\X{rt}`. + +* Then the instruction is valid with type :math:`[\I32~\I32] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{rt}) + \qquad + C \vdashreftypematch C.\CELEMS[y] \matchesreftype \X{rt} + }{ + C \vdashinstr \ARRAYNEWELEM~x~n : [\I32~\I32] \to [(\REF~x)] + } + + +.. _valid-array.new_data: + +:math:`\ARRAYNEWDATA~x~y` +......................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let :math:`\fieldtype` be :math:`\mut~\storagetype`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* The type :math:`t` must be a :ref:`numeric type ` or a :ref:`vector type `. + +* The :ref:`data segment ` :math:`C.\CDATAS[y]` must exist. + +* Then the instruction is valid with type :math:`[\I32~\I32] \to [(\REF~x)]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \qquad + \unpacktype(\X{st}) = \numtype \lor \unpacktype(\X{st}) = \vectype + \qquad + C.\CDATAS[y] = {\ok} + }{ + C \vdashinstr \ARRAYNEWDATA~x~n : [\I32~\I32] \to [(\REF~x)] + } + + +.. _valid-array.get: +.. _valid-array.get_u: +.. _valid-array.get_s: + +:math:`\ARRAYGET\K{\_}\sx^?~x` +.............................. + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* The extension :math:`\sx` must be present if and only if :math:`\storagetype` is a :ref:`packed type `. + +* Then the instruction is valid with type :math:`[(\REF~\NULL~x)~\I32] \to [t]`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \qquad + \sx = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st}) + }{ + C \vdashinstr \ARRAYGET\K{\_}\sx^?~x : [(\REF~\NULL~x)~\I32] \to [\unpacktype(\X{st})] + } + +.. _valid-array.set: + +:math:`\ARRAYSET~x~i` +..................... + +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must exist. + +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. + +* Let the :ref:`field type ` :math:`\mut~\storagetype` be :math:`\fieldtype`. + +* The prefix :math:`\mut` must be :math:`\MVAR`. + +* Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. + +* Then the instruction is valid with type :math:`[(\REF~\NULL~x)~\I32~t] \to []`. + +.. math:: + \frac{ + \expand(C.\CTYPES[x]) = \TARRAY~(\MVAR~\X{st}) + }{ + C \vdashinstr \ARRAYSET~x : [(\REF~\NULL~x)~\I32~\unpacktype(\X{st})] \to [] + } + +.. _valid-array.len: + +:math:`\ARRAYLEN` +................. + +* The the instruction is valid with type :math:`[(\REF~\NULL~\ARRAY)] \to [\I32]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \ARRAYLEN : [(\REF~\NULL~\ARRAY)] \to [\I32] + } + + + +.. index:: scalar reference + +Scalar Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. _valid-i31.new: + +:math:`\I31NEW` +............... + +* The instruction is valid with type :math:`[\I32] \to [(\REF~\I31)]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \I31NEW : [\I32] \to [(\REF~\I31)] + } + +.. _valid-i31.get_sx: + +:math:`\I31GET\K{\_}\sx` +........................ + +* The instruction is valid with type :math:`[(\REF~\NULL~\I31)] \to [\I32]`. + +.. math:: + \frac{ + }{ + C \vdashinstr \I31GET\K{\_}\sx : [(\REF~\NULL~\I31)] \to [\I32] + } + + +.. index:: external reference + +External Reference Instructions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. _valid-extern.internalize: + +:math:`\EXTERNINTERNALIZE` +.......................... + +* The instruction is valid with type :math:`[(\REF~\NULL_1^?~\EXTERN)] \to [(\REF~\NULL_2^?~\ANY)]` for any :math:`\NULL_1^?` that equals :math:`\NULL_2^?`. + +.. math:: + \frac{ + \NULL_1^? = \NULL_2^? + }{ + C \vdashinstr \EXTERNINTERNALIZE : [(\REF~\NULL_1^?~\EXTERN)] \to [(\REF~\NULL_2^?~\ANY)] + } + +.. _valid-extern.externalize: + +:math:`\EXTERNEXTERNALIZE` +.......................... + +* The instruction is valid with type :math:`[(\REF~\NULL_1^?~\ANY)] \to [(\REF~\NULL_2^?~\EXTERN)]` for any :math:`\NULL_1^?` that equals :math:`\NULL_2^?`. + +.. math:: + \frac{ + \NULL_1^? = \NULL_2^? + }{ + C \vdashinstr \EXTERNEXTERNALIZE : [(\REF~\NULL_1^?~\ANY)] \to [(\REF~\NULL_2^?~\EXTERN)] + } + + .. index:: vector instruction pair: validation; instruction single: abstract syntax; instruction @@ -1491,6 +1924,84 @@ Control Instructions } +.. _valid-br_on_cast: + +:math:`\BRONCAST~l~\X{rt}_1~\X{rt}_2` +..................................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* Let :math:`[t_l^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* The type sequence :math:`t_l^\ast` must be of the form :math:`t^\ast~\X{rt}'`. + +* The :ref:`reference type ` :math:`\X{rt}_1` must be :ref:`valid `. + +* The :ref:`reference type ` :math:`\X{rt}_2` must be :ref:`valid `. + +* The :ref:`reference type ` :math:`\X{rt}_2` must :ref:`match ` :math:`\X{rt}_1`. + +* The :ref:`reference type ` :math:`\X{rt}_2` must :ref:`match ` :math:`\X{rt}'`. + +* Let :math:`\X{rt}'_1` be the :ref:`type difference ` between :math:`\X{rt}_1` and :math:`\X{rt}_2`. + +* Then the instruction is valid with type :math:`[t^\ast~\X{rt}_1] \to [t^\ast~\X{rt}'_1]`. + +.. math:: + \frac{ + C.\CLABELS[l] = [t^\ast~\X{rt}'] + \qquad + C \vdashreftype \X{rt}_1 \ok + \qquad + C \vdashreftype \X{rt}_2 \ok + \qquad + C \vdashreftypematch \X{rt}_2 \matchesreftype \X{rt}_1 + \qquad + C \vdashreftypematch \X{rt}_2 \matchesreftype \X{rt}' + }{ + C \vdashinstr \BRONCAST~l~\X{rt}_1~\X{rt}_2` : [t^\ast~\X{rt}_1] \to [t^\ast~\X{rt}_1\reftypediff\X{rt}_2] + } + + +.. _valid-br_on_cast_fail: + +:math:`\BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2` +......................................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* Let :math:`[t_l^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* The type sequence :math:`t_l^\ast` must be of the form :math:`t^\ast~\X{rt}'`. + +* The :ref:`reference type ` :math:`\X{rt}_1` must be :ref:`valid `. + +* The :ref:`reference type ` :math:`\X{rt}_2` must be :ref:`valid `. + +* The :ref:`reference type ` :math:`\X{rt}_2` must :ref:`match ` :math:`\X{rt}_1`. + +* Let :math:`\X{rt}'_1` be the :ref:`type difference ` between :math:`\X{rt}_1` and :math:`\X{rt}_2`. + +* The :ref:`reference type ` :math:`\X{rt}'_1` must :ref:`match ` :math:`\X{rt}'`. + +* Then the instruction is valid with type :math:`[t^\ast~\X{rt}_1] \to [t^\ast~\X{rt}_2]`. + +.. math:: + \frac{ + C.\CLABELS[l] = [t^\ast~\X{rt}'] + \qquad + C \vdashreftype \X{rt}_1 \ok + \qquad + C \vdashreftype \X{rt}_2 \ok + \qquad + C \vdashreftypematch \X{rt}_2 \matchesreftype \X{rt}_1 + \qquad + C \vdashreftypematch \X{rt}_1\reftypediff\X{rt}_2 \matchesreftype \X{rt}' + }{ + C \vdashinstr \BRONCASTFAIL~l~\X{rt}_1~\X{rt}_2` : [t^\ast~\X{rt}_1] \to [t^\ast~\X{rt}_2] + } + + .. _valid-return: :math:`\RETURN` diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 550d89577..0f835f3f8 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -20,9 +20,9 @@ Functions :math:`\func` are classified by :ref:`type indices ` r :math:`\{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \}` ..................................................... -* The type :math:`C.\CTYPES[x]` must be defined in the context. +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must be a :ref:`function type `. -* Let :math:`[t_1^\ast] \toF [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. +* Let :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]` be the :ref:`expansion ` of the :ref:`defined type ` :math:`C.\CTYPES[x]`. * For each local declared by a :ref:`value type ` :math:`t` in :math:`t^\ast`: @@ -46,7 +46,7 @@ Functions :math:`\func` are classified by :ref:`type indices ` r .. math:: \frac{ - C.\CTYPES[x] = [t_1^\ast] \toF [t_2^\ast] + \expand(C.\CTYPES[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] \qquad (C \vdashlocal t : \init~t)^\ast \qquad @@ -379,14 +379,14 @@ Start function declarations :math:`\start` are not classified by any type. * Assert: The type :math:`C.\CTYPES[y]` is defined in the context. -* The type :math:`C.\CTYPES[y]` must be the :ref:`function type ` :math:`[] \toF []`. +* The type :math:`C.\CTYPES[y]` must be the :ref:`function type ` :math:`\TFUNC~[] \toF []`. * Then the start function is valid. .. math:: \frac{ - C.\CTYPES[C.\CFUNCS[x]] = [] \toF [] + C.\CTYPES[C.\CFUNCS[x]] = \TFUNC~[] \toF [] }{ C \vdashstart \{ \SFUNC~x \} \ok } @@ -430,7 +430,7 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi \frac{ C.\CFUNCS[x] = \functype }{ - C \vdashexportdesc \EDFUNC~x : \ETFUNC~\functype + C \vdashexportdesc \EDFUNC~x : \ETFUNC~(\TFUNC~\functype) } @@ -509,15 +509,15 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi :math:`\IDFUNC~x` ................. -* The :ref:`function type ` :math:`C.\CTYPES[x]` must be defined in the context. +* The :ref:`defined type ` :math:`C.\CTYPES[x]` must be a :ref:`function type `. -* Then the import description is valid with type :math:`\ETFUNC~x`. +* Then the import description is valid with type :math:`\ETFUNC~C.\CTYPES[x]`. .. math:: \frac{ - C.\CTYPES[x] = \functype + \expand(C.\CTYPES[x]) = \TFUNC~\functype }{ - C \vdashimportdesc \IDFUNC~x : \ETFUNC~x + C \vdashimportdesc \IDFUNC~x : \ETFUNC~C.\CTYPES[x] } @@ -588,6 +588,8 @@ The :ref:`external types ` classifying a module may contain f * Let :math:`C` be a :ref:`context ` where: + * .. todo:: Adjust type context + * :math:`C.\CTYPES` is :math:`\module.\MTYPES`, * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`, @@ -614,11 +616,13 @@ The :ref:`external types ` classifying a module may contain f * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)`, i.e., the set of :ref:`function indices ` occurring in the module, except in its :ref:`functions ` or :ref:`start function `. -* For each function type :math:`\functype_i` in :math:`\module.\MTYPES`: +* For each recursive type :math:`\rectype_i` in :math:`\module.\MTYPES`: + + * .. todo:: expand rectypes * Let :math:`C_i` be the :ref:`context ` where :math:`C_i.\CTYPES` is :math:`C.\CTYPES[0 \slice i]` and all other fields are empty. - * The function :math:`\functype_i` must be :ref:`valid ` under context :math:`C_i`. + * The recursive type :math:`\rectype_i` must be :ref:`valid ` under context :math:`C_i`. * Let :math:`C'` be the :ref:`context ` where: diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index dc21aa29e..04492b4ab 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -169,7 +169,7 @@ Block Types .. math:: \frac{ - C.\CTYPES[\typeidx] = [t_1^\ast] \toF [t_2^\ast] + \expand(C.\CTYPES[\typeidx]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] }{ C \vdashblocktype \typeidx : [t_1^\ast] \to [t_2^\ast] } @@ -388,18 +388,22 @@ Global Types External Types ~~~~~~~~~~~~~~ -:math:`\ETFUNC~\typeidx` +:math:`\ETFUNC~\deftype` ........................ -* The :ref:`function type ` :math:`C.\CTYPES[x]` must be defined in the context. +* The :ref:`defined type ` :math:`\deftype` must be :ref:`valid `. + +* The :ref:`defined type ` :math:`\deftype` must be a :ref:`function type `. * Then the external type is valid. .. math:: \frac{ - C.\CTYPES[x] = \functype + C \vdashdeftype \deftype \ok + \qquad + \expand(\deftype) = \TFUNC~\functype }{ - C \vdashexterntype \ETFUNC~x + C \vdashexterntype \ETFUNC~\deftype } :math:`\ETTABLE~\tabletype` diff --git a/proposals/gc/MVP.md b/proposals/gc/MVP.md index 8039aa9e3..c060e0feb 100644 --- a/proposals/gc/MVP.md +++ b/proposals/gc/MVP.md @@ -688,8 +688,6 @@ where: - `(ref null1? ht1)\(ref null ht2) = (ref ht1)` - `(ref null1? ht1)\(ref ht2) = (ref null1? ht1)` -Note: Cast instructions do _not_ require the operand's source type to be a supertype of the target type. It can also be a "sibling" in the same hierarchy, i.e., they only need to have a common supertype (in practice, it is sufficient to test that both types share the same top heap type.). Allowing so is necessary to maintain subtype substitutability, i.e., the ability to maintain well-typedness when operands are replaced by subtypes. - Note: The [reference types](https://github.com/WebAssembly/reference-types) and [typed function references](https://github.com/WebAssembly/function-references)already introduce similar `ref.is_null`, `br_on_null`, and `br_on_non_null` instructions. These can now be interpreted as syntactic sugar: * `ref.is_null` is equivalent to `ref.test null ht`, where `ht` is the suitable bottom type (`none`, `nofunc`, or `noextern`) @@ -700,8 +698,6 @@ Note: The [reference types](https://github.com/WebAssembly/reference-types) and * finally, `ref.as_non_null` is equivalent to `ref.cast ht`, where `ht` is the heap type of the operand -TODO: Should we remove the latter 3 from the typed function references proposal? - #### Constant Expressions