blob: a7b928313ec2da02a03a88fffb3c9c3f363ec768 [file] [log] [blame]
Types
-----
Most :ref:`types <syntax-type>` are universally valid.
However, restrictions apply to :ref:`function types <syntax-functype>` as well as the :ref:`limits <syntax-limits>` of :ref:`table types <syntax-tabletype>` and :ref:`memory types <syntax-memtype>`, which must be checked during validation.
.. index:: limits
pair: validation; limits
single: abstract syntax; limits
.. _valid-limits:
Limits
~~~~~~
:ref:`Limits <syntax-limits>` must have meaningful bounds that are within a given range.
:math:`\{ \LMIN~n, \LMAX~m^? \}`
................................
* The value of :math:`n` must not be larger than :math:`k`.
* If the maximum :math:`m^?` is not empty, then:
* Its value must not be larger than :math:`k`.
* Its value must not be smaller than :math:`n`.
* Then the limit is valid within range :math:`k`.
.. math::
\frac{
n \leq k
\qquad
(m \leq k)^?
\qquad
(n \leq m)^?
}{
\vdashlimits \{ \LMIN~n, \LMAX~m^? \} : k
}
.. index:: function type
pair: validation; function type
single: abstract syntax; function type
.. _valid-functype:
Function Types
~~~~~~~~~~~~~~
:ref:`Function types <syntax-functype>` may not specify more than one result.
:math:`[t_1^n] \to [t_2^m]`
...........................
* The arity :math:`m` must not be larger than :math:`1`.
* Then the function type is valid.
.. math::
\frac{
}{
\vdashfunctype [t_1^\ast] \to [t_2^?] \ok
}
.. note::
The restriction to at most one result may be removed in future versions of WebAssembly.
.. index:: table type, element type, limits
pair: validation; table type
single: abstract syntax; table type
.. _valid-tabletype:
Table Types
~~~~~~~~~~~
:math:`\limits~\elemtype`
.........................
* The limits :math:`\limits` must be :ref:`valid <valid-limits>` within range :math:`2^{32}`.
* Then the table type is valid.
.. math::
\frac{
\vdashlimits \limits : 2^{32}
}{
\vdashtabletype \limits~\elemtype \ok
}
.. index:: memory type, limits
pair: validation; memory type
single: abstract syntax; memory type
.. _valid-memtype:
Memory Types
~~~~~~~~~~~~
:math:`\limits`
...............
* The limits :math:`\limits` must be :ref:`valid <valid-limits>` within range :math:`2^{16}`.
* Then the memory type is valid.
.. math::
\frac{
\vdashlimits \limits : 2^{16}
}{
\vdashmemtype \limits \ok
}
.. index:: global type, value type, mutability
pair: validation; global type
single: abstract syntax; global type
.. _valid-globaltype:
Global Types
~~~~~~~~~~~~
:math:`\mut~\valtype`
.....................
* The global type is valid.
.. math::
\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
.. _valid-externtype:
External Types
~~~~~~~~~~~~~~
:math:`\ETFUNC~\functype`
.........................
* The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
* Then the external type is valid.
.. math::
\frac{
\vdashfunctype \functype \ok
}{
\vdashexterntype \ETFUNC~\functype \ok
}
:math:`\ETTABLE~\tabletype`
...........................
* The :ref:`table type <syntax-tabletype>` :math:`\tabletype` must be :ref:`valid <valid-tabletype>`.
* Then the external type is valid.
.. math::
\frac{
\vdashtabletype \tabletype \ok
}{
\vdashexterntype \ETTABLE~\tabletype \ok
}
:math:`\ETMEM~\memtype`
.......................
* The :ref:`memory type <syntax-memtype>` :math:`\memtype` must be :ref:`valid <valid-memtype>`.
* Then the external type is valid.
.. math::
\frac{
\vdashmemtype \memtype \ok
}{
\vdashexterntype \ETMEM~\memtype \ok
}
:math:`\ETGLOBAL~\globaltype`
.............................
* The :ref:`global type <syntax-globaltype>` :math:`\globaltype` must be :ref:`valid <valid-globaltype>`.
* Then the external type is valid.
.. math::
\frac{
\vdashglobaltype \globaltype \ok
}{
\vdashexterntype \ETGLOBAL~\globaltype \ok
}