diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index e7d13ae9..5d99cce2 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -13,8 +13,9 @@ The only exception are :ref:`structured control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for |END| and |ELSE|. +:ref:`Block types ` are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type, as a single :ref:`value type `, or as a :ref:`type index ` encoded as a positive :ref:`signed integer `. + +.. _binary-blocktype: .. _binary-nop: .. _binary-unreachable: .. _binary-block: @@ -36,18 +40,22 @@ Control Instructions .. math:: \begin{array}{llclll} + \production{block type} & \Bblocktype &::=& + \hex{40} &\Rightarrow& \epsilon \\ &&|& + t{:}\Bvaltype &\Rightarrow& t \\ &&|& + x{:}\Bs33 &\Rightarrow& x \\ \production{instruction} & \Binstr &::=& \hex{00} &\Rightarrow& \UNREACHABLE \\ &&|& \hex{01} &\Rightarrow& \NOP \\ &&|& - \hex{02}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \BLOCK~\X{rt}~\X{in}^\ast~\END \\ &&|& - \hex{03}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \LOOP~\X{rt}~\X{in}^\ast~\END \\ &&|& - \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \IF~\X{rt}~\X{in}^\ast~\ELSE~\epsilon~\END \\ &&|& - \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ + \hex{02}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \BLOCK~\X{bt}~\X{in}^\ast~\END \\ &&|& + \hex{03}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \LOOP~\X{bt}~\X{in}^\ast~\END \\ &&|& + \hex{04}~~\X{bt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \IF~\X{bt}~\X{in}^\ast~\ELSE~\epsilon~\END \\ &&|& + \hex{04}~~\X{bt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ \hex{05}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \IF~\X{rt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|& + &\Rightarrow& \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|& \hex{0C}~~l{:}\Blabelidx &\Rightarrow& \BR~l \\ &&|& \hex{0D}~~l{:}\Blabelidx &\Rightarrow& \BRIF~l \\ &&|& \hex{0E}~~l^\ast{:}\Bvec(\Blabelidx)~~l_N{:}\Blabelidx @@ -60,6 +68,10 @@ Control Instructions .. note:: The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty. + Unlike any :ref:`other occurrence `, the :ref:`type index ` in a :ref:`block type ` is encoded as a positive :ref:`signed integer `, so that its `LEB128 `_ bit pattern cannot collide with the encoding of :ref:`value types ` or the special code :math:`\hex{40}`, which correspond to the LEB128 encoding of negative integers. + To avoid any loss in the range of allowed indices, it is treated as a 33 bit signed integer. + + .. index:: value type, polymorphism pair: binary format; instruction diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index e5342259..4e11d6be 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -24,30 +24,25 @@ Value Types \end{array} .. 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. + Value types can occur in contexts where :ref:`type indices ` are also allowed, such as in the case of :ref:`block types `. + 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 be distinguished from (positive) type indices. .. index:: result type, value type pair: binary format; result type -.. _binary-blocktype: .. _binary-resulttype: Result Types ~~~~~~~~~~~~ -The only :ref:`result types ` occurring in the binary format are the types of blocks. These are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type or as a single :ref:`value type `. +:ref:`Result types ` are encoded by the respective :ref:`vectors ` of :ref:`value types ``. .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{result type} & \Bblocktype &::=& - \hex{40} &\Rightarrow& [] \\ &&|& - t{:}\Bvaltype &\Rightarrow& [t] \\ + \production{result type} & \Bresulttype &::=& + t^\ast{:\,}\Bvec(\Bvaltype) &\Rightarrow& [t^\ast] \\ \end{array} -.. note:: - In future versions of WebAssembly, this scheme may be extended to support multiple results or more general block types. - .. index:: function type, value type, result type pair: binary format; function type @@ -61,8 +56,8 @@ Function Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{function type} & \Bfunctype &::=& - \hex{60}~~t_1^\ast{:\,}\Bvec(\Bvaltype)~~t_2^\ast{:\,}\Bvec(\Bvaltype) - &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ + \hex{60}~~\X{rt}_1{:\,}\Bresulttype~~\X{rt}_2{:\,}\Bresulttype + &\Rightarrow& \X{rt}_1 \to \X{rt}_2 \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 7d20577b..b8d42ef9 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -651,70 +651,80 @@ Control Instructions .. _exec-block: -:math:`\BLOCK~[t^?]~\instr^\ast~\END` -..................................... +:math:`\BLOCK~\blocktype~\instr^\ast~\END` +.......................................... -1. Let :math:`n` be the arity :math:`|t^?|` of the :ref:`result type ` :math:`t^?`. +1. Assert: due to :ref:`validation `, :math:`\expand_F(\blocktype)` is defined. -2. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the block. +2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type ` :math:`\expand_F(\blocktype)`. -3. :ref:`Enter ` the block :math:`\instr^\ast` with label :math:`L`. +3. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the block. + +4. :ref:`Enter ` the block :math:`\instr^\ast` with label :math:`L`. .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - \BLOCK~[t^n]~\instr^\ast~\END &\stepto& - \LABEL_n\{\epsilon\}~\instr^\ast~\END + F; \BLOCK~\X{bt}~\instr^\ast~\END &\stepto& + F; \LABEL_n\{\epsilon\}~\instr^\ast~\END + & (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \end{array} .. _exec-loop: -:math:`\LOOP~[t^?]~\instr^\ast~\END` -.................................... +:math:`\LOOP~\blocktype~\instr^\ast~\END` +......................................... + +1. Assert: due to :ref:`validation `, :math:`\expand_F(\blocktype)` is defined. + +2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type ` :math:`\expand_F(\blocktype)`. -1. Let :math:`L` be the label whose arity is :math:`0` and whose continuation is the start of the loop. +3. Let :math:`L` be the label whose arity is :math:`m` and whose continuation is the start of the loop. -2. :ref:`Enter ` the block :math:`\instr^\ast` with label :math:`L`. +4. :ref:`Enter ` the block :math:`\instr^\ast` with label :math:`L`. .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - \LOOP~[t^?]~\instr^\ast~\END &\stepto& - \LABEL_0\{\LOOP~[t^?]~\instr^\ast~\END\}~\instr^\ast~\END + F; \LOOP~\X{bt}~\instr^\ast~\END &\stepto& + F; \LABEL_m\{\LOOP~\X{bt}~\instr^\ast~\END\}~\instr^\ast~\END + & (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \end{array} .. _exec-if: -:math:`\IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END` -........................................................ +:math:`\IF~\blocktype~\instr_1^\ast~\ELSE~\instr_2^\ast~\END` +............................................................. -1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. +1. Assert: due to :ref:`validation `, :math:`\expand_F(\blocktype)` is defined. -2. Pop the value :math:`\I32.\CONST~c` from the stack. +2. Let :math:`[t_1^m] \to [t_2^n]` be the :ref:`function type ` :math:`\expand_F(\blocktype)`. -3. Let :math:`n` be the arity :math:`|t^?|` of the :ref:`result type ` :math:`t^?`. +3. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the |IF| instruction. -4. Let :math:`L` be the label whose arity is :math:`n` and whose continuation is the end of the |IF| instruction. +4. Assert: due to :ref:`validation `, a value of :ref:`value type ` |I32| is on the top of the stack. -5. If :math:`c` is non-zero, then: +5. Pop the value :math:`\I32.\CONST~c` from the stack. + +6. If :math:`c` is non-zero, then: a. :ref:`Enter ` the block :math:`\instr_1^\ast` with label :math:`L`. -6. Else: +7. Else: a. :ref:`Enter ` the block :math:`\instr_2^\ast` with label :math:`L`. .. math:: ~\\[-1ex] \begin{array}{lcl@{\qquad}l} - (\I32.\CONST~c)~\IF~[t^n]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto& - \LABEL_n\{\epsilon\}~\instr_1^\ast~\END - & (\iff c \neq 0) \\ - (\I32.\CONST~c)~\IF~[t^n]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto& - \LABEL_n\{\epsilon\}~\instr_2^\ast~\END - & (\iff c = 0) \\ + F; (\I32.\CONST~c)~\IF~\X{bt}~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto& + F; \LABEL_n\{\epsilon\}~\instr_1^\ast~\END + & (\iff c \neq 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\ + F; (\I32.\CONST~c)~\IF~\X{bt}~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto& + F; \LABEL_n\{\epsilon\}~\instr_2^\ast~\END + & (\iff c = 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\ \end{array} @@ -1021,13 +1031,15 @@ Invocation of :ref:`function address ` :math:`a` 10. Push the activation of :math:`F` with arity :math:`m` to the stack. -11. :ref:`Execute ` the instruction :math:`\BLOCK~[t_2^m]~\instr^\ast~\END`. +11. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. + +12. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L`. .. math:: ~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} - S; \val^n~(\INVOKE~a) &\stepto& S; \FRAME_m\{F\}~\BLOCK~[t_2^m]~\instr^\ast~\END~\END + S; \val^n~(\INVOKE~a) &\stepto& S; \FRAME_m\{F\}~\LABEL_m\{\}~\instr^\ast~\END~\END \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index b721836e..5758dd41 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -307,13 +307,7 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]` -.. index:: ! stack, ! frame, ! label, instruction, store, activation, function, call, local, module instance - pair: abstract syntax; frame - pair: abstract syntax; label -.. _syntax-frame: -.. _syntax-label: -.. _frame: -.. _label: +.. index:: ! stack, frame, label, instruction, store, activation, function, call, local, module instance .. _stack: Stack @@ -342,6 +336,12 @@ Values Values are represented by :ref:`themselves `. + +.. index:: ! label, instruction + pair: abstract syntax; label +.. _syntax-label: +.. _label: + Labels ...... @@ -359,7 +359,7 @@ Intuitively, :math:`\instr^\ast` is the *continuation* to execute when the branc For example, a loop label has the form .. math:: - \LABEL_n\{\LOOP~[t^?]~\dots~\END\} + \LABEL_n\{\LOOP~\dots~\END\} When performing a branch to this label, this executes the loop, effectively restarting it from the beginning. Conversely, a simple block label has the form @@ -369,6 +369,12 @@ Intuitively, :math:`\instr^\ast` is the *continuation* to execute when the branc When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions. + +.. index:: ! frame, instruction, activation, local, module instance + pair: abstract syntax; frame +.. _syntax-frame: +.. _frame: + Frames ...... @@ -394,9 +400,13 @@ Conventions * The meta variable :math:`F` ranges over frames where clear from context. -.. note:: - In the current version of WebAssembly, the arities of labels and frames cannot be larger than :math:`1`. - This may be generalized in future versions. +* The following auxiliary definition takes a :ref:`block type ` and looks up the :ref:`function type ` that it denotes in the current frame: + +.. math:: + \begin{array}{lll} + \expand_F(\typeidx) &=& F.\AMODULE.\MITYPES[\typeidx] \\ + \expand_F([\valtype^?]) &=& [] \to [\valtype^?] \\ + \end{array} .. index:: ! administrative instructions, function, function instance, function address, label, frame, instruction, trap, call diff --git a/document/core/syntax/instrindex.rst b/document/core/syntax/instrindex.rst index d6230dbb..9fb5020d 100644 --- a/document/core/syntax/instrindex.rst +++ b/document/core/syntax/instrindex.rst @@ -3,14 +3,14 @@ Index of Instructions --------------------- -=================================== ================ ========================================== ======================================== =============================================================== -Instruction 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~[t^?]` :math:`\hex{02}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\LOOP~[t^?]` :math:`\hex{03}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\IF~[t^?]` :math:`\hex{04}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +=================================== ================ ============================================= ======================================== =============================================================== +Instruction 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` :math:`\hex{02}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\LOOP` :math:`\hex{03}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\IF` :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}` @@ -18,12 +18,12 @@ Instruction Opcode Type (reserved) :math:`\hex{09}` (reserved) :math:`\hex{0A}` :math:`\END` :math:`\hex{0B}` -:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^?~\I32] \to [t^?]` :ref:`validation ` :ref:`execution ` -:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^?] \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` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +: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` :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}` @@ -32,171 +32,171 @@ Instruction Opcode Type (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:`\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 ` (reserved) :math:`\hex{1C}` (reserved) :math:`\hex{1D}` (reserved) :math:`\hex{1E}` (reserved) :math:`\hex{1F}` -:math:`\GETLOCAL~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\SETLOCAL~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TEELOCAL~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GETGLOBAL~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\SETGLOBAL~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\GETLOCAL~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\SETLOCAL~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\TEELOCAL~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GETGLOBAL~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\SETGLOBAL~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` (reserved) :math:`\hex{25}` (reserved) :math:`\hex{26}` (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:`\CURRENTMEMORY` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\GROWMEMORY` :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{\_s/}\F32` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_u/}\F32` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_s/}\F64` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_u/}\F64` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_s/}\I32` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_u/}\I32` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_s/}\F32` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_u/}\F32` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_s/}\F64` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_u/}\F64` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_s/}\I32` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_u/}\I32` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_s/}\I64` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_u/}\I64` :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{\_s/}\I32` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_u/}\I32` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_s/}\I64` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_u/}\I64` :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.\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:`\CURRENTMEMORY` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\GROWMEMORY` :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{\_s/}\F32` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_u/}\F32` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_s/}\F64` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_u/}\F64` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_s/}\I32` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_u/}\I32` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_s/}\F32` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_u/}\F32` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_s/}\F64` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_u/}\F64` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_s/}\I32` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_u/}\I32` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_s/}\I64` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_u/}\I64` :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{\_s/}\I32` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_u/}\I32` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_s/}\I64` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_u/}\I64` :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 ` +=================================== ================ ============================================= ======================================== =============================================================== diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index a740e7cb..6bf0b25d 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -9,11 +9,6 @@ WebAssembly code consists of sequences of *instructions*. Its computational model is based on a *stack machine* in that instructions manipulate values on an implicit *operand stack*, consuming (popping) argument values and producing (pushing) result values. -.. note:: - In the current version of WebAssembly, - at most one result value can be pushed by a single instruction. - This restriction may be lifted in future versions. - In addition to dynamic operands from the stack, some instructions also have static *immediate* arguments, typically :ref:`indices ` or type annotations, which are part of the instruction itself. @@ -266,8 +261,11 @@ Both instructions operate in units of :ref:`page size `. This restriction may be lifted in future versions. -.. index:: ! control instruction, ! structured control, ! label, ! block, ! branch, ! unwinding, result type, label index, function index, type index, vector, trap, function, table, function type +.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, result type, label index, function index, type index, vector, trap, function, table, function type, value type, type index pair: abstract syntax; instruction + pair: abstract syntax; block type + pair: block; type +.. _syntax-blocktype: .. _syntax-nop: .. _syntax-unreachable: .. _syntax-block: @@ -289,13 +287,15 @@ Instructions in this group affect the flow of control. .. math:: \begin{array}{llcl} + \production{block type} & \blocktype &::=& + \typeidx ~|~ \valtype^? \\ \production{instruction} & \instr &::=& \dots \\&&|& \NOP \\&&|& \UNREACHABLE \\&&|& - \BLOCK~\resulttype~\instr^\ast~\END \\&&|& - \LOOP~\resulttype~\instr^\ast~\END \\&&|& - \IF~\resulttype~\instr^\ast~\ELSE~\instr^\ast~\END \\&&|& + \BLOCK~\blocktype~\instr^\ast~\END \\&&|& + \LOOP~\blocktype~\instr^\ast~\END \\&&|& + \IF~\blocktype~\instr^\ast~\ELSE~\instr^\ast~\END \\&&|& \BR~\labelidx \\&&|& \BRIF~\labelidx \\&&|& \BRTABLE~\vec(\labelidx)~\labelidx \\&&|& @@ -311,7 +311,9 @@ The |UNREACHABLE| instruction causes an unconditional :ref:`trap `. The |BLOCK|, |LOOP| and |IF| instructions are *structured* instructions. They bracket nested sequences of instructions, called *blocks*, terminated with, or separated by, |END| or |ELSE| pseudo-instructions. As the grammar prescribes, they must be well-nested. -A structured instruction can produce a value as described by the annotated :ref:`result type `. + +A structured instruction can consume *input* and produce *output* on the operand stack according to its annotated *block type*. +It is given either as a :ref:`type index ` that refers to a suitable :ref:`function type `, or as an optional :ref:`value type ` inline, which is a shorthand for the function type :math:`[] \to [\valtype^?]`. Each structured control instruction introduces an implicit *label*. Labels are targets for branch instructions that reference them with :ref:`label indices `. @@ -337,7 +339,9 @@ Branch instructions come in several flavors: 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 |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, forward branches that target a control instruction with a non-empty result type consume matching operands first and push them back on the operand stack after unwinding, as a result for the terminated structured instruction. +However, branches may additionally consume operands themselves, which they push back on the operand stack after unwinding. +Forward branches require operands according to the output of the targeted block's type, i.e., represent the values produced by the terminated 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 `. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 7065057f..e52480d3 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -40,7 +40,7 @@ Conventions That is, :math:`|\I32| = |\F32| = 32` and :math:`|\I64| = |\F64| = 64`. -.. index:: ! result type, value type, instruction, execution, block +.. index:: ! result type, value type, instruction, execution, function pair: abstract syntax; result type pair: result; type .. _syntax-resulttype: @@ -48,21 +48,17 @@ Conventions Result Types ~~~~~~~~~~~~ -*Result types* classify the result of :ref:`executing ` :ref:`instructions ` or :ref:`blocks `, +*Result types* classify the result of :ref:`executing ` :ref:`instructions ` or :ref:`functions `, which is a sequence of values. .. math:: \begin{array}{llll} \production{result type} & \resulttype &::=& - [\valtype^?] \\ + [\vec(\valtype)] \\ \end{array} -.. note:: - In the current version of WebAssembly, at most one value is allowed as a result. - However, this may be generalized to sequences of values in future versions. - -.. index:: ! function type, value type, vector, function, parameter, result +.. index:: ! function type, value type, vector, function, parameter, result, result type pair: abstract syntax; function type pair: function; type .. _syntax-functype: @@ -72,18 +68,14 @@ Function Types *Function types* classify the signature of :ref:`functions `, mapping a vector of parameters to a vector of results. +They are also used to classify the inputs and outputs of :ref:`instructions `. .. math:: \begin{array}{llll} \production{function type} & \functype &::=& - [\vec(\valtype)] \to [\vec(\valtype)] \\ + \resulttype \to \resulttype \\ \end{array} -.. note:: - In the current version of WebAssembly, - the length of the result type vector of a :ref:`valid ` function type may be at most :math:`1`. - This restriction may be removed in future versions. - .. index:: ! limits, memory type, table type pair: abstract syntax; limits diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 7d743220..57f5257a 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -52,6 +52,7 @@ The following grammar handles the corresponding update to the :ref:`identifier c Control Instructions ~~~~~~~~~~~~~~~~~~~~ +.. _text-blocktype: .. _text-block: .. _text-loop: .. _text-if: @@ -60,21 +61,35 @@ Control Instructions :ref:`Structured control instructions ` can bind an optional symbolic :ref:`label identifier `. The same label identifier may optionally be repeated after the corresponding :math:`\T{end}` and :math:`\T{else}` pseudo instructions, to indicate the matching delimiters. +Their :ref:`block type ` is given as a :ref:`type use `, analogous to the type of :ref:`functions `. +However, the special case of a type use that is syntactically empty or consists of only a single :ref:`result ` is not regarded as an :ref:`abbreviation ` for an inline :ref:`function type `, but is parsed directly into an optional :ref:`value type `. + .. math:: \begin{array}{llclll} + \production{block type} & \Tblocktype_I & + \begin{array}[t]{@{}c@{}} ::= \\ | \\ \end{array} + & + \begin{array}[t]{@{}lcll@{}} + (t{:}\Tresult)^? &\Rightarrow& t^? \\ + x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\}) \\ + \end{array} \\ \production{block instruction} & \Tblockinstr_I &::=& - \text{block}~~I'{:}\Tlabel_I~~\X{rt}{:}\Tresulttype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? - \\ &&&\qquad \Rightarrow\quad \BLOCK~\X{rt}~\X{in}^\ast~\END + \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\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{rt}{:}\Tresulttype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? - \\ &&&\qquad \Rightarrow\quad \LOOP~\X{rt}~\X{in}^\ast~\END + \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\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{rt}{:}\Tresulttype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ + \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\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{rt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END + \\ &&&\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) \\ \end{array} +.. note:: + The side condition stating that the :ref:`identifier context ` :math:`I'` must be empty in the rule for |Ttypeuse| block types enforces that no identifier can be bound in any |Tparam| declaration for a block type. + + .. _text-nop: .. _text-unreachable: .. _text-br: @@ -109,9 +124,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~~\Tresulttype~~\Tinstr^\ast~~\text{end} + \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{end} &\equiv& - \text{if}~~\Tlabel~~\Tresulttype~~\Tinstr^\ast~~\text{else}~~\text{end} + \text{if}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~~\text{else}~~\text{end} \end{array} diff --git a/document/core/text/types.rst b/document/core/text/types.rst index de5ed5f3..cefb53bc 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -22,23 +22,6 @@ Value Types \end{array} -.. index:: result type, value type - pair: text format; result type -.. _text-resulttype: - -Result Types -~~~~~~~~~~~~ - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{result type} & \Tresulttype &::=& - (t{:}\Tresult)^? &\Rightarrow& [t^?] \\ - \end{array} - -.. note:: - In future versions of WebAssembly, this scheme may be extended to support multiple results or more general result types. - - .. index:: function type, value type, result type pair: text format; function type .. _text-param: @@ -61,6 +44,7 @@ Function Types &\Rightarrow& t \\ \end{array} + Abbreviations ............. diff --git a/document/core/util/math.def b/document/core/util/math.def index a9c593b0..48242113 100644 --- a/document/core/util/math.def +++ b/document/core/util/math.def @@ -88,6 +88,7 @@ .. |s8| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{8}}} .. |s16| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{16}}} .. |s32| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{32}}} +.. |s33| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{33}}} .. |s64| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{64}}} .. |iN| mathdef:: \xref{syntax/values}{syntax-int}{\iX{N}} @@ -140,6 +141,7 @@ .. |valtype| mathdef:: \xref{syntax/types}{syntax-valtype}{\X{valtype}} .. |resulttype| mathdef:: \xref{syntax/types}{syntax-resulttype}{\X{resulttype}} .. |functype| mathdef:: \xref{syntax/types}{syntax-functype}{\X{functype}} + .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}} .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} .. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}} @@ -341,6 +343,8 @@ .. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}} .. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}} +.. |blocktype| mathdef:: \xref{syntax/instructions}{syntax-blocktype}{\X{blocktype}} + .. |instr| mathdef:: \xref{syntax/instructions}{syntax-instr}{\X{instr}} .. |expr| mathdef:: \xref{syntax/instructions}{syntax-expr}{\X{expr}} @@ -372,6 +376,7 @@ .. |BsN| mathdef:: \xref{binary/values}{binary-int}{\BsX{N}} .. |Bs32| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{32}}} +.. |Bs33| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{33}}} .. |Bs64| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{64}}} .. |BiN| mathdef:: \xref{binary/values}{binary-int}{\BiX{N}} @@ -395,7 +400,6 @@ .. |Bvaltype| mathdef:: \xref{binary/types}{binary-valtype}{\B{valtype}} .. |Bresulttype| mathdef:: \xref{binary/types}{binary-resulttype}{\B{resulttype}} -.. |Bblocktype| mathdef:: \xref{binary/types}{binary-blocktype}{\B{blocktype}} .. |Bfunctype| mathdef:: \xref{binary/types}{binary-functype}{\B{functype}} .. |Bglobaltype| mathdef:: \xref{binary/types}{binary-globaltype}{\B{globaltype}} .. |Btabletype| mathdef:: \xref{binary/types}{binary-tabletype}{\B{tabletype}} @@ -457,6 +461,7 @@ .. Instructions, non-terminals .. |Bmemarg| mathdef:: \xref{binary/instructions}{binary-memarg}{\B{memarg}} +.. |Bblocktype| mathdef:: \xref{binary/instructions}{binary-blocktype}{\B{blocktype}} .. |Binstr| mathdef:: \xref{binary/instructions}{binary-instr}{\B{instr}} .. |Bexpr| mathdef:: \xref{binary/instructions}{binary-expr}{\B{expr}} @@ -552,13 +557,14 @@ .. |Tvaltype| mathdef:: \xref{text/types}{text-valtype}{\T{valtype}} .. |Tresulttype| mathdef:: \xref{text/types}{text-resulttype}{\T{resulttype}} -.. |Tblocktype| mathdef:: \xref{text/types}{text-blocktype}{\T{blocktype}} .. |Tfunctype| mathdef:: \xref{text/types}{text-functype}{\T{functype}} + .. |Tglobaltype| mathdef:: \xref{text/types}{text-globaltype}{\T{globaltype}} .. |Ttabletype| mathdef:: \xref{text/types}{text-tabletype}{\T{tabletype}} .. |Telemtype| mathdef:: \xref{text/types}{text-elemtype}{\T{elemtype}} .. |Tmemtype| mathdef:: \xref{text/types}{text-memtype}{\T{memtype}} .. |Tlimits| mathdef:: \xref{text/types}{text-limits}{\T{limits}} + .. |Tparam| mathdef:: \xref{text/types}{text-functype}{\T{param}} .. |Tresult| mathdef:: \xref{text/types}{text-functype}{\T{result}} @@ -612,6 +618,8 @@ .. |Talign| mathdef:: \xref{text/instructions}{text-memarg}{\T{align}} .. |Toffset| mathdef:: \xref{text/instructions}{text-memarg}{\T{offset}} +.. |Tblocktype| mathdef:: \xref{text/instructions}{text-blocktype}{\T{blocktype}} + .. |Tlabel| mathdef:: \xref{text/instructions}{text-label}{\T{label}} .. |Tinstr| mathdef:: \xref{text/instructions}{text-instr}{\T{instr}} .. |Tplaininstr| mathdef:: \xref{text/instructions}{text-plaininstr}{\T{plaininstr}} @@ -775,6 +783,11 @@ .. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}} +.. Stack, meta functions + +.. |expand| mathdef:: \xref{exec/runtime}{syntax-frame}{\F{expand}} + + .. Administrative Instructions, terminals .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 1596ed18..6f1b10db 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -172,15 +172,17 @@ and there is one respective rule for each relevant construct :math:`A` of the ab .. math:: \frac{ - C,\LABEL\,[t^?] \vdash \instr^\ast : [] \to [t^?] + C \vdash \blocktype : [t_1^\ast] \to [t_2^\ast] + \qquad + C,\LABEL\,[t_2^\ast] \vdash \instr^\ast : [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?] + C \vdash \BLOCK~\blocktype~\instr^\ast~\END : [t_1^\ast] \to [t_2^\ast] } A |BLOCK| instruction is only valid when the instruction sequence in its body is. - Moreover, the result type must match the block's annotation :math:`[t^?]`. + Moreover, the result type must match the block's annotation :math:`\blocktype`. If so, then the |BLOCK| instruction has the same type as the body. - Inside the body an additional label of the same type is available, + Inside the body an additional label of the corresponding result type is available, which is expressed by extending the context :math:`C` with the additional label information for the premise. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 8d6aa30f..82604905 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -425,7 +425,7 @@ Memory Instructions } -.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism, context +.. index:: control instructions, structured control, label, block, branch, block type, result type, label index, function index, type index, vector, polymorphism, context pair: validation; instruction single: abstract syntax; instruction .. _valid-label: @@ -467,80 +467,80 @@ Control Instructions .. _valid-block: -:math:`\BLOCK~[t^?]~\instr^\ast~\END` -..................................... +:math:`\BLOCK~\blocktype~\instr^\ast~\END` +.......................................... -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t^?]` prepended to the |CLABELS| vector. +* The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^?]`. + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. -* Then the compound instruction is valid with type :math:`[] \to [t^?]`. +* Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. .. math:: \frac{ - C,\CLABELS\,[t^?] \vdash \instr^\ast : [] \to [t^?] + C \vdash \blocktype : [t_1^\ast] \to [t_2^\ast] + \qquad + C,\CLABELS\,[t_2^\ast] \vdash \instr^\ast : [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?] + C \vdash \BLOCK~\blocktype~\instr^\ast~\END : [t_1^\ast] \to [t_2^\ast] } -.. note:: - The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the block was entered. - This may be generalized in future versions of WebAssembly. - .. _valid-loop: -:math:`\LOOP~[t^?]~\instr^\ast~\END` -.................................... +:math:`\LOOP~\blocktype~\instr^\ast~\END` +......................................... + +* The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the empty :ref:`result type ` :math:`[]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the empty :ref:`result type ` :math:`[t_1^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^?]`. + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. -* Then the compound instruction is valid with type :math:`[] \to [t^?]`. +* Then the compound instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. .. math:: \frac{ - C,\CLABELS\,[] \vdash \instr^\ast : [] \to [t^?] + C \vdash \blocktype : [t_1^\ast] \to [t_2^\ast] + \qquad + C,\CLABELS\,[t_1^\ast] \vdash \instr^\ast : [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?] + C \vdash \LOOP~\blocktype~\instr^\ast~\END : [t_1^\ast] \to [t_2^\ast] } -.. note:: - The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the loop was entered. - This may be generalized in future versions of WebAssembly. - .. _valid-if: -:math:`\IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END` -........................................................ +:math:`\IF~\blocktype~\instr_1^\ast~\ELSE~\instr_2^\ast~\END` +............................................................. + +* The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the empty :ref:`result type ` :math:`[t^?]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the empty :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, - the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[] \to [t^?]`. + the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. * Under context :math:`C'`, - the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[] \to [t^?]`. + the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. -* Then the compound instruction is valid with type :math:`[\I32] \to [t^?]`. +* Then the compound instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_2^\ast]`. .. math:: \frac{ - C,\CLABELS\,[t^?] \vdash \instr_1^\ast : [] \to [t^?] + C \vdash \blocktype : [t_1^\ast] \to [t_2^\ast] \qquad - C,\CLABELS\,[t^?] \vdash \instr_2^\ast : [] \to [t^?] + C,\CLABELS\,[t_2^\ast] \vdash \instr_1^\ast : [t_1^\ast] \to [t_2^\ast] + \qquad + C,\CLABELS\,[t_2^\ast] \vdash \instr_2^\ast : [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?] + C \vdash \IF~\blocktype~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [t_1^\ast~\I32] \to [t_2^\ast] } -.. note:: - The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the conditional was entered. - This may be generalized in future versions of WebAssembly. - .. _valid-br: @@ -549,15 +549,15 @@ Control Instructions * The label :math:`C.\CLABELS[l]` must be defined in the context. -* Let :math:`[t^?]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. +* 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^?] \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:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - C.\CLABELS[l] = [t^?] + C.\CLABELS[l] = [t^\ast] }{ - C \vdash \BR~l : [t_1^\ast~t^?] \to [t_2^\ast] + C \vdash \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast] } .. note:: @@ -571,15 +571,15 @@ Control Instructions * The label :math:`C.\CLABELS[l]` must be defined in the context. -* Let :math:`[t^?]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. +* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l]`. -* Then the instruction is valid with type :math:`[t^?~\I32] \to [t^?]`. +* Then the instruction is valid with type :math:`[t^\ast~\I32] \to [t^\ast]`. .. math:: \frac{ - C.\CLABELS[l] = [t^?] + C.\CLABELS[l] = [t^\ast] }{ - C \vdash \BRIF~l : [t^?~\I32] \to [t^?] + C \vdash \BRIF~l : [t^\ast~\I32] \to [t^\ast] } @@ -590,23 +590,23 @@ Control Instructions * The label :math:`C.\CLABELS[l]` must be defined in the context. -* Let :math:`[t^?]` be the :ref:`result type ` :math:`C.\CLABELS[l_N]`. +* Let :math:`[t^\ast]` be the :ref:`result type ` :math:`C.\CLABELS[l_N]`. * For all :math:`l_i` in :math:`l^\ast`, the label :math:`C.\CLABELS[l_i]` must be defined in the context. * For all :math:`l_i` in :math:`l^\ast`, - :math:`C.\CLABELS[l_i]` must be :math:`t^?`. + :math:`C.\CLABELS[l_i]` must be :math:`t^\ast`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^?~\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:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - (C.\CLABELS[l] = [t^?])^\ast + (C.\CLABELS[l] = [t^\ast])^\ast \qquad - C.\CLABELS[l_N] = [t^?] + C.\CLABELS[l_N] = [t^\ast] }{ - C \vdash \BRTABLE~l^\ast~l_N : [t_1^\ast~t^?~\I32] \to [t_2^\ast] + C \vdash \BRTABLE~l^\ast~l_N : [t_1^\ast~t^\ast~\I32] \to [t_2^\ast] } .. note:: @@ -620,15 +620,15 @@ Control Instructions * The return type :math:`C.\CRETURN` must not be empty in the context. -* Let :math:`[t^?]` be the :ref:`result type ` of :math:`C.\CRETURN`. +* 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^?] \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:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - C.\CRETURN = [t^?] + C.\CRETURN = [t^\ast] }{ - C \vdash \RETURN : [t_1^\ast~t^?] \to [t_2^\ast] + C \vdash \RETURN : [t_1^\ast~t^\ast] \to [t_2^\ast] } .. note:: @@ -727,7 +727,7 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` } -.. index:: expression +.. index:: expression,result type pair: validation; expression single: abstract syntax; expression single: expression; constant @@ -736,22 +736,22 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` Expressions ~~~~~~~~~~~ -Expressions :math:`\expr` are classified by :ref:`result types ` of the form :math:`[t^?]`. +Expressions :math:`\expr` are classified by :ref:`result types ` of the form :math:`[t^\ast]`. :math:`\instr^\ast~\END` ........................ -* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^?]`, - for some optional :ref:`value type ` :math:`t^?`. +* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`, + for some :ref:`result type ` :math:`[t^\ast]`. -* Then the expression is valid with :ref:`result type ` :math:`[t^?]`. +* Then the expression is valid with :ref:`result type ` :math:`[t^\ast]`. .. math:: \frac{ - C \vdash \instr^\ast : [] \to [t^?] + C \vdash \instr^\ast : [] \to [t^\ast] }{ - C \vdash \instr^\ast~\END : [t^?] + C \vdash \instr^\ast~\END : [t^\ast] } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 10dcd05c..87ca1bcd 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -14,7 +14,7 @@ Furthermore, most definitions are themselves classified with a suitable type. Functions ~~~~~~~~~ -Functions :math:`\func` are classified by :ref:`function types ` of the form :math:`[t_1^\ast] \to [t_2^?]`. +Functions :math:`\func` are classified by :ref:`function types ` of the form :math:`[t_1^\ast] \to [t_2^\ast]`. :math:`\{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \}` @@ -22,34 +22,31 @@ Functions :math:`\func` are classified by :ref:`function types * The type :math:`C.\CTYPES[x]` must be defined in the context. -* Let :math:`[t_1^\ast] \to [t_2^?]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. +* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`C.\CTYPES[x]`. * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with: * |CLOCALS| set to the sequence of :ref:`value types ` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals, - * |CLABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^?]`. + * |CLABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^\ast]`. - * |CRETURN| set to the :ref:`result type ` :math:`[t_2^?]`. + * |CRETURN| set to the :ref:`result type ` :math:`[t_2^\ast]`. * Under the context :math:`C'`, - the expression :math:`\expr` must be valid with type :math:`t_2^?`. + the expression :math:`\expr` must be valid with type :math:`[t_2^\ast]`. -* Then the function definition is valid with type :math:`[t_1^\ast] \to [t_2^?]`. +* Then the function definition is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. .. math:: \frac{ - C.\CTYPES[x] = [t_1^\ast] \to [t_2^?] + C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] \qquad - C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdash \expr : [t_2^?] + C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdash \expr : [t_2^\ast] }{ - C \vdash \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?] + C \vdash \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^\ast] } -.. note:: - The restriction on the length of the result types :math:`t_2^\ast` may be lifted in future versions of WebAssembly. - .. index:: table, table type, limits, element type pair: validation; table diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index b30008e7..7dbf6d31 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -2,34 +2,46 @@ Types ----- Most :ref:`types ` are universally valid. -However, restrictions apply to :ref:`function types ` and :ref:`limits `, which must be checked during validation. +However, restrictions apply to :ref:`limits `, which must be checked during validation. +Moreover, :ref:`block types ` are converted to plain :ref:`function types ` for ease of processing. -.. index:: function type - pair: validation; function type - single: abstract syntax; function type -.. _valid-functype: +.. index:: block type + pair: validation; block type + single: abstract syntax; block type +.. _valid-blocktype: -Function Types -~~~~~~~~~~~~~~ +Block Types +~~~~~~~~~~~ -:ref:`Function types ` may not specify more than one result. +:ref:`Block types ` may be expressed in one of two forms, both of which are converted to plain :ref:`function types ` by the following rules. -:math:`[t_1^n] \to [t_2^m]` -........................... +:math:`\typeidx` +................ -* The arity :math:`m` must not be larger than :math:`1`. +* The type :math:`C.\CTYPES[\typeidx]` must be defined in the context. -* Then the function type is valid. +* Then the block type is valid as :ref:`function type ` :math:`C.\CTYPES[\typeidx]`. .. math:: \frac{ + C.\CTYPES[\typeidx] = \functype }{ - \vdash [t_1^\ast] \to [t_2^?] \ok + C \vdash \typeidx : \functype + } + + +:math:`[\valtype^?]` +.................... + +* The block type is valid as :ref:`function type ` :math:`[] \to [\valtype^?]`. + +.. math:: + \frac{ + }{ + C \vdash [\valtype^?] : [] \to [\valtype^?] } -.. note:: - This restriction may be removed in future versions of WebAssembly. .. index:: limits