Instructions — WebAssembly 3.0 (2025-09-21) (original) (raw)

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

\[(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~1)~(\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{const}}~3)~(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}})\]

and

\[(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+64})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+64})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+64})~(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}})\]

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,

\[(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\]

is valid by assuming type \(\epsilon \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) for the \(\mathsf{unreachable}\) instruction. In contrast,

\[(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\]

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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} : \epsilon \rightarrow \epsilon } \qquad \end{array}\]

\(\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}} : t \rightarrow \epsilon } \qquad \end{array}\]

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}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~t : t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t } \qquad \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-valtype}{\leq} {t'} \qquad {t'} = {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} \lor {t'} = {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}} : t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t } \qquad \end{array}\]

Note

In future versions of WebAssembly, \(\mathsf{select}\) may allow more than one value per choice.

Control Instructions¶

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/types.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶

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}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

Note

The notation \(\{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t^\ast}) \} \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/types.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶

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}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_1^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\href{../syntax/types.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\)¶

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}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_1^\ast}} {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_2^\ast}} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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} : {t_1^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast} \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l : {t_1^\ast}~{t^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

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:

• 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}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l : {t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t^\ast} } \qquad \end{array}\]

\(\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.
  • 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}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/matching.html#match-resulttype}{\vdash} {t^\ast} \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l])^\ast \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t^\ast} \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}] \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~{l^\ast}~{l'} : {t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t_2^\ast} } \qquad \end{array}\]

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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})~\rightarrow~{t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}})\) 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 heap type \({\mathit{ht}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast} \qquad C \href{../valid/types.html#valid-heaptype}{\vdash} {\mathit{ht}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_null}}~l : {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) \rightarrow {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})~\rightarrow~{t^\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}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\mathit{ht}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\mathit{ht}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l : {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) \rightarrow {t^\ast} } \qquad \end{array}\]

\(\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}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) 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}}\).
• The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) is \({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast}~{\mathit{rt}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_1 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_2 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}}_1 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2 : {t^\ast}~{\mathit{rt}}_1 \rightarrow {t^\ast}~({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2) } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast}~{\mathit{rt}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_1 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_2 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}}_1 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2 : {t^\ast}~{\mathit{rt}}_1 \rightarrow {t^\ast}~{\mathit{rt}}_2 } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow}~{t_2^\ast})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\rightarrow~{t_2^\ast}\) if:

• The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
• The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow}~{t_2^\ast})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_ref}}~x : {t_1^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x) \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow}~{t_2^\ast})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}} \href{../valid/matching.html#match-reftype}{\leq} (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}) \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y : {t_1^\ast}~{\mathit{at}} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{return}} = ({t^\ast}) \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}} : {t_1^\ast}~{t^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{return}} = ({{t'}_2^\ast}) \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t_2^\ast} \href{../valid/matching.html#match-resulttype}{\leq} {{t'}_2^\ast} \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_3^\ast} \rightarrow {t_4^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call}}~x : {t_3^\ast}~{t_1^\ast} \rightarrow {t_4^\ast} } \qquad \end{array}\]

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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\rightarrow~{t_4^\ast}\) if:

• The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
• The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{return}} = ({{t'}_2^\ast}) \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t_2^\ast} \href{../valid/matching.html#match-resulttype}{\leq} {{t'}_2^\ast} \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_3^\ast} \rightarrow {t_4^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call\_ref}}~x : {t_3^\ast}~{t_1^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x) \rightarrow {t_4^\ast} } \qquad \end{array}\]

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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\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.

\[\begin{split}\begin{array}{@{}c@{}}\displaystyle \frac{ \begin{array}{@{}c@{}} C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}} \href{../valid/matching.html#match-reftype}{\leq} (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}) \\ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{return}} = ({{t'}_2^\ast}) \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t_2^\ast} \href{../valid/matching.html#match-resulttype}{\leq} {{t'}_2^\ast} \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_3^\ast} \rightarrow {t_4^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} \end{array} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return\_call\_indirect}}~x~y : {t_3^\ast}~{t_1^\ast}~{\mathit{at}} \rightarrow {t_4^\ast} } \qquad \end{array}\end{split}\]

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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow})\).
• The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} \epsilon \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw}}~x : {t_1^\ast}~{t^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

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}}~\href{../syntax/types.html#syntax-reftype}{\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{throw\_ref}} : {t_1^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}}) \rightarrow {t_2^\ast} } \qquad \end{array}\]

Note

The \(\mathsf{throw\_ref}\) instruction is stack-polymorphic.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try\_table}}~\href{../syntax/types.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶

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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} \qquad (C \href{../valid/instructions.html#valid-catch}{\vdash} {\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}} : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}})^\ast }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow})\).
• 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]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} \epsilon \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t^\ast} \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] }{ C \href{../valid/instructions.html#valid-catch}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~l : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}} } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow})\).
• 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]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} \epsilon \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}}) \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] }{ C \href{../valid/instructions.html#valid-catch}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_ref}}~x~l : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}} } \qquad \end{array}\]

\(\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]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-resulttype}{\vdash} \epsilon \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] }{ C \href{../valid/instructions.html#valid-catch}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~l : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}} } \qquad \end{array}\]

\(\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]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-resulttype}{\vdash} (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}}) \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] }{ C \href{../valid/instructions.html#valid-catch}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all\_ref}}~l : \href{../valid/instructions.html#valid-catch}{\mathsf{ok}} } \qquad \end{array}\]

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:

• The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) exists.
• The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) is of the form \((\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x] = \href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}get}}~x : \epsilon \rightarrow t } \qquad \end{array}\]

\(\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:

• The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) exists.
• The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) is of the form \(({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x] = {\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}set}}~x : t \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} \epsilon } \qquad \end{array}\]

\(\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:

• The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) exists.
• The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) is of the form \(({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x] = {\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}tee}}~x : t \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} t } \qquad \end{array}\]

\(\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:

• 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 \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x] = {\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x : \epsilon \rightarrow t } \qquad \end{array}\]

\(\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:

• 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 \((\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~t)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x] = \href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}set}}~x : t \rightarrow \epsilon } \qquad \end{array}\]

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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}get}}~x : {\mathit{at}} \rightarrow {\mathit{rt}} } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}set}}~x : {\mathit{at}}~{\mathit{rt}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}size}}~x : \epsilon \rightarrow {\mathit{at}} } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}grow}}~x : {\mathit{rt}}~{\mathit{at}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}fill}}~x : {\mathit{at}}~{\mathit{rt}}~{\mathit{at}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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~{\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~\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\).
• The address type \({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}\) is \({\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_1] = {\mathit{at}}_1~{\mathit{lim}}_1~{\mathit{rt}}_1 \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_2] = {\mathit{at}}_2~{\mathit{lim}}_2~{\mathit{rt}}_2 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}}_1 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}copy}}~x_1~x_2 : {\mathit{at}}_1~{\mathit{at}}_2~{\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2) \rightarrow \epsilon } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}}_1 \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y] = {\mathit{rt}}_2 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}}_1 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table{.}init}}~x~y : {\mathit{at}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[x] = {\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem{.}drop}}~x : \epsilon \rightarrow \epsilon } \qquad \end{array}\]

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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|{\mathit{nt}}|} / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : {\mathit{at}} \rightarrow {\mathit{nt}} } \qquad \end{array}\]

\(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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq M / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {{\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}}} : {\mathit{at}} \rightarrow {\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}} } \qquad \end{array}\]

\(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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|{\mathit{nt}}|} / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : {\mathit{at}}~{\mathit{nt}} \rightarrow \epsilon } \qquad \end{array}\]

\(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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq M / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {{\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}}} : {\mathit{at}}~{\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}|} / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}}} : {\mathit{at}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq M / 8 \cdot N }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\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}}} : {\mathit{at}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq N / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\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}}} : {\mathit{at}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq N / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\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}}} : {\mathit{at}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq N / 8 \qquad i < 128 / N }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\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 : {\mathit{at}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}|} / 8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}}} : {\mathit{at}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq N / 8 \qquad i < 128 / N }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\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 : {\mathit{at}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}size}}~x : \epsilon \rightarrow {\mathit{at}} } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}grow}}~x : {\mathit{at}} \rightarrow {\mathit{at}} } \qquad \end{array}\]

\(\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:

• 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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}fill}}~x : {\mathit{at}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\mathit{at}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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~{\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~\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}})\).
• The address type \({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}\) is \({\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_1] = {\mathit{at}}_1~{\mathit{lim}}_1~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_2] = {\mathit{at}}_2~{\mathit{lim}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}copy}}~x_1~x_2 : {\mathit{at}}_1~{\mathit{at}}_2~{\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2) \rightarrow \epsilon } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y] = \href{../valid/modules.html#valid-data}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}init}}~x~y : {\mathit{at}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[x] = \href{../valid/modules.html#valid-data}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data{.}drop}}~x : \epsilon \rightarrow \epsilon } \qquad \end{array}\]

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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})\) if:

• The heap type \({\mathit{ht}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-heaptype}{\vdash} {\mathit{ht}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}} : \epsilon \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) } \qquad \end{array}\]

\(\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:

• The function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) exists.
• The function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is of the form \({\mathit{dt}}\).
• \(x\) is contained in \(C{.}\href{../valid/conventions.html#context}{\mathsf{refs}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x] = {\mathit{dt}} \qquad x \in C{.}\href{../valid/conventions.html#context}{\mathsf{refs}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x : \epsilon \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{dt}}) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) if:

• The heap type \({\mathit{ht}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-heaptype}{\vdash} {\mathit{ht}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}is\_null}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}})\) if:

• The heap type \({\mathit{ht}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-heaptype}{\vdash} {\mathit{ht}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}as\_non\_null}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}})~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}eq}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}})~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}) \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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}'}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}'} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}} \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}'} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}test}}~{\mathit{rt}} : {\mathit{rt}'} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

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}'}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}'} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}} \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}'} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}cast}}~{\mathit{rt}} : {\mathit{rt}'} \rightarrow {\mathit{rt}} } \qquad \end{array}\]

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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast})\).
• The value type sequence \({t^\ast}\) is \({{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x : {{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})^\ast} \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x) } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\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 \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast} \qquad ({{\href{../exec/runtime.html#aux-default}{\mathrm{default}}}}_{{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})} \neq \epsilon)^\ast }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x : \epsilon \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\rightarrow~t\) if:

• The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
• The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{ft}}^\ast})\).
• The length of \({{\mathit{ft}}^\ast}\) is greater than \(i\).
• The field type \({{\mathit{ft}}^\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 \({\mathit{zt}}\) is a packed type.
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{ft}}^\ast} \qquad {{\mathit{ft}}^\ast}{}[i] = {\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}} \qquad {{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?} = \epsilon \Leftrightarrow {\mathit{zt}} = {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}get}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~x~i : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x) \rightarrow {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~t~\rightarrow~\epsilon\) if:

• The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
• The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{ft}}^\ast})\).
• The length of \({{\mathit{ft}}^\ast}\) is greater than \(i\).
• The field type \({{\mathit{ft}}^\ast}{}[i]\) is of the form \((\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}})\).
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{ft}}^\ast} \qquad {{\mathit{ft}}^\ast}{}[i] = \href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}set}}~x~i : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) \rightarrow \epsilon } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x : {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x) } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
• A default value for \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}) \qquad {{\href{../exec/runtime.html#aux-default}{\mathrm{default}}}}_{{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})} \neq \epsilon }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x) } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x~n : {{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})^{n}} \rightarrow (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x) } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{rt}}) \qquad C \href{../valid/matching.html#match-reftype}{\vdash} C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y] \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_elem}}~x~y : \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) } \qquad \end{array}\]

\(\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}) \qquad {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) = {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} \lor {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) = {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y] = \href{../valid/modules.html#valid-data}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_data}}~x~y : \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) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\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 \({\mathit{zt}}\) is a packed type.
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}) \qquad {{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?} = \epsilon \Leftrightarrow {\mathit{zt}} = {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}get}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~x : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}))\).
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}set}}~x : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) \rightarrow \epsilon } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}len}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}) \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}))\).
• The value type \(t\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}fill}}~x : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x_1)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}_1))\).
• The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) exists.
• The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) is \((\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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}_1) \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}_2) \qquad C \href{../valid/matching.html#match-storagetype}{\vdash} {\mathit{zt}}_2 \href{../valid/matching.html#match-storagetype}{\leq} {\mathit{zt}}_1 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}copy}}~x_1~x_2 : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x_1)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x_2)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \epsilon } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}) \qquad C \href{../valid/matching.html#match-storagetype}{\vdash} C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y] \href{../valid/matching.html#match-storagetype}{\leq} {\mathit{zt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}init\_elem}}~x~y : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\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 } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\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 \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is \((\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}) \qquad {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) = {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} \lor {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}}) = {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} \qquad C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y] = \href{../valid/modules.html#valid-data}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}init\_data}}~x~y : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\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 } \qquad \end{array}\]

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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}} : \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}}) } \qquad \end{array}\]

\(\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}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}})~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{i{\scriptstyle31}{.}get}}}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}} : (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}}) \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

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^?}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ {{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}_1^?} = {{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}_2^?} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}} : (\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}}) } \qquad \end{array}\]

\(\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^?}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ {{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}_1^?} = {{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}_2^?} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}} : (\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}}) } \qquad \end{array}\]

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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{nt}} : \epsilon \rightarrow {\mathit{nt}} } \qquad \end{array}\]

\(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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}}}_{\mathit{nt}} : {\mathit{nt}} \rightarrow {\mathit{nt}} } \qquad \end{array}\]

\(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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}}_{\mathit{nt}} : {\mathit{nt}}~{\mathit{nt}} \rightarrow {\mathit{nt}} } \qquad \end{array}\]

\(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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}}}_{\mathit{nt}} : {\mathit{nt}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}}}_{\mathit{nt}} : {\mathit{nt}}~{\mathit{nt}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(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\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}}_1 {.} {{\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}}}{\mathsf{\_}}{{\mathit{nt}}_2} : {\mathit{nt}}_2 \rightarrow {\mathit{nt}}_1 } \qquad \end{array}\]

\(t_1\mathsf{.}\href{../syntax/instructions.html#syntax-wideop}{\mathit{wideop}}\)¶

The instruction \(({\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-wideop}{\mathit{wideop}}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~{\mathit{nt}}~{\mathit{nt}}~{\mathit{nt}}~\rightarrow~{\mathit{nt}}~{\mathit{nt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-wideop}{\mathit{wideop}}}_{\mathit{nt}} : {\mathit{nt}}~{\mathit{nt}}~{\mathit{nt}}~{\mathit{nt}} \rightarrow {\mathit{nt}}~{\mathit{nt}} } \qquad \end{array}\]

\(t_1\mathsf{.}\href{../syntax/instructions.html#syntax-extwideop}{\mathit{extwideop}}\)¶

The instruction \(({\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-extwideop}{\mathit{extwideop}}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~{\mathit{nt}}~\rightarrow~{\mathit{nt}}~{\mathit{nt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\href{../syntax/instructions.html#syntax-extwideop}{\mathit{extwideop}}}_{\mathit{nt}} : {\mathit{nt}}~{\mathit{nt}} \rightarrow {\mathit{nt}}~{\mathit{nt}} } \qquad \end{array}\]

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:

\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}} {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({{\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}}{\href{../syntax/instructions.html#syntax-shape}{\mathsf{x}}}{N}) & = & {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}}) \\ \end{array}\end{split}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : \epsilon \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} {.} {\href{../syntax/instructions.html#syntax-vvtestop}{\mathit{vvtestop}}} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}}} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vternop}{\mathit{vternop}}} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vtestop}}} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}}} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vshiftop}{\mathit{vshiftop}}} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}} {.} {\href{../syntax/instructions.html#syntax-vswizzlop}{\mathit{vswizzlop}}} : \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}} } \qquad \end{array}\]

\(\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}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (i < 2 \cdot {\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}}))^\ast }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~{i^\ast} : \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}} } \qquad \end{array}\]

\(\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 \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:

• The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}} : {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}}) \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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}}~{\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}~\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}})\).
• The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) is \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ i < {\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{replace\_lane}}~i : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}}) \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vextunop}{\mathit{vextunop}}}}{\mathsf{\_}}{{\mathit{sh}}_2} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vextbinop}{\mathit{vextbinop}}}}{\mathsf{\_}}{{\mathit{sh}}_2} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vextternop}{\mathit{vextternop}}}}{\mathsf{\_}}{{\mathit{sh}}_2} : \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}} } \qquad \end{array}\]

\(\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {{\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}}}} : \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}} } \qquad \end{array}\]

\(\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{\_}}{{\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}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{sh}}_1 {.} {{\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}}}{\mathsf{\_}}{{\mathit{sh}}_2} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \qquad \end{array}\]

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}\).
  • For all \(x_1\) in \({x_1^\ast}\):

     * The [local](conventions.html#syntax-localtype) \\(C{.}\\href{../valid/conventions.html#context}{\\mathsf{locals}}{}\[x\_1\]\\) exists.

   * The [local](conventions.html#syntax-localtype) \\(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\) with the local types of \({x_1^\ast}\) updated to \({(\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 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 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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instrs}{\vdash} \epsilon : \epsilon \rightarrow \epsilon } \qquad \end{array}\]

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1 : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_1^\ast}} {t_2^\ast} \qquad (C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x_1] = {\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t)^\ast \qquad C{}[{.}\href{../syntax/modules.html#syntax-local}{\mathsf{local}}{}[{x_1^\ast}] = {(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t)^\ast}] \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast} : {t_2^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_2^\ast}} {t_3^\ast} }{ C \href{../valid/instructions.html#valid-instrs}{\vdash} {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_1^\ast}~{x_2^\ast}} {t_3^\ast} } \qquad \end{array}\]

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {\mathit{it}} \qquad C \href{../valid/matching.html#match-instrtype}{\vdash} {\mathit{it}} \href{../valid/matching.html#match-instrtype}{\leq} {\mathit{it}'} \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {\mathit{it}'} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {\mathit{it}'} } \qquad \frac{ C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} \qquad C \href{../valid/types.html#valid-resulttype}{\vdash} {t^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : ({t^\ast}~{t_1^\ast}) \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} ({t^\ast}~{t_2^\ast}) } \qquad \end{array}\]

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

\[(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~1)~(\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}})\]

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}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : \epsilon \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{\epsilon} {t^\ast} }{ C \href{../valid/instructions.html#valid-expr}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t^\ast} } \qquad \end{array}\]

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}}\)].

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/instructions.html#valid-const}{\vdash} {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}~\href{../valid/instructions.html#valid-const}{\mathsf{const}})^\ast }{ C \href{../valid/instructions.html#valid-const}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \end{array}\]

\[\begin{split}\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} ({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{nt}})~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} ({\mathit{vt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{vt}})~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ {\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}} \in \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}} \qquad {\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}} \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}} }{ C \href{../valid/instructions.html#valid-const}{\vdash} ({\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{../valid/instructions.html#valid-const}{\mathsf{const}} } \\[3ex]\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}})~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}})~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \\[3ex]\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \\[3ex]\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x~n)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \\[3ex]\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}})~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}})~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \\[3ex]\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x] = t }{ C \href{../valid/instructions.html#valid-const}{\vdash} (\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x)~\href{../valid/instructions.html#valid-const}{\mathsf{const}} } \qquad \end{array}\end{split}\]

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.