diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index dbb2baa7e..4768e4012 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -188,7 +188,7 @@ Added managed reference types [#proposal-gc]_. * New :ref:`reference instructions ` for :ref:`array types `: |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |ARRAYNEWDATA|, |ARRAYNEWELEM|, :math:`\ARRAYGET\K{\_}\sx^?`, |ARRAYSET|, |ARRAYLEN|, |ARRAYFILL|, |ARRAYCOPY|, |ARRAYINITDATA|, |ARRAYINITELEM| -* New :ref:`reference instructions ` for converting :ref:`host types `: |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE| +* New :ref:`reference instructions ` for converting :ref:`host types `: |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE| * Extended set of :ref:`constant instructions ` with |I31NEW|, |STRUCTNEW|, |STRUCTNEWDEFAULT|, |ARRAYNEW|, |ARRAYNEWDEFAULT|, |ARRAYNEWFIXED|, |EXTERNINTERNALIZE|, |EXTERNEXTERNALIZE|, and |GLOBALGET| for any previously declared immutable :ref:`global ` diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index ea5c5c67c..51e0433fc 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -20,6 +20,24 @@ The typing rules defining WebAssembly :ref:`validation ` only cover the * In order to state and prove soundness precisely, the typing rules must be extended to the *dynamic* components of the abstract :ref:`runtime `, that is, the :ref:`store `, :ref:`configurations `, and :ref:`administrative instructions `. [#cite-pldi2017]_ +.. index:: context, recursive types, recursive type indices +.. context-rec: + +Contexts +~~~~~~~~ + +.. todo:: maybe move elsewhere? + +In order to check :ref:`rolled up ` recursive types, +the :ref:`context ` is locally extended with an additional component that records the :ref:`supertypes ` of each :ref:`recursive type index `, represented as :ref:`defined types `: + +.. math:: + \begin{array}{llll} + \production{context} & C &::=& + \{~ \dots, \CRECS ~ (\deftype^\ast)^\ast ~\} \\ + \end{array} + + .. index:: value, value type, result, result type, trap .. _valid-result: diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ec347147f..dbaca3c07 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -394,12 +394,12 @@ Reference Instructions \end{array} -.. _exec-i31.get_s: +.. _exec-i31.get_sx: :math:`\I31GET\K{\_}\sx` ........................ -1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~\I31)` is on the top of the stack. +1. Assert: due to :ref:`validation `, a :ref:`value ` of :ref:`type ` :math:`(\REF~\NULL~\I31)` is on the top of the stack. 2. Pop the value :math:`\reff` from the stack. @@ -462,7 +462,7 @@ Reference Instructions S; F; \val^n~(\STRUCTNEW~x) &\stepto& S'; F; (\REFSTRUCTADDR~|S.\SSTRUCTS|) \\&& \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n) + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}) + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + (\iff & \expanddt(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} \\ @@ -728,7 +728,7 @@ Reference Instructions 4. Let :math:`\TARRAY~\X{ft}` be the :ref:`array type ` :math:`\deftype`. (todo: unroll) -5. Assert: due to :ref:`validation `, :math:`n` :ref:`values ` are on the top of the stack. +5. Assert: due to :ref:`validation `, :math:`n` :ref:`values ` are on the top of the stack. 6. Pop the :math:`n` values :math:`\val^\ast` from the stack. @@ -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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ + (\iff & \expanddt(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} \\ @@ -788,9 +788,9 @@ Reference Instructions 11. Pop the value :math:`(\I32.\CONST~s)` from the stack. -12. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`size `. +12. Assert: due to :ref:`validation `, the :ref:`field type ` :math:`\X{ft}` has a defined :ref:`bit width `. -13. Let :math:`z` be the :ref:`size ` of :ref:`field type ` :math:`\X{ft}`. +13. Let :math:`z` be the :ref:`bit width ` of :ref:`field type ` :math:`\X{ft}`. 14. If the sum of :math:`s` and :math:`n` times :math:`z` is larger than the length of :math:`\datainst.\DIDATA`, then: @@ -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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ + (\iff & \expanddt(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft}^n \\ \land & t = \unpacktype(\X{ft}) \\ \land & (\bytes_{\X{ft}}(c))^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|] \\ \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 & \expand(F.\AMODULE.\MITYPES[x]) = \TARRAY~\X{ft} \\ + (\iff & \expanddt(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 & \expand(F.\AMODULE.\MITYPES[x]) = \TSTRUCT~\X{ft}^n \\ + (\iff & \expanddt(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 @@ -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:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`structured type ` :math:`\expand(\X{f}.\FITYPE)`. +3. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`compound type ` :math:`\expanddt(\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 & \expand(S.f.\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m] \\ + \wedge & \expanddt(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:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`structured type ` :math:`\expand(S.\SFUNCS[a].\FITYPE)`. +2. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`compound type ` :math:`\expanddt(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 \expand(S.\SFUNCS[a].\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m]) + & (\iff \expanddt(S.\SFUNCS[a].\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m]) \end{array} @@ -4337,7 +4337,7 @@ Furthermore, the resulting store must be :ref:`valid `, i.e., all d \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTCODE~\X{hf} \} \\ - \wedge & \expand(\deftype) = \TFUNC~[t_1^n] \toF [t_2^m] \\ + \wedge & \expanddt(\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} @@ -4346,7 +4346,7 @@ Furthermore, the resulting store must be :ref:`valid `, i.e., all d \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTCODE~\X{hf} \} \\ - \wedge & \expand(\deftype) = \TFUNC~[t_1^n] \toF [t_2^m] \\ + \wedge & \expanddt(\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 f0bb58ee1..8d107a6f9 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -290,6 +290,9 @@ Growing :ref:`memories ` :ref:`Modules ` .................................. +.. todo:: update prose for types +.. todo:: change semantics for globals + The allocation function for :ref:`modules ` requires a suitable list of :ref:`external values ` that are assumed to :ref:`match ` the :ref:`import ` vector of the module, a list of initialization :ref:`values ` for the module's :ref:`globals `, and list of :ref:`reference ` vectors for the module's :ref:`element segments `. @@ -381,8 +384,6 @@ and list of :ref:`reference ` vectors for the module's :ref:`element where: -.. todo:: adjust deftypes - .. math:: \begin{array}{@{}rlll@{}} \table^\ast &=& \module.\MTABLES \\ @@ -403,7 +404,7 @@ where: \MIEXPORTS~\exportinst^\ast ~\} \end{array} \\[1ex] \deftype^\ast &=& - \insttype_{\moduleinst}(\module.\MTYPES) \\ + \alloctype^\ast(\module.\MTYPES) \\ S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\ S_2, \tableaddr^\ast &=& @@ -450,8 +451,30 @@ Here, the notation :math:`\F{allocx}^\ast` is shorthand for multiple :ref:`alloc Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals or tables), then the elements of this sequence are passed to the allocation function pointwise. +For types, however, allocation is defined in terms of :ref:`rolling `: + +.. math:: + \begin{array}{rlll} + \alloctype^\ast(\rectype^n) = \deftype^\ast \\[1ex] + \mbox{where for all $i < n$:} \hfill \\ + \deftype^\ast[x_i \slice m_i] &=& \rolldt{x_i}(\rectype^n[i])[\subst \deftype^\ast[0 : \slice x_i]) \\ + x_{i+1} &=& x_i + m_i \land x_n = |\deftype^\ast| \\ + \end{array} + +.. todo:: unify with type closure somehow? + + +.. scratch + \begin{array}{rlll} + \alloctype^\ast(\epsilon) = \epsilon \\ + \alloctype^\ast(\rectype^\ast~\rectype') = \deftype^\ast~{\deftype'}^\ast \\[1ex] + \mbox{where:} \hfill \\ + \deftype^\ast &=& \alloctype^\ast(\reftype^\ast) \\ + {\deftype'}^\ast &=& \rolldt{|\deftype^\ast|}(\rectype)[\subst \deftype^\ast) \\ + \end{array} + .. note:: - The definition of module allocation is mutually recursive with the allocation of its associated types and functions, because the resulting module instance :math:`\moduleinst` is passed to the allocators as an argument, in order to form the necessary closures. + The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance :math:`\moduleinst` is passed to the allocators as an argument, in order to form the necessary closures. In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step. @@ -665,7 +688,7 @@ The following steps are performed: 2. Let :math:`\funcinst` be the :ref:`function instance ` :math:`S.\SFUNCS[\funcaddr]`. -3. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`structured type ` :math:`\expand(\funcinst.\FITYPE)`. +3. Let :math:`\TFUNC~[t_1^n] \toF [t_2^m]` be the :ref:`compound type ` :math:`\expanddt(\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: @@ -697,7 +720,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 & \expand(S.\SFUNCS[\funcaddr].\FITYPE) = \TFUNC~[t_1^n] \toF [t_2^m] \\ + &(\iff & \expanddt(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 4aace7289..bf3b4ef69 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -609,7 +609,7 @@ Conventions .. math:: \begin{array}{llll} - \fblocktype_{S;F}(\typeidx) &=& \functype & (\iff \expand(F.\AMODULE.\MITYPES[\typeidx]) = \TFUNC~\functype) \\ + \fblocktype_{S;F}(\typeidx) &=& \functype & (\iff \expanddt(F.\AMODULE.\MITYPES[\typeidx]) = \TFUNC~\functype) \\ \fblocktype_{S;F}([\valtype^?]) &=& [] \to [\valtype^?] \\ \end{array} diff --git a/document/core/exec/types.rst b/document/core/exec/types.rst index 6742ba1aa..89f2e1fa4 100644 --- a/document/core/exec/types.rst +++ b/document/core/exec/types.rst @@ -24,3 +24,6 @@ Any form of :ref:`type ` can be *instantiated* into a :ref:`closed .. math:: \insttype_{\moduleinst}(t) = t[\subst \moduleinst.\MITYPES] + +.. note:: + This is the runtime equivalent to :ref:`type closure `. diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst index 27543c71c..d7a7de952 100644 --- a/document/core/exec/values.rst +++ b/document/core/exec/values.rst @@ -91,7 +91,7 @@ The following auxiliary typing rules specify this typing relation relative to a * Let :math:`\deftype` be the :ref:`defined type ` :math:`\structinst.\SITYPE`. -* The :ref:`expansion ` of :math:`\deftype` must be a :ref:`struct type `. +* The :ref:`expansion ` of :math:`\deftype` must be a :ref:`struct type `. * Then the value is valid with :ref:`reference type ` :math:`(\REF~\deftype)`. @@ -99,7 +99,7 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ \deftype = S.\SSTRUCTS[a].\SITYPE \qquad - \expand(\deftype) = \TSTRUCT~\structtype + \expanddt(\deftype) = \TSTRUCT~\structtype }{ S \vdashval \REFSTRUCTADDR~a : \REF~\deftype } @@ -116,7 +116,7 @@ The following auxiliary typing rules specify this typing relation relative to a * Let :math:`\deftype` be the :ref:`defined type ` :math:`\arrayinst.\AITYPE`. -* The :ref:`expansion ` of :math:`\deftype` must be an :ref:`array type `. +* The :ref:`expansion ` of :math:`\deftype` must be an :ref:`array type `. * Then the value is valid with :ref:`reference type ` :math:`(\REF~\arraytype)`. @@ -124,7 +124,7 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ \deftype = S.\SARRAYS[a].\AITYPE \qquad - \expand(\deftype) = \TARRAY~\arraytype + \expanddt(\deftype) = \TARRAY~\arraytype }{ S \vdashval \REFARRAYADDR~a : \REF~\deftype } @@ -139,7 +139,7 @@ The following auxiliary typing rules specify this typing relation relative to a * Let :math:`\deftype` be the :ref:`defined type ` :math:`\funcinst.\FITYPE`. -* The :ref:`expansion ` of :math:`\deftype` must be a :ref:`function type `. +* The :ref:`expansion ` of :math:`\deftype` must be a :ref:`function type `. * Then the value is valid with :ref:`reference type ` :math:`(\REF~\functype)`. @@ -147,7 +147,7 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ \deftype = S.\SFUNCS[a].\FITYPE \qquad - \expand(\deftype) = \TFUNC~\functype + \expanddt(\deftype) = \TFUNC~\functype }{ S \vdashval \REFFUNCADDR~a : \REF~\deftype } diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 5e146af08..8d4efe959 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -351,7 +351,7 @@ Operations are performed point-wise on the values of each lane. .. note:: For example, the shape :math:`\K{i32x4}` interprets the operand as four |i32| values, packed into an |i128|. - The bitwidth of the numeric type :math:`t` times :math:`N` always is 128. + The bit width of the numeric type :math:`t` times :math:`N` always is 128. Instructions prefixed with :math:`\K{v128}` do not involve a specific interpretation, and treat the |V128| as an |i128| value or a vector of 128 individual bits. @@ -451,7 +451,7 @@ while |REFASNONNULL| converts a :ref:`nullable ` to a non-null o The |REFEQ| compares two references. -The instructions |REFTEST| and |REFCAST| test the :ref:`dynamic type ` of a reference operand. +The instructions |REFTEST| and |REFCAST| test the :ref:`dynamic type ` of a reference operand. The former merely returns the result of the test, while the latter performs a downcast and :ref:`traps ` if the operand's type does not match. @@ -495,7 +495,7 @@ while the latter performs a downcast and :ref:`traps ` if the operand's ty Aggregate Instructions ~~~~~~~~~~~~~~~~~~~~~~ -Instructions in this group are concerned with creating and accessing :ref:`references ` to :ref:`aggregate ` types. +Instructions in this group are concerned with creating and accessing :ref:`references ` to :ref:`aggregate ` types. .. math:: \begin{array}{llrl} diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index a32644612..e4cbed2db 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -34,7 +34,8 @@ They correspond to the respective binary floating-point representations, also kn Number types are *transparent*, meaning that their bit patterns can be observed. Values of number type can be stored in :ref:`memories `. -.. _bitwidth: +.. _bitwidth-numtype: +.. _bitwidth-valtype: Conventions ........... @@ -66,17 +67,17 @@ values, or a single 128 bit type. The interpretation is determined by individual Vector types, like :ref:`number types ` are *transparent*, meaning that their bit patterns can be observed. Values of vector type can be stored in :ref:`memories `. +.. _bitwidth-vectype: + Conventions ........... -* The notation :math:`|t|` for :ref:`bit width ` extends to vector types as well, that is, :math:`|\V128| = 128`. +* The notation :math:`|t|` for :ref:`bit width ` extends to vector types as well, that is, :math:`|\V128| = 128`. -.. index:: ! heap type, store, type identifier, ! substitution, ! closed type, ! abstract type, ! concrete type, ! unboxed scalar +.. index:: ! heap type, store, type index, ! abstract type, ! concrete type, ! unboxed scalar pair: abstract syntax; heap type -.. _type-subst: -.. _type-closed: .. _type-abstract: .. _type-concrete: .. _syntax-i31: @@ -97,11 +98,12 @@ That is, both type hierarchies are inhabited by an isomorphic set of values, but .. math:: \begin{array}{llrl} - \production{heap type} & \heaptype &::=& + \production{abstract heap type} & \absheaptype &::=& \FUNC ~|~ \NOFUNC \\&&|& \EXTERN ~|~ \NOEXTERN \\&&|& - \ANY ~|~ \EQT ~|~ \I31 ~|~ \STRUCT ~|~ \ARRAY ~|~ \NONE \\&&|& - \typeidx ~|~ \deftype ~|~ \BOT \\ + \ANY ~|~ \EQT ~|~ \I31 ~|~ \STRUCT ~|~ \ARRAY ~|~ \NONE \\ + \production{heap type} & \heaptype &::=& + \absheaptype ~|~ \typeidx \\ \end{array} A heap type is either *abstract* or *concrete*. @@ -132,34 +134,13 @@ Their observable value range is limited to 31 bits. Engines need to perform some form of *pointer tagging* to achieve this, which is why 1 bit is reserved. - -A concrete heap type consists of a :ref:`type index ` and classifies an object of the respective :ref:`type ` defined in some module. - -A concrete heap type can also consist of a :ref:`defined type ` directly. -However, this form is representable in neither the :ref:`binary format ` nor the :ref:`text format `, such that it cannot be used in a program; -it only occurs during :ref:`validation ` or :ref:`execution `, as the result of *substituting* a :ref:`type index ` with its definition. - -A type of any form is *closed* when it does not contain a heap type that is a :ref:`type index `, -i.e., all :ref:`type indices ` have been :ref:`substituted ` with their :ref:`defined type `. - -The type :math:`\BOT` is a :ref:`subtype ` of all heap types. -By virtue of being representable in neither the :ref:`binary format ` nor the :ref:`text format `, it cannot be used in a program; -it only occurs during :ref:`validation `, as a part of a possible operand type for instructions. - -.. note:: Although the types |NONE|, |NOFUNC|, and |NOEXTERN| are not inhabited by any values, they can be used to form the types of all null :ref:`references ` in their respective hierarchy. For example, :math:`(\REF~\NULL~\NOFUNC)` is the generic type of a null reference compatible with all function reference types. +A concrete heap type consists of a :ref:`type index ` and classifies an object of the respective :ref:`type ` defined in a module. -.. _notation-subst: - -Convention -.......... - -* :math:`t[x^\ast \subst \X{ft}^\ast]` denotes the parallel *substitution* of :ref:`type indices ` :math:`x^\ast` with :ref:`function types ` :math:`\X{ft}^\ast`, provided :math:`|x^\ast| = |\X{ft}^\ast|` in type :math:`t`. - -* :math:`t[\subst \X{ft}^\ast]` is shorthand for the substitution :math:`t[x^\ast \subst \X{ft}^\ast]` where :math:`x^\ast = 0 \cdots (|\X{ft}^\ast| - 1)` in type :math:`t`. +The syntax of heap types is :ref:`extended ` with additional forms for the purpose of specifying :ref:`validation ` and :ref:`execution `. .. index:: ! reference type, heap type, reference, table, function, function type, null @@ -187,47 +168,26 @@ 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 +.. index:: ! value type, number type, vector type, reference type pair: abstract syntax; value type pair: value; type .. _syntax-valtype: -.. _syntax-bottype: Value Types ~~~~~~~~~~~ *Value types* classify the individual values that WebAssembly code can compute with and the values that a variable accepts. -They are either :ref:`number types `, :ref:`vector types `, :ref:`reference types `, or the unique *bottom type*, written :math:`\BOT`. - -The type :math:`\BOT` is a :ref:`subtype ` of all other value types. -By virtue of being representable in neither the :ref:`binary format ` nor the :ref:`text format `, it cannot be used in a program; -it only occurs during :ref:`validation `, as a possible operand type for instructions. +They are either :ref:`number types `, :ref:`vector types `, or :ref:`reference types `. .. math:: \begin{array}{llrl} \production{value type} & \valtype &::=& - \numtype ~|~ \vectype ~|~ \reftype ~|~ \BOT \\ + \numtype ~|~ \vectype ~|~ \reftype \\ \end{array} +The syntax of value types is :ref:`extended ` with additional forms for the purpose of specifying :ref:`validation `. + Conventions ........... @@ -252,55 +212,6 @@ which is a sequence of values, written with brackets. \end{array} -.. index:: ! instruction type, value type, result type, instruction, local, local index - pair: abstract syntax; instruction type - pair: instruction; type -.. _syntax-instrtype: - -Instruction Types -~~~~~~~~~~~~~~~~~ - -*Instruction types* classify the behaviour of :ref:`instructions ` or instruction sequences, by describing how they manipulate the :ref:`operand stack ` and the initialization status of :ref:`locals `: - -.. math:: - \begin{array}{llrl} - \production{instruction type} & \instrtype &::=& - \resulttype \toX{\localidx^\ast} \resulttype \\ - \end{array} - -An instruction type :math:`[t_1^\ast] \toX{x^\ast} [t_2^\ast]` describes the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off -and the provided output stack with result values of types :math:`t_2^\ast` that it pushes back. -Moreover, it enumerates the :ref:`indices ` :math:`x^\ast` of locals that have been set by the instruction or sequence. - -.. note:: - Instruction types are only used for :ref:`validation `, - they do not occur in programs. - - -.. index:: ! local type, value type, local, local index - pair: abstract syntax; local type - pair: local; type -.. _syntax-init: -.. _syntax-localtype: - -Local Types -~~~~~~~~~~~ - -*Local types* classify :ref:`locals `, by describing their :ref:`value type ` as well as their *initialization status*: - -.. math:: - \begin{array}{llrl} - \production{initialization status} & \init &::=& - \SET ~|~ \UNSET \\ - \production{local type} & \localtype &::=& - \init~\valtype \\ - \end{array} - -.. note:: - Local types are only used for :ref:`validation `, - they do not occur in programs. - - .. index:: ! function type, value type, vector, function, parameter, result, result type pair: abstract syntax; function type pair: function; type @@ -316,11 +227,11 @@ They are also used to classify the inputs and outputs of :ref:`instructions ` extends to packed types as well, that is, :math:`|\I8| = 8` and :math:`|\I16| = 16`. -.. index:: ! structured type, function type, aggreagate type, structure type, array type - pair: abstract syntax; structured type -.. _syntax-strtype: -Structured Types -~~~~~~~~~~~~~~~~ +.. index:: ! compound type, function type, aggreagate type, structure type, array type + pair: abstract syntax; compound type +.. _syntax-comptype: -*Structured types* are all types composed from simpler types, +Compound Types +~~~~~~~~~~~~~~ + +*Compound types* are all types composed from simpler types, including :ref:`function types ` and :ref:`aggregate types `. .. math:: \begin{array}{llrl} - \production{structured type} & \strtype &::=& + \production{compound type} & \comptype &::=& \TFUNC~\functype ~|~ \TSTRUCT~\structtype ~|~ \TARRAY~\arraytype \\ \end{array} -.. index:: ! recursive type, ! sub type, structured type, ! final, subtyping +.. index:: ! recursive type, ! sub type, compound type, ! final, subtyping, ! roll, ! unroll, recursive type index pair: abstract syntax; recursive type pair: abstract syntax; sub type .. _syntax-rectype: @@ -382,59 +300,21 @@ including :ref:`function types ` and :ref:`aggregate types `, each of which can optionally declare a list of supertypes that it :ref:`matches `. +*Recursive types* denote a group of mutually recursive :ref:`compound types `, each of which can optionally declare a list of :ref:`type indices ` 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 \\ + \TSUB~\TFINAL^?~\typeidx^\ast~\comptype \\ \end{array} +In a :ref:`module `, each member of a recursive type is assigned a separate :ref:`type index `. -.. index:: ! defined type, recursive type, ! unroll, ! expand - pair: abstract syntax; defined type -.. _syntax-deftype: - -Defined Types -~~~~~~~~~~~~~ - -*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. - - -.. math:: - \begin{array}{llrl} - \production{defined type} & \deftype &::=& - \rectype.i \\ - \end{array} - -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} +The syntax of sub types is :ref:`generalized ` for the purpose of specifying :ref:`validation ` and :ref:`execution `. .. index:: ! limits, memory type, table type diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 43660d7dc..59aed667f 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -181,7 +181,8 @@ .. |to| mathdef:: \xref{syntax/types}{syntax-instrtype}{\rightarrow} .. |toX#1| mathdef:: \xref{syntax/types}{syntax-instrtype}{\rightarrow_{#1}} -.. |BOT| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{bot}} +.. |BOTH| mathdef:: \xref{valid/conventions}{syntax-heaptype-ext}{\K{bot}} +.. |BOT| mathdef:: \xref{valid/conventions}{syntax-valtype-ext}{\K{bot}} .. |I8| mathdef:: \xref{syntax/runtime}{syntax-storagetype}{\K{i8}} .. |I16| mathdef:: \xref{syntax/runtime}{syntax-storagetype}{\K{i16}} @@ -223,9 +224,11 @@ .. |NULLFUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullfuncref}} .. |NULLEXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{nullexternref}} -.. |TFUNC| mathdef:: \xref{syntax/types}{syntax-strtype}{\K{func}} -.. |TSTRUCT| mathdef:: \xref{syntax/types}{syntax-strtype}{\K{struct}} -.. |TARRAY| mathdef:: \xref{syntax/types}{syntax-strtype}{\K{array}} +.. |REC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{rec}} + +.. |TFUNC| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{func}} +.. |TSTRUCT| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{struct}} +.. |TARRAY| mathdef:: \xref{syntax/types}{syntax-comptype}{\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{final}} @@ -250,6 +253,7 @@ .. |numtype| mathdef:: \xref{syntax/types}{syntax-numtype}{\X{numtype}} .. |vectype| mathdef:: \xref{syntax/types}{syntax-vectype}{\X{vectype}} .. |heaptype| mathdef:: \xref{syntax/types}{syntax-heaptype}{\X{heaptype}} +.. |absheaptype| mathdef:: \xref{syntax/types}{syntax-absheaptype}{\X{absheaptype}} .. |reftype| mathdef:: \xref{syntax/types}{syntax-reftype}{\X{reftype}} .. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}} .. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}} @@ -259,10 +263,10 @@ .. |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}} +.. |comptype| mathdef:: \xref{syntax/types}{syntax-comptype}{\X{comptype}} .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}} .. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}} -.. |deftype| mathdef:: \xref{syntax/types}{syntax-deftype}{\X{deftype}} +.. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}} .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} @@ -272,17 +276,20 @@ .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}} .. |init| mathdef:: \xref{syntax/types}{syntax-init}{\X{init}} -.. |instrtype| mathdef:: \xref{syntax/types}{syntax-instrtype}{\X{instrtype}} -.. |localtype| mathdef:: \xref{syntax/types}{syntax-localtype}{\X{localtype}} +.. |instrtype| mathdef:: \xref{valid/conventions}{syntax-instrtype}{\X{instrtype}} +.. |localtype| mathdef:: \xref{valid/conventions}{syntax-localtype}{\X{localtype}} .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}} .. Types, meta functions -.. |reftypediff| mathdef:: \xref{syntax/types}{aux-reftypediff}{\setminus} +.. |reftypediff| mathdef:: \xref{valid/conventions}{aux-reftypediff}{\setminus} -.. |unroll| mathdef:: \xref{syntax/types}{aux-unroll}{\F{unroll}} -.. |expand| mathdef:: \xref{syntax/types}{aux-expand}{\F{expand}} +.. |rollrt#1| mathdef:: \xref{valid/conventions}{aux-roll-rectype}{\F{roll}_{#1}} +.. |unrollrt| mathdef:: \xref{valid/conventions}{aux-unroll-rectype}{\F{unroll}} +.. |rolldt#1| mathdef:: \xref{valid/conventions}{aux-roll-deftype}{\F{roll}^\ast_{#1}} +.. |unrolldt| mathdef:: \xref{valid/conventions}{aux-unroll-deftype}{\F{unroll}} +.. |expanddt| mathdef:: \xref{valid/conventions}{aux-expand-deftype}{\F{expand}} .. |packtype| mathdef:: \xref{syntax/types}{aux-packtype}{\F{pack}} .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}} @@ -383,7 +390,7 @@ .. Modules, non-terminals .. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}} -.. |type| mathdef:: \xref{syntax/types}{syntax-deftype}{\X{type}} +.. |type| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{type}} .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |local| mathdef:: \xref{syntax/modules}{syntax-local}{\X{local}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} @@ -1005,9 +1012,12 @@ .. |matchesresulttype| mathdef:: \xref{valid/matching}{match-resulttype}{\leq} .. |matchesinstrtype| mathdef:: \xref{valid/matching}{match-instrtype}{\leq} .. |matchesfunctype| mathdef:: \xref{valid/matching}{match-functype}{\leq} +.. |matchesfieldtype| mathdef:: \xref{valid/matching}{match-fieldtype}{\leq} +.. |matchesstoragetype| mathdef:: \xref{valid/matching}{match-storagetype}{\leq} +.. |matchespackedtype| mathdef:: \xref{valid/matching}{match-packedtype}{\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} +.. |matchescomptype| mathdef:: \xref{valid/matching}{match-comptype}{\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} @@ -1016,6 +1026,11 @@ .. |matcheslimits| mathdef:: \xref{valid/matching}{match-limits}{\leq} +.. Meta functions + +.. |clostype| mathdef:: \xref{valid/conventions}{closure}{\K{clos}} + + .. Contexts .. |CTYPES| mathdef:: \xref{valid/conventions}{context}{\K{types}} @@ -1029,6 +1044,7 @@ .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} .. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}} +.. |CRECS| mathdef:: \xref{valid/matching}{context-rec}{\K{rec}} .. Judgments @@ -1042,6 +1058,12 @@ .. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash} .. |vdashblocktype| mathdef:: \xref{valid/types}{valid-blocktype}{\vdash} .. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} +.. |vdashcomptype| mathdef:: \xref{valid/types}{valid-comptype}{\vdash} +.. |vdashfieldtype| mathdef:: \xref{valid/types}{valid-fieldtype}{\vdash} +.. |vdashpackedtype| mathdef:: \xref{valid/types}{valid-packedtype}{\vdash} +.. |vdashstoragetype| mathdef:: \xref{valid/types}{valid-storagetype}{\vdash} +.. |vdashsubtype| mathdef:: \xref{valid/types}{valid-subtype}{\vdash} +.. |vdashrectype| mathdef:: \xref{valid/types}{valid-rectype}{\vdash} .. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash} .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash} .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} @@ -1060,9 +1082,12 @@ .. |vdashresulttypematch| mathdef:: \xref{valid/matching}{match-resulttype}{\vdash} .. |vdashinstrtypematch| mathdef:: \xref{valid/matching}{match-instrtype}{\vdash} .. |vdashfunctypematch| mathdef:: \xref{valid/matching}{match-functype}{\vdash} +.. |vdashfieldtypematch| mathdef:: \xref{valid/matching}{match-fieldtype}{\vdash} +.. |vdashstoragetypematch| mathdef:: \xref{valid/matching}{match-storagetype}{\vdash} +.. |vdashpackedtypematch| mathdef:: \xref{valid/matching}{match-packedtype}{\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} +.. |vdashcomptypematch| mathdef:: \xref{valid/matching}{match-comptype}{\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} @@ -1110,6 +1135,7 @@ .. |insttype| mathdef:: \xref{exec/types}{type-inst}{\F{clos}} +.. |alloctype| mathdef:: \xref{exec/modules}{alloc-type}{\F{alloctype}} .. |allocfunc| mathdef:: \xref{exec/modules}{alloc-func}{\F{allocfunc}} .. |allochostfunc| mathdef:: \xref{exec/modules}{alloc-hostfunc}{\F{allochostfunc}} .. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 5d1767e53..54fb70490 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -24,6 +24,215 @@ That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the :ref:`appendix `. +.. index:: heap type, abstract type, concrete type, type index, ! recursive type index, ! closed type, rolling, unrolling, sub type, subtyping, ! bottom type + pair: abstract syntax; value type + pair: abstract syntax; heap type + pair: abstract syntax; sub type + pair: abstract syntax; recursive type index +.. _syntax-rectypeidx: +.. _syntax-valtype-ext: +.. _syntax-heaptype-ext: +.. _syntax-subtype-ext: +.. _type-closed: + +Types +~~~~~ + +To define the semantics, the definition of some sorts of types is extended to include additional forms. +By virtue of not being representable in either the :ref:`binary format ` or the :ref:`text format `, +these forms cannot be used in a program; +they only occur during :ref:`validation ` or :ref:`execution `. + +.. math:: + \begin{array}{llrl} + \production{value type} & \valtype &::=& + \dots ~|~ \BOT \\ + \production{abstract heap type} & \absheaptype &::=& + \dots ~|~ \BOTH \\ + \production{heap type} & \heaptype &::=& + \dots ~|~ \deftype ~|~ \REC~i \\ + \production{sub types} & \subtype &::=& + \TSUB~\TFINAL^?~\heaptype^\ast~\comptype \\ + \end{array} + +The unique :ref:`value type ` |BOT| is a *bottom type* that :ref:`matches ` all value types. +Similarly, |BOTH| is also used as a bottom type of all :ref:`heap types `. + +.. note:: + No validation rule uses bottom types explicitly, + but various rules can pick any value or heap type, including bottom. + This ensures the existence of :ref:`principal types `, + and thus a :ref:`validation algorithm ` without back tracking. + +A :ref:`concrete heap type ` can consist of a :ref:`defined type ` directly. +this occurs as the result of :ref:`substituting ` a :ref:`type index ` with its definition. + +A concrete heap type may also be a *recursive type index*. +Such an index refers to the :math:`i`-th component of a surrounding :ref:`recursive type `. +It occurs as the result of :ref:`rolling up ` the definition of a :ref:`recursive type `. + +Finally, the representation of supertypes in a :ref:`sub type ` is generalized from mere :ref:`type indices ` to :ref:`heap types `. +They occur as :ref:`defined types ` or :ref:`recursive type indices ` after :ref:`substituting ` type indices or :ref:`rolling up ` :ref:`recursive types `. + +A type of any form is *closed* when it does not contain a heap type that is a :ref:`type index ` or a recursive type index without a surrounding :ref:`recursive type `, +i.e., all :ref:`type indices ` have been :ref:`substituted ` with their :ref:`defined type ` and all free recursive type indices have been :ref:`unrolled `. + +.. note:: + Recursive type indices are internal to a recursive type. + They are distinguished from regular type indices and represented such that two closed types are syntactically equal if and only if they have the same recursive structure. + +.. _aux-reftypediff: + +Convention +.......... + +* The *difference* :math:`\X{rt}_1\reftypediff\X{rt}_2` between two :ref:`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 defnition only affects the presence of null and cannot express the absence of other values. + + +.. index:: ! defined type, recursive type + pair: abstract syntax; defined type +.. _syntax-deftype: + +Defined Types +~~~~~~~~~~~~~ + +*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. + +.. math:: + \begin{array}{llrl} + \production{defined type} & \deftype &::=& + \rectype.i \\ + \end{array} + +Defined types do not occur in the :ref:`binary ` or :ref:`text ` format, +but are formed by :ref:`rolling up ` the :ref:`recursive types ` defined in a module. + +It is hence an invariant of the semantics that all :ref:`recursive types ` occurring in defined types are :ref:`rolled up `. + + +.. index:: ! substitution +.. _type-subst: +.. _notation-subst: + +Conventions +........... + +* :math:`t[x^\ast \subst \X{dt}^\ast]` denotes the parallel *substitution* of :ref:`type indices ` :math:`x^\ast` with :ref:`defined types ` :math:`\X{dt}^\ast` in type :math:`t`, provided :math:`|x^\ast| = |\X{dt}^\ast|`. + +* :math:`t[(\REC~i)^\ast \subst \X{dt}^\ast]` denotes the parallel *substitution* of :ref:`recursive type indices ` :math:`(\REC~i)^\ast` with :ref:`defined types ` :math:`\X{dt}^\ast` in type :math:`t`, provided :math:`|(\REC~i)^\ast| = |\X{dt}^\ast|`. + +* :math:`t[\subst \X{dt}^\ast]` is shorthand for the substitution :math:`t[x^\ast \subst \X{dt}^\ast]`, where :math:`x^\ast = 0 \cdots (|\X{dt}^\ast| - 1)`. + + +.. index:: recursive type, defined type, sub type, ! rolling, ! unrolling, ! expansion, type equivalence +.. _aux-roll-rectype: +.. _aux-unroll-rectype: +.. _aux-roll-deftype: +.. _aux-unroll-deftype: +.. _aux-expand-deftype: + +Rolling and Unrolling +~~~~~~~~~~~~~~~~~~~~~ + +In order to allow comparing :ref:`recursive types ` for :ref:`equivalence `, their representation is changed such that all :ref:`type indices ` internal to the same recursive type are replaced by :ref:`recursive type indices `. + +.. note:: + This representation is independent of the type index space, + so that it is meaningful across module boundaries. + Moreover, this representation ensures that types with equivalent recursive structure are also syntactically equal, + hence allowing a simple equality check on (closed) types. + It gives rise to an *iso-recursive* interpretation of types. + +The representation change is performed by two auxiliary operations on the syntax of :ref:`recursive types `: + +* *Rolling up* a recursive type :ref:`substitutes ` its internal :ref:`type indices ` with corresponding :ref:`recursive type indices `. + +* *Unrolling* a recursive type :ref:`substitutes ` its :ref:`recursive type indices ` with the corresponding :ref:`defined types `. + +These operations are extended to :ref:`defined types ` and defined as follows: + +.. math:: + \begin{array}{@{}l@{~}l@{~}l@{~}r@{~}l@{}} + \rollrt{x}(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(x + i)^\ast \subst (\REC~i)^\ast])^\ast + & (\iff & i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\ + \unrollrt(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(\REC~i)^\ast \subst ((\TREC~\subtype^\ast).i)^\ast])^\ast + & (\iff & i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\[2ex] + \rolldt{x}(\rectype) &=& ((\TREC~\subtype^\ast).i)^\ast + & (\iff & i^\ast = 0 \cdots (|\subtype^\ast| - 1) \\ + &&& \land & \rollrt{x}(\rectype) = \TREC~\subtype^\ast) \\ + \unrolldt(\rectype.i) &=& \subtype^\ast[i] + & (\iff & \unrollrt(\rectype) = \TREC~\subtype^\ast) \\ + \end{array} + +In addition, the following auxiliary function denotes the *expansion* of a :ref:`defined type `: + +.. math:: + \begin{array}{@{}llll@{}} + \expanddt(\deftype) &=& \comptype & (\iff \unrolldt(\deftype) = \TSUB~\TFINAL^?~\X{ht}^?~\comptype) \\ + \end{array} + + +.. index:: ! instruction type, value type, result type, instruction, local, local index + pair: abstract syntax; instruction type + pair: instruction; type +.. _syntax-instrtype: + +Instruction Types +~~~~~~~~~~~~~~~~~ + +*Instruction types* classify the behaviour of :ref:`instructions ` or instruction sequences, by describing how they manipulate the :ref:`operand stack ` and the initialization status of :ref:`locals `: + +.. math:: + \begin{array}{llrl} + \production{instruction type} & \instrtype &::=& + \resulttype \toX{\localidx^\ast} \resulttype \\ + \end{array} + +An instruction type :math:`[t_1^\ast] \toX{x^\ast} [t_2^\ast]` describes the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off +and the provided output stack with result values of types :math:`t_2^\ast` that it pushes back. +Moreover, it enumerates the :ref:`indices ` :math:`x^\ast` of locals that have been set by the instruction or sequence. + +.. note:: + Instruction types are only used for :ref:`validation `, + they do not occur in programs. + + +.. index:: ! local type, value type, local, local index + pair: abstract syntax; local type + pair: local; type +.. _syntax-init: +.. _syntax-localtype: + +Local Types +~~~~~~~~~~~ + +*Local types* classify :ref:`locals `, by describing their :ref:`value type ` as well as their *initialization status*: + +.. math:: + \begin{array}{llrl} + \production{initialization status} & \init &::=& + \SET ~|~ \UNSET \\ + \production{local type} & \localtype &::=& + \init~\valtype \\ + \end{array} + +.. note:: + Local types are only used for :ref:`validation `, + they do not occur in programs. + + .. index:: ! context, local type, function type, table type, memory type, global type, value type, result type, index space, module, function, local type .. _context: @@ -84,6 +293,24 @@ In addition to field access written :math:`C.\K{field}` the following notation i Accordingly, the notation is defined to append at the *front* of the respective sequence, introducing a new relative index :math:`0` and shifting the existing ones. +.. index:: ! type closure +.. _type-closure: + +Convention +.......... + +.. todo:: move this elsewhere? + +Any form of :ref:`type ` can be *closed* to bring it into :ref:`closed ` form relative to a :ref:`context ` it is :ref:`valid ` in by :ref:`substituting ` each :ref:`type index ` :math:`x` occurring in it with the corresponding :ref:`defined type ` :math:`C.\CTYPES[x]`, after first closing the the types in :math:`C.\CTYPES` themselves. + +.. math:: + \begin{array}{@{}lcll@{}} + \clostype_C(t) &=& t[\subst clostype^\ast(C.\CTYPES)] \\[2ex] + \clostype^\ast(\epsilon) &=& \epsilon \\ + \clostype^\ast(\X{dt}^\ast~\X{dt}_N) &=& {\X{dt}'}^\ast~\X{dt}_N[\subst {\X{dt}'}^\ast] & (\iff {\X{dt}'}^\ast = \clostype^\ast(\X{dt}^\ast)) \\ + \end{array} + + .. _valid-notation-textual: Prose Notation diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f60adc76f..a822dd149 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -294,7 +294,7 @@ Aggregate Reference Instructions * 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`. +* 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`: @@ -308,7 +308,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TSTRUCT~(\mut~\X{st})^\ast + \expanddt(C.\CTYPES[x]) = \TSTRUCT~(\mut~\X{st})^\ast }{ C \vdashinstr \STRUCTNEW~x : [(\unpacktype(\X{st}))^\ast] \to [(\REF~x)] } @@ -320,7 +320,7 @@ Aggregate Reference Instructions * 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`. +* 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`: @@ -336,7 +336,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TSTRUCT~(\mut~\X{st})^\ast + \expanddt(C.\CTYPES[x]) = \TSTRUCT~(\mut~\X{st})^\ast \qquad (C \vdashvaltypedefaultable \unpacktype(\X{st}) \defaultable)^\ast }{ @@ -352,7 +352,7 @@ Aggregate Reference Instructions * 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`. +* 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]`. @@ -364,7 +364,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast + \expanddt(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast \qquad \X{ft}^\ast[i] = \mut~\X{st} \qquad @@ -380,7 +380,7 @@ Aggregate Reference Instructions * 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`. +* 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]`. @@ -392,7 +392,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast + \expanddt(C.\CTYPES[x]) = \TSTRUCT~\X{ft}^\ast \qquad \X{ft}^\ast[i] = \MVAR~\X{st} }{ @@ -407,7 +407,7 @@ Aggregate Reference Instructions * 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`. +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. * Let :math:`\fieldtype` be :math:`\mut~\storagetype`. @@ -417,7 +417,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) }{ C \vdashinstr \ARRAYNEW~x : [\unpacktype(\X{st})~\I32] \to [(\REF~x)] } @@ -429,7 +429,7 @@ Aggregate Reference Instructions * 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`. +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. * Let :math:`\fieldtype` be :math:`\mut~\storagetype`. @@ -441,7 +441,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) \qquad C \vdashvaltypedefaultable \unpacktype(\X{st}) \defaultable }{ @@ -455,7 +455,7 @@ Aggregate Reference Instructions * 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`. +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. * Let :math:`\fieldtype` be :math:`\mut~\storagetype`. @@ -465,7 +465,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) }{ C \vdashinstr \ARRAYNEWFIXED~x~n : [\unpacktype(\X{st})^n] \to [(\REF~x)] } @@ -477,7 +477,7 @@ Aggregate Reference Instructions * 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`. +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. * Let :math:`\fieldtype` be :math:`\mut~\storagetype`. @@ -493,7 +493,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{rt}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{rt}) \qquad C \vdashreftypematch C.\CELEMS[y] \matchesreftype \X{rt} }{ @@ -508,7 +508,7 @@ Aggregate Reference Instructions * 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`. +* The :ref:`expansion ` of :math:`C.\CTYPES[x]` must be an :ref:`array type ` :math:`\TARRAY~\fieldtype`. * Let :math:`\fieldtype` be :math:`\mut~\storagetype`. @@ -522,7 +522,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) \qquad \unpacktype(\X{st}) = \numtype \lor \unpacktype(\X{st}) = \vectype \qquad @@ -541,7 +541,7 @@ Aggregate Reference Instructions * 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`. +* 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`. @@ -553,7 +553,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) \qquad \sx = \epsilon \Leftrightarrow \X{st} = \unpacktype(\X{st}) }{ @@ -567,7 +567,7 @@ Aggregate Reference Instructions * 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`. +* 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`. @@ -579,7 +579,7 @@ Aggregate Reference Instructions .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TARRAY~(\MVAR~\X{st}) + \expanddt(C.\CTYPES[x]) = \TARRAY~(\MVAR~\X{st}) }{ C \vdashinstr \ARRAYSET~x : [(\REF~\NULL~x)~\I32~\unpacktype(\X{st})] \to [] } diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index e6fededdb..b8ddbe56a 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -1,11 +1,11 @@ -.. index:: ! matching, ! subtyping +.. index:: ! matching, ! subtyping .. _subtyping: .. _match: Matching -------- -On most types, a simple notion of *subtyping* is defined that is applicable in validation rules or during :ref:`module instantiation ` when checking the types of imports. +On most types, a notion of *subtyping* is defined that is applicable in :ref:`validation ` rules, during :ref:`module instantiation ` when checking the types of imports, or during :ref:`execution `, when performing casts. .. index:: number type @@ -44,7 +44,7 @@ A :ref:`vector type ` :math:`\vectype_1` matches a :ref:`vector } -.. index:: heap type +.. index:: heap type, defined type, structure type, array type, function type, unboxed scalar type .. _match-heaptype: Heap Types @@ -54,13 +54,31 @@ A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap ty * Either both :math:`\heaptype_1` and :math:`\heaptype_2` are the same. -* Or :math:`\heaptype_1` is a :ref:`function type ` and :math:`\heaptype_2` is :math:`FUNC`. +* Or there exists a :ref:`valid ` :ref:`heap type ` :math:`\heaptype'`, such that :math:`\heaptype_1` :ref:`matches ` :math:`\heaptype'` and :math:`\heaptype'` :ref:`matches ` :math:`\heaptype_2`. -* Or :math:`\heaptype_1` is a :ref:`function type ` :math:`\functype_1` and :math:`\heaptype_2` is a :ref:`function type ` :math:`\functype_2`, and :math:`\functype_1` :ref:`matches ` :math:`\functype_2`. +* Or :math:`heaptype_1` is :math:`\EQT` and :math:`\heaptype_2` is :math:`\ANY`. -* Or :math:`\heaptype_1` is a :ref:`type index ` :math:`x_1`, and :math:`C.\CTYPES[x_1]` :ref:`matches ` :math:`\heaptype_2`. +* Or :math:`\heaptype_1` is one of :math:`\I31`, :math:`\STRUCT`, or :math:`\ARRAY` and :math:`heaptype_2` is :math:`\EQT`. -* Or :math:`\heaptype_2` is a :ref:`type index ` :math:`x_2`, and :math:`\heaptype_1` :ref:`matches ` :math:`C.\CTYPES[x_2]`. +* Or :math:`\heaptype_1` is a :ref:`defined type ` which :ref:`expands ` to a :ref:`structure type ` and :math:`\heaptype_2` is :math:`\STRUCT`. + +* Or :math:`\heaptype_1` is a :ref:`defined type ` which :ref:`expands ` to an :ref:`array type ` and :math:`\heaptype_2` is :math:`\ARRAY`. + +* Or :math:`\heaptype_1` is a :ref:`defined type ` which :ref:`expands ` to a :ref:`function type ` and :math:`\heaptype_2` is :math:`\FUNC`. + +* Or :math:`\heaptype_1` is a :ref:`defined type ` :math:`\deftype_1` and :math:`\heaptype_2` is a :ref:`defined type ` :math:`\deftype_2`, and :math:`\deftype_1` :ref:`matches ` :math:`\deftype_2`. + +* Or :math:`\heaptype_1` is a :ref:`type index ` :math:`x_1`, and the :ref:`defined type ` :math:`C.\CTYPES[x_1]` :ref:`matches ` :math:`\heaptype_2`. + +* Or :math:`\heaptype_2` is a :ref:`type index ` :math:`x_2`, and :math:`\heaptype_1` :ref:`matches ` the :ref:`defined type ` :math:`C.\CTYPES[x_2]`. + +* Or :math:`\heaptype_1` is :math:`\NONE` and :math:`\heaptype_2` :ref:`matches ` :math:`\ANY`. + +* Or :math:`\heaptype_1` is :math:`\NOFUNC` and :math:`\heaptype_2` :ref:`matches ` :math:`\FUNC`. + +* Or :math:`\heaptype_1` is :math:`\NOEXTERN` and :math:`\heaptype_2` :ref:`matches ` :math:`\EXTERN`. + +* Or :math:`\heaptype_1` is :math:`\BOTH`. .. math:: ~\\[-1ex] @@ -70,16 +88,55 @@ A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap ty } \qquad \frac{ + C \vdashheaptype \heaptype' \ok + \qquad + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype' + \qquad + C \vdashheaptypematch \heaptype' \matchesheaptype \heaptype_2 }{ - C \vdashheaptypematch \functype \matchesheaptype \FUNC + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 } .. math:: ~\\[-1ex] \frac{ - C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2 }{ - C \vdashheaptypematch \functype_1 \matchesheaptype \functype_2 + C \vdashheaptypematch \EQT \matchesheaptype \ANY + } + \qquad + \frac{ + }{ + C \vdashheaptypematch \I31 \matchesheaptype \EQT + } + \qquad + \frac{ + }{ + C \vdashheaptypematch \STRUCT \matchesheaptype \EQT + } + \qquad + \frac{ + }{ + C \vdashheaptypematch \ARRAY \matchesheaptype \EQT + } + +.. math:: + ~\\[-1ex] + \frac{ + \expanddt(\deftype) = \TSTRUCT~\X{st} + }{ + C \vdashheaptypematch \deftype \matchesheaptype \FUNC + } + \qquad + \frac{ + \expanddt(\deftype) = \TARRAY~\X{at} + }{ + C \vdashheaptypematch \deftype \matchesheaptype \ARRAY + } + \qquad + \frac{ + \expanddt(\deftype) = \TFUNC~\X{ft} + }{ + C \vdashheaptypematch \deftype \matchesheaptype \FUNC } .. math:: @@ -96,6 +153,33 @@ A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap ty C \vdashheaptypematch \heaptype_1 \matchesheaptype \typeidx_2 } +.. math:: + ~\\[-1ex] + \frac{ + C \vdashheaptypematch \X{ht} \matchesheaptype \ANY + }{ + C \vdashheaptypematch \NONE \matchesheaptype \X{ht} + } + \qquad + \frac{ + C \vdashheaptypematch \X{ht} \matchesheaptype \FUNC + }{ + C \vdashheaptypematch \NOFUNC \matchesheaptype \X{ht} + } + \qquad + \frac{ + C \vdashheaptypematch \X{ht} \matchesheaptype \EXTERN + }{ + C \vdashheaptypematch \NOEXTERN \matchesheaptype \X{ht} + } + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashheaptypematch \BOTH \matchesheaptype \heaptype + } + .. index:: reference type @@ -214,32 +298,160 @@ An :ref:`instruction type ` :math:`[t_{11}^\ast] \toX{x_1^\ast Function Types ~~~~~~~~~~~~~~ -Subtyping is also defined for :ref:`function types `. -However, it is required that they match in both directions, effectively demanding type equivalence. -That is, a :ref:`function type ` :math:`[t_{11}^\ast] \toF [t_{12}^\ast]` matches a type :math:`[t_{21}^ast] \toF [t_{22}^\ast]` if and only if: +A :ref:`function type ` :math:`[t_{11}^\ast] \toF [t_{12}^\ast]` matches a type :math:`[t_{21}^ast] \toF [t_{22}^\ast]` if and only if: -* The :ref:`result type ` :math:`[t_{11}^\ast]` :ref:`matches ` :math:`[t_{21}^\ast]`, and vice versa. +* The :ref:`result type ` :math:`[t_{21}^\ast]` :ref:`matches ` :math:`[t_{11}^\ast]`. -* The :ref:`result type ` :math:`[t_{12}^\ast]` :ref:`matches ` :math:`[t_{22}^\ast]`, and vice versa. +* The :ref:`result type ` :math:`[t_{12}^\ast]` :ref:`matches ` :math:`[t_{22}^\ast]`. .. math:: ~\\[-1ex] \frac{ - \begin{array}{@{}c@{}} - C \vdashresulttypematch [t_{11}^\ast] \matchesresulttype [t_{21}^\ast] + C \vdashresulttypematch [t_{21}^\ast] \matchesresulttype [t_{11}^\ast] \qquad C \vdashresulttypematch [t_{12}^\ast] \matchesresulttype [t_{22}^\ast] + }{ + C \vdashfunctypematch [t_{11}^\ast] \toF [t_{12}^\ast] \matchesfunctype [t_{21}^\ast] \toF [t_{22}^\ast] + } + + +.. index:: compound types, aggregate type, structure type, array type, field type +.. _match-comptype: +.. _match-structtype: +.. _match-arraytype: + +Compound Types +~~~~~~~~~~~~~~ + +A :ref:`compound type ` :math:`\comptype_1` matches a type :math:`\comptype_2` if and only if: + +* Either the compound type :math:`\comptype_1` is :math:`\TFUNC~\functype_1` and :math:`\comptype_2` is :math:`\TFUNC~\functype_2` and: + + * The :ref:`function type ` :math:`\functype_1` :ref:`matches ` :math:`\functype_2`. + +* Or the compound type :math:`\comptype_1` is :math:`\TSTRUCT~\fieldtype_1^{n_1}` and :math:`\comptype_2` is :math:`\TSTRUCT~\fieldtype_2` and: + + * The arity :math:`n_1` is greater than or equal to :math:`n_2`. + + * For every :ref:`field type ` :math:`\fieldtype_{2i}` in :math:`\fieldtype_2^{n_2}` and corresponding :math:`\fieldtype_{1i}` in :math:`\fieldtype_1^{n_1}` + + * The :ref:`field type ` :math:`\fieldtype_{1i}` :ref:`matches ` :math:`\fieldtype_{2i}`. + +* Or the compound type :math:`\comptype_1` is :math:`\TARRAY~\fieldtype_1` and :math:`\comptype_2` is :math:`\TARRAY~\fieldtype_2` and: + + * The :ref:`field type ` :math:`\fieldtype_1` :ref:`matches ` :math:`\fieldtype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2 + }{ + C \vdashcomptypematch \TFUNC~\functype_1 \matchescomptype \TFUNC~\functype_2 + } + +.. math:: + ~\\[-1ex] + \frac{ + (C \vdashfieldtypematch \fieldtype_1 \matchesfieldtype \fieldtype_2)^\ast + }{ + C \vdashcomptypematch \TSTRUCT~\fieldtype_1^\ast~{\fieldtype'}_1^\ast \matchescomptype \TSTRUCT~\fieldtype_2^\ast + } + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashfieldtypematch \fieldtype_1 \matchesfieldtype \fieldtype_2 + }{ + C \vdashcomptypematch \TARRAY~\fieldtype_1 \matchescomptype \TARRAY~\fieldtype_2 + } + + +.. index:: field type, storage type, value type, packed type, mutability +.. _match-fieldtype: +.. _match-storagetype: +.. _match-packedtype: + +Field Types +~~~~~~~~~~~ + +A :ref:`field type ` :math:`\mut_1~\storagetype_1` matches a type :math:`\mut_2~\storagetype_2` if and only if: + +* :ref:`Storage type ` :math:`\storagetype_1` :ref:`matches ` :math:`\storagetype_2`. + +* Either both :math:`\mut_1` and :math:`\mut_2` are :math:`\MCONST`. + +* Or both :math:`\mut_1` and :math:`\mut_2` are :math:`\MVAR` and :math:`\storagetype_2` :ref:`matches ` :math:`\storagetype_1` as well. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2 + }{ + C \vdashfieldtypematch \MCONST~\storagetype_1 \matchescomptype \MCONST~\storagetype_2 + } + \qquad + \frac{ + \begin{array}[b]{@{}c@{}} + C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2 \\ - C \vdashresulttypematch [t_{21}^\ast] \matchesresulttype [t_{11}^\ast] - \qquad - C \vdashresulttypematch [t_{22}^\ast] \matchesresulttype [t_{12}^\ast] + C \vdashstoragetypematch \storagetype_2 \matchesstoragetype \storagetype_1 \end{array} }{ - C \vdashfunctypematch [t_{11}^\ast] \toF [t_{12}^\ast] \matchesfunctype [t_{21}^\ast] \toF [t_{22}^\ast] + C \vdashfieldtypematch \MVAR~\storagetype_1 \matchescomptype \MVAR~\storagetype_2 } -.. note:: - In future versions of WebAssembly, subtyping on function types may be relaxed to support co- and contra-variance. +A :ref:`storage type ` :math:`\storagetype_1` matches a type :math:`\storagetype_2` if and only if: + +* Either :math:`\storagetype_1` is a :ref:`value type ` :math:`\valtype_1` and :math:`\storagetype_2` is a :ref:`value type ` :math:`\valtype_2` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + +* Or :math:`\storagetype_1` is a :ref:`packed type ` :math:`\packedtype_1` and :math:`\storagetype_2` is a :ref:`packed type ` :math:`\packedtype_2` and :math:`\packedtype_1` :ref:`matches ` :math:`\packedtype_2`. + +A :ref:`packed type ` :math:`\packedtype_1` matches a type :math:`\packedtype_2` if and only if: + +* The :ref:`packed type ` :math:`\packedtype_1` is the same as :math:`\packedtype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashpackedtypematch \packedtype \matchespackedtype \packedtype + } + + +.. index:: defined type, recursive type, unroll, type equivalence + pair: abstract syntax; defined type +.. _match-deftype: + +Defined Types +~~~~~~~~~~~~~ + +A :ref:`defined type ` :math:`\deftype_1` matches a type :math:`\deftype_2` if and only if: + +* Either :math:`\deftype_1` and :math:`\deftype_2` are equal when :ref:`closed ` under context :math:`C`. + +* Or: + + * Let the :ref:`sub type ` :math:`\TSUB~\TFINAL^?~\heaptype^\ast~\comptype` be the result of :ref:`unrolling ` :math:`\deftype_1`. + + * Then there must exist a :ref:`heap type ` :math:`\heaptype_i` in :math:`\heaptype^\ast` that :ref:`matches ` :math:`\deftype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + \clostype_C(\deftype_1) = \clostype_C(\deftype_2) + }{ + C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2 + } + +.. math:: + ~\\[-1ex] + \frac{ + \unrolldt(\deftype_1) = \TSUB~\TFINAL^?~\heaptype^\ast~\comptype + \qquad + C \vdashheaptypematch \heaptype^\ast[i] \matchesheaptype \deftype_2 + }{ + C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2 + } .. index:: limits diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 0f835f3f8..89d1c54d3 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -5,6 +5,62 @@ Modules Furthermore, most definitions are themselves classified with a suitable type. +.. index:: type, type index, defined type, recursive type + pair: abstract syntax; type + single: abstract syntax; type +.. _valid-types: + +Types +~~~~~ + +The sequence of :ref:`types ` defined in a module is validated incrementally, yielding a suitable :ref:`context `. + +:math:`\type^\ast` +.................. + +* If the sequence is empty, then: + + * The :ref:`context ` :math:`C` must be empty. + + * Then the type sequence is valid. + +* Otherwise: + + * Let the :ref:`recursive type ` :math:`\rectype` be the last element in the sequence. + + * The sequence without :math:`\rectype` must be valid for some context :math:`C'`. + + * Let the :ref:`type index ` :math:`x` be the length of :math:`C'.\CTYPES`, i.e., the first type index free in :math:`C'`. + + * Let the sequence of :ref:`defined types ` :math:`\deftype^\ast` be the result :math:`\rolldt{x}(\rectype)` of :ref:`rolling up ` into its sequence of :ref:`defined types `. + + * The :ref:`recursive type ` :math:`\rectype` must be :ref:`valid ` under the context :math:`C` for :ref:`type index ` :math:`x`. + + * The current :ref:`context ` :math:`C` be the same as :math:`C'`, but with :math:`\deftype^\ast` appended to |CTYPES|. + + * Then the type sequence is valid. + +.. math:: + \frac{ + }{ + \{\} \vdashtypes \epsilon \ok + } + +.. math:: + \frac{ + C' \vdashtypes \type^\ast \ok + \qquad + C = C' \with \CTYPES = C'.\CTYPES~\rolldt{|C'.\CTYPES|}(\rectype) + \qquad + C \vdashrectype \rectype ~{\ok}(|C'.\CTYPES|) + }{ + C \vdashtypes \type^\ast~\rectype \ok + } + +.. note:: + Despite the appearance, the context :math:`C` is effectively an _output_ of this judgement. + + .. index:: function, local, function index, local index, type index, function type, value type, local type, expression, import pair: abstract syntax; function single: abstract syntax; function @@ -22,7 +78,7 @@ Functions :math:`\func` are classified by :ref:`type indices ` r * The :ref:`defined type ` :math:`C.\CTYPES[x]` must be a :ref:`function type `. -* Let :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]` be the :ref:`expansion ` of the :ref:`defined 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 +102,7 @@ Functions :math:`\func` are classified by :ref:`type indices ` r .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] + \expanddt(C.\CTYPES[x]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] \qquad (C \vdashlocal t : \init~t)^\ast \qquad @@ -515,7 +571,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \expand(C.\CTYPES[x]) = \TFUNC~\functype + \expanddt(C.\CTYPES[x]) = \TFUNC~\functype }{ C \vdashimportdesc \IDFUNC~x : \ETFUNC~C.\CTYPES[x] } @@ -586,11 +642,11 @@ The :ref:`external types ` classifying a module may contain f * Let :math:`\module` be the module to validate. -* Let :math:`C` be a :ref:`context ` where: +* The :ref:`types ` :math:`\module.\MTYPES` must be :ref:`valid ` yielding a :ref:`context ` :math:`C_0`. - * .. todo:: Adjust type context +* Let :math:`C` be a :ref:`context ` where: - * :math:`C.\CTYPES` is :math:`\module.\MTYPES`, + * :math:`C.\CTYPES` is :math:`C_0.\CTYPES`, * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`, with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :ref:`function types ` :math:`\X{ft}^\ast` as determined below, @@ -616,14 +672,6 @@ 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 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 recursive type :math:`\rectype_i` must be :ref:`valid ` under context :math:`C_i`. - * Let :math:`C'` be the :ref:`context ` where: * :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`, @@ -690,7 +738,7 @@ The :ref:`external types ` classifying a module may contain f .. math:: \frac{ \begin{array}{@{}c@{}} - \vdashtypes \type^\ast \ok + C_0 \vdashtypes \type^\ast \ok \quad (C \vdashfunc \func : \X{ft})^\ast \quad @@ -720,7 +768,7 @@ The :ref:`external types ` classifying a module may contain f \\ x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon) \\ - C = \{ \CTYPES~\type^\ast, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} + C = \{ \CTYPES~C_0.\CTYPES, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \} \\ C' = \{ \CTYPES~\type^\ast, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} \qquad @@ -746,27 +794,8 @@ The :ref:`external types ` classifying a module may contain f \vdashmodule \module : \X{it}^\ast \to \X{et}^\ast } -.. _valid-types: - -where: - -.. math:: - \frac{ - \vdashtypes \type^\ast \ok - \qquad - \{\CTYPES~\type^\ast\} \vdashtypes \type \ok - }{ - \vdashtypes \type^\ast~\type \ok - } - \qquad - \frac{ - }{ - \vdashtypes \epsilon \ok - } - - .. note:: - Most definitions in a module -- particularly functions -- are mutually recursive. + All functions in a module are mutually recursive. Consequently, the definition of the :ref:`context ` :math:`C` in this rule is recursive: it depends on the outcome of validation of the function, table, memory, and global definitions contained in the module, which itself depends on :math:`C`. diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 04492b4ab..63cf0e465 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -53,26 +53,15 @@ Heap Types Concrete :ref:`Heap types ` are only valid when the :ref:`type index ` is. -:math:`\FUNC` -............. - -* The heap type is valid. - -.. math:: - \frac{ - }{ - C \vdashheaptype \FUNC \ok - } - -:math:`\EXTERN` -............... +:math:`\absheaptype` +.................... * The heap type is valid. .. math:: \frac{ }{ - C \vdashheaptype \EXTERN \ok + C \vdashheaptype \absheaptype \ok } :math:`\typeidx` @@ -89,17 +78,18 @@ Concrete :ref:`Heap types ` are only valid when the :ref:`type C \vdashheaptype \typeidx \ok } -:math:`\BOT` -............ +:math:`\BOTH` +............. * The heap type is valid. .. math:: \frac{ }{ - C \vdashheaptype \BOT \ok + C \vdashheaptype \BOTH \ok } + .. index:: reference type, heap type pair: validation; reference type single: abstract syntax; reference type @@ -129,12 +119,12 @@ Reference Types pair: validation; value type single: abstract syntax; value type .. _valid-valtype: -.. _valid-bottype: +.. _valid-valtype-bot: Value Types ~~~~~~~~~~~ -Valid :ref:`value types ` are either valid :ref:`number type `, :ref:`reference type `, or the :ref:`bottom type `. +Valid :ref:`value types ` are either valid :ref:`number type `, :ref:`reference type `, or the :ref:`bottom type `. :math:`\BOT` ............ @@ -169,7 +159,7 @@ Block Types .. math:: \frac{ - \expand(C.\CTYPES[\typeidx]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] + \expanddt(C.\CTYPES[\typeidx]) = \TFUNC~[t_1^\ast] \toF [t_2^\ast] }{ C \vdashblocktype \typeidx : [t_1^\ast] \to [t_2^\ast] } @@ -248,7 +238,6 @@ Instruction Types pair: validation; function type single: abstract syntax; function type .. _valid-functype: -.. _valid-deftype: Function Types ~~~~~~~~~~~~~~ @@ -272,6 +261,227 @@ Function Types } +.. index:: compound type, function type, aggregate type, structure type, array type, field type + pair: validation; compound type + pair: validation; aggregate type + pair: validation; structure type + pair: validation; array type + single: abstract syntax; compound type + single: abstract syntax; function type + single: abstract syntax; structure type + single: abstract syntax; array type + single: abstract syntax; field type +.. _valid-comptype: +.. _valid-aggrtype: +.. _valid-structtype: +.. _valid-arraytype: + +Compound Types +~~~~~~~~~~~~~~ + +:math:`\TFUNC~\functype` +........................ + +* The :ref:`function type ` :math:`\functype` must be :ref:`valid `. + +* Then the compound type is valid. + +.. math:: + \frac{ + C \vdashfunctype \functype \ok + }{ + C \vdashcomptype \TFUNC~\functype \ok + } + +:math:`\TSTRUCT~\fieldtype^\ast` +................................ + +* For each :ref:`field type ` :math:`\fieldtype_i` in :math:`\fieldtype^\ast`: + + * The :ref:`field type ` :math:`\fieldtype_i` must be :ref:`valid `. + +* Then the compound type is valid. + +.. math:: + \frac{ + (C \vdashfieldtype \X{ft} \ok)^\ast + }{ + C \vdashcomptype \TSTRUCT~\X{ft}^\ast \ok + } + +:math:`\TARRAY~\fieldtype` +.......................... + +* The :ref:`field type ` :math:`\fieldtype` must be :ref:`valid `. + +* Then the compound type is valid. + +.. math:: + \frac{ + C \vdashfieldtype \X{ft} \ok + }{ + C \vdashcomptype \TARRAY~\X{ft} \ok + } + + +.. index:: field type, storage type, packed type, value type, mutability + pair: validation; field type + pair: validation; storage type + pair: validation; packed type + single: abstract syntax; field type + single: abstract syntax; storage type + single: abstract syntax; packed type + single: abstract syntax; value type +.. _valid-fieldtype: +.. _valid-storagetype: +.. _valid-packedtype: + +Field Types +~~~~~~~~~~~ + +:math:`\mut~\storagetype` +......................... + +* The :ref:`storage type ` :math:`\storagetype` must be :ref:`valid `. + +* Then the field type is valid. + +.. math:: + \frac{ + C \vdashstoragetype \X{st} \ok + }{ + C \vdashfieldtype \mut~\X{st} \ok + } + +:math:`\packedtype` +................... + +* The packed type is valid. + +.. math:: + \frac{ + }{ + C \vdashpackedtype \packedtype \ok + } + + +.. index:: recursive type, sub type, compound type, final, subtyping + pair: abstract syntax; recursive type + pair: abstract syntax; sub type +.. _valid-rectype: +.. _valid-subtype: + +Recursive Types +~~~~~~~~~~~~~~~ + +:ref:`Recursive types ` are validated for a specific :ref:`type index ` that denotes the index of the type defined by the recursive group. + +:math:`\TREC~\subtype^\ast` +........................... + +.. todo:: add version of this for extended type syntax to appendix + +* Either the sequence :math:`\subtype^\ast` is empty. + +* Or: + + * The first :ref:`sub type ` of the sequence :math:`\subtype^\ast` must be :ref:`valid ` for the :ref:`type index ` :math:`x`. + + * The remaining sequence :math:`\subtype^\ast` must be :ref:`valid ` for the :ref:`type index ` :math:`x + 1`. + +* Then the recursive type is valid for the :ref:`type index ` :math:`x`. + +.. math:: + \frac{ + }{ + C \vdashrectype \TREC~\epsilon ~{\ok}(x) + } + \qquad + \frac{ + C \vdashsubtype \subtype ~{\ok}(x) + \qquad + C \vdashrectype \TREC~{\subtype'}^\ast ~{\ok}(x + 1) + }{ + C \vdashrectype \TREC~\subtype~{\subtype'}^\ast ~{\ok}(x) + } + +:math:`\TSUB~\TFINAL^?~y^\ast~\comptype` +........................................ + +* The :ref:`compound type ` :math:`\comptype` must be :ref:`valid `. + +* The sequence :math:`y^\ast` may be no longer than :math:`1`. + +* For every :ref:`type index ` :math:`y_i` in :math:`y^\ast`: + + * The :ref:`type index ` :math:`y_i` must be smaller than :math:`x`. + + * The :ref:`type index ` :math:`y_i` must exist in the context :math:`C`. + + * Let :math:`\subtype_i` be the :ref:`unrolling ` of the :ref:`defined type ` :math:`C.\CTYPES[y_i]`. + + * The :ref:`sub type ` :math:`\subtype_i` must not contain :math:`\TFINAL`. + + * Let :math:`\comptype'_i` be the :ref:`expansion ` of the :ref:`defined type ` :math:`C.\CTYPES[y_i]`. + + * The :ref:`compound type ` :math:`\comptype` must :ref:`match ` :math:`\comptype'_i`. + +* Then the sub type is valid for the :ref:`type index ` :math:`x`. + +.. math:: + \frac{ + \begin{array}{@{}c@{}} + |y^\ast| \leq 1 + \qquad + (y < x)^\ast + \qquad + (\unrolldt(C.\CTYPES[y]) = \TSUB~{y'}^\ast~\comptype')^\ast + \\ + C \vdashcomptype \comptype \ok + \qquad + (C \vdashcomptypematch \comptype \matchescomptype \comptype')^\ast + \end{array} + }{ + C \vdashsubtype \TSUB~\TFINAL^?~y^\ast~\comptype ~{\ok}(x) + } + +.. note:: + The side condition on the index ensures that a declared supertype is a previously defined types, + preventing cyclic subtype hierarchies. + + Future versions of WebAssembly may allow more than one supertype. + + +.. index:: defined type, recursive type, unroll, expand + pair: abstract syntax; defined type +.. _valid-deftype: + +Defined Types +~~~~~~~~~~~~~ + +:math:`\rectype.i` +.................. + +* The :ref:`recursive type ` :math:`\rectype` must be :ref:`valid ` for some :ref:`type index ` :math:`x`. + +* Let :math:`\TREC~\subtype^\ast` be the :ref:`defined type ` :math:`\rectype`. + +* The number :math:`i` must be smaller than the length of the sequence :math:`\subtype^\ast` of :ref:`sub types `. + +* Then the defined type is valid. + +.. math:: + \frac{ + C \vdashrectype \rectype ~{\ok}(x) + \qquad + \rectype = \TREC~\subtype^n + \qquad + i < n + }{ + C \vdashdeftype \rectype.i \ok + } + + .. index:: limits pair: validation; limits single: abstract syntax; limits @@ -401,7 +611,7 @@ External Types \frac{ C \vdashdeftype \deftype \ok \qquad - \expand(\deftype) = \TFUNC~\functype + \expanddt(\deftype) = \TFUNC~\functype }{ C \vdashexterntype \ETFUNC~\deftype }