Most :ref:`types <syntax-type>` are universally valid. However, restrictions apply to :ref:`limits <syntax-limits>`, which must be checked during validation. Moreover, :ref:`block types <syntax-blocktype>` are converted to plain :ref:`function types <syntax-functype>` for ease of processing.

.. index:: limits
   pair: validation; limits
   single: abstract syntax; limits

:ref:`Limits <syntax-limits>` must have meaningful bounds that are within a given range.

• The value of n must not be larger than k.
• If the maximum m^? is not empty, then:
  • Its value must not be larger than k.
  • Its value must not be smaller than n.
• Then the limit is valid within range k.

\frac{
  n \leq k
  \qquad
  (m \leq k)^?
  \qquad
  (n \leq m)^?
}{
  \vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k
}

.. index:: block type
   pair: validation; block type
   single: abstract syntax; block type

:ref:`Block types <syntax-blocktype>` may be expressed in one of two forms, both of which are converted to plain :ref:`function types <syntax-functype>` by the following rules.

• The type C.\CTYPES[\typeidx] must be defined in the context.
• Then the block type is valid as :ref:`function type <syntax-functype>` C.\CTYPES[\typeidx].

\frac{
  C.\CTYPES[\typeidx] = \functype
}{
  C \vdashblocktype \typeidx : \functype
}

• The block type is valid as :ref:`function type <syntax-functype>` [] \to [\valtype^?].

\frac{
}{
  C \vdashblocktype [\valtype^?] : [] \to [\valtype^?]
}

.. index:: function type
   pair: validation; function type
   single: abstract syntax; function type

:ref:`Function types <syntax-functype>` are always valid.

• The function type is valid.

\frac{
}{
  \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok
}

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

• The limits \limits must be :ref:`valid <valid-limits>` within range 2^{32}-1.
• Then the table type is valid.

\frac{
  \vdashlimits \limits : 2^{32} - 1
}{
  \vdashtabletype \limits~\reftype \ok
}

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

• The limits \limits must be :ref:`valid <valid-limits>` within range 2^{16}.
• Then the memory type is valid.

\frac{
  \vdashlimits \limits : 2^{16}
}{
  \vdashmemtype \limits \ok
}

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

• The global type is valid.

\frac{
}{
  \vdashglobaltype \mut~\valtype \ok
}

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

• The :ref:`function type <syntax-functype>` \functype must be :ref:`valid <valid-functype>`.
• Then the external type is valid.

\frac{
  \vdashfunctype \functype \ok
}{
  \vdashexterntype \ETFUNC~\functype \ok
}

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

\frac{
  \vdashtabletype \tabletype \ok
}{
  \vdashexterntype \ETTABLE~\tabletype \ok
}

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

\frac{
  \vdashmemtype \memtype \ok
}{
  \vdashexterntype \ETMEM~\memtype \ok
}

• The :ref:`global type <syntax-globaltype>` \globaltype must be :ref:`valid <valid-globaltype>`.
• Then the external type is valid.

\frac{
  \vdashglobaltype \globaltype \ok
}{
  \vdashexterntype \ETGLOBAL~\globaltype \ok
}

.. index:: ! matching, external type

When :ref:`instantiating <exec-module>` a module, :ref:`external values <syntax-externval>` must be provided whose :ref:`types <valid-externval>` are matched against the respective :ref:`external types <syntax-externtype>` classifying each import. In some cases, this allows for a simple form of subtyping, as defined here.

.. index:: limits

:ref:`Limits <syntax-limits>` \{ \LMIN~n_1, \LMAX~m_1^? \} match limits \{ \LMIN~n_2, \LMAX~m_2^? \} if and only if:

• n_1 is larger than or equal to n_2.
• Either:
  • m_2^? is empty.
• Or:
  • Both m_1^? and m_2^? are non-empty.
  • m_1 is smaller than or equal to m_2.

~\\[-1ex]
\frac{
  n_1 \geq n_2
}{
  \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matcheslimits \{ \LMIN~n_2, \LMAX~\epsilon \}
}
\quad
\frac{
  n_1 \geq n_2
  \qquad
  m_1 \leq m_2
}{
  \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matcheslimits \{ \LMIN~n_2, \LMAX~m_2 \}
}

.. index:: function type

An :ref:`external type <syntax-externtype>` \ETFUNC~\functype_1 matches \ETFUNC~\functype_2 if and only if:

• Both \functype_1 and \functype_2 are the same.

~\\[-1ex]
\frac{
}{
  \vdashexterntypematch \ETFUNC~\functype \matchesexterntype \ETFUNC~\functype
}

.. index:: table type, limits, element type

An :ref:`external type <syntax-externtype>` \ETTABLE~(\limits_1~\reftype_1) matches \ETTABLE~(\limits_2~\reftype_2) if and only if:

• Limits \limits_1 :ref:`match <match-limits>` \limits_2.
• Both \reftype_1 and \reftype_2 are the same.

\frac{
  \vdashlimitsmatch \limits_1 \matcheslimits \limits_2
}{
  \vdashexterntypematch \ETTABLE~(\limits_1~\reftype) \matchesexterntype \ETTABLE~(\limits_2~\reftype)
}

.. index:: memory type, limits

An :ref:`external type <syntax-externtype>` \ETMEM~\limits_1 matches \ETMEM~\limits_2 if and only if:

• Limits \limits_1 :ref:`match <match-limits>` \limits_2.

\frac{
  \vdashlimitsmatch \limits_1 \matcheslimits \limits_2
}{
  \vdashexterntypematch \ETMEM~\limits_1 \matchesexterntype \ETMEM~\limits_2
}

.. index:: global type, value type, mutability

An :ref:`external type <syntax-externtype>` \ETGLOBAL~\globaltype_1 matches \ETGLOBAL~\globaltype_2 if and only if:

• Both \globaltype_1 and \globaltype_2 are the same.

~\\[-1ex]
\frac{
}{
  \vdashexterntypematch \ETGLOBAL~\globaltype \matchesexterntype \ETGLOBAL~\globaltype
}