约定

验证检查 WebAssembly 模块是否格式正确。只有有效的模块才能实例化。

有效性由一个针对 抽象语法 的 模块 及其内容的 *类型系统* 定义。对于每个抽象语法片段，都存在一个类型规则，用于指定对其适用的约束。所有规则都以两种 *等效* 形式给出

  1. 以 *散文* 形式描述，以直观的形式描述含义。

  2. 以 *正式表示法* 形式描述，以数学形式描述规则。 [1]

注意

散文和正式规则是等效的，因此 *不需要* 理解正式表示法即可阅读本规范。形式化提供了更简洁的描述，其表示法在编程语言语义中广泛使用，并且易于进行数学证明。

在这两种情况下，规则都是以 *声明式* 方式制定的。也就是说，它们只制定约束，不定义算法。在 附录 中提供了根据本规范对指令序列进行类型检查的健全且完整的算法的骨架。

上下文

单个定义的有效性是相对于一个 *上下文* 指定的，该上下文收集了有关周围 模块 和作用域内定义的相关信息

  • *类型*：当前模块中定义的类型列表。

  • *函数*：当前模块中声明的函数列表，以其函数类型表示。

  • *表*：当前模块中声明的表列表，以其表类型表示。

  • *内存*：当前模块中声明的内存列表，以其内存类型表示。

  • *全局变量*：当前模块中声明的全局变量列表，以其全局变量类型表示。

  • *元素段*：当前模块中声明的元素段列表，以其元素类型表示。

  • *数据段*：当前模块中声明的数据段列表，每个数据段都由一个 \(\mathrel{\mbox{ok}}\) 条目表示。

  • *局部变量*：当前函数（包括参数）中声明的局部变量列表，以其值类型表示。

  • *标签*：从当前位置访问的标签堆栈，以其结果类型表示。

  • *返回*：当前函数的返回类型，表示为可选的结果类型，当不允许返回时（如在独立表达式中）不存在。

  • *引用*：模块中函数外部出现的 函数索引 列表，因此可以在函数内部使用它们来形成引用。

换句话说，上下文包含一系列适合的 类型，用于每个 索引空间，描述了该空间中的每个已定义条目。局部变量、标签和返回类型仅用于验证 指令 在 函数体 中，在其他地方留空。标签堆栈是上下文中唯一在验证指令序列时会发生变化的部分。

更具体地说，上下文定义为 记录 \(C\)，其抽象语法为

\[\begin{split}\begin{array}{llll} \def\mathdef4005#1{{}}\mathdef4005{context} & C &::=& \begin{array}[t]{l@{~}ll} \{ & \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}}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{locals}} & \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{labels}} & \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^\ast, \\ & \href{../valid/conventions.html#context}{\mathsf{return}} & \href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}}^?, \\ & \href{../valid/conventions.html#context}{\mathsf{refs}} & \href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}^\ast ~\} \\ \end{array} \end{array}\end{split}\]

除了字段访问写成 \(C.\mathsf{field}\) 之外，还采用以下表示法来操纵上下文

  • 在拼写上下文时，省略空字段。

  • \(C,\mathsf{field}\,A^\ast\) 表示与 \(C\) 相同的上下文，但将其 \(\mathsf{field}\) 组件序列的开头追加了元素 \(A^\ast\)。

注意

索引表示法 如 \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[i]\) 用于在上下文中的各自 索引空间 中查找索引。上下文扩展表示法 \(C,\mathsf{field}\,A\) 主要用于局部扩展 *相对* 索引空间，例如 标签索引。因此，该表示法定义为追加到各自序列的 *开头*，引入新的相对索引 \(0\) 并移动现有索引。

散文表示法

验证由针对 抽象语法 的每个相关部分的程式化规则指定。这些规则不仅说明了定义何时一个短语有效的约束，还用类型对它进行分类。在陈述这些规则时，采用以下约定。

  • 如果短语 \(A\) 被称为“具有类型 \(T\) 有效”，当且仅当满足相应规则表达的所有约束。 \(T\) 的形式取决于 \(A\) 是什么。

    注意

    例如，如果 \(A\) 是一个 函数，那么 \(T\) 是一个 函数类型；对于一个 \(A\) 是一个 全局变量， \(T\) 是一个 全局变量类型；等等。

  • 这些规则隐式地假设给定了一个 上下文 \(C\)。

  • 在某些地方，此上下文会局部扩展到上下文 \(C'\)，其中包含其他条目。使用“在上下文 \(C'\) 下，… *语句* …” 的表述来表达以下语句必须在扩展上下文体现的假设下适用。

正式表示法

注意

本节简要解释了正式指定类型规则的表示法。对于感兴趣的读者，可以在相应的教科书中找到更详细的介绍。 [2]

断言短语 \(A\) 具有相应的类型 \(T\) 被写成 \(A : T\)。但是，一般来说，类型依赖于上下文 \(C\)。为了明确表达这一点，完整形式是一个 *判断* \(C \vdash A : T\)，它表示 \(A : T\) 在 \(C\) 中编码的假设下成立。

正式类型规则使用一种标准方法来指定类型系统，将其渲染成 *推导规则*。每个规则都具有以下一般形式

\[\frac{ \mathit{前提}_1 \qquad \mathit{前提}_2 \qquad \dots \qquad \mathit{前提}_n }{ \mathit{结论} }\]

这样的规则被理解为一个大的蕴含关系：如果所有前提都成立，那么结论就成立。某些规则没有前提；它们是 *公理*，其结论无条件成立。结论始终是一个判断 \(C \vdash A : T\)，并且抽象语法的每个相关构造 \(A\) 都有一个相应的规则。

注意

例如，\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) 指令的类型规则可以作为公理给出

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

该指令始终具有类型 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\)（表示它消耗两个 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}\) 值并生成一个值），独立于任何辅助条件。

像 \(\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local.get}}\) 这样的指令可以这样类型化

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

这里，前提强制执行立即 局部变量索引 \(x\) 存在于上下文中。该指令生成其相应类型 \(t\) 的值（并且不消耗任何值）。如果 \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) 不存在，那么前提不成立，并且该指令类型错误。

最后，一个 结构化 指令需要一个递归规则，其中前提本身就是一个类型判断

\[\frac{ C \vdash \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\,[t_2^\ast] \vdash \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }{ C \vdash \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

当且仅当 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) 指令中的指令序列有效时，该指令才有效。此外，结果类型必须与块的注解 \(\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}\) 匹配。如果满足以上条件，则 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) 指令的类型与指令序列相同。在指令序列中，可以使用一个对应结果类型的附加标签，这可以通过在上下文 \(C\) 中添加附加标签信息来实现。