diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index dde34900..75514218 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -13,13 +13,13 @@ Typing of Static Constructs =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== -:ref:`Limits ` :math:`\vdashlimits \limits : k` -:ref:`Function type ` :math:`\vdashfunctype \functype \ok` -:ref:`Block type ` :math:`\vdashblocktype \blocktype \ok` -:ref:`Table type ` :math:`\vdashtabletype \tabletype \ok` -:ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` -:ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` -:ref:`External type ` :math:`\vdashexterntype \externtype \ok` +:ref:`Limits ` :math:`C \vdashlimits \limits : k` +:ref:`Function type ` :math:`C \vdashfunctype \functype \ok` +:ref:`Block type ` :math:`C \vdashblocktype \blocktype \ok` +:ref:`Table type ` :math:`C \vdashtabletype \tabletype \ok` +:ref:`Memory type ` :math:`C \vdashmemtype \memtype \ok` +:ref:`Global type ` :math:`C \vdashglobaltype \globaltype \ok` +:ref:`External type ` :math:`C \vdashexterntype \externtype \ok` :ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` :ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` :ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` @@ -83,8 +83,17 @@ Matching =============================================== =============================================================================== Construct Judgement =============================================== =============================================================================== -:ref:`External type ` :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` -:ref:`Limits ` :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2` +:ref:`Number type ` :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2` +:ref:`Heap type ` :math:`C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2` +:ref:`Reference type ` :math:`C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2` +:ref:`Value type ` :math:`C \vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2` +:ref:`Result type ` :math:`C \vdashresulttypematch \resulttype_1 \matchesresulttype \resulttype_2` +:ref:`Function type ` :math:`C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2` +:ref:`Table type ` :math:`C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2` +:ref:`Memory type ` :math:`C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2` +:ref:`Global type ` :math:`C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2` +:ref:`External type ` :math:`C \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` +:ref:`Limits ` :math:`C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2` =============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst index fd38fe20..90a41193 100644 --- a/document/core/appendix/index-types.rst +++ b/document/core/appendix/index-types.rst @@ -13,9 +13,12 @@ Category Constructor :ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) :ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) (reserved) :math:`\hex{7B}` .. :math:`\hex{71}` -:ref:`Reference type ` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|) -:ref:`Reference type ` |EXTERNREF| :math:`\hex{6F}` (-17 as |Bs7|) -(reserved) :math:`\hex{6E}` .. :math:`\hex{61}` +:ref:`Heap type ` |FUNC| :math:`\hex{70}` (-16 as |Bs7|) +:ref:`Heap type ` |EXTERN| :math:`\hex{6F}` (-17 as |Bs7|) +(reserved) :math:`\hex{6E}` .. :math:`\hex{6D}` +:ref:`Reference type ` |REF| |NULL| :math:`\hex{6C}` (-20 as |Bs7|) +:ref:`Reference type ` |REF| :math:`\hex{6B}` (-21 as |Bs7|) +(reserved) :math:`\hex{6A}` .. :math:`\hex{61}` :ref:`Function type ` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) (reserved) :math:`\hex{5F}` .. :math:`\hex{41}` :ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index cf1fd0fb..7aa01099 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -4,6 +4,10 @@ Soundness --------- +.. todo:: need to operate wrt semantic types +.. todo:: define "S \vdash t ok" +.. todo:: ensure wf of guessed valtypes + The :ref:`type system ` of WebAssembly is *sound*, implying both *type safety* and *memory safety* with respect to the WebAssembly semantics. For example: * All types declared and derived during validation are respected at run time; @@ -50,7 +54,7 @@ Results :ref:`Results ` :math:`\TRAP` ............................................ -* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types `. +* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`valid ` :ref:`value types `. .. math:: \frac{ @@ -221,6 +225,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Then the table instance is valid with :ref:`table type ` :math:`\limits~t`. +.. todo:: reftypematch needs C + .. math:: \frac{ \vdashtabletype \limits~t \ok @@ -229,7 +235,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \qquad (S \vdash \reff : t')^n \qquad - (\vdashreftypematch t' \matchesvaltype t)^n + (C \vdashreftypematch t' \matchesvaltype t)^n }{ S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t } @@ -297,11 +303,13 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Then the table instance is valid. +.. todo:: reftypematch needs C + .. math:: \frac{ (S \vdash \reff : t')^\ast \qquad - (\vdashreftypematch t' \matchesvaltype t)^\ast + (C \vdashreftypematch t' \matchesvaltype t)^\ast }{ S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok } diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 9c789978..89724697 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -88,7 +88,7 @@ Reference Instructions .. math:: \begin{array}{llclll} \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{D0}~~t{:}\Breftype &\Rightarrow& \REFNULL~t \\ &&|& + \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|& \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ \end{array} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 975f17ad..e9adc4df 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -29,6 +29,24 @@ Number Types \end{array} +.. index:: heap type + pair: binary format; heap type +.. _binary-heaptype: + +Heap Types +~~~~~~~~~~ + +:ref:`Heap types ` are encoded as either a single byte, or as a :ref:`type index ` encoded as a positive :ref:`signed integer `. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{heap type} & \Bheaptype &::=& + \hex{6F} &\Rightarrow& \EXTERN \\ &&|& + \hex{70} &\Rightarrow& \FUNC \\ &&|& + x{:}\Bs33 &\Rightarrow& x & (\iff x \geq 0) \\ + \end{array} + + .. index:: reference type pair: binary format; reference type .. _binary-reftype: @@ -36,13 +54,15 @@ Number Types Reference Types ~~~~~~~~~~~~~~~ -:ref:`Reference types ` are also encoded by a single byte. +:ref:`Reference types ` are either encoded by a single byte followed by a :ref:`heap type `, or, as a short form, directly as a non-index heap type. .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{reference type} & \Breftype &::=& - \hex{70} &\Rightarrow& \FUNCREF \\ &&|& - \hex{6F} &\Rightarrow& \EXTERNREF \\ + \hex{6B}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\X{ht} \\ &&|& + \hex{6C}~~\X{ht}{:}\Bheaptype &\Rightarrow& \REF~\NULL~\X{ht} \\ &&|& + \hex{6F} &\Rightarrow& \EXTERNREF \\ &&|& + \hex{70} &\Rightarrow& \FUNCREF \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index cf0cf087..2547aa49 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -3,7 +3,7 @@ Modules For modules, the execution semantics primarily defines :ref:`instantiation `, which :ref:`allocates ` instances for a module and its contained definitions, initializes :ref:`tables ` and :ref:`memories ` from contained :ref:`element ` and :ref:`data ` segments, and invokes the :ref:`start function ` if present. It also includes :ref:`invocation ` of exported functions. -Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports ` and :ref:`allocating ` instances. +Instantiation depends on a number of auxiliary notions for :ref:`type-checking imports ` and :ref:`allocating ` instances. .. index:: external value, external type, validation, import, store diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 02b90c01..5f042cd5 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -13,6 +13,7 @@ Runtime Structure .. _syntax-ref: .. _syntax-ref.extern: .. _syntax-val: +.. _syntax-null: Values ~~~~~~ diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 9c582d64..ed3aff9c 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -434,7 +434,7 @@ Forward branches require operands according to the output of the targeted block' Backward branches require operands according to the input of the targeted block's type, i.e., represent the values consumed by the restarted block. The |CALL| instruction invokes another :ref:`function `, consuming the necessary arguments from the stack and returning the result values of the call. -The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table ` that is denoted by a :ref:`table index ` and must have type |FUNCREF|. +The |CALLINDIRECT| instruction calls a function indirectly through an operand indexing into a :ref:`table ` that is denoted by a :ref:`table index ` and must contain :ref:`function references `. Since it may contain functions of heterogeneous type, the callee is dynamically checked against the :ref:`function type ` indexed by the instruction's second immediate, and the call is aborted with a :ref:`trap ` if it does not match. diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index cfd8935a..f51a504f 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -273,7 +273,7 @@ The |EOFFSET| is given by a :ref:`constant ` :ref:`expression `. .. note:: - In the current version of WebAssembly, only tables of element type |FUNCREF| can be initialized with an element segment. + In the current version of WebAssembly, only tables whose elements are :ref:`function references ` can be initialized with an element segment. This limitation may be lifted in the future. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 858fbc1a..ac8b224c 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -41,7 +41,29 @@ Conventions That is, :math:`|\I32| = |\F32| = 32` and :math:`|\I64| = |\F64| = 64`. -.. index:: ! reference type, reference, table, function, function type, null +.. index:: ! heap type, store, type index + pair: abstract syntax; heap type +.. _syntax-heaptype: + +Heap Types +~~~~~~~~~~ + +*Heap types* classify objects in the runtime :ref:`store `. + +.. math:: + \begin{array}{llll} + \production{heap type} & \heaptype &::=& + \FUNC ~|~ \EXTERN ~|~ \typeidx \\ + \end{array} + +The type |FUNC| denotes the infinite union of all types of :ref:`functions `, regardless of their concrete :ref:`function types `. + +The type |EXTERN| denotes the infinite union of all objects owned by the :ref:`embedder ` and that can be passed into WebAssembly under this type. + +A *concrete* heap type consists of a :ref:`type index ` and classifies an object of the respective :ref:`type ` defined in the module. + + +.. index:: ! reference type, heap type, reference, table, function, function type, null pair: abstract syntax; reference type pair: reference; type .. _syntax-reftype: @@ -49,26 +71,28 @@ Conventions Reference Types ~~~~~~~~~~~~~~~ -*Reference types* classify first-class references to objects in the runtime :ref:`store `. +*Reference types* classify :ref:`values ` that are first-class references to objects in the runtime :ref:`store `. .. math:: \begin{array}{llll} \production{reference type} & \reftype &::=& - \FUNCREF ~|~ \EXTERNREF \\ + \REF~\NULL^?~\heaptype \\ \end{array} -The type |FUNCREF| denotes the infinite union of all references to :ref:`functions `, regardless of their :ref:`function types `. +A reference type is characterised by the :ref:`heap type ` it points to. -The type |EXTERNREF| denotes the infinite union of all references to objects owned by the :ref:`embedder ` and that can be passed into WebAssembly under this type. +In addition, a reference type of the form :math:`\REF \NULL \X{ht}` is *nullable*, meaning that it can either be a proper reference to :math:`\X{ht}` or :ref:`null `. +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 `. -.. index:: ! value type, number type, reference type +.. index:: ! value type, number type, reference type, ! bottom type pair: abstract syntax; value type pair: value; type .. _syntax-valtype: +.. _syntax-bottype: Value Types ~~~~~~~~~~~ diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 6112a766..0c350d00 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -70,7 +70,7 @@ However, the special case of a type use that is syntactically empty or consists \begin{array}[t]{@{}c@{}} ::= \\ | \\ \end{array} & \begin{array}[t]{@{}lcll@{}} - (t{:}\Tresult)^? &\Rightarrow& t^? \\ + (t{:}\Tresult_I)^? &\Rightarrow& t^? \\ x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\ \end{array} \\ \production{block instruction} & \Tblockinstr_I &::=& @@ -128,9 +128,9 @@ The :math:`\text{else}` keyword of an :math:`\text{if}` instruction can be omitt .. math:: \begin{array}{llclll} \production{block instruction} & - \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} + \text{if}~~\Tlabel~~\Tblocktype_I~~\Tinstr^\ast~~\text{end} &\equiv& - \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{else}~~\text{end} + \text{if}~~\Tlabel~~\Tblocktype_I~~\Tinstr^\ast~~\text{else}~~\text{end} \end{array} Also, for backwards compatibility, the table index to :math:`\text{call\_indirect}` can be omitted, defaulting to :math:`0`. @@ -178,7 +178,7 @@ Parametric Instructions \begin{array}{llclll} \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|& \text{drop} &\Rightarrow& \DROP \\ &&|& - \text{select}~((t{:}\Tresult)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\ + \text{select}~((t{:}\Tresult_I)^\ast)^? &\Rightarrow& \SELECT~(t^\ast)^? \\ \end{array} diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 848f6880..d9e75984 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -72,8 +72,8 @@ Type definitions can bind a symbolic :ref:`type identifier `. .. math:: \begin{array}{llclll} - \production{type definition} & \Ttype &::=& - \text{(}~\text{type}~~\Tid^?~~\X{ft}{:}\Tfunctype~\text{)} + \production{type definition} & \Ttype_I &::=& + \text{(}~\text{type}~~\Tid^?~~\X{ft}{:}\Tfunctype_I~\text{)} &\Rightarrow& \X{ft} \\ \end{array} @@ -167,11 +167,11 @@ The descriptors in imports can bind a symbolic function, table, memory, or globa \production{import description} & \Timportdesc_I &::=& \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~\text{)} &\Rightarrow& \IDFUNC~x \\ &&|& - \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype~\text{)} + \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype_I~\text{)} &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& - \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype_I~\text{)} &\Rightarrow& \IDMEM~~\X{mt} \\ &&|& - \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype~\text{)} + \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype_I~\text{)} &\Rightarrow& \IDGLOBAL~\X{gt} \\ \end{array} @@ -198,11 +198,11 @@ Function definitions can bind a symbolic :ref:`function identifier `, a \begin{array}{llclll} \production{function} & \Tfunc_I &::=& \text{(}~\text{func}~~\Tid^?~~x,I'{:}\Ttypeuse_I~~ - (t{:}\Tlocal)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad + (t{:}\Tlocal_I)^\ast~~(\X{in}{:}\Tinstr_{I''})^\ast~\text{)} \\ &&& \qquad \Rightarrow\quad \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\X{in}^\ast~\END \} \\ &&& \qquad\qquad\qquad (\iff I'' = I' \compose \{\ILOCALS~\F{id}(\Tlocal)^\ast\} \idcwellformed) \\[1ex] - \production{local} & \Tlocal &::=& - \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype~\text{)} + \production{local} & \Tlocal_I &::=& + \text{(}~\text{local}~~\Tid^?~~t{:}\Tvaltype_I~\text{)} \quad\Rightarrow\quad t \\ \end{array} @@ -265,7 +265,7 @@ Table definitions can bind a symbolic :ref:`table identifier `. .. math:: \begin{array}{llclll} \production{table} & \Ttable_I &::=& - \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype~\text{)} + \text{(}~\text{table}~~\Tid^?~~\X{tt}{:}\Ttabletype_I~\text{)} &\Rightarrow& \{ \TTYPE~\X{tt} \} \\ \end{array} @@ -334,7 +334,7 @@ Memory definitions can bind a symbolic :ref:`memory identifier `. .. math:: \begin{array}{llclll} \production{memory} & \Tmem_I &::=& - \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype~\text{)} + \text{(}~\text{memory}~~\Tid^?~~\X{mt}{:}\Tmemtype_I~\text{)} &\Rightarrow& \{ \MTYPE~\X{mt} \} \\ \end{array} @@ -394,7 +394,7 @@ Global definitions can bind a symbolic :ref:`global identifier `. .. math:: \begin{array}{llclll} \production{global} & \Tglobal_I &::=& - \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype~~e{:}\Texpr_I~\text{)} + \text{(}~\text{global}~~\Tid^?~~\X{gt}{:}\Tglobaltype_I~~e{:}\Texpr_I~\text{)} &\Rightarrow& \{ \GTYPE~\X{gt}, \GINIT~e \} \\ \end{array} @@ -505,7 +505,7 @@ Element segments allow for an optional :ref:`table index ` to ide \text{(}~\text{elem}~~\Tid^?~~\text{declare}~~(et, y^\ast){:}\Telemlist_I~\text{)} \\ &&& \qquad \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EDECLARATIVE \} \\ \production{element list} & \Telemlist_I &::=& - t{:}\Treftype~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ + t{:}\Treftype_I~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ \production{element expression} & \Telemexpr_I &::=& \text{(}~\text{item}~~e{:}\Texpr_I~\text{)} \quad\Rightarrow\quad e \\ @@ -641,7 +641,7 @@ The name serves a documentary role only. \production{module field} & \Tmodulefield_I & \begin{array}[t]{@{}clll} ::=& - \X{ty}{:}\Ttype &\Rightarrow& \{\MTYPES~\X{ty}\} \\ |& + \X{ty}{:}\Ttype_I &\Rightarrow& \{\MTYPES~\X{ty}\} \\ |& \X{im}{:}\Timport_I &\Rightarrow& \{\MIMPORTS~\X{im}\} \\ |& \X{fn}{:}\Tfunc_I &\Rightarrow& \{\MFUNCS~\X{fn}\} \\ |& \X{ta}{:}\Ttable_I &\Rightarrow& \{\MTABLES~\X{ta}\} \\ |& diff --git a/document/core/text/types.rst b/document/core/text/types.rst index 6d4ee375..17a3f46a 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -14,7 +14,7 @@ Number Types .. math:: \begin{array}{llcll@{\qquad\qquad}l} - \production{number type} & \Tnumtype &::=& + \production{number type} & \Tnumtype_I &::=& \text{i32} &\Rightarrow& \I32 \\ &&|& \text{i64} &\Rightarrow& \I64 \\ &&|& \text{f32} &\Rightarrow& \F32 \\ &&|& @@ -22,22 +22,48 @@ Number Types \end{array} +.. index:: heap type + pair: text format; heap type +.. _text-heaptype: + +Heap Types +~~~~~~~~~~ + +.. math:: + \begin{array}{llcll@{\qquad\qquad}l} + \production{heap type} & \Theaptype_I &::=& + \text{func} &\Rightarrow& \FUNC \\ &&|& + \text{extern} &\Rightarrow& \EXTERN \\ &&|& + x{:}\Ttypeidx_I &\Rightarrow& x \\ + \end{array} + + .. index:: reference type pair: text format; reference type .. _text-reftype: -.. _text-heaptype: Reference Types ~~~~~~~~~~~~~~~ .. math:: \begin{array}{llcll@{\qquad\qquad}l} - \production{reference type} & \Treftype &::=& - \text{funcref} &\Rightarrow& \FUNCREF \\ &&|& - \text{externref} &\Rightarrow& \EXTERNREF \\ - \production{heap type} & \Theaptype &::=& - \text{func} &\Rightarrow& \FUNCREF \\ &&|& - \text{extern} &\Rightarrow& \EXTERNREF \\ + \production{reference type} & \Treftype_I &::=& + \text{(}~\text{ref}~~\X{ht}{:}\Theaptype~\text{)} + &\Rightarrow& \REF~\X{ht} \\ &&|& + \text{(}~\text{ref}~~\text{null}~~\X{ht}{:}\Theaptype~\text{)} + &\Rightarrow& \REF~\NULL~\X{ht} \\ + \end{array} + +Abbreviations +............. + +There are shorthands for references to abstract heap types. + +.. math:: + \begin{array}{llclll} + \production{reference type} & + \text{funcref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{func}~\text{)} \\ + \text{externref} &\equiv& \text{(}~\text{ref}~~\text{null}~~\text{extern}~\text{)} \\ \end{array} @@ -50,9 +76,9 @@ Value Types .. math:: \begin{array}{llcll@{\qquad\qquad}l} - \production{value type} & \Tvaltype &::=& - t{:}\Tnumtype &\Rightarrow& t \\ &&|& - t{:}\Treftype &\Rightarrow& t \\ + \production{value type} & \Tvaltype_I &::=& + t{:}\Tnumtype_I &\Rightarrow& t \\ &&|& + t{:}\Treftype_I &\Rightarrow& t \\ \end{array} @@ -67,14 +93,14 @@ Function Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{function type} & \Tfunctype &::=& - \text{(}~\text{func}~~t_1^\ast{:\,}\Tvec(\Tparam)~~t_2^\ast{:\,}\Tvec(\Tresult)~\text{)} + \production{function type} & \Tfunctype_I &::=& + \text{(}~\text{func}~~t_1^\ast{:\,}\Tvec(\Tparam_I)~~t_2^\ast{:\,}\Tvec(\Tresult_I)~\text{)} &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ - \production{parameter} & \Tparam &::=& - \text{(}~\text{param}~~\Tid^?~~t{:}\Tvaltype~\text{)} + \production{parameter} & \Tparam_I &::=& + \text{(}~\text{param}~~\Tid^?~~t{:}\Tvaltype_I~\text{)} &\Rightarrow& t \\ - \production{result} & \Tresult &::=& - \text{(}~\text{result}~~t{:}\Tvaltype~\text{)} + \production{result} & \Tresult_I &::=& + \text{(}~\text{result}~~t{:}\Tvaltype_I~\text{)} &\Rightarrow& t \\ \end{array} @@ -119,7 +145,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{memory type} & \Tmemtype &::=& + \production{memory type} & \Tmemtype_I &::=& \X{lim}{:}\Tlimits &\Rightarrow& \X{lim} \\ \end{array} @@ -133,8 +159,8 @@ Table Types .. math:: \begin{array}{llclll} - \production{table type} & \Ttabletype &::=& - \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype &\Rightarrow& \X{lim}~\X{et} \\ + \production{table type} & \Ttabletype_I &::=& + \X{lim}{:}\Tlimits~~\X{et}{:}\Treftype_I &\Rightarrow& \X{lim}~\X{et} \\ \end{array} @@ -148,7 +174,7 @@ Global Types .. math:: \begin{array}{llclll} - \production{global type} & \Tglobaltype &::=& + \production{global type} & \Tglobaltype_I &::=& t{:}\Tvaltype &\Rightarrow& \MCONST~t \\ &&|& - \text{(}~\text{mut}~~t{:}\Tvaltype~\text{)} &\Rightarrow& \MVAR~t \\ + \text{(}~\text{mut}~~t{:}\Tvaltype_I~\text{)} &\Rightarrow& \MVAR~t \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 0a7a9cf7..a4d950e9 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -179,8 +179,12 @@ .. |F32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32}} .. |F64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f64}} -.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{funcref}} -.. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{externref}} +.. |REF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{ref}} +.. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}} +.. |FUNC| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{func}} +.. |EXTERN| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{extern}} +.. |FUNCREF| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{funcref}} +.. |EXTERNREF| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{externref}} .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}} @@ -197,6 +201,7 @@ .. Types, non-terminals .. |numtype| mathdef:: \xref{syntax/types}{syntax-numtype}{\X{numtype}} +.. |heaptype| mathdef:: \xref{syntax/types}{syntax-heaptype}{\X{heaptype}} .. |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}} @@ -500,6 +505,7 @@ .. Types, non-terminals .. |Bnumtype| mathdef:: \xref{binary/types}{binary-numtype}{\B{numtype}} +.. |Bheaptype| mathdef:: \xref{binary/types}{binary-heaptype}{\B{heaptype}} .. |Breftype| mathdef:: \xref{binary/types}{binary-reftype}{\B{reftype}} .. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}} .. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}} @@ -661,8 +667,8 @@ .. Types, non-terminals .. |Tnumtype| mathdef:: \xref{text/types}{text-numtype}{\T{numtype}} -.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}} .. |Theaptype| mathdef:: \xref{text/types}{text-heaptype}{\T{heaptype}} +.. |Treftype| mathdef:: \xref{text/types}{text-reftype}{\T{reftype}} .. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}} .. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}} @@ -774,8 +780,17 @@ .. |ok| mathdef:: \mathrel{\mbox{ok}} .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} -.. |matchesvaltype| mathdef:: \xref{valid/types}{match-valtype}{\leq} -.. |matchesresulttype| mathdef:: \xref{valid/types}{match-resulttype}{\leq} +.. |matchesnumtype| mathdef:: \xref{valid/matching}{match-numtype}{\leq} +.. |matchesheaptype| mathdef:: \xref{valid/matching}{match-heaptype}{\leq} +.. |matchesreftype| mathdef:: \xref{valid/matching}{match-reftype}{\leq} +.. |matchesvaltype| mathdef:: \xref{valid/matching}{match-valtype}{\leq} +.. |matchesresulttype| mathdef:: \xref{valid/matching}{match-resulttype}{\leq} +.. |matchesfunctype| mathdef:: \xref{valid/matching}{match-functype}{\leq} +.. |matchestabletype| mathdef:: \xref{valid/matching}{match-tabletype}{\leq} +.. |matchesmemtype| mathdef:: \xref{valid/matching}{match-memtype}{\leq} +.. |matchesglobaltype| mathdef:: \xref{valid/matching}{match-globaltype}{\leq} +.. |matchesexterntype| mathdef:: \xref{exec/matching}{match-externtype}{\leq} +.. |matcheslimits| mathdef:: \xref{exec/matching}{match-limits}{\leq} .. Contexts @@ -795,6 +810,11 @@ .. Judgments +.. |vdashnumtype| mathdef:: \xref{valid/types}{valid-numtype}{\vdash} +.. |vdashheaptype| mathdef:: \xref{valid/types}{valid-heaptype}{\vdash} +.. |vdashreftype| mathdef:: \xref{valid/types}{valid-reftype}{\vdash} +.. |vdashvaltype| mathdef:: \xref{valid/types}{valid-valtype}{\vdash} +.. |vdashresulttype| mathdef:: \xref{valid/types}{valid-resulttype}{\vdash} .. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash} .. |vdashblocktype| mathdef:: \xref{valid/types}{valid-blocktype}{\vdash} .. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} @@ -803,10 +823,17 @@ .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} -.. |vdashnumtypematch| mathdef:: \xref{valid/types}{match-numtype}{\vdash} -.. |vdashreftypematch| mathdef:: \xref{valid/types}{match-reftype}{\vdash} -.. |vdashvaltypematch| mathdef:: \xref{valid/types}{match-valtype}{\vdash} -.. |vdashresulttypematch| mathdef:: \xref{valid/types}{match-resulttype}{\vdash} +.. |vdashnumtypematch| mathdef:: \xref{valid/matching}{match-numtype}{\vdash} +.. |vdashheaptypematch| mathdef:: \xref{valid/matching}{match-heaptype}{\vdash} +.. |vdashreftypematch| mathdef:: \xref{valid/matching}{match-reftype}{\vdash} +.. |vdashvaltypematch| mathdef:: \xref{valid/matching}{match-valtype}{\vdash} +.. |vdashresulttypematch| mathdef:: \xref{valid/matching}{match-resulttype}{\vdash} +.. |vdashfunctypematch| mathdef:: \xref{valid/matching}{match-functype}{\vdash} +.. |vdashtabletypematch| mathdef:: \xref{valid/matching}{match-tabletype}{\vdash} +.. |vdashmemtypematch| mathdef:: \xref{valid/matching}{match-memtype}{\vdash} +.. |vdashglobaltypematch| mathdef:: \xref{valid/matching}{match-globaltype}{\vdash} +.. |vdashexterntypematch| mathdef:: \xref{exec/matching}{match-externtype}{\vdash} +.. |vdashlimitsmatch| mathdef:: \xref{exec/matching}{match-limits}{\vdash} .. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash} .. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash} @@ -814,6 +841,7 @@ .. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} .. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} +.. |vdashtypes| mathdef:: \xref{valid/modules}{valid-types}{\vdash} .. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} .. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} .. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} @@ -837,8 +865,6 @@ .. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow} .. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq} -.. |matchesexterntype| mathdef:: \xref{exec/modules}{match-externtype}{\leq} -.. |matcheslimits| mathdef:: \xref{exec/modules}{match-limits}{\leq} .. Allocation @@ -1092,9 +1118,6 @@ .. |vdashexternval| mathdef:: \xref{exec/modules}{valid-externval}{\vdash} -.. |vdashlimitsmatch| mathdef:: \xref{exec/modules}{match-limits}{\vdash} -.. |vdashexterntypematch| mathdef:: \xref{exec/modules}{match-externtype}{\vdash} - .. Soundness .. --------- diff --git a/document/core/valid/index.rst b/document/core/valid/index.rst index 34cf3b90..cd5fce18 100644 --- a/document/core/valid/index.rst +++ b/document/core/valid/index.rst @@ -8,5 +8,6 @@ Validation conventions types + matching instructions modules diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 2594a1e0..9478e96c 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -201,17 +201,19 @@ Reference Instructions * The function :math:`C.\CFUNCS[x]` must be defined in the context. +* There must exist a :ref:`type index ` :math:`y` such that :math:`C.\CTYPES[y]` is the same :ref:`function type ` as :math:`C.\CFUNCS[x]`. + * The :ref:`function index ` :math:`x` must be contained in :math:`C.\CREFS`. -* The instruction is valid with type :math:`[] \to [\FUNCREF]`. +* The instruction is valid with type :math:`[] \to [(\REF~y)]`. .. math:: \frac{ - C.\CFUNCS[x] = \functype + C.\CFUNCS[x] = C.\CTYPES[y] \qquad x \in C.\CREFS }{ - C \vdashinstr \REFFUNC~x : [] \to [\FUNCREF] + C \vdashinstr \REFFUNC~x : [] \to [(\REF~y)] } @@ -248,22 +250,27 @@ Parametric Instructions * If :math:`t^\ast` is present, then: + * The :ref:`result type ` :math:`[t^\ast]` must be :ref:`valid `. + * The length of :math:`t^\ast` must be :math:`1`. * Then the instruction is valid with type :math:`[t^\ast~t^\ast~\I32] \to [t^\ast]`. * Else: - * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`value type ` :math:`t` that :ref:`matches ` some :ref:`number type `. + * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`valid ` :ref:`value type ` :math:`t` that :ref:`matches ` some :ref:`number type `. .. math:: \frac{ + C \vdashresulttype [t] \ok }{ C \vdashinstr \SELECT~t : [t~t~\I32] \to [t] } \qquad \frac{ - \vdashvaltypematch t \matchesvaltype \numtype + C \vdashresulttype [t] \ok + \qquad + C \vdashresulttypematch [t] \matchesresulttype [\numtype] }{ C \vdashinstr \SELECT : [t~t~\I32] \to [t] } @@ -501,7 +508,7 @@ Table Instructions \qquad C.\CTABLES[x] = \limits_2~t_2 \qquad - \vdashreftypematch t_2 \matchesvaltype t_1 + C \vdashreftypematch t_2 \matchesvaltype t_1 }{ C \vdashinstr \TABLECOPY~x~y : [\I32~\I32~\I32] \to [] } @@ -530,7 +537,7 @@ Table Instructions \qquad C.\CELEMS[y] = t_2 \qquad - \vdashreftypematch t_2 \matchesvaltype t_1 + C \vdashreftypematch t_2 \matchesvaltype t_1 }{ C \vdashinstr \TABLEINIT~x~y : [\I32~\I32~\I32] \to [] } @@ -778,10 +785,11 @@ Control Instructions :math:`\UNREACHABLE` .................... -* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \UNREACHABLE : [t_1^\ast] \to [t_2^\ast] } @@ -885,11 +893,13 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ C.\CLABELS[l] = [t^\ast] + \qquad + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast] } @@ -942,13 +952,15 @@ Control Instructions * For all :math:`l_i` in :math:`l^\ast`, the result type :math:`[t^\ast]` :ref:`matches ` :math:`C.\CLABELS[l_i]`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - (\vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l])^\ast + (C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l])^\ast \qquad - \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l_N] + C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l_N] + \qquad + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \BRTABLE~l^\ast~l_N : [t_1^\ast~t^\ast~\I32] \to [t_2^\ast] } @@ -972,11 +984,13 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` of :math:`C.\CRETURN`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`valid ` :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ C.\CRETURN = [t^\ast] + \qquad + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok }{ C \vdashinstr \RETURN : [t_1^\ast~t^\ast] \to [t_2^\ast] } @@ -1015,7 +1029,7 @@ Control Instructions * Let :math:`\limits~t` be the :ref:`table type ` :math:`C.\CTABLES[x]`. -* The :ref:`reference type ` :math:`t` must :ref:`match ` type |FUNCREF|. +* The :ref:`reference type ` :math:`t` must :ref:`match ` type :math:`\REF~\NULL~\FUNC`. * The type :math:`C.\CTYPES[y]` must be defined in the context. @@ -1027,7 +1041,7 @@ Control Instructions \frac{ C.\CTABLES[x] = \limits~t \qquad - \vdashvaltypematch t \leq \FUNCREF + C \vdashvaltypematch t \matchesreftype \REF~\NULL~\FUNC \qquad C.\CTYPES[y] = [t_1^\ast] \to [t_2^\ast] }{ @@ -1077,7 +1091,7 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` \frac{ C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~{t'}^\ast] \qquad - (\vdashvaltypematch t' \matchesvaltype t)^\ast + (C \vdashvaltypematch t' \matchesvaltype t)^\ast \qquad C \vdashinstr \instr_N : [t^\ast] \to [t_3^\ast] }{ @@ -1102,7 +1116,7 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`type ` :math:`[] \to [{t'}^\ast]`. -* For each :ref:`value type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. +* For each :ref:`value type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`valid ` :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. * Then the expression is valid with :ref:`result type ` :math:`[t^\ast]`. @@ -1110,7 +1124,9 @@ Expressions :math:`\expr` are classified by :ref:`result types ` when checking the types of imports. + +.. todo:: externtype matching is used on semantic types; need to define how to reinterpret C for semantic types + + +.. index:: number type +.. _match-numtype: + +Number Types +~~~~~~~~~~~~ + +A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number type ` :math:`\numtype_2` if and only if: + +* Both :math:`\numtype_1` and :math:`\numtype_2` are the same. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashnumtypematch \numtype \matchesvaltype \numtype + } + + +.. index:: heap type +.. _match-heaptype: + +Heap Types +~~~~~~~~~~ + +A :ref:`heap type ` :math:`\heaptype_1` matches a :ref:`heap type ` :math:`\heaptype_2` if and only if: + +* Either both :math:`\heaptype_1` and :math:`\heaptype_2` are the same. + +* Or :math:`\heaptype_1` is a :ref:`type index ` that defines a function type and :math:`\heaptype_2` is :math:`FUNC`. + +* Or :math:`\heaptype_1` is a :ref:`type index ` that defines a function type :math:`\functype_1`, and :math:`\heaptype_2` is a :ref:`type index ` that defines a function type :math:`\functype_2`, and :math:`\functype_1` :ref:`matches ` :math:`\functype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashheaptypematch \heaptype \matchesheaptype \heaptype + } + \qquad + \frac{ + C.\CTYPES[\typeidx] = \functype + }{ + C \vdashheaptypematch \typeidx \matchesheaptype \FUNC + } + +.. math:: + ~\\[-1ex] + \frac{ + C.\CTYPES[\typeidx_1] = \functype_1 + \qquad + C.\CTYPES[\typeidx_2] = \functype_2 + \qquad + C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2 + }{ + C \vdashheaptypematch \typeidx_1 \matchesheaptype \typeidx_2 + } + + +.. index:: reference type +.. _match-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +A :ref:`reference type ` :math:`\REF~\NULL_1^?~heaptype_1` matches a :ref:`reference type ` :math:`\REF~\NULL_2^?~heaptype_2` if and only if: + +* The :ref:`heap type ` :math:`\heaptype_1` :ref:`matches ` :math:`\heaptype_2`. + +* :math:`\NULL_1` is absent or :math:`\NULL_2` is present. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 + }{ + C \vdashreftypematch \REF~\heaptype_1 \matchesreftype \REF~\heaptype_2 + } + \qquad + \frac{ + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 + }{ + C \vdashreftypematch \REF~\NULL~\heaptype_1 \matchesreftype \REF~\NULL^?~\heaptype_2 + } + + +.. index:: value type, number type, reference type +.. _match-valtype: + +Value Types +~~~~~~~~~~~ + +A :ref:`value type ` :math:`\valtype_1` matches a :ref:`value type ` :math:`\valtype_2` if and only if: + +* Either both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`number types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + +* Or both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`reference types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. + +* Or :math:`\valtype_1` is :math:`\BOT`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashvaltypematch \BOT \matchesvaltype \valtype + } + + +.. index:: result type, value type +.. _match-resulttype: + +Result Types +~~~~~~~~~~~~ + +Subtyping is lifted to :ref:`result types ` in a pointwise manner. +That is, a :ref:`result type ` :math:`[t_1^\ast]` matches a :ref:`result type ` :math:`[t_2^\ast]` if and only if: + +* Every :ref:`value type ` :math:`t_1` in :math:`[t_1^\ast]` :ref:`matches ` the corresponding :ref:`value type ` :math:`t_2` in :math:`[t_2^\ast]`. + +.. math:: + ~\\[-1ex] + \frac{ + (C \vdashvaltypematch t_1 \matchesvaltype t_2)^\ast + }{ + C \vdashresulttypematch [t_1^\ast] \matchesresulttype [t_2^\ast] + } + + +.. index:: function type, result type +.. _match-functype: + +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] \to [t_{12}^\ast]` matches a type :math:`[t_{21}^ast] \to [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_{12}^\ast]` :ref:`matches ` :math:`[t_{22}^\ast]`, and vice versa. + +.. math:: + ~\\[-1ex] + \frac{ + \begin{array}{@{}c@{}} + C \vdashresulttypematch [t_{11}^\ast] \matchesresulttype [t_{21}^\ast] + \qquad + C \vdashresulttypematch [t_{12}^\ast] \matchesresulttype [t_{22}^\ast] + \\ + C \vdashresulttypematch [t_{21}^\ast] \matchesresulttype [t_{11}^\ast] + \qquad + C \vdashresulttypematch [t_{22}^\ast] \matchesresulttype [t_{12}^\ast] + \end{array} + }{ + C \vdashfunctypematch [t_{11}^\ast] \to [t_{12}^\ast] \matchesfunctype [t_{21}^\ast] \to [t_{22}^\ast] + } + +.. note:: + In future versions of WebAssembly, subtyping on function types may be relaxed to support co- and contra-variance. + + +.. index:: limits +.. _match-limits: + +Limits +~~~~~~ + +:ref:`Limits ` :math:`\{ \LMIN~n_1, \LMAX~m_1^? \}` match limits :math:`\{ \LMIN~n_2, \LMAX~m_2^? \}` if and only if: + +* :math:`n_1` is larger than or equal to :math:`n_2`. + +* Either: + + * :math:`m_2^?` is empty. + +* Or: + + * Both :math:`m_1^?` and :math:`m_2^?` are non-empty. + + * :math:`m_1` is smaller than or equal to :math:`m_2`. + +.. math:: + ~\\[-1ex] + \frac{ + n_1 \geq n_2 + }{ + C \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matcheslimits \{ \LMIN~n_2, \LMAX~\epsilon \} + } + \quad + \frac{ + n_1 \geq n_2 + \qquad + m_1 \leq m_2 + }{ + C \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matcheslimits \{ \LMIN~n_2, \LMAX~m_2 \} + } + + +.. index:: table type, limits, element type +.. _match-tabletype: + +Table Types +~~~~~~~~~~~ + +A :ref:`table type ` :math:`(\limits_1~\reftype_1)` matches :math:`(\limits_2~\reftype_2)` if and only if: + +* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. + +* The :ref:`reference type ` :math:`\reftype_1` :ref:`matches ` :math:`\reftype_2`, and vice versa. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 + \qquad + C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2 + \qquad + C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1 + }{ + C \vdashtabletypematch \limits_1~\reftype_1 \matchestabletype \limits_2~\reftype_2 + } + + +.. index:: memory type, limits +.. _match-memtype: + +Memory Types +~~~~~~~~~~~~ + +A :ref:`memory type ` :math:`\limits_1` matches :math:`\limits_2` if and only if: + +* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. + + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 + }{ + C \vdashmemtypematch \limits_1 \matchesmemtype \limits_2 + } + + +.. index:: global type, value type, mutability +.. _match-globaltype: + +Global Types +~~~~~~~~~~~~ + +A :ref:`global type ` :math:`(\mut_1~t_1)` matches :math:`(\mut_2~t_2)` if and only if: + +* Either both :math:`\mut_1` and :math:`\mut_2` are |MVAR| and :math:`t_1` and :math:`t_2` are the same. + +* Or both :math:`\mut_1` and :math:`\mut_2` are |MCONST| and :math:`t_1` :ref:`matches ` :math:`t_2`. + +.. math:: + ~\\[-1ex] + \frac{ + }{ + C \vdashglobaltypematch \MVAR~t \matchesglobaltype \MVAR~t + } + \qquad + \frac{ + C \vdashvaltypematch t_1 \matchesvaltype t_2 + }{ + C \vdashglobaltypematch \MCONST~t_1 \matchesglobaltype \MCONST~t_2 + } + + +.. index:: external type, function type, table type, memory type, global type +.. _match-externtype: + +External Types +~~~~~~~~~~~~~~ + +Functions +......... + +An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches :math:`\ETFUNC~\functype_2` if and only if: + +* Function type :math:`\functype_1` :ref:`matches ` :math:`\functype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashfunctypematch \functype_1 \matchesfunctype \functype_2 + }{ + C \vdashexterntypematch \ETFUNC~\functype_1 \matchesexterntype \ETFUNC~\functype_2 + } + + +Tables +...... + +An :ref:`external type ` :math:`\ETTABLE~\tabletype_1` matches :math:`\ETTABLE~\tabletype_2` if and only if: + +* Table type :math:`\tabletype_1` :ref:`matches ` :math:`\tabletype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashtabletypematch \tabletype_1 \matchestabletype \tabletype_2 + }{ + C \vdashexterntypematch \ETTABLE~\tabletype_1 \matchesexterntype \ETTABLE~\tabletype_2 + } + + +Memories +........ + +An :ref:`external type ` :math:`\ETMEM~\memtype_1` matches :math:`\ETMEM~\memtype_2` if and only if: + +* Memory type :math:`\memtype_1` :ref:`matches ` :math:`\memtype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashmemtypematch \memtype_1 \matchesmemtype \memtype_2 + }{ + C \vdashexterntypematch \ETMEM~\memtype_1 \matchesexterntype \ETMEM~\memtype_2 + } + + +Globals +....... + +An :ref:`external type ` :math:`\ETGLOBAL~\globaltype_1` matches :math:`\ETGLOBAL~\globaltype_2` if and only if: + +* Global type :math:`\globaltype_1` :ref:`matches ` :math:`\globaltype_2`. + +.. math:: + ~\\[-1ex] + \frac{ + C \vdashglobaltypematch \globaltype_1 \matchesglobaltype \globaltype_2 + }{ + C \vdashexterntypematch \ETGLOBAL~\globaltype_1 \matchesexterntype \ETGLOBAL~\globaltype_2 + } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 87546493..1d28153c 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -67,7 +67,7 @@ Tables :math:`\table` are classified by :ref:`table types `. .. math:: \frac{ - \vdashtabletype \tabletype \ok + C \vdashtabletype \tabletype \ok }{ C \vdashtable \{ \TTYPE~\tabletype \} : \tabletype } @@ -92,7 +92,7 @@ Memories :math:`\mem` are classified by :ref:`memory types `. .. math:: \frac{ - \vdashmemtype \memtype \ok + C \vdashmemtype \memtype \ok }{ C \vdashmem \{ \MTYPE~\memtype \} : \memtype } @@ -122,7 +122,7 @@ Globals :math:`\global` are classified by :ref:`global types .. math:: \frac{ - \vdashglobaltype \mut~t \ok + C \vdashglobaltype \mut~t \ok \qquad C \vdashexpr \expr : [t] \qquad @@ -147,6 +147,8 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`t` must be :ref:`valid `. + * For each :math:`e_i` in :math:`e^\ast`, * The expression :math:`e_i` must be :ref:`valid `. @@ -155,20 +157,22 @@ Element segments :math:`\elem` are classified by the :ref:`reference type ` :math:`t'`. -* The :ref:`reference type ` :math:`t` must :ref:`match ` the reference type :math:`t'`. +* The reference type :math:`t` must :ref:`match ` the reference type :math:`t'`. * Then the element segment is valid with :ref:`reference type ` :math:`t`. .. math:: \frac{ + C \vdashreftype t \ok + \qquad (C \vdashexpr e \ok)^\ast \qquad (C \vdashexprconst e \const)^\ast \qquad C \vdashelemmode \elemmode : t' \qquad - \vdashreftypematch t \matchesvaltype t' + C \vdashreftypematch t \matchesreftype t' }{ C \vdashelem \{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \} : t } @@ -179,10 +183,11 @@ Element segments :math:`\elem` are classified by the :ref:`reference type `. +* The element mode is valid with any :ref:`valid ` :ref:`reference type `. .. math:: \frac{ + C \vdashreftype \reftype \ok }{ C \vdashelemmode \EPASSIVE : \reftype } @@ -217,10 +222,11 @@ Element segments :math:`\elem` are classified by the :ref:`reference type `. +* The element mode is valid with any :ref:`valid ` :ref:`reference type `. .. math:: \frac{ + C \vdashreftype \reftype \ok }{ C \vdashelemmode \EDECLARATIVE : \reftype } @@ -436,7 +442,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi :math:`\IDFUNC~x` ................. -* The function :math:`C.\CTYPES[x]` must be defined in the context. +* The function type :math:`C.\CTYPES[x]` must be defined in the context. * Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. @@ -459,7 +465,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \vdashtable \tabletype \ok + C \vdashtable \tabletype \ok }{ C \vdashimportdesc \IDTABLE~\tabletype : \ETTABLE~\tabletype } @@ -474,7 +480,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \vdashmemtype \memtype \ok + C \vdashmemtype \memtype \ok }{ C \vdashimportdesc \IDMEM~\memtype : \ETMEM~\memtype } @@ -489,7 +495,7 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - \vdashglobaltype \globaltype \ok + C \vdashglobaltype \globaltype \ok }{ C \vdashimportdesc \IDGLOBAL~\globaltype : \ETGLOBAL~\globaltype } @@ -540,21 +546,26 @@ Instead, the context :math:`C` for validation of the module's content is constru * :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 `. -* Let :math:`C'` be the :ref:`context ` where: +* For each function type :math:`\functype_i` in :math:`\module.\MTYPES`: + + * Let :math:`C'_i` be the :ref:`context ` where :math:`C'_i.\CTYPES` is :math:`C.\CTYPES[0 \slice i]` and all other fields are empty. + + * The function :math:`\functype_i` must be :ref:`valid ` under context :math:`C'_i`. + +* Let :math:`C''` be the :ref:`context ` where: - * :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`, + * :math:`C''.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)`, - * :math:`C'.\CFUNCS` is the same as :math:`C.\CFUNCS`, + * :math:`C''.\CTYPES` is the same as :math:`C.\CTYPES`, - * :math:`C'.\CREFS` is the same as :math:`C.\CREFS`, + * :math:`C''.\CFUNCS` is the same as :math:`C.\CFUNCS`, + + * :math:`C''.\CREFS` is the same as :math:`C.\CREFS`, * all other fields are empty. * Under the context :math:`C`: - * For each :math:`\functype_i` in :math:`\module.\MTYPES`, - the :ref:`function type ` :math:`\functype_i` must be :ref:`valid `. - * For each :math:`\func_i` in :math:`\module.\MFUNCS`, the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. @@ -566,7 +577,7 @@ Instead, the context :math:`C` for validation of the module's content is constru * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: - * Under the context :math:`C'`, + * Under the context :math:`C''`, the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEMS`, @@ -607,7 +618,7 @@ Instead, the context :math:`C` for validation of the module's content is constru .. math:: \frac{ \begin{array}{@{}c@{}} - (\vdashfunctype \type \ok)^\ast + \vdashtypes \type^\ast \ok \quad (C \vdashfunc \func : \X{ft})^\ast \quad @@ -615,7 +626,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C \vdashmem \mem : \X{mt})^\ast \quad - (C' \vdashglobal \global : \X{gt})^\ast + (C'' \vdashglobal \global : \X{gt})^\ast \\ (C \vdashelem \elem : \X{rt})^\ast \quad @@ -639,7 +650,9 @@ Instead, the context :math:`C` for validation of the module's content is constru \\ 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' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} + (C' = \{ \CTYPES~\type^\ast \})^\ast + \\ + C'' = \{ \CTYPES~\type^\ast, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} \qquad |C.\CMEMS| \leq 1 \qquad @@ -663,6 +676,25 @@ Instead, the context :math:`C` for validation of the module's content is constru \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 1b790bb4..1fd575b1 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -1,14 +1,147 @@ Types ----- -Most :ref:`types ` are universally valid. -However, restrictions apply to :ref:`function types ` as well as the :ref:`limits ` of :ref:`table types ` and :ref:`memory types `, which must be checked during validation. - -On :ref:`value types `, a simple notion of subtyping is defined. +Simple :ref:`types `, such as :ref:`number types ` are universally valid. +However, restrictions apply to most other types, such as :ref:`reference types `, :ref:`function types `, as well as the :ref:`limits ` of :ref:`table types ` and :ref:`memory types `, which must be checked during validation. Moreover, :ref:`block types ` are converted to plain :ref:`function types ` for ease of processing. +.. index:: number type + pair: validation; number type + single: abstract syntax; number type +.. _valid-numtype: + +Number Types +~~~~~~~~~~~~ + +:ref:`Number types ` are always valid. + +.. math:: + \frac{ + }{ + C \vdashnumtype \numtype \ok + } + + +.. index:: heap type + pair: validation; heap type + single: abstract syntax; heap type +.. _valid-heaptype: + +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` +............... + +* The heap type is valid. + +.. math:: + \frac{ + }{ + C \vdashheaptype \EXTERN \ok + } + +:math:`\typeidx` +................ + +* The type :math:`C.\CTYPES[\typeidx]` must be defined in the context. + +* Then the heap type is valid. + +.. math:: + \frac{ + C.\CTYPES[\typeidx] = \functype + }{ + C \vdashheaptype \typeidx \ok + } + + +.. index:: reference type, heap type + pair: validation; reference type + single: abstract syntax; reference type +.. _valid-reftype: + +Reference Types +~~~~~~~~~~~~~~~ + +:ref:`Reference types ` are valid when the referenced :ref:`heap type ` is. + +:math:`\REF~\NULL^?~\heaptype` +.............................. + +* The heap type :math:`\heaptype` must be :ref:`valid `. + +* Then the reference type is valid. + +.. math:: + \frac{ + C \vdashreftype \heaptype \ok + }{ + C \vdashreftype \REF~\NULL^?~\heaptype \ok + } + + +.. index:: value type, reference type, heap type, bottom type + pair: validation; value type + single: abstract syntax; value type +.. _valid-valtype: +.. _valid-bottype: + +Value Types +~~~~~~~~~~~ + +Valid :ref:`value types ` are either valid :ref:`number type `, :ref:`reference type `, or the :ref:`bottom type `. + +:math:`\BOT` +............ + +* The value type is valid. + +.. math:: + \frac{ + }{ + C \vdashvaltype \BOT \ok + } + + +.. index:: result type, value type + pair: validation; result type + single: abstract syntax; result type +.. _valid-resulttype: + +Result Types +~~~~~~~~~~~~ + +:math:`[t^\ast]` +................ + +* Each :ref:`value type ` :math:`t_i` in the type sequence :math:`t^\ast` must be :ref:`valid `. + +* Then the result type is valid. + +.. math:: + \frac{ + (C \vdashvaltype t \ok)^\ast + }{ + C \vdashresulttype [t^\ast] \ok + } + + .. index:: limits pair: validation; limits single: abstract syntax; limits @@ -40,7 +173,7 @@ Limits \qquad (n \leq m)^? }{ - \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k + C \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k } @@ -72,10 +205,13 @@ Block Types :math:`[\valtype^?]` .................... -* The block type is valid as :ref:`function type ` :math:`[] \to [\valtype^?]`. +* The value type :math:`\valtype` must either be absent, or :ref:`valid `. + +* Then the block type is valid as :ref:`function type ` :math:`[] \to [\valtype^?]`. .. math:: \frac{ + (C \vdashvaltype \valtype \ok)^? }{ C \vdashblocktype [\valtype^?] : [] \to [\valtype^?] } @@ -89,17 +225,22 @@ Block Types Function Types ~~~~~~~~~~~~~~ -:ref:`Function types ` are always valid. +:math:`[t_1^\ast] \to [t_2^\ast]` +................................. -:math:`[t_1^n] \to [t_2^m]` -........................... +* The :ref:`result type ` :math:`[t_1^\ast]` must be :ref:`valid `. -* The function type is valid. +* The :ref:`result type ` :math:`[t_2^\ast]` must be :ref:`valid `. + +* Then the function type is valid. .. math:: \frac{ + C \vdashvaltype [t_1^\ast] \ok + \qquad + C \vdashvaltype [t_2^\ast] \ok }{ - \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok + C \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok } @@ -116,13 +257,17 @@ Table Types * The limits :math:`\limits` must be :ref:`valid ` within range :math:`2^{32}-1`. +* The reference type :math:`\reftype` must be :ref:`valid `. + * Then the table type is valid. .. math:: \frac{ - \vdashlimits \limits : 2^{32} - 1 + C \vdashlimits \limits : 2^{32} - 1 + \qquad + C \vdashreftype \reftype \ok }{ - \vdashtabletype \limits~\reftype \ok + C \vdashtabletype \limits~\reftype \ok } @@ -143,9 +288,9 @@ Memory Types .. math:: \frac{ - \vdashlimits \limits : 2^{16} + C \vdashlimits \limits : 2^{16} }{ - \vdashmemtype \limits \ok + C \vdashmemtype \limits \ok } @@ -160,12 +305,15 @@ Global Types :math:`\mut~\valtype` ..................... -* The global type is valid. +* The value type :math:`\valtype` must be :ref:`valid `. + +* Then the global type is valid. .. math:: \frac{ + C \vdashreftype \valtype \ok }{ - \vdashglobaltype \mut~\valtype \ok + C \vdashglobaltype \mut~\valtype \ok } @@ -186,9 +334,9 @@ External Types .. math:: \frac{ - \vdashfunctype \functype \ok + C \vdashfunctype \functype \ok }{ - \vdashexterntype \ETFUNC~\functype \ok + C \vdashexterntype \ETFUNC~\functype \ok } :math:`\ETTABLE~\tabletype` @@ -200,9 +348,9 @@ External Types .. math:: \frac{ - \vdashtabletype \tabletype \ok + C \vdashtabletype \tabletype \ok }{ - \vdashexterntype \ETTABLE~\tabletype \ok + C \vdashexterntype \ETTABLE~\tabletype \ok } :math:`\ETMEM~\memtype` @@ -214,9 +362,9 @@ External Types .. math:: \frac{ - \vdashmemtype \memtype \ok + C \vdashmemtype \memtype \ok }{ - \vdashexterntype \ETMEM~\memtype \ok + C \vdashexterntype \ETMEM~\memtype \ok } :math:`\ETGLOBAL~\globaltype` @@ -228,226 +376,7 @@ External Types .. math:: \frac{ - \vdashglobaltype \globaltype \ok - }{ - \vdashexterntype \ETGLOBAL~\globaltype \ok - } - - -.. index:: subtyping - -Value Subtyping -~~~~~~~~~~~~~~~ - -.. index:: number type - -.. _match-numtype: - -Number Types -............ - -A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number type ` :math:`\numtype_2` if and only if: - -* Both :math:`\numtype_1` and :math:`\numtype_2` are the same. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashnumtypematch \numtype \matchesvaltype \numtype - } - - - -.. index:: reference type - -.. _match-reftype: - -Reference Types -............... - -A :ref:`reference type ` :math:`\reftype_1` matches a :ref:`reference type ` :math:`\reftype_2` if and only if: - -* Either both :math:`\reftype_1` and :math:`\reftype_2` are the same. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashreftypematch \reftype \matchesvaltype \reftype - } - - -.. index:: value type, number type, reference type - -.. _match-valtype: - -Value Types -........... - -A :ref:`value type ` :math:`\valtype_1` matches a :ref:`value type ` :math:`\valtype_2` if and only if: - -* Either both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`number types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. - -* Or both :math:`\valtype_1` and :math:`\valtype_2` are :ref:`reference types ` and :math:`\valtype_1` :ref:`matches ` :math:`\valtype_2`. - -* Or :math:`\valtype_1` is :math:`\BOT`. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashvaltypematch \BOT \matchesvaltype \valtype - } - - -.. _match-resulttype: - -Result Types -............ - -Subtyping is lifted to :ref:`result types ` in a pointwise manner. -That is, a :ref:`result type ` :math:`[t_1^\ast]` matches a :ref:`result type ` :math:`[t_2^\ast]` if and only if: - -* Every :ref:`value type ` :math:`t_1` in :math:`[t_1^\ast]` :ref:`matches ` the corresponding :ref:`value type ` :math:`t_2` in :math:`[t_2^\ast]`. - -.. math:: - ~\\[-1ex] - \frac{ - (\vdashvaltypematch t_1 \matchesvaltype t_2)^\ast - }{ - \vdashresulttypematch [t_1^\ast] \matchesresulttype [t_2^ast] - } - - -.. index:: ! matching, external type -.. _exec-import: -.. _match: - -Import Subtyping -~~~~~~~~~~~~~~~~ - -When :ref:`instantiating ` a module, -:ref:`external values ` must be provided whose :ref:`types ` are *matched* against the respective :ref:`external types ` classifying each import. -In some cases, this allows for a simple form of subtyping, as defined here. - - -.. index:: limits -.. _match-limits: - -Limits -...... - -:ref:`Limits ` :math:`\{ \LMIN~n_1, \LMAX~m_1^? \}` match limits :math:`\{ \LMIN~n_2, \LMAX~m_2^? \}` if and only if: - -* :math:`n_1` is larger than or equal to :math:`n_2`. - -* Either: - - * :math:`m_2^?` is empty. - -* Or: - - * Both :math:`m_1^?` and :math:`m_2^?` are non-empty. - - * :math:`m_1` is smaller than or equal to :math:`m_2`. - -.. math:: - ~\\[-1ex] - \frac{ - n_1 \geq n_2 - }{ - \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matcheslimits \{ \LMIN~n_2, \LMAX~\epsilon \} - } - \quad - \frac{ - n_1 \geq n_2 - \qquad - m_1 \leq m_2 - }{ - \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matcheslimits \{ \LMIN~n_2, \LMAX~m_2 \} - } - - -.. _match-externtype: - -.. index:: function type -.. _match-functype: - -Functions -......... - -An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches :math:`\ETFUNC~\functype_2` if and only if: - -* Both :math:`\functype_1` and :math:`\functype_2` are the same. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashexterntypematch \ETFUNC~\functype \matchesexterntype \ETFUNC~\functype - } - - -.. index:: table type, limits, element type -.. _match-tabletype: - -Tables -...... - -An :ref:`external type ` :math:`\ETTABLE~(\limits_1~\reftype_1)` matches :math:`\ETTABLE~(\limits_2~\reftype_2)` if and only if: - -* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. - -* Both :math:`\reftype_1` and :math:`\reftype_2` are the same. - -.. math:: - \frac{ - \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 - }{ - \vdashexterntypematch \ETTABLE~(\limits_1~\reftype) \matchesexterntype \ETTABLE~(\limits_2~\reftype) - } - - -.. index:: memory type, limits -.. _match-memtype: - -Memories -........ - -An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :math:`\ETMEM~\limits_2` if and only if: - -* Limits :math:`\limits_1` :ref:`match ` :math:`\limits_2`. - -.. math:: - \frac{ - \vdashlimitsmatch \limits_1 \matcheslimits \limits_2 - }{ - \vdashexterntypematch \ETMEM~\limits_1 \matchesexterntype \ETMEM~\limits_2 - } - - -.. index:: global type, value type, mutability -.. _match-globaltype: - -Globals -....... - -An :ref:`external type ` :math:`\ETGLOBAL~(\mut_1~t_1)` matches :math:`\ETGLOBAL~(\mut_2~t_2)` if and only if: - -* Either both :math:`\mut_1` and :math:`\mut_2` are |MVAR| and :math:`t_1` and :math:`t_2` are the same. - -* Or both :math:`\mut_1` and :math:`\mut_2` are |MCONST| and :math:`t_1` :ref:`matches ` :math:`t_2`. - -.. math:: - ~\\[-1ex] - \frac{ - }{ - \vdashexterntypematch \ETGLOBAL~(\MVAR~t) \matchesexterntype \ETGLOBAL~(\MVAR~t) - } - \qquad - \frac{ - \vdashvaltypematch t_1 \matchesvaltype t_2 + C \vdashglobaltype \globaltype \ok }{ - \vdashexterntypematch \ETGLOBAL~(\MCONST~t_1) \matchesexterntype \ETGLOBAL~(\MCONST~t_2) + C \vdashexterntype \ETGLOBAL~\globaltype \ok } diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 646d8a43..471e11d7 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -148,19 +148,25 @@ let num_type s = let heap_type s = let pos = pos s in - match vs33 s with - | -0x10l -> FuncHeapType - | -0x11l -> ExternHeapType - | i when i >= 0l -> DefHeapType (SynVar i) - | _ -> error s pos "malformed heap type" + match peek s with + | Some i when i land 0xc0 = 0x40 -> + (match vs7 s with + | -0x10 -> FuncHeapType + | -0x11 -> ExternHeapType + | _ -> error s pos "malformed heap type" + ) + | _ -> + match vs33 s with + | i when i >= 0l -> DefHeapType (SynVar i) + | _ -> error s pos "malformed heap type" let ref_type s = let pos = pos s in - match vs33 s with - | -0x10l -> (Nullable, FuncHeapType) - | -0x11l -> (Nullable, ExternHeapType) - | -0x14l -> (Nullable, heap_type s) - | -0x15l -> (NonNullable, heap_type s) + match vs7 s with + | -0x10 -> (Nullable, FuncHeapType) + | -0x11 -> (Nullable, ExternHeapType) + | -0x14 -> (Nullable, heap_type s) + | -0x15 -> (NonNullable, heap_type s) | _ -> error s pos "malformed reference type" let value_type s = diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 567dcc33..051606d9 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -108,10 +108,10 @@ struct | BotHeapType -> assert false let ref_type = function - | (Nullable, FuncHeapType) -> vs32 (-0x10l) - | (Nullable, ExternHeapType) -> vs32 (-0x11l) - | (Nullable, t) -> vs33 (-0x14l); heap_type t - | (NonNullable, t) -> vs33 (-0x15l); heap_type t + | (Nullable, FuncHeapType) -> vs7 (-0x10) + | (Nullable, ExternHeapType) -> vs7 (-0x11) + | (Nullable, t) -> vs7 (-0x14); heap_type t + | (NonNullable, t) -> vs7 (-0x15); heap_type t let value_type = function | NumType t -> num_type t