:ref:`Modules <syntax-module>` are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.

.. index:: function, local, function index, local index, type index, function type, value type, expression, import
   pair: abstract syntax; function
   single: abstract syntax; function

Functions \func are classified by :ref:`function types <syntax-functype>` of the form [t_1^\ast] \to [t_2^\ast].

• The type C.\CTYPES[x] must be defined in the context.
• Let [t_1^\ast] \to [t_2^\ast] be the :ref:`function type <syntax-functype>` C.\CTYPES[x].
• Let C' be the same :ref:`context <context>` as C, but with:
  • |CLOCALS| set to the sequence of :ref:`value types <syntax-valtype>` t_1^\ast~t^\ast, concatenating parameters and locals,
  • |CLABELS| set to the singular sequence containing only :ref:`result type <syntax-resulttype>` [t_2^\ast].
  • |CRETURN| set to the :ref:`result type <syntax-resulttype>` [t_2^\ast].
• Under the context C', the expression \expr must be valid with type [t_2^\ast].
• Then the function definition is valid with type [t_1^\ast] \to [t_2^\ast].

\frac{
  C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast]
  \qquad
  C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast]
}{
  C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^\ast]
}

.. index:: table, table type
   pair: validation; table
   single: abstract syntax; table

Tables \table are classified by :ref:`table types <syntax-tabletype>`.

• The :ref:`table type <syntax-tabletype>` \tabletype must be :ref:`valid <valid-tabletype>`.
• Then the table definition is valid with type \tabletype.

\frac{
  \vdashtabletype \tabletype \ok
}{
  C \vdashtable \{ \TTYPE~\tabletype \} : \tabletype
}

.. index:: memory, memory type
   pair: validation; memory
   single: abstract syntax; memory

Memories \mem are classified by :ref:`memory types <syntax-memtype>`.

• The :ref:`memory type <syntax-memtype>` \memtype must be :ref:`valid <valid-memtype>`.
• Then the memory definition is valid with type \memtype.

\frac{
  \vdashmemtype \memtype \ok
}{
  C \vdashmem \{ \MTYPE~\memtype \} : \memtype
}

.. index:: global, global type, expression
   pair: validation; global
   single: abstract syntax; global

Globals \global are classified by :ref:`global types <syntax-globaltype>` of the form \mut~t.

• The :ref:`global type <syntax-globaltype>` \mut~t must be :ref:`valid <valid-globaltype>`.
• The expression \expr must be :ref:`valid <valid-expr>` with :ref:`result type <syntax-resulttype>` [t].
• The expression \expr must be :ref:`constant <valid-constant>`.
• Then the global definition is valid with type \mut~t.

\frac{
  \vdashglobaltype \mut~t \ok
  \qquad
  C \vdashexpr \expr : [t]
  \qquad
  C \vdashexprconst \expr \const
}{
  C \vdashglobal \{ \GTYPE~\mut~t, \GINIT~\expr \} : \mut~t
}

.. index:: element, table, table index, expression, function index
   pair: validation; element
   single: abstract syntax; element
   single: table; element
   single: element; segment

Element segments \elem are classified by the :ref:`reference type <syntax-reftype>` of their elements.

• For each e_i in e^\ast,
  • The expression e_i must be :ref:`valid <valid-expr>`.
  • The expression e_i must be :ref:`constant <valid-const>`.
• The element mode \elemmode must be valid with :ref:`reference type <syntax-reftype>` t.
• Then the element segment is valid with :ref:`reference type <syntax-reftype>` t.

\frac{
  (C \vdashexpr e \ok)^\ast
  \qquad
  (C \vdashexprconst e \const)^\ast
  \qquad
  C \vdashelemmode \elemmode : t
}{
  C \vdashelem \{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \} : t
}

• The element mode is valid with any :ref:`reference type <syntax-reftype>`.

\frac{
}{
  C \vdashelemmode \EPASSIVE : \reftype
}

• The table C.\CTABLES[x] must be defined in the context.
• Let \limits~t be the :ref:`table type <syntax-tabletype>` C.\CTABLES[x].
• The expression \expr must be :ref:`valid <valid-expr>` with :ref:`result type <syntax-resulttype>` [\I32].
• The expression \expr must be :ref:`constant <valid-constant>`.
• Then the element mode is valid with :ref:`reference type <syntax-reftype>` t.

\frac{
  \begin{array}{@{}c@{}}
  C.\CTABLES[x] = \limits~t
  \\
  C \vdashexpr \expr : [\I32]
  \qquad
  C \vdashexprconst \expr \const
  \end{array}
}{
  C \vdashelemmode \EACTIVE~\{ \ETABLE~x, \EOFFSET~\expr \} : t
}

• The element mode is valid with any :ref:`reference type <syntax-reftype>`.

\frac{
}{
  C \vdashelemmode \EDECLARATIVE : \reftype
}

.. index:: data, memory, memory index, expression, byte
   pair: validation; data
   single: abstract syntax; data
   single: memory; data
   single: data; segment

Data segments \data are not classified by any type but merely checked for well-formedness.

• The data mode \datamode must be valid.
• Then the data segment is valid.

\frac{
  C \vdashdatamode \datamode \ok
}{
  C \vdashdata \{ \DINIT~b^\ast, \DMODE~\datamode \} \ok
}

• The data mode is valid.

\frac{
}{
  C \vdashdatamode \DPASSIVE \ok
}

• The memory C.\CMEMS[x] must be defined in the context.
• The expression \expr must be :ref:`valid <valid-expr>` with :ref:`result type <syntax-resulttype>` [\I32].
• The expression \expr must be :ref:`constant <valid-constant>`.
• Then the data mode is valid.

\frac{
  C.\CMEMS[x] = \limits
  \qquad
  C \vdashexpr \expr : [\I32]
  \qquad
  C \vdashexprconst \expr \const
}{
  C \vdashdatamode \DACTIVE~\{ \DMEM~x, \DOFFSET~\expr \} \ok
}

.. index:: start function, function index
   pair: validation; start function
   single: abstract syntax; start function

Start function declarations \start are not classified by any type.

• The function C.\CFUNCS[x] must be defined in the context.
• The type of C.\CFUNCS[x] must be [] \to [].
• Then the start function is valid.

\frac{
  C.\CFUNCS[x] = [] \to []
}{
  C \vdashstart \{ \SFUNC~x \} \ok
}

.. index:: export, name, index, function index, table index, memory index, global index
   pair: validation; export
   single: abstract syntax; export

Exports \export and export descriptions \exportdesc are classified by their :ref:`external type <syntax-externtype>`.

• The export description \exportdesc must be valid with :ref:`external type <syntax-externtype>` \externtype.
• Then the export is valid with :ref:`external type <syntax-externtype>` \externtype.

\frac{
  C \vdashexportdesc \exportdesc : \externtype
}{
  C \vdashexport \{ \ENAME~\name, \EDESC~\exportdesc \} : \externtype
}

• The function C.\CFUNCS[x] must be defined in the context.
• Then the export description is valid with :ref:`external type <syntax-externtype>` \ETFUNC~C.\CFUNCS[x].

\frac{
  C.\CFUNCS[x] = \functype
}{
  C \vdashexportdesc \EDFUNC~x : \ETFUNC~\functype
}

• The table C.\CTABLES[x] must be defined in the context.
• Then the export description is valid with :ref:`external type <syntax-externtype>` \ETTABLE~C.\CTABLES[x].

\frac{
  C.\CTABLES[x] = \tabletype
}{
  C \vdashexportdesc \EDTABLE~x : \ETTABLE~\tabletype
}

• The memory C.\CMEMS[x] must be defined in the context.
• Then the export description is valid with :ref:`external type <syntax-externtype>` \ETMEM~C.\CMEMS[x].

\frac{
  C.\CMEMS[x] = \memtype
}{
  C \vdashexportdesc \EDMEM~x : \ETMEM~\memtype
}

• The global C.\CGLOBALS[x] must be defined in the context.
• Then the export description is valid with :ref:`external type <syntax-externtype>` \ETGLOBAL~C.\CGLOBALS[x].

\frac{
  C.\CGLOBALS[x] = \globaltype
}{
  C \vdashexportdesc \EDGLOBAL~x : \ETGLOBAL~\globaltype
}

.. index:: import, name, function type, table type, memory type, global type
   pair: validation; import
   single: abstract syntax; import

Imports \import and import descriptions \importdesc are classified by :ref:`external types <syntax-externtype>`.

• The import description \importdesc must be valid with type \externtype.
• Then the import is valid with type \externtype.

\frac{
  C \vdashimportdesc \importdesc : \externtype
}{
  C \vdashimport \{ \IMODULE~\name_1, \INAME~\name_2, \IDESC~\importdesc \} : \externtype
}

• The function C.\CTYPES[x] must be defined in the context.
• Let [t_1^\ast] \to [t_2^\ast] be the :ref:`function type <syntax-functype>` C.\CTYPES[x].
• Then the import description is valid with type \ETFUNC~[t_1^\ast] \to [t_2^\ast].

\frac{
  C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast]
}{
  C \vdashimportdesc \IDFUNC~x : \ETFUNC~[t_1^\ast] \to [t_2^\ast]
}

• The table type \tabletype must be :ref:`valid <valid-tabletype>`.
• Then the import description is valid with type \ETTABLE~\tabletype.

\frac{
  \vdashtable \tabletype \ok
}{
  C \vdashimportdesc \IDTABLE~\tabletype : \ETTABLE~\tabletype
}

• The memory type \memtype must be :ref:`valid <valid-memtype>`.
• Then the import description is valid with type \ETMEM~\memtype.

\frac{
  \vdashmemtype \memtype \ok
}{
  C \vdashimportdesc \IDMEM~\memtype : \ETMEM~\memtype
}

• The global type \globaltype must be :ref:`valid <valid-globaltype>`.
• Then the import description is valid with type \ETGLOBAL~\globaltype.

\frac{
  \vdashglobaltype \globaltype \ok
}{
  C \vdashimportdesc \IDGLOBAL~\globaltype : \ETGLOBAL~\globaltype
}

.. index:: module, type definition, function type, function, table, memory, global, element, data, start function, import, export, context
   pair: validation; module
   single: abstract syntax; module

Modules are classified by their mapping from the :ref:`external types <syntax-externtype>` of their :ref:`imports <syntax-import>` to those of their :ref:`exports <syntax-export>`.

A module is entirely closed, that is, its components can only refer to definitions that appear in the module itself. Consequently, no initial :ref:`context <context>` is required. Instead, the context C for validation of the module's content is constructed from the definitions in the module.

• Let \module be the module to validate.
• Let C be a :ref:`context <context>` where:
  • C.\CTYPES is \module.\MTYPES,
  • C.\CFUNCS is \etfuncs(\X{it}^\ast) concatenated with \X{ft}^\ast, with the import's :ref:`external types <syntax-externtype>` \X{it}^\ast and the internal :ref:`function types <syntax-functype>` \X{ft}^\ast as determined below,
  • C.\CTABLES is \ettables(\X{it}^\ast) concatenated with \X{tt}^\ast, with the import's :ref:`external types <syntax-externtype>` \X{it}^\ast and the internal :ref:`table types <syntax-tabletype>` \X{tt}^\ast as determined below,
  • C.\CMEMS is \etmems(\X{it}^\ast) concatenated with \X{mt}^\ast, with the import's :ref:`external types <syntax-externtype>` \X{it}^\ast and the internal :ref:`memory types <syntax-memtype>` \X{mt}^\ast as determined below,
  • C.\CGLOBALS is \etglobals(\X{it}^\ast) concatenated with \X{gt}^\ast, with the import's :ref:`external types <syntax-externtype>` \X{it}^\ast and the internal :ref:`global types <syntax-globaltype>` \X{gt}^\ast as determined below,
  • C.\CELEMS is {\X{rt}}^\ast as determined below,
  • C.\CDATAS is {\ok}^n, where n is the length of the vector \module.\MDATAS,
  • C.\CLOCALS is empty,
  • C.\CLABELS is empty,
  • C.\CRETURN is empty.
  • C.\CREFS is the set \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon), i.e., the set of :ref:`function indices <syntax-funcidx>` occurring in the module, except in its :ref:`functions <syntax-func>` or :ref:`start function <syntax-start>`.
• Let C' be the :ref:`context <context>` where:
  • C'.\CGLOBALS is the sequence \etglobals(\X{it}^\ast),
  • C'.\CFUNCS is the same as C.\CFUNCS,
  • C'.\CREFS is the same as C.\CREFS,
  • all other fields are empty.
• Under the context C:
  • For each \functype_i in \module.\MTYPES, the :ref:`function type <syntax-functype>` \functype_i must be :ref:`valid <valid-functype>`.
  • For each \func_i in \module.\MFUNCS, the definition \func_i must be :ref:`valid <valid-func>` with a :ref:`function type <syntax-functype>` \X{ft}_i.
  • For each \table_i in \module.\MTABLES, the definition \table_i must be :ref:`valid <valid-table>` with a :ref:`table type <syntax-tabletype>` \X{tt}_i.
  • For each \mem_i in \module.\MMEMS, the definition \mem_i must be :ref:`valid <valid-mem>` with a :ref:`memory type <syntax-memtype>` \X{mt}_i.
  • For each \global_i in \module.\MGLOBALS:
    • Under the context C', the definition \global_i must be :ref:`valid <valid-global>` with a :ref:`global type <syntax-globaltype>` \X{gt}_i.
  • For each \elem_i in \module.\MELEMS, the segment \elem_i must be :ref:`valid <valid-elem>` with :ref:`reference type <syntax-reftype>` \X{rt}_i.
  • For each \data_i in \module.\MDATAS, the segment \data_i must be :ref:`valid <valid-data>`.
  • If \module.\MSTART is non-empty, then \module.\MSTART must be :ref:`valid <valid-start>`.
  • For each \import_i in \module.\MIMPORTS, the segment \import_i must be :ref:`valid <valid-import>` with an :ref:`external type <syntax-externtype>` \X{it}_i.
  • For each \export_i in \module.\MEXPORTS, the segment \export_i must be :ref:`valid <valid-export>` with :ref:`external type <syntax-externtype>` \X{et}_i.
• The length of C.\CMEMS must not be larger than 1.
• All export names \export_i.\ENAME must be different.
• Let \X{ft}^\ast be the concatenation of the internal :ref:`function types <syntax-functype>` \X{ft}_i, in index order.
• Let \X{tt}^\ast be the concatenation of the internal :ref:`table types <syntax-tabletype>` \X{tt}_i, in index order.
• Let \X{mt}^\ast be the concatenation of the internal :ref:`memory types <syntax-memtype>` \X{mt}_i, in index order.
• Let \X{gt}^\ast be the concatenation of the internal :ref:`global types <syntax-globaltype>` \X{gt}_i, in index order.
• Let \X{rt}^\ast be the concatenation of the :ref:`reference types <syntax-reftype>` \X{rt}_i, in index order.
• Let \X{it}^\ast be the concatenation of :ref:`external types <syntax-externtype>` \X{it}_i of the imports, in index order.
• Let \X{et}^\ast be the concatenation of :ref:`external types <syntax-externtype>` \X{et}_i of the exports, in index order.
• Then the module is valid with :ref:`external types <syntax-externtype>` \X{it}^\ast \to \X{et}^\ast.

\frac{
  \begin{array}{@{}c@{}}
  (\vdashfunctype \type \ok)^\ast
  \quad
  (C \vdashfunc \func : \X{ft})^\ast
  \quad
  (C \vdashtable \table : \X{tt})^\ast
  \quad
  (C \vdashmem \mem : \X{mt})^\ast
  \quad
  (C' \vdashglobal \global : \X{gt})^\ast
  \\
  (C \vdashelem \elem : \X{rt})^\ast
  \quad
  (C \vdashdata \data \ok)^n
  \quad
  (C \vdashstart \start \ok)^?
  \quad
  (C \vdashimport \import : \X{it})^\ast
  \quad
  (C \vdashexport \export : \X{et})^\ast
  \\
  \X{ift}^\ast = \etfuncs(\X{it}^\ast)
  \qquad
  \X{itt}^\ast = \ettables(\X{it}^\ast)
  \qquad
  \X{imt}^\ast = \etmems(\X{it}^\ast)
  \qquad
  \X{igt}^\ast = \etglobals(\X{it}^\ast)
  \\
  x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)
  \\
  C = \{ \CTYPES~\type^\ast, \CFUNCS~\X{ift}^\ast\,\X{ft}^\ast, \CTABLES~\X{itt}^\ast\,\X{tt}^\ast, \CMEMS~\X{imt}^\ast\,\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast\,\X{gt}^\ast, \CELEMS~\X{rt}^\ast, \CDATAS~{\ok}^n, \CREFS~x^\ast \}
  \\
  C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \}
  \qquad
  |C.\CMEMS| \leq 1
  \qquad
  (\export.\ENAME)^\ast ~\F{disjoint}
  \\
  \module = \{
    \begin{array}[t]{@{}l@{}}
      \MTYPES~\type^\ast,
      \MFUNCS~\func^\ast,
      \MTABLES~\table^\ast,
      \MMEMS~\mem^\ast,
      \MGLOBALS~\global^\ast, \\
      \MELEMS~\elem^\ast,
      \MDATAS~\data^n,
      \MSTART~\start^?,
      \MIMPORTS~\import^\ast,
      \MEXPORTS~\export^\ast \}
    \end{array}
  \end{array}
}{
  \vdashmodule \module : \X{it}^\ast \to \X{et}^\ast
}