Instructions

WebAssembly computation is performed by executing individual instructions.

Numeric Instructions

Numeric instructions are defined in terms of the generic numeric operators. The mapping of numeric instructions to their underlying operators is expressed by the following definition:

$$\begin{array}{r}\begin{array}{lll}{\mathit{op}}_{\mathsf{i}N}(i_1,\dots ,i_k)& =& \mathrm{i}{\mathit{op}}_N(i_1,\dots ,i_k)\\ {\mathit{op}}_{\mathsf{f}N}(z_1,\dots ,z_k)& =& \mathrm{f}{\mathit{op}}_N(z_1,\dots ,z_k)\\ {\mathit{op}}_{\mathsf{v}N}(i_1,\dots ,i_k)& =& \mathrm{i}{\mathit{op}}_N(i_1,\dots ,i_k)\end{array}\end{array}$$

And for conversion operators:

$$\begin{array}{r}\begin{array}{lll}{\mathit{cvtop}}_{t_1,t_2}^{{\mathit{sx}}^{?}}(c)& =& {\mathit{cvtop}}_{|t_1|,|t_2|}^{{\mathit{sx}}^{?}}(c)\end{array}\end{array}$$

Where the underlying operators are partial, the corresponding instruction will trap when the result is not defined. Where the underlying operators are non-deterministic, because they may return one of multiple possible NaN values, so are the corresponding instructions.

Note

For example, the result of instruction $\mathsf{i}\mathsf{32}.\mathsf{add}$ applied to operands $i_1,i_2$ invokes ${\mathsf{add}}_{\mathsf{i}\mathsf{32}}(i_1,i_2)$, which maps to the generic ${\mathrm{iadd}}_{32}(i_1,i_2)$ via the above definition. Similarly, $\mathsf{i}\mathsf{64}.\mathsf{trunc}\mathsf{\_}\mathsf{f}\mathsf{32}\mathsf{\_}\mathsf{s}$ applied to $z$ invokes ${\mathsf{trunc}}_{\mathsf{f}\mathsf{32},\mathsf{i}\mathsf{64}}^{\mathsf{s}}(z)$, which maps to the generic ${\mathrm{trunc}}_{32,64}^{\mathsf{s}}(z)$.

$t\mathsf{.}\mathsf{const}c$

1. Push the value $t.\mathsf{const}c$ to the stack.

Note

No formal reduction rule is required for this instruction, since $\mathsf{const}$ instructions already are values.

$t\mathsf{.}\mathit{unop}$

1. Assert: due to validation, a value of value type $t$ is on the top of the stack.

2. Pop the value $t.\mathsf{const}{c}_1$ from the stack.

3. If ${\mathit{unop}}_t(c_1)$ is defined, then:

   1. Let $c$ be a possible result of computing ${\mathit{unop}}_t(c_1)$.

   2. Push the value $t.\mathsf{const}c$ to the stack.

4. Else:

   1. Trap.

$$\begin{array}{r}\begin{array}{lcll}(t\mathsf{.}\mathsf{const}{c}_1)t\mathsf{.}\mathit{unop}& \hookrightarrow & (t\mathsf{.}\mathsf{const}c)& (\text{if}c\in {\mathit{unop}}_t(c_1))\\ (t\mathsf{.}\mathsf{const}{c}_1)t\mathsf{.}\mathit{unop}& \hookrightarrow & \mathsf{trap}& (\text{if}{\mathit{unop}}_t(c_1)=\{\})\end{array}\end{array}$$

$t\mathsf{.}\mathit{binop}$

1. Assert: due to validation, two values of value type $t$ are on the top of the stack.

2. Pop the value $t.\mathsf{const}{c}_2$ from the stack.

3. Pop the value $t.\mathsf{const}{c}_1$ from the stack.

4. If ${\mathit{binop}}_t(c_1,c_2)$ is defined, then:

   1. Let $c$ be a possible result of computing ${\mathit{binop}}_t(c_1,c_2)$.

   2. Push the value $t.\mathsf{const}c$ to the stack.

5. Else:

   1. Trap.

$$\begin{array}{r}\begin{array}{lcll}(t\mathsf{.}\mathsf{const}{c}_1)(t\mathsf{.}\mathsf{const}{c}_2)t\mathsf{.}\mathit{binop}& \hookrightarrow & (t\mathsf{.}\mathsf{const}c)& (\text{if}c\in {\mathit{binop}}_t(c_1,c_2))\\ (t\mathsf{.}\mathsf{const}{c}_1)(t\mathsf{.}\mathsf{const}{c}_2)t\mathsf{.}\mathit{binop}& \hookrightarrow & \mathsf{trap}& (\text{if}{\mathit{binop}}_t(c_1,c_2)=\{\})\end{array}\end{array}$$

$t\mathsf{.}\mathit{testop}$

1. Assert: due to validation, a value of value type $t$ is on the top of the stack.

2. Pop the value $t.\mathsf{const}{c}_1$ from the stack.

3. Let $c$ be the result of computing ${\mathit{testop}}_t(c_1)$.

4. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}(t\mathsf{.}\mathsf{const}{c}_1)t\mathsf{.}\mathit{testop}& \hookrightarrow & (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathit{testop}}_t(c_1))\end{array}\end{array}$$

$t\mathsf{.}\mathit{relop}$

1. Assert: due to validation, two values of value type $t$ are on the top of the stack.

2. Pop the value $t.\mathsf{const}{c}_2$ from the stack.

3. Pop the value $t.\mathsf{const}{c}_1$ from the stack.

4. Let $c$ be the result of computing ${\mathit{relop}}_t(c_1,c_2)$.

5. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}(t\mathsf{.}\mathsf{const}{c}_1)(t\mathsf{.}\mathsf{const}{c}_2)t\mathsf{.}\mathit{relop}& \hookrightarrow & (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathit{relop}}_t(c_1,c_2))\end{array}\end{array}$$

$t_2\mathsf{.}\mathit{cvtop}\mathsf{\_}{t}_1\mathsf{\_}{\mathit{sx}}^{?}$

1. Assert: due to validation, a value of value type $t_1$ is on the top of the stack.

2. Pop the value $t_1.\mathsf{const}{c}_1$ from the stack.

3. If ${\mathit{cvtop}}_{t_1,t_2}^{{\mathit{sx}}^{?}}(c_1)$ is defined:

   1. Let $c_2$ be a possible result of computing ${\mathit{cvtop}}_{t_1,t_2}^{{\mathit{sx}}^{?}}(c_1)$.

   2. Push the value $t_2.\mathsf{const}{c}_2$ to the stack.

4. Else:

   1. Trap.

$$\begin{array}{r}\begin{array}{lcll}(t_1\mathsf{.}\mathsf{const}{c}_1)t_2\mathsf{.}\mathit{cvtop}\mathsf{\_}{t}_1\mathsf{\_}{\mathit{sx}}^{?}& \hookrightarrow & (t_2\mathsf{.}\mathsf{const}{c}_2)& (\text{if}{c}_2\in {\mathit{cvtop}}_{t_1,t_2}^{{\mathit{sx}}^{?}}(c_1))\\ (t_1\mathsf{.}\mathsf{const}{c}_1)t_2\mathsf{.}\mathit{cvtop}\mathsf{\_}{t}_1\mathsf{\_}{\mathit{sx}}^{?}& \hookrightarrow & \mathsf{trap}& (\text{if}{\mathit{cvtop}}_{t_1,t_2}^{{\mathit{sx}}^{?}}(c_1)=\{\})\end{array}\end{array}$$

Reference Instructions

$\mathsf{ref}\mathsf{.}\mathsf{null}t$

1. Push the value $\mathsf{ref}\mathsf{.}\mathsf{null}t$ to the stack.

Note

No formal reduction rule is required for this instruction, since the $\mathsf{ref}\mathsf{.}\mathsf{null}$ instruction is already a value.

$\mathsf{ref}\mathsf{.}\mathsf{is}\mathsf{\_}\mathsf{null}$

1. Assert: due to validation, a reference value is on the top of the stack.

2. Pop the value $\mathit{val}$ from the stack.

3. If $\mathit{val}$ is $\mathsf{ref}\mathsf{.}\mathsf{null}t$, then:

   1. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}1$ to the stack.

4. Else:

   1. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}0$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}\mathit{val}\mathsf{ref}\mathsf{.}\mathsf{is}\mathsf{\_}\mathsf{null}& \hookrightarrow & (\mathsf{i}\mathsf{32}.\mathsf{const}1)& (\text{if}\mathit{val}=\mathsf{ref}\mathsf{.}\mathsf{null}t)\\ \mathit{val}\mathsf{ref}\mathsf{.}\mathsf{is}\mathsf{\_}\mathsf{null}& \hookrightarrow & (\mathsf{i}\mathsf{32}.\mathsf{const}0)& (\text{otherwise})\end{array}\end{array}$$

$\mathsf{ref}\mathsf{.}\mathsf{func}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{funcaddrs}[x]$ exists.

3. Let $a$ be the function address $F.\mathsf{module}.\mathsf{funcaddrs}[x]$.

4. Push the value $\mathsf{ref}a$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}F;(\mathsf{ref}\mathsf{.}\mathsf{func}x)& \hookrightarrow & F;(\mathsf{ref}a)& (\text{if}a=F.\mathsf{module}.\mathsf{funcaddrs}[x])\end{array}\end{array}$$

Vector Instructions

Most vector instructions are defined in terms of generic numeric operators applied lane-wise based on the shape.

$$\begin{array}{lll}{\mathit{op}}_{t\mathsf{x}N}(n_1,\dots ,n_k)& =& {\mathrm{lanes}}_{t\mathsf{x}N}^{-1}(o{p}_t({\mathrm{lanes}}_{t\mathsf{x}N}(n_1)\dots {\mathrm{lanes}}_{t\mathsf{x}N}(n_k))\end{array}$$

Note

For example, the result of instruction $\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}.\mathsf{add}$ applied to operands $i_1,i_2$ invokes ${\mathsf{add}}_{\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}}(i_1,i_2)$, which maps to ${\mathrm{lanes}}_{\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}}^{-1}({\mathsf{add}}_{\mathsf{i}\mathsf{32}}(i_1^{+},i_2^{+}))$, where $i_1^{+}$ and $i_2^{+}$ are sequences resulting from invoking ${\mathrm{lanes}}_{\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}}(i_1)$ and ${\mathrm{lanes}}_{\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}}(i_2)$ respectively.

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c$

1. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

Note

No formal reduction rule is required for this instruction, since $\mathsf{const}$ instructions coincide with values.

$\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vvunop}$

1. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

3. Let $c$ be the result of computing ${\mathit{vvunop}}_{\mathsf{v}\mathsf{128}}(c_1)$.

4. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vvunop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathit{vvunop}}_{\mathsf{v}\mathsf{128}}(c_1))\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vvbinop}$

1. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $c$ be the result of computing ${\mathit{vvbinop}}_{\mathsf{v}\mathsf{128}}(c_1,c_2)$.

5. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vvbinop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathit{vvbinop}}_{\mathsf{v}\mathsf{128}}(c_1,c_2))\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vvternop}$

1. Assert: due to validation, three values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_3$ from the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

4. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

5. Let $c$ be the result of computing ${\mathit{vvternop}}_{\mathsf{v}\mathsf{128}}(c_1,c_2,c_3)$.

6. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_3)\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vvternop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathit{vvternop}}_{\mathsf{v}\mathsf{128}}(c_1,c_2,c_3))\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{any}\mathsf{\_}\mathsf{true}$

1. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

3. Let $i$ be the result of computing ${\mathrm{ine}}_{128}(c_1,0)$.

4. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ onto the stack.

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{any}\mathsf{\_}\mathsf{true}& \hookrightarrow & (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}i)& (\text{if}i={\mathrm{ine}}_{128}(c_1,0))\end{array}\end{array}$$

$\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16.}\mathsf{swizzle}$

1. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

3. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_2)$.

4. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

5. Let $j^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_1)$.

6. Let $c^{\ast }$ be the concatenation of the two sequences $j^{\ast }$ and $0^{240}$.

7. Let $c^{\prime }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}^{-1}(c^{\ast }[i^{\ast }[0]]\dots c^{\ast }[i^{\ast }[15]])$.

8. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}^{\prime }$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}\mathsf{.}\mathsf{swizzle}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}^{\prime })\end{array}\\ \begin{array}{rl}(\text{if}& i^{\ast }={\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_2)\\ \wedge & c^{\ast }={\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_1)0^{240}\\ \wedge & c^{\prime }={\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}^{-1}(c^{\ast }[i^{\ast }[0]]\dots c^{\ast }[i^{\ast }[15]]))\end{array}\end{array}\end{array}$$

$\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16.}\mathsf{shuffle}{x}^{\ast }$

1. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Assert: due to validation, for all $x_i$ in $x^{\ast }$ it holds that $x_i<32$.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

4. Let $i_2^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_2)$.

5. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

6. Let $i_1^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_1)$.

7. Let $i^{\ast }$ be the concatenation of the two sequences $i_1^{\ast }$ and $i_2^{\ast }$.

8. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}^{-1}(i^{\ast }[x^{\ast }[0]]\dots i^{\ast }[x^{\ast }[15]])$.

9. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)(\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}\mathsf{.}\mathsf{shuffle}{x}^{\ast })& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& i^{\ast }={\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_1){\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}(c_2)\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}\mathsf{8}\mathsf{x}\mathsf{16}}^{-1}(i^{\ast }[x^{\ast }[0]]\dots i^{\ast }[x^{\ast }[15]]))\end{array}\end{array}\end{array}$$

$\mathit{shape}\mathsf{.}\mathsf{splat}$

1. Let $t$ be the type $\mathrm{unpacked}(\mathit{shape})$.

2. Assert: due to validation, a value of value type $t$ is on the top of the stack.

3. Pop the value $t.\mathsf{const}{c}_1$ from the stack.

4. Let $N$ be the integer $\dim (\mathit{shape})$.

5. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathit{shape}}^{-1}(c_1^N)$.

6. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}(t\mathsf{.}\mathsf{const}{c}_1)\mathit{shape}\mathsf{.}\mathsf{splat}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)& (\text{if}t=\mathrm{unpacked}(\mathit{shape})\wedge c={\mathrm{lanes}}_{\mathit{shape}}^{-1}(c_1^{\dim (\mathit{shape})}))\end{array}\end{array}$$

$t_1\mathsf{x}N\mathsf{.}\mathsf{extract}\mathsf{\_}\mathsf{lane}\mathsf{\_}{\mathit{sx}}^{?}x$

1. Assert: due to validation, $x<N$.

2. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}N}(c_1)$.

5. Let $t_2$ be the type $\mathrm{unpacked}(t_1\mathsf{x}N)$.

6. Let $c_2$ be the result of computing ${\mathrm{extend}}_{t_1,t_2}^{s{x}^{?}}(i^{\ast }[x])$.

7. Push the value $t_2.\mathsf{const}{c}_2$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(t_1\mathsf{x}N\mathsf{.}\mathsf{extract}\mathsf{\_}\mathsf{lane}x)& \hookrightarrow & (t_2\mathsf{.}\mathsf{const}{c}_2)\end{array}\\ \begin{array}{rl}(\text{if}& t_2=\mathrm{unpacked}(t_1\mathsf{x}N)\\ \wedge & c_2={\mathrm{extend}}_{t_1,t_2}^{s{x}^{?}}({\mathrm{lanes}}_{t_1\mathsf{x}N}(c_1)[x]))\end{array}\end{array}\end{array}$$

$\mathit{shape}\mathsf{.}\mathsf{replace}\mathsf{\_}\mathsf{lane}x$

1. Assert: due to validation, $x<\dim (\mathit{shape})$.

2. Let $t_1$ be the type $\mathrm{unpacked}(\mathit{shape})$.

3. Assert: due to validation, a value of value type $t_1$ is on the top of the stack.

4. Pop the value $t_1.\mathsf{const}{c}_1$ from the stack.

5. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

6. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

7. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathit{shape}}(c_2)$.

8. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathit{shape}}^{-1}(i^{\ast }\text{with}[x]=c_1)$.

9. Push $\mathsf{v}\mathsf{128}.\mathsf{const}c$ on the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(t_1\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)(\mathit{shape}\mathsf{.}\mathsf{replace}\mathsf{\_}\mathsf{lane}x)& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& i^{\ast }={\mathrm{lanes}}_{\mathit{shape}}(c_2)\\ \wedge & c={\mathrm{lanes}}_{\mathit{shape}}^{-1}(i^{\ast }\text{with}[x]=c_1))\end{array}\end{array}\end{array}$$

$\mathit{shape}\mathsf{.}\mathit{vunop}$

1. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

3. Let $c$ be the result of computing ${\mathit{vunop}}_{\mathit{shape}}(c_1)$.

4. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)\mathsf{v}\mathsf{128}\mathsf{.}\mathit{vunop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathit{vunop}}_{\mathit{shape}}(c_1))\end{array}$$

$\mathit{shape}\mathsf{.}\mathit{vbinop}$

1. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. If ${\mathit{vbinop}}_{\mathit{shape}}(c_1,c_2)$ is defined:

   1. Let $c$ be a possible result of computing ${\mathit{vbinop}}_{\mathit{shape}}(c_1,c_2)$.

   2. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

5. Else:

   1. Trap.

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)\mathit{shape}\mathsf{.}\mathit{vbinop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)& (\text{if}c\in {\mathit{vbinop}}_{\mathit{shape}}(c_1,c_2))\\ (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)\mathit{shape}\mathsf{.}\mathit{vbinop}& \hookrightarrow & \mathsf{trap}& (\text{if}{\mathit{vbinop}}_{\mathit{shape}}(c_1,c_2)=\{\})\end{array}\end{array}$$

$t\mathsf{x}N\mathsf{.}\mathit{vrelop}$

1. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i_1^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t\mathsf{x}N}(c_1)$.

5. Let $i_2^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t\mathsf{x}N}(c_2)$.

6. Let $i^{\ast }$ be the result of computing ${\mathit{vrelop}}_t(i_1^{\ast },i_2^{\ast })$.

7. Let $j^{\ast }$ be the result of computing ${\mathrm{extend}}_{1,|t|}^{\mathsf{s}}(i^{\ast })$.

8. Let $c$ be the result of computing ${\mathrm{lanes}}_{t\mathsf{x}N}^{-1}(j^{\ast })$.

9. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)t\mathsf{x}N\mathsf{.}\mathit{vrelop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{r}(\text{if}c={\mathrm{lanes}}_{t\mathsf{x}N}^{-1}({\mathrm{extend}}_{1,|t|}^{\mathsf{s}}({\mathit{vrelop}}_t({\mathrm{lanes}}_{t\mathsf{x}N}(c_1),{\mathrm{lanes}}_{t\mathsf{x}N}(c_2)))))\end{array}\end{array}\end{array}$$

$t\mathsf{x}N\mathsf{.}\mathit{vishiftop}$

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ from the stack.

3. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

4. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

5. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t\mathsf{x}N}(c_1)$.

6. Let $j^{\ast }$ be the result of computing ${\mathit{vishiftop}}_t(i^{\ast },s^N)$.

7. Let $c$ be the result of computing ${\mathrm{lanes}}_{t\mathsf{x}N}^{-1}(j^{\ast })$.

8. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}s)t\mathsf{x}N\mathsf{.}\mathit{vishiftop}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& i^{\ast }={\mathrm{lanes}}_{t\mathsf{x}N}(c_1)\\ \wedge & c={\mathrm{lanes}}_{t\mathsf{x}N}^{-1}({\mathit{vishiftop}}_t(i^{\ast },s^N)))\end{array}\end{array}\end{array}$$

$\mathit{shape}\mathsf{.}\mathsf{all}\mathsf{\_}\mathsf{true}$

1. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

3. Let $i_1^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathit{shape}}(c_1)$.

4. Let $i$ be the result of computing $\mathrm{bool}(\bigwedge (i_1\ne 0{)}^{\ast })$.

5. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)\mathit{shape}\mathsf{.}\mathsf{all}\mathsf{\_}\mathsf{true}& \hookrightarrow & (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}i)\end{array}\\ \begin{array}{rl}(\text{if}& i_1^{\ast }={\mathrm{lanes}}_{\mathit{shape}}(c)\\ \wedge & i=\mathrm{bool}(\bigwedge (i_1\ne 0{)}^{\ast }))\end{array}\end{array}\end{array}$$

$t\mathsf{x}N\mathsf{.}\mathsf{bitmask}$

1. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

3. Let $i_1^N$ be the result of computing ${\mathrm{lanes}}_{t\mathsf{x}N}(c)$.

4. Let $B$ be the bit width $|t|$ of value type $t$.

5. Let $i_2^N$ be the result of computing ${\mathrm{ilt}\mathrm{\_}\mathrm{s}}_B(i_1^N,0^N)$.

6. Let $j^{\ast }$ be the concatenation of the two sequences $i_2^N$ and $0^{32-N}$.

7. Let $c$ be the result of computing ${\mathrm{ibits}}_{32}^{-1}(j^{\ast })$.

8. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{lcll}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)t\mathsf{x}N\mathsf{.}\mathsf{bitmask}& \hookrightarrow & (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}c)& (\text{if}c={\mathrm{ibits}}_{32}^{-1}({\mathrm{ilt}\mathrm{\_}\mathrm{s}}_{|t|}({\mathrm{lanes}}_{t\mathsf{x}N}(c),0^N)))\end{array}\end{array}$$

$t_2\mathsf{x}N\mathsf{.}\mathsf{narrow}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}\mathit{sx}$

1. Assert: due to syntax, $N=2\cdot M$.

2. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

4. Let $i_2^M$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)$.

5. Let $d_2^M$ be the result of computing ${\mathrm{narrow}}_{|t_1|,|t_2|}^{\mathit{sx}}(i_2^M)$.

6. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

7. Let $i_1^M$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)$.

8. Let $d_1^M$ be the result of computing ${\mathrm{narrow}}_{|t_1|,|t_2|}^{\mathit{sx}}(i_1^M)$.

9. Let $j^N$ be the concatenation of the two sequences $d_1^M$ and $d_2^M$.

10. Let $c$ be the result of computing ${\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(j^N)$.

11. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)t_2\mathsf{x}N\mathsf{.}\mathsf{narrow}\mathrm{\_}{t}_1\mathsf{x}M\mathrm{\_}\mathit{sx}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& d_1^M={\mathrm{narrow}}_{|t_1|,|t_2|}^{\mathit{sx}}({\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1))\\ \wedge & d_2^M={\mathrm{narrow}}_{|t_1|,|t_2|}^{\mathit{sx}}({\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2))\\ \wedge & c={\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(d_1^M{d}_2^M))\end{array}\end{array}\end{array}$$

$t_2\mathsf{x}N\mathsf{.}\mathit{vcvtop}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}\mathit{sx}$

1. Assert: due to syntax, $N=M$.

2. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)$.

5. Let $j^{\ast }$ be the result of computing ${\mathit{vcvtop}}_{|t_1|,|t_2|}^{\mathit{sx}}(i^{\ast })$.

6. Let $c$ be the result of computing ${\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(j^{\ast })$.

7. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)t_2\mathsf{x}N\mathsf{.}\mathit{vcvtop}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}\mathit{sx}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& c={\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}({\mathit{vcvtop}}_{|t_1|,|t_2|}^{\mathit{sx}}({\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1))))\end{array}\end{array}\end{array}$$

$t_2\mathsf{x}N\mathsf{.}\mathit{vcvtop}\mathsf{\_}\mathit{half}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}{\mathit{sx}}^{?}$

1. Assert: due to syntax, $N=M/2$.

2. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)$.

5. If $\mathit{half}$ is $\mathsf{low}$, then:

   1. Let $j^{\ast }$ be the sequence $i^{\ast }[0\mathbf{:}N]$.

6. Else:

   1. Let $j^{\ast }$ be the sequence $i^{\ast }[N\mathbf{:}N]$.

7. Let $k^{\ast }$ be the result of computing ${\mathit{vcvtop}}_{|t_1|,|t_2|}^{{\mathit{sx}}^{?}}(j^{\ast })$.

8. Let $c$ be the result of computing ${\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(k^{\ast })$.

9. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)t_2\mathsf{x}N\mathsf{.}\mathit{vcvtop}\mathsf{\_}\mathit{half}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}{\mathit{sx}}^{?}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& c={\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}({\mathit{vcvtop}}_{|t_1|,|t_2|}^{{\mathit{sx}}^{?}}({\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)[\mathit{half}(0,N)\mathbf{:}N])))\end{array}\end{array}\end{array}$$

where:

$$\begin{array}{r}\begin{array}{lcl}\mathsf{low}(x,y)& =& x\\ \mathsf{high}(x,y)& =& y\end{array}\end{array}$$

$t_2\mathsf{x}N\mathsf{.}\mathit{vcvtop}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}\mathit{sx}\mathsf{\_}\mathsf{zero}$

1. Assert: due to syntax, $N=2\cdot M$.

2. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)$.

5. Let $j^{\ast }$ be the result of computing ${\mathit{vcvtop}}_{|t_1|,|t_2|}^{\mathit{sx}}(i^{\ast })$.

6. Let $k^{\ast }$ be the concatenation of the two sequences $j^{\ast }$ and $0^M$.

7. Let $c$ be the result of computing ${\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(k^{\ast })$.

8. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)t_2\mathsf{x}N\mathsf{.}\mathit{vcvtop}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}\mathit{sx}\mathsf{\_}\mathsf{zero}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& c={\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}({\mathit{vcvtop}}_{|t_1|,|t_2|}^{\mathit{sx}}({\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1))0^M))\end{array}\end{array}\end{array}$$

$\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4.}\mathsf{dot}\mathsf{\_}\mathsf{i}\mathsf{16}\mathsf{x}\mathsf{8}\mathsf{\_}\mathsf{s}$

1. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

2. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i_1^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{16}\mathsf{x}\mathsf{8}}(c_1)$.

5. Let $j_1^{\ast }$ be the result of computing ${\mathrm{extend}}_{16,32}^{\mathsf{s}}(i_1^{\ast })$.

6. Let $i_2^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{16}\mathsf{x}\mathsf{8}}(c_2)$.

7. Let $j_2^{\ast }$ be the result of computing ${\mathrm{extend}}_{16,32}^{\mathsf{s}}(i_2^{\ast })$.

8. Let $(k_1{k}_2{)}^{\ast }$ be the result of computing ${\mathrm{imul}}_{32}(j_1^{\ast },j_2^{\ast })$.

9. Let $k^{\ast }$ be the result of computing ${\mathrm{iadd}}_{32}(k_1,k_2{)}^{\ast }$.

10. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}}^{-1}(k^{\ast })$.

11. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4.}\mathsf{dot}\mathsf{\_}\mathsf{i}\mathsf{16}\mathsf{x}\mathsf{8}\mathsf{\_}\mathsf{s}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& (i_1{i}_2{)}^{\ast }={\mathrm{imul}}_{32}({\mathrm{extend}}_{16,32}^{\mathsf{s}}({\mathrm{lanes}}_{\mathsf{i}\mathsf{16}\mathsf{x}\mathsf{8}}(c_1)),{\mathrm{extend}}_{16,32}^{\mathsf{s}}({\mathrm{lanes}}_{\mathsf{i}\mathsf{16}\mathsf{x}\mathsf{8}}(c_2)))\\ \wedge & j^{\ast }={\mathrm{iadd}}_{32}(i_1,i_2{)}^{\ast }\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}\mathsf{32}\mathsf{x}\mathsf{4}}^{-1}(j^{\ast }))\end{array}\end{array}\end{array}$$

$t_2\mathsf{x}N\mathsf{.}\mathsf{extmul}\mathsf{\_}\mathit{half}\mathsf{\_}{t}_1\mathsf{x}M\mathsf{\_}\mathit{sx}$

1. Assert: due to syntax, $N=M/2$.

2. Assert: due to validation, two values of value type $\mathsf{v}\mathsf{128}$ are on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_2$ from the stack.

4. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

5. Let $i_1^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)$.

6. Let $i_2^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)$.

7. If $\mathit{half}$ is $\mathsf{low}$, then:

   1. Let $j_1^{\ast }$ be the sequence $i_1^{\ast }[0\mathbf{:}N]$.

   2. Let $j_2^{\ast }$ be the sequence $i_2^{\ast }[0\mathbf{:}N]$.

8. Else:

   1. Let $j_1^{\ast }$ be the sequence $i_1^{\ast }[N\mathbf{:}N]$.

   2. Let $j_2^{\ast }$ be the sequence $i_2^{\ast }[N\mathbf{:}N]$.

9. Let $k_1^{\ast }$ be the result of computing ${\mathrm{extend}}_{|t_1|,|t_2|}^{\mathit{sx}}(j_1^{\ast })$.

10. Let $k_2^{\ast }$ be the result of computing ${\mathrm{extend}}_{|t_1|,|t_2|}^{\mathit{sx}}(j_2^{\ast })$.

11. Let $k^{\ast }$ be the result of computing ${\mathrm{imul}}_{t_2\mathsf{x}N}(k_1^{\ast },k_2^{\ast })$.

12. Let $c$ be the result of computing ${\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(k^{\ast })$.

13. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ onto the stack.

$$\begin{array}{r}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_2)t_2\mathsf{x}N\mathsf{.}\mathsf{extmul}\mathsf{\_}\mathit{half}\mathsf{\_}{t}_1\mathsf{x}M\mathrm{\_}\mathit{sx}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& i^{\ast }={\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)[\mathit{half}(0,N)\mathbf{:}N]\\ \wedge & j^{\ast }={\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)[\mathit{half}(0,N)\mathbf{:}N]\\ \wedge & c={\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}({\mathrm{imul}}_{t_2\mathsf{x}N}({\mathrm{extend}}_{|t_1|,|t_2|}^{\mathit{sx}}(i^{\ast }),{\mathrm{extend}}_{|t_1|,|t_2|}^{\mathit{sx}}(j^{\ast }))))\end{array}\end{array}$$

where:

$$\begin{array}{r}\begin{array}{lcl}\mathsf{low}(x,y)& =& x\\ \mathsf{high}(x,y)& =& y\end{array}\end{array}$$

$t_2\mathsf{x}N\mathsf{.}\mathsf{extadd}\mathsf{\_}\mathsf{pairwise}\mathrm{\_}{t}_1\mathsf{x}M\mathrm{\_}\mathit{sx}$

1. Assert: due to syntax, $N=M/2$.

2. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

3. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}{c}_1$ from the stack.

4. Let $i^{\ast }$ be the result of computing ${\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)$.

5. Let $(j_1{j}_2{)}^{\ast }$ be the result of computing ${\mathrm{extend}}_{|t_1|,|t_2|}^{\mathit{sx}}(i^{\ast })$.

6. Let $k^{\ast }$ be the result of computing ${\mathrm{iadd}}_N(j_1,j_2{)}^{\ast }$.

7. Let $c$ be the result of computing ${\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(k^{\ast })$.

8. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}{c}_1)t_2\mathsf{x}N\mathsf{.}\mathsf{extadd}\mathsf{\_}\mathsf{pairwise}\mathrm{\_}{t}_1\mathsf{x}M\mathrm{\_}\mathit{sx}& \hookrightarrow & (\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& (i_1{i}_2{)}^{\ast }={\mathrm{extend}}_{|t_1|,|t_2|}^{\mathit{sx}}({\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1))\\ \wedge & j^{\ast }={\mathrm{iadd}}_N(i_1,i_2{)}^{\ast }\\ \wedge & c={\mathrm{lanes}}_{t_2\mathsf{x}N}^{-1}(j^{\ast }))\end{array}\end{array}\end{array}$$

Parametric Instructions

$\mathsf{drop}$

1. Assert: due to validation, a value is on the top of the stack.

2. Pop the value $\mathit{val}$ from the stack.

$$\begin{array}{lcl}\mathit{val}\mathsf{drop}& \hookrightarrow & ϵ\end{array}$$

$\mathsf{select}(t^{\ast }{)}^{?}$

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}c$ from the stack.

3. Assert: due to validation, two more values (of the same value type) are on the top of the stack.

4. Pop the value ${\mathit{val}}_2$ from the stack.

5. Pop the value ${\mathit{val}}_1$ from the stack.

6. If $c$ is not $0$, then:

   1. Push the value ${\mathit{val}}_1$ back to the stack.

7. Else:

   1. Push the value ${\mathit{val}}_2$ back to the stack.

$$\begin{array}{r}\begin{array}{lcll}{\mathit{val}}_1{\mathit{val}}_2(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}c)(\mathsf{select}{t}^{?})& \hookrightarrow & {\mathit{val}}_1& (\text{if}c\ne 0)\\ {\mathit{val}}_1{\mathit{val}}_2(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{const}c)(\mathsf{select}{t}^{?})& \hookrightarrow & {\mathit{val}}_2& (\text{if}c=0)\end{array}\end{array}$$

Note

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

Variable Instructions

$\mathsf{local}\mathsf{.}\mathsf{get}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{locals}[x]$ exists.

3. Let $\mathit{val}$ be the value $F.\mathsf{locals}[x]$.

4. Push the value $\mathit{val}$ to the stack.

$$\begin{array}{r}\begin{array}{lcll}F;(\mathsf{local}\mathsf{.}\mathsf{get}x)& \hookrightarrow & F;\mathit{val}& (\text{if}F.\mathsf{locals}[x]=\mathit{val})\end{array}\end{array}$$

$\mathsf{local}\mathsf{.}\mathsf{set}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{locals}[x]$ exists.

3. Assert: due to validation, a value is on the top of the stack.

4. Pop the value $\mathit{val}$ from the stack.

5. Replace $F.\mathsf{locals}[x]$ with the value $\mathit{val}$.

$$\begin{array}{r}\begin{array}{lcll}F;\mathit{val}(\mathsf{local}\mathsf{.}\mathsf{set}x)& \hookrightarrow & F^{\prime };ϵ& (\text{if}{F}^{\prime }=F\text{with}\mathsf{locals}[x]=\mathit{val})\end{array}\end{array}$$

$\mathsf{local}\mathsf{.}\mathsf{tee}x$

1. Assert: due to validation, a value is on the top of the stack.

2. Pop the value $\mathit{val}$ from the stack.

3. Push the value $\mathit{val}$ to the stack.

4. Push the value $\mathit{val}$ to the stack.

5. Execute the instruction $\mathsf{local}\mathsf{.}\mathsf{set}x$.

$$\begin{array}{lcl}\mathit{val}(\mathsf{local}\mathsf{.}\mathsf{tee}x)& \hookrightarrow & \mathit{val}\mathit{val}(\mathsf{local}\mathsf{.}\mathsf{set}x)\end{array}$$

$\mathsf{global}\mathsf{.}\mathsf{get}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{globaladdrs}[x]$ exists.

3. Let $a$ be the global address $F.\mathsf{module}.\mathsf{globaladdrs}[x]$.

4. Assert: due to validation, $S.\mathsf{globals}[a]$ exists.

5. Let $\mathit{glob}$ be the global instance $S.\mathsf{globals}[a]$.

6. Let $\mathit{val}$ be the value $\mathit{glob}.\mathsf{value}$.

7. Push the value $\mathit{val}$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{global}\mathsf{.}\mathsf{get}x)& \hookrightarrow & S;F;\mathit{val}\end{array}\\ (\text{if}S.\mathsf{globals}[F.\mathsf{module}.\mathsf{globaladdrs}[x]].\mathsf{value}=\mathit{val})\end{array}\end{array}$$

$\mathsf{global}\mathsf{.}\mathsf{set}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{globaladdrs}[x]$ exists.

3. Let $a$ be the global address $F.\mathsf{module}.\mathsf{globaladdrs}[x]$.

4. Assert: due to validation, $S.\mathsf{globals}[a]$ exists.

5. Let $\mathit{glob}$ be the global instance $S.\mathsf{globals}[a]$.

6. Assert: due to validation, a value is on the top of the stack.

7. Pop the value $\mathit{val}$ from the stack.

8. Replace $\mathit{glob}.\mathsf{value}$ with the value $\mathit{val}$.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;\mathit{val}(\mathsf{global}\mathsf{.}\mathsf{set}x)& \hookrightarrow & S^{\prime };F;ϵ\end{array}\\ (\text{if}{S}^{\prime }=S\text{with}\mathsf{globals}[F.\mathsf{module}.\mathsf{globaladdrs}[x]].\mathsf{value}=\mathit{val})\end{array}\end{array}$$

Note

Validation ensures that the global is, in fact, marked as mutable.

Table Instructions

$\mathsf{table}\mathsf{.}\mathsf{get}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $a$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[a]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[a]$.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

8. If $i$ is not smaller than the length of $\mathit{tab}.\mathsf{elem}$, then:

   1. Trap.

9. Let $\mathit{val}$ be the value $\mathit{tab}.\mathsf{elem}[i]$.

10. Push the value $\mathit{val}$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{table}\mathsf{.}\mathsf{get}x)& \hookrightarrow & S;F;\mathit{val}\end{array}\\ (\text{if}S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}[i]=\mathit{val})\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{table}\mathsf{.}\mathsf{get}x)& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise})\end{array}\end{array}$$

$\mathsf{table}\mathsf{.}\mathsf{set}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $a$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[a]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[a]$.

6. Assert: due to validation, a reference value is on the top of the stack.

7. Pop the value $\mathit{val}$ from the stack.

8. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

9. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

10. If $i$ is not smaller than the length of $\mathit{tab}.\mathsf{elem}$, then:

    1. Trap.

11. Replace the element $\mathit{tab}.\mathsf{elem}[i]$ with $\mathit{val}$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)\mathit{val}(\mathsf{table}\mathsf{.}\mathsf{set}x)& \hookrightarrow & S^{\prime };F;ϵ\end{array}\\ (\text{if}{S}^{\prime }=S\text{with}\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}[i]=\mathit{val})\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)\mathit{val}(\mathsf{table}\mathsf{.}\mathsf{set}x)& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise})\end{array}\end{array}$$

$\mathsf{table}\mathsf{.}\mathsf{size}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $a$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[a]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[a]$.

6. Let $\mathit{sz}$ be the length of $\mathit{tab}.\mathsf{elem}$.

7. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz}$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{table}\mathsf{.}\mathsf{size}x)& \hookrightarrow & S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz})\end{array}\\ (\text{if}|S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}|=\mathit{sz})\end{array}\end{array}$$

$\mathsf{table}\mathsf{.}\mathsf{grow}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $a$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[a]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[a]$.

6. Let $\mathit{sz}$ be the length of $S.\mathsf{tables}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

8. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

9. Assert: due to validation, a reference value is on the top of the stack.

10. Pop the value $\mathit{val}$ from the stack.

11. Let $\mathit{err}$ be the $\mathit{i}\mathit{32}$ value $2^{32}-1$, for which ${\mathrm{signed}}_{32}(\mathit{err})$ is $-1$.

12. Either:

1. If growing $\mathit{tab}$ by $n$ entries with initialization value $\mathit{val}$ succeeds, then:

   1. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz}$ to the stack.

2. Else:

   1. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{err}$ to the stack.

13. Or:

1. push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{err}$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{grow}x)& \hookrightarrow & S^{\prime };F;(\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz})\end{array}\\ \begin{array}{rl}(\text{if}& F.\mathsf{module}.\mathsf{tableaddrs}[x]=a\\ \wedge & \mathit{sz}=|S.\mathsf{tables}[a].\mathsf{elem}|\\ \wedge & S^{\prime }=S\text{with}\mathsf{tables}[a]=\mathrm{growtable}(S.\mathsf{tables}[a],n,\mathit{val}))\end{array}\\ \begin{array}{lcl}S;F;\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{grow}x)& \hookrightarrow & S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}{\mathrm{signed}}_{32}^{-1}(-1))\end{array}\end{array}\end{array}$$

Note

The $\mathsf{table}\mathsf{.}\mathsf{grow}$ instruction is non-deterministic. It may either succeed, returning the old table size $\mathit{sz}$, or fail, returning $-1$. Failure must occur if the referenced table instance has a maximum size defined that would be exceeded. However, failure can occur in other cases as well. In practice, the choice depends on the resources available to the embedder.

$\mathsf{table}\mathsf{.}\mathsf{fill}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $\mathit{ta}$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[\mathit{ta}]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[\mathit{ta}]$.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

8. Assert: due to validation, a reference value is on the top of the stack.

9. Pop the value $\mathit{val}$ from the stack.

10. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

11. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

12. If $i+n$ is larger than the length of $\mathit{tab}.\mathsf{elem}$, then:

    1. Trap.

12. If $n$ is $0$, then:

    1. Return.

13. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ to the stack.

14. Push the value $\mathit{val}$ to the stack.

15. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{set}x$.

16. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(i+1)$ to the stack.

17. Push the value $\mathit{val}$ to the stack.

18. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(n-1)$ to the stack.

19. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{fill}x$.

$$\begin{array}{r}\begin{array}{l}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{fill}x)\hookrightarrow S;F;\mathsf{trap}\\ \begin{array}{rl}(\text{if}& i+n>|S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}|)\end{array}\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}0)(\mathsf{table}\mathsf{.}\mathsf{fill}x)\hookrightarrow S;F;ϵ\\ (\text{otherwise})\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)(\mathsf{table}\mathsf{.}\mathsf{fill}x)\hookrightarrow \\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}i)\mathit{val}(\mathsf{table}\mathsf{.}\mathsf{set}x)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}i+1)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{fill}x)\end{array}\\ (\text{otherwise})\end{array}\end{array}$$

$\mathsf{table}\mathsf{.}\mathsf{copy}xy$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let ${\mathit{ta}}_x$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[{\mathit{ta}}_x]$ exists.

5. Let ${\mathit{tab}}_x$ be the table instance $S.\mathsf{tables}[{\mathit{ta}}_x]$.

6. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[y]$ exists.

7. Let ${\mathit{ta}}_y$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[y]$.

8. Assert: due to validation, $S.\mathsf{tables}[{\mathit{ta}}_y]$ exists.

9. Let ${\mathit{tab}}_y$ be the table instance $S.\mathsf{tables}[{\mathit{ta}}_y]$.

10. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

11. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

12. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

13. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ from the stack.

14. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

15. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ from the stack.

16. If $s+n$ is larger than the length of ${\mathit{tab}}_y.\mathsf{elem}$ or $d+n$ is larger than the length of ${\mathit{tab}}_x.\mathsf{elem}$, then:

    1. Trap.

17. If $n=0$, then:

1. Return.

18. If $d\le s$, then:

1. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

2. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ to the stack.

3. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{get}y$.

4. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{set}x$.

5. Assert: due to the earlier check against the table size, $d+1<2^{32}$.

6. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+1)$ to the stack.

7. Assert: due to the earlier check against the table size, $s+1<2^{32}$.

8. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(s+1)$ to the stack.

19. Else:

1. Assert: due to the earlier check against the table size, $d+n-1<2^{32}$.

2. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+n-1)$ to the stack.

3. Assert: due to the earlier check against the table size, $s+n-1<2^{32}$.

4. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(s+n-1)$ to the stack.

3. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{get}y$.

6. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{set}x$.

7. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

8. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ to the stack.

20. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(n-1)$ to the stack.

21. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{copy}xy$.

$$\begin{array}{r}\\ \begin{array}{l}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{copy}xy)\hookrightarrow S;F;\mathsf{trap}\\ \begin{array}{rl}(\text{if}& s+n>|S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[y]].\mathsf{elem}|\\ \vee & d+n>|S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}|)\end{array}\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}0)(\mathsf{table}\mathsf{.}\mathsf{copy}xy)\hookrightarrow S;F;ϵ\\ (\text{otherwise})\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)(\mathsf{table}\mathsf{.}\mathsf{copy}xy)\hookrightarrow \\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{table}\mathsf{.}\mathsf{get}y)(\mathsf{table}\mathsf{.}\mathsf{set}x)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d+1)(\mathsf{i}\mathsf{32}.\mathsf{const}s+1)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{copy}xy)\end{array}\\ (\text{otherwise},\text{if}d\le s)\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)(\mathsf{table}\mathsf{.}\mathsf{copy}xy)\hookrightarrow \\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d+n)(\mathsf{i}\mathsf{32}.\mathsf{const}s+n)(\mathsf{table}\mathsf{.}\mathsf{get}y)(\mathsf{table}\mathsf{.}\mathsf{set}x)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{copy}xy)\end{array}\\ (\text{otherwise},\text{if}d>s)\end{array}\end{array}$$

$\mathsf{table}\mathsf{.}\mathsf{init}xy$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $\mathit{ta}$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[\mathit{ta}]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[\mathit{ta}]$.

6. Assert: due to validation, $F.\mathsf{module}.\mathsf{elemaddrs}[y]$ exists.

7. Let $\mathit{ea}$ be the element address $F.\mathsf{module}.\mathsf{elemaddrs}[y]$.

8. Assert: due to validation, $S.\mathsf{elems}[\mathit{ea}]$ exists.

9. Let $\mathit{elem}$ be the element instance $S.\mathsf{elems}[\mathit{ea}]$.

10. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

11. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

12. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

13. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ from the stack.

14. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

15. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ from the stack.

16. If $s+n$ is larger than the length of $\mathit{elem}.\mathsf{elem}$ or $d+n$ is larger than the length of $\mathit{tab}.\mathsf{elem}$, then:

    1. Trap.

17. If $n=0$, then:

    1. Return.

18. Let $\mathit{val}$ be the reference value $\mathit{elem}.\mathsf{elem}[s]$.

19. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

20. Push the value $\mathit{val}$ to the stack.

21. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{set}x$.

22. Assert: due to the earlier check against the table size, $d+1<2^{32}$.

23. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+1)$ to the stack.

24. Assert: due to the earlier check against the segment size, $s+1<2^{32}$.

25. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(s+1)$ to the stack.

26. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(n-1)$ to the stack.

27. Execute the instruction $\mathsf{table}\mathsf{.}\mathsf{init}xy$.

$$\begin{array}{r}\\ \begin{array}{l}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{init}xy)\hookrightarrow S;F;\mathsf{trap}\\ \begin{array}{rl}(\text{if}& s+n>|S.\mathsf{elems}[F.\mathsf{module}.\mathsf{elemaddrs}[y]].\mathsf{elem}|\\ \vee & d+n>|S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}|)\end{array}\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}0)(\mathsf{table}\mathsf{.}\mathsf{init}xy)\hookrightarrow S;F;ϵ\\ (\text{otherwise})\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)(\mathsf{table}\mathsf{.}\mathsf{init}xy)\hookrightarrow \\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d)\mathit{val}(\mathsf{table}\mathsf{.}\mathsf{set}x)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d+1)(\mathsf{i}\mathsf{32}.\mathsf{const}s+1)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{table}\mathsf{.}\mathsf{init}xy)\end{array}\\ (\text{otherwise},\text{if}\mathit{val}=S.\mathsf{elems}[F.\mathsf{module}.\mathsf{elemaddrs}[y]].\mathsf{elem}[s])\end{array}\end{array}$$

$\mathsf{elem}\mathsf{.}\mathsf{drop}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{elemaddrs}[x]$ exists.

3. Let $a$ be the element address $F.\mathsf{module}.\mathsf{elemaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{elems}[a]$ exists.

5. Replace $S.\mathsf{elems}[a].\mathsf{elem}$ with $ϵ$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{elem}\mathsf{.}\mathsf{drop}x)& \hookrightarrow & S^{\prime };F;ϵ\end{array}\\ (\text{if}{S}^{\prime }=S\text{with}\mathsf{elems}[F.\mathsf{module}.\mathsf{elemaddrs}[x]].\mathsf{elem}=ϵ)\end{array}\end{array}$$

Memory Instructions

Note

The alignment $\mathit{memarg}.\mathsf{align}$ in load and store instructions does not affect the semantics. It is an indication that the offset $\mathit{ea}$ at which the memory is accessed is intended to satisfy the property $\mathit{ea}\mathrm{mod}{2}^{\mathit{memarg}.\mathsf{align}}=0$. A WebAssembly implementation can use this hint to optimize for the intended use. Unaligned access violating that property is still allowed and must succeed regardless of the annotation. However, it may be substantially slower on some hardware.

$t\mathsf{.}\mathsf{load}\mathit{memarg}$ and $t\mathsf{.}\mathsf{load}N\mathsf{\_}\mathit{sx}\mathit{memarg}$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

8. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

9. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

10. If $N$ is not part of the instruction, then:

1. Let $N$ be the bit width $|t|$ of number type $t$.

11. If both $\mathit{ord}$ is $\mathsf{seqcst}$ and $\mathit{ea}$ modulo $N/8$ is not equal to $0$, then:

1. Trap.

12. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Let $b^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$.

13. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Let ${\mathit{notears}}^{?}$ be $\mathrm{tearing}(t,N,\mathit{ea})$.

    4. Perform the action $({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast }{\mathit{notears}}^{?})$ to read $N/8$ bytes $b^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

14. Let $c_N$ be the integer for which ${\mathrm{bytes}}_{\mathit{i}N}(n)=b^{\ast }$.

15. Let $c$ be the result of computing ${\mathrm{extend}}_{N,|t|}^{\mathit{sx}}(c_N)$.

16. Push the value $t.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{load}(N\mathsf{\_}\mathit{sx}{)}^{?}\mathit{memarg})& \hookrightarrow & S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & (\mathit{ord}=\mathsf{unord}\vee \mathit{ea}\mathrm{mod}N/8=0)\\ \wedge & c={\mathrm{extend}}_{N,|t|}^{\mathit{sx}}({\mathrm{bytes}}_{\mathit{i}N}^{-1}(\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8])))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{load}(N\mathsf{\_}\mathit{sx}{)}^{?}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{load}(N\mathsf{\_}\mathit{sx})?\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast }{\mathit{notears}}^{?})}& S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & (\mathit{ord}=\mathsf{unord}\vee \mathit{ea}\mathrm{mod}N/8=0)\\ \wedge & c={\mathrm{extend}}_{N,|t|}^{\mathit{sx}}({\mathrm{bytes}}_{\mathit{i}N}^{-1}(b^{\ast })))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{load}(N\mathsf{\_}\mathit{sx}{)}^{?}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n\vee \mathit{ord}=\mathsf{seqcst}\wedge \mathit{ea}\mathrm{mod}N/8\ne 0))\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & N=|t|\text{if}N\text{not present}\\ \wedge & \mathit{sx}=\mathsf{u}\text{if}\mathit{sx}\text{not present}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset}\\ \wedge & {\mathit{notears}}^{?}=\mathrm{tearing}(t,N,\mathit{ea}))\end{array}\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}M\mathsf{x}N\mathrm{\_}\mathit{sx}\mathit{memarg}$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

8. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

9. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

10. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

1. If $\mathit{ea}+M\cdot N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

   1. Trap.

2. Let $b^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}M\cdot N/8]$.

11. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+M\cdot N/8$ is larger than $n$, then:

       1. Trap.

    3. Perform the action $({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })$ to read $M\cdot N/8$ bytes $b^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

12. Let $m_k$ be the integer for which ${\mathrm{bytes}}_{\mathit{i}M}(m_k)=b^{\ast }[k\cdot M/8\mathbf{:}M/8]$.

13. Let $W$ be the integer $M\cdot 2$.

14. Let $n_k$ be the result of computing ${\mathrm{extend}}_{M,W}^{\mathit{sx}}(m_k)$.

15. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}W\mathsf{x}N}^{-1}(n_0\dots n_{N-1})$.

16. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}M\mathsf{x}N\mathrm{\_}\mathit{sx}\mathit{memarg})& \hookrightarrow & S;F;(\mathsf{v}\mathsf{128}.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+M\cdot N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & {\mathrm{bytes}}_{\mathit{i}M}(m_k)=\mathit{mem}.\mathsf{data}[\mathit{ea}+k\cdot M/8\mathbf{:}M/8]\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}W\mathsf{x}N}^{-1}({\mathrm{extend}}_{M,W}^{\mathit{sx}}(m_0)\dots {\mathrm{extend}}_{M,W}^{\mathit{sx}}(m_{N-1})))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}M\mathsf{x}N\mathsf{\_}\mathit{sx}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}M\mathsf{x}N\mathrm{\_}\mathit{sx}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}& S;F;(\mathsf{v}\mathsf{128}.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+M\cdot N/8\le n\\ \wedge & {\mathrm{bytes}}_{\mathit{i}M}(m_k)=b^{\ast }[k\cdot M/8\mathbf{:}M/8]\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}W\mathsf{x}N}^{-1}({\mathrm{extend}}_{M,W}^{\mathit{sx}}(m_0)\dots {\mathrm{extend}}_{M,W}^{\mathit{sx}}(m_{N-1})))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}M\mathsf{x}N\mathrm{\_}\mathit{sx}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+M\cdot N/8>n)\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset}\\ \wedge & W=M\cdot 2)\end{array}\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{splat}\mathit{memarg}$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

8. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

9. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

10. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

   1. Trap.

2. Let $b^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$.

11. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Perform the action $({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })$ to read $N/8$ bytes $b^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

12. Let $n$ be the integer for which ${\mathrm{bytes}}_{\mathit{i}N}(n)=b^{\ast }$.

13. Let $L$ be the integer $128/N$.

14. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}^{-1}(n^L)$.

15. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{splat}\mathit{memarg})& \hookrightarrow & S;F;(\mathsf{v}\mathsf{128}.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & {\mathrm{bytes}}_{\mathit{i}N}(n)=\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}^{-1}(n^L))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}N\mathsf{\_}\mathsf{splat}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{splat}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}& S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & {\mathrm{bytes}}_{\mathit{i}N}(n)=b^{\ast }\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}^{-1}(n^L))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{splat}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n)\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset})\end{array}\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{zero}\mathit{memarg}$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

8. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

9. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

10. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

   1. Trap.

2. Let $b^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$.

11. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Perform the action $({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })$ to read $N/8$ bytes $b^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

12. Let $n$ be the integer for which ${\mathrm{bytes}}_{\mathit{i}N}(n)=b^{\ast }$.

13. Let $c$ be the result of computing ${\mathrm{extend}}_{N,128}^{\mathsf{u}}(n)$.

14. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{zero}\mathit{memarg})& \hookrightarrow & S;F;(\mathsf{v}\mathsf{128}.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & {\mathrm{bytes}}_{\mathit{i}N}(n)=\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]\\ \wedge & c={\mathrm{extend}}_{N,128}^{\mathsf{u}}(n))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}N\mathsf{\_}\mathsf{zero}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}N\mathsf{\_}\mathsf{zero}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}& S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & {\mathrm{bytes}}_{\mathit{i}N}(n)=b^{\ast }\\ \wedge & c={\mathrm{extend}}_{N,128}^{\mathsf{u}}(n))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{load}N\mathsf{\_}\mathsf{zero}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n)\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset})\end{array}\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

8. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}v$ from the stack.

9. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

10. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

11. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

12. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Let $b^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$.

13. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Perform the action $({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })$ to read $N/8$ bytes $b^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

14. Let $r$ be the constant for which ${\mathrm{bytes}}_{\mathit{i}N}(r)=b^{\ast }$.

15. Let $L$ be $128/N$.

16. Let $j^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(v)$.

17. Let $c$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(j^{\ast }\text{with}[x]=r)$.

18. Push the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}v)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& \hookrightarrow & S;F;(\mathsf{v}\mathsf{128}.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & {\mathrm{bytes}}_{\mathit{i}N}(n)=\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}^{-1}({\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(v)\text{with}[x]=r))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}v)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}v)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}& S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & {\mathrm{bytes}}_{\mathit{i}N}(n)=b^{\ast }\\ \wedge & c={\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}^{-1}({\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(v)\text{with}[x]=r))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}v)(\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{load}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n)\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset})\\ \wedge & L=128/N\end{array}\end{array}\end{array}$$

$t\mathsf{.}\mathsf{store}\mathit{memarg}$ and $t\mathsf{.}\mathsf{store}N\mathit{memarg}$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $t$ is on the top of the stack.

8. Pop the value $t.\mathsf{const}c$ from the stack.

9. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

10. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

11. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

12. If $N$ is not part of the instruction, then:

    1. Let $N$ be the bit width $|t|$ of number type $t$.

13. If both $\mathit{ord}$ is $\mathsf{seqcst}$ and $\mathit{ea}$ modulo $N/8$ is not equal to $0$, then:

1. Trap.

15. Let $n$ be the result of computing ${\mathrm{wrap}}_{|t|,N}(c)$.

16. Let $b^{\ast }$ be the byte sequence ${\mathrm{bytes}}_{\mathit{i}N}(n)$.

17. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Replace the bytes $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$ with $b^{\ast }$.

18. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Let ${\mathit{notears}}^{?}$ be $\mathrm{tearing}(t,N,\mathit{ea})$.

    4. Perform the action $({\mathsf{wr}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast }{\mathit{notears}}^{?})$ to write the bytes $b^{\ast }$ to data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}c)(t.\mathsf{store}{N}^{?}\mathit{memarg})& \hookrightarrow & S^{\prime };F;ϵ\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & (\mathit{ord}=\mathsf{unord}\vee \mathit{ea}\mathrm{mod}N/8=0)\\ \wedge & S^{\prime }=S\text{with}\mathsf{mems}[F.\mathsf{module}.\mathsf{memaddrs}[0]].\mathsf{data}[\mathit{ea}\mathbf{:}N/8]={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{wrap}}_{|t|,N}(c)))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}c)(t.\mathsf{store}{N}^{?}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}c)(t.\mathsf{store}{N}^{?}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{wr}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })\mathit{notears}}& S;F;ϵ\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & (\mathit{ord}=\mathsf{unord}\vee \mathit{ea}\mathrm{mod}N/8=0)\\ \wedge & b^{\ast }={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{wrap}}_{|t|,N}(c)))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}c)(t.\mathsf{store}{N}^{?}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n\vee \mathit{ord}=\mathsf{seqcst}\wedge \mathit{ea}\mathrm{mod}N/8\ne 0))\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & N=|t|\text{if}N\text{not present}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset}\\ \wedge & {\mathit{notears}}^{?}=\mathrm{tearing}(t,N,\mathit{ea}))\end{array}\end{array}\end{array}$$

$\mathsf{v}\mathsf{128}\mathsf{.}\mathsf{store}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x$

1. Let $\mathit{ord}$ be $\mathsf{unord}$.

2. Let $F$ be the current frame.

3. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

4. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

5. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

6. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

7. Assert: due to validation, a value of value type $\mathsf{v}\mathsf{128}$ is on the top of the stack.

8. Pop the value $\mathsf{v}\mathsf{128}.\mathsf{const}c$ from the stack.

9. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

10. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

11. Let $\mathit{ea}$ be the integer $i+\mathit{memarg}.\mathsf{offset}$.

12. Let $L$ be $128/N$.

13. Let $j^{\ast }$ be the result of computing ${\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(c)$.

14. Let $b^{\ast }$ be the result of computing ${\mathrm{bytes}}_{\mathit{i}N}(j^{\ast }[x])$.

15. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Replace the bytes $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$ with $b^{\ast }$.

16. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Perform the action $({\mathsf{wr}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })$ to write the bytes $b^{\ast }$ to data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}c)(\mathsf{v}\mathsf{128}.\mathsf{store}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& \hookrightarrow & S^{\prime };F;ϵ\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & S^{\prime }=S\text{with}\mathsf{mems}[F.\mathsf{module}.\mathsf{memaddrs}[0]].\mathsf{data}[\mathit{ea}\mathbf{:}N/8]={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(c)[x]))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}c)(\mathsf{v}\mathsf{128}.\mathsf{store}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise},\text{if}\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}c)(\mathsf{v}\mathsf{128}.\mathsf{store}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{wr}}_{\mathit{ord}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}& S;F;ϵ\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & b^{\ast }={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{lanes}}_{\mathsf{i}N\mathsf{x}L}(c)[x]))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{v}\mathsf{128}.\mathsf{const}c)(\mathsf{v}\mathsf{128}.\mathsf{store}N\mathsf{\_}\mathsf{lane}\mathit{memarg}x)& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n\vee \mathit{ord}=\mathsf{seqcst}\wedge \mathit{ea}\mathrm{mod}N/8\ne 0))\end{array}\\ \\ \begin{array}{rl}(\text{where}& \mathit{ord}=\mathsf{unord}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset}\\ \wedge & L=128/N)\end{array}\end{array}\end{array}$$

$\mathsf{memory}\mathsf{.}\mathsf{size}$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

3. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

4. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

5. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

6. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

   1. Let $n$ be the length of $\mathit{mem}.\mathsf{data}$.

7. Else:

   1. Perform the action $({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

8. Let $\mathit{sz}$ be $n$ divided by the page size.

9. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz}$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;\mathsf{memory}\mathsf{.}\mathsf{size}& \hookrightarrow & S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz})\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & |\mathit{mem}.\mathsf{data}|=\mathit{sz}\cdot 64\mathrm{Ki}\end{array}\\ \\ \begin{array}{lcl}S;F;\mathsf{memory}\mathsf{.}\mathsf{size}& {\hookrightarrow }^{({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{len}n)}& S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz})\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & n=\mathit{sz}\cdot 64\mathrm{Ki})\end{array}\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a])\end{array}\end{array}\end{array}$$

$\mathsf{memory}\mathsf{.}\mathsf{grow}$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

3. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

4. Assert: due to validation, $S.\mathsf{mems}[a]$ exists.

5. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

8. Let $\mathit{err}$ be the $\mathit{i}\mathit{32}$ value $2^{32}-1$, for which ${\mathrm{signed}}_{32}(\mathit{err})$ is $-1$.

9. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

   2. Let $\mathit{sz}$ be the length of $S.\mathsf{mems}[a]$ divided by the page size.

   3. Either, try growing $\mathit{mem}$ by $n$ pages:

      1. If it succeeds, push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz}$ to the stack.

      2. Else, push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{err}$ to the stack.

   4. Or, push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{err}$ to the stack.

10. Else:

1. Either successfully grow the memory:

   1. Let $k$ be $n$ multiplied by the page size.

   2. Perform the action $(\mathsf{rmw}a.\mathsf{len}l(l+k))$ to update the current length $l$ of the shared memory instance at memory address $a$ to $l+k$.

   3. Perform the action $(\mathsf{wr}a.\mathsf{data}[l](0{)}^k)$ to append $k$ zero bytes to the end of the shared memory instance at memory address $a$.

   4. Let $\mathit{sz}$ be $l$ divided by the page size.

   5. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz}$ to the stack.

2. Or indicate failure:

   1. Perform the action $({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{len}l)$ to read the length $l$ of the shared memory instance at memory address $a$.

   2. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{err}$ to the stack.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{grow}& \hookrightarrow & S^{\prime };F;(\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz})\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{sz}=|\mathit{mem}.\mathsf{data}|/64\mathrm{Ki}\\ \wedge & S^{\prime }=S\text{with}\mathsf{mems}[a]=\mathrm{growmem}(S.\mathsf{mems}[a],n))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{grow}& \hookrightarrow & S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}{\mathrm{signed}}_{32}^{-1}(-1))\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\end{array}\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{grow}& {\hookrightarrow }^{(\mathsf{rmw}a.\mathsf{len}l(l+k))(\mathsf{wr}a.\mathsf{data}[l](0{)}^k)}& S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}\mathit{sz})\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{sz}=l/64\mathrm{Ki}\\ \wedge & n=k/64\mathrm{Ki})\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{grow}& {\hookrightarrow }^{({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{len}n)}& S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}-1)\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared})\end{array}\end{array}\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a])\end{array}\end{array}\end{array}$$

Note

The $\mathsf{memory}\mathsf{.}\mathsf{grow}$ instruction is non-deterministic, even on unshared memories. It may either succeed, returning the old memory size $\mathit{sz}$, or fail, returning $-1$. Failure must occur if the referenced memory instance has a maximum size defined that would be exceeded. However, failure can occur in other cases as well. In practice, the choice depends on the resources available to the embedder.

$\mathsf{memory}\mathsf{.}\mathsf{fill}$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

3. Let $\mathit{ma}$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

4. Assert: due to validation, $S.\mathsf{mems}[\mathit{ma}]$ exists.

5. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[\mathit{ma}]$.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

8. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

9. Pop the value $\mathit{val}$ from the stack.

10. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

11. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ from the stack.

12. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $d+n$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

13. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}l)$ to read the length $l$ of the shared memory instance at memory address $a$.

    2. If $d+n$ is larger than $l$, then:

       1. Trap.

14. If $n=0$, then:

    1. Return.

15. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

16. Push the value $\mathit{val}$ to the stack.

17. Execute the instruction $\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\}$.

18. Assert: due to the earlier check against the memory size, $d+1<2^{32}$.

19. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+1)$ to the stack.

20. Push the value $\mathit{val}$ to the stack.

21. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(n-1)$ to the stack.

22. Execute the instruction $\mathsf{memory}\mathsf{.}\mathsf{fill}$.

$$\begin{array}{r}\\ \begin{array}{l}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{fill}{\hookrightarrow }^{\mathit{act}}S;F;\mathsf{trap}\\ \begin{array}{rl}(\text{if}& d+n>l\end{array}\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}0)\mathsf{memory}\mathsf{.}\mathsf{fill}{\hookrightarrow }^{\mathit{act}}S;F;ϵ\\ (\text{otherwise})\\ \\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)\mathsf{memory}\mathsf{.}\mathsf{fill}{\hookrightarrow }^{\mathit{act}}\\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d)\mathit{val}(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\})\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d+1)\mathit{val}(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{fill}\end{array}\\ (\text{otherwise})\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & ((\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\wedge l=|\mathit{mem}.\mathsf{data}|\wedge \mathit{act}=ϵ)\vee (\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\wedge \mathit{act}=(\mathsf{rd}a.\mathsf{len}l)))\end{array}\end{array}\end{array}$$

$\mathsf{memory}\mathsf{.}\mathsf{copy}$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

3. Let $\mathit{ma}$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

4. Assert: due to validation, $S.\mathsf{mems}[\mathit{ma}]$ exists.

5. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[\mathit{ma}]$.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

8. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

9. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ from the stack.

10. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

11. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ from the stack.

12. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $s+n$ is larger than the length of $\mathit{mem}.\mathsf{data}$ or $d+n$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

13. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}l)$ to read the length $l$ of the shared memory instance at memory address $a$.

    1. If $s+n$ is larger than $l$ or $d+n$ is larger than $l$, then:

       1. Trap.

14. If $n=0$, then:

1. Return.

15. If $d\le s$, then:

1. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

2. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ to the stack.

3. Execute the instruction $\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{load}\mathsf{8}\mathsf{\_}\mathsf{u}\{\mathsf{offset}0,\mathsf{align}0\}$.

4. Execute the instruction $\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\}$.

5. Assert: due to the earlier check against the memory size, $d+1<2^{32}$.

6. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+1)$ to the stack.

7. Assert: due to the earlier check against the memory size, $s+1<2^{32}$.

8. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(s+1)$ to the stack.

16. Else:

1. Assert: due to the earlier check against the memory size, $d+n-1<2^{32}$.

2. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+n-1)$ to the stack.

3. Assert: due to the earlier check against the memory size, $s+n-1<2^{32}$.

4. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(s+n-1)$ to the stack.

5. Execute the instruction $\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{load}\mathsf{8}\mathsf{\_}\mathsf{u}\{\mathsf{offset}0,\mathsf{align}0\}$.

6. Execute the instruction $\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\}$.

7. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

8. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ to the stack.

17. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(n-1)$ to the stack.

18. Execute the instruction $\mathsf{memory}\mathsf{.}\mathsf{copy}$.

$$\begin{array}{r}\\ \begin{array}{l}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{copy}{\hookrightarrow }^{\mathit{act}}S;F;\mathsf{trap}\\ \begin{array}{rl}(\text{if}& (s+n>l\\ \vee & d+n>l))\end{array}\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}0)\mathsf{memory}\mathsf{.}\mathsf{copy}\hookrightarrow S;F;ϵ\\ (\text{otherwise})\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)\mathsf{memory}\mathsf{.}\mathsf{copy}{\hookrightarrow }^{\mathit{act}}\\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{load}\mathsf{8}\mathsf{\_}\mathsf{u}\{\mathsf{offset}0,\mathsf{align}0\})\\ (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\})\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d+1)(\mathsf{i}\mathsf{32}.\mathsf{const}s+1)(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{copy}\end{array}\\ (\text{otherwise})\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)\mathsf{memory}\mathsf{.}\mathsf{copy}{\hookrightarrow }^{\mathit{act}}\\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d+n)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}s+n)(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{load}\mathsf{8}\mathsf{\_}\mathsf{u}\{\mathsf{offset}0,\mathsf{align}0\})\\ (\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\})\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n)\mathsf{memory}\mathsf{.}\mathsf{copy}\end{array}\\ (\text{otherwise})\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & ((\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\wedge l=|\mathit{mem}.\mathsf{data}|\wedge \mathit{act}=ϵ)\vee (\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\wedge \mathit{act}=(\mathsf{rd}a.\mathsf{len}l)))\end{array}\end{array}\end{array}$$

$\mathsf{memory}\mathsf{.}\mathsf{init}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

3. Let $\mathit{ma}$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

4. Assert: due to validation, $S.\mathsf{mems}[\mathit{ma}]$ exists.

5. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[\mathit{ma}]$.

6. Assert: due to validation, $F.\mathsf{module}.\mathsf{dataaddrs}[x]$ exists.

7. Let $\mathit{da}$ be the data address $F.\mathsf{module}.\mathsf{dataaddrs}[x]$.

8. Assert: due to validation, $S.\mathsf{datas}[\mathit{da}]$ exists.

9. Let $\mathit{data}$ be the data instance $S.\mathsf{datas}[\mathit{da}]$.

10. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

11. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}n$ from the stack.

12. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

13. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}s$ from the stack.

14. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

15. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ from the stack.

16. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $s+n$ is larger than the length of $\mathit{data}.\mathsf{data}$ or $d+n$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

17. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}l)$ to read the length $l$ of the shared memory instance at memory address $a$.

    1. If $s+n$ is larger than the length of $\mathit{data}.\mathsf{data}$ or $d+n$ is larger than $l$, then:

       1. Trap.

18. If $n=0$, then:

    1. Return.

19. Let $b$ be the byte $\mathit{data}.\mathsf{data}[s]$.

20. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}d$ to the stack.

21. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}b$ to the stack.

22. Execute the instruction $\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\}$.

23. Assert: due to the earlier check against the memory size, $d+1<2^{32}$.

24. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(d+1)$ to the stack.

25. Assert: due to the earlier check against the memory size, $s+1<2^{32}$.

26. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(s+1)$ to the stack.

27. Push the value $\mathsf{i}\mathsf{32}.\mathsf{const}(n-1)$ to the stack.

28. Execute the instruction $\mathsf{memory}\mathsf{.}\mathsf{init}x$.

$$\begin{array}{r}\\ \begin{array}{l}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{memory}\mathsf{.}\mathsf{init}x){\hookrightarrow }^{\mathit{act}}S;F;\mathsf{trap}\\ \begin{array}{rl}(\text{if}& (s+n>|S.\mathsf{datas}[F.\mathsf{module}.\mathsf{dataaddrs}[x]].\mathsf{data}|\\ \vee & d+n>l))\end{array}\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}0)(\mathsf{memory}\mathsf{.}\mathsf{init}x){\hookrightarrow }^{\mathit{act}}S;F;ϵ\\ (\text{otherwise})\\ S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}s)(\mathsf{i}\mathsf{32}.\mathsf{const}n+1)(\mathsf{memory}\mathsf{.}\mathsf{init}x){\hookrightarrow }^{\mathit{act}}\\ S;F;\begin{array}{c}(\mathsf{i}\mathsf{32}.\mathsf{const}d)(\mathsf{i}\mathsf{32}.\mathsf{const}b)(\mathsf{i}\mathsf{32}\mathsf{.}\mathsf{store}\mathsf{8}\{\mathsf{offset}0,\mathsf{align}0\})\\ (\mathsf{i}\mathsf{32}.\mathsf{const}d+1)(\mathsf{i}\mathsf{32}.\mathsf{const}s+1)(\mathsf{i}\mathsf{32}.\mathsf{const}n)(\mathsf{memory}\mathsf{.}\mathsf{init}x)\end{array}\\ (\text{otherwise},\text{if}b=S.\mathsf{datas}[F.\mathsf{module}.\mathsf{dataaddrs}[x]].\mathsf{data}[s])\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & ((\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\wedge l=|\mathit{mem}.\mathsf{data}|\wedge \mathit{act}=ϵ)\vee (\mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\wedge \mathit{act}=(\mathsf{rd}a.\mathsf{len}l)))\end{array}\end{array}\end{array}$$

$\mathsf{data}\mathsf{.}\mathsf{drop}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{dataaddrs}[x]$ exists.

3. Let $a$ be the data address $F.\mathsf{module}.\mathsf{dataaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{datas}[a]$ exists.

5. Replace $S.\mathsf{datas}[a]$ with the data instance $\{\mathsf{data}ϵ\}$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{data}\mathsf{.}\mathsf{drop}x)& \hookrightarrow & S^{\prime };F;ϵ\end{array}\\ (\text{if}{S}^{\prime }=S\text{with}\mathsf{datas}[F.\mathsf{module}.\mathsf{dataaddrs}[x]]=\{\mathsf{data}ϵ\})\end{array}\end{array}$$

Atomic Memory Instructions

$t\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{load}(N\mathsf{\_}\mathsf{u}{)}^{?}\mathit{memarg}$

The rules are identical to non-atomic loads, except that $\mathit{ord}=\mathsf{seqcst}$.

$t\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{store}{N}^{?}\mathit{memarg}$

The rules are identical to non-atomic stores, except that $\mathit{ord}=\mathsf{seqcst}$.

$t\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}\mathsf{.}\mathit{atop}\mathit{memarg}$

1. If $N$ is not part of the instruction, then:

   1. Let $N$ be the bit width $|t|$ of value type $t$.

3. Assert: due to validation, a value of value type $t$ is on the top of the stack.

4. Pop the value $t.\mathsf{const}{c}_2$ from the stack.

5. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

6. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

7. Let $\mathit{ea}$ be $i+\mathit{memarg}.\mathsf{offset}$.

8. If $\mathit{ea}$ modulo $N/8$ is not equal to $0$, then:

   1. Trap.

9. Let $F$ be the current frame.

10. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

11. Let $\mathit{a}$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

12. Assert: due to validation, $S.\mathsf{mems}[\mathit{a}]$ exists.

13. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[\mathit{a}]$.

14. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Let $b_{\mathrm{r}}^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$.

13. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Let $b_{\mathrm{r}}^{\ast }$ be chosen to represent $N/8$ bytes of memory at location $\mathit{ea}$ of $\mathit{mem}$.

14. Let $c_{\mathrm{r}}$ be the integer for which ${\mathrm{bytes}}_{\mathit{i}N}(n)=b_{\mathrm{r}}^{\ast }$.

15. Let $c_1$ be the result of computing ${\mathrm{extend}}_{N,|t|}^{\mathsf{u}}(c_{\mathrm{r}})$.

16. Let $c$ be the result of computing ${\mathit{atop}}_t(c_1,c_2)$.

17. Let $c_{\mathrm{w}}$ be the result of computing ${\mathrm{wrap}}_{|t|,N}(c)$.

18. Let $b_{\mathrm{w}}^{\ast }$ be the byte sequence ${\mathrm{bytes}}_{\mathit{i}N}(c_{\mathrm{w}})$.

19. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. Replace the bytes $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$ with $b_{\mathrm{w}}^{\ast }$.

10. Else:

    1. Perform the atomic action $({\mathsf{rmw}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b_{\mathrm{r}}^{\ast }{b}_{\mathrm{w}}^{\ast })$ to read $N/8$ bytes $b_{\mathrm{r}}^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$ and replace them with bytes $b_{\mathrm{w}}^{\ast }$.

20. Push the value $t.\mathsf{const}c$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathit{atop}\mathit{memarg})& \hookrightarrow & S^{\prime };F;(t.\mathsf{const}{c}_1)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & c_1={\mathrm{extend}}_{N,|t|}^{\mathsf{u}}({\mathrm{bytes}}_{\mathit{i}N}^{-1}(\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]))\\ \wedge & S^{\prime }=S\text{with}\mathsf{mems}[a].\mathsf{data}[\mathit{ea}\mathbf{:}N/8]={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{wrap}}_{|t|,N}({\mathit{atop}}_t(c_1,c_2))))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}k)(t.\mathsf{const}c)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathit{atop}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8>|\mathit{mem}.\mathsf{data}|\vee \mathit{ea}\mathrm{mod}N/8\ne 0)\end{array}\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathit{atop}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)(\mathsf{rmw}a.\mathsf{data}[\mathit{ea}]b_{\mathrm{r}}^{\ast }{b}_{\mathrm{w}}^{\ast })}& S;F;(t.\mathsf{const}{c}_1)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & c_1={\mathrm{extend}}_{N,|t|}^{\mathsf{u}}({\mathrm{bytes}}_{\mathit{i}N}^{-1}(b_{\mathrm{r}}^{\ast }))\\ \wedge & b_{\mathrm{w}}^{\ast }={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{wrap}}_{|t|,N}({\mathit{atop}}_t(c_1,c_2))))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}k)(t.\mathsf{const}c)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathit{atop}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8>n\vee \mathit{ea}\mathrm{mod}N/8\ne 0)\end{array}\\ \\ \begin{array}{rl}(\text{where}& N=|t|\text{if}N\text{not present}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset})\end{array}\end{array}\end{array}$$

$t\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}\mathsf{.}\mathsf{cmpxchg}\mathit{memarg}$

1. If $N$ is not part of the instruction, then:

   1. Let $N$ be the bit width $|t|$ of value type $t$.

3. Assert: due to validation, two values of value type $t$ are on the top of the stack.

4. Pop the value $t.\mathsf{const}{c}_3$ from the stack.

5. Pop the value $t.\mathsf{const}{c}_2$ from the stack.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

8. Let $\mathit{ea}$ be $i+\mathit{memarg}.\mathsf{offset}$.

9. If $\mathit{ea}$ modulo $N/8$ is not equal to $0$, then:

   1. Trap.

10. Let $F$ be the current frame.

11. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

12. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

13. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

14. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Let $b_{\mathrm{r}}^{\ast }$ be the byte sequence $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$.

15. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Let $b_{\mathrm{r}}^{\ast }$ be chosen to represent $N/8$ bytes of memory at location $\mathit{ea}$ of $\mathit{mem}$.

16. Let $c_{\mathrm{r}}$ be the integer for which ${\mathrm{bytes}}_{\mathit{i}N}(n)=b_{\mathrm{r}}^{\ast }$.

17. Let $c_{\mathrm{ex}}$ be the result of computing ${\mathrm{wrap}}_{|t|,N}(c_2)$.

18. If $c_{\mathrm{r}}$ equals $c_{\mathrm{ex}}$, then:

    1. Let $c_{\mathrm{w}}$ be the result of computing ${\mathrm{wrap}}_{|t|,N}(c_3)$.

    2. Let $b_{\mathrm{w}}^{\ast }$ be the byte sequence ${\mathrm{bytes}}_{\mathit{i}N}(c_{\mathrm{w}})$.

    3. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

       1. Replace the bytes $\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8]$ with $b_{\mathrm{w}}^{\ast }$.

    4. Else:

       1. Perform the atomic action $({\mathsf{rmw}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b_{\mathrm{r}}^{\ast }{b}_{\mathrm{w}}^{\ast })$ to read $N/8$ bytes $b_{\mathrm{r}}^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$ and replace them with bytes $b_{\mathrm{w}}^{\ast }$.

19. Else:

    1. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{shared}$, then:

       1. Perform the action $({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b_{\mathrm{r}}^{\ast })$ to read $N/8$ bytes $b_{\mathrm{r}}^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

20. Let $c_1$ be the result of computing ${\mathrm{extend}}_{N,|t|}^{\mathsf{u}}(c_{\mathrm{r}})$.

21. Push the value $t.\mathsf{const}{c}_1$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{const}{c}_3)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathsf{cmpxchg}\mathit{memarg})& \hookrightarrow & S^{\prime };F;(t.\mathsf{const}({\mathrm{extend}}_{N,|t|}^{\mathsf{u}}(c_{\mathrm{r}})))\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & c_{\mathrm{r}}={\mathrm{bytes}}_{\mathit{i}N}^{-1}(\mathit{mem}.\mathsf{data}[\mathit{ea}\mathbf{:}N/8])\\ \wedge & c_{\mathrm{ex}}={\mathrm{wrap}}_{|t|,N}(c_2)\\ \wedge & ((c_{\mathrm{r}}=c_{\mathrm{ex}}\wedge c={\mathrm{wrap}}_{|t|,N}(c_3))\vee (c_{\mathrm{r}}\ne c_{\mathrm{ex}}\wedge c=c_{\mathrm{r}}))\\ \wedge & S^{\prime }=S\text{with}\mathsf{mems}[a].\mathsf{data}[\mathit{ea}\mathbf{:}N/8]={\mathrm{bytes}}_{\mathit{i}N}(c))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{const}{c}_3)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathsf{cmpxchg}\mathit{memarg})& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8>|\mathit{mem}.\mathsf{data}|\vee \mathit{ea}\mathrm{mod}N/8\ne 0)\end{array}\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{const}{c}_3)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathsf{cmpxchg}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)(\mathsf{rmw}a.\mathsf{data}[\mathit{ea}]b_{\mathrm{r}}^{\ast }{b}_{\mathrm{w}}^{\ast })}& S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & c_{\mathrm{r}}={\mathrm{bytes}}_{\mathit{i}N}^{-1}(b_{\mathrm{r}}^{\ast })\\ \wedge & c_{\mathrm{ex}}={\mathrm{wrap}}_{|t|,N}(c_2)\\ \wedge & c_{\mathrm{r}}=c_{\mathrm{ex}}\\ \wedge & b_{\mathrm{w}}^{\ast }={\mathrm{bytes}}_{\mathit{i}N}({\mathrm{wrap}}_{|t|,N}(c_3)))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{const}{c}_3)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathsf{cmpxchg}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b_{\mathrm{r}}^{\ast })}& S;F;(t.\mathsf{const}c)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & c_{\mathrm{r}}={\mathrm{bytes}}_{\mathit{i}N}^{-1}(b_{\mathrm{r}}^{\ast })\\ \wedge & c_{\mathrm{ex}}={\mathrm{wrap}}_{|t|,N}(c_2)\\ \wedge & c_{\mathrm{r}}\ne c_{\mathrm{ex}}\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(t.\mathsf{const}{c}_2)(t.\mathsf{const}{c}_3)(t.\mathsf{atomic}\mathsf{.}\mathsf{rmw}(N\mathsf{\_}\mathsf{u}{)}^{?}.\mathsf{cmpxchg}\mathit{memarg})& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8>n\vee \mathit{ea}\mathrm{mod}N/8\ne 0)\end{array}\\ \\ \begin{array}{rl}(\text{where}& N=|t|\text{if}N\text{not present}\\ \wedge & a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset})\end{array}\end{array}\end{array}$$

$\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{notify}\mathit{memarg}$

9. Let $N$ be 32.

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}k$ from the stack.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

8. Let $\mathit{ea}$ be $i+\mathit{memarg}.\mathsf{offset}$.

9. If $\mathit{ea}$ modulo $N/8$ is not equal to $0$, then:

   1. Trap.

10. Let $F$ be the current frame.

11. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

12. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

13. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

14. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. If $\mathit{ea}+N/8$ is larger than the length of $\mathit{mem}.\mathsf{data}$, then:

       1. Trap.

    2. Else:

       1. Push the value $t.\mathsf{const}0$ to the stack.

15. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Else:

       1. Perform the action $(\mathsf{notify}a.\mathsf{data}[\mathit{ea}]nk)$ to notify $n$ threads (up to $k$) waiting at data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

       2. Push the value $t.\mathsf{const}n$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{i}\mathsf{32}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{notify}\mathit{memarg}& \hookrightarrow & S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}0)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & \mathit{ea}+N/8\le |\mathit{mem}.\mathsf{data}|\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0)\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{i}\mathsf{32}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{notify}\mathit{memarg}& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared}\\ \wedge & (\mathit{ea}+N/8>|\mathit{mem}.\mathsf{data}|\vee \mathit{ea}\mathrm{mod}N/8\ne 0))\end{array}\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{i}\mathsf{32}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{notify}\mathit{memarg}& & \\ {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)(\mathsf{notify}a.\mathsf{data}[\mathit{ea}]jk)}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}j)& & \end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & j\le k\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0)\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{i}\mathsf{32}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{notify}\mathit{memarg}& {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}& S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n\vee \mathit{ea}\mathrm{mod}N/8\ne 0))\end{array}\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset}\\ \wedge & N=32)\end{array}\end{array}\end{array}$$

$\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{wait}N\mathit{memarg}$

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{64}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{64}.\mathsf{const}k$ from the stack.

1. Assert: due to validation, a value of value type $\mathit{i}N$ is on the top of the stack.

5. Pop the value $\mathit{i}N.\mathsf{const}c$ from the stack.

6. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

7. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

8. Let $\mathit{ea}$ be $i+\mathit{memarg}.\mathsf{offset}$.

9. If $\mathit{ea}$ modulo $N/8$ is not equal to $0$, then:

   1. Trap.

10. Let $F$ be the current frame.

11. Assert: due to validation, $F.\mathsf{module}.\mathsf{memaddrs}[0]$ exists.

12. Let $a$ be the memory address $F.\mathsf{module}.\mathsf{memaddrs}[0]$.

13. Let $\mathit{mem}$ be the memory instance $S.\mathsf{mems}[a]$.

14. If $\mathit{mem}.\mathsf{type}$ is $\mathit{limits}\mathsf{unshared}$, then:

    1. Trap.

15. Else:

    1. Perform the action $(\mathsf{rd}a.\mathsf{len}n)$ to read the length $n$ of the shared memory instance at memory address $a$.

    2. If $\mathit{ea}+N/8$ is larger than $n$, then:

       1. Trap.

    3. Perform the action $({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b^{\ast })$ to read $N/8$ bytes $b^{\ast }$ from data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

    4. If ${\mathrm{bytes}}_{\mathit{i}N}(c)$ is equal to $b^{\ast }$ then:

       1. Let $t$ be ${\mathrm{signed}}_N(k)$.

       2. Perform the action $(\mathsf{wait}a.\mathsf{data}[\mathit{ea}]t)$ to register the current thread as waiting for a signal at data offset $\mathit{ea}$ of the shared memory instance at memory address $a$.

       3. Execute the instruction ${\mathsf{wait}}^{\prime }a.\mathsf{data}[\mathit{ea}]k$.

    5. Else:

       1. Push the value $t.\mathsf{const}1$ to the stack.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathit{i}N.\mathsf{const}c)(\mathsf{i}\mathsf{64}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{wait}N\mathit{memarg}& & \\ \hookrightarrow S;F;\mathsf{trap}& & \end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{unshared})\end{array}\\ \\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathit{i}N.\mathsf{const}c)(\mathsf{i}\mathsf{64}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{wait}N\mathit{memarg}& & \\ {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b^{\ast })(\mathsf{wait}a.\mathsf{data}[\mathit{ea}]t)}S;F;({\mathsf{wait}}^{\prime }a.\mathsf{data}[\mathit{ea}]k)& & \end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & b^{\ast }={\mathrm{bytes}}_{\mathit{i}N}(c))\\ \wedge & t={\mathrm{signed}}_N(k)\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathit{i}N.\mathsf{const}c)(\mathsf{i}\mathsf{64}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{wait}N\mathit{memarg}& & \\ {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)({\mathsf{rd}}_{\mathsf{seqcst}}a.\mathsf{data}[\mathit{ea}]b^{\ast })}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}1)\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & \mathit{ea}+N/8\le n\\ \wedge & \mathit{ea}\mathrm{mod}N/8=0\\ \wedge & b^{\ast }\ne {\mathrm{bytes}}_{\mathit{i}N}(c))\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathit{i}N.\mathsf{const}c)(\mathsf{i}\mathsf{64}.\mathsf{const}k)\mathsf{memory}\mathsf{.}\mathsf{atomic}\mathsf{.}\mathsf{wait}N\mathit{memarg}& & \\ {\hookrightarrow }^{(\mathsf{rd}a.\mathsf{len}n)}S;F;\mathsf{trap}\end{array}\\ \begin{array}{rl}(\text{if}& \mathit{mem}.\mathsf{type}=\mathit{limits}\mathsf{shared}\\ \wedge & (\mathit{ea}+N/8>n\vee \mathit{ea}\mathrm{mod}N/8\ne 0))\end{array}\\ \\ \begin{array}{rl}(\text{where}& a=F.\mathsf{module}.\mathsf{memaddrs}[0]\\ \wedge & \mathit{mem}=S.\mathsf{mems}[a]\\ \wedge & \mathit{ea}=i+\mathit{memarg}.\mathsf{offset})\end{array}\end{array}\end{array}$$

${\mathsf{wait}}^{\prime }\mathit{loc}n$

1. Either the thread has been notified by an $(\mathsf{notify}\mathit{loc})$ action performed in another thread:

   1. Perform the action $(\mathsf{woken}\mathit{loc})$.

   2. Push the value $t.\mathsf{const}0$ to the stack.

2. Or:

   1. If $n$ is less than $0$:

      1. The thread remains suspended.

   2. Else:

      1. Either the thread’s suspension times out:

         1. Perform the action $(\mathsf{timeout}\mathit{loc})$.

         2. Push the value $t.\mathsf{const}2$ to the stack.

      2. Or the thread remains suspended.

$$\begin{array}{r}\begin{array}{l}\begin{array}{lcl}{\mathsf{wait}}^{\prime }\mathit{loc}n& {\hookrightarrow }^{(\mathsf{woken}\mathit{loc})}& (\mathsf{i}\mathsf{32}.\mathsf{const}0)\end{array}\\ \begin{array}{lcl}{\mathsf{wait}}^{\prime }\mathit{loc}n& {\hookrightarrow }^{(\mathsf{timeout}\mathit{loc})}& (\mathsf{i}\mathsf{32}.\mathsf{const}2)\end{array}\\ \begin{array}{rl}(\text{if}& n\ge 0)\end{array}\\ \begin{array}{lcl}{\mathsf{wait}}^{\prime }\mathit{loc}n& \hookrightarrow & {\mathsf{wait}}^{\prime }\mathit{loc}n\end{array}\end{array}\end{array}$$

$\mathsf{atomic}\mathsf{.}\mathsf{fence}$

1. Perform the action $({\mathsf{fence}}_{\mathsf{seqcst}})$.

$$\begin{array}{l}\begin{array}{lcl}\mathsf{atomic}\mathsf{.}\mathsf{fence}& {\hookrightarrow }^{({\mathsf{fence}}_{\mathsf{seqcst}})}& ϵ\end{array}\end{array}$$

Control Instructions

$\mathsf{nop}$

1. Do nothing.

$$\begin{array}{lcl}\mathsf{nop}& \hookrightarrow & ϵ\end{array}$$

$\mathsf{unreachable}$

1. Trap.

$$\begin{array}{lcl}\mathsf{unreachable}& \hookrightarrow & \mathsf{trap}\end{array}$$

$\mathsf{block}\mathit{blocktype}{\mathit{instr}}^{\ast }\mathsf{end}$

1. Let $F$ be the current frame.

2. Assert: due to validation, ${\mathrm{expand}}_F(\mathit{blocktype})$ is defined.

3. Let $[t_1^m]\to [t_2^n]$ be the function type ${\mathrm{expand}}_F(\mathit{blocktype})$.

4. Let $L$ be the label whose arity is $n$ and whose continuation is the end of the block.

5. Assert: due to validation, there are at least $m$ values on the top of the stack.

6. Pop the values ${\mathit{val}}^m$ from the stack.

7. Enter the block ${\mathit{val}}^m{\mathit{instr}}^{\ast }$ with label $L$.

$$\begin{array}{r}\\ \begin{array}{lcl}F;{\mathit{val}}^m\mathsf{block}\mathit{bt}{\mathit{instr}}^{\ast }\mathsf{end}& \hookrightarrow & F;{\mathsf{label}}_n\{ϵ\}{\mathit{val}}^m{\mathit{instr}}^{\ast }\mathsf{end}\\ & & (\text{if}{\mathrm{expand}}_F(\mathit{bt})=[t_1^m]\to [t_2^n])\end{array}\end{array}$$

$\mathsf{loop}\mathit{blocktype}{\mathit{instr}}^{\ast }\mathsf{end}$

1. Let $F$ be the current frame.

2. Assert: due to validation, ${\mathrm{expand}}_F(\mathit{blocktype})$ is defined.

3. Let $[t_1^m]\to [t_2^n]$ be the function type ${\mathrm{expand}}_F(\mathit{blocktype})$.

4. Let $L$ be the label whose arity is $m$ and whose continuation is the start of the loop.

5. Assert: due to validation, there are at least $m$ values on the top of the stack.

6. Pop the values ${\mathit{val}}^m$ from the stack.

7. Enter the block ${\mathit{val}}^m{\mathit{instr}}^{\ast }$ with label $L$.

$$\begin{array}{r}\\ \begin{array}{lcl}F;{\mathit{val}}^m\mathsf{loop}\mathit{bt}{\mathit{instr}}^{\ast }\mathsf{end}& \hookrightarrow & F;{\mathsf{label}}_m\{\mathsf{loop}\mathit{bt}{\mathit{instr}}^{\ast }\mathsf{end}\}{\mathit{val}}^m{\mathit{instr}}^{\ast }\mathsf{end}\\ & & (\text{if}{\mathrm{expand}}_F(\mathit{bt})=[t_1^m]\to [t_2^n])\end{array}\end{array}$$

$\mathsf{if}\mathit{blocktype}{\mathit{instr}}_1^{\ast }\mathsf{else}{\mathit{instr}}_2^{\ast }\mathsf{end}$

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}c$ from the stack.

3. If $c$ is non-zero, then:

   1. Execute the block instruction $\mathsf{block}\mathit{blocktype}{\mathit{instr}}_1^{\ast }\mathsf{end}$.

4. Else:

   1. Execute the block instruction $\mathsf{block}\mathit{blocktype}{\mathit{instr}}_2^{\ast }\mathsf{end}$.

$$\begin{array}{r}\\ \begin{array}{lcl}(\mathsf{i}\mathsf{32}.\mathsf{const}c)\mathsf{if}\mathit{bt}{\mathit{instr}}_1^{\ast }\mathsf{else}{\mathit{instr}}_2^{\ast }\mathsf{end}& \hookrightarrow & \mathsf{block}\mathit{bt}{\mathit{instr}}_1^{\ast }\mathsf{end}\\ & & (\text{if}c\ne 0)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}c)\mathsf{if}\mathit{bt}{\mathit{instr}}_1^{\ast }\mathsf{else}{\mathit{instr}}_2^{\ast }\mathsf{end}& \hookrightarrow & \mathsf{block}\mathit{bt}{\mathit{instr}}_2^{\ast }\mathsf{end}\\ & & (\text{if}c=0)\end{array}\end{array}$$

$\mathsf{br}l$

1. Assert: due to validation, the stack contains at least $l+1$ labels.

2. Let $L$ be the $l$-th label appearing on the stack, starting from the top and counting from zero.

3. Let $n$ be the arity of $L$.

4. Assert: due to validation, there are at least $n$ values on the top of the stack.

5. Pop the values ${\mathit{val}}^n$ from the stack.

6. Repeat $l+1$ times:

   1. While the top of the stack is a value, do:

      1. Pop the value from the stack.

   2. Assert: due to validation, the top of the stack now is a label.

   3. Pop the label from the stack.

7. Push the values ${\mathit{val}}^n$ to the stack.

8. Jump to the continuation of $L$.

$$\begin{array}{r}\\ \begin{array}{lcl}{\mathsf{label}}_n\{{\mathit{instr}}^{\ast }\}{B}^l[{\mathit{val}}^n(\mathsf{br}l)]\mathsf{end}& \hookrightarrow & {\mathit{val}}^n{\mathit{instr}}^{\ast }\end{array}\end{array}$$

$\mathsf{br}\mathsf{\_}\mathsf{if}l$

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}c$ from the stack.

3. If $c$ is non-zero, then:

   1. Execute the instruction $\mathsf{br}l$.

4. Else:

   1. Do nothing.

$$\begin{array}{r}\\ \begin{array}{lcll}(\mathsf{i}\mathsf{32}.\mathsf{const}c)(\mathsf{br}\mathsf{\_}\mathsf{if}l)& \hookrightarrow & (\mathsf{br}l)& (\text{if}c\ne 0)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}c)(\mathsf{br}\mathsf{\_}\mathsf{if}l)& \hookrightarrow & ϵ& (\text{if}c=0)\end{array}\end{array}$$

$\mathsf{br}\mathsf{\_}\mathsf{table}{l}^{\ast }{l}_N$

1. Assert: due to validation, a value of value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

2. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

3. If $i$ is smaller than the length of $l^{\ast }$, then:

   1. Let $l_i$ be the label $l^{\ast }[i]$.

   2. Execute the instruction $\mathsf{br}{l}_i$.

4. Else:

   1. Execute the instruction $\mathsf{br}{l}_N$.

$$\begin{array}{r}\\ \begin{array}{lcll}(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{br}\mathsf{\_}\mathsf{table}{l}^{\ast }{l}_N)& \hookrightarrow & (\mathsf{br}{l}_i)& (\text{if}{l}^{\ast }[i]=l_i)\\ (\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{br}\mathsf{\_}\mathsf{table}{l}^{\ast }{l}_N)& \hookrightarrow & (\mathsf{br}{l}_N)& (\text{if}|l^{\ast }|\le i)\end{array}\end{array}$$

$\mathsf{return}$

1. Let $F$ be the current frame.

2. Let $n$ be the arity of $F$.

3. Assert: due to validation, there are at least $n$ values on the top of the stack.

4. Pop the results ${\mathit{val}}^n$ from the stack.

5. Assert: due to validation, the stack contains at least one frame.

6. While the top of the stack is not a frame, do:

   1. Pop the top element from the stack.

7. Assert: the top of the stack is the frame $F$.

8. Pop the frame from the stack.

9. Push ${\mathit{val}}^n$ to the stack.

10. Jump to the instruction after the original call that pushed the frame.

$$\begin{array}{r}\\ \begin{array}{lcl}{\mathsf{frame}}_n\{F\}{B}^k[{\mathit{val}}^n\mathsf{return}]\mathsf{end}& \hookrightarrow & {\mathit{val}}^n\end{array}\end{array}$$

$\mathsf{call}x$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{funcaddrs}[x]$ exists.

3. Let $a$ be the function address $F.\mathsf{module}.\mathsf{funcaddrs}[x]$.

4. Invoke the function instance at address $a$.

$$\begin{array}{lcll}F;(\mathsf{call}x)& \hookrightarrow & F;(\mathsf{invoke}a)& (\text{if}F.\mathsf{module}.\mathsf{funcaddrs}[x]=a)\end{array}$$

$\mathsf{call}\mathsf{\_}\mathsf{indirect}xy$

1. Let $F$ be the current frame.

2. Assert: due to validation, $F.\mathsf{module}.\mathsf{tableaddrs}[x]$ exists.

3. Let $\mathit{ta}$ be the table address $F.\mathsf{module}.\mathsf{tableaddrs}[x]$.

4. Assert: due to validation, $S.\mathsf{tables}[\mathit{ta}]$ exists.

5. Let $\mathit{tab}$ be the table instance $S.\mathsf{tables}[\mathit{ta}]$.

6. Assert: due to validation, $F.\mathsf{module}.\mathsf{types}[y]$ exists.

7. Let ${\mathit{ft}}_{\mathrm{expect}}$ be the function type $F.\mathsf{module}.\mathsf{types}[y]$.

8. Assert: due to validation, a value with value type $\mathsf{i}\mathsf{32}$ is on the top of the stack.

9. Pop the value $\mathsf{i}\mathsf{32}.\mathsf{const}i$ from the stack.

10. If $i$ is not smaller than the length of $\mathit{tab}.\mathsf{elem}$, then:

    1. Trap.

11. Let $r$ be the reference $\mathit{tab}.\mathsf{elem}[i]$.

12. If $r$ is $\mathsf{ref}\mathsf{.}\mathsf{null}t$, then:

    1. Trap.

13. Assert: due to validation of table mutation, $r$ is a function reference.

14. Let $\mathsf{ref}a$ be the function reference $r$.

15. Assert: due to validation of table mutation, $S.\mathsf{funcs}[a]$ exists.

16. Let $\mathit{f}$ be the function instance $S.\mathsf{funcs}[a]$.

17. Let ${\mathit{ft}}_{\mathrm{actual}}$ be the function type $\mathit{f}.\mathsf{type}$.

18. If ${\mathit{ft}}_{\mathrm{actual}}$ and ${\mathit{ft}}_{\mathrm{expect}}$ differ, then:

    1. Trap.

19. Invoke the function instance at address $a$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{call}\mathsf{\_}\mathsf{indirect}xy)& \hookrightarrow & S;F;(\mathsf{invoke}a)\end{array}\\ \begin{array}{rl}(\text{if}& S.\mathsf{tables}[F.\mathsf{module}.\mathsf{tableaddrs}[x]].\mathsf{elem}[i]=\mathsf{ref}a\\ \wedge & S.\mathsf{funcs}[a]=f\\ \wedge & F.\mathsf{module}.\mathsf{types}[y]=f.\mathsf{type})\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{i}\mathsf{32}.\mathsf{const}i)(\mathsf{call}\mathsf{\_}\mathsf{indirect}xy)& \hookrightarrow & S;F;\mathsf{trap}\end{array}\\ (\text{otherwise})\end{array}\end{array}$$

Blocks

The following auxiliary rules define the semantics of executing an instruction sequence that forms a block.

Entering ${\mathit{instr}}^{\ast }$ with label $L$

1. Push $L$ to the stack.

2. Jump to the start of the instruction sequence ${\mathit{instr}}^{\ast }$.

Note

No formal reduction rule is needed for entering an instruction sequence, because the label $L$ is embedded in the administrative instruction that structured control instructions reduce to directly.

Exiting ${\mathit{instr}}^{\ast }$ with label $L$

When the end of a block is reached without a jump or trap aborting it, then the following steps are performed.

1. Pop all values ${\mathit{val}}^{\ast }$ from the top of the stack.

2. Assert: due to validation, the label $L$ is now on the top of the stack.

3. Pop the label from the stack.

4. Push ${\mathit{val}}^{\ast }$ back to the stack.

5. Jump to the position after the $\mathsf{end}$ of the structured control instruction associated with the label $L$.

$$\begin{array}{r}\\ \begin{array}{lcl}{\mathsf{label}}_n\{{\mathit{instr}}^{\ast }\}{\mathit{val}}^{\ast }\mathsf{end}& \hookrightarrow & {\mathit{val}}^{\ast }\end{array}\end{array}$$

Note

This semantics also applies to the instruction sequence contained in a $\mathsf{loop}$ instruction. Therefore, execution of a loop falls off the end, unless a backwards branch is performed explicitly.

Function Calls

The following auxiliary rules define the semantics of invoking a function instance through one of the call instructions and returning from it.

Invocation of function address $a$

1. Assert: due to validation, $S.\mathsf{funcs}[a]$ exists.

2. Let $f$ be the function instance, $S.\mathsf{funcs}[a]$.

3. Let $[t_1^n]\to [t_2^m]$ be the function type $f.\mathsf{type}$.

4. Let $t^{\ast }$ be the list of value types $f.\mathsf{code}.\mathsf{locals}$.

5. Let ${\mathit{instr}}^{\ast }\mathsf{end}$ be the expression $f.\mathsf{code}.\mathsf{body}$.

6. Assert: due to validation, $n$ values are on the top of the stack.

7. Pop the values ${\mathit{val}}^n$ from the stack.

8. Let $F$ be the frame $\{\mathsf{module}f.\mathsf{module},\mathsf{locals}{\mathit{val}}^n({\mathrm{default}}_t{)}^{\ast }\}$.

9. Push the activation of $F$ with arity $m$ to the stack.

10. Let $L$ be the label whose arity is $m$ and whose continuation is the end of the function.

11. Enter the instruction sequence ${\mathit{instr}}^{\ast }$ with label $L$.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;{\mathit{val}}^n(\mathsf{invoke}a)& \hookrightarrow & S;{\mathsf{frame}}_m\{F\}{\mathsf{label}}_m\{\}{\mathit{instr}}^{\ast }\mathsf{end}\mathsf{end}\end{array}\\ \begin{array}{rl}(\text{if}& S.\mathsf{funcs}[a]=f\\ \wedge & f.\mathsf{type}=[t_1^n]\to [t_2^m]\\ \wedge & f.\mathsf{code}=\{\mathsf{type}x,\mathsf{locals}{t}^k,\mathsf{body}{\mathit{instr}}^{\ast }\mathsf{end}\}\\ \wedge & F=\{\mathsf{module}f.\mathsf{module},\mathsf{locals}{\mathit{val}}^n({\mathrm{default}}_t{)}^k\})\end{array}\end{array}\end{array}$$

Returning from a function

When the end of a function is reached without a jump (i.e., $\mathsf{return}$) or trap aborting it, then the following steps are performed.

1. Let $F$ be the current frame.

2. Let $n$ be the arity of the activation of $F$.

3. Assert: due to validation, there are $n$ values on the top of the stack.

4. Pop the results ${\mathit{val}}^n$ from the stack.

5. Assert: due to validation, the frame $F$ is now on the top of the stack.

6. Pop the frame from the stack.

7. Push ${\mathit{val}}^n$ back to the stack.

8. Jump to the instruction after the original call.

$$\begin{array}{r}\\ \begin{array}{lcl}{\mathsf{frame}}_n\{F\}{\mathit{val}}^n\mathsf{end}& \hookrightarrow & {\mathit{val}}^n\end{array}\end{array}$$

Host Functions

Invoking a host function has non-deterministic behavior. It may either terminate with a trap or return regularly. However, in the latter case, it must consume and produce the right number and types of WebAssembly values on the stack, according to its function type.

A host function may also modify the store. However, all store modifications must result in an extension of the original store, i.e., they must only modify mutable contents and must not have instances removed. Furthermore, the resulting store must be valid, i.e., all data and code in it is well-typed.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;{\mathit{val}}^n(\mathsf{invoke}a)& \hookrightarrow & S;\mathsf{host}[t_2^m]\end{array}\\ \begin{array}{rl}(\text{if}& S.\mathsf{funcs}[a]=\{\mathsf{type}[t_1^n]\to [t_2^m],\mathsf{hostcode}\mathit{hf}\}\end{array}\end{array}\end{array}$$

During its execution, a host function call may do any of the following.

• Instantiate an arbitrary WebAssembly module.

• Allocate a new host function.

• Continue execution, possibly spawning a new thread, with no other observable effects.

• Terminate with a list of values that respects the host function’s type annotation.

• Terminate with a trap.

$$\begin{array}{r}\\ \begin{array}{l}\begin{array}{lcl}S;F;(\mathsf{host}[t^{\ast }])& \hookrightarrow & S^{\prime };F;({\mathsf{frame}}_0\{F_0\}{e}^{\ast }\mathsf{end})(\mathsf{host}[t^{\ast }])\end{array}\\ \begin{array}{rl}(\text{if}& \mathrm{instantiate}(S,\mathit{module},{\mathit{externval}}^k)=S^{\prime };F_0;e^{\ast })\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{host}[t^{\ast }])& \hookrightarrow & S^{\prime };F;(\mathsf{host}[t^{\ast }])\end{array}\\ \begin{array}{rl}(\text{if}& \mathrm{allochostfunc}(S,\mathit{functype},\mathit{hostfunc})=S^{\prime },\mathit{funcaddr})\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{host}[t^{\ast }])& {\hookrightarrow }^{{\mathsf{spawn}}^{?}}& S;F;(\mathsf{host}[t^{\ast }])\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{host}[t^{\ast }])& \hookrightarrow & S;F;{\mathit{val}}^{\ast }\end{array}\\ \begin{array}{rl}(\text{if}& S⊢{\mathit{val}}^{\ast }:[t^{\ast }])\end{array}\\ \begin{array}{lcl}S;F;(\mathsf{host}[t^{\ast }])& \hookrightarrow & S;F;\mathsf{trap}\end{array}\end{array}\end{array}$$

Note

A host function can call back into WebAssembly by invoking a function exported from a module. However, the effects of any such call are subsumed by the non-deterministic behavior allowed for the host function.

Expressions

An expression is evaluated relative to a current frame pointing to its containing module instance.

1. Jump to the start of the instruction sequence ${\mathit{instr}}^{\ast }$ of the expression.

2. Execute the instruction sequence.

3. Assert: due to validation, the top of the stack contains a value.

4. Pop the value $\mathit{val}$ from the stack.

The value $\mathit{val}$ is the result of the evaluation.

$$S;F;{\mathit{instr}}^{\ast }{\hookrightarrow }^{{\mathit{act}}^{\ast }}{S}^{\prime };F^{\prime };{\mathit{instr}}^{\prime \ast }(\text{if}S;F;{\mathit{instr}}^{\ast }\mathsf{end}{\hookrightarrow }^{{\mathit{act}}^{\ast }}{S}^{\prime };F^{\prime };{\mathit{instr}}^{\prime \ast }\mathsf{end})$$

Note

Evaluation iterates this reduction rule until reaching a value. Expressions constituting function bodies are executed during function invocation.