模块

当模块包含的所有组件均有效时，该模块才有效。此外，大多数定义本身也用适当的类型分类。

函数

函数 \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) 由 函数类型 分类，形式为 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\(\{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~t^\ast, \href{../syntax/modules.html#syntax-func}{\mathsf{body}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \}\)

  • 类型 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) 必须在上下文中定义。

  • 令 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) 为 函数类型 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).

  • 令 \(C'\) 与 \(C\) 相同，但 上下文 为

    • \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) 设置为 值类型 \(t_1^\ast~t^\ast\) 的序列，连接参数和局部变量，

    • \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) 设置为仅包含 结果类型 \([t_2^\ast]\) 的单个序列。

    • \(\href{../valid/conventions.html#context}{\mathsf{return}}\) 设置为 结果类型 \([t_2^\ast]\).

  • 在上下文 \(C'\) 下，表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须有效，类型为 \([t_2^\ast]\).

  • 那么，函数定义有效，类型为 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[x] = [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{locals}}\,t_1^\ast~t^\ast,\href{../valid/conventions.html#context}{\mathsf{labels}}~[t_2^\ast],\href{../valid/conventions.html#context}{\mathsf{return}}~[t_2^\ast] \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} : [t_2^\ast] }{ C \href{../valid/modules.html#valid-func}{\vdash} \{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~t^\ast, \href{../syntax/modules.html#syntax-func}{\mathsf{body}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

表

表 \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}\) 由 表类型 分类。

\(\{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \}\)

  • 表类型 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 必须 有效.

  • 那么，表定义有效，类型为 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).

\[\frac{ \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-table}{\vdash} \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \} : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} }\]

内存

内存 \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}\) 由 内存类型 分类。

\(\{ \href{../syntax/modules.html#syntax-mem}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \}\)

  • 内存类型 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 必须 有效.

  • 那么，内存定义有效，类型为 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\).

\[\frac{ \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-mem}{\vdash} \{ \href{../syntax/modules.html#syntax-mem}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \} : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }\]

全局变量

全局变量 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}\) 由 全局变量类型 分类，形式为 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\).

\(\{ \href{../syntax/modules.html#syntax-global}{\mathsf{type}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t, \href{../syntax/modules.html#syntax-global}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \}\)

  • 全局变量类型 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) 必须 有效.

  • 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须 有效，结果类型 为 \([t]\).

  • 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须 常量.

  • 那么，全局变量定义有效，类型为 \(\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 C \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} : [t] \qquad C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} }{ C \href{../valid/modules.html#valid-global}{\vdash} \{ \href{../syntax/modules.html#syntax-global}{\mathsf{type}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t, \href{../syntax/modules.html#syntax-global}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \} : \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t }\]

元素段

元素段 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}\) 由其元素的 引用类型 分类。

\(\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~t, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~e^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}} \}\)

  • 对于 \(e^\ast\) 中的每个 \(e_i\)

  • 元素模式 \(\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}\) 必须有效，引用类型 为 \(t\).

  • 那么，元素段有效，引用类型 为 \(t\).

\[\frac{ (C \href{../valid/instructions.html#valid-expr}{\vdash} e : [t])^\ast \qquad (C \href{../valid/instructions.html#valid-constant}{\vdash} e \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}})^\ast \qquad C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}} : t }{ C \href{../valid/modules.html#valid-elem}{\vdash} \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~t, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~e^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}} \} : t }\]

\(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}\)

\[\frac{ }{ C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} }\]

\(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \}\)

  • 表 \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) 必须在上下文中定义。

  • 令 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) 为 表类型 \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

  • 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须 有效，结果类型 为 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

  • 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须 常量.

  • 那么，元素模式有效，引用类型 为 \(t\).

\[\begin{split}\frac{ \begin{array}{@{}c@{}} C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t \\ C \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \qquad C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} \end{array} }{ C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \} : t }\end{split}\]

\(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}}\)

\[\frac{ }{ C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} }\]

数据段

数据段 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}\) 不被任何类型分类，但需要检查其格式是否正确。

\(\{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}} \}\)

  • 数据模式 \(\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}\) 必须是有效的。

  • 然后数据段是有效的。

\[\frac{ C \href{../valid/modules.html#valid-datamode}{\vdash} \href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-data}{\vdash} \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}} \} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}\)

  • 数据模式是有效的。

\[\frac{ }{ C \href{../valid/modules.html#valid-datamode}{\vdash} \href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}} \mathrel{\mbox{ok}} }\]

\(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~x, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \}\)

  • 内存 \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) 必须在上下文中定义。

  • 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须 有效，结果类型 为 \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).

  • 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) 必须 常量.

  • 然后数据模式是有效的。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \qquad C \href{../valid/instructions.html#valid-expr}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} : [\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}] \qquad C \href{../valid/instructions.html#valid-constant}{\vdash} \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \href{../valid/instructions.html#valid-constant}{\mathrel{\mbox{const}}} }{ C \href{../valid/modules.html#valid-datamode}{\vdash} \href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~x, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \} \mathrel{\mbox{ok}} }\]

开始函数

开始函数声明 \(\href{../syntax/modules.html#syntax-start}{\mathit{start}}\) 不被任何类型分类。

\(\{ \href{../syntax/modules.html#syntax-start}{\mathsf{func}}~x \}\)

  • 函数 \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) 必须在上下文中定义。

  • 函数 \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) 的类型必须是 \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

  • 然后开始函数是有效的。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x] = [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] }{ C \href{../valid/modules.html#valid-start}{\vdash} \{ \href{../syntax/modules.html#syntax-start}{\mathsf{func}}~x \} \mathrel{\mbox{ok}} }\]

导出

导出 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}\) 和导出描述 \(\href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}}\) 由其 外部类型 分类。

\(\{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~\href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}} \}\)

  • 导出描述 \(\href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}}\) 必须与 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) 有效。

  • 然后导出与 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) 有效。

\[\frac{ C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} }{ C \href{../valid/modules.html#valid-export}{\vdash} \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~\href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}} \} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} }\]

\(\href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x\)

  • 函数 \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) 必须在上下文中定义。

  • 然后导出描述与 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) 有效。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\]

\(\href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x\)

  • 表 \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) 必须在上下文中定义。

  • 然后导出描述与 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) 有效。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} }{ C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} }\]

\(\href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x\)

  • 内存 \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) 必须在上下文中定义。

  • 然后导出描述与 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) 有效。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }{ C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }\]

\(\href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x\)

  • 全局 \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\) 必须在上下文中定义。

  • 然后导出描述与 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\) 有效。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x] = \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }{ C \href{../valid/modules.html#valid-exportdesc}{\vdash} \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }\]

导入

导入 \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}\) 和导入描述 \(\href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}}\) 由 外部类型 分类。

\(\{ \href{../syntax/modules.html#syntax-import}{\mathsf{module}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_1, \href{../syntax/modules.html#syntax-import}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_2, \href{../syntax/modules.html#syntax-import}{\mathsf{desc}}~\href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}} \}\)

  • 导入描述 \(\href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}}\) 必须与类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) 有效。

  • 然后导入与类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\) 有效。

\[\frac{ C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} }{ C \href{../valid/modules.html#valid-import}{\vdash} \{ \href{../syntax/modules.html#syntax-import}{\mathsf{module}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_1, \href{../syntax/modules.html#syntax-import}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}_2, \href{../syntax/modules.html#syntax-import}{\mathsf{desc}}~\href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}} \} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} }\]

\(\href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x\)

  • 函数 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) 必须在上下文中定义。

  • 令 \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) 为 函数类型 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).

  • 然后导入描述与类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) 有效。

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[x] = [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }{ C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\]

\(\href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)

  • 表格类型 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 必须 有效.

  • 然后导入描述与类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 有效。

\[\frac{ \href{../valid/modules.html#valid-table}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} }\]

\(\href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)

  • 内存类型 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 必须 有效.

  • 然后导入描述与类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 有效。

\[\frac{ \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} }\]

\(\href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)

  • 全局类型 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) 必须 有效.

  • 然后导入描述与类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) 有效。

\[\frac{ \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-importdesc}{\vdash} \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }\]

模块

模块根据其从外部类型 的 导入 到其导出 的外部类型的映射进行分类。

模块完全封闭，即其组件只能引用模块本身中出现的定义。因此，不需要任何初始上下文。相反，模块内容验证的上下文 \(C\) 是从模块中的定义构造的。

  • 令 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) 为要验证的模块。

  • 令 \(C\) 为一个 上下文，其中

    • \(C.\href{../valid/conventions.html#context}{\mathsf{types}}\) 是 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}\)，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}\) 是 \(\href{../syntax/types.html#syntax-externtype}{\mathrm{funcs}}(\mathit{it}^\ast)\) 与 \(\mathit{ft}^\ast\) 的串联，导入的 外部类型 \(\mathit{it}^\ast\) 和内部 函数类型 \(\mathit{ft}^\ast\) 如下确定，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}\) 是 \(\href{../syntax/types.html#syntax-externtype}{\mathrm{tables}}(\mathit{it}^\ast)\) 与 \(\mathit{tt}^\ast\) 的串联，导入的 外部类型 \(\mathit{it}^\ast\) 和内部 表格类型 \(\mathit{tt}^\ast\) 如下确定，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}\) 是 \(\href{../syntax/types.html#syntax-externtype}{\mathrm{mems}}(\mathit{it}^\ast)\) 与 \(\mathit{mt}^\ast\) 的串联，导入的 外部类型 \(\mathit{it}^\ast\) 和内部 内存类型 \(\mathit{mt}^\ast\) 如下确定，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}\) 是 \(\href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}(\mathit{it}^\ast)\) 与 \(\mathit{gt}^\ast\) 的串联，导入的 外部类型 \(\mathit{it}^\ast\) 和内部 全局类型 \(\mathit{gt}^\ast\) 如下确定，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{elems}}\) 是 \({\mathit{rt}}^\ast\)，如下确定，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{datas}}\) 是 \({\mathrel{\mbox{ok}}}^n\)，其中 \(n\) 是向量 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\) 的长度，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}\) 为空，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}\) 为空，

    • \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\) 为空。

    • \(C.\href{../valid/conventions.html#context}{\mathsf{refs}}\) 是集合 \(\href{../syntax/modules.html#syntax-funcidx}{\mathrm{funcidx}}(\href{../syntax/modules.html#syntax-module}{\mathit{module}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/modules.html#syntax-module}{\mathsf{funcs}} = \epsilon \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon)\)，即模块中出现的 函数索引 集合，但其 函数 或 起始函数 除外。

  • 令 \(C'\) 与 \(C\) 相同的 上下文，除了 \(C'.\href{../valid/conventions.html#context}{\mathsf{globals}}\) 仅仅是序列 \(\href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}(\mathit{it}^\ast)\)。

  • 对于 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}\)，函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) 必须是 有效 的。

  • 在上下文 \(C'\) 下

    • 对于 \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}\)，定义 \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\) 必须是 有效 的，并且具有 表格类型 \(\mathit{tt}_i\)。

    • 对于 \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}\)，定义 \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\) 必须是 有效 的，并且具有 内存类型 \(\mathit{mt}_i\)。

    • 对于 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\)，定义 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) 必须是 有效 的，并且具有 全局类型 \(\mathit{gt}_i\)。

    • 对于 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\)，段 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) 必须是 有效 的，并且具有 引用类型 \(\mathit{rt}_i\)。

    • 对于 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\)，段 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) 必须是 有效 的。

  • 在上下文 \(C\) 下

    • 对于 \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}\)，定义 \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) 必须是 有效 的，并且具有 函数类型 \(\mathit{ft}_i\)。

    • 如果 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) 不为空，则 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) 必须是 有效 的。

    • 对于 \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}\)，段 \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i\) 必须是 有效 的，并且具有 外部类型 \(\mathit{it}_i\)。

    • 对于 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) 中的每个 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\)，段 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) 必须是 有效 的，并且具有 外部类型 \(\mathit{et}_i\)。

  • \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}\) 的长度不能大于 \(1\)。

  • 所有导出名称 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}\) 必须不同。

  • 令 \(\mathit{ft}^\ast\) 为内部 函数类型 \(\mathit{ft}_i\) 按索引顺序的串联。

  • 令 \(\mathit{tt}^\ast\) 为内部 表格类型 \(\mathit{tt}_i\) 按索引顺序的串联。

  • 令 \(\mathit{mt}^\ast\) 为内部 内存类型 \(\mathit{mt}_i\) 按索引顺序的串联。

  • 令 \(\mathit{gt}^\ast\) 为内部 全局类型 \(\mathit{gt}_i\) 按索引顺序的串联。

  • 令 \(\mathit{rt}^\ast\) 为 引用类型 \(\mathit{rt}_i\) 按索引顺序的串联。

  • 令 \(\mathit{it}^\ast\) 为导入的 外部类型 \(\mathit{it}_i\) 按索引顺序的串联。

  • 令 \(\mathit{et}^\ast\) 为导出的 外部类型 \(\mathit{et}_i\) 按索引顺序的串联。

  • 那么该模块是有效的，其 外部类型 为 \(\mathit{it}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} \mathit{et}^\ast\)。

\[\begin{split}\frac{ \begin{array}{@{}c@{}} (\href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{type}} \mathrel{\mbox{ok}})^\ast \quad (C \href{../valid/modules.html#valid-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \mathit{ft})^\ast \quad (C' \href{../valid/modules.html#valid-table}{\vdash} \href{../syntax/modules.html#syntax-table}{\mathit{table}} : \mathit{tt})^\ast \quad (C' \href{../valid/modules.html#valid-mem}{\vdash} \href{../syntax/modules.html#syntax-mem}{\mathit{mem}} : \mathit{mt})^\ast \quad (C' \href{../valid/modules.html#valid-global}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}} : \mathit{gt})^\ast \\ (C' \href{../valid/modules.html#valid-elem}{\vdash} \href{../syntax/modules.html#syntax-elem}{\mathit{elem}} : \mathit{rt})^\ast \quad (C' \href{../valid/modules.html#valid-data}{\vdash} \href{../syntax/modules.html#syntax-data}{\mathit{data}} \mathrel{\mbox{ok}})^n \quad (C \href{../valid/modules.html#valid-start}{\vdash} \href{../syntax/modules.html#syntax-start}{\mathit{start}} \mathrel{\mbox{ok}})^? \quad (C \href{../valid/modules.html#valid-import}{\vdash} \href{../syntax/modules.html#syntax-import}{\mathit{import}} : \mathit{it})^\ast \quad (C \href{../valid/modules.html#valid-export}{\vdash} \href{../syntax/modules.html#syntax-export}{\mathit{export}} : \mathit{et})^\ast \\ \mathit{ift}^\ast = \href{../syntax/types.html#syntax-externtype}{\mathrm{funcs}}(\mathit{it}^\ast) \qquad \mathit{itt}^\ast = \href{../syntax/types.html#syntax-externtype}{\mathrm{tables}}(\mathit{it}^\ast) \qquad \mathit{imt}^\ast = \href{../syntax/types.html#syntax-externtype}{\mathrm{mems}}(\mathit{it}^\ast) \qquad \mathit{igt}^\ast = \href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}(\mathit{it}^\ast) \\ x^\ast = \href{../syntax/modules.html#syntax-funcidx}{\mathrm{funcidx}}(\href{../syntax/modules.html#syntax-module}{\mathit{module}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/modules.html#syntax-module}{\mathsf{funcs}} = \epsilon \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon) \\ C = \{ \href{../valid/conventions.html#context}{\mathsf{types}}~\href{../syntax/types.html#syntax-functype}{\mathit{type}}^\ast, \href{../valid/conventions.html#context}{\mathsf{funcs}}~\mathit{ift}^\ast\,\mathit{ft}^\ast, \href{../valid/conventions.html#context}{\mathsf{tables}}~\mathit{itt}^\ast\,\mathit{tt}^\ast, \href{../valid/conventions.html#context}{\mathsf{mems}}~\mathit{imt}^\ast\,\mathit{mt}^\ast, \href{../valid/conventions.html#context}{\mathsf{globals}}~\mathit{igt}^\ast\,\mathit{gt}^\ast, \href{../valid/conventions.html#context}{\mathsf{elems}}~\mathit{rt}^\ast, \href{../valid/conventions.html#context}{\mathsf{datas}}~{\mathrel{\mbox{ok}}}^n, \href{../valid/conventions.html#context}{\mathsf{refs}}~x^\ast \} \\ C' = C \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../valid/conventions.html#context}{\mathsf{globals}} = \mathit{igt}^\ast \qquad |C.\href{../valid/conventions.html#context}{\mathsf{mems}}| \leq 1 \qquad (\href{../syntax/modules.html#syntax-export}{\mathit{export}}.\href{../syntax/modules.html#syntax-export}{\mathsf{name}})^\ast ~\mathrm{disjoint} \\ \href{../syntax/modules.html#syntax-module}{\mathit{module}} = \{ \begin{array}[t]{@{}l@{}} \href{../syntax/modules.html#syntax-module}{\mathsf{types}}~\href{../syntax/types.html#syntax-functype}{\mathit{type}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{tables}}~\href{../syntax/modules.html#syntax-table}{\mathit{table}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{mems}}~\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{globals}}~\href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast, \\ \href{../syntax/modules.html#syntax-module}{\mathsf{elems}}~\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{datas}}~\href{../syntax/modules.html#syntax-data}{\mathit{data}}^n, \href{../syntax/modules.html#syntax-module}{\mathsf{start}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}^?, \href{../syntax/modules.html#syntax-module}{\mathsf{imports}}~\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{exports}}~\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast \} \end{array} \end{array} }{ \href{../valid/modules.html#valid-module}{\vdash} \href{../syntax/modules.html#syntax-module}{\mathit{module}} : \mathit{it}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} \mathit{et}^\ast }\end{split}\]

注意

模块中的大多数定义（尤其是函数）都是相互递归的。因此，此规则中上下文 \(C\) 的定义是递归的：它依赖于模块中包含的函数、表格、内存和全局定义的验证结果，而这些结果本身又依赖于 \(C\)。但是，这种递归只是一个规范设备。所有构建 \(C\) 所需的类型都可以很容易地从模块上的简单预处理中确定，该预处理不会执行任何实际的验证。

然而，全局变量不是递归的，并且在它们在本地定义时，在常量表达式中不可访问。定义有限上下文 \(C'\) 来验证某些定义的效果是，它们只能访问函数和导入的全局变量，而不能访问其他任何内容。

注意

WebAssembly 未来版本可能会取消对内存数量的限制。