Instructions¶
Instructions are classified by instruction types that describe how they manipulate the operand stack and initialize locals: A type \({t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast}\) describes the required input stack with argument values of types \({t_1^\ast}\) that an instruction pops off and the provided output stack with result values of types \({t_2^\ast}\) that it pushes back. Moreover, it enumerates the indices \({x^\ast}\) of locals that have been set by the instruction. In most cases, this is empty.
Note
For example, the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) has type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\), consuming two \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) values and producing one. The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}set}}~x)\) has type \(t \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} \epsilon\), provided \(t\) is the type declared for the local \(x\).
Typing extends to instruction sequences \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\). Such a sequence has an instruction type \({t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast}\) if the accumulative effect of executing the instructions is consuming values of types \({t_1^\ast}\) off the operand stack, pushing new values of types \({t_2^\ast}\), and setting all locals \({x^\ast}\).
For some instructions, the typing rules do not fully constrain the type, and therefore allow for multiple types. Such instructions are called polymorphic. Two degrees of polymorphism can be distinguished:
value-polymorphic: the value type \(t\) of one or several individual operands is unconstrained. That is the case for all parametric instructions like \(\mathsf{drop}\) and \(\mathsf{select}\).
stack-polymorphic: the entire (or most of the) instruction type \({t_1^\ast} \rightarrow {t_2^\ast}\) of the instruction is unconstrained. That is the case for all control instructions that perform an unconditional control transfer, such as \(\mathsf{unreachable}\), \(\mathsf{br}\), or \(\mathsf{return}\).
In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.
Note
For example, the \(\mathsf{select}\) instruction is valid with type \(t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t\), for any possible number type \(t\). Consequently, both instruction sequences
and
are valid, with \(t\) in the typing of \(\mathsf{select}\) being instantiated to \(\mathsf{i{\scriptstyle 32}}\) or \(\mathsf{f{\scriptstyle 64}}\), respectively.
The \(\mathsf{unreachable}\) instruction is stack-polymorphic, and hence valid with type \({t_1^\ast} \rightarrow {t_2^\ast}\) for any possible sequences of value types \({t_1^\ast}\) and \({t_2^\ast}\). Consequently,
is valid by assuming type \(\epsilon \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) for the \(\mathsf{unreachable}\) instruction. In contrast,
is invalid, because there is no possible type to pick for the \(\mathsf{unreachable}\) instruction that would make the sequence well-typed.
The Appendix describes a type checking algorithm that efficiently implements validation of instruction sequences as prescribed by the rules given here.
Parametric Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\) is valid with the instruction type \(\epsilon~\rightarrow~\epsilon\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:
The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.
Note
The \(\mathsf{unreachable}\) instruction is stack-polymorphic.
\(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\) is valid with the instruction type \(t~\rightarrow~\epsilon\) if:
The value type \(t\) is valid.
Note
Both \(\mathsf{drop}\) and \(\mathsf{select}\) without annotation are value-polymorphic instructions.
\(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~(t^\ast)^?\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?})\) is valid with the instruction type \(t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~t\) if:
The value type \(t\) is valid.
Either:
The value type sequence \({{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) is of the form \(t\).
Or:
The value type sequence \({{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) is absent.
The value type \(t\) matches the value type \({t'}\).
The value type \({t'}\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({t'}\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).
Note
In future versions of WebAssembly, \(\mathsf{select}\) may allow more than one value per choice.
Numeric Instructions¶
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)¶
The instruction \(({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{nt}})\) is valid with the instruction type \(\epsilon~\rightarrow~{\mathit{nt}}\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}}\)¶
The instruction \(({\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~\rightarrow~{\mathit{nt}}\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}\)¶
The instruction \(({\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~{\mathit{nt}}~\rightarrow~{\mathit{nt}}\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}}\)¶
The instruction \(({\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}}\)¶
The instruction \(({\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~{\mathit{nt}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(t_1\mathsf{.}\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}\mathsf{\_}t_2\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\)¶
The instruction \(({\mathit{nt}}_1 {.} {{\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}}}{\mathsf{\_}}{{\mathit{nt}}_2})\) is valid with the instruction type \({\mathit{nt}}_2~\rightarrow~{\mathit{nt}}_1\).
Reference Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~\mathit{ht}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}})\) is valid with the instruction type \(\epsilon~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}})\) if:
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}})\) if:
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}is\_null}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}is\_null}}\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) if:
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}as\_non\_null}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}as\_non\_null}}\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}})~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}})\) if:
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}eq}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}eq}}\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}})~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}test}}~\mathit{rt}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}test}}~{\mathit{rt}})\) is valid with the instruction type \({\mathit{rt}'}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) if:
The reference type \({\mathit{rt}}\) is valid.
The reference type \({\mathit{rt}'}\) is valid.
The reference type \({\mathit{rt}}\) matches the reference type \({\mathit{rt}'}\).
Note
The liberty to pick a supertype \({\mathit{rt}'}\) allows typing the instruction with the least precise super type of \({\mathit{rt}}\) as input, that is, the top type in the corresponding heap subtyping hierarchy.
\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}cast}}~\mathit{rt}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}cast}}~{\mathit{rt}})\) is valid with the instruction type \({\mathit{rt}'}~\rightarrow~{\mathit{rt}}\) if:
The reference type \({\mathit{rt}}\) is valid.
The reference type \({\mathit{rt}'}\) is valid.
The reference type \({\mathit{rt}}\) matches the reference type \({\mathit{rt}'}\).
Note
The liberty to pick a supertype \({\mathit{rt}'}\) allows typing the instruction with the least precise super type of \({\mathit{rt}}\) as input, that is, the top type in the corresponding heap subtyping hierarchy.
Aggregate Reference Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x)\) is valid with the instruction type \({t^\ast}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast})\).
Let \({t^\ast}\) be the value type sequence \({{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})^\ast}\).
\(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast})\).
For all \({\mathit{zt}}\) in \({{\mathit{zt}}^\ast}\):
A default value for the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.
\(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}get}}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?~x~y\)¶
The instruction \(({\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}get}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~x~i)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\rightarrow~t\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}^\ast})\).
The length of \({{\mathit{yt}}^\ast}\) is greater than \(i\).
The field type \({{\mathit{yt}}^\ast}{}[i]\) is of the form \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})\).
The signedness \({{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}\) is absent if and only if the storage type \({\mathit{zt}}\) is of the form \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}set}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}set}}~x~i)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~t~\rightarrow~\epsilon\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}^\ast})\).
The length of \({{\mathit{yt}}^\ast}\) is greater than \(i\).
The field type \({{\mathit{yt}}^\ast}{}[i]\) is of the form \((\mathsf{mut}~{\mathit{zt}})\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x)\) is valid with the instruction type \(t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x)\) is valid with the instruction type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
A default value for the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x~n\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x~n)\) is valid with the instruction type \({t^{n}}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_elem}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_elem}}~x~y)\) is valid with the instruction type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{rt}}))\).
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) matches the reference type \({\mathit{rt}}\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_data}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_data}}~x~y)\) is valid with the instruction type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
The value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) exists.
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is of the form \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}get}}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?~x\)¶
The instruction \(({\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}get}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~x)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~t\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
The signedness \({{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}\) is absent if and only if the storage type \({\mathit{zt}}\) is of the form \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}set}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}set}}~x)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t~\rightarrow~\epsilon\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}len}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}len}}\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}fill}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}fill}}~x)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).
Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}copy}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}copy}}~x_1~x_2)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x_1)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x_2)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}_1))\).
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}_2))\).
The storage type \({\mathit{zt}}_2\) matches the storage type \({\mathit{zt}}_1\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}init\_elem}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}init\_elem}}~x~y)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) matches the storage type \({\mathit{zt}}\).
\(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}init\_data}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}init\_data}}~x~y)\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).
The value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) exists.
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is of the form \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).
Scalar Reference Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}}\) is valid with the instruction type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}})\).
\(\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{i{\scriptstyle31}{.}get}}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)¶
The instruction \(({\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{i{\scriptstyle31}{.}get}}}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}})\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
External Reference Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}}\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{1}^?}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}})~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}})\) if:
\({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{1}^?}}\) is of the form \({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}\).
\(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}}\) is valid with the instruction type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{1}^?}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}})~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}})\) if:
\({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{1}^?}}\) is of the form \({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}\).
Vector Instructions¶
Vector instructions can have a prefix to describe the shape of the operand. Packed numeric types, \(\href{../syntax/types.html#syntax-storagetype}{\mathsf{i\scriptstyle8}}\) and \(\href{../syntax/types.html#syntax-storagetype}{\mathsf{i\scriptstyle16}}\), are not value types. An auxiliary function maps such packed type shapes to value types:
\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)\) is valid with the instruction type \(\epsilon~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvtestop}{\mathit{vvtestop}}\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvtestop}{\mathit{vvtestop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vternop}{\mathit{vternop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vternop}{\mathit{vternop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vtestop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vtestop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vshiftop}{\mathit{vishiftop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vshiftop}{\mathit{vshiftop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}}\)¶
The instruction \(({\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).
\(\mathsf{i8x16.}\href{../syntax/instructions.html#syntax-vswizzlop}{\mathit{vswizzlop}}\)¶
The instruction \(({\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vswizzlop}{\mathit{vswizzlop}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}^{16}\)¶
The instruction \(({\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~{i^\ast})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
For all \(i\) in \({i^\ast}\):
The lane index \(i\) is less than \(2 \cdot {\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}})\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}}\)¶
The instruction \(({\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}})\) is valid with the instruction type \(t~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
Let \(t\) be the number type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extract\_lane}}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)¶
The instruction \(({{\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extract\_lane}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~i)\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~t\) if:
The lane index \(i\) is less than \({\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}})\).
Let \(t\) be the number type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{replace\_lane}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)¶
The instruction \(({\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{replace\_lane}}~i)\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~t~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
The lane index \(i\) is less than \({\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}})\).
Let \(t\) be the number type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_1\mathsf{.}\href{../syntax/instructions.html#syntax-vextunop}{\mathit{vextunop}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\)¶
The instruction \(({\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vextunop}{\mathit{vextunop}}}}{\mathsf{\_}}{{\mathit{sh}}_2})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_1\mathsf{.}\href{../syntax/instructions.html#syntax-vextbinop}{\mathit{vextbinop}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\)¶
The instruction \(({\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vextbinop}{\mathit{vextbinop}}}}{\mathsf{\_}}{{\mathit{sh}}_2})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_1\mathsf{.}\href{../syntax/instructions.html#syntax-vextternop}{\mathit{vextternop}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\)¶
The instruction \(({\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vextternop}{\mathit{vextternop}}}}{\mathsf{\_}}{{\mathit{sh}}_2})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_1\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{narrow}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)¶
The instruction \(({{\mathit{sh}}_1{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{narrow}}}{\mathsf{\_}}{{\mathit{sh}}_2}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}\href{../syntax/instructions.html#syntax-half}{\mathit{half}}^?\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\mathsf{\_zero}^?\)¶
The instruction \(({\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-zero}{\mathit{zero}}}^?}}{\mathsf{\_}}{{\mathit{sh}}_2}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-half}{\mathit{half}}}^?}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).
Variable Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}get}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}get}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~t\) if:
\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}set}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}set}}~x)\) is valid with the instruction type \(t~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{x}\,\epsilon\) if:
\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}tee}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}tee}}~x)\) is valid with the instruction type \(t~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{x}\,t\) if:
\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~t\) if:
\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}set}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}set}}~x)\) is valid with the instruction type \(t~\rightarrow~\epsilon\) if:
Table Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}get}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}get}}~x)\) is valid with the instruction type \({\mathit{at}}~\rightarrow~{\mathit{rt}}\) if:
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}set}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}set}}~x)\) is valid with the instruction type \({\mathit{at}}~{\mathit{rt}}~\rightarrow~\epsilon\) if:
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}size}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}size}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~{\mathit{at}}\) if:
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}grow}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}grow}}~x)\) is valid with the instruction type \({\mathit{rt}}~{\mathit{at}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) if:
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}fill}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}fill}}~x)\) is valid with the instruction type \({\mathit{at}}~{\mathit{rt}}~{\mathit{at}}~\rightarrow~\epsilon\) if:
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}copy}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}copy}}~x_1~x_2)\) is valid with the instruction type \({\mathit{at}}_1~{\mathit{at}}_2~t~\rightarrow~\epsilon\) if:
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_1]\) exists.
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_1]\) is of the form \(({\mathit{at}}_1~{\mathit{lim}}_1~{\mathit{rt}}_1)\).
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_2]\) exists.
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_2]\) is of the form \(({\mathit{at}}_2~{\mathit{lim}}_2~{\mathit{rt}}_2)\).
The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}_1\).
Let \(t\) be the address type \({\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2)\).
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}init}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}init}}~x~y)\) is valid with the instruction type \({\mathit{at}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}}_1)\).
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) is of the form \({\mathit{rt}}_2\).
The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}_1\).
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~\epsilon\) if:
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[x]\) exists.
The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[x]\) is of the form \({\mathit{rt}}\).
Memory Instructions¶
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~{\mathit{nt}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \({|{\mathit{nt}}|} / 8\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({{\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{M}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~{\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(M / 8\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~{\mathit{nt}}~\rightarrow~\epsilon\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \({|{\mathit{nt}}|} / 8\).
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({{\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{M}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~{\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}~\rightarrow~\epsilon\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(M / 8\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \({|\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}|} / 8\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{M}{\href{../syntax/instructions.html#syntax-shape}{\mathsf{x}}}{N}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(M / 8 \cdot N\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{N}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{splat}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(N / 8\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \(({\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{N}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{zero}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(N / 8\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)¶
The instruction \(({\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{N}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{lane}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}~i)\) is valid with the instruction type \({\mathit{at}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(N / 8\).
\(i\) is less than \(128 / N\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)¶
The instruction \((\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\epsilon\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \({|\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}|} / 8\).
\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)¶
The instruction \(({\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{N}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{lane}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}~i)\) is valid with the instruction type \({\mathit{at}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\epsilon\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
\({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}}\) is less than or equal to \(N / 8\).
\(i\) is less than \(128 / N\).
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}size}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}size}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~{\mathit{at}}\) if:
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}grow}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}grow}}~x)\) is valid with the instruction type \({\mathit{at}}~\rightarrow~{\mathit{at}}\) if:
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}fill}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}fill}}~x)\) is valid with the instruction type \({\mathit{at}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\mathit{at}}~\rightarrow~\epsilon\) if:
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}copy}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}copy}}~x_1~x_2)\) is valid with the instruction type \({\mathit{at}}_1~{\mathit{at}}_2~t~\rightarrow~\epsilon\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_1]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_1]\) is of the form \(({\mathit{at}}_1~{\mathit{lim}}_1~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_2]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_2]\) is of the form \(({\mathit{at}}_2~{\mathit{lim}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
Let \(t\) be the address type \({\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2)\).
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}init}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}init}}~x~y)\) is valid with the instruction type \({\mathit{at}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.
The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) exists.
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is of the form \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data{.}drop}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data{.}drop}}~x)\) is valid with the instruction type \(\epsilon~\rightarrow~\epsilon\) if:
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[x]\) exists.
The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[x]\) is of the form \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).
Control Instructions¶
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:
The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).
Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).
Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).
Note
The notation \(\{ \begin{array}[t]{@{}l@{}} \href{../valid/conventions.html#context}{\mathsf{labels}}~({t^\ast}) \}\end{array} \oplus C\) inserts the new label type at index \(0\), shifting all others. The same applies to all other block instructions.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:
The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).
Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_1^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).
Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast})\) is valid with the instruction type \({t_1^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) if:
The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).
Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).
Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}}\,{t_2^\ast}\).
Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_2^\ast}}\,{t_2^\ast}\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try\_table}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try\_table}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}^\ast}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:
The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).
Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).
Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).
For all \({\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}\) in \({{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}^\ast}\):
The catch clause \({\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}\) is valid.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~l\)¶
The catch clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~l)\) is valid if:
The tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) exists.
The expansion of the tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~\epsilon)\).
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_ref}}~x~l\)¶
The catch clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_ref}}~x~l)\) is valid if:
The tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) exists.
The expansion of the tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~\epsilon)\).
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The result type \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}})\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~l\)¶
The catch clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~l)\) is valid if:
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The result type \(\epsilon\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all\_ref}}~l\)¶
The catch clause \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all\_ref}}~l)\) is valid if:
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The result type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}})\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l)\) is valid with the instruction type \({t_1^\ast}~{t^\ast}~\rightarrow~{t_2^\ast}\) if:
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}\).
The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.
Note
The label index space in the context \(C\) contains the most recent label first, so that \(C{.}\mathsf{labels}{}[l]\) performs a relative lookup as expected. This applies to other branch instructions as well.
The \(\mathsf{br}\) instruction is stack-polymorphic.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l)\) is valid with the instruction type \({t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t^\ast}\) if:
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~{l^\ast}~{l'})\) is valid with the instruction type \({t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) if:
For all \(l\) in \({l^\ast}\):
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
For all \(l\) in \({l^\ast}\):
The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}]\) exists.
The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}]\).
The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.
Note
The \(\mathsf{br\_table}\) instruction is stack-polymorphic.
Furthermore, the result type \({t^\ast}\) is also chosen non-deterministically in this rule. Although it may seem necessary to compute \({t^\ast}\) as the greatest lower bound of all label types in practice, a simple sequential algorithm does not require this.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_null}}~l\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_null}}~l)\) is valid with the instruction type \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}})~\rightarrow~{t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}})\) if:
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l)\) is valid with the instruction type \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}})~\rightarrow~{t^\ast}\) if:
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast}}~l~\mathit{rt}_1~\mathit{rt}_2\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2)\) is valid with the instruction type \({t^\ast}~{\mathit{rt}}_1~\rightarrow~{t^\ast}~{t'}\) if:
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}~{\mathit{rt}}\).
The reference type \({\mathit{rt}}_1\) is valid.
The reference type \({\mathit{rt}}_2\) is valid.
The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}_1\).
The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}\).
Let \({t'}\) be the reference type \({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~\mathit{rt}_1~\mathit{rt}_2\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2)\) is valid with the instruction type \({t^\ast}~{\mathit{rt}}_1~\rightarrow~{t^\ast}~{\mathit{rt}}_2\) if:
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.
The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}~{\mathit{rt}}\).
The reference type \({\mathit{rt}}_1\) is valid.
The reference type \({\mathit{rt}}_2\) is valid.
The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}_1\).
The reference type \({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x)\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:
The function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) exists.
The expansion of the function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_ref}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_ref}}~x)\) is valid with the instruction type \({t_1^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\rightarrow~{t_2^\ast}\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y)\) is valid with the instruction type \({t_1^\ast}~{\mathit{at}}~\rightarrow~{t_2^\ast}\) if:
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).
The reference type \({\mathit{rt}}\) matches the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}})\).
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\) is valid with the instruction type \({t_1^\ast}~{t^\ast}~\rightarrow~{t_2^\ast}\) if:
The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({t^\ast}\).
The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.
Note
The \(\mathsf{return}\) instruction is stack-polymorphic.
\(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is absent (set to \(\epsilon\)) when validating an expression that is not a function body. This differs from it being set to the empty result type \({}[\epsilon]\), which is the case for functions not returning anything.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call}}~x)\) is valid with the instruction type \({t_3^\ast}~{t_1^\ast}~\rightarrow~{t_4^\ast}\) if:
The function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) exists.
The expansion of the function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).
The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({{t'}_2^\ast}\).
The result type \({t_2^\ast}\) matches the result type \({{t'}_2^\ast}\).
The instruction type \({t_3^\ast}~\rightarrow~{t_4^\ast}\) is valid.
Note
The \(\mathsf{return\_call}\) instruction is stack-polymorphic.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call\_ref}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call\_ref}}~x)\) is valid with the instruction type \({t_3^\ast}~{t_1^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x)~\rightarrow~{t_4^\ast}\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).
The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({{t'}_2^\ast}\).
The result type \({t_2^\ast}\) matches the result type \({{t'}_2^\ast}\).
The instruction type \({t_3^\ast}~\rightarrow~{t_4^\ast}\) is valid.
Note
The \(\mathsf{return\_call\_ref}\) instruction is stack-polymorphic.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call\_indirect}}~x~y\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call\_indirect}}~x~y)\) is valid with the instruction type \({t_3^\ast}~{t_1^\ast}~{\mathit{at}}~\rightarrow~{t_4^\ast}\) if:
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.
The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).
The reference type \({\mathit{rt}}\) matches the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}})\).
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) exists.
The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).
The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({{t'}_2^\ast}\).
The result type \({t_2^\ast}\) matches the result type \({{t'}_2^\ast}\).
The instruction type \({t_3^\ast}~\rightarrow~{t_4^\ast}\) is valid.
Note
The \(\mathsf{return\_call\_indirect}\) instruction is stack-polymorphic.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw}}~x\)¶
The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw}}~x)\) is valid with the instruction type \({t_1^\ast}~{t^\ast}~\rightarrow~{t_2^\ast}\) if:
The tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) exists.
The expansion of the tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~\epsilon)\).
The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.
Note
The \(\mathsf{throw}\) instruction is stack-polymorphic.
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\)¶
The instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}}\) is valid with the instruction type \({t_1^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}})~\rightarrow~{t_2^\ast}\) if:
The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.
Note
The \(\mathsf{throw\_ref}\) instruction is stack-polymorphic.
Instruction Sequences¶
Typing of instruction sequences is defined recursively.
Empty Instruction Sequence: \(\epsilon\)¶
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is valid with the instruction type \({\mathit{it}''}\) if:
Either:
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is empty.
The instruction type \({\mathit{it}''}\) is of the form \(\epsilon~\rightarrow~\epsilon\).
Or:
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is of the form \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\).
The instruction type \({\mathit{it}''}\) is of the form \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}~{x_2^\ast}}\,{t_3^\ast}\).
The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}}\,{t_2^\ast}\).
The length of \({{\href{../valid/conventions.html#syntax-init}{\mathit{init}}}^\ast}\) is equal to the length of \({t^\ast}\).
The length of \({{\href{../valid/conventions.html#syntax-init}{\mathit{init}}}^\ast}\) is equal to the length of \({x_1^\ast}\).
For all \(x_1\) in \({x_1^\ast}\):
The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x_1]\) exists.
For all \({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}\) in \({{\href{../valid/conventions.html#syntax-init}{\mathit{init}}}^\ast}\), and corresponding \(t\) in \({t^\ast}\), and corresponding \(x_1\) in \({x_1^\ast}\):
The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x_1]\) is of the form \(({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t)\).
Under the context \(C{}[{.}\href{../syntax/modules.html#syntax-local}{\mathsf{local}}{}[{x_1^\ast}] = {(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t)^\ast}]\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\) is valid with the instruction type \({t_2^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_2^\ast}}\,{t_3^\ast}\).
Or:
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is of the form \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\).
The instruction type \({\mathit{it}''}\) is of the form \({\mathit{it}'}\).
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({\mathit{it}}\).
The instruction type \({\mathit{it}}\) matches the instruction type \({\mathit{it}'}\).
The instruction type \({\mathit{it}'}\) is valid.
Or:
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is of the form \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\).
The instruction type \({\mathit{it}''}\) is of the form \({t^\ast}~{t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t^\ast}~{t_2^\ast}\).
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).
The result type \({t^\ast}\) is valid.
Note
In combination with the previous rule, subsumption allows to compose instructions whose types would not directly fit otherwise. For example, consider the instruction sequence
To type this sequence, its subsequence \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~2)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\) needs to be valid with an intermediate type. But the direct type of \((\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~2)\) is \(\epsilon \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\), not matching the two inputs expected by \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\). The subsumption rule allows to weaken the type of \((\mathsf{const}~\mathsf{i{\scriptstyle 32}}~2)\) to the supertype \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\), such that it can be composed with \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) and yields the intermediate type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) for the subsequence. That can in turn be composed with the first constant.
Furthermore, subsumption allows to drop init variables \({x^\ast}\) from the instruction type in a context where they are not needed, for example, at the end of the body of a block.
Expressions¶
Expressions \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) are classified by result types \({t^\ast}\).
The expression \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the result type \({t^\ast}\) if:
The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \(\epsilon~\rightarrow~{t^\ast}\).
Constant Expressions¶
In a constant expression, all instructions must be constant.
\({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is constant if:
For all \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}\) in \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\):
\({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}\) is constant.
\({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is constant if:
Either:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \(({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{nt}})\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \(({\mathit{vt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{vt}})\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}})\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \(\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}}\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x~n)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}}\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}}\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x)\).
The global \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) exists.
The global \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) is of the form \((\epsilon~t)\).
Or:
The value \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}\) is of the form \(({\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}} {.} {\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}})\).
\({\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}\) is contained in [\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\); \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}\)].
\({\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}}\) is contained in [\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\); \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{sub}}\); \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\)].
Note
Currently, constant expressions occurring in globals are further constrained in that contained \(\mathsf{global{.}get}\) instructions are only allowed to refer to imported or previously defined globals. Constant expressions occurring in tables may only have \(\mathsf{global{.}get}\) instructions that refer to imported globals. This is enforced in the validation rule for modules by constraining the context \(C\) accordingly.
The definition of constant expression may be extended in future versions of WebAssembly.