Modules

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

Types

The sequence of types defined in a module is validated incrementally, yielding a suitable context.

\(\href{../syntax/types.html#syntax-rectype}{\mathit{type}}^\ast\)

  • If the sequence is empty, then:

    • The context \(C\) must be empty.

    • Then the type sequence is valid.

  • Otherwise:

    • Let the recursive type \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\) be the last element in the sequence.

    • The sequence without \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\) must be valid for some context \(C'\).

    • Let the type index \(x\) be the length of \(C'.\href{../valid/conventions.html#context}{\mathsf{types}}\), i.e., the first type index free in \(C'\).

    • Let the sequence of defined types \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast\) be the result \(\href{../valid/conventions.html#aux-roll-deftype}{\mathrm{roll}^\ast}_{x}(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}})\) of rolling up into its sequence of defined types.

    • The recursive type \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\) must be valid under the context \(C\) for type index \(x\).

    • The current context \(C\) be the same as \(C'\), but with \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}^\ast\) appended to \(\href{../valid/conventions.html#context}{\mathsf{types}}\).

    • Then the type sequence is valid.

\[\frac{ }{ \{\} \href{../valid/modules.html#valid-types}{\vdash} \epsilon \mathrel{\mbox{ok}} }\]
\[\frac{ C' \href{../valid/modules.html#valid-types}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{type}}^\ast \mathrel{\mbox{ok}} \qquad C = C' \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../valid/conventions.html#context}{\mathsf{types}} = C'.\href{../valid/conventions.html#context}{\mathsf{types}}~\href{../valid/conventions.html#aux-roll-deftype}{\mathrm{roll}^\ast}_{|C'.\href{../valid/conventions.html#context}{\mathsf{types}}|}(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}) \qquad C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{rectype}} ~{\mathrel{\mbox{ok}}}(|C'.\href{../valid/conventions.html#context}{\mathsf{types}}|) }{ C \href{../valid/modules.html#valid-types}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{type}}^\ast~\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}} \mathrel{\mbox{ok}} }\]

Note

Despite the appearance, the context \(C\) is effectively an _output_ of this judgement.

Functions

Functions \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) are classified by defined types that expand to function types of the form \(\href{../syntax/types.html#syntax-comptype}{\mathsf{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}} \}\)

  • The defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a function type.

  • Let \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\) be the expansion of the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).

  • For each local declared by a value type \(t\) in \(t^\ast\):

    • The local for type \(t\) must be valid with local type \(\href{../valid/conventions.html#syntax-localtype}{\mathit{localtype}}_i\).

  • Let \(\href{../valid/conventions.html#syntax-localtype}{\mathit{localtype}}^\ast\) be the concatenation of all \(\href{../valid/conventions.html#syntax-localtype}{\mathit{localtype}}_i\).

  • Let \(C'\) be the same context as \(C\), but with:

    • \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) set to the sequence of value types \((\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t_1)^\ast~\href{../valid/conventions.html#syntax-localtype}{\mathit{localtype}}^\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 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).

\[\frac{ \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad (C \href{../valid/modules.html#valid-local}{\vdash} \{\href{../syntax/modules.html#syntax-local}{\mathsf{type}}~t\} : \href{../valid/conventions.html#syntax-init}{\mathit{init}}~t)^\ast \qquad C,\href{../valid/conventions.html#context}{\mathsf{locals}}\,(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t_1)^\ast~(\href{../valid/conventions.html#syntax-init}{\mathit{init}}~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}}~\{\href{../syntax/modules.html#syntax-local}{\mathsf{type}}~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] }\]

Locals

Locals are classified with local types.

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

  • The value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must be valid.

  • If \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) is defaultable, then:

    • The local is valid with local type \(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\).

  • Else:

    • The local is valid with local type \(\href{../valid/conventions.html#syntax-init}{\mathsf{unset}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\).

\[\frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t \mathrel{\mbox{ok}} \qquad C \href{../valid/types.html#valid-defaultable}{\vdash} t \href{../valid/types.html#valid-defaultable}{\mathrel{\mbox{defaultable}}} }{ C \href{../valid/modules.html#valid-local}{\vdash} \{ \href{../syntax/modules.html#syntax-local}{\mathsf{type}}~t \} : \href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t }\]
\[\frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-local}{\vdash} \{ \href{../syntax/modules.html#syntax-local}{\mathsf{type}}~t \} : \href{../valid/conventions.html#syntax-init}{\mathsf{unset}}~t }\]

Note

For cases where both rules are applicable, the former yields the more permissable type.

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}}, \href{../syntax/modules.html#syntax-table}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \}\)

  • The table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) must be valid.

  • Let \(t\) be the element reference type of \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).

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

\[\frac{ C \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} \qquad \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t \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-table}{\vdash} \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../syntax/modules.html#syntax-table}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} \} : \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{ C \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\).

Sequences of globals are handled incrementally, such that each definition has access to previous definitions.

\(\{ \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{ C \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-global}{\mathit{global}}^\ast\)

  • If the sequence is empty, then it is valid with the empty sequence of global types.

  • Else:

    • The first global definition must be valid with some type global type \(\mathit{gt}_1\).

    • Let \(C'\) be the same context as \(C\), but with the global type \(\mathit{gt}_1\) apppended to the \(\href{../valid/conventions.html#context}{\mathsf{globals}}\) vector.

    • Under context \(C'\), the remainder of the sequence must be valid with some sequence \(\mathit{gt}^\ast\) of global types.

    • Then the sequence is valid with the sequence of global types consisting of \(\mathit{gt}_1\) prepended to \(\mathit{gt}^\ast\).

\[\begin{split}~\\ \frac{ }{ C \href{../valid/modules.html#valid-globalseq}{\vdash} \epsilon : \epsilon } \qquad \frac{ C \href{../valid/modules.html#valid-global}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}}_1 : \mathit{gt}_1 \qquad C \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../valid/conventions.html#context}{\mathsf{globals}}~\mathit{gt}_1\} \href{../valid/modules.html#valid-globalseq}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast : \mathit{gt}^\ast }{ C \href{../valid/modules.html#valid-globalseq}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}}_1~\href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast : \mathit{gt}_1~\mathit{gt}^\ast }\end{split}\]

Element Segments

Element segments \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}\) are classified by the reference type of their elements.

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

  • The reference type \(t\) must be valid.

  • For each \(e_i\) in \(e^\ast\),

  • The element mode \(\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}\) must be valid with some reference type \(t'\).

  • The reference type \(t\) must match the reference type \(t'\).

  • Then the element segment is valid with reference type \(t\).

\[\frac{ C \href{../valid/types.html#valid-reftype}{\vdash} t \mathrel{\mbox{ok}} \qquad (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' \qquad C \href{../valid/matching.html#match-reftype}{\vdash} t \href{../valid/matching.html#match-reftype}{\leq} 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/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}} }{ 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}} \}\)

  • 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}}~t\) be the table type \(C.\href{../valid/conventions.html#context}{\mathsf{tables}}[x]\).

  • 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 element mode is valid with reference type \(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/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}} }{ C \href{../valid/modules.html#valid-elemmode}{\vdash} \href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}} : \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} }\]

Data Segments

Data segments \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}\) are not classified by any type but merely checked for well-formedness.

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

  • The data mode \(\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}\) must be valid.

  • Then the data segment is valid.

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

  • The data mode is valid.

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

  • 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 mode 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-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}} }\]

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 expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\) must be a function type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\).

  • Then the start function is valid.

\[\frac{ \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[] \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.

  • Let \(\mathit{dt}\) be the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x]\).

  • Then the export description is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\mathit{dt}\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[x] = \mathit{dt} }{ 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}}~\mathit{dt} }\]

\(\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 defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\) must be a function type.

  • Then the import description is valid with type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]\).

\[\frac{ \href{../valid/conventions.html#aux-expand-deftype}{\mathrm{expand}}(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x]) = \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ 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}}~C.\href{../valid/conventions.html#context}{\mathsf{types}}[x] }\]

\(\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{ C \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{ C \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{ C \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.

The external types classifying a module may contain free type indices that refer to types defined within the module.

  • Let \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) be the module to validate.

  • The types \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}\) must be valid yielding a context \(C_0\).

  • Let \(C\) be a context where:

    • \(C.\href{../valid/conventions.html#context}{\mathsf{types}}\) is \(C_0.\href{../valid/conventions.html#context}{\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{dt}^\ast\), with the import’s external types \(\mathit{it}^\ast\) and the internal defined types \(\mathit{dt}^\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{elems}}\) is \({\mathit{rt}}^\ast\) as determined below,

    • \(C.\href{../valid/conventions.html#context}{\mathsf{datas}}\) is \({\mathrel{\mbox{ok}}}^n\), where \(n\) is the length of the vector \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\),

    • \(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.

    • \(C.\href{../valid/conventions.html#context}{\mathsf{refs}}\) is the set \(\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)\), i.e., the set of function indices occurring in the module, except in its functions or start function.

  • 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)\),

    • \(C'.\href{../valid/conventions.html#context}{\mathsf{types}}\) is the same as \(C.\href{../valid/conventions.html#context}{\mathsf{types}}\),

    • \(C'.\href{../valid/conventions.html#context}{\mathsf{funcs}}\) is the same as \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}\),

    • \(C'.\href{../valid/conventions.html#context}{\mathsf{refs}}\) is the same as \(C.\href{../valid/conventions.html#context}{\mathsf{refs}}\),

    • all other fields are empty.

  • Under the context \(C'\):

    • The sequence \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\) of globals must be valid with a sequence \(\mathit{gt}^\ast\) of global types.

    • 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\).

  • Under the context \(C\):

    • 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 defined type \(\mathit{dt}_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{elems}}\), the segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) must be valid with reference type \(\mathit{rt}_i\).

    • 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{datas}}\), 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\).

  • Let \(\mathit{dt}^\ast\) be the concatenation of the internal function types \(\mathit{dt}_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{rt}^\ast\) be the concatenation of the reference types \(\mathit{rt}_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.

  • 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.

  • Then the module is valid with external types \(\mathit{it}^\ast \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} \mathit{et}^\ast\).

\[\begin{split}\frac{ \begin{array}{@{}c@{}} C_0 \href{../valid/modules.html#valid-types}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathit{type}}^\ast \mathrel{\mbox{ok}} \quad C' \href{../valid/modules.html#valid-globalseq}{\vdash} \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast : \mathit{gt}^\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-func}{\vdash} \href{../syntax/modules.html#syntax-func}{\mathit{func}} : \mathit{dt})^\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{idt}^\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}}~C_0.\href{../valid/conventions.html#context}{\mathsf{types}}, \href{../valid/conventions.html#context}{\mathsf{funcs}}~\mathit{idt}^\ast\,\mathit{dt}^\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' = \{ \href{../valid/conventions.html#context}{\mathsf{types}}~C_0.\href{../valid/conventions.html#context}{\mathsf{types}}, \href{../valid/conventions.html#context}{\mathsf{globals}}~\mathit{igt}^\ast, \href{../valid/conventions.html#context}{\mathsf{funcs}}~(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}), \href{../valid/conventions.html#context}{\mathsf{refs}}~(C.\href{../valid/conventions.html#context}{\mathsf{refs}}) \} \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-rectype}{\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 \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} \mathit{et}^\ast }\end{split}\]

Note

All functions in a module 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 but evaluated sequentially, such that each constant expressions only has access to imported or previously defined globals.

Note

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