Merge pull request WebAssembly#33 from Huxpro/missing-functype-ok

[spec] Reinstantiate lost functype in soundness

document/core/appendix/index-rules.rst

@@ -14,6 +14,7 @@ Typing of Static Constructs
 Construct                                        Judgement
 ===============================================  ===============================================================================
 :ref:`Limits <valid-limits>`                     :math:`\vdashlimits \limits : k`
+:ref:`Function type <valid-functype>`            :math:`\vdashfunctype \functype \ok`
 :ref:`Block type <valid-blocktype>`              :math:`\vdashblocktype \blocktype \ok`
 :ref:`Table type <valid-tabletype>`              :math:`\vdashtabletype \tabletype \ok`
 :ref:`Memory type <valid-memtype>`               :math:`\vdashmemtype \memtype \ok`

document/core/appendix/properties.rst

@@ -131,6 +131,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 :ref:`Function Instances <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}`
 .......................................................................................................................
 
+* The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
+
 * The :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst` must be :ref:`valid <valid-moduleinst>` with some :ref:`context <context>` :math:`C`.
 
 * Under :ref:`context <context>` :math:`C`, the :ref:`function <syntax-func>` :math:`\func` must be :ref:`valid <valid-func>` with :ref:`function type <syntax-functype>` :math:`\functype`.
@@ -139,6 +141,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 .. math::
    \frac{
+     \vdashfunctype \functype \ok
+     \qquad
      S \vdashmoduleinst \moduleinst : C
      \qquad
      C \vdashfunc \func : \functype
@@ -279,6 +283,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 :ref:`Module Instances <syntax-moduleinst>` :math:`\moduleinst`
 ...............................................................
 
+* Each :ref:`function type <syntax-functype>` :math:`\functype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid <valid-functype>`.
+
 * For each :ref:`function address <syntax-funcaddr>` :math:`\funcaddr_i` in :math:`\moduleinst.\MIFUNCS`, the :ref:`external value <syntax-externval>` :math:`\EVFUNC~\funcaddr_i` must be :ref:`valid <valid-externval-func>` with some :ref:`external type <syntax-externtype>` :math:`\ETFUNC~\functype'_i`.
 
 * For each :ref:`table address <syntax-tableaddr>` :math:`\tableaddr_i` in :math:`\moduleinst.\MITABLES`, the :ref:`external value <syntax-externval>` :math:`\EVTABLE~\tableaddr_i` must be :ref:`valid <valid-externval-table>` with some :ref:`external type <syntax-externtype>` :math:`\ETTABLE~\tabletype_i`.
@@ -305,6 +311,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
    ~\\[-1ex]
    \frac{
      \begin{array}{@{}c@{}}
+     (\vdashfunctype \functype \ok)^\ast
+     \\
      (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast
      \qquad
      (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast