健全性¶

WebAssembly 的类型系统是健全的，这意味着它在 WebAssembly 语义方面既具有类型安全又具有内存安全。例如

验证期间声明和派生的所有类型在运行时都会被遵守；例如，每个局部变量或全局变量只包含类型正确的的值，每个指令只应用于预期类型的操作数，并且每个函数调用始终评估为正确类型的结果（如果它不陷入或发散）。
没有内存位置会被读取或写入，除非这些位置被程序明确定义，即作为局部变量、全局变量、表中的元素或线性内存中的位置。
没有未定义的行为，即执行规则涵盖了有效程序中可能出现的任何情况，并且这些规则是相互一致的。

健全性也有助于确保其他属性，最显著的是函数和模块作用域的封装：没有局部变量可以在其自身函数之外访问，并且没有模块组件可以在其自身模块之外访问，除非它们被明确导出或导入。

定义 WebAssembly 验证的类型规则只涵盖 WebAssembly 程序的静态组件。为了准确地陈述和证明健全性，类型规则必须扩展到抽象运行时的动态组件，即存储、配置和管理指令。[1]

结果¶

结果可以按结果类型进行分类，如下所示。

结果 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\)¶

对于值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) 在 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 中
- 值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) 在某种值类型 \(t_i\)下是有效的。
设 \(t^\ast\) 为所有 \(t_i\) 的连接。
那么该结果在结果类型 \([t^\ast]\) 下是有效的。

\[\frac{ (S \href{../exec/modules.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t)^\ast }{ S \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast : [t^\ast] }\]

结果 \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\)¶

该结果在结果类型 \([t^\ast]\) 下是有效的，对于任何值类型序列 \(t^\ast\) 均是如此。

\[\frac{ }{ S \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} : [t^\ast] }\]

存储有效性¶

以下类型规则指定了何时运行时存储 \(S\) 是有效的。有效存储必须包含函数、表、内存、全局变量和模块实例，这些实例本身相对于 \(S\) 是有效的。

为此，每种实例都由相应的函数、表、内存或全局变量类型进行分类。模块实例由模块上下文进行分类，模块上下文是作为模块类型重新利用的常规上下文，用于描述模块定义的索引空间。

存储 \(S\)¶

在 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) 中，每个函数实例 \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_i\) 必须在某种函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) 下是有效的。
在 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) 中，每个表实例 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i\) 必须在某种表类型 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_i\) 下是有效的。
在 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) 中，每个内存实例 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i\) 必须在某种内存类型 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\) 下是有效的。
在 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) 中，每个全局变量实例 \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_i\) 必须在某种全局变量类型 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\) 下是有效的。
在 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\) 中，每个元素实例 \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_i\) 必须在某种引用类型 \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_i\) 下是有效的。
在 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\) 中，每个数据实例 \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_i\) 必须是有效的。
那么该存储是有效的。

\[\begin{split}~\\[-1ex] \frac{ \begin{array}{@{}c@{}} (S \href{../appendix/properties.html#valid-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}})^\ast \qquad (S \href{../appendix/properties.html#valid-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}})^\ast \\ (S \href{../appendix/properties.html#valid-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}})^\ast \qquad (S \href{../appendix/properties.html#valid-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}})^\ast \\ (S \href{../appendix/properties.html#valid-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}})^\ast \qquad (S \href{../appendix/properties.html#valid-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} \mathrel{\mbox{ok}})^\ast \\ S = \{ \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}^\ast, \href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}^\ast \} \end{array} }{ \href{../appendix/properties.html#valid-store}{\vdash} S \mathrel{\mbox{ok}} }\end{split}\]

函数实例 \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}\}\)¶

该函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 必须是有效的。
模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) 必须在某个上下文 \(C\) 中是有效的。
在上下文 \(C\) 下，函数 \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) 必须在函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 下是有效的。
那么函数实例在函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 下是有效的。

\[\frac{ \href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}} \qquad S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C \qquad C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ S \href{../appendix/properties.html#valid-funcinst}{\vdash} \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}\} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\]

宿主函数实例 \(\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf}\}\)¶

该函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 必须是有效的。
令 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) 为函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)。
对于每个有效的存储 \(S_1\) 扩展 \(S\) 以及每个其类型与 \(t_1^\ast\) 相符的值序列 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\)
- 执行 \(\mathit{hf}\) 在存储 \(S_1\) 中使用参数 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 将得到一组非空的可能结果。
- 对于此集合中的每个元素 \(R\)
  - 要么 \(R\) 必须为 \(\bot\) （即发散）。
  - 要么 \(R\) 由一个有效的存储 \(S_2\) 扩展 \(S_1\) 以及一个其类型与 \([t_2^\ast]\) 相符的结果 \(\href{../exec/runtime.html#syntax-result}{\mathit{result}}\) 组成。
那么函数实例在函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 下是有效的。

\[\begin{split}\frac{ \begin{array}[b]{@{}l@{}} \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} \\ \end{array} \quad \begin{array}[b]{@{}l@{}} \forall S_1, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast,~ {\href{../appendix/properties.html#valid-store}{\vdash} S_1 \mathrel{\mbox{ok}}} \wedge {\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S_1} \wedge {S_1 \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast : [t_1^\ast]} \Longrightarrow {} \\ \qquad \mathit{hf}(S_1; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \supset \emptyset \wedge {} \\ \qquad \forall R \in \mathit{hf}(S_1; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast),~ R = \bot \vee {} \\ \qquad\qquad \exists S_2, \href{../exec/runtime.html#syntax-result}{\mathit{result}},~ {\href{../appendix/properties.html#valid-store}{\vdash} S_2 \mathrel{\mbox{ok}}} \wedge {\href{../appendix/properties.html#extend-store}{\vdash} S_1 \href{../appendix/properties.html#extend}{\preceq} S_2} \wedge {S_2 \href{../appendix/properties.html#valid-result}{\vdash} \href{../exec/runtime.html#syntax-result}{\mathit{result}} : [t_2^\ast]} \wedge R = (S_2; \href{../exec/runtime.html#syntax-result}{\mathit{result}}) \end{array} }{ S \href{../appendix/properties.html#valid-funcinst}{\vdash} \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast], \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\mathit{hf}\} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\end{split}\]

注意

此规则指出，如果存储和参数满足适当的先决条件，则执行宿主函数必须满足存储和结果的适当后置条件。后置条件与执行规则中调用宿主函数的条件相匹配。

调用函数的任何存储都被认为是当前存储的扩展。这样，函数本身就能对未来的存储做出充分的假设。

表格实例 \(\{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t), \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\)¶

表格类型 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) 必须是有效的。
\(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast\) 的长度必须等于 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\)。
对于表格元素 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n\) 中的每个引用 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_i\)
- 引用 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_i\) 必须在引用类型 \(t\) 下是有效的。
那么表格实例在表格类型 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) 下是有效的。

\[\frac{ \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t \mathrel{\mbox{ok}} \qquad n = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}} \qquad (S \vdash \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} : t)^n }{ S \href{../appendix/properties.html#valid-tableinst}{\vdash} \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t), \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \} : \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t }\]

内存实例 \(\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^\ast \}\)¶

内存类型 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) 必须是有效的。
\(b^\ast\) 的长度必须等于 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\) 乘以页面大小 \(64\,\mathrm{Ki}\)。
那么内存实例在内存类型 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) 下是有效的。

\[\frac{ \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \mathrel{\mbox{ok}} \qquad n = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}.\href{../syntax/types.html#syntax-limits}{\mathsf{min}} \cdot 64\,\mathrm{Ki} }{ S \href{../appendix/properties.html#valid-meminst}{\vdash} \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^n \} : \href{../syntax/types.html#syntax-limits}{\mathit{limits}} }\]

全局实例 \(\{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \}\)¶

全局类型 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) 必须是有效的。
值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\) 必须在值类型 \(t\) 下是有效的。
那么全局实例在全局类型 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) 下是有效的。

\[\frac{ \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t \mathrel{\mbox{ok}} \qquad S \href{../exec/modules.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t }{ S \href{../appendix/properties.html#valid-globalinst}{\vdash} \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \} : \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t }\]

元素实例 \(\{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\)¶

对于元素 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n\) 中的每个引用 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_i\)
- 引用 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_i\) 必须在引用类型 \(t\) 下是有效的。
那么元素实例在引用类型 \(t\) 下是有效的。

\[\frac{ (S \vdash \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} : t)^\ast }{ S \href{../appendix/properties.html#valid-eleminst}{\vdash} \{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \} : t }\]

数据实例 \(\{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b^\ast \}\)¶

数据实例是有效的。

\[\frac{ }{ S \href{../appendix/properties.html#valid-datainst}{\vdash} \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b^\ast \} \mathrel{\mbox{ok}} }\]

导出实例 \(\{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \}\)¶

该外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}\) 必须与某个有效的外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) 匹配。
然后导出实例是有效的。

\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} }{ S \href{../appendix/properties.html#valid-exportinst}{\vdash} \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \} \mathrel{\mbox{ok}} }\]

模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)¶

在 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}\) 中的每个函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) 必须是有效的。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}\) 中的每个函数地址 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\)，外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) 必须与某个有效的外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'_i\) 匹配。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}\) 中的每个表格地址 \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\)，外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) 必须与某个有效的外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_i\) 匹配。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}\) 中的每个内存地址 \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\)，外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) 必须与某个有效的外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\) 匹配。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}\) 中的每个全局地址 \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\)，外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) 必须与某个有效的外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\) 匹配。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}\) 中的每个元素地址 \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\)，元素实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i]\) 必须是有效的，并且与某个引用类型 \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_i\) 匹配。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}\) 中的每个数据地址 \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\)，数据实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i]\) 必须是有效的。
在 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\) 中的每个导出实例 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) 必须是有效的。
对于 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\) 中的每个导出实例 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\)，名称 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}\) 必须与 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\) 中出现的任何其他名称不同。
令 \({\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'}^\ast\) 是所有 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'_i\) 按顺序的串联。
令 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}^\ast\) 是所有 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_i\) 按顺序的串联。
令 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}^\ast\) 是所有 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_i\) 按顺序的串联。
令 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^\ast\) 是所有 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_i\) 按顺序的串联。
令 \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}^\ast\) 是所有 \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_i\) 按顺序的串联。
令 \(m\) 是 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}\) 的长度。
令 \(n\) 是 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}}\) 的长度。
令 \(x^\ast\) 是从 \(0\) 到 \(m-1\) 的函数索引序列。
那么该模块实例在上下文 \(\{\href{../valid/conventions.html#context}{\mathsf{types}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast,\) \(\href{../valid/conventions.html#context}{\mathsf{funcs}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'}^\ast,\) \(\href{../valid/conventions.html#context}{\mathsf{tables}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}^\ast,\) \(\href{../valid/conventions.html#context}{\mathsf{mems}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}^\ast,\) \(\href{../valid/conventions.html#context}{\mathsf{globals}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^\ast,\) \(\href{../valid/conventions.html#context}{\mathsf{elems}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}^\ast,\) \(\href{../valid/conventions.html#context}{\mathsf{datas}}~{\mathrel{\mbox{ok}}}^n,\) \(\href{../valid/conventions.html#context}{\mathsf{refs}}~x^\ast\}\) 中是有效的。

\[\begin{split}~\\[-1ex] \frac{ \begin{array}{@{}c@{}} (\href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}})^\ast \\ (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}')^\ast \qquad (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}})^\ast \\ (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}})^\ast \qquad (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}})^\ast \\ (S \href{../appendix/properties.html#valid-eleminst}{\vdash} S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}] : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}})^\ast \qquad (S \href{../appendix/properties.html#valid-datainst}{\vdash} S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}[\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}] \mathrel{\mbox{ok}})^n \\ (S \href{../appendix/properties.html#valid-exportinst}{\vdash} \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} \mathrel{\mbox{ok}})^\ast \qquad (\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}})^\ast ~\mbox{disjoint} \end{array} }{ S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \{ \begin{array}[t]{@{}l@{~}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^n, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} : \{ \begin{array}[t]{@{}l@{~}l@{}} \href{../valid/conventions.html#context}{\mathsf{types}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\ \href{../valid/conventions.html#context}{\mathsf{funcs}} & {\href{../syntax/types.html#syntax-functype}{\mathit{functype}}'}^\ast, \\ \href{../valid/conventions.html#context}{\mathsf{tables}} & \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}^\ast, \\ \href{../valid/conventions.html#context}{\mathsf{mems}} & \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}^\ast, \\ \href{../valid/conventions.html#context}{\mathsf{globals}} & \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}^\ast, \\ \href{../valid/conventions.html#context}{\mathsf{elems}} & \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}^\ast, \\ \href{../valid/conventions.html#context}{\mathsf{datas}} & {\mathrel{\mbox{ok}}}^n, \\ \href{../valid/conventions.html#context}{\mathsf{refs}} & 0 \dots (|\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast|-1) ~\} \end{array} \end{array} }\end{split}\]

配置有效性¶

为了将 WebAssembly 的类型系统与其执行语义联系起来，指令的类型规则必须扩展到配置 \(S;T\)，这将存储与执行线程联系起来。

配置和线程按其结果类型进行分类。除了存储 \(S\) 之外，线程还在返回类型 \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\) 下进行类型化，该类型控制是否以及以何种类型允许使用 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}}\) 指令。这种类型在管理 \(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}\) 指令内部的指令序列中除外 (\(\epsilon\))。

最后，帧按帧上下文进行分类，帧上下文扩展了帧关联的模块实例的模块上下文，并包含该帧包含的局部变量。

配置 \(S;T\)¶

存储 \(S\) 必须是有效的。
在不允许返回类型的条件下，线程 \(T\) 必须是有效的，并且具有某种结果类型 \([t^\ast]\)。
然后，配置使用结果类型 \([t^\ast]\) 是有效的。

\[\frac{ \href{../appendix/properties.html#valid-store}{\vdash} S \mathrel{\mbox{ok}} \qquad S; \epsilon \href{../appendix/properties.html#valid-thread}{\vdash} T : [t^\ast] }{ \href{../appendix/properties.html#valid-config}{\vdash} S; T : [t^\ast] }\]

线程 \(F;\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)¶

令 \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\) 为当前允许的返回类型。
帧 \(F\) 必须是有效的，并且具有上下文 \(C\)。
令 \(C'\) 与 \(C\) 相同，但 \(\href{../valid/conventions.html#context}{\mathsf{return}}\) 设置为 \(\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?\)。
在上下文 \(C'\) 下，指令序列 \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) 必须是有效的，并且具有某种类型 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast]\)。
然后，该线程使用结果类型 \([t^\ast]\) 是有效的。

\[\frac{ S \href{../appendix/properties.html#valid-frame}{\vdash} F : C \qquad S; C,\href{../valid/conventions.html#context}{\mathsf{return}}~\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^\ast] }{ S; \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^? \href{../appendix/properties.html#valid-thread}{\vdash} F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t^\ast] }\]

帧 \(\{\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\}\)¶

模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) 必须是有效的，并且具有某种模块上下文 \(C\)。
每个值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) 在 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 中必须是有效的，并且具有某种值类型 \(t_i\)。
令 \(t^\ast\) 为所有 \(t_i\) 按顺序连接的结果。
令 \(C'\) 与 \(C\) 相同，但将值类型 \(t^\ast\) 添加到 \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) 向量前面。
然后，该帧使用帧上下文 \(C'\) 是有效的。

\[\frac{ S \href{../appendix/properties.html#valid-moduleinst}{\vdash} \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} : C \qquad (S \href{../exec/modules.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t)^\ast }{ S \href{../appendix/properties.html#valid-frame}{\vdash} \{\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\} : (C, \href{../valid/conventions.html#context}{\mathsf{locals}}~t^\ast) }\]

管理指令¶

指定管理指令的类型规则如下。除了上下文 \(C\) 之外，这些指令的类型化是在给定的存储 \(S\) 下定义的。为此，所有先前的类型化判断 \(C \vdash \mathit{prop}\) 都被概括为包括存储，如 \(S; C \vdash \mathit{prop}\)，通过将 \(S\) 隐式添加到所有规则中 - \(S\) 从未被现有规则修改，但它在下面给出的管理指令的额外规则中被访问。

\(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\)¶

该指令的类型为 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\)，对于任何值类型序列 \(t_1^\ast\) 和 \(t_2^\ast\) 均有效。

\[\frac{ }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

\(\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}}\)¶

该指令的类型为 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-reftype}{\mathsf{externref}}]\)。

\[\frac{ }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-reftype}{\mathsf{externref}}] }\]

\(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)¶

该外部函数值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) 必须是有效的，并具有外部函数类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)。
那么该指令的类型为 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}}]\)。

\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}}] }\]

\(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)¶

该外部函数值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) 必须是有效的，并具有外部函数类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}} ([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast])\)。
那么该指令的类型为 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\)。

\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

\(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶

指令序列 \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\) 必须是有效的，并具有某些类型 \([t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^*]\)。
令 \(C'\) 与 \(C\) 相同，但其上下文中的结果类型 \([t_1^n]\) 被添加到 \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) 向量的前端。
在上下文 \(C'\) 下，指令序列 \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) 必须是有效的，并具有类型 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^*]\)。
那么该复合指令的类型为 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^*]\)。

\[\frac{ S; C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast : [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^*] \qquad S; C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_1^n] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^*] }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_0^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^*] }\]

\(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶

在返回类型 \([t^n]\) 下，该线程 \(F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) 必须是有效的，并具有结果类型 \([t^n]\)。
那么该复合指令的类型为 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^n]\)。

\[\frac{ S; [t^n] \href{../valid/instructions.html#valid-instr-seq}{\vdash} F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t^n] }{ S; C \href{../appendix/properties.html#valid-instr-admin}{\vdash} \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t^n] }\]

存储扩展¶

程序可以修改存储及其包含的实例。任何此类修改都必须遵守某些不变式，例如不删除已分配的实例或更改不可变定义。虽然这些不变式是 WebAssembly 指令和模块执行语义固有的，但宿主函数并不会自动遵守它们。因此，必须将所需的不变式表述为对调用宿主函数的明确约束。只有当嵌入器确保这些约束时，健壮性才成立。

必要的约束由存储扩展的概念进行编码：当以下规则成立时，存储状态 \(S'\) 扩展状态 \(S\)，记为 \(S \href{../appendix/properties.html#extend}{\preceq} S'\)。

注意

扩展并不意味着新存储是有效的，有效性在上面单独定义。

存储 \(S\)¶

\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) 的长度不能缩短。
\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) 的长度不能缩短。
\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) 的长度不能缩短。
\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) 的长度不能缩短。
\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\) 的长度不能缩短。
\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\) 的长度不能缩短。
对于原始 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) 中的每个函数实例 \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_i\)，新的函数实例必须是旧实例的扩展。
对于原始 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) 中的每个表格实例 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i\)，新的表格实例必须是旧实例的扩展。
对于原始 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) 中的每个内存实例 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i\)，新的内存实例必须是旧实例的扩展。
对于原始 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) 中的每个全局实例 \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_i\)，新的全局实例必须是旧实例的扩展。
对于原始 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\) 中的每个元素实例 \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_i\)，新的元素实例必须是旧实例的扩展。
对于原始 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\) 中的每个数据实例 \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_i\)，新的数据实例必须是旧实例的扩展。

\[\begin{split}\frac{ \begin{array}{@{}ccc@{}} S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} = \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} = {\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_2^\ast & (\href{../appendix/properties.html#extend-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} = {\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_2^\ast & (\href{../appendix/properties.html#extend-tableinst}{\vdash} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} = {\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'_1}^\ast~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_2^\ast & (\href{../appendix/properties.html#extend-meminst}{\vdash} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} = \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} = {\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}'_1}^\ast~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_2^\ast & (\href{../appendix/properties.html#extend-globalinst}{\vdash} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}} = \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}} = {\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}'_1}^\ast~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_2^\ast & (\href{../appendix/properties.html#extend-eleminst}{\vdash} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}'_1)^\ast \\ S_1.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}} = \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_1^\ast & S_2.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}} = {\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}'_1}^\ast~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_2^\ast & (\href{../appendix/properties.html#extend-datainst}{\vdash} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}_1 \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}'_1)^\ast \\ \end{array} }{ \href{../appendix/properties.html#extend-store}{\vdash} S_1 \href{../appendix/properties.html#extend}{\preceq} S_2 }\end{split}\]

函数实例 \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\)¶

函数实例必须保持不变。

\[\frac{ }{ \href{../appendix/properties.html#extend-funcinst}{\vdash} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} \href{../appendix/properties.html#extend}{\preceq} \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} }\]

表格实例 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\)¶

表格类型 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\) 必须保持不变。
\(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度不能缩短。

\[\frac{ n_1 \leq n_2 }{ \href{../appendix/properties.html#extend-tableinst}{\vdash} \{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\mathit{tt}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}_1^?)^{n_1}\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\mathit{tt}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}_2^?)^{n_2}\} }\]

内存实例 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\)¶

内存类型 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\) 必须保持不变。
\(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度不能缩短。

\[\frac{ n_1 \leq n_2 }{ \href{../appendix/properties.html#extend-meminst}{\vdash} \{\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\mathit{mt}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b_1^{n_1}\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\mathit{mt}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b_2^{n_2}\} }\]

全局实例 \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\)¶

全局类型 \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\) 必须保持不变。
令 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) 为 \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\) 的结构。
如果 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) 是 \(\href{../syntax/types.html#syntax-mut}{\mathsf{const}}\)，那么值 \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\) 必须保持不变。

\[\frac{ \href{../syntax/types.html#syntax-mut}{\mathit{mut}} = \href{../syntax/types.html#syntax-mut}{\mathsf{var}} \vee \href{../exec/runtime.html#syntax-val}{\mathit{val}}_1 = \href{../exec/runtime.html#syntax-val}{\mathit{val}}_2 }{ \href{../appendix/properties.html#extend-globalinst}{\vdash} \{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}_1\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}_2\} }\]

元素实例 \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\)¶

向量 \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}.\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}\) 必须保持不变或缩短到长度 0。

\[\frac{ \mathit{fa}_1^\ast = \mathit{fa}_2^\ast \vee \mathit{fa}_2^\ast = \epsilon }{ \href{../appendix/properties.html#extend-eleminst}{\vdash} \{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\mathit{fa}_1^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\mathit{fa}_2^\ast\} }\]

数据实例 \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\)¶

向量 \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}.\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}\) 必须保持不变或缩短到长度 0。

\[\frac{ b_1^\ast = b_2^\ast \vee b_2^\ast = \epsilon }{ \href{../appendix/properties.html#extend-datainst}{\vdash} \{\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b_1^\ast\} \href{../appendix/properties.html#extend}{\preceq} \{\href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b_2^\ast\} }\]

定理¶

在有效配置的定义下，标准的健壮性定理成立。 [2] [3]

定理（保持）。 如果一个配置 \(S;T\) 是有效的，具有结果类型 \([t^\ast]\) （即，\(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]\)），并且步骤到 \(S';T'\) （即，\(S;T \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S';T'\)），那么 \(S';T'\) 是具有相同结果类型（即，\(\href{../appendix/properties.html#valid-config}{\vdash} S';T' : [t^\ast]\)）的有效配置。此外，\(S'\) 是 \(S\) 的扩展（即，\(\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S'\)）。

一个终端线程是指其指令序列为结果的线程。终端配置是指其线程为终端的配置。

定理（进展）。 如果一个配置 \(S;T\) 是有效的（即，\(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]\) 对于某个结果类型 \([t^\ast]\)），那么它要么是终端的，要么可以步骤到某个配置 \(S';T'\) （即，\(S;T \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S';T'\)）。

从保持和进展定理中，可以直接得出 WebAssembly 类型系统的健壮性。

推论（健壮性）。 如果一个配置 \(S;T\) 是有效的（即，\(\href{../appendix/properties.html#valid-config}{\vdash} S;T : [t^\ast]\) 对于某个结果类型 \([t^\ast]\)），那么它要么发散，要么经过有限次数的步骤到达一个终端配置 \(S';T'\) （即，\(S;T \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S';T'\)），该终端配置是有效并且具有相同的结果类型（即，\(\href{../appendix/properties.html#valid-config}{\vdash} S';T' : [t^\ast]\)），并且 \(S'\) 是 \(S\) 的扩展（即，\(\href{../appendix/properties.html#extend-store}{\vdash} S \href{../appendix/properties.html#extend}{\preceq} S'\)）。

换句话说，有效配置中的每个线程要么永远运行，要么陷入陷阱，要么以具有预期类型的结果终止。因此，给定一个有效存储，由实例化或调用有效模块定义的任何计算都不会“崩溃”或以本规范中未涵盖的方式（错误）执行。