Modules¶

Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.

Functions¶

Functions \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) are classified by function types of the form \([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}} \}\)¶

The type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be defined in the context.
Let \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) be the function type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).
Let \(C'\) be the same context as \(C\), but with:
- \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) set to the sequence of value types \(t_1^\ast~t^\ast\), concatenating parameters and locals,
- \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) set to the singular sequence containing only result type \([t_2^\ast]\).
- \(\href{../valid/conventions.html#context}{\mathsf{return}}\) set to the result type \([t_2^\ast]\).
Under the context \(C'\), the expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be valid with type \([t_2^\ast]\).
Then the function definition is valid with type \([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] }\]

Tables¶

Tables \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}\) are classified by table types.

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

The table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) must be valid.
Then the table definition is valid with type \(\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}} }\]

Memories¶

Memories \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}\) are classified by memory types.

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

The memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) must be valid.
Then the memory definition is valid with type \(\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}} }\]

Globals¶

Globals \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}\) are classified by global types of the form \(\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}} \}\)¶

The global type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) must be valid.
The expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be valid with result type \([t]\).
The expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be constant.
Then the global definition is valid with type \(\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 }\]

Element Segments¶

Element segments \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}\) are not classified by a type.

\(\{ \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}}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast \}\)¶

The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.
Let \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).
The element type \(\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}\) must be \(\href{../syntax/types.html#syntax-elemtype}{\mathsf{funcref}}\).
The expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be valid with result type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).
The expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be constant.
For each \(y_i\) in \(y^\ast\), the function \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[y]\) must be defined in the context.
Then the element segment is valid.

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x] = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{funcref}} \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}}} \qquad (C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[y] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}})^\ast }{ C \href{../valid/modules.html#valid-elem}{\vdash} \{ \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}}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast \} \mathrel{\mbox{ok}} }\]

Data Segments¶

Data segments \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}\) are not classified by any type.

\(\{ \href{../syntax/modules.html#syntax-data}{\mathsf{data}}~x, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}, \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast \}\)¶

The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.
The expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be valid with result type \([\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}]\).
The expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}\) must be constant.
Then the data segment is valid.

\[\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-data}{\vdash} \{ \href{../syntax/modules.html#syntax-data}{\mathsf{data}}~x, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}, \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast \} \mathrel{\mbox{ok}} }\]

Start Function¶

Start function declarations \(\href{../syntax/modules.html#syntax-start}{\mathit{start}}\) are not classified by any type.

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

The function \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be defined in the context.
The type of \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).
Then the start function is valid.

\[\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}} }\]

Exports¶

Exports \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}\) and export descriptions \(\href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}}\) are classified by their external type.

\(\{ \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}} \}\)¶

The export description \(\href{../syntax/modules.html#syntax-exportdesc}{\mathit{exportdesc}}\) must be valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\).
Then the export is valid with external type \(\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\)¶

The function \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be defined in the context.
Then the export description is valid with external type \(\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\)¶

The table \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\) must be defined in the context.
Then the export description is valid with external type \(\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\)¶

The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.
Then the export description is valid with external type \(\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\)¶

The global \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}[x]\) must be defined in the context.
Then the export description is valid with external type \(\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}} }\]

Imports¶

Imports \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}\) and import descriptions \(\href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}}\) are classified by external types.

\(\{ \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}} \}\)¶

The import description \(\href{../syntax/modules.html#syntax-importdesc}{\mathit{importdesc}}\) must be valid with type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}\).
Then the import is valid with type \(\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\)¶

The function \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be defined in the context.
Let \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) be the function type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).
Then the import description is valid with type \(\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}}\)¶

The table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) must be valid.
Then the import description is valid with type \(\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}}\)¶

The memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) must be valid.
Then the import description is valid with type \(\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}}\)¶

The global type \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) must be valid.
Then the import description is valid with type \(\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}} }\]

Modules¶

Modules are classified by their mapping from the external types of their imports to those of their exports.

A module is entirely closed, that is, its components can only refer to definitions that appear in the module itself. Consequently, no initial context is required. Instead, the context \(C\) for validation of the module’s content is constructed from the definitions in the module.

Let \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) be the module to validate.
Let \(C\) be a context where:
- \(C.\href{../valid/conventions.html#context}{\mathsf{types}}\) is \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}\),
- \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}\) is \(\href{../syntax/types.html#syntax-externtype}{\mathrm{funcs}}(\mathit{it}^\ast)\) concatenated with \(\mathit{ft}^\ast\), with the import’s external types \(\mathit{it}^\ast\) and the internal function types \(\mathit{ft}^\ast\) as determined below,
- \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}\) is \(\href{../syntax/types.html#syntax-externtype}{\mathrm{tables}}(\mathit{it}^\ast)\) concatenated with \(\mathit{tt}^\ast\), with the import’s external types \(\mathit{it}^\ast\) and the internal table types \(\mathit{tt}^\ast\) as determined below,
- \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}\) is \(\href{../syntax/types.html#syntax-externtype}{\mathrm{mems}}(\mathit{it}^\ast)\) concatenated with \(\mathit{mt}^\ast\), with the import’s external types \(\mathit{it}^\ast\) and the internal memory types \(\mathit{mt}^\ast\) as determined below,
- \(C.\href{../valid/conventions.html#context}{\mathsf{globals}}\) is \(\href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}(\mathit{it}^\ast)\) concatenated with \(\mathit{gt}^\ast\), with the import’s external types \(\mathit{it}^\ast\) and the internal global types \(\mathit{gt}^\ast\) as determined below,
- \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}\) is empty,
- \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}\) is empty,
- \(C.\href{../valid/conventions.html#context}{\mathsf{return}}\) is empty.
Let \(C'\) be the context where \(C'.\href{../valid/conventions.html#context}{\mathsf{globals}}\) is the sequence \(\href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}(\mathit{it}^\ast)\) and all other fields are empty.
Under the context \(C\):
- For each \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}\), the function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_i\) must be valid.
- For each \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}\), the definition \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) must be valid with a function type \(\mathit{ft}_i\).
- For each \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}\), the definition \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\) must be valid with a table type \(\mathit{tt}_i\).
- For each \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}\), the definition \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\) must be valid with a memory type \(\mathit{mt}_i\).
- For each \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\):
  - Under the context \(C'\), the definition \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) must be valid with a global type \(\mathit{gt}_i\).
- For each \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elem}}\), the segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) must be valid.
- For each \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{data}}\), the segment \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) must be valid.
- If \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) is non-empty, then \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) must be valid.
- For each \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}\), the segment \(\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i\) must be valid with an external type \(\mathit{it}_i\).
- For each \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\), the segment \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) must be valid with external type \(\mathit{et}_i\).
The length of \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}\) must not be larger than \(1\).
The length of \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}\) must not be larger than \(1\).
All export names \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}\) must be different.
Let \(\mathit{ft}^\ast\) be the concatenation of the internal function types \(\mathit{ft}_i\), in index order.
Let \(\mathit{tt}^\ast\) be the concatenation of the internal table types \(\mathit{tt}_i\), in index order.
Let \(\mathit{mt}^\ast\) be the concatenation of the internal memory types \(\mathit{mt}_i\), in index order.
Let \(\mathit{gt}^\ast\) be the concatenation of the internal global types \(\mathit{gt}_i\), in index order.
Let \(\mathit{it}^\ast\) be the concatenation of external types \(\mathit{it}_i\) of the imports, in index order.
Let \(\mathit{et}^\ast\) be the concatenation of external types \(\mathit{et}_i\) of the exports, in index order.
Then the module is valid with external types \(\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{functype}} \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}} \mathrel{\mbox{ok}})^\ast \quad (C \href{../valid/modules.html#valid-data}{\vdash} \href{../syntax/modules.html#syntax-data}{\mathit{data}} \mathrel{\mbox{ok}})^\ast \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) \\ C = \{ \href{../valid/conventions.html#context}{\mathsf{types}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\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 \} \\ C' = \{ \href{../valid/conventions.html#context}{\mathsf{globals}}~\mathit{igt}^\ast \} \qquad |C.\href{../valid/conventions.html#context}{\mathsf{tables}}| \leq 1 \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} \end{array} }{ \href{../valid/modules.html#valid-module}{\vdash} \{ \begin{array}[t]{@{}l@{}} \href{../syntax/modules.html#syntax-module}{\mathsf{types}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\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{elem}}~\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^\ast, \href{../syntax/modules.html#syntax-module}{\mathsf{data}}~\href{../syntax/modules.html#syntax-data}{\mathit{data}}^\ast, \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 \} : \mathit{it}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} \mathit{et}^\ast \\ \end{array} }\end{split}\]

Note

Most definitions in a module – particularly functions – are mutually recursive. Consequently, the definition of the context \(C\) in this rule is recursive: it depends on the outcome of validation of the function, table, memory, and global definitions contained in the module, which itself depends on \(C\). However, this recursion is just a specification device. All types needed to construct \(C\) can easily be determined from a simple pre-pass over the module that does not perform any actual validation.

Globals, however, are not recursive. The effect of defining the limited context \(C'\) for validating the module’s globals is that their initialization expressions can only access imported globals and nothing else.

Note

The restriction on the number of tables and memories may be lifted in future versions of WebAssembly.