From 746b0c63e80e1f34c3b7ce74cd4fabb4fee909e5 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 23 May 2023 10:18:59 +0200 Subject: [PATCH 1/9] WIP --- document/core/exec/instructions.rst | 4 +- document/core/exec/modules.rst | 2 +- document/core/exec/types.rst | 3 + document/core/syntax/types.rst | 177 ++----------- document/core/util/macros.def | 41 +-- document/core/valid/conventions.rst | 195 +++++++++++++++ document/core/valid/matching.rst | 374 ++++++++++++++++++++++++++-- document/core/valid/modules.rst | 75 ++++-- document/core/valid/types.rst | 262 +++++++++++++++++-- 9 files changed, 905 insertions(+), 228 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 050fba593..c6b6d1b7f 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3635,7 +3635,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:`\expand(\X{f}.\FITYPE)`. 4. Let :math:`\local^\ast` be the list of :ref:`locals ` :math:`f.\FICODE.\FLOCALS`. @@ -3679,7 +3679,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:`\expand(S.\SFUNCS[a].\FITYPE)`. 3. Assert: due to :ref:`validation `, there are at least :math:`n` values on the top of the stack. diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 9528446b6..8ce92e9df 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -665,7 +665,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:`\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: 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/syntax/types.rst b/document/core/syntax/types.rst index 6983ad3a7..8cbbcae2f 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -73,9 +73,8 @@ Conventions -.. 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: @@ -97,11 +96,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} & \abdheaptype &::=& \FUNC ~|~ \NOFUNC \\&&|& \EXTERN ~|~ \NOEXTERN \\&&|& \ANY ~|~ \EQT ~|~ \I31 ~|~ \STRUCT ~|~ \ARRAY ~|~ \NONE \\&&|& - \typeidx ~|~ \deftype ~|~ \BOT \\ + \production{heap type} & \heaptype &::=& + \absheaptype ~|~ \typeidx \\ \end{array} A heap type is either *abstract* or *concrete*. @@ -132,34 +132,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 +166,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 defnition 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 ` and :ref:`execution `. + Conventions ........... @@ -252,55 +210,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,7 +225,7 @@ 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 &::=& + \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 +291,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 \\ - \end{array} - - -.. 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 \\ + \TSUB~\TFINAL^?~\typeidx^\ast~\comptype \\ \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: +In a :ref:`module `, each member of a recursive type is assigned a separate :ref:`type index `. - .. 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 2e113e91d..159da65ba 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}} @@ -221,9 +222,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{filan}} @@ -248,6 +251,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}} @@ -257,10 +261,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}} @@ -270,17 +274,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| mathdef:: \xref{valid/conventions}{aux-roll-rectype}{\F{roll}} +.. |unrollrt| mathdef:: \xref{valid/conventions}{aux-unroll-rectype}{\F{unroll}} +.. |rolldt| mathdef:: \xref{valid/conventions}{aux-roll-deftype}{\F{roll}^\ast} +.. |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}} @@ -381,7 +388,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}} @@ -986,7 +993,7 @@ .. |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} +.. |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} @@ -995,6 +1002,11 @@ .. |matcheslimits| mathdef:: \xref{valid/matching}{match-limits}{\leq} +.. Meta functions + +.. |clostype| mathdef:: \xref{valid/types}{closure}{\K{clos}} + + .. Contexts .. |CTYPES| mathdef:: \xref{valid/conventions}{context}{\K{types}} @@ -1008,6 +1020,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 @@ -1041,7 +1054,7 @@ .. |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} +.. |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} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 5d1767e53..a681fb87a 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -24,6 +24,201 @@ 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 `. + +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 types. + 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. + + +.. index:: ! substitution +.. _type-subst: +.. _notation-subst: +.. _aux-reftypediff: + +Convention +.......... + +* :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)`. + +* 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:: 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, + such that types with the same recursive structure are also syntactically equal. + 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}{@{}llll@{}} + \rollrt_x(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(x + i)^\ast \subst (\REC~i)^\ast])^\ast \\ + &&& (\iff :math:`i^\ast = 0 \cdots (|\subtype^\ast| - 1)`) + \unrollrt(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(\REC~i)^\ast \subst ((\TREC~\subtype^\ast).i)^\ast])^\ast \\[2ex] + &&& (\iff :math:`i^\ast = 0 \cdots (|\subtype^\ast| - 1)`) + \rolldt_x(\rectype) &=& (\rectype'.i)^\ast & (\iff \rollrt_x(\rectype) = \rectype' = \TREC~\subtype^\ast \\ + &&& \land :math:`i^\ast = 0 \cdots (|\subtype^\ast| - 1)`) \\ + \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 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: diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index e6fededdb..5cdc25ff0 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -1,11 +1,25 @@ -.. 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. + + +.. context-rec: + +.. todo:: move this to conventions + +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:: number type @@ -44,7 +58,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 +68,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 :math:`\EQT` and :math:`\heaptype_2` is :math:`\ANY`. + +* Or :math:`\heaptype_1` is one of :math:`\I31`, :math:`\STRUCT`, or :math:`\ARRAY` and :math:`heaptype_2` is :math:`\EQT`. + +* 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 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:`\NONE` and :math:`\heaptype_2` :ref:`matches ` :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 :math:`\NOFUNC` and :math:`\heaptype_2` :ref:`matches ` :math:`\FUNC`. -* 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 :math:`\NOEXTERN` and :math:`\heaptype_2` :ref:`matches ` :math:`\EXTERN`. + +* Or :math:`\heaptype_1` is :math:`\BOTH`. .. math:: ~\\[-1ex] @@ -70,16 +102,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{ + \expand(\deftype) = \TSTRUCT~\X{st} + }{ + C \vdashheaptypematch \deftype \matchesheaptype \FUNC + } + \qquad + \frac{ + \expand(\deftype) = \TARRAY~\X{at} + }{ + C \vdashheaptypematch \deftype \matchesheaptype \ARRAY + } + \qquad + \frac{ + \expand(\deftype) = \TFUNC~\X{ft} + }{ + C \vdashheaptypematch \deftype \matchesheaptype \FUNC } .. math:: @@ -96,6 +167,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 +312,266 @@ 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-compoundtype: +.. _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 types are immutable, i.e., both :math:`\MUT_1` and :math:`\MUT_2` are absent. + +* Or both types are immutable, i.e., both :math:`\MUT_1` and :math:`\MUT_2` are present, :math:`\storagetype_2` :ref:`matches ` :math:`\storagetype_1` as well. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2 + }{ + C \vdashfieldtypematch \epsilon~\storagetype_1 \matchescomptype \epsilon~\storagetype_2 + } + \qquad + \frac{ + \begin{array}[b]{@{}c@{}} + C \vdashstoragetypematch \storagetype_1 \matchesstoragetype \storagetype_2 \\ - C \vdashresulttypematch [t_{21}^\ast] \matchesresulttype [t_{11}^\ast] + C \vdashstoragetypematch \storagetype_2 \matchesstoragetype \storagetype_1 + \end{array} + }{ + C \vdashfieldtypematch \MUT~\storagetype_1 \matchescomptype \MUT~\storagetype_2 + } + +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:: recursive type, sub type, compound type, final, subtyping, type equivalence + pair: abstract syntax; recursive type + pair: abstract syntax; sub type +.. _valid-rectype: +.. _valid-subtype: + +Recursive Types +~~~~~~~~~~~~~~~ + +:ref:`Recursive types ` are validated with respect to their specific :ref:`type index`. + +:math:`\TREC~\subtype^\ast` +........................... + +* The sequence :math:`\subtype^\ast` of :ref:`sub types ` must be :ref:`valid ` for the :ref:`type index ` :math:`x`. + +* Then the recursive type is valid for the :ref:`type index ` :math:`x`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashsubtype \subtype^\ast \ok(x) + }{ + C \vdashrectype \TREC~\subtype^\ast \ok(x) + } + +:math:`\subtype^\ast` +..................... + +* Either the sequence 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 sequence is valid for the :ref:`type index ` :math:`x`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashsubtypeseq \epsilon \ok(x) + } + \qquad + \frac{ + C \vdashsubtype \subtype \ok(x) + \qquad + C \vdashsubtypeseq {\subtype'}^+ \ok(x + 1) + }{ + C \vdashsubtypeseq \subtype~{\subtype'}^+ \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:`\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:: + ~\\[-1ex] + \frac{ + \begin{array}{@{}c@{}} + |y^\ast| \leq 1 \qquad - C \vdashresulttypematch [t_{22}^\ast] \matchesresulttype [t_{12}^\ast] + (y < x)^\ast + \qquad + C \vdashcomptype \comptype \ok + \qquad + (C \vdashcomptypematch \comptype \matchescomptype \expand(C.\CTYPES[y]))^\ast \end{array} }{ - C \vdashfunctypematch [t_{11}^\ast] \toF [t_{12}^\ast] \matchesfunctype [t_{21}^\ast] \toF [t_{22}^\ast] + C \vdashsubtype \TSUB~\TFINAL^?~y^\ast~\comptype \ok(x) } .. note:: - In future versions of WebAssembly, subtyping on function types may be relaxed to support co- and contra-variance. + The side condition on the index ensures that a type can only be declared a subtype of previously defined types, + preventing cyclic subtype hierarchies. + + Future versions of WebAssembly may allow more than one supertype. + + +.. 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 the :ref:`unrolling ` of :math:`\deftype_1` is :math:`\TSUB~\FINAL^?~x^\ast~\comptype` and there exists a :ref:`type index ` :math:`x_i` in :math:`x^\ast` such that the :ref:`defined type ` :math:`C.\CTYPES[x_i]` :ref:`matches ` :math:`\deftype_2`. + +* Or the :ref:`unrolling ` of :math:`\deftype_1` is :math:`\TSUB~\FINAL^?~{\deftype'_1}^\ast~\comptype` and there exists a :ref:`defined type ` :math:`\deftype'_{1i}` in :math:`{\deftype'_1}^\ast` such that :math:`\deftype'_{1i}` :ref:`matches ` :math:`\deftype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + \clostype_C(\deftype_1) = \clostype_C(\deftype_2) + }{ + C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2 + } + +.. todo:: fix + +.. math:: + ~\\[-1ex] + \frac{ + \subtype_1^\ast[i] = \TSUB~\FINAL^?~\heaptype^\ast~\comptype + \qquad + C \vdashdeftypematch C.\CTYPES[x^\ast[i]] \matchesdeftype \deftype_2 + }{ + C \vdashdeftypematch (\TREC~\subtype_1^\ast).i \matchesdeftype \deftype_2 + } + +.. math:: + ~\\[-1ex] + \frac{ + \subtype_1^\ast[i] = \TSUB~\FINAL^?~{\deftype'_1}^\ast~\comptype + \qquad + C \vdashdeftypematch C.\CTYPES[x^\ast[i]] \matchesdeftype \deftype_2 + }{ + C \vdashdeftypematch (\TREC~\subtype_1^\ast).i \matchesdeftype \deftype_2 + } .. index:: limits diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 0470386d1..c644113d8 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. + +:math:`\type^\ast` +.................. + +* If the sequence is empty, then: + + * The type :ref:`context ` :math:`C.\CTYPES` 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{ + 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 + } + \qquad + \frac{ + C.\CTYPES = \epsilon + }{ + C \vdashtypes \epsilon \ok + } + +.. note:: + Despite the appearance, the |CTYPES| component of :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 @@ -746,25 +802,6 @@ 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. Consequently, the definition of the :ref:`context ` :math:`C` in this rule is recursive: diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 2e2622c75..234399c16 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 @@ -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 closed types and generalised supertypes 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:`\FINAL`. + + * 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 @@ -486,3 +696,19 @@ Value Types }{ C \vdashvaltypedefaultable (\REF~\NULL~\heaptype) \defaultable } + + +.. index:: type index, defined type, type closure +.. _type-closure: + +Closure +~~~~~~~ + +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} From 9bc7b6930cc95a04a2073af0b7c67c83439e7476 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 30 May 2023 16:41:55 +0200 Subject: [PATCH 2/9] Complete --- document/core/appendix/properties.rst | 18 +++ document/core/exec/instructions.rst | 38 +++--- document/core/exec/modules.rst | 35 +++++- document/core/exec/runtime.rst | 2 +- document/core/exec/values.rst | 12 +- document/core/syntax/instructions.rst | 4 +- document/core/syntax/types.rst | 6 +- document/core/util/macros.def | 15 ++- document/core/valid/conventions.rst | 64 +++++++--- document/core/valid/instructions.rst | 44 +++---- document/core/valid/matching.rst | 162 ++++---------------------- document/core/valid/modules.rst | 30 ++--- document/core/valid/types.rst | 38 ++---- 13 files changed, 204 insertions(+), 264 deletions(-) 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 c6b6d1b7f..399c7cc08 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -434,7 +434,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} \\ @@ -453,7 +453,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} @@ -463,7 +463,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} \\ @@ -483,7 +483,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}[i]}(S.\SSTRUCTS[a].\SIFIELDS[i])) \end{array} \\ \end{array} @@ -501,7 +501,7 @@ Reference Instructions S; (\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}[i]}(\val)) \end{array} \\ \end{array} @@ -525,7 +525,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} \\ @@ -544,7 +544,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} @@ -554,7 +554,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} \\ @@ -573,7 +573,7 @@ Reference Instructions S; F; \val^n~(\I32.\CONST~n)~(\ARRAYNEWFIXED~x) &\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} \\ @@ -594,14 +594,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~i)^n~(\ARRAYNEWFIXED~x) \\&& \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 & (b^\ast)^n = S.\SDATAS[F.\AMODULE.\MIDATAS[y]].\DIDATA[s \slice n\cdot|\X{ft}|] \\ \land & (\bytes_{\X{ft}}(i) = \unpackval_{\X{ft}}(b^\ast))^n) @@ -644,7 +644,7 @@ Reference Instructions S; (\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} \\ \end{array} @@ -662,7 +662,7 @@ Reference Instructions S; (\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} \\ \end{array} @@ -3635,7 +3635,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:`compound 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`. @@ -3662,7 +3662,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} \\ @@ -3679,7 +3679,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:`compound 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. @@ -3704,7 +3704,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} @@ -3762,7 +3762,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} @@ -3771,7 +3771,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 8ce92e9df..c844c063c 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:`compound 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 16cddfb5a..50faf5a6a 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/values.rst b/document/core/exec/values.rst index 0dfcdf47d..df8df14d7 100644 --- a/document/core/exec/values.rst +++ b/document/core/exec/values.rst @@ -86,7 +86,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)`. @@ -94,7 +94,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 } @@ -109,7 +109,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)`. @@ -117,7 +117,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 } @@ -132,7 +132,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)`. @@ -140,7 +140,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 85003f437..b1c492cd1 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -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. @@ -491,7 +491,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 8cbbcae2f..8447640dc 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -96,10 +96,10 @@ That is, both type hierarchies are inhabited by an isomorphic set of values, but .. math:: \begin{array}{llrl} - \production{abstract heap type} & \abdheaptype &::=& + \production{abstract heap type} & \absheaptype &::=& \FUNC ~|~ \NOFUNC \\&&|& \EXTERN ~|~ \NOEXTERN \\&&|& - \ANY ~|~ \EQT ~|~ \I31 ~|~ \STRUCT ~|~ \ARRAY ~|~ \NONE \\&&|& + \ANY ~|~ \EQT ~|~ \I31 ~|~ \STRUCT ~|~ \ARRAY ~|~ \NONE \\ \production{heap type} & \heaptype &::=& \absheaptype ~|~ \typeidx \\ \end{array} @@ -184,7 +184,7 @@ They are either :ref:`number types `, :ref:`vector types ` with additional forms for the purpose of specifying :ref:`validation ` and :ref:`execution `. +The syntax of value types is :ref:`extended ` with additional forms for the purpose of specifying :ref:`validation `. Conventions ........... diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 159da65ba..9b876cd2a 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -991,6 +991,9 @@ .. |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} .. |matchescomptype| mathdef:: \xref{valid/matching}{match-comptype}{\leq} @@ -1004,7 +1007,7 @@ .. Meta functions -.. |clostype| mathdef:: \xref{valid/types}{closure}{\K{clos}} +.. |clostype| mathdef:: \xref{valid/conventions}{closure}{\K{clos}} .. Contexts @@ -1034,6 +1037,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-retype}{\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} @@ -1052,6 +1061,9 @@ .. |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} .. |vdashcomptypematch| mathdef:: \xref{valid/matching}{match-comptype}{\vdash} @@ -1102,6 +1114,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 a681fb87a..863a1c9ff 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -58,6 +58,12 @@ they only occur during :ref:`validation ` or :ref:`execution `. 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. @@ -69,27 +75,17 @@ Finally, the representation of supertypes in a :ref:`sub type ` 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 `. +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 types. 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. - -.. index:: ! substitution -.. _type-subst: -.. _notation-subst: .. _aux-reftypediff: Convention .......... -* :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)`. - * The *difference* :math:`\X{rt}_1\reftypediff\X{rt}_2` between two :ref:`reference types ` is defined as follows: .. math:: @@ -126,6 +122,20 @@ but are formed by :ref:`rolling up ` the :ref:`recursive types 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: @@ -136,11 +146,13 @@ It is hence an invariant of the semantics that all :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 `. +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, - such that types with the same recursive structure are also syntactically equal. + 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 `: @@ -154,15 +166,15 @@ These operations are extended to :ref:`defined types ` and defin .. math:: \begin{array}{@{}llll@{}} \rollrt_x(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(x + i)^\ast \subst (\REC~i)^\ast])^\ast \\ - &&& (\iff :math:`i^\ast = 0 \cdots (|\subtype^\ast| - 1)`) + &&& (\iff i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\ \unrollrt(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(\REC~i)^\ast \subst ((\TREC~\subtype^\ast).i)^\ast])^\ast \\[2ex] - &&& (\iff :math:`i^\ast = 0 \cdots (|\subtype^\ast| - 1)`) + &&& (\iff i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\ \rolldt_x(\rectype) &=& (\rectype'.i)^\ast & (\iff \rollrt_x(\rectype) = \rectype' = \TREC~\subtype^\ast \\ - &&& \land :math:`i^\ast = 0 \cdots (|\subtype^\ast| - 1)`) \\ + &&& \land i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\ \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 defined type: +In addition, the following auxiliary function denotes the *expansion* of a :ref:`defined type `: .. math:: \begin{array}{llll} @@ -279,6 +291,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 5c7af1654..8108f1c2e 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]) = \TSTRUCT~(\MVAR~\X{st}) + \expanddt(C.\CTYPES[x]) = \TSTRUCT~(\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 5cdc25ff0..b7a932945 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -8,20 +8,6 @@ Matching 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. -.. context-rec: - -.. todo:: move this to conventions - -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:: number type .. _match-numtype: @@ -74,11 +60,11 @@ A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap ty * Or :math:`\heaptype_1` is one of :math:`\I31`, :math:`\STRUCT`, or :math:`\ARRAY` and :math:`heaptype_2` is :math:`\EQT`. -* 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 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 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 ` 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`. @@ -136,19 +122,19 @@ A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap ty .. math:: ~\\[-1ex] \frac{ - \expand(\deftype) = \TSTRUCT~\X{st} + \expanddt(\deftype) = \TSTRUCT~\X{st} }{ C \vdashheaptypematch \deftype \matchesheaptype \FUNC } \qquad \frac{ - \expand(\deftype) = \TARRAY~\X{at} + \expanddt(\deftype) = \TARRAY~\X{at} }{ C \vdashheaptypematch \deftype \matchesheaptype \ARRAY } \qquad \frac{ - \expand(\deftype) = \TFUNC~\X{ft} + \expanddt(\deftype) = \TFUNC~\X{ft} }{ C \vdashheaptypematch \deftype \matchesheaptype \FUNC } @@ -330,7 +316,7 @@ A :ref:`function type ` :math:`[t_{11}^\ast] \toF [t_{12}^\ast] .. index:: compound types, aggregate type, structure type, array type, field type -.. _match-compoundtype: +.. _match-comptype: .. _match-structtype: .. _match-arraytype: @@ -345,7 +331,7 @@ A :ref:`compound type ` :math:`\comptype_1` matches a type :mat * 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`. + * 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}` @@ -368,7 +354,7 @@ A :ref:`compound type ` :math:`\comptype_1` matches a type :mat \frac{ (C \vdashfieldtypematch \fieldtype_1 \matchesfieldtype \fieldtype_2)^\ast }{ - C \vdashcomptypematch \TSTRUCT~\fieldtype_1^\ast~\fieldtype'_1^\ast \matchescomptype \TSTRUCT~\fieldtype_2^\ast + C \vdashcomptypematch \TSTRUCT~\fieldtype_1^\ast~{\fieldtype'}_1^\ast \matchescomptype \TSTRUCT~\fieldtype_2^\ast } .. math:: @@ -388,20 +374,20 @@ A :ref:`compound type ` :math:`\comptype_1` matches a type :mat Field Types ~~~~~~~~~~~ -A :ref:`field type ` :math:`\MUT_1^?~\storagetype_1` matches a type :math:`\MUT_2^~\storagetype_2` if and only if: +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 types are immutable, i.e., both :math:`\MUT_1` and :math:`\MUT_2` are absent. +* Either both :math:`\mut_1` and :math:`\mut_2` are :math:`\MCONST`. -* Or both types are immutable, i.e., both :math:`\MUT_1` and :math:`\MUT_2` are present, :math:`\storagetype_2` :ref:`matches ` :math:`\storagetype_1` as well. +* 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 \epsilon~\storagetype_1 \matchescomptype \epsilon~\storagetype_2 + C \vdashfieldtypematch \MCONST~\storagetype_1 \matchescomptype \MCONST~\storagetype_2 } \qquad \frac{ @@ -411,7 +397,7 @@ A :ref:`field type ` :math:`\MUT_1^?~\storagetype_1` matches a C \vdashstoragetypematch \storagetype_2 \matchesstoragetype \storagetype_1 \end{array} }{ - C \vdashfieldtypematch \MUT~\storagetype_1 \matchescomptype \MUT~\storagetype_2 + C \vdashfieldtypematch \MVAR~\storagetype_1 \matchescomptype \MVAR~\storagetype_2 } A :ref:`storage type ` :math:`\storagetype_1` matches a type :math:`\storagetype_2` if and only if: @@ -432,102 +418,6 @@ A :ref:`packed type ` :math:`\packedtype_1` matches a type :m } -.. index:: recursive type, sub type, compound type, final, subtyping, type equivalence - pair: abstract syntax; recursive type - pair: abstract syntax; sub type -.. _valid-rectype: -.. _valid-subtype: - -Recursive Types -~~~~~~~~~~~~~~~ - -:ref:`Recursive types ` are validated with respect to their specific :ref:`type index`. - -:math:`\TREC~\subtype^\ast` -........................... - -* The sequence :math:`\subtype^\ast` of :ref:`sub types ` must be :ref:`valid ` for the :ref:`type index ` :math:`x`. - -* Then the recursive type is valid for the :ref:`type index ` :math:`x`. - -.. math:: - ~\\[-1ex] - \frac{ - C \vdashsubtype \subtype^\ast \ok(x) - }{ - C \vdashrectype \TREC~\subtype^\ast \ok(x) - } - -:math:`\subtype^\ast` -..................... - -* Either the sequence 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 sequence is valid for the :ref:`type index ` :math:`x`. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - C \vdashsubtypeseq \epsilon \ok(x) - } - \qquad - \frac{ - C \vdashsubtype \subtype \ok(x) - \qquad - C \vdashsubtypeseq {\subtype'}^+ \ok(x + 1) - }{ - C \vdashsubtypeseq \subtype~{\subtype'}^+ \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:`\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:: - ~\\[-1ex] - \frac{ - \begin{array}{@{}c@{}} - |y^\ast| \leq 1 - \qquad - (y < x)^\ast - \qquad - C \vdashcomptype \comptype \ok - \qquad - (C \vdashcomptypematch \comptype \matchescomptype \expand(C.\CTYPES[y]))^\ast - \end{array} - }{ - C \vdashsubtype \TSUB~\TFINAL^?~y^\ast~\comptype \ok(x) - } - -.. note:: - The side condition on the index ensures that a type can only be declared a subtype of previously defined types, - preventing cyclic subtype hierarchies. - - Future versions of WebAssembly may allow more than one supertype. - - .. index:: defined type, recursive type, unroll, type equivalence pair: abstract syntax; defined type .. _match-deftype: @@ -539,9 +429,11 @@ A :ref:`defined type ` :math:`\deftype_1` matches a type :math:` * Either :math:`\deftype_1` and :math:`\deftype_2` are equal when :ref:`closed ` under context :math:`C`. -* Or the :ref:`unrolling ` of :math:`\deftype_1` is :math:`\TSUB~\FINAL^?~x^\ast~\comptype` and there exists a :ref:`type index ` :math:`x_i` in :math:`x^\ast` such that the :ref:`defined type ` :math:`C.\CTYPES[x_i]` :ref:`matches ` :math:`\deftype_2`. +* Or: + + * Let the :ref:`sub type ` :math:`\TSUB~\TFINAL^?~\heaptype^\ast~\comptype` be the result of :ref:`unrolling ` :math:`\deftype_1`. -* Or the :ref:`unrolling ` of :math:`\deftype_1` is :math:`\TSUB~\FINAL^?~{\deftype'_1}^\ast~\comptype` and there exists a :ref:`defined type ` :math:`\deftype'_{1i}` in :math:`{\deftype'_1}^\ast` such that :math:`\deftype'_{1i}` :ref:`matches ` :math:`\deftype_2`. + * Then there must exist a :ref:`heap type ` :math:`\heaptype_i` in :math:`\heaptype^\ast` that :ref:`matches ` :math:`\deftype_2`. .. math:: ~\\[-1ex] @@ -551,26 +443,14 @@ A :ref:`defined type ` :math:`\deftype_1` matches a type :math:` C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2 } -.. todo:: fix - .. math:: ~\\[-1ex] \frac{ - \subtype_1^\ast[i] = \TSUB~\FINAL^?~\heaptype^\ast~\comptype + \unrolldt(\deftype_1) = \TSUB~\TFINAL^?~\heaptype^\ast~\comptype \qquad - C \vdashdeftypematch C.\CTYPES[x^\ast[i]] \matchesdeftype \deftype_2 + C \vdashheaptypematch \heaptype^\ast[i] \matchesheaptype \deftype_2 }{ - C \vdashdeftypematch (\TREC~\subtype_1^\ast).i \matchesdeftype \deftype_2 - } - -.. math:: - ~\\[-1ex] - \frac{ - \subtype_1^\ast[i] = \TSUB~\FINAL^?~{\deftype'_1}^\ast~\comptype - \qquad - C \vdashdeftypematch C.\CTYPES[x^\ast[i]] \matchesdeftype \deftype_2 - }{ - C \vdashdeftypematch (\TREC~\subtype_1^\ast).i \matchesdeftype \deftype_2 + C \vdashdeftypematch \deftype_1 \matchesdeftype \deftype_2 } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index c644113d8..f25685217 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -13,14 +13,14 @@ Furthermore, most definitions are themselves classified with a suitable type. Types ~~~~~ -The sequence of :ref:`types ` defined in a module is validated incrementally. +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 type :ref:`context ` :math:`C.\CTYPES` must be empty. + * The type :ref:`context ` :math:`C` must be empty. * Then the type sequence is valid. @@ -58,7 +58,7 @@ The sequence of :ref:`types ` defined in a module is validated incr } .. note:: - Despite the appearance, the |CTYPES| component of :math:`C` is effectively an _output_ of this judgement. + 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 @@ -78,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`: @@ -102,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 @@ -642,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, @@ -672,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)`, @@ -746,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 @@ -776,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 @@ -803,7 +795,7 @@ The :ref:`external types ` classifying a module may contain f } .. 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 234399c16..192b86dfa 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -119,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` ............ @@ -339,8 +339,8 @@ Compound Types Field Types ~~~~~~~~~~~ -:math:`\MUT^?~\storagetype` -........................... +:math:`\mut~\storagetype` +......................... * The :ref:`storage type ` :math:`\storagetype` must be :ref:`valid `. @@ -350,7 +350,7 @@ Field Types \frac{ C \vdashstoragetype \X{st} \ok }{ - C \vdashfieldtype \MUT^?~\X{st} \ok + C \vdashfieldtype \mut~\X{st} \ok } :math:`\packedtype` @@ -379,15 +379,15 @@ Recursive Types :math:`\TREC~\subtype^\ast` ........................... -.. todo:: add version of this for closed types and generalised supertypes to appendix +.. 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 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`. + * 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`. @@ -420,9 +420,9 @@ Recursive Types * 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:`\FINAL`. + * 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]`. + * 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`. @@ -611,7 +611,7 @@ External Types \frac{ C \vdashdeftype \deftype \ok \qquad - \expand(\deftype) = \TFUNC~\functype + \expanddt(\deftype) = \TFUNC~\functype }{ C \vdashexterntype \ETFUNC~\deftype } @@ -696,19 +696,3 @@ Value Types }{ C \vdashvaltypedefaultable (\REF~\NULL~\heaptype) \defaultable } - - -.. index:: type index, defined type, type closure -.. _type-closure: - -Closure -~~~~~~~ - -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} From 2e3f80a2b87dd59cc60c66c584c26e1d443fee3e Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 30 May 2023 17:08:56 +0200 Subject: [PATCH 3/9] Fix some errors --- document/core/syntax/types.rst | 1 - document/core/valid/instructions.rst | 8 ++++---- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 8447640dc..46bdcec23 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -75,7 +75,6 @@ Conventions .. index:: ! heap type, store, type index, ! abstract type, ! concrete type, ! unboxed scalar pair: abstract syntax; heap type -.. _type-closed: .. _type-abstract: .. _type-concrete: .. _syntax-i31: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 8108f1c2e..5e0901bdc 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -413,13 +413,13 @@ Aggregate Reference Instructions * Let :math:`t` be the :ref:`value type ` :math:`\unpacktype(\storagetype)`. -* Then the instruction is valid with type :math:`[t~I32] \to [(\REF~x)]`. +* Then the instruction is valid with type :math:`[t~\I32] \to [(\REF~x)]`. .. math:: \frac{ \expanddt(C.\CTYPES[x]) = \TARRAY~(\mut~\X{st}) }{ - C \vdashinstr \ARRAYNEW~x : [\unpacktype(\X{st})~I32] \to [(\REF~x)] + C \vdashinstr \ARRAYNEW~x : [\unpacktype(\X{st})~\I32] \to [(\REF~x)] } .. _valid-array.new_default: @@ -437,7 +437,7 @@ Aggregate Reference Instructions * The type :math:`t` must be :ref:`defaultable `. -* Then the instruction is valid with type :math:`[I32] \to [(\REF~x)]`. +* Then the instruction is valid with type :math:`[\I32] \to [(\REF~x)]`. .. math:: \frac{ @@ -445,7 +445,7 @@ Aggregate Reference Instructions \qquad C \vdashvaltypedefaultable \unpacktype(\X{st}) \defaultable }{ - C \vdashinstr \ARRAYNEW~x : [I32] \to [(\REF~x)] + C \vdashinstr \ARRAYNEW~x : [\I32] \to [(\REF~x)] } .. _valid-array.new_fixed: From 92bb682821367c92826f58a0c90231e1d2dd14f2 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 31 May 2023 09:25:42 +0200 Subject: [PATCH 4/9] Typo --- document/core/util/macros.def | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 9b876cd2a..88121543e 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -229,7 +229,7 @@ .. |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{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}} From 97e06e0784f7fb4c25d39e4e098e941999006ebc Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 31 May 2023 09:27:26 +0200 Subject: [PATCH 5/9] Tweak --- document/core/valid/modules.rst | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 20642dbe4..37f6a5e10 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -20,7 +20,7 @@ The sequence of :ref:`types ` defined in a module is validated incr * If the sequence is empty, then: - * The type :ref:`context ` :math:`C` must be empty. + * The :ref:`context ` :math:`C` must be empty. * Then the type sequence is valid. @@ -52,9 +52,8 @@ The sequence of :ref:`types ` defined in a module is validated incr } \qquad \frac{ - C.\CTYPES = \epsilon }{ - C \vdashtypes \epsilon \ok + \{\} \vdashtypes \epsilon \ok } .. note:: From 06c497ec08d256e9a04b12bbf7d2f8826a5dff2d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 27 Jun 2023 08:31:12 +0200 Subject: [PATCH 6/9] Bit width for packed types --- document/core/exec/instructions.rst | 1 - document/core/syntax/types.rst | 7 ++++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 05b05fb8f..2c3024b4d 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -586,7 +586,6 @@ Reference Instructions ....................................... .. todo:: Prose -.. todo:: extend type size convention to field types .. math:: ~\\[-1ex] diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 46bdcec23..398024ce9 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -228,7 +228,7 @@ 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:: ! compound type, function type, aggreagate type, structure type, array type pair: abstract syntax; compound type From 75169496533f9c994540e88e6e5481000055e3b2 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 19 Jul 2023 11:26:05 +0200 Subject: [PATCH 7/9] Comments --- document/core/exec/modules.rst | 4 ++-- document/core/util/macros.def | 6 +++--- document/core/valid/conventions.rst | 22 ++++++++++++---------- document/core/valid/matching.rst | 6 +++--- document/core/valid/modules.rst | 15 ++++++++------- document/core/valid/types.rst | 4 ++-- 6 files changed, 30 insertions(+), 27 deletions(-) diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 3ed67a327..8d107a6f9 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -457,7 +457,7 @@ For types, however, allocation is defined in terms of :ref:`rolling ` 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 types. + 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: @@ -164,20 +164,22 @@ The representation change is performed by two auxiliary operations on the syntax These operations are extended to :ref:`defined types ` and defined as follows: .. math:: - \begin{array}{@{}llll@{}} - \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 \\[2ex] - &&& (\iff i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\ - \rolldt_x(\rectype) &=& (\rectype'.i)^\ast & (\iff \rollrt_x(\rectype) = \rectype' = \TREC~\subtype^\ast \\ - &&& \land i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\ - \unrolldt(\rectype.i) &=& \subtype^\ast[i] & (\iff \unrollrt(\rectype) = \TREC~\subtype^\ast) \\ + \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} + \begin{array}{@{}llll@{}} \expanddt(\deftype) &=& \comptype & (\iff \unrolldt(\deftype) = \TSUB~\TFINAL^?~\X{ht}^?~\comptype) \\ \end{array} diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index b7a932945..b8ddbe56a 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -60,11 +60,11 @@ A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap ty * Or :math:`\heaptype_1` is one of :math:`\I31`, :math:`\STRUCT`, or :math:`\ARRAY` and :math:`heaptype_2` is :math:`\EQT`. -* 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 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 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 ` 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`. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 37f6a5e10..511beb3c9 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -32,7 +32,7 @@ The sequence of :ref:`types ` defined in a module is validated incr * 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 `. + * 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`. @@ -40,21 +40,22 @@ The sequence of :ref:`types ` defined in a module is validated incr * 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) + C = C' \with \CTYPES = C'.\CTYPES~\rolldt{|C'.\CTYPES|}(\rectype) \qquad C \vdashrectype \rectype \ok(|C'.\CTYPES|) }{ C \vdashtypes \type^\ast~\rectype \ok } - \qquad - \frac{ - }{ - \{\} \vdashtypes \epsilon \ok - } .. note:: Despite the appearance, the context :math:`C` is effectively an _output_ of this judgement. diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 192b86dfa..678282c0b 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -309,8 +309,8 @@ Compound Types C \vdashcomptype \TSTRUCT~\X{ft}^\ast \ok } -:math:`TARRAY~\fieldtype` -......................... +:math:`\TARRAY~\fieldtype` +.......................... * The :ref:`field type ` :math:`\fieldtype` must be :ref:`valid `. From 2a857e2601a9f109d55e2a042d7b3d9d583f25d7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 19 Jul 2023 13:15:20 +0200 Subject: [PATCH 8/9] Fix spacing --- document/core/valid/modules.rst | 2 +- document/core/valid/types.rst | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 511beb3c9..6fd1cbabd 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -52,7 +52,7 @@ The sequence of :ref:`types ` defined in a module is validated incr \qquad C = C' \with \CTYPES = C'.\CTYPES~\rolldt{|C'.\CTYPES|}(\rectype) \qquad - C \vdashrectype \rectype \ok(|C'.\CTYPES|) + C \vdashrectype \rectype ~{\ok}(|C'.\CTYPES|) }{ C \vdashtypes \type^\ast~\rectype \ok } diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 678282c0b..69ac07c36 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -394,15 +394,15 @@ Recursive Types .. math:: \frac{ }{ - C \vdashrectype \TREC~\epsilon \ok(x) + C \vdashrectype \TREC~\epsilon ~{\ok}(x) } \qquad \frac{ - C \vdashsubtype \subtype \ok(x) + C \vdashsubtype \subtype ~{\ok}(x) \qquad - C \vdashrectype \TREC~{\subtype'}^\ast \ok(x + 1) + C \vdashrectype \TREC~{\subtype'}^\ast ~{\ok}(x + 1) }{ - C \vdashrectype \TREC~\subtype~{\subtype'}^\ast \ok(x) + C \vdashrectype \TREC~\subtype~{\subtype'}^\ast ~{\ok}(x) } :math:`\TSUB~\TFINAL^?~y^\ast~\comptype` @@ -442,7 +442,7 @@ Recursive Types (C \vdashcomptypematch \comptype \matchescomptype \comptype')^\ast \end{array} }{ - C \vdashsubtype \TSUB~\TFINAL^?~y^\ast~\comptype \ok(x) + C \vdashsubtype \TSUB~\TFINAL^?~y^\ast~\comptype ~{\ok}(x) } .. note:: @@ -472,7 +472,7 @@ Defined Types .. math:: \frac{ - C \vdashrectype \rectype \ok(x) + C \vdashrectype \rectype ~{\ok}(x) \qquad \rectype = \TREC~\subtype^n \qquad From fd152805057510e97461acb2ed9f31f1b68789d1 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 20 Jul 2023 07:58:23 +0200 Subject: [PATCH 9/9] Resolve some more errors and conflicts --- document/core/appendix/changes.rst | 2 +- document/core/exec/instructions.rst | 10 ++++----- document/core/syntax/instructions.rst | 2 +- document/core/syntax/types.rst | 29 ++++++++------------------- document/core/valid/modules.rst | 2 +- document/core/valid/types.rst | 2 +- 6 files changed, 17 insertions(+), 30 deletions(-) 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/exec/instructions.rst b/document/core/exec/instructions.rst index 3e152da41..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. @@ -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. @@ -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: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 13860772b..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. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 87e2cacfc..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,10 +67,12 @@ 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`. @@ -165,24 +168,6 @@ 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 pair: abstract syntax; value type @@ -281,10 +266,12 @@ Structures are heterogeneous, but require static indexing, while arrays need to \I8 ~|~ \I16 \\ \end{array} +.. _bitwidth-fieldtype: + Conventions ........... -* The notation :math:`|t|` for :ref:`bit width ` extends to packed types as well, that is, :math:`|\I8| = 8` and :math:`|\I16| = 16`. +* The notation :math:`|t|` for :ref:`bit width ` extends to packed types as well, that is, :math:`|\I8| = 8` and :math:`|\I16| = 16`. .. index:: ! compound type, function type, aggreagate type, structure type, array type diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index cd446359f..89d1c54d3 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -571,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] } diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index baee64ad4..63cf0e465 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -159,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] }