Types¶

The sequence of types defined in a module is validated incrementally, yielding a sequence of defined types representing them individually.

The type definition \((\href{../syntax/modules.html#syntax-type}{\mathsf{type}}~{\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}})\) is valid with the defined type sequence \({{\mathit{dt}}^\ast}\) if:

• The length of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}\) is equal to \(x\).

• The defined type sequence \({{\mathit{dt}}^\ast}\) is of the form \({{{{\href{../valid/conventions.html#aux-roll-deftype}{\mathrm{roll}}}}_{x}^\ast}}{({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}})}\).

• Let \({C'}\) be the same context as \(C\), but with the defined type sequence \({{\mathit{dt}}^\ast}\) appended to the field \(\href{../valid/conventions.html#context}{\mathsf{types}}\).

• Under the context \({C'}\), the recursive type \({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}}\) is valid for the type index \(x\).

The type definition sequence \({{\href{../syntax/modules.html#syntax-type}{\mathit{type}}}^\ast}\) is valid with the defined type sequence \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast}\) if:

• Either:

  • The type definition sequence \({{\href{../syntax/modules.html#syntax-type}{\mathit{type}}}^\ast}\) is empty.

  • The defined type sequence \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast}\) is empty.

• Or:

  • The type definition sequence \({{\href{../syntax/modules.html#syntax-type}{\mathit{type}}}^\ast}\) is of the form \({\href{../syntax/modules.html#syntax-type}{\mathit{type}}}_1~{{\href{../syntax/modules.html#syntax-type}{\mathit{type}}'}^\ast}\).

  • The defined type sequence \({{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}^\ast}\) is of the form \({{\mathit{dt}}_1^\ast}~{{\mathit{dt}}^\ast}\).

  • The type definition \({\href{../syntax/modules.html#syntax-type}{\mathit{type}}}_1\) is valid with the defined type sequence \({{\mathit{dt}}_1^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the defined type sequence \({{\mathit{dt}}_1^\ast}\) appended to the field \(\href{../valid/conventions.html#context}{\mathsf{types}}\).

  • Under the context \({C'}\), the type definition sequence \({{\href{../syntax/modules.html#syntax-type}{\mathit{type}}'}^\ast}\) is valid with the defined type sequence \({{\mathit{dt}}^\ast}\).

Tags¶

Tags \(\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}\) are classified by their tag types, which are defined types expanding to function types.

The tag \((\href{../syntax/modules.html#syntax-tag}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}})\) is valid with the tag type \({\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}'}\) if:

• The tag type \({\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}}\) is valid.

• The tag type \({\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}'}\) is \({{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}})\).

Globals¶

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

The global \((\href{../syntax/modules.html#syntax-global}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}})\) is valid with the global type \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\) if:

• The global type \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\) is valid.

• The global type \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\) is of the form \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t)\).

• The expression \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is valid with the value type \(t\).

• \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is constant.

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

The global sequence \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}\) is valid with the global type sequence \({{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}\) if:

• Either:

  • The global sequence \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}\) is empty.

  • The global type sequence \({{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}\) is empty.

• Or:

  • The global sequence \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}\) is of the form \({\href{../syntax/modules.html#syntax-global}{\mathit{global}}}_1~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}'}^\ast}\).

  • The global type sequence \({{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}^\ast}\) is of the form \({\mathit{gt}}_1~{{\mathit{gt}}^\ast}\).

  • The global \({\href{../syntax/modules.html#syntax-global}{\mathit{global}}}_1\) is valid with the global type \({\mathit{gt}}_1\).

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

  • Under the context \({C'}\), the global sequence \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}'}^\ast}\) is valid with the global type sequence \({{\mathit{gt}}^\ast}\).

Memories¶

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

The memory \((\href{../syntax/modules.html#syntax-mem}{\mathsf{memory}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}})\) is valid with the memory type \({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}\) if:

• The memory type \({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}\) is valid.

Tables¶

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

The table \((\href{../syntax/modules.html#syntax-table}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}})\) is valid with the table type \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\) if:

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

• The table type \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\) is of the form \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}})\).

• The expression \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is valid with the value type \({\mathit{rt}}\).

• \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is constant.

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-comptype}{\rightarrow} {t_2^\ast}\).

The function \((\href{../syntax/modules.html#syntax-func}{\mathsf{func}}~x~{{\href{../syntax/modules.html#syntax-local}{\mathit{local}}}^\ast}~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}})\) is valid with the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) if:

• The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.

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

• For all \({\href{../syntax/modules.html#syntax-local}{\mathit{local}}}\) in \({{\href{../syntax/modules.html#syntax-local}{\mathit{local}}}^\ast}\):

  • The local \({\href{../syntax/modules.html#syntax-local}{\mathit{local}}}\) is valid with the local type \({{\mathit{lt}}}\).

• \({{{\mathit{lt}}}^\ast}\) is the concatenation of all such \({{\mathit{lt}}}\).

• Under the context \(C\) with the field \(\href{../valid/conventions.html#context}{\mathsf{locals}}\) appended by \({(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t_1)^\ast}~{{{\mathit{lt}}}^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) appended by \({t_2^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{return}}\) appended by \({t_2^\ast}\), the expression \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is valid with the result type \({t_2^\ast}\).

Locals¶

Locals \({\href{../syntax/modules.html#syntax-local}{\mathit{local}}}\) are classified with local types.

The local \((\href{../syntax/modules.html#syntax-local}{\mathsf{local}}~t)\) is valid with the local type \(({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}~t)\) if:

• The value type \(t\) is valid.

• Either:

  • The initialization status \({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}\) is of the form \(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}\).

  • A default value for \(t\) is defined.

• Or:

  • The initialization status \({\href{../valid/conventions.html#syntax-init}{\mathit{init}}}\) is of the form \(\href{../valid/conventions.html#syntax-init}{\mathsf{unset}}\).

  • A default value for \(t\) is not defined.

Data Segments¶

Data segments \({\href{../syntax/modules.html#syntax-data}{\mathit{data}}}\) are classified by the singleton data type, which merely expresses well-formedness.

The memory segment \((\href{../syntax/modules.html#syntax-data}{\mathsf{data}}~{b^\ast}~{\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}})\) is valid if:

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

The data mode \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}}\) is valid if:

• Either:

  • The data mode \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}}\) is of the form \(\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}\).

• Or:

  • The data mode \({\href{../syntax/modules.html#syntax-datamode}{\mathit{datamode}}}\) is of the form \((\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~x~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}})\).

  • The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) exists.

  • The memory \(C{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\).

  • The expression \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is valid with the value type \({\mathit{at}}\).

  • \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is constant.

Element Segments¶

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

The table segment \((\href{../syntax/modules.html#syntax-elem}{\mathsf{elem}}~{\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}~{{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}^\ast}~{\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}})\) is valid with the element type \({\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}\) if:

• The reference type \({\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}\) is valid.

• For all \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) in \({{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}^\ast}\):

  • The expression \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is valid with the value type \({\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}\).

  • \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is constant.

• The element mode \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is valid with the element type \({\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}\).

The element mode \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is valid with the element type \({\mathit{rt}}\) if:

• Either:

  • The element mode \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is of the form \(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}\).

• Or:

  • The element mode \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is of the form \(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declare}}\).

• Or:

  • The element mode \({\href{../syntax/modules.html#syntax-elemmode}{\mathit{elemmode}}}\) is of the form \((\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~x~{\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}})\).

  • The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) exists.

  • The table \(C{.}\href{../valid/conventions.html#context}{\mathsf{tables}}{}[x]\) is of the form \(({\mathit{at}}~{\mathit{lim}}~{\mathit{rt}'})\).

  • The reference type \({\mathit{rt}}\) matches the reference type \({\mathit{rt}'}\).

  • The expression \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is valid with the value type \({\mathit{at}}\).

  • \({\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}}\) is constant.

Start Function¶

The start function \((\href{../syntax/modules.html#syntax-start}{\mathsf{start}}~x)\) is valid if:

• The function \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) exists.

• The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{funcs}}{}[x]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-comptype}{\rightarrow})\).

Imports¶

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

The import \((\href{../syntax/modules.html#syntax-import}{\mathsf{import}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}_1~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}_2~{\mathit{xt}})\) is valid with the external type \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}}\) if:

• The external type \({\mathit{xt}}\) is valid.

• The external type \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}}\) is \({{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({\mathit{xt}})\).

Exports¶

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

The export \((\href{../syntax/modules.html#syntax-export}{\mathsf{export}}~{\href{../syntax/values.html#syntax-name}{\mathit{name}}}~{\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}})\) is valid with the name \({\href{../syntax/values.html#syntax-name}{\mathit{name}}}\) and the external type \({\mathit{xt}}\) if:

• The external index \({\href{../syntax/modules.html#syntax-externidx}{\mathit{externidx}}}\) is valid with the external type \({\mathit{xt}}\).

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 module \((\href{../syntax/modules.html#syntax-module}{\mathsf{module}}~{{\href{../syntax/modules.html#syntax-type}{\mathit{type}}}^\ast}~{{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}~{{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}~{{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}~{{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-start}{\mathit{start}}}^?}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast})\) is valid with the module type \({\href{../valid/modules.html#syntax-moduletype}{\mathit{moduletype}}}\) if:

• Under the context \(\{ \href{../valid/conventions.html#context}{\mathsf{return}}~\epsilon \}\), the type definition sequence \({{\href{../syntax/modules.html#syntax-type}{\mathit{type}}}^\ast}\) is valid with the defined type sequence \({{\mathit{dt}'}^\ast}\).

• For all \({\href{../syntax/modules.html#syntax-import}{\mathit{import}}}\) in \({{\href{../syntax/modules.html#syntax-import}{\mathit{import}}}^\ast}\):

  • Under the context \(\{ \href{../valid/conventions.html#context}{\mathsf{types}}~{{\mathit{dt}'}^\ast},\;\allowbreak \href{../valid/conventions.html#context}{\mathsf{return}}~\epsilon \}\), the import \({\href{../syntax/modules.html#syntax-import}{\mathit{import}}}\) is valid with the external type \({\mathit{xt}}_{\mathsf{i}}\).

• \({{\mathit{xt}}_{\mathsf{i}}^\ast}\) is the concatenation of all such \({\mathit{xt}}_{\mathsf{i}}\).

• For all \({\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}\) in \({{\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}^\ast}\):

  • Under the context \({C'}\), the tag \({\href{../syntax/modules.html#syntax-tag}{\mathit{tag}}}\) is valid with the tag type \({\mathit{jt}}\).

• \({{\mathit{jt}}^\ast}\) is the concatenation of all such \({\mathit{jt}}\).

• Under the context \({C'}\), the global sequence \({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}\) is valid with the global type sequence \({{\mathit{gt}}^\ast}\).

• For all \({\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}\) in \({{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}\):

  • Under the context \({C'}\), the memory \({\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}\) is valid with the memory type \({\mathit{mt}}\).

• \({{\mathit{mt}}^\ast}\) is the concatenation of all such \({\mathit{mt}}\).

• For all \({\href{../syntax/modules.html#syntax-table}{\mathit{table}}}\) in \({{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}\):

  • Under the context \({C'}\), the table \({\href{../syntax/modules.html#syntax-table}{\mathit{table}}}\) is valid with the table type \({\mathit{tt}}\).

• \({{\mathit{tt}}^\ast}\) is the concatenation of all such \({\mathit{tt}}\).

• For all \({\href{../syntax/modules.html#syntax-func}{\mathit{func}}}\) in \({{\href{../syntax/modules.html#syntax-func}{\mathit{func}}}^\ast}\):

  • The function \({\href{../syntax/modules.html#syntax-func}{\mathit{func}}}\) is valid with the defined type \({\mathit{dt}}\).

• \({{\mathit{dt}}^\ast}\) is the concatenation of all such \({\mathit{dt}}\).

• For all \({\href{../syntax/modules.html#syntax-data}{\mathit{data}}}\) in \({{\href{../syntax/modules.html#syntax-data}{\mathit{data}}}^\ast}\):

  • The memory segment \({\href{../syntax/modules.html#syntax-data}{\mathit{data}}}\) is valid.

• \({{\mathit{ok}}^\ast}\) is the concatenation of all such \({\mathit{ok}}\).

• For all \({\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}\) in \({{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}\):

  • The table segment \({\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}\) is valid with the element type \({\mathit{rt}}\).

• \({{\mathit{rt}}^\ast}\) is the concatenation of all such \({\mathit{rt}}\).

• If \({\href{../syntax/modules.html#syntax-start}{\mathit{start}}}\) is defined, then:

  • The start function \({\href{../syntax/modules.html#syntax-start}{\mathit{start}}}\) is valid.

• For all \({\href{../syntax/modules.html#syntax-export}{\mathit{export}}}\) in \({{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast}\):

  • The export \({\href{../syntax/modules.html#syntax-export}{\mathit{export}}}\) is valid with the name \({\mathit{nm}}\) and the external type \({\mathit{xt}}_{\mathsf{e}}\).

• \({{\mathit{nm}}^\ast}\) is the concatenation of all such \({\mathit{nm}}\).

• \({{\mathit{xt}}_{\mathsf{e}}^\ast}\) is the concatenation of all such \({\mathit{xt}}_{\mathsf{e}}\).

• \({{\mathit{nm}}^\ast}~{\mathrm{disjoint}}\) is true.

• The context \(C\) is of the form \({C'}\) with the field \(\href{../valid/conventions.html#context}{\mathsf{tags}}\) appended by \({{\mathit{jt}}_{\mathsf{i}}^\ast}~{{\mathit{jt}}^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{globals}}\) appended by \({{\mathit{gt}}^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{mems}}\) appended by \({{\mathit{mt}}_{\mathsf{i}}^\ast}~{{\mathit{mt}}^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{tables}}\) appended by \({{\mathit{tt}}_{\mathsf{i}}^\ast}~{{\mathit{tt}}^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{datas}}\) appended by \({{\mathit{ok}}^\ast}\) and the field \(\href{../valid/conventions.html#context}{\mathsf{elems}}\) appended by \({{\mathit{rt}}^\ast}\).

• The context \({C'}\) is of the form \(\{ \href{../valid/conventions.html#context}{\mathsf{types}}~{{\mathit{dt}'}^\ast},\;\allowbreak \href{../valid/conventions.html#context}{\mathsf{globals}}~{{\mathit{gt}}_{\mathsf{i}}^\ast},\;\allowbreak \href{../valid/conventions.html#context}{\mathsf{funcs}}~{{\mathit{dt}}_{\mathsf{i}}^\ast}~{{\mathit{dt}}^\ast},\;\allowbreak \href{../valid/conventions.html#context}{\mathsf{return}}~\epsilon,\;\allowbreak \href{../valid/conventions.html#context}{\mathsf{refs}}~{x^\ast} \}\).

• The function index sequence \({x^\ast}\) is of the form \({\href{../syntax/modules.html#syntax-funcidx}{\mathrm{funcidx}}}({{\href{../syntax/modules.html#syntax-global}{\mathit{global}}}^\ast}~{{\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}}^\ast}~{{\href{../syntax/modules.html#syntax-table}{\mathit{table}}}^\ast}~{{\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}}^\ast}~{{\href{../syntax/modules.html#syntax-export}{\mathit{export}}}^\ast})\).

• The tag type sequence \({{\mathit{jt}}_{\mathsf{i}}^\ast}\) is of the form \({\href{../syntax/types.html#syntax-externtype}{\mathrm{tags}}}({{\mathit{xt}}_{\mathsf{i}}^\ast})\).

• The global type sequence \({{\mathit{gt}}_{\mathsf{i}}^\ast}\) is of the form \({\href{../syntax/types.html#syntax-externtype}{\mathrm{globals}}}({{\mathit{xt}}_{\mathsf{i}}^\ast})\).

• The memory type sequence \({{\mathit{mt}}_{\mathsf{i}}^\ast}\) is of the form \({\href{../syntax/types.html#syntax-externtype}{\mathrm{mems}}}({{\mathit{xt}}_{\mathsf{i}}^\ast})\).

• The table type sequence \({{\mathit{tt}}_{\mathsf{i}}^\ast}\) is of the form \({\href{../syntax/types.html#syntax-externtype}{\mathrm{tables}}}({{\mathit{xt}}_{\mathsf{i}}^\ast})\).

• The defined type sequence \({{\mathit{dt}}_{\mathsf{i}}^\ast}\) is of the form \({\href{../syntax/types.html#syntax-externtype}{\mathrm{funcs}}}({{\mathit{xt}}_{\mathsf{i}}^\ast})\).

• The module type \({\href{../valid/modules.html#syntax-moduletype}{\mathit{moduletype}}}\) is \({{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({{\mathit{xt}}_{\mathsf{i}}^\ast}~\mathrel{\href{../valid/modules.html#syntax-moduletype}{\rightarrow}}~{{\mathit{xt}}_{\mathsf{e}}^\ast})\).