From 96ae61e1ff6ebe0e51e1e4faeb64e681067e8a53 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 24 Jun 2021 20:36:56 +0200 Subject: [PATCH 1/2] [spec] Add concrete ref types and surrounding semantics --- document/core/appendix/index-types.rst | 9 +- document/core/appendix/properties.rst | 4 +- document/core/binary/instructions.rst | 2 +- document/core/binary/types.rst | 30 ++- document/core/exec/runtime.rst | 1 + document/core/syntax/instructions.rst | 2 +- document/core/syntax/modules.rst | 2 +- document/core/syntax/types.rst | 36 ++- document/core/text/instructions.rst | 14 +- document/core/text/modules.rst | 26 +-- document/core/text/types.rst | 70 ++++-- document/core/util/macros.def | 25 ++- document/core/valid/instructions.rst | 38 +++- document/core/valid/modules.rst | 76 +++++-- document/core/valid/types.rst | 294 ++++++++++++++++++++++--- interpreter/binary/decode.ml | 16 +- interpreter/binary/encode.ml | 8 +- 17 files changed, 514 insertions(+), 139 deletions(-) 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..749616b9 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -4,6 +4,8 @@ Soundness --------- +.. todo:: need to ensure wf of nondet types and operate wrt semantic types + 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 +52,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{ diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 3529aab9..9da4e188 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -87,7 +87,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 85ee3250..67e378ae 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -6,8 +6,8 @@ Types ----- .. note:: - In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. - Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future. + In some places, possible types include both type constructors or types denoted by :ref:`type indices `. + Thus, the binary format for most type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices. .. index:: number type @@ -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/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 039d4cfb..67bc409e 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..33b6bfb7 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 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 45c2a059..0c350d00 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -70,17 +70,17 @@ 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 &::=& - \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? + \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? \\ &&&\qquad \Rightarrow\quad \BLOCK~\X{bt}~\X{in}^\ast~\END \qquad\quad~~ (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ &&|& - \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? + \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? \\ &&&\qquad \Rightarrow\quad \LOOP~\X{bt}~\X{in}^\ast~\END \qquad\qquad (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ &&|& - \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ + \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ \text{else}~~\Tid_1^?~~(\X{in}_2{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid_2^? \\ &&&\qquad \Rightarrow\quad \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \qquad (\iff \Tid_1^? = \epsilon \vee \Tid_1^? = \Tlabel, \Tid_2^? = \epsilon \vee \Tid_2^? = \Tlabel) \\ @@ -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 3e970ccf..dd900bcd 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}} @@ -307,7 +312,7 @@ .. Modules, non-terminals .. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}} -.. |type| mathdef:: \xref{syntax/modules}{syntax-typedef}{\X{type}} +.. |type| mathdef:: \xref{syntax/types}{syntax-functype}{\X{type}} .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} .. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}} @@ -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,11 @@ .. |ok| mathdef:: \mathrel{\mbox{ok}} .. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} +.. |matchesheaptype| mathdef:: \xref{valid/types}{match-heaptype}{\leq} +.. |matchesreftype| mathdef:: \xref{valid/types}{match-reftype}{\leq} .. |matchesvaltype| mathdef:: \xref{valid/types}{match-valtype}{\leq} .. |matchesresulttype| mathdef:: \xref{valid/types}{match-resulttype}{\leq} +.. |matchesfunctype| mathdef:: \xref{valid/types}{match-functype}{\leq} .. Contexts @@ -795,6 +804,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} @@ -804,9 +818,11 @@ .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} .. |vdashnumtypematch| mathdef:: \xref{valid/types}{match-numtype}{\vdash} +.. |vdashheaptypematch| mathdef:: \xref{valid/types}{match-heaptype}{\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} +.. |vdashfunctypematch| mathdef:: \xref{valid/types}{match-functype}{\vdash} .. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash} .. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash} @@ -814,6 +830,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} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 610c49cd..89c0c21e 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -248,22 +248,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] } @@ -569,7 +574,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32] \to [t]`. @@ -609,7 +614,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t] \to []`. @@ -778,10 +783,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 +891,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 +950,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 \qquad \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 +982,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 +1027,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 +1039,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] }{ @@ -1100,9 +1112,9 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`type ` :math:`[] \to [t^\ast]`. +* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` 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,6 +1122,8 @@ Expressions :math:`\expr` are classified by :ref:`result 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..da276506 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -1,13 +1,148 @@ 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. +On most types, a simple notion of subtyping is defined that is applicable in validation rules or during :ref:`module instantiation `. + + +.. 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 @@ -72,10 +207,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 +227,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 :ref:`result type ` :math:`[t_2^\ast]` must be :ref:`valid `. -* The function type is 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 +259,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 + \qquad + C \vdashreftype \reftype \ok }{ - \vdashtabletype \limits~\reftype \ok + C \vdashtabletype \limits~\reftype \ok } @@ -160,12 +307,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 +336,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 +350,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 +364,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,9 +378,9 @@ External Types .. math:: \frac{ - \vdashglobaltype \globaltype \ok + C \vdashglobaltype \globaltype \ok }{ - \vdashexterntype \ETGLOBAL~\globaltype \ok + C \vdashexterntype \ETGLOBAL~\globaltype \ok } @@ -258,6 +408,44 @@ A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number } +.. 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 + } + ~\\ + \frac{ + C.\CTYPES[\typeidx] = \functype + }{ + C \vdashheaptypematch \typeidx \matchesheaptype \FUNC + } + ~\\ + \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 @@ -266,15 +454,24 @@ A :ref:`number type ` :math:`\numtype_1` matches a :ref:`number Reference Types ............... -A :ref:`reference type ` :math:`\reftype_1` matches a :ref:`reference type ` :math:`\reftype_2` if and only if: +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`. -* Either both :math:`\reftype_1` and :math:`\reftype_2` are the same. +* :math:`\NULL_1` is absent or :math:`\NULL_2` is present. .. math:: ~\\[-1ex] \frac{ + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 }{ - \vdashreftypematch \reftype \matchesvaltype \reftype + C \vdashreftypematch \REF~\heaptype_1 \matchesreftype \REF~\heaptype_2 + } + ~\\[-1ex] + \frac{ + C \vdashheaptypematch \heaptype_1 \matchesheaptype \heaptype_2 + }{ + C \vdashreftypematch \REF~\NULL~\heaptype_1 \matchesreftype \REF~\NULL^?~\heaptype_2 } @@ -297,7 +494,7 @@ A :ref:`value type ` :math:`\valtype_1` matches a :ref:`value ty ~\\[-1ex] \frac{ }{ - \vdashvaltypematch \BOT \matchesvaltype \valtype + C \vdashvaltypematch \BOT \matchesvaltype \valtype } @@ -314,12 +511,45 @@ That is, a :ref:`result type ` :math:`[t_1^\ast]` matches a : .. math:: ~\\[-1ex] \frac{ - (\vdashvaltypematch t_1 \matchesvaltype t_2)^\ast + (C \vdashvaltypematch t_1 \matchesvaltype t_2)^\ast }{ - \vdashresulttypematch [t_1^\ast] \matchesresulttype [t_2^ast] + C \vdashresulttypematch [t_1^\ast] \matchesresulttype [t_2^ast] } +.. _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:: ! matching, external type .. _exec-import: .. _match: @@ -331,6 +561,8 @@ 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. +.. todo:: this requires semantics types + .. index:: limits .. _match-limits: @@ -372,7 +604,7 @@ Limits .. _match-externtype: .. index:: function type -.. _match-functype: +.. _match-externfunctype: Functions ......... @@ -390,7 +622,7 @@ An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches .. index:: table type, limits, element type -.. _match-tabletype: +.. _match-externtabletype: Tables ...... @@ -410,7 +642,7 @@ An :ref:`external type ` :math:`\ETTABLE~(\limits_1~\reftype_ .. index:: memory type, limits -.. _match-memtype: +.. _match-externmemtype: Memories ........ @@ -428,7 +660,7 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma .. index:: global type, value type, mutability -.. _match-globaltype: +.. _match-externglobaltype: Globals ....... diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 646d8a43..12d696e9 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -148,15 +148,19 @@ 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" + if peek s land 0xc0 = 0x40 then + match vs7 s with + | -0x10l -> FuncHeapType + | -0x11l -> ExternHeapType + | _ -> error s pos "malformed heap type" + else + 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 + match vs7 s with | -0x10l -> (Nullable, FuncHeapType) | -0x11l -> (Nullable, ExternHeapType) | -0x14l -> (Nullable, heap_type s) diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 567dcc33..60edb66c 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 (-0x10l) + | (Nullable, ExternHeapType) -> vs7 (-0x11l) + | (Nullable, t) -> vs7 (-0x14l); heap_type t + | (NonNullable, t) -> vs7 (-0x15l); heap_type t let value_type = function | NumType t -> num_type t From ea1e36c3ea7ffe2fa8b9767722305bc3ab204190 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 25 Jun 2021 08:52:34 +0200 Subject: [PATCH 2/2] [spec] New instructions --- .../core/appendix/gen-index-instructions.py | 12 +- document/core/appendix/index-instructions.rst | 548 +++++++++--------- document/core/binary/instructions.rst | 15 +- document/core/exec/instructions.rst | 125 +++- document/core/syntax/instructions.rst | 14 +- document/core/text/instructions.rst | 12 +- document/core/util/macros.def | 6 +- document/core/valid/instructions.rst | 120 +++- proposals/function-references/Overview.md | 2 +- 9 files changed, 528 insertions(+), 326 deletions(-) diff --git a/document/core/appendix/gen-index-instructions.py b/document/core/appendix/gen-index-instructions.py index 6191a07b..f366ae48 100755 --- a/document/core/appendix/gen-index-instructions.py +++ b/document/core/appendix/gen-index-instructions.py @@ -81,7 +81,7 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\CALLINDIRECT~x~y', r'\hex{11}', r'[t_1^\ast~\I32] \to [t_2^\ast]', r'valid-call_indirect', r'exec-call_indirect'), Instruction(None, r'\hex{12}'), Instruction(None, r'\hex{13}'), - Instruction(None, r'\hex{14}'), + Instruction(r'\CALLREF', r'\hex{14}', r'[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]', r'valid-call_ref', r'exec-call_ref'), Instruction(None, r'\hex{15}'), Instruction(None, r'\hex{16}'), Instruction(None, r'\hex{17}'), @@ -269,13 +269,13 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(None, r'\hex{CD}'), Instruction(None, r'\hex{CE}'), Instruction(None, r'\hex{CF}'), - Instruction(r'\REFNULL~t', r'\hex{D0}', r'[] \to [t]', r'valid-ref.null', r'exec-ref.null'), - Instruction(r'\REFISNULL', r'\hex{D1}', r'[t] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'), + Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'), + Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'), Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'), - Instruction(None, r'\hex{D3}'), - Instruction(None, r'\hex{D4}'), + Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'), + Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'), Instruction(None, r'\hex{D5}'), - Instruction(None, r'\hex{D6}'), + Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'), Instruction(None, r'\hex{D7}'), Instruction(None, r'\hex{D8}'), Instruction(None, r'\hex{D9}'), diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst index 55bf8fb9..545638b6 100644 --- a/document/core/appendix/index-instructions.rst +++ b/document/core/appendix/index-instructions.rst @@ -6,277 +6,277 @@ Index of Instructions --------------------- -========================================= ========================= ============================================= ======================================= =============================================================== -Instruction Binary Opcode Type Validation Execution -========================================= ========================= ============================================= ======================================= =============================================================== -:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\BLOCK~\X{bt}` :math:`\hex{02}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\LOOP~\X{bt}` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\IF~\X{bt}` :math:`\hex{04}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\ELSE` :math:`\hex{05}` -(reserved) :math:`\hex{06}` -(reserved) :math:`\hex{07}` -(reserved) :math:`\hex{08}` -(reserved) :math:`\hex{09}` -(reserved) :math:`\hex{0A}` -:math:`\END` :math:`\hex{0B}` -:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^\ast~\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALLINDIRECT~x~y` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{12}` -(reserved) :math:`\hex{13}` -(reserved) :math:`\hex{14}` -(reserved) :math:`\hex{15}` -(reserved) :math:`\hex{16}` -(reserved) :math:`\hex{17}` -(reserved) :math:`\hex{18}` -(reserved) :math:`\hex{19}` -:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\SELECT~t` :math:`\hex{1C}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{1D}` -(reserved) :math:`\hex{1E}` -(reserved) :math:`\hex{1F}` -:math:`\LOCALGET~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\LOCALSET~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\LOCALTEE~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GLOBALGET~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GLOBALSET~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEGET~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\TABLESET~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{27}` -:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution ` -:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation ` :ref:`execution ` -:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\WRAP\K{\_}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_}\I32\K{\_s}` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_}\I32\K{\_u}` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\DEMOTE\K{\_}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\PROMOTE\K{\_}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REINTERPRET\K{\_}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REINTERPRET\K{\_}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EXTEND\K{8\_s}` :math:`\hex{C0}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EXTEND\K{16\_s}` :math:`\hex{C1}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{8\_s}` :math:`\hex{C2}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{16\_s}` :math:`\hex{C3}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{32\_s}` :math:`\hex{C4}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -(reserved) :math:`\hex{C5}` -(reserved) :math:`\hex{C6}` -(reserved) :math:`\hex{C7}` -(reserved) :math:`\hex{C8}` -(reserved) :math:`\hex{C9}` -(reserved) :math:`\hex{CA}` -(reserved) :math:`\hex{CB}` -(reserved) :math:`\hex{CC}` -(reserved) :math:`\hex{CD}` -(reserved) :math:`\hex{CE}` -(reserved) :math:`\hex{CF}` -:math:`\REFNULL~t` :math:`\hex{D0}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\REFISNULL` :math:`\hex{D1}` :math:`[t] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\REFFUNC~x` :math:`\hex{D2}` :math:`[] \to [\FUNCREF]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{D3}` -(reserved) :math:`\hex{D4}` -(reserved) :math:`\hex{D5}` -(reserved) :math:`\hex{D6}` -(reserved) :math:`\hex{D7}` -(reserved) :math:`\hex{D8}` -(reserved) :math:`\hex{D9}` -(reserved) :math:`\hex{DA}` -(reserved) :math:`\hex{DB}` -(reserved) :math:`\hex{DC}` -(reserved) :math:`\hex{DD}` -(reserved) :math:`\hex{DE}` -(reserved) :math:`\hex{DF}` -(reserved) :math:`\hex{E0}` -(reserved) :math:`\hex{E1}` -(reserved) :math:`\hex{E2}` -(reserved) :math:`\hex{E3}` -(reserved) :math:`\hex{E4}` -(reserved) :math:`\hex{E5}` -(reserved) :math:`\hex{E6}` -(reserved) :math:`\hex{E7}` -(reserved) :math:`\hex{E8}` -(reserved) :math:`\hex{E9}` -(reserved) :math:`\hex{EA}` -(reserved) :math:`\hex{EB}` -(reserved) :math:`\hex{EC}` -(reserved) :math:`\hex{ED}` -(reserved) :math:`\hex{EE}` -(reserved) :math:`\hex{EF}` -(reserved) :math:`\hex{F0}` -(reserved) :math:`\hex{F1}` -(reserved) :math:`\hex{F2}` -(reserved) :math:`\hex{F3}` -(reserved) :math:`\hex{F4}` -(reserved) :math:`\hex{F5}` -(reserved) :math:`\hex{F6}` -(reserved) :math:`\hex{F7}` -(reserved) :math:`\hex{F8}` -(reserved) :math:`\hex{F9}` -(reserved) :math:`\hex{FA}` -(reserved) :math:`\hex{FB}` -:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{00}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{01}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{02}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{03}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{04}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{05}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{06}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{07}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\MEMORYINIT~x` :math:`\hex{FC}~\hex{08}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\DATADROP~x` :math:`\hex{FC}~\hex{09}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYCOPY` :math:`\hex{FC}~\hex{0A}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYFILL` :math:`\hex{FC}~\hex{0B}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEINIT~x~y` :math:`\hex{FC}~\hex{0C}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\ELEMDROP~x` :math:`\hex{FC}~\hex{0D}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLECOPY~x~y` :math:`\hex{FC}~\hex{0E}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEGROW~x` :math:`\hex{FC}~\hex{0F}` :math:`[t~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLESIZE~x` :math:`\hex{FC}~\hex{10}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\TABLEFILL~x` :math:`\hex{FC}~\hex{11}` :math:`[\I32~t~\I32] \to []` :ref:`validation ` :ref:`execution ` -========================================= ========================= ============================================= ======================================= =============================================================== +========================================= ========================= =============================================================== ========================================= =============================================================== +Instruction Binary Opcode Type Validation Execution +========================================= ========================= =============================================================== ========================================= =============================================================== +:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\BLOCK~\X{bt}` :math:`\hex{02}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\LOOP~\X{bt}` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\IF~\X{bt}` :math:`\hex{04}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\ELSE` :math:`\hex{05}` +(reserved) :math:`\hex{06}` +(reserved) :math:`\hex{07}` +(reserved) :math:`\hex{08}` +(reserved) :math:`\hex{09}` +(reserved) :math:`\hex{0A}` +:math:`\END` :math:`\hex{0B}` +:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^\ast~\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALLINDIRECT~x~y` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{12}` +(reserved) :math:`\hex{13}` +:math:`\CALLREF` :math:`\hex{14}` :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{15}` +(reserved) :math:`\hex{16}` +(reserved) :math:`\hex{17}` +(reserved) :math:`\hex{18}` +(reserved) :math:`\hex{19}` +:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\SELECT~t` :math:`\hex{1C}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{1D}` +(reserved) :math:`\hex{1E}` +(reserved) :math:`\hex{1F}` +:math:`\LOCALGET~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\LOCALSET~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\LOCALTEE~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GLOBALGET~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GLOBALSET~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLEGET~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\TABLESET~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{27}` +:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution ` +:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation ` :ref:`execution ` +:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\WRAP\K{\_}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_}\I32\K{\_s}` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_}\I32\K{\_u}` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\DEMOTE\K{\_}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\PROMOTE\K{\_}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REINTERPRET\K{\_}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REINTERPRET\K{\_}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EXTEND\K{8\_s}` :math:`\hex{C0}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EXTEND\K{16\_s}` :math:`\hex{C1}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{8\_s}` :math:`\hex{C2}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{16\_s}` :math:`\hex{C3}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{32\_s}` :math:`\hex{C4}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +(reserved) :math:`\hex{C5}` +(reserved) :math:`\hex{C6}` +(reserved) :math:`\hex{C7}` +(reserved) :math:`\hex{C8}` +(reserved) :math:`\hex{C9}` +(reserved) :math:`\hex{CA}` +(reserved) :math:`\hex{CB}` +(reserved) :math:`\hex{CC}` +(reserved) :math:`\hex{CD}` +(reserved) :math:`\hex{CE}` +(reserved) :math:`\hex{CF}` +:math:`\REFNULL~\X{ht}` :math:`\hex{D0}` :math:`[] \to [(\REF~\NULL~\X{ht})]` :ref:`validation ` :ref:`execution ` +:math:`\REFISNULL` :math:`\hex{D1}` :math:`[(\REF~\NULL~\X{ht})] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\REFFUNC~x` :math:`\hex{D2}` :math:`[] \to [\FUNCREF]` :ref:`validation ` :ref:`execution ` +:math:`\REFASNONNULL` :math:`\hex{D3}` :math:`[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]` :ref:`validation ` :ref:`execution ` +:math:`\BRONNULL~l` :math:`\hex{D4}` :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{D5}` +:math:`\BRONNONNULL~l` :math:`\hex{D6}` :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{D7}` +(reserved) :math:`\hex{D8}` +(reserved) :math:`\hex{D9}` +(reserved) :math:`\hex{DA}` +(reserved) :math:`\hex{DB}` +(reserved) :math:`\hex{DC}` +(reserved) :math:`\hex{DD}` +(reserved) :math:`\hex{DE}` +(reserved) :math:`\hex{DF}` +(reserved) :math:`\hex{E0}` +(reserved) :math:`\hex{E1}` +(reserved) :math:`\hex{E2}` +(reserved) :math:`\hex{E3}` +(reserved) :math:`\hex{E4}` +(reserved) :math:`\hex{E5}` +(reserved) :math:`\hex{E6}` +(reserved) :math:`\hex{E7}` +(reserved) :math:`\hex{E8}` +(reserved) :math:`\hex{E9}` +(reserved) :math:`\hex{EA}` +(reserved) :math:`\hex{EB}` +(reserved) :math:`\hex{EC}` +(reserved) :math:`\hex{ED}` +(reserved) :math:`\hex{EE}` +(reserved) :math:`\hex{EF}` +(reserved) :math:`\hex{F0}` +(reserved) :math:`\hex{F1}` +(reserved) :math:`\hex{F2}` +(reserved) :math:`\hex{F3}` +(reserved) :math:`\hex{F4}` +(reserved) :math:`\hex{F5}` +(reserved) :math:`\hex{F6}` +(reserved) :math:`\hex{F7}` +(reserved) :math:`\hex{F8}` +(reserved) :math:`\hex{F9}` +(reserved) :math:`\hex{FA}` +(reserved) :math:`\hex{FB}` +:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{00}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{01}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{02}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{03}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_s}` :math:`\hex{FC}~\hex{04}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F32\K{\_u}` :math:`\hex{FC}~\hex{05}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_s}` :math:`\hex{FC}~\hex{06}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_sat\_}\F64\K{\_u}` :math:`\hex{FC}~\hex{07}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\MEMORYINIT~x` :math:`\hex{FC}~\hex{08}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\DATADROP~x` :math:`\hex{FC}~\hex{09}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYCOPY` :math:`\hex{FC}~\hex{0A}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYFILL` :math:`\hex{FC}~\hex{0B}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLEINIT~x~y` :math:`\hex{FC}~\hex{0C}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\ELEMDROP~x` :math:`\hex{FC}~\hex{0D}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLECOPY~x~y` :math:`\hex{FC}~\hex{0E}` :math:`[\I32~\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLEGROW~x` :math:`\hex{FC}~\hex{0F}` :math:`[t~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TABLESIZE~x` :math:`\hex{FC}~\hex{10}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\TABLEFILL~x` :math:`\hex{FC}~\hex{11}` :math:`[\I32~t~\I32] \to []` :ref:`validation ` :ref:`execution ` +========================================= ========================= =============================================================== ========================================= =============================================================== diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 9da4e188..f6e8051f 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -34,8 +34,11 @@ Control Instructions .. _binary-br: .. _binary-br_if: .. _binary-br_table: +.. _binary-br_on_null: +.. _binary-br_on_non_null: .. _binary-return: .. _binary-call: +.. _binary-call_ref: .. _binary-call_indirect: .. math:: @@ -62,7 +65,10 @@ Control Instructions &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& \hex{0F} &\Rightarrow& \RETURN \\ &&|& \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|& - \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ + \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ &&|& + \hex{14}~~x{:}\Bfuncidx &\Rightarrow& \CALLREF \\ &&|& + \hex{D4}~~x{:}\Bfuncidx &\Rightarrow& \BRONNULL \\ &&|& + \hex{D6}~~x{:}\Bfuncidx &\Rightarrow& \BRONNONNULL \\ \end{array} .. note:: @@ -82,14 +88,17 @@ Reference Instructions :ref:`Reference instructions ` are represented by single byte codes. .. _binary-ref.null: -.. _binary-ref.isnull: +.. _binary-ref.func: +.. _binary-ref.is_null: +.. _binary-ref.as_non_null: .. math:: \begin{array}{llclll} \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{D0}~~t{:}\Bheaptype &\Rightarrow& \REFNULL~t \\ &&|& \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& - \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ + \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& + \hex{D3} &\Rightarrow& \REFASNONNULL \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6f4c7dc7..2872970b 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -192,15 +192,35 @@ Reference Instructions .. _exec-ref.null: -:math:`\REFNULL~t` -.................. +:math:`\REFNULL~\X{ht}` +....................... -1. Push the value :math:`\REFNULL~t` to the stack. +1. Push the value :math:`\REFNULL~\X{ht}` to the stack. .. note:: No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value `. +.. _exec-ref.func: + +:math:`\REFFUNC~x` +.................. + +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. + +2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIFUNCS[x]` exists. + +3. Let :math:`a` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x]`. + +4. Push the value :math:`\REFFUNCADDR~a` to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a + & (\iff a = F.\AMODULE.\MIFUNCS[x]) \\ + \end{array} + + .. _exec-ref.is_null: :math:`\REFISNULL` @@ -210,7 +230,7 @@ Reference Instructions 2. Pop the value :math:`\val` from the stack. -3. If :math:`\val` is :math:`\REFNULL~t`, then: +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: a. Push the value :math:`\I32.\CONST~1` to the stack. @@ -221,29 +241,33 @@ Reference Instructions .. math:: \begin{array}{lcl@{\qquad}l} \val~\REFISNULL &\stepto& \I32.\CONST~1 - & (\iff \val = \REFNULL~t) \\ + & (\iff \val = \REFNULL~\X{ht}) \\ \val~\REFISNULL &\stepto& \I32.\CONST~0 & (\otherwise) \\ \end{array} -.. _exec-ref.func: +.. _exec-ref.as_non_null: -:math:`\REFFUNC~x` -.................. +:math:`\REFASNONNULL` +..................... -1. Let :math:`F` be the :ref:`current ` :ref:`frame `. +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. -2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MIFUNCS[x]` exists. +2. Pop the value :math:`\val` from the stack. -3. Let :math:`a` be the :ref:`function address ` :math:`F.\AMODULE.\MIFUNCS[x]`. +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: -4. Push the value :math:`\REFFUNCADDR~a` to the stack. + a. Trap. + +4. Push the value :math:`\val` back to the stack. .. math:: \begin{array}{lcl@{\qquad}l} - F; \REFFUNC~x &\stepto& F; \REFFUNCADDR~a - & (\iff a = F.\AMODULE.\MIFUNCS[x]) \\ + \val~\REFASNONNULL &\stepto& \TRAP + & (\iff \val = \REFNULL~\X{ht}) \\ + \val~\REFASNONNULL &\stepto& \val + & (\otherwise) \\ \end{array} @@ -1722,6 +1746,60 @@ Control Instructions \end{array} +.. _exec-br_on_null: + +:math:`\BRONNULL~l` +................... + +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. + +2. Pop the value :math:`\val` from the stack. + +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: + + a. :ref:`Execute ` the instruction :math:`(\BR~l)`. + +4. Else: + + a. Push the value :math:`\val` back to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \val~(\BRONNULL~l) &\stepto& (\BR~l) + & (\iff \val = \REFNULL~\X{ht}) \\ + \val~(\BRONNULL~l) &\stepto& \val + & (\otherwise) \\ + \end{array} + + +.. _exec-br_on_non_null: + +:math:`\BRONNONNULL~l` +...................... + +1. Assert: due to :ref:`validation `, a :ref:`reference value ` is on the top of the stack. + +2. Pop the value :math:`\val` from the stack. + +3. If :math:`\val` is :math:`\REFNULL~\X{ht}`, then: + + a. Do nothing. + +4. Else: + + a. Push the value :math:`\val` back to the stack. + + b. :ref:`Execute ` the instruction :math:`(\BR~l)`. + +.. math:: + \begin{array}{lcl@{\qquad}l} + \val~(\BRONNONNULL~l) &\stepto& \epsilon + & (\iff \val = \REFNULL~\X{ht}) \\ + \val~(\BRONNONNULL~l) &\stepto& \val~(\BR~l) + & (\otherwise) \\ + \end{array} + + .. _exec-return: :math:`\RETURN` @@ -1776,6 +1854,23 @@ Control Instructions \end{array} +.. _exec-call_ref: + +:math:`\CALLREF` +................ + +1. Assert: due to :ref:`validation `, a :ref:`function reference ` is on the top of the stack. + +2. Pop the value :math:`\REFFUNCADDR~a` from the stack. + +3. :ref:`Invoke ` the function instance at address :math:`a`. + +.. math:: + \begin{array}{lcl@{\qquad}l} + F; (\REFFUNCADDR~a)~\CALLREF &\stepto& F; (\INVOKE~a) + \end{array} + + .. _exec-call_indirect: :math:`\CALLINDIRECT~x~y` @@ -1805,7 +1900,7 @@ Control Instructions 11. Let :math:`r` be the :ref:`reference ` :math:`\X{tab}.\TIELEM[i]`. -12. If :math:`r` is :math:`\REFNULL~t`, then: +12. If :math:`r` is :math:`\REFNULL~\X{ht}`, then: a. Trap. diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 67bc409e..3bebe174 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -174,8 +174,9 @@ Occasionally, it is convenient to group operators together according to the foll .. index:: ! reference instruction, reference, null pair: abstract syntax; instruction .. _syntax-ref.null: -.. _syntax-ref.is_null: .. _syntax-ref.func: +.. _syntax-ref.is_null: +.. _syntax-ref.as_non_null: .. _syntax-instr-ref: Reference Instructions @@ -188,11 +189,13 @@ Instructions in this group are concerned with accessing :ref:`references ` value, produce a reference to a given function, or check for a null value, respectively. +The |REFASNONNULL| casts a :ref:`nullable ` to a non-null one, and :ref:`traps ` if it encounters null. .. index:: ! parametric instruction, value type @@ -389,8 +392,11 @@ Instructions in this group affect the flow of control. \BR~\labelidx \\&&|& \BRIF~\labelidx \\&&|& \BRTABLE~\vec(\labelidx)~\labelidx \\&&|& + \BRONNULL~\labelidx \\&&|& + \BRONNONNULL~\labelidx \\&&|& \RETURN \\&&|& \CALL~\funcidx \\&&|& + \CALLREF \\&&|& \CALLINDIRECT~\tableidx~\typeidx \\ \end{array} @@ -427,6 +433,7 @@ Branch instructions come in several flavors: |BR| performs an unconditional branch, |BRIF| performs a conditional branch, and |BRTABLE| performs an indirect branch through an operand indexing into the label vector that is an immediate to the instruction, or to a default target if the operand is out of bounds. +The |BRONNULL| and |BRONNONNULL| instructions check whether a reference operand is :ref:`null ` and branch if that is the case or not the case, respectively. The |RETURN| instruction is a shortcut for an unconditional branch to the outermost block, which implicitly is the body of the current function. Taking a branch *unwinds* the operand stack up to the height where the targeted structured control instruction was entered. However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding. @@ -434,6 +441,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 |CALLREF| instruction invokes a function indirectly through a :ref:`function reference ` operand. 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/text/instructions.rst b/document/core/text/instructions.rst index 0c350d00..d116523d 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -95,8 +95,11 @@ However, the special case of a type use that is syntactically empty or consists .. _text-br: .. _text-br_if: .. _text-br_table: +.. _text-br_on_null: +.. _text-br_on_non_null: .. _text-return: .. _text-call: +.. _text-call_ref: .. _text-call_indirect: All other control instruction are represented verbatim. @@ -110,8 +113,11 @@ All other control instruction are represented verbatim. \text{br\_if}~~l{:}\Tlabelidx_I &\Rightarrow& \BRIF~l \\ &&|& \text{br\_table}~~l^\ast{:}\Tvec(\Tlabelidx_I)~~l_N{:}\Tlabelidx_I &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& + \text{br\_on\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNULL~l \\ &&|& + \text{br\_on\_non\_null}~~l{:}\Tlabelidx_I &\Rightarrow& \BRONNONNULL~l \\ &&|& \text{return} &\Rightarrow& \RETURN \\ &&|& \text{call}~~x{:}\Tfuncidx_I &\Rightarrow& \CALL~x \\ &&|& + \text{call\_ref} &\Rightarrow& \CALLREF \\ &&|& \text{call\_indirect}~~x{:}\Ttableidx~~y,I'{:}\Ttypeuse_I &\Rightarrow& \CALLINDIRECT~x~y & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\ \end{array} @@ -152,15 +158,17 @@ Reference Instructions ~~~~~~~~~~~~~~~~~~~~~~ .. _text-ref.null: -.. _text-ref.is_null: .. _text-ref.func: +.. _text-ref.is_null: +.. _text-ref.as_non_null: .. math:: \begin{array}{llclll} \production{instruction} & \Tplaininstr_I &::=& \dots \\ &&|& \text{ref.null}~~t{:}\Theaptype &\Rightarrow& \REFNULL~t \\ &&|& - \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|& \text{ref.func}~~x{:}\Tfuncidx &\Rightarrow& \REFFUNC~x \\ &&|& + \text{ref.is\_null} &\Rightarrow& \REFISNULL \\ &&|& + \text{ref.as\_non\_null} &\Rightarrow& \REFASNONNULL \\ \end{array} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index dd900bcd..24e07740 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -351,8 +351,11 @@ .. |BR| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br}} .. |BRIF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_if}} .. |BRTABLE| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_table}} +.. |BRONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_null}} +.. |BRONNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{br\_on\_non\_null}} .. |RETURN| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{return}} .. |CALL| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call}} +.. |CALLREF| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_ref}} .. |CALLINDIRECT| mathdef:: \xref{syntax/instructions}{syntax-instr-control}{\K{call\_indirect}} .. |DROP| mathdef:: \xref{syntax/instructions}{syntax-instr-parametric}{\K{drop}} @@ -383,8 +386,9 @@ .. |DATADROP| mathdef:: \xref{syntax/instructions}{syntax-instr-memory}{\K{data.drop}} .. |REFNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}null}} -.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}} .. |REFFUNC| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}func}} +.. |REFISNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}is\_null}} +.. |REFASNONNULL| mathdef:: \xref{syntax/instructions}{syntax-instr-ref}{\K{ref{.}as\_non\_null}} .. |CONST| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{const}} .. |EQZ| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{eqz}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 89c0c21e..22d6647e 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -166,32 +166,18 @@ Reference Instructions .. _valid-ref.null: -:math:`\REFNULL~t` -.................. - -* The instruction is valid with type :math:`[] \to [t]`. - -.. math:: - \frac{ - }{ - C \vdashinstr \REFNULL~t : [] \to [t] - } +:math:`\REFNULL~\X{ht}` +....................... -.. note:: - In future versions of WebAssembly, there may be reference types for which no null reference is allowed. +* The :ref:`heap type ` :math:`\X{ht}` must be :ref:`valid `. -.. _valid-ref.is_null: - -:math:`\REFISNULL` -.................. - -* The instruction is valid with type :math:`[t] \to [\I32]`, for any :ref:`reference type ` :math:`t`. +* Then the instruction is valid with type :math:`[] \to [(\REF~\NULL~\X{ht})]`. .. math:: \frac{ - t = \reftype + C \vdashheaptype \X{ht} \ok }{ - C \vdashinstr \REFISNULL : [t] \to [\I32] + C \vdashinstr \REFNULL~\X{ht} : [] \to [(\REF~\NULL~\X{ht})] } .. _valid-ref.func: @@ -214,6 +200,34 @@ Reference Instructions C \vdashinstr \REFFUNC~x : [] \to [\FUNCREF] } +.. _valid-ref.is_null: + +:math:`\REFISNULL` +.................. + +* The instruction is valid with type :math:`[(\REF~\NULL~\X{ht})] \to [\I32]`, for any :ref:`valid ` :ref:`heap type ` :math:`\X{ht}`. + +.. math:: + \frac{ + C \vdashheaptype \X{ht} \ok + }{ + C \vdashinstr \REFISNULL : [(\REF~\NULL~\X{ht})] \to [\I32] + } + +.. _valid-ref.as_non_null: + +:math:`\REFASNONNULL` +..................... + +* The instruction is valid with type :math:`[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]`, for any :ref:`valid ` :ref:`heap type ` :math:`\X{ht}`. + +.. math:: + \frac{ + C \vdashheaptype \X{ht} \ok + }{ + C \vdashinstr \REFASNONNULL : [(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})] + } + .. index:: parametric instructions, value type, polymorphism pair: validation; instruction @@ -228,10 +242,11 @@ Parametric Instructions :math:`\DROP` ............. -* The instruction is valid with type :math:`[t] \to []`, for any :ref:`value type ` :math:`t`. +* The instruction is valid with type :math:`[t] \to []`, for any :ref:`valid ` :ref:`value type ` :math:`t`. .. math:: \frac{ + C \vdashvaltype t \ok }{ C \vdashinstr \DROP : [t] \to [] } @@ -973,6 +988,52 @@ Control Instructions a simple :ref:`linear algorithm ` does not require this. +.. _valid-br_on_null: + +:math:`\BRONNULL~l` +................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* Then the instruction is valid with type :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]` for any :ref:`valid ` :ref:`heap type ` :math:`\X{ht}`. + +.. math:: + \frac{ + C.\CLABELS[l] = [t^\ast] + \qquad + C \vdashheaptype \X{ht} \ok + }{ + C \vdashinstr \BRONNULL~l : [t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})] + } + + +.. _valid-br_on_non_null: + +:math:`\BRONNONNULL~l` +...................... + +* The label :math:`C.\CLABELS[l]` must be defined in the context. + +* Let :math:`[{t'}^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. + +* The result type :math:`[{t'}^\ast]` must contain at least one type. + +* Let the :ref:`value type ` :math:`t_l` be the last element in the sequence :math:`{t'}^\ast`, and :math:`[t^\ast]` the remainder of the sequence preceding it. + +* The value type :math:`t_l` must be a reference type of the form :math:`\REF~\NULL^?~\X{ht}`. + +* Then the instruction is valid with type :math:`[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]`. + +.. math:: + \frac{ + C.\CLABELS[l] = [t^\ast~(\REF~\X{ht})] + }{ + C \vdashinstr \BRONNONNULL~l : [t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast] + } + + .. _valid-return: :math:`\RETURN` @@ -1018,6 +1079,23 @@ Control Instructions } +.. _valid-call_ref: + +:math:`\CALLREF` +................ + +* Let :math:`x` be some :ref:`type index ` for which :math:`C.\CTYPES[x]` is a :ref:`function type ` of the form :math:`[t_1^\ast] \to [t_2^\ast]`. + +* Then the instruction is valid with type :math:`[t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast]`. + +.. math:: + \frac{ + C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] + }{ + C \vdashinstr \CALLREF : [t_1^\ast~(\REF~\NULL~x)] \to [t_2^\ast] + } + + .. _valid-call_indirect: :math:`\CALLINDIRECT~x~y` diff --git a/proposals/function-references/Overview.md b/proposals/function-references/Overview.md index 7d08ed54..36dc946d 100644 --- a/proposals/function-references/Overview.md +++ b/proposals/function-references/Overview.md @@ -168,7 +168,7 @@ The following rules, now defined in terms of heap types, replace and extend the - `(ref ) <: (ref null )` - iff ` <: ` -##### Constructed Types +##### Heap Types * Any function type is a subtype of `func` - `$t <: func`