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 \(\mathsf{binop}~\mathsf{i{\scriptstyle 32}}~\mathsf{add}\) has type \(\mathsf{i{\scriptstyle 32}}~\mathsf{i{\scriptstyle 32}} \rightarrow \mathsf{i{\scriptstyle 32}}\), consuming two \(\mathsf{i{\scriptstyle 32}}\) values and producing one. The instruction \(\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

\[(\mathsf{const}~\mathsf{i{\scriptstyle 32}}~1)~(\mathsf{const}~\mathsf{i{\scriptstyle 32}}~2)~(\mathsf{const}~\mathsf{i{\scriptstyle 32}}~3)~\mathsf{select}\]

and

\[(\mathsf{const}~\mathsf{f{\scriptstyle 64}}~1 {.} 0)~(\mathsf{const}~\mathsf{f{\scriptstyle 64}}~2 {.} 0)~(\mathsf{const}~\mathsf{f{\scriptstyle 64}}~3 {.} 0)~\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,

\[\mathsf{unreachable}~\mathsf{binop}~\mathsf{i{\scriptstyle 32}}~\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,

\[\mathsf{unreachable}~(\mathsf{const}~\mathsf{i{\scriptstyle 64}}~0)~\mathsf{binop}~\mathsf{i{\scriptstyle 32}}~\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\).

Todo

below is the official specification

• The instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\)

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

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

Todo

below is the official specification

• The instruction is valid with any valid type of the form \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

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

Note

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

\(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\)

The instruction \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\) is valid with the instruction type \(t~\rightarrow~\epsilon\) if:

• The value type \(t\) is valid.

Todo

below is the official specification

• The instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\), for any valid value type \(t\).

\[\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}}~{t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?})\) 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 \({t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}\) is equal to \(t\).

• Or:

  • The value type sequence \({t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}\) is absent.

  • The value type \(t\) matches the value type \({t'}\).

  • The value type \({t'}\) is equal to \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({t'}\) is equal to \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).

Todo

below is the official specification

(*) - [contained in]

• If \(t^\ast\) is present, then:

  • The result type \([t^\ast]\) must be valid.

  • The length of \(t^\ast\) must be \(1\).

  • Then the instruction is valid with type \([t^\ast~t^\ast~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast]\).

• Else:

  • The instruction is valid with type \([t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\), for any valid value type \(t\) that matches some number type or vector type.

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

Todo

below is the official specification

• The instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

\[\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}} {.} {\mathit{unop}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~\rightarrow~{\mathit{nt}}\).

Todo

below is the official specification

• The instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\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}} {.} {\mathit{binop}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~{\mathit{nt}}~\rightarrow~{\mathit{nt}}\).

Todo

below is the official specification

• The instruction is valid with type \([t~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}} {.} {\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}} {.} {\mathit{testop}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).

Todo

below is the official specification

• The instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}} {.} {\mathit{relop}}_{\mathit{nt}})\) is valid with the instruction type \({\mathit{nt}}~{\mathit{nt}}~\rightarrow~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\).

Todo

below is the official specification

• The instruction is valid with type \([t~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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 {.} {{\mathit{cvtop}}}{\mathsf{\_}}{{\mathit{nt}}_2})\) is valid with the instruction type \({\mathit{nt}}_2~\rightarrow~{\mathit{nt}}_1\).

Todo

below is the official specification

• The instruction is valid with type \([t_2] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_1]\).

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

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

Todo

below is the official specification

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

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/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}}~\epsilon~{\mathit{dt}})\) if:

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

• The defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is equal to \({\mathit{dt}}\).

• The index \(C{.}\href{../valid/conventions.html#context}{\mathsf{refs}}{}[0]\) exists.

• \(x\) is contained in \(C{.}\href{../valid/conventions.html#context}{\mathsf{refs}}\).

Todo

below is the official specification

• The function \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be defined in the context.

• Let \(\mathit{dt}\) be the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\).

• The function index \(x\) must be contained in \(C.\href{../valid/conventions.html#context}{\mathsf{refs}}\).

• The instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{dt})]\).

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

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

Todo

below is the official specification

• The instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\), for any valid heap type \(\mathit{ht}\).

\[\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}}~\epsilon~{\mathit{ht}})\) if:

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

Todo

below is the official specification

• The instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{ht})]\), for any valid heap type \(\mathit{ht}\).

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

Todo

below is the official specification

• The instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}) (\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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:

• The reference type \({\mathit{rt}}\) is valid.

• The reference type \({\mathit{rt}'}\) is valid.

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

Todo

below is the official specification

• The reference type \(\mathit{rt}\) must be valid.

• Then the instruction is valid with type \([\mathit{rt}'] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\) for any valid reference type \(\mathit{rt}'\) for which \(\mathit{rt}\) matches \(\mathit{rt}'\).

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

Note

The liberty to pick a supertype \({\mathit{rt}'}\) allows typing the instruction with the least precise super type of \({\mathit{rt}}\) as input, that is, the top type in the corresponding heap subtyping hierarchy.

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

The instruction \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}cast}}~{\mathit{rt}})\) is valid with the instruction type \({\mathit{rt}'}~\rightarrow~{\mathit{rt}}\) if:

• The reference type \({\mathit{rt}}\) is valid.

• The reference type \({\mathit{rt}'}\) is valid.

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

Todo

below is the official specification

• The reference type \(\mathit{rt}\) must be valid.

• Then the instruction is valid with type \([\mathit{rt}'] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\mathit{rt}]\) for any valid reference type \(\mathit{rt}'\) for which \(\mathit{rt}\) matches \(\mathit{rt}'\).

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

Note

The liberty to pick a supertype \({\mathit{rt}'}\) allows typing the instruction with the least precise super type of \({\mathit{rt}}\) as input, that is, the top type in the corresponding heap subtyping hierarchy.

Aggregate Reference Instructions

\(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x)\) is valid with the instruction type \({t^\ast}~\rightarrow~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\epsilon~x)\) if:

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

• The expansion of the defined 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}\).

Todo

below is the official specification

(*) - unpack(zt)* vs let t* be concatenation of ti

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a structure type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\).

• For each field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) in \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\):

  • Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_i\).

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

• Let \(t^\ast\) be the concatenation of all \(t_i\).

• Then the instruction is valid with type \([t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

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

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

• The expansion of the defined 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 value type the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.

Todo

below is the official specification

(*) Different notation for “defaultable”

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a structure type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\).

• For each field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) in \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\):

  • Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_i\).

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

  • The type \(t_i\) must be defaultable.

• Let \(t^\ast\) be the concatenation of all \(t_i\).

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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#default-val}{\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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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})\).

• \({|{{\mathit{yt}}^\ast}|}\) is greater than \(i\).

• The field type \({{\mathit{yt}}^\ast}{}[i]\) is equal to \(({\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 equal to \({\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}})\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a structure type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast[y]\).

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

• The extension \(\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\) must be present if and only if \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) is a packed type.

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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})\).

• \({|{{\mathit{yt}}^\ast}|}\) is greater than \(i\).

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

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

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a structure type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast[y]\).

• The prefix \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

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

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

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

• The expansion of the defined 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}})\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\).

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

• Then the instruction is valid with type \([t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

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

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

• The expansion of the defined 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 value type the value type \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is defined.

Todo

below is the official specification

(*) Different notation for “defaultable”

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\).

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

• The type \(t\) must be defaultable.

• Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

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

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

• The expansion of the defined 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}})\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\).

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

• Then the instruction is valid with type \([t^n] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

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

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

• The expansion of the defined 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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.

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

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\).

• The storage type \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) must be a reference type \(\mathit{rt}\).

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

• Let \(\mathit{rt}'\) be the reference type \(C.\href{../valid/conventions.html#context}{\mathsf{elems}}[y]\).

• The reference type \(\mathit{rt}'\) must match \(\mathit{rt}\).

• Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

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

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

• The expansion of the defined 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 equal to \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is equal to \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).

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

• The data type \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is equal to \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).

Todo

below is the official specification

(*) contained in

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\) be \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\).

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

• The type \(t\) must be a numeric type or a vector type.

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

• Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~x)]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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 equal to \({\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}})\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

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

• The extension \(\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\) must be present if and only if \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) is a packed type.

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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}})\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• The prefix \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

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

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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}}\).

Todo

below is the official specification

• The the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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}})\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• The prefix \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

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

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1]\) exists.

• The expansion of the defined 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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_2]\) exists.

• The expansion of the defined 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\).

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1\).

• The prefix \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2\).

• The storage type \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) must match \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\).

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~y)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x_1] \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] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) exists.

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

Todo

below is the official specification

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• The prefix \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

• The storage type \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) must be a reference type \(\mathit{rt}\).

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

• Let \(\mathit{rt}'\) be the reference type \(C.\href{../valid/conventions.html#context}{\mathsf{elems}}[y]\).

• The reference type \(\mathit{rt}'\) must match \(\mathit{rt}\).

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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 equal to \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({\href{../syntax/types.html#aux-unpack}{\mathrm{unpack}}}({\mathit{zt}})\) is equal to \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).

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

• The data type \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is equal to \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).

Todo

below is the official specification

(*) contained in

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

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be an array type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• Let the field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\) be \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\).

• The prefix \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

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

• The value type \(t\) must be a numeric type or a vector type.

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

• Then the instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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}}~\epsilon~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}})\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 equal to \({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}\).

Todo

below is the official specification

• The instruction is valid with 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}})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}})]\) for any \(\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}_1^?\) that equals \(\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 equal to \({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}\).

Todo

below is the official specification

• The instruction is valid with 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}})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}})]\) for any \(\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}_1^?\) that equals \(\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}}\).

Todo

below is the official specification

• The instruction is valid with 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}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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 is valid with 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}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\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}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] }\]

\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vtestop}}\)

The instruction \(({\mathit{sh}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}} {.} {\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}})\).

Todo

below is the official specification

• For all \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}_i\), in \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}^{16}\), \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}_i\) must be smaller than \(32\).

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

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

Todo

below is the official specification

• Let \(t\) be \(\href{../valid/instructions.html#aux-unpackshape}{\mathrm{unpack}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

• The instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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-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}})\).

Todo

below is the official specification

• The lane index \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\) must be smaller than \(\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

• Let \(t\) be \(\href{../valid/instructions.html#aux-unpackshape}{\mathrm{unpack}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

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

Todo

below is the official specification

• The lane index \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\) must be smaller than \(\href{../syntax/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

• Let \(t\) be \(\href{../valid/instructions.html#aux-unpackshape}{\mathrm{unpack}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

\[\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-instr-vec}{\mathsf{extadd\_pairwise}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)

The instruction \(({\mathit{sh}}_1 {.} {{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 {.} {{\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-instr-vec}{\mathsf{extmul}}\mathsf{\_}\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)

The instruction \(({\mathit{sh}}_1 {.} {{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 {.} {{\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-instr-vec}{\mathsf{relaxed\_dot\_add}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_3\)

• The instruction is valid with 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}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 {.} {{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 {.} {{\mathit{vcvtop}}}{\mathsf{\_}}{{{\mathit{zero}}^?}}{\mathsf{\_}}{{\mathit{sh}}_2}{\mathsf{\_}}{{{\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}}\).

Todo

below is the official specification

• The instruction is valid with type \([\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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 {.} {{\mathit{vcvtop}}}{\mathsf{\_}}{{{\mathit{zero}}^?}}{\mathsf{\_}}{{\mathit{sh}}_2}{\mathsf{\_}}{{{\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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) exists.

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

Todo

below is the official specification

• The local \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) must be defined in the context.

• Let \(\href{../valid/conventions.html#syntax-init}{\mathit{init}}~t\) be the local type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\).

• The initialization status \(\href{../valid/conventions.html#syntax-init}{\mathit{init}}\) must be \(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}\).

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) exists.

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

Todo

below is the official specification

• The local \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) must be defined in the context.

• Let \(\href{../valid/conventions.html#syntax-init}{\mathit{init}}~t\) be the local type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\).

• Then the instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} []\).

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

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

Todo

below is the official specification

• The local \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) must be defined in the context.

• Let \(\href{../valid/conventions.html#syntax-init}{\mathit{init}}~t\) be the local type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\).

• Then the instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} [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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) exists.

• The global type \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) is equal to \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t)\).

Todo

below is the official specification

• The global \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\) must be defined in the context.

• Let \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) be the global type \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\).

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) exists.

• The global type \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) is equal to \((\mathsf{mut}~t)\).

Todo

below is the official specification

• The global \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\) must be defined in the context.

• Let \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) be the global type \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\).

• The mutability \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) must be \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\).

• Then the instruction is valid with type \([t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

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

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• Then the instruction is valid with type \([\mathit{at}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).

Todo

below is the official specification

(*) - [Erase last statement]

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\mathit{at}]\).

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

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

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• Then the instruction is valid with type \([t~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\mathit{at}]\).

\[\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 {\mathit{at}} } \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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• Then the instruction is valid with type \([\mathit{at}~t~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_1]\) exists.

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

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

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x_2]\) is equal to \(({\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)\).

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}_1~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~t_1\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[y]\) must be defined in the context.

• Let \(\mathit{at}_2~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~t_2\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[y]\).

• The reference type \(t_2\) must match \(t_1\).

• Let \(\mathit{at}\) be the minimum of \(\mathit{at}_1\) and \(\mathit{at}_2\)

• Then the instruction is valid with type \([\mathit{at}_1~\mathit{at}_2~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}}_1)\).

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

• The element type \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[y]\) is equal to \({\mathit{rt}}_2\).

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

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t_1\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• The element segment \(C.\href{../valid/conventions.html#context}{\mathsf{elems}}[y]\) must be defined in the context.

• Let \(t_2\) be the reference type \(C.\href{../valid/conventions.html#context}{\mathsf{elems}}[y]\).

• The reference type \(t_2\) must match \(t_1\).

• Then the instruction is valid with type \([\mathit{at}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The element type \(C{.}\href{../valid/conventions.html#context}{\mathsf{elems}}{}[x]\) is equal to \({\mathit{rt}}\).

Todo

below is the official specification

• The element segment \(C.\href{../valid/conventions.html#context}{\mathsf{elems}}[x]\) must be defined in the context.

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\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}}}{\epsilon}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~\rightarrow~{\mathit{nt}}\) if:

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

\[\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}}}{\epsilon}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}})\) is valid with the instruction type \({\mathit{at}}~{\mathit{nt}}~\rightarrow~\epsilon\) if:

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

• Then the instruction is valid with type \([\mathit{at}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

• Then the instruction is valid with type \([\mathit{at}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\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}}}{\epsilon}~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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

• Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8 \cdot M\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

• The lane index \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\) must be smaller than \(128/N\).

• Then the instruction is valid with type \([\mathit{at}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

• Then the instruction is valid with type \([\mathit{at}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\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\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The offset \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\) must be less than \(2^{|\mathit{at}|}\).

• The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

• The lane index \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\) must be smaller than \(128/N\).

• Then the instruction is valid with type \([\mathit{at}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\mathit{at}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• Then the instruction is valid with type \([\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\mathit{at}]\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• Then the instruction is valid with type \([\mathit{at}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

\[\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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_1]\) exists.

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

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x_2]\) is equal to \(({\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)\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[y]\) must be defined in the context.

• Let \(\mathit{at}_x~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_x\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• Let \(\mathit{at}_y~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_y\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[y]\).

• Let \(\mathit{at}\) be the minimum of \(\mathit{at}_x\) and \(\mathit{at}_y\)

• Then the instruction is valid with type \([\mathit{at}_x~\mathit{at}_y~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The memory type \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is equal to \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

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

• The data type \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[y]\) is equal to \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).

Todo

below is the official specification

• The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the memory type \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\).

• The data segment \(C.\href{../valid/conventions.html#context}{\mathsf{datas}}[y]\) must be defined in the context.

• Then the instruction is valid with type \([\mathit{at}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

• The data type \(C{.}\href{../valid/conventions.html#context}{\mathsf{datas}}{}[x]\) is equal to \(\href{../valid/modules.html#valid-data}{\mathsf{ok}}\).

Todo

below is the official specification

• The data segment \(C.\href{../valid/conventions.html#context}{\mathsf{datas}}[x]\) must be defined in the context.

• Then the instruction is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

Todo

below is the official specification

(*) - [changed notation for context]

• The block type must be valid as some instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

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

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

• Then the compound instruction is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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 with 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}\).

Todo

below is the official specification

(*) - changed notation for context

• The block type must be valid as some instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x^\ast} [t_2^\ast]\).

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

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

• Then the compound instruction is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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 with 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}\).

Todo

below is the official specification

(*) - [changed notation for context]

• The block type must be valid as some instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

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

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

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

• Then the compound instruction is valid with type \([t_1^\ast~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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 with 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.

Todo

below is the official specification.

(*)- [changed notation for context]

• The block type must be valid as some function type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

• For every catch clause \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_i\) in \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}^\ast\), \(\href{../syntax/instructions.html#syntax-catch}{\mathit{catch}}_i\) must be valid.

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

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

• Then the compound instruction is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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} \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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) exists.

• The expansion of the tag type \(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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

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

Todo

below is the official specification

(**) - [THE OFFICIAL SPECIFICATION IS WRONG! It should have “expansion” in the tag type ]

• The tag \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x]\) must be defined in the context.

• Let \([t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [{t'}^\ast]\) be the expansion of the tag type \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x]\).

• The result type \([{t'}^\ast]\) must be empty.

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

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

• Then the catch clause is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x] \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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x]\) exists.

• The expansion of the tag type \(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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

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

Todo

below is the official specification

(**) - [THE OFFICIAL SPECIFICATION IS WRONG! It should have “expansion” in the tag type ]

(**) - [“R E F E X N” to “ref exn” IN THE OFFICIAL PROSE]

• The tag \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x]\) must be defined in the context.

• Let \([t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [{t'}^\ast]\) be the expansion of the tag type \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x]\).

• The result type \([{t'}^\ast]\) must be empty.

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

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

• Then the catch clause is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x] \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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

• The value type sequence \(\epsilon\) matches the result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

• The result type \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be empty.

• Then the catch clause is valid.

\[\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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

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

Todo

below is the official specification

(**) - [“R E F E X N” to “ref exn” IN THE OFFICIAL PROSE]

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

• The result type \([(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}})]\) must match \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\).

• Then the catch clause is valid.

\[\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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

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

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

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

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

• Then the instruction is valid with any valid type of the form \([t_1^\ast~t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

\[\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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

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

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

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

• Then the instruction is valid with type \([t^\ast~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

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

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

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

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

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

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l_N]\) must be defined in the context.

• For each label \(l_i\) in \(l^\ast\), the label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l_i]\) must be defined in the context.

• There must be a sequence \(t^\ast\) of value types, such that:

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

  • For all \(l_i\) in \(l^\ast\), the result type \([t^\ast]\) matches \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l_i]\).

• Then the instruction is valid with any valid type of the form \([t_1^\ast~t^\ast~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

\[\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 linear 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}}~\epsilon~{\mathit{ht}})\) if:

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

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

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

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

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

• Then the instruction is valid with type \([t^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{ht})]\) for any valid heap type \(\mathit{ht}\).

\[\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 result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

• The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is equal to \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\epsilon~{\mathit{ht}})\).

Todo

below is the official specification

(*) - Simplified prose.

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

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

• The result type \([{t'}^\ast]\) must contain at least one type.

• Let the value type \(t_l\) be the last element in the sequence \({t'}^\ast\), and \([t^\ast]\) the remainder of the sequence preceding it.

• The value type \(t_l\) must be a reference type of the form \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\mathit{ht}\).

• Then the instruction is valid with type \([t^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast]\).

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

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

• The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is equal to \({t^\ast}~{\mathit{rt}}\).

• The reference type \({\mathit{rt}}_1\) is valid.

• The reference type \({\mathit{rt}}_2\) is valid.

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

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

• Let \({t'}\) be the reference type \({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2\).

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

• Let \([t_l^\ast]\) be the result type \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\).

• The type sequence \(t_l^\ast\) must be of the form \(t^\ast~\mathit{rt}'\).

• The reference type \(\mathit{rt}_1\) must be valid.

• The reference type \(\mathit{rt}_2\) must be valid.

• The reference type \(\mathit{rt}_2\) must match \(\mathit{rt}_1\).

• The reference type \(\mathit{rt}_2\) must match \(\mathit{rt}'\).

• Let \(\mathit{rt}'_1\) be the type difference between \(\mathit{rt}_1\) and \(\mathit{rt}_2\).

• Then the instruction is valid with type \([t^\ast~\mathit{rt}_1] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast~\mathit{rt}'_1]\).

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

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~\mathit{rt}_1~\mathit{rt}_2\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2)\) is valid with the instruction type \({t^\ast}~{\mathit{rt}}_1~\rightarrow~{t^\ast}~{\mathit{rt}}_2\) if:

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

• The result type \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is equal to \({t^\ast}~{\mathit{rt}}\).

• The reference type \({\mathit{rt}}_1\) is valid.

• The reference type \({\mathit{rt}}_2\) is valid.

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

• The reference type \({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}\).

Todo

below is the official specification

• The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.

• Let \([t_l^\ast]\) be the result type \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\).

• The type sequence \(t_l^\ast\) must be of the form \(t^\ast~\mathit{rt}'\).

• The reference type \(\mathit{rt}_1\) must be valid.

• The reference type \(\mathit{rt}_2\) must be valid.

• The reference type \(\mathit{rt}_2\) must match \(\mathit{rt}_1\).

• Let \(\mathit{rt}'_1\) be the type difference between \(\mathit{rt}_1\) and \(\mathit{rt}_2\).

• The reference type \(\mathit{rt}'_1\) must match \(\mathit{rt}'\).

• Then the instruction is valid with type \([t^\ast~\mathit{rt}_1] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast~\mathit{rt}_2]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast}~{\mathit{rt}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_1 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_2 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}}_1 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) exists.

• The expansion of the defined type \(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})\).

Todo

below is the official specification

• The function \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be defined in the context.

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

• Then the instruction is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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})\).

Todo

below is the official specification

• The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be defined in the context.

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

• Then the instruction is valid with type \([t_1^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) exists.

• The expansion of the defined 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})\).

Todo

below is the official specification

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• The reference type \(t\) must match type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/modules.html#syntax-func}{\mathsf{func}}\).

• The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y]\) must be defined in the context.

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

• Then the instruction is valid with type \([t_1^\ast~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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] \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 equal to \({t^\ast}\).

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

Todo

below is the official specification

(*) - [changed prose from (seemingly wrong) “t1* -> t2*” to (seemingly correct) “t1* t* -> t2*”]

• The return type \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\) must not be absent in the context.

• Let \([t^\ast]\) be the result type of \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\).

• Then the instruction is valid with any valid type of the form \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\).

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

• The expansion of the defined type \(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 equal to \({{t'}_2^\ast}\).

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

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

Todo

below is the official specification

• The return type \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\) must not be absent in the context.

• The function \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be defined in the context.

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be a function 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 \([t_2^\ast]\) must match \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\).

• Then the instruction is valid with any valid type \([t_3^\ast~t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_4^\ast]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x] \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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

• The expansion of the defined 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 equal to \({{t'}_2^\ast}\).

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

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

Todo

below is the official specification

• The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be defined in the context.

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a function 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 \([t_2^\ast]\) must match \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\).

• Then the instruction is valid with any valid type \([t_3^\ast~t_1^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_4^\ast]\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x] \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 type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.

• The table type \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is equal to \(({\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 defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[y]\) exists.

• The expansion of the defined 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 equal to \({{t'}_2^\ast}\).

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

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

Todo

below is the official specification

• The return type \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\) must not be empty in the context.

• The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.

• Let \(\mathit{at}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

• The reference type \(t\) must match type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/modules.html#syntax-func}{\mathsf{func}}\).

• The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y]\) must be defined in the context.

• The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y]\) must be a function 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 \([t_2^\ast]\) must match \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\).

• Then the instruction is valid with type \([t_3^\ast~t_1^\ast~\mathit{at}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_4^\ast]\), for any sequences of value types \(t_3^\ast\) and \(t_4^\ast\).

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

• The expansion of the tag type \(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.

Todo

below is the official specification.

• The tag \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x]\) must be defined in the context.

• Let \([t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [{t'}^\ast]\) be the tag type \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x]\).

• The result type \([{t'}^\ast]\) must be empty.

• Then the instruction is valid with type \([t_1^\ast t^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\), for any sequences of value types \(t_1^\ast\) and \(t_2^\ast\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{tags}}{}[x] \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:

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

Todo

below is the official specification

• The instruction is valid with type \([t_1^\ast~\href{../syntax/types.html#syntax-reftype}{\mathsf{exnref}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^\ast]\), for any sequences of value types \(t_1^\ast\) and \(t_2^\ast\).

\[\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}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is valid with the instruction type \({\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) if:

• Either:

  • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \(\epsilon\).

  • The instruction type \({\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(\epsilon~\rightarrow~\epsilon\).

• Or:

  • The instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\).

  • The instruction type \({\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \({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}\).

  • \({|{\mathit{t*}}|}\) is equal to \({|{\mathit{init*}}|}\).

  • \({|x_{\mathit{{\scriptstyle 1}*}}|}\) is equal to \({|{\mathit{init*}}|}\).

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

    • The local type \(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 \(t\) in \({t^\ast}\) and \(x_1\) in \({x_1^\ast}\):

    • The local type \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x_1]\) is equal to \(({\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}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\).

  • The instruction type \({\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \({\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}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\).

  • The instruction type \({\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \({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.

Todo

below is the official specification

• The empty instruction sequence is valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

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

Non-empty Instruction Sequence: \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}~{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast\)

Todo

below is the official specification

(*) - Simpified notaion for context

• The instruction \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}\) must be valid with some type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast} [t_2^\ast]\).

• Let \(C'\) be the same context as \(C\), but with:

  • \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) the same as in C, except that for every local index \(x\) in \(x_1^\ast\), the local type \(\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) has been updated to initialization status \(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}\).

• Under the context \(C'\), the instruction sequence \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast\) must be valid with some type \([t_2^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_2^\ast} [t_3^\ast]\).

• Then the combined instruction sequence is valid with type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast x_2^\ast} [t_3^\ast]\).

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

Subsumption for \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)

Todo

below is the official specification

• The instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with some type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\).

• The instruction type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\): must be a valid

• The instruction type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}\) must match the type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\).

• Then the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is also valid with type \(\href{../valid/conventions.html#syntax-instrtype}{\mathit{instrtype}}'\).

\[\begin{split}\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}'} } \\[3ex]\displaystyle \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}\end{split}\]

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

\[(\mathsf{const}~\mathsf{i{\scriptstyle 31}}~1)~(\mathsf{const}~\mathsf{i{\scriptstyle 32}}~2)~\mathsf{binop}~\mathsf{i{\scriptstyle 32}}~\mathsf{add}\]

\[(\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 \((\mathsf{const}~\mathsf{i{\scriptstyle 32}}~2)~\mathsf{binop}~\mathsf{i{\scriptstyle 32}}~\mathsf{add}\) needs to be valid with an intermediate type. But the direct type of \((\mathsf{const}~\mathsf{i{\scriptstyle 32}}~2)\) is \(\epsilon \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\), not matching the two inputs expected by \(\mathsf{binop}~\mathsf{i{\scriptstyle 32}}~\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 \(\mathsf{add}~\mathsf{i{\scriptstyle 32}}\) 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}\).

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

The expression \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the result type \({t^\ast}\) if:

• The expression \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \(\epsilon~\rightarrow~{t^\ast}\).

Todo

below is the official specification

(L1) - [should expr be be “instr* end”?]

• The instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t^\ast]\).

• Then the expression is valid with result type \([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

\({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is const 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 const.

\({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is const if:

• Either:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(({\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{nt}})\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(({\mathit{vt}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_{\mathit{vt}})\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~{\mathit{ht}})\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}}\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x~n)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}}\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}}\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x)\).

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

  • The global type \(C{.}\href{../valid/conventions.html#context}{\mathsf{globals}}{}[x]\) is equal to \((\epsilon~t)\).

• Or:

  • The instruction \({\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(({\href{../syntax/types.html#syntax-numtype}{\mathsf{i}}}{{\href{../syntax/types.html#syntax-numtype}{\scriptstyle\kern-0.1emN}}} {.} {\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}}\)].

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

Todo

below is the official specification

• In a constant expression \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) all instructions in \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be constant.

• A constant instruction \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}\) must be:

  • either of the form \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\),

  • or of the form \(\mathsf{i}\mathit{nn}\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{ibinop}}\), where \(\href{../syntax/instructions.html#syntax-binop}{\mathit{ibinop}}\) is limited to \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\), \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{sub}}\), or \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\).

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-i31}{\mathsf{ref{.}i\scriptstyle31}}\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new}}~x\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-struct}{\mathsf{struct{.}new\_default}}~x\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new}}~x\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_default}}~x\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-array}{\mathsf{array{.}new\_fixed}}~x\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{any{.}convert\_extern}}\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-extern}{\mathsf{extern{.}convert\_any}}\),

  • or of the form \(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global{.}get}}~x\), in which case \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\) must be a global type of the form \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~t\).

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