Instructions

Instructions are classified by function types \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) that describe how they manipulate the operand stack. The types describe 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.

Note

For example, the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) has type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\), consuming two \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) values and producing one.

Typing extends to instruction sequences \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\). Such a sequence has a function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) if the accumulative effect of executing the instructions is consuming values of types \(t_1^\ast\) off the operand stack and pushing new values of types \(t_2^\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 \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\) and \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}\).

  • stack-polymorphic: the entire (or most of the) function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\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 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\), \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}\), \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}\), and \(\href{../syntax/instructions.html#syntax-instr-control}{\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 \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}\) instruction is valid with type \([t~t~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t]\), for any possible number type \(t\). Consequently, both instruction sequences

\[(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~1)~~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~2)~~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~3)~~\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}{}\]

and

\[(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~1.0)~~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~2.0)~~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~3)~~\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}{}\]

are valid, with \(t\) in the typing of \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}\) being instantiated to \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) or \(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}\), respectively.

The \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\) instruction is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) for any possible sequences of value types \(t_1^\ast\) and \(t_2^\ast\). Consequently,

\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}~~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\]

is valid by assuming type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\) for the \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\) instruction. In contrast,

\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}~~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\]

is invalid, because there is no possible type to pick for the \(\href{../syntax/instructions.html#syntax-instr-control}{\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.

Numeric Instructions

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)

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

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}}\)

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

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.}\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}} : [t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}\)

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

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}} : [t~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}}\)

  • The instruction is valid with type \([t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.}\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}} : [t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}}\)

  • The instruction is valid with type \([t~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.}\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}} : [t~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(t_2\mathsf{.}\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}\mathsf{\_}t_1\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\)

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

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t_2\mathsf{.}\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}\mathsf{\_}t_1\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^? : [t_1] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2] }\]

Reference Instructions

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

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

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

\[\frac{ C \href{../valid/types.html#valid-heaptype}{\vdash} \mathit{ht} \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~\mathit{ht} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] }\]

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

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

  • There must exist a type index \(y\) such that \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y]\) is the same function type as \(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 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~y)]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x] = C.\href{../valid/conventions.html#context}{\mathsf{types}}[y] \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 : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~y)] }\]

\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}is\_null}}\)

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

\[\frac{ C \href{../valid/types.html#valid-heaptype}{\vdash} \mathit{ht} \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}is\_null}} : [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}as\_non\_null}}\)

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

\[\frac{ C \href{../valid/types.html#valid-heaptype}{\vdash} \mathit{ht} \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}as\_non\_null}} : [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\mathit{ht})] \href{../syntax/types.html#syntax-functype}{\rightarrow} [(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{ht})] }\]

Vector Instructions

Vector instructions can have a prefix to describe the shape of the operand. Packed numeric types, \(\href{../exec/runtime.html#syntax-storagetype}{\mathsf{i8}}\) and \(\href{../exec/runtime.html#syntax-storagetype}{\mathsf{i16}}\), are not value type, we define an auxiliary function to map such packed types into value types:

\[\begin{split}\begin{array}{lll@{\qquad}l} \href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\mathsf{i8x16}) &=& \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}} \\ \href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\mathsf{i16x8}) &=& \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}} \\ \href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(t\mathsf{x}N) &=& t \end{array}\end{split}\]

We also define an auxiliary function to get number of packed numeric types in a \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\), dimension:

\[\begin{array}{lll@{\qquad}l} \href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(t\mathsf{x}N) &=& N \end{array}\]

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\)

  • The instruction is valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvtestop}{\mathit{vvtestop}}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvtestop}{\mathit{vvtestop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(\mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{swizzle}}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{swizzle}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}^{16}\)

  • 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-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ (\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < 32)^{16} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}^{16} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}}\)

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

  • The instruction is valid with type \([t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}} : [\href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\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 lane index \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\) must be smaller than \(\href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})]\).

\[\frac{ \href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < \href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{x}N\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}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})] }\]

\(\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 lane index \(\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\) must be smaller than \(\href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\).

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

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ \href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < \href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

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

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

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

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

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

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

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

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vishiftop}{\mathit{vishiftop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

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

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vtestop}{\mathit{vtestop}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(\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 is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}^? : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\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 is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_1\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{dot}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\mathsf{\_s}\)

  • The instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_1\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{dot}}\mathsf{\_}\href{../syntax/instructions.html#syntax-shape}{\mathit{ishape}}_2\mathsf{\_s} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\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 is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\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 is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \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}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

Parametric Instructions

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

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

\[\frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}} : [t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

Note

Both \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\) and \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}\) without annotation are value-polymorphic instructions.

\(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~(t^\ast)^?\)

  • 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-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast]\).

  • Else:

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

\[\frac{ C \href{../valid/types.html#valid-resulttype}{\vdash} [t] \mathrel{\mbox{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-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] } \qquad \frac{ C \href{../valid/types.html#valid-resulttype}{\vdash} [t] \mathrel{\mbox{ok}} \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} [t] \href{../valid/matching.html#match-resulttype}{\leq} [\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}] }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}} : [t~t~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] } \qquad \frac{ \vdash t \leq \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-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

Note

In future versions of WebAssembly, \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}\) may allow more than one value per choice.

Variable Instructions

\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.get}}~x\)

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

  • Let \(t\) be the value type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\).

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

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x] = t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.get}}~x : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.set}}~x\)

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

  • Let \(t\) be the value type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\).

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

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x] = t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.set}}~x : [t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.tee}}~x\)

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

  • Let \(t\) be the value type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\).

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

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x] = t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.tee}}~x : [t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global.get}}~x\)

  • 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 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x] = \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global.get}}~x : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global.set}}~x\)

  • 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] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x] = \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global.set}}~x : [t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

Table Instructions

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

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

  • Let \(\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 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~x : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

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

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

  • Let \(\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 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

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

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

  • Then the instruction is valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.size}}~x : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

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

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

  • Let \(\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~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.grow}}~x : [t~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

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

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

  • Let \(\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 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y\)

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

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

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~t_1 \qquad C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~t_2 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} t_2 \href{../valid/matching.html#match-valtype}{\leq} t_1 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y\)

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

  • Let \(\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 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~t_1 \qquad C.\href{../valid/conventions.html#context}{\mathsf{elems}}[y] = t_2 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} t_2 \href{../valid/matching.html#match-valtype}{\leq} t_1 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~x\)

  • 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 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{elems}}[x] = t }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~x : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

Memory Instructions

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \qquad 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq |t|/8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.load}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \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} t\mathsf{.load}N\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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-valtype}{\mathsf{i32}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \qquad 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq |t|/8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.store}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \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} t\mathsf{.store}N~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~t] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8 \cdot M\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \qquad 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq N/8 \cdot M }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \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} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \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} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)

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

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ \href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < 128/N \qquad C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \qquad 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} < N/8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] }\]

\(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)

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

  • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0]\) 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 \(N/8\).

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}]\).

\[\frac{ \href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < 128/N \qquad C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \qquad 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} < N/8 }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.size}}\)

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

  • Then the instruction is valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.size}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.grow}}\)

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

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.grow}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] }\]

\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}}\)

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

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}}\)

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

  • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

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

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

  • 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 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[0] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \qquad C.\href{../valid/conventions.html#context}{\mathsf{datas}}[x] = {\mathrel{\mbox{ok}}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~x\)

  • 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 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{datas}}[x] = {\mathrel{\mbox{ok}}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~x : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

Control Instructions

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

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

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }\]

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

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

\[\frac{ C \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\) instruction is stack-polymorphic.

\(\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 block type must be valid as some function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\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}}\) vector.

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

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

\[\frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_2^\ast] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [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{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}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The notation \(C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t^\ast]\) inserts the new label type at index \(0\), shifting all others.

\(\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 block type must be valid as some function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [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}}\) vector.

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

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

\[\frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_1^\ast] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [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{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}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The notation \(C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t^\ast]\) inserts the new label type at index \(0\), shifting all others.

\(\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 block type must be valid as some function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\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}}\) vector.

  • Under context \(C'\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\) must be valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\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] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

  • Then the compound instruction is valid with type \([t_1^\ast~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\[\frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_2^\ast] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_2^\ast] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast : [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{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}} : [t_1^\ast~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The notation \(C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t^\ast]\) inserts the new label type at index \(0\), shifting all others.

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

  • 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_1^\ast~t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\), for any sequences of valid value types \(t_1^\ast\) and \(t_2^\ast\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l] = [t^\ast] \qquad C \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l : [t_1^\ast~t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The label index space in the context \(C\) contains the most recent label first, so that \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) performs a relative lookup as expected.

The \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}\) instruction is stack-polymorphic.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l\)

  • 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-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast]\).

\[\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-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast] }\]

Note

The label index space in the context \(C\) contains the most recent label first, so that \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) performs a relative lookup as expected.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N\)

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

  • For all \(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 result type \([t^\ast]\), 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 type \([t_1^\ast~t^\ast~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\), for any sequences of valid value types \(t_1^\ast\) and \(t_2^\ast\).

\[\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_N] \qquad C \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N : [t_1^\ast~t^\ast~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The label index space in the context \(C\) contains the most recent label first, so that \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l_i]\) performs a relative lookup as expected.

The \(\href{../syntax/instructions.html#syntax-instr-control}{\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 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})] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathit{ht})]\) for any valid heap type \(\mathit{ht}\).

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

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l\)

  • 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})] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast]\).

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

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

  • 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 type \([t_1^\ast~t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\), for any sequences of valid value types \(t_1^\ast\) and \(t_2^\ast\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{return}} = [t^\ast] \qquad C \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}} : [t_1^\ast~t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Note

The \(\href{../syntax/instructions.html#syntax-instr-control}{\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{call}}~x\)

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

  • Then the instruction is valid with type \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x] = [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] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

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

  • Let \(x\) be some type index for which \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) is a function type of the form \([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)] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[x] = [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}} : [t_1^\ast~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~x)] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y\)

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

  • Let \(\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/types.html#syntax-heaptype}{\mathsf{func}}\).

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

  • Let \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) be the function type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y]\).

  • Then the instruction is valid with type \([t_1^\ast~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t \qquad C \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}} \qquad C.\href{../valid/conventions.html#context}{\mathsf{types}}[y] = [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~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

Instruction Sequences

Typing of instruction sequences is defined recursively.

Empty Instruction Sequence: \(\epsilon\)

  • The empty instruction sequence is valid with type \([t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast]\), for any sequence of value types \(t^\ast\).

\[\frac{ }{ C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \epsilon : [t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast] }\]

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

  • The instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\), for some sequences of value types \(t_1^\ast\) and \(t_2^\ast\).

  • The instruction \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_N\) must be valid with type \([t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_3^\ast]\), for some sequences of value types \(t^\ast\) and \(t_3^\ast\).

  • There must be a sequence of value types \(t_0^\ast\), such that \(t_2^\ast = t_0^\ast~{t'}^\ast\) where the type sequence \({t'}^\ast\) is as long as \(t^\ast\).

  • For each value type \(t'_i\) in \({t'}^\ast\) and corresponding type \(t_i\) in \(t^\ast\), the type \(t'_i\) must match \(t_i\).

  • Then the combined instruction sequence is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_0^\ast~t_3^\ast]\).

\[\frac{ C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_0^\ast~{t'}^\ast] \qquad (C \href{../valid/matching.html#match-valtype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t)^\ast \qquad C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_N : [t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_3^\ast] }{ C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_N : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_0^\ast~t_3^\ast] }\]

Expressions

Expressions \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) are classified by result types of the form \([t^\ast]\).

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

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

  • For each value type \(t'_i\) in \({t'}^\ast\) and corresponding valid value type type \(t_i\) in \(t^\ast\), \(t'_i\) matches \(t_i\).

  • Then the expression is valid with result type \([t^\ast]\).

\[\frac{ C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [{t'}^\ast] \qquad C \href{../valid/types.html#valid-resulttype}{\vdash} [t^\ast] \mathrel{\mbox{ok}} \qquad (C \href{../valid/matching.html#match-valtype}{\vdash} t' \href{../valid/matching.html#match-valtype}{\leq} t)^\ast }{ C \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [t^\ast] }\]

Constant Expressions

  • 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 \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}\),

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

\[\frac{ (C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}})^\ast }{ C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} }\]
\[\frac{ }{ C \href{../valid/instructions.html#valid-constant}{\vdash} t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} } \qquad \frac{ }{ C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}func}}~x \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} }\]
\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x] = \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~t }{ C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global.get}}~x \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} }\]

Note

Currently, constant expressions occurring as initializers of globals are further constrained in that contained \(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{global.get}}\) instructions are only allowed to 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.