数值指令
数值指令根据通用数值运算符定义。数值指令与其底层运算符的映射由以下定义表示
\[\begin{split}\begin{array}{lll@{\qquad}l} \mathit{op}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}}(i_1,\dots,i_k) &=& \href{../exec/numerics.html#int-ops}{\mathrm{i}\mathit{op}}_N(i_1,\dots,i_k) \\ \mathit{op}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{f}N}}(z_1,\dots,z_k) &=& \href{../exec/numerics.html#float-ops}{\mathrm{f}\mathit{op}}_N(z_1,\dots,z_k) \\ \end{array}\end{split}\]
以及对于转换运算符
\[\begin{split}\begin{array}{lll@{\qquad}l} \href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{t_1,t_2}(c) &=& \href{../exec/numerics.html#convert-ops}{\mathit{cvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{|t_1|,|t_2|}(c) \\ \end{array}\end{split}\]
当底层运算符为部分运算符时，如果结果未定义，则相应的指令将陷入陷阱。当底层运算符为非确定性运算符时，因为它们可能返回多个可能的NaN值，相应的指令也是如此。
注意
例如，指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\)应用于操作数\(i_1, i_2\)将调用\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}}(i_1, i_2)\)，通过上述定义映射到通用\(\href{../exec/numerics.html#op-iadd}{\mathrm{iadd}}_{32}(i_1, i_2)\)。类似地，\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{trunc}}\mathsf{\_}\href{../syntax/types.html#syntax-valtype}{\mathsf{f32}}\mathsf{\_s}\)应用于\(z\)将调用\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{trunc}}^{\mathsf{s}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{f32}},\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}}(z)\)，映射到通用\(\href{../exec/numerics.html#op-trunc-s}{\mathrm{trunc}^{\mathsf{s}}}_{32,64}(z)\)。
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)
将值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)推入栈。
注意
此指令不需要正式的归约规则，因为\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\)指令本身就是值。
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}}\)
断言：由于验证，栈顶有一个值类型\(t\)的值。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1\)。
如果\(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{unop}}_t(c_1)\)已定义，则
令\(c\)为计算\(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{unop}}_t(c_1)\)的可能结果。
将值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)推入栈。
否则
陷入陷阱。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~t\mathsf{.}\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c \in \href{../exec/instructions.html#exec-instr-numeric}{\mathit{unop}}_t(c_1)) \\ (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~t\mathsf{.}\href{../syntax/instructions.html#syntax-unop}{\mathit{unop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} & (\mathrel{\mbox{if}} \href{../exec/instructions.html#exec-instr-numeric}{\mathit{unop}}_{t}(c_1) = \{\}) \end{array}\end{split}\]
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}}\)
断言：由于验证，栈顶有两个值类型\(t\)的值。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2\)。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1\)。
如果\(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{binop}}_t(c_1, c_2)\)已定义，则
令\(c\)为计算\(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{binop}}_t(c_1, c_2)\)的可能结果。
将值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)推入栈。
否则
陷入陷阱。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2)~t\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c \in \href{../exec/instructions.html#exec-instr-numeric}{\mathit{binop}}_t(c_1,c_2)) \\ (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2)~t\mathsf{.}\href{../syntax/instructions.html#syntax-binop}{\mathit{binop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} & (\mathrel{\mbox{if}} \href{../exec/instructions.html#exec-instr-numeric}{\mathit{binop}}_{t}(c_1,c_2) = \{\}) \end{array}\end{split}\]
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}}\)
断言：由于验证，栈顶有一个值类型\(t\)的值。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1\)。
令\(c\)为计算\(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{testop}}_t(c_1)\)的结果。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)推入栈。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~t\mathsf{.}\href{../syntax/instructions.html#syntax-testop}{\mathit{testop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c = \href{../exec/instructions.html#exec-instr-numeric}{\mathit{testop}}_t(c_1)) \\ \end{array}\end{split}\]
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}}\)
断言：由于验证，栈顶有两个值类型\(t\)的值。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2\)。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1\)。
令\(c\)为计算\(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{relop}}_t(c_1, c_2)\)的结果。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)推入栈。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2)~t\mathsf{.}\href{../syntax/instructions.html#syntax-relop}{\mathit{relop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c = \href{../exec/instructions.html#exec-instr-numeric}{\mathit{relop}}_t(c_1,c_2)) \\ \end{array}\end{split}\]
\(t_2\mathsf{.}\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}\mathsf{\_}t_1\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\)
断言：由于验证，栈顶有一个值类型\(t_1\)的值。
从栈顶弹出值\(t_1.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1\)。
如果\(\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{t_1,t_2}(c_1)\)已定义
令\(c_2\)为计算\(\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{t_1,t_2}(c_1)\)的可能结果。
将值\(t_2.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2\)推入栈。
否则
陷入陷阱。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (t_1\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~t_2\mathsf{.}\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}\mathsf{\_}t_1\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^? &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (t_2\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2) & (\mathrel{\mbox{if}} c_2 \in \href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{t_1,t_2}(c_1)) \\ (t_1\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~t_2\mathsf{.}\href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}\mathsf{\_}t_1\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^? &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} & (\mathrel{\mbox{if}} \href{../syntax/instructions.html#syntax-cvtop}{\mathit{cvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{t_1,t_2}(c_1) = \{\}) \end{array}\end{split}\]
向量指令
按位操作的向量指令被视为相应宽度的整数操作。
\[\begin{split}\begin{array}{lll@{\qquad}l} \mathit{op}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v}N}}(i_1,\dots,i_k) &=& \href{../exec/numerics.html#int-ops}{\mathrm{i}\mathit{op}}_N(i_1,\dots,i_k) \\ \end{array}\end{split}\]
大多数其他向量指令根据给定的 形状，以逐车道应用的数值运算符来定义。
\[\begin{split}\begin{array}{llll} \mathit{op}_{t\mathsf{x}N}(n_1,\dots,n_k) &=& \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t\mathsf{x}N}(\href{../exec/instructions.html#exec-instr-numeric}{\mathit{op}}_t(i_1,\dots,i_k)^\ast) & \qquad(\mathrel{\mbox{if}} i_1^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(n_1) \land \dots \land i_k^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(n_k) \\ \end{array}\end{split}\]
注意
例如，指令 \(\mathsf{i32x4}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) 应用于操作数 \(v_1, v_2\) 的结果会调用 \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}_{\mathsf{i32x4}}(v_1, v_2)\)，这映射到 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\mathsf{i32x4}}(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}}(i_1, i_2)^\ast)\)，其中 \(i_1^\ast\) 和 \(i_2^\ast\) 分别是调用 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\mathsf{i32x4}}(v_1)\) 和 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\mathsf{i32x4}}(v_2)\) 得到的序列。
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\)
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
注意
此指令不需要正式的归约规则，因为 \(\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}\) 指令与 值 相符。
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}\)
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(c\) 为计算 \(\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}}(c_1)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c = \href{../syntax/instructions.html#syntax-vvunop}{\mathit{vvunop}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}}(c_1)) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}\)
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(c\) 为计算 \(\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}}(c_1, c_2)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c = \href{../syntax/instructions.html#syntax-vvbinop}{\mathit{vvbinop}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}}(c_1, c_2)) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}\)
断言：由于 验证，栈顶有三个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_3\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(c\) 为计算 \(\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}}(c_1, c_2, c_3)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) & (\mathrel{\mbox{if}} c = \href{../syntax/instructions.html#syntax-vvternop}{\mathit{vvternop}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}}(c_1, c_2, c_3)) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{any\_true}}\)
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i\) 为计算 \(\href{../exec/numerics.html#op-ine}{\mathrm{ine}}_{128}(c_1, 0)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\) 推入栈中。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{any\_true}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) & (\mathrel{\mbox{if}} i = \href{../exec/numerics.html#op-ine}{\mathrm{ine}}_{128}(c_1, 0)) \\ \end{array}\end{split}\]
\(\mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{swizzle}}\)
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_2)\) 的结果。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(j^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_1)\) 的结果。
令 \(c^\ast\) 为两个序列 \(j^\ast\) 和 \(0^{240}\) 的连接。
令 \(c'\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c'\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{swizzle}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c') \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & i^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_2) \\ \wedge & c^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_1)~0^{240} \\ \wedge & c' = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])) \end{array} \end{array}\end{split}\]
\(\mathsf{i8x16.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~x^\ast\)
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
断言：由于 验证，对于 \(x^\ast\) 中的所有 \(x_i\)，都有 \(x_i < 32\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
令 \(i_2^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_2)\) 的结果。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i_1^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_1)\) 的结果。
令 \(i^\ast\) 为两个序列 \(i_1^\ast\) 和 \(i_2^\ast\) 的连接。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{shuffle}}~x^\ast) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & i^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_1)~\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(c_2) \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i8x16}}}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])) \end{array} \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}}\)
令 \(t\) 为类型 \(\href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\)。
断言：由于 验证，栈顶的值的 值类型 为 \(t\)。
从栈顶弹出值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1\)。
令 \(N\) 为整数 \(\href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\)。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1^N)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_1)~\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{splat}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) & (\mathrel{\mbox{如果}} t = \href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}) \wedge c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1^{\href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})})) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{replace\_lane}}~x\)
断言：由于 验证，\(x < \href{../valid/instructions.html#aux-dim}{\mathrm{dim}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\)。
令 \(t_2\) 为类型 \(\href{../valid/instructions.html#aux-unpacked}{\mathrm{unpacked}}(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}})\)。
断言：由于 验证，栈顶的值的 值类型 为 \(t_1\)。
弹出栈顶的值 \(t_2.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2\)。
断言：由于 验证，栈顶的值的 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(i^\ast \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} [x] = c_2)\) 的结果。
将 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(t_2\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_2)~(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{replace\_lane}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & i^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1) \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(i^\ast \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} [x] = c_2)) \end{array} \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}}\)
断言：由于 验证，栈顶的值的 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(c\) 为计算 \(\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) & (\mathrel{\mbox{如果}} c = \href{../syntax/instructions.html#syntax-vunop}{\mathit{vunop}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1)) \end{array}\]
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}\)
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
如果 \(\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1, c_2)\) 已定义
令 \(c\) 为计算 \(\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1, c_2)\) 的一个可能结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
否则
陷入陷阱。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) & (\mathrel{\mbox{如果}} c \in \href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1, c_2)) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}} & (\mathrel{\mbox{如果}} \href{../syntax/instructions.html#syntax-vbinop}{\mathit{vbinop}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c_1, c_2) = \{\}) \end{array}\end{split}\]
\(t\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}}\)
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i_1^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c_1)\) 的结果。
令 \(i_2^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c_2)\) 的结果。
令 \(i^\ast\) 为计算 \(\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}}_t(i_1^\ast, i_2^\ast)\) 的结果。
令 \(j^\ast\) 为计算 \(\href{../exec/numerics.html#op-extend-s}{\mathrm{extend}^{\mathsf{s}}}_{1,|t|}(i^\ast)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t\mathsf{x}N}(j^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~t\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t\mathsf{x}N}(\href{../exec/numerics.html#op-extend-s}{\mathrm{extend}^{\mathsf{s}}}_{1,|t|}(\href{../syntax/instructions.html#syntax-vrelop}{\mathit{vrelop}}_t(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c_1), \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c_2))))) \end{array} \end{array}\end{split}\]
\(t\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vishiftop}{\mathit{vishiftop}}\)
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c_1)\) 的结果。
令 \(j^\ast\) 为计算 \(\href{../syntax/instructions.html#syntax-vishiftop}{\mathit{vishiftop}}_{t}(i^\ast, s^N)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t\mathsf{x}N}(j^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~t\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vishiftop}{\mathit{vishiftop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & i^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c_1) \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t\mathsf{x}N}(\href{../syntax/instructions.html#syntax-vishiftop}{\mathit{vishiftop}}_{t}(i^\ast, s^N))) \end{array} \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{all\_true}}\)
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\)。
令 \(i_1^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c)\) 的结果。
令 \(i\) 为计算 \(\href{../exec/numerics.html#aux-bool}{\mathrm{bool}}(\bigwedge(i_1 \neq 0)^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c)~\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{all\_true}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & i_1^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/instructions.html#syntax-shape}{\mathit{shape}}}(c) \\ \wedge & i = \href{../exec/numerics.html#aux-bool}{\mathrm{bool}}(\bigwedge(i_1 \neq 0)^\ast)) \end{array} \end{array}\end{split}\]
\(t\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}}\)
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\)。
令 \(i_1^N\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c)\) 的结果。
令 \(B\) 为值类型 \(t\) 的 位宽 \(|t|\)。
令 \(i_2^N\) 为计算 \(\href{../exec/numerics.html#op-ilt-s}{\mathrm{ilt\_s}}_{B}(i_1^N, 0^N)\) 的结果。
令 \(j^\ast\) 为两个序列 \(i_2^N\) 和 \(0^{32-N}\) 的连接。
令 \(i\) 为计算 \(\href{../exec/numerics.html#aux-ibits}{\mathrm{ibits}}_{32}^{-1}(j^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\) 推入栈中。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c)~t\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{bitmask}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) & (\mathrel{\mbox{如果}} i = \href{../exec/numerics.html#aux-ibits}{\mathrm{ibits}}_{32}^{-1}(\href{../exec/numerics.html#op-ilt-s}{\mathrm{ilt\_s}}_{|t|}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t\mathsf{x}N}(c), 0^N))) \\ \end{array}\end{split}\]
\(t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{narrow}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)
断言：根据 语法，\(N = 2\cdot M\)。
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
令 \(i_2^M\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)\) 的结果。
令 \(d_2^M\) 为计算 \(\href{../exec/numerics.html#op-narrow-u}{\mathrm{narrow}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(i_2^M)\) 的结果。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i_1^M\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)\) 的结果。
令 \(d_1^M\) 为计算 \(\href{../exec/numerics.html#op-narrow-u}{\mathrm{narrow}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(i_1^M)\) 的结果。
令 \(j^N\) 为两个序列 \(d_1^M\) 和 \(d_2^M\) 的连接。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(j^N)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{narrow}}\_t_1\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & d_1^M = \href{../exec/numerics.html#op-narrow-u}{\mathrm{narrow}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}( \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)) \\ \wedge & d_2^M = \href{../exec/numerics.html#op-narrow-u}{\mathrm{narrow}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}( \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)) \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(d_1^M~d_2^M)) \end{array} \end{array}\end{split}\]
\(t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)
断言：根据 语法，\(N = M\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)\) 的结果。
令 \(j^\ast\) 为计算 \(\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(i^\ast)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(j^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)))) \end{array} \end{array}\end{split}\]
\(t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\)
断言：根据 语法，\(N = M / 2\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)\) 的结果。
如果 \(\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\) 为 \(\mathsf{low}\)，则
令 \(j^\ast\) 为序列 \(i^\ast[0 \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]\)。
否则
令 \(j^\ast\) 为序列 \(i^\ast[N \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]\)。
令 \(k^\ast\) 为计算 \(\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{|t_1|,|t_2|}(j^\ast)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(k^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^? &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{|t_1|,|t_2|}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)[\href{../syntax/instructions.html#syntax-half}{\mathit{half}}(0, N) \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]))) \end{array} \end{array}\end{split}\]
其中
\[\begin{split}\begin{array}{lcl} \mathsf{low}(x, y) &=& x \\ \mathsf{high}(x, y) &=& y \\ \end{array}\end{split}\]
\(t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\mathsf{\_zero}\)
断言：由于 语法，\(N = 2 \cdot M\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)\) 的结果。
令 \(j^\ast\) 为计算 \(\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{|t_1|,|t_2|}(i^\ast)\) 的结果。
令 \(k^\ast\) 为两个序列 \(j^\ast\) 和 \(0^M\) 的连接。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(k^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?\mathsf{\_zero} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(\href{../syntax/instructions.html#syntax-vcvtop}{\mathit{vcvtop}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}^?}_{|t_1|,|t_2|}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1))~0^M)) \end{array} \end{array}\end{split}\]
\(\mathsf{i32x4.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{dot}}\mathsf{\_i16x8\_s}\)
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i_1^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i16x8}}}(c_1)\) 的结果。
令 \(j_1^\ast\) 为计算 \(\href{../exec/numerics.html#op-extend-s}{\mathrm{extend}^{\mathsf{s}}}_{16,32}(i_1^\ast)\) 的结果。
令 \(i_2^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i16x8}}}(c_2)\) 的结果。
令 \(j_2^\ast\) 为计算 \(\href{../exec/numerics.html#op-extend-s}{\mathrm{extend}^{\mathsf{s}}}_{16,32}(i_2^\ast)\) 的结果。
令 \((k_1~k_2)^\ast\) 为计算 \(\href{../exec/numerics.html#op-imul}{\mathrm{imul}}_{32}(j_1^\ast, j_2^\ast)\) 的结果。
令 \(k^\ast\) 为计算 \(\href{../exec/numerics.html#op-iadd}{\mathrm{iadd}}_{32}(k_1, k_2)^\ast\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i32x4}}}(k^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~\mathsf{i32x4.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{dot}}\mathsf{\_i16x8\_s} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & (i_1~i_2)^\ast = \href{../exec/numerics.html#op-imul}{\mathrm{imul}}_{32}(\href{../exec/numerics.html#op-extend-s}{\mathrm{extend}^{\mathsf{s}}}_{16,32}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i16x8}}}(c_1)), \href{../exec/numerics.html#op-extend-s}{\mathrm{extend}^{\mathsf{s}}}_{16,32}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i16x8}}}(c_2))) \\ \wedge & j^\ast = \href{../exec/numerics.html#op-iadd}{\mathrm{iadd}}_{32}(i_1, i_2)^\ast \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i32x4}}}(j^\ast)) \end{array} \end{array}\end{split}\]
\(t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extmul}}\mathsf{\_}\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\mathsf{\_}t_1\mathsf{x}M\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)
断言：根据 语法，\(N = M / 2\)。
断言：由于 验证，栈顶有两个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i_1^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)\) 的结果。
令 \(i_2^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)\) 的结果。
如果 \(\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\) 为 \(\mathsf{low}\)，则
令 \(j_1^\ast\) 为序列 \(i_1^\ast[0 \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]\)。
令 \(j_2^\ast\) 为序列 \(i_2^\ast[0 \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]\)。
否则
令 \(j_1^\ast\) 为序列 \(i_1^\ast[N \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]\)。
令 \(j_2^\ast\) 为序列 \(i_2^\ast[N \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N]\)。
令 \(k_1^\ast\) 为计算 \(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(j_1^\ast)\) 的结果。
令 \(k_2^\ast\) 为计算 \(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(j_2^\ast)\) 的结果。
令 \(k^\ast\) 为计算 \(\href{../exec/numerics.html#op-imul}{\mathrm{imul}}_{|t_2|}(k_1^\ast, k_2^\ast)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(k^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈顶。
\[\begin{split}\begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_2)~t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extmul}}\mathsf{\_}\href{../syntax/instructions.html#syntax-half}{\mathit{half}}\mathsf{\_}t_1\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & i^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)[\href{../syntax/instructions.html#syntax-half}{\mathit{half}}(0, N) \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N] \\ \wedge & j^\ast = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_2)[\href{../syntax/instructions.html#syntax-half}{\mathit{half}}(0, N) \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N] \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(\href{../exec/numerics.html#op-imul}{\mathrm{imul}}_{|t_2|}(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(i^\ast), \href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(j^\ast)))) \end{array}\end{split}\]
其中
\[\begin{split}\begin{array}{lcl} \mathsf{low}(x, y) &=& x \\ \mathsf{high}(x, y) &=& y \\ \end{array}\end{split}\]
\(t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extadd\_pairwise}}\_t_1\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\)
断言：根据 语法，\(N = M / 2\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1\)。
令 \(i^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)\) 的结果。
令 \((j_1~j_2)^\ast\) 为计算 \(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(i^\ast)\) 的结果。
令 \(k^\ast\) 为计算 \(\href{../exec/numerics.html#op-iadd}{\mathrm{iadd}}_{|t_2|}(j_1, j_2)^\ast\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(k^\ast)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c_1)~t_2\mathsf{x}N\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{extadd\_pairwise}}\_t_1\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & (i_1~i_2)^\ast = \href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{|t_1|,|t_2|}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{t_1\mathsf{x}M}(c_1)) \\ \wedge & j^\ast = \href{../exec/numerics.html#op-iadd}{\mathrm{iadd}}_{|t_2|}(i_1, i_2)^\ast \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{t_2\mathsf{x}N}(j^\ast)) \end{array} \end{array}\end{split}\]
表指令
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~x\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\) 存在。
令\(a\) 为表地址\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) 存在。
令\(\mathit{tab}\) 为表实例\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\)。
断言：由于验证，栈顶有一个值类型\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
如果\(i\)不小于\(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)的长度，则
陷入陷阱。
令\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\) 为值\(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\)。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)压入栈顶。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}} \end{array} \\ \qquad (S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = \href{../exec/runtime.html#syntax-val}{\mathit{val}} 的情况) \\ \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (其他情况) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\) 存在。
令\(a\) 为表地址\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) 存在。
令\(\mathit{tab}\) 为表实例\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\)。
断言：由于验证，栈顶有一个引用值。
从栈顶弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)。
断言：由于验证，栈顶有一个值类型\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
如果\(i\)不小于\(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)的长度，则
陷入陷阱。
用\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)替换元素\(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \epsilon \end{array} \\ \qquad (\mathrel{\mbox{如果}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = \href{../exec/runtime.html#syntax-val}{\mathit{val}}) \\ \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.size}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\) 存在。
令\(a\) 为表地址\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) 存在。
令\(\mathit{tab}\) 为表实例\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\)。
令 \(\mathit{sz}\) 为 \(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.size}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}) \end{array} \\ \qquad (\mathrel{\mbox{如果}} |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| = \mathit{sz}) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.grow}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\) 存在。
令\(a\) 为表地址\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) 存在。
令\(\mathit{tab}\) 为表实例\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\)。
令 \(\mathit{sz}\) 为 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) 的长度。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于 验证，栈顶有一个 引用值。
从栈顶弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)。
令 \(\mathit{err}\) 为 \(\href{../syntax/values.html#syntax-int}{\mathit{i32}}\) 值 \(2^{32}-1\)，其中 \(\href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{32}(\mathit{err})\) 为 \(-1\)。
或者
如果 扩展 \(\mathit{tab}\) \(n\) 个条目并使用初始化值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\) 成功，则
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}\) 推入栈中。
否则
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{err}\) 推入栈中。
或者
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{err}\) 推入栈中。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.grow}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x] = a \\ \wedge & \mathit{sz} = |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| \\ \wedge & S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a] = \href{../exec/modules.html#grow-table}{\mathrm{growtable}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a], n, \href{../exec/runtime.html#syntax-val}{\mathit{val}})) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.grow}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{32}^{-1}(-1)) \end{array} \end{array}\end{split}\]
注意
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.grow}}\) 指令是非确定性的。它可能成功，返回旧的表大小 \(\mathit{sz}\)，也可能失败，返回 \({-1}\)。如果引用的表实例定义了最大大小并且会被超出，则**必须**发生失败。但是，在其他情况下也**可能**发生失败。在实践中，选择取决于 资源 可用于 嵌入器。
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\) 存在。
令 \(\mathit{ta}\) 为 表地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}]\) 存在。
令 \(\mathit{tab}\) 为 表实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}]\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于 验证，栈顶有一个 引用值。
从栈顶弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
如果 \(i + n\) 大于 \(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度，则
陷入陷阱。
如果 \(n\) 为 \(0\)，则
返回。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\) 推入栈中。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)压入栈顶。
执行指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x\)。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(i+1)\) 推入栈中。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)压入栈顶。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n-1)\) 推入栈中。
执行指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x\)。
\[\begin{split}\begin{array}{l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & i + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}|) \\[1ex] \end{array} \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \epsilon \\ \qquad (\mathrel{\mbox{否则}}) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i+1)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.fill}}~x) \\ \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\) 存在。
令 \(\mathit{ta}_x\) 为 表地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}_x]\) 存在。
令 \(\mathit{tab}_x\) 为 表实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}_x]\)。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[y]\) 存在。
令 \(\mathit{ta}_y\) 为 表地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[y]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}_y]\) 存在。
令 \(\mathit{tab}_y\) 为 表实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}_y]\)。
断言：由于验证，栈顶有一个值类型为\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于验证，栈顶有一个值类型为\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)。
断言：由于验证，栈顶有一个值类型为\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)。
如果\(s + n\)大于\(\mathit{tab}_y.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)的长度，或者\(d + n\)大于\(\mathit{tab}_x.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)的长度，则
陷入陷阱。
如果\(n = 0\)，则
如果\(d \leq s\)，则
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)压入栈中。
执行指令\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~y\)。
执行指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x\)。
断言：由于之前对表格大小的检查，\(d+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+1)\)压入栈中。
断言：由于之前对表格大小的检查，\(s+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(s+1)\)压入栈中。
否则
断言：由于之前对表格大小的检查，\(d+n-1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+n-1)\)压入栈中。
断言：由于之前对表格大小的检查，\(s+n-1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(s+n-1)\)压入栈中。
执行指令\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~y\)。
执行指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)压入栈中。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n-1)\) 推入栈中。
执行指令\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & s + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[y]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| \\ \vee & d + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}|) \\[1ex] \end{array} \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \epsilon \\ \qquad (\mathrel{\mbox{otherwise}}) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~y)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y) \\ \end{array} \\ \qquad (\mathrel{\mbox{otherwise}}, \mathrel{\mbox{if}} d \leq s) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+n)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s+n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.get}}~y)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.copy}}~x~y) \\ \end{array} \\ \qquad (\mathrel{\mbox{otherwise}}, \mathrel{\mbox{if}} d > s) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)存在。
令 \(\mathit{ta}\) 为 表地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}]\)存在。
令 \(\mathit{tab}\) 为 表实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}]\)。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[y]\)存在。
令\(\mathit{ea}\)为元素地址\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[y]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[\mathit{ea}]\)存在。
令\(\mathit{elem}\)为元素实例\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[\mathit{ea}]\)。
断言：由于验证，栈顶有一个值类型为\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于验证，栈顶有一个值类型为\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)。
断言：由于验证，栈顶有一个值类型为\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)。
如果\(s + n\)大于\(\mathit{elem}.\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}\)的长度，或者\(d + n\)大于\(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)的长度，则
陷入陷阱。
如果\(n = 0\)，则
返回。
令\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)为引用值\(\mathit{elem}.\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}[s]\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)压入栈顶。
执行指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x\)。
断言：由于之前对表格大小的检查，\(d+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+1)\)压入栈中。
断言：由于之前对段大小的检查，\(s+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(s+1)\)压入栈中。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n-1)\) 推入栈中。
执行指令\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & s + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[y]].\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}| \\ \vee & d + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}|) \\[1ex] \end{array} \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \epsilon \\ \qquad (\mathrel{\mbox{otherwise}}) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.set}}~x) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~y) \\ \end{array} \\ \qquad (\mathrel{\mbox{otherwise}}, \mathrel{\mbox{if}} \href{../exec/runtime.html#syntax-val}{\mathit{val}} = S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[y]].\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}[s]) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~x\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]\)存在。
令\(a\)为元素地址\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[a]\)存在。
将\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[a].\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}\)替换为\(\epsilon\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \epsilon \end{array} \\ \qquad (\mathrel{\mbox{如果}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} \href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]].\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}} = \epsilon) \\ \end{array}\end{split}\]
内存指令
注意
加载和存储指令中的对齐方式 \(\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}\) 不会影响语义。它表示访问内存的偏移量 \(\mathit{ea}\) 旨在满足属性 \(\mathit{ea} \mathbin{\mathrm{mod}} 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} = 0\)。WebAssembly 实现可以使用此提示针对预期用途进行优化。违反该属性的未对齐访问仍然允许并且必须成功，无论注释如何。但是，在某些硬件上，它可能会慢得多。
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\) 和 \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(N\) 不是指令的一部分，则
令 \(N\) 为 位宽 \(|t|\)，数值类型 \(t\)。
如果 \(\mathit{ea} + N/8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
令 \(b^\ast\) 为字节序列 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]\)。
如果 \(N\) 和 \(\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}\) 是指令的一部分，则
令 \(n\) 为使得 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n) = b^\ast\) 的整数。
令 \(c\) 为计算 \(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{N,|t|}(n)\) 的结果。
否则
令 \(c\) 为使得 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_t(c) = b^\ast\) 的常量。
将值\(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)推入栈。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(t.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + |t|/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_t(c) = S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} |t|/8]) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(t.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{N,|t|}(n)) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + N/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n) = S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(t.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}({N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}})^?~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{M}\mathsf{x}N\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(\mathit{ea} + M \cdot N /8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
令 \(b^\ast\) 为字节序列 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} M \cdot N /8]\)。
令 \(m_k\) 为使得 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}M}}(m_k) = b^\ast[k \cdot M/8 \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} M/8]\) 的整数。
令 \(W\) 为整数 \(M \cdot 2\)。
令 \(n_k\) 为计算 \(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{M,W}(m_k)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\mathsf{i}W\mathsf{x}N}(n_0 \dots n_{N-1})\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{M}\mathsf{x}N\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + M \cdot N / 8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}M}}(m_k) = S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} + k \cdot M/8 \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} M/8] \\ \wedge & W = M \cdot 2 \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\mathsf{i}W\mathsf{x}N}(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{M,W}(m_0) \dots \href{../exec/numerics.html#op-extend-u}{\mathrm{extend}}^{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}_{M,W}(m_{N-1}))) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{M}\mathsf{x}N\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(\mathit{ea} + N/8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
令 \(b^\ast\) 为字节序列 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]\)。
令 \(n\) 为使得 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n) = b^\ast\) 的整数。
令 \(L\) 为整数 \(128 / N\)。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(n^L)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + N/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n) = S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8] \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(n^L)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(\mathit{ea} + N/8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
令 \(b^\ast\) 为字节序列 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]\)。
令 \(n\) 为使得 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n) = b^\ast\) 的整数。
令 \(c\) 为计算 \(\href{../exec/numerics.html#op-extend-u}{\mathrm{extend}^{\mathsf{u}}}_{N,128}(n)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + N/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n) = S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8] \\ \wedge & c = \href{../exec/numerics.html#op-extend-u}{\mathrm{extend}^{\mathsf{u}}}_{N,128}(n)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~v\)。
断言：由于 验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(\mathit{ea} + N/8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
令 \(b^\ast\) 为字节序列 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]\)。
令 \(r\) 为满足 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(r) = b^\ast\) 的常量。
令 \(L\) 为 \(128 / N\)。
令 \(j^\ast\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(v)\) 的结果。
令 \(c\) 为计算 \(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(j^\ast \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} [x] = r)\) 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\) 推入栈中。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~v)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + N/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(r) = S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8] \\ \wedge & L = 128/N \\ \wedge & c = \href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}^{-1}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(v) \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} [x] = r)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~v)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\) 和 \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶的值类型为 值类型 \(t\)。
从栈中弹出值 \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(N\) 不是指令的一部分，则
令 \(N\) 为 位宽 \(|t|\)，数值类型 \(t\)。
如果 \(\mathit{ea} + N/8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
如果 \(N\) 是指令的一部分，则
令 \(n\) 为计算 \(\href{../exec/numerics.html#op-wrap}{\mathrm{wrap}}_{|t|,N}(c)\) 的结果。
令 \(b^\ast\) 为字节序列 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(n)\)。
否则
令 \(b^\ast\) 为字节序列 \(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_t(c)\)。
用 \(b^\ast\) 替换字节 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(t.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + |t|/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} |t|/8] = \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_t(c)) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(t.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + N/8 \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{替换}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8] = \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(\href{../exec/numerics.html#op-wrap}{\mathrm{wrap}}_{|t|,N}(c))) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(t.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}^?~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}\)。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)。
断言：由于 验证，栈顶的值类型为 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
令 \(\mathit{ea}\) 为整数 \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\)。
如果 \(\mathit{ea} + N/8\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
令 \(L\) 为 \(128/N\)。
令\(j^\ast\) 为计算\(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(c)\) 的结果。
令\(b^\ast\) 为计算\(\href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(j^\ast[x])\) 的结果。
用 \(b^\ast\) 替换字节 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8]\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \epsilon \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & \mathit{ea} = i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}} \\ \wedge & \mathit{ea} + N \leq |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \wedge & L = 128/N \\ \wedge & S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{用}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{ea} \href{../syntax/conventions.html#notation-slice}{\mathrel{\mathbf{:}}} N/8] = \href{../exec/numerics.html#aux-bytes}{\mathrm{bytes}}_{\href{../syntax/values.html#syntax-int}{\mathit{i}N}}(\href{../exec/numerics.html#aux-lanes}{\mathrm{lanes}}_{\href{../syntax/types.html#syntax-valtype}{\mathsf{i}N}\mathsf{x}L}(c)[x])) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.size}}\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
令\(\mathit{sz}\) 为\(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度除以页面大小 的结果。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}\) 推入栈中。
\[\begin{split}\begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.size}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}) \end{array} \\ \qquad (\mathrel{\mbox{如果}} |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| = \mathit{sz}\cdot64\,\mathrm{Ki}) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.grow}}\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令 \(a\) 为 内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 存在。
令 \(\mathit{mem}\) 为 内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)。
令\(\mathit{sz}\) 为\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) 的长度除以页面大小 的结果。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
令 \(\mathit{err}\) 为 \(\href{../syntax/values.html#syntax-int}{\mathit{i32}}\) 值 \(2^{32}-1\)，其中 \(\href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{32}(\mathit{err})\) 为 \(-1\)。
或者
如果将\(\mathit{mem}\) 的大小增加\(n\) 个页面 成功，则
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}\) 推入栈中。
否则
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{err}\) 推入栈中。
或者
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{err}\) 推入栈中。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.grow}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz}) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0] = a \\ \wedge & \mathit{sz} = |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}|/64\,\mathrm{Ki} \\ \wedge & S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{用}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a] = \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a], n)) \\[1ex] \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.grow}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{32}^{-1}(-1)) \end{array} \end{array}\end{split}\]
注意
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.grow}}\) 指令是不确定的。它可能会成功，返回旧的内存大小\(\mathit{sz}\)，也可能失败，返回\({-1}\)。如果引用的内存实例定义了最大大小，并且该大小会被超出，则**必须**发生失败。但是，在其他情况下也**可能**发生失败。在实践中，选择取决于资源 是否可供嵌入器 使用。
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}}\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令\(\mathit{ma}\) 为内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\mathit{ma}]\) 存在。
令\(\mathit{mem}\) 为内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\mathit{ma}]\)。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)。
如果\(d + n\) 大于\(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
如果\(n = 0\)，则
返回。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)压入栈顶。
执行指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}\)。
断言：由于之前对内存大小的检查，\(d+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+1)\)压入栈中。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)压入栈顶。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n-1)\) 推入栈中。
执行指令\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}}\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \qquad (\mathrel{\mbox{如果}} d + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}|) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \epsilon \\ \qquad (\mathrel{\mbox{否则}}) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+1)~\href{../exec/runtime.html#syntax-val}{\mathit{val}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.fill}} \\ \end{array} \\ \qquad (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}}\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令\(\mathit{ma}\) 为内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\mathit{ma}]\) 存在。
令\(\mathit{mem}\) 为内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\mathit{ma}]\)。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)。
断言：由于验证，栈顶有一个值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)。
如果\(s + n\) 大于\(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度或\(d + n\) 大于\(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
如果\(n = 0\)，则
如果\(d \leq s\)，则
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)压入栈中。
执行指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_u}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}\)。
执行指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}\)。
断言：由于之前对内存大小的检查，\(d+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+1)\)压入栈中。
断言：由于之前对内存大小的检查，\(s+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(s+1)\)压入栈中。
否则
断言：由于之前对内存大小的检查，\(d+n-1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+n-1)\)压入栈中。
断言：由于之前对内存大小的检查，\(s+n-1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(s+n-1)\)压入栈中。
执行指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_u}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}\)。
执行指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)压入栈中。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n-1)\) 推入栈中。
执行指令\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}}\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & s + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| \\ \vee & d + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}|) \\[1ex] \end{array} \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \epsilon \\ \qquad (\mathrel{\mbox{否则}}) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_u}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} \\ \end{array} \\ \qquad (\mathrel{\mbox{否则}}, \mathrel{\mbox{如果}} d \leq s) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+n) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s+n)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_u}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.copy}} \\ \end{array} \\ \qquad (\mathrel{\mbox{否则}}, \mathrel{\mbox{如果}} d > s) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\) 存在。
令\(\mathit{ma}\) 为内存地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\mathit{ma}]\) 存在。
令\(\mathit{mem}\) 为内存实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\mathit{ma}]\)。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]\) 存在。
令 \(\mathit{da}\) 为 数据地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[\mathit{da}]\) 存在。
令 \(\mathit{data}\) 为 数据实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[\mathit{da}]\)。
断言：由于 验证，栈顶有一个 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)。
断言：由于 验证，栈顶有一个 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s\)。
断言：由于 验证，栈顶有一个 值类型 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)。
如果 \(s + n\) 大于 \(\mathit{data}.\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}\) 的长度，或者 \(d + n\) 大于 \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则
陷入陷阱。
如果\(n = 0\)，则
返回。
令 \(b\) 为字节 \(\mathit{data}.\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}[s]\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d\)压入栈中。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~b\) 推入栈中。
执行指令\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}\)。
断言：由于之前对内存大小的检查，\(d+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(d+1)\)压入栈中。
断言：由于之前对内存大小的检查，\(s+1 < 2^{32}\)。
将值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(s+1)\)压入栈中。
将值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n-1)\) 推入栈中。
执行指令 \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{如果}} & s + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]].\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}| \\ \vee & d + n > |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[0]].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}|) \\[1ex] \end{array} \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad S; F; \epsilon \\ \qquad (\mathrel{\mbox{否则}}) \\[1ex] S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n+1)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x) \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow} \\ \qquad S; F; \begin{array}[t]{@{}l@{}} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~b)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~\{ \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}~0, \href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}~0 \}) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~d+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~s+1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~x) \\ \end{array} \\ \qquad (\mathrel{\mbox{否则}}, \mathrel{\mbox{如果}} b = S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]].\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}[s]) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~x\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]\) 存在。
令 \(a\) 为 数据地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]\)。
断言：由于 验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[a]\) 存在。
将 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[a]\) 替换为 数据实例 \(\{\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\epsilon\}\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \epsilon \end{array} \\ \qquad (\mathrel{\mbox{如果}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{用}}} \href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}[x]] = \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\epsilon \}) \\ \end{array}\end{split}\]
控制指令
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\)
什么也不做。
\[\begin{array}{lcl@{\qquad}l} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \epsilon \end{array}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\)
陷入陷阱。
\[\begin{array}{lcl@{\qquad}l} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\) 已定义。
令 \( [t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n] \) 为 函数类型 \(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\)。
令 \(L\) 为一个元数为 \(n\) 且延续为块末尾的标签。
断言：由于验证，栈顶至少有\(m\)个值。
从栈中弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\)。
进入带有标签\(L\)的块\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)。
\[\begin{split}~\\[-1ex] \begin{array}{lcl} F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& F; \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\&&\quad (\mathrel{\mbox{if}} \href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\mathit{bt}) = [t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n]) \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)
令 \(F\) 为当前 帧。
断言：由于 验证，\(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\) 已定义。
令 \( [t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n] \) 为 函数类型 \(\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}})\)。
令\(L\)为元数为\(m\)且其延续为循环开头的标签。
断言：由于验证，栈顶至少有\(m\)个值。
从栈中弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m\)。
进入带有标签\(L\)的块\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)。
\[\begin{split}~\\[-1ex] \begin{array}{lcl} F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& F; \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_m\{\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^m~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\&&\quad (\mathrel{\mbox{if}} \href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\mathit{bt}) = [t_1^m] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^n]) \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)
断言：由于验证，栈顶有一个值类型\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)。
如果\(c\)不为零，则
执行块指令\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)。
否则
执行块指令\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)。
\[\begin{split}~\\[-1ex] \begin{array}{lcl} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\&&\quad (\mathrel{\mbox{if}} c \neq 0) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\mathit{bt}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\&&\quad (\mathrel{\mbox{if}} c = 0) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\)
断言：由于验证，栈包含至少\(l+1\)个标签。
令\(L\)为栈中从顶部开始，从零开始计数的第\(l\)个标签。
令\(n\)为\(L\)的元数。
断言：由于验证，栈顶至少有\(n\)个值。
从栈中弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)。
重复\(l+1\)次
当栈顶为值时，执行
从栈中弹出该值。
断言：由于验证，栈顶现在是一个标签。
从栈中弹出该标签。
将值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)压入栈中。
跳转到\(L\)的延续。
\[\begin{split}~\\[-1ex] \begin{array}{lcl@{\qquad}l} \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^l[\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l)]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l\)
断言：由于验证，栈顶有一个值类型\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈中弹出值 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)。
如果\(c\)不为零，则
执行指令\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\)。
否则
什么也不做。
\[\begin{split}~\\[-1ex] \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l) & (\mathrel{\mbox{if}} c \neq 0) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \epsilon & (\mathrel{\mbox{if}} c = 0) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N\)
断言：由于验证，栈顶有一个值类型\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\)的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
如果\(i\)小于\(l^\ast\)的长度，则
令\(l_i\)为标签\(l^\ast[i]\)。
执行指令\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l_i\)。
否则
执行指令\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l_N\)。
\[\begin{split}~\\[-1ex] \begin{array}{lcl@{\qquad}l} (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l_i) & (\mathrel{\mbox{if}} l^\ast[i] = l_i) \\ (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l_N) & (\mathrel{\mbox{if}} |l^\ast| \leq i) \\ \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\)
令 \(F\) 为当前 帧。
令\(n\)为\(F\)的元数。
断言：由于验证，栈顶至少有\(n\)个值。
从栈中弹出结果\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)。
断言：由于验证，栈至少包含一个帧。
当栈顶不是帧时，执行
从栈中弹出栈顶元素。
断言：栈顶是帧\(F\)。
从栈中弹出该帧。
将\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)压入栈中。
跳转到最初压入该帧的调用的下一条指令。
\[\begin{split}~\\[-1ex] \begin{array}{lcl@{\qquad}l} \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^k[\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n \end{array}\end{split}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x]\)存在。
令 \(a\) 为函数地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x]\)。
调用地址\(a\)处的函数实例。
\[\begin{array}{lcl@{\qquad}l} F; (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& F; (\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) & (\mathrel{\mbox{if}} F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x] = a) \end{array}\]
\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y\)
令 \(F\) 为当前 帧。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)存在。
令 \(\mathit{ta}\) 为 表地址 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]\)。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}]\)存在。
令 \(\mathit{tab}\) 为 表实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\mathit{ta}]\)。
断言：由于验证，\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[y]\) 存在。
令 \(\mathit{ft}_{\mathrm{expect}}\) 为 函数类型 \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[y]\)。
断言：由于验证，栈顶有一个 值类型 为 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 的值。
从栈顶弹出值\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\)。
如果\(i\)不小于\(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)的长度，则
陷入陷阱。
令 \(r\) 为 引用 \(\mathit{tab}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\)。
如果 \(r\) 为 \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t\)，则
陷入陷阱。
断言：由于表格变异的验证，\(r\) 是一个 函数引用。
令 \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~a\) 为 函数引用 \(r\)。
断言：由于表格变异的验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\) 存在。
令 \(\mathit{f}\) 为 函数实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\)。
令 \(\mathit{ft}_{\mathrm{actual}}\) 为 函数类型 \(\mathit{f}.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\)。
如果 \(\mathit{ft}_{\mathrm{actual}}\) 和 \(\mathit{ft}_{\mathrm{expect}}\) 不同，则
陷入陷阱。
调用地址\(a\)处的函数实例。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x]].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = \href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~a \\ \wedge & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = f \\ \wedge & F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[y] = f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} S; F; (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i)~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x~y) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array} \\ \qquad (\mathrel{\mbox{otherwise}}) \end{array}\end{split}\]
函数调用
以下辅助规则定义了通过其中一个调用指令调用函数实例并从中返回的语义。
断言：由于验证，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\) 存在。
令 \(f\) 为 函数实例，\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\)。
令 \([t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m]\) 为 函数类型 \(f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\)。
令 \(t^\ast\) 为 值类型 列表 \(f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}.\href{../syntax/modules.html#syntax-func}{\mathsf{locals}}\)。
令 \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) 为 表达式 \(f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}.\href{../syntax/modules.html#syntax-func}{\mathsf{body}}\)。
断言：由于验证，栈顶有 \(n\) 个值。
从栈中弹出值\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)。
令 \(F\) 为 帧 \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#default-val}{\mathrm{default}}_t)^\ast \}\)。
将 \(F\) 的激活（元数为 \(m\)）推入栈中。
令 \(L\) 为元数为 \(m\) 且延续为函数末尾的标签。
进入 带有标签 \(L\) 的指令序列 \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_m\{F\}~\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_m\{\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = f \\ \wedge & f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} = [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ \wedge & f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}} = \{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~t^k, \href{../syntax/modules.html#syntax-func}{\mathsf{body}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \} \\ \wedge & F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~f.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}, ~\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#default-val}{\mathrm{default}}_t)^k \}) \end{array} \\ \end{array}\end{split}\]
从函数返回
当到达函数的末尾且没有跳转（即 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\)）或陷阱终止它时，执行以下步骤。
令 \(F\) 为当前 帧。
令 \(n\) 为 \(F\) 的激活的元数。
断言：由于验证，栈顶有 \(n\) 个值。
从栈中弹出结果\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)。
断言：由于验证，帧 \(F\) 现在位于栈顶。
从栈中弹出该帧。
将 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\) 推回栈中。
跳转到原始调用的下一条指令。
\[\begin{split}~\\[-1ex] \begin{array}{lcl@{\qquad}l} \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n \end{array}\end{split}\]
宿主函数
调用宿主函数的行为是不确定的。它可能以陷阱终止，也可能正常返回。但是，在后一种情况下，它必须根据其函数类型，在栈上消耗和生成正确数量和类型的 WebAssembly 值。
主机函数也可以修改存储。但是，所有存储修改都必须导致原始存储的扩展，即它们只能修改可变内容，并且不能删除实例。此外，生成的存储必须是有效的，即其中的所有数据和代码都具有良好的类型。
\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; \href{../exec/runtime.html#syntax-result}{\mathit{result}} \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m], \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf} \} \\ \wedge & (S'; \href{../exec/runtime.html#syntax-result}{\mathit{result}}) \in \mathit{hf}(S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n)) \\ \end{array} \\ \begin{array}{lcl@{\qquad}l} S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~a) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m], \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf} \} \\ \wedge & \bot \in \mathit{hf}(S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n)) \\ \end{array} \\ \end{array}\end{split}\]
这里，\(\mathit{hf}(S; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n)\) 表示主机函数 \(\mathit{hf}\) 在当前存储 \(S\) 中使用参数 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\) 的实现定义执行。它产生一组可能的结果，其中每个元素要么是一对修改后的存储 \(S'\) 和一个结果，要么是表示发散的特殊值 \(\bot\)。如果至少存在一个参数，其结果集不是单一的，则主机函数是非确定性的。
为了使 WebAssembly 实现健全（在存在主机函数的情况下），每个主机函数实例都必须是有效的，这意味着它符合合适的先决条件和后置条件：在有效存储 \(S\) 下，并且给定与指定的参数类型 \(t_1^n\) 匹配的参数 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\)，执行主机函数必须产生一组非空可能的结果，每个结果要么是发散，要么包含一个有效的存储 \(S'\)（它是 \(S\) 的扩展）和与指定的返回类型 \(t_2^m\) 匹配的结果。所有这些概念都在附录中进行了精确定义。
注意
主机函数可以通过调用从模块中导出的函数来回调到 WebAssembly 中。但是，任何此类调用的影响都包含在主机函数允许的非确定性行为中。
