Instructions

Instructions are classified by instruction types that describe how they manipulate the operand stack and initialize locals: A type \({t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast}\) describes the required input stack with argument values of types \({t_1^\ast}\) that an instruction pops off and the provided output stack with result values of types \({t_2^\ast}\) that it pushes back. Moreover, it enumerates the indices \({x^\ast}\) of locals that have been set by the instruction. In most cases, this is empty.

Note

For example, the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) has type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\), consuming two \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) values and producing one. The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}set}}~x)\) has type \(t \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} \epsilon\), provided \(t\) is the type declared for the local \(x\).

Typing extends to instruction sequences \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\). Such a sequence has an instruction type \({t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast}\) if the accumulative effect of executing the instructions is consuming values of types \({t_1^\ast}\) off the operand stack, pushing new values of types \({t_2^\ast}\), and setting all locals \({x^\ast}\).

For some instructions, the typing rules do not fully constrain the type, and therefore allow for multiple types. Such instructions are called polymorphic. Two degrees of polymorphism can be distinguished:

  • value-polymorphic: the value type \(t\) of one or several individual operands is unconstrained. That is the case for all parametric instructions like \(\mathsf{drop}\) and \(\mathsf{select}\).

  • stack-polymorphic: the entire (or most of the) instruction type \({t_1^\ast} \rightarrow {t_2^\ast}\) of the instruction is unconstrained. That is the case for all control instructions that perform an unconditional control transfer, such as \(\mathsf{unreachable}\), \(\mathsf{br}\), or \(\mathsf{return}\).

In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program.

Note

For example, the \(\mathsf{select}\) instruction is valid with type \(t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t\), for any possible number type \(t\). Consequently, both instruction sequences

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

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

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

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

Reference Instructions

\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~\mathit{ht}\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}})\) is valid with the instruction type \(\epsilon~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}})\) if:

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

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

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

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

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

\[\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 the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast})\).

  • Let \({t^\ast}\) be the value type sequence \({{\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})^\ast}\).

\[\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 the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})^\ast})\).

  • For all \({\mathit{zt}}\) in \({{\mathit{zt}}^\ast}\):

    • A default value for the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.

\[\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}}~\mathsf{null}~x)~\rightarrow~t\) if:

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}^\ast})\).

  • The length of \({{\mathit{yt}}^\ast}\) is greater than \(i\).

  • The field type \({{\mathit{yt}}^\ast}{}[i]\) is of the form \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}})\).

  • The signedness \({{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}\) is absent if and only if the storage type \({\mathit{zt}}\) is of the form \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\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{yt}}^\ast} \qquad {{\mathit{yt}}^\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}}~\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}}~\mathsf{null}~x)~t~\rightarrow~\epsilon\) if:

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}^\ast})\).

  • The length of \({{\mathit{yt}}^\ast}\) is greater than \(i\).

  • The field type \({{\mathit{yt}}^\ast}{}[i]\) is of the form \((\mathsf{mut}~{\mathit{zt}})\).

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

\[\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{yt}}^\ast} \qquad {{\mathit{yt}}^\ast}{}[i] = \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}}~\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 the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

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

  • A default value for the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.

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

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

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

  • The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.

  • The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) matches the reference type \({\mathit{rt}}\).

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

  • The value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).

  • The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) exists.

  • The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is of the form \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).

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

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}))\).

  • The signedness \({{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}\) is absent if and only if the storage type \({\mathit{zt}}\) is of the form \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

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

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

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

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).

  • Let \(t\) be the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\).

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

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}_1))\).

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}_2))\).

  • The storage type \({\mathit{zt}}_2\) matches the storage type \({\mathit{zt}}_1\).

\[\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}}~(\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}}~\mathsf{null}~x_1)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~x_2)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \epsilon } \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}}~\mathsf{null}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~\epsilon\) if:

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).

  • The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.

  • The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) matches the storage type \({\mathit{zt}}\).

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

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

  • The expansion of the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~(\mathsf{mut}~{\mathit{zt}}))\).

  • The value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).

  • The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) exists.

  • The data segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is of the form \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).

\[\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}}~(\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}}~\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}}~\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}}~\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}\]

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

  • Let \(t\) be the number type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).

\[\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{extract\_lane}}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)

The instruction \(({{\mathit{sh}}{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extract\_lane}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~i)\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~t\) if:

  • The lane index \(i\) is less than \({\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}})\).

  • Let \(t\) be the number type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).

\[\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{extract\_lane}}}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}^?}}~i : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow {\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}}) } \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}}~t~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) if:

  • The lane index \(i\) is less than \({\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}}({\mathit{sh}})\).

  • Let \(t\) be the number type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{sh}})\).

\[\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{\_}}{{{\href{../syntax/instructions.html#syntax-zero}{\mathit{zero}}}^?}}{\mathsf{\_}}{{\mathit{sh}}_2}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-half}{\mathit{half}}}^?}})\) is valid with the instruction type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\rightarrow~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\).

\[\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{\_}}{{{\href{../syntax/instructions.html#syntax-zero}{\mathit{zero}}}^?}}{\mathsf{\_}}{{\mathit{sh}}_2}{\mathsf{\_}}{{{\href{../syntax/instructions.html#syntax-half}{\mathit{half}}}^?}} : \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} } \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 \((\mathsf{mut}~t)\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x] = \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~t~\rightarrow~\epsilon\) if:

  • The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_1]\) exists.

  • The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_1]\) is of the form \(({\mathit{at}}_1~{\mathit{lim}}_1~{\mathit{rt}}_1)\).

  • The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_2]\) exists.

  • The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_2]\) is of the form \(({\mathit{at}}_2~{\mathit{lim}}_2~{\mathit{rt}}_2)\).

  • The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}_1\).

  • Let \(t\) be the address type \({\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2)\).

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

  • The element segment \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[x]\) is of the form \({\mathit{rt}}\).

\[\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~t~\rightarrow~\epsilon\) if:

  • The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_1]\) exists.

  • The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_1]\) is of the form \(({\mathit{at}}_1~{\mathit{lim}}_1~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

  • The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_2]\) exists.

  • The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_2]\) is of the form \(({\mathit{at}}_2~{\mathit{lim}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

  • Let \(t\) be the address type \({\href{../syntax/types.html#aux-addrtype-min}{\mathrm{min}}}({\mathit{at}}_1, {\mathit{at}}_2)\).

\[\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}\]

Control Instructions

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

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \begin{array}[t]{@{}l@{}} \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \}\end{array} \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 \(\{ \begin{array}[t]{@{}l@{}} \href{../valid/conventions.html#context}{\mathsf{labels}}~({t^\ast}) \}\end{array} \oplus C\) inserts the new label type at index \(0\), shifting all others. The same applies to all other block instructions.

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

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_1^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \begin{array}[t]{@{}l@{}} \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_1^\ast}) \}\end{array} \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/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast})\) is valid with the instruction type \({t_1^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}}\,{t_2^\ast}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_2^\ast}}\,{t_2^\ast}\).

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

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try\_table}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}^\ast}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).

  • For all \({\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}\) in \({{\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}^\ast}\):

    • The catch clause \({\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \begin{array}[t]{@{}l@{}} \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \}\end{array} \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 the tag \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~\epsilon)\).

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).

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

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The result type \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}})\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).

\[\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-functype}{\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}\]

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

  • For all \(l\) in \({l^\ast}\):

    • The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}]\) exists.

  • The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}]\).

  • The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.

\[\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} \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}}~\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}}~\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}}~\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}}~{\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}}~{\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}}~\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}~{t'}\) if:

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

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

\[\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-functype}{\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}}~\mathsf{null}~x)~\rightarrow~{t_2^\ast}\) if:

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

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

\[\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-functype}{\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}}~\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}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}})\).

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) exists.

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

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

  • The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({{t'}_2^\ast}\).

  • The result type \({t_2^\ast}\) matches the result type \({{t'}_2^\ast}\).

  • The instruction type \({t_3^\ast}~\rightarrow~{t_4^\ast}\) is valid.

\[\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-functype}{\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}}~\mathsf{null}~x)~\rightarrow~{t_4^\ast}\) if:

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

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

  • The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({{t'}_2^\ast}\).

  • The result type \({t_2^\ast}\) matches the result type \({{t'}_2^\ast}\).

  • The instruction type \({t_3^\ast}~\rightarrow~{t_4^\ast}\) is valid.

\[\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-functype}{\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}}~\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}}~\mathsf{null}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}})\).

  • The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) exists.

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

  • The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is of the form \({{t'}_2^\ast}\).

  • The result type \({t_2^\ast}\) matches the result type \({{t'}_2^\ast}\).

  • The instruction type \({t_3^\ast}~\rightarrow~{t_4^\ast}\) is valid.

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

  • The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.

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

\[\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}}~\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.

Instruction Sequences

Typing of instruction sequences is defined recursively.

Empty Instruction Sequence: \(\epsilon\)

The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is valid with the instruction type \({\mathit{it}''}\) if:

  • Either:

    • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is empty.

    • The instruction type \({\mathit{it}''}\) is of the form \(\epsilon~\rightarrow~\epsilon\).

  • Or:

    • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is of the form \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\).

    • The instruction type \({\mathit{it}''}\) is of the form \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}~{x_2^\ast}}\,{t_3^\ast}\).

    • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}}\,{t_2^\ast}\).

    • The length of \({{\href{../valid/conventions.html#syntax-init}{\mathit{init}}}^\ast}\) is equal to the length of \({t^\ast}\).

    • The length of \({{\href{../valid/conventions.html#syntax-init}{\mathit{init}}}^\ast}\) is equal to the length of \({x_1^\ast}\).

    • For all \(x_1\) in \({x_1^\ast}\):

      • The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x_1]\) exists.

    • For all \({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}\) in \({{\href{../valid/conventions.html#syntax-init}{\mathit{init}}}^\ast}\), and corresponding \(t\) in \({t^\ast}\), and corresponding \(x_1\) in \({x_1^\ast}\):

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

    • Under the context \(C{}[{.}\href{../syntax/modules.html#syntax-local}{\mathsf{local}}{}[{x_1^\ast}] = {(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t)^\ast}]\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\) is valid with the instruction type \({t_2^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_2^\ast}}\,{t_3^\ast}\).

  • Or:

    • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is of the form \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\).

    • The instruction type \({\mathit{it}''}\) is of the form \({\mathit{it}'}\).

    • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({\mathit{it}}\).

    • The instruction type \({\mathit{it}}\) matches the instruction type \({\mathit{it}'}\).

    • The instruction type \({\mathit{it}'}\) is valid.

  • Or:

    • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast}\) is of the form \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\).

    • The instruction type \({\mathit{it}''}\) is of the form \({t^\ast}~{t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t^\ast}~{t_2^\ast}\).

    • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).

    • The result type \({t^\ast}\) is valid.

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