diff --git a/document/core/appendix/implementation.rst b/document/core/appendix/implementation.rst
index df2885c..d5e5392 100644
--- a/document/core/appendix/implementation.rst
+++ b/document/core/appendix/implementation.rst
@@ -43,6 +43,8 @@ An implementation may impose restrictions on the following dimensions of a modul
 * the number of :ref:`exports <syntax-export>` from a :ref:`module <syntax-module>`
 * the number of parameters in a :ref:`function type <syntax-functype>`
 * the number of results in a :ref:`function type <syntax-functype>`
+* the number of parameters in a :ref:`block type <syntax-blocktype>`
+* the number of results in a :ref:`block type <syntax-blocktype>`
 * the number of :ref:`locals <syntax-local>` in a :ref:`function <syntax-func>`
 * the size of a :ref:`function <syntax-func>` body
 * the size of a :ref:`structured control instruction <syntax-instr-control>`
diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst
index f05f8af..9ad9ebb 100644
--- a/document/core/appendix/properties.rst
+++ b/document/core/appendix/properties.rst
@@ -157,6 +157,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 :ref:`Host Function Instances <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}`
 ..................................................................................................
 
+* The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
+
 * Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`\functype`.
 
 * For every :ref:`valid <valid-store>` :ref:`store <syntax-store>` :math:`S_1` :ref:`extending <extend-store>` :math:`S` and every sequence :math:`\val^\ast` of :ref:`values <syntax-val>` whose :ref:`types <valid-val>` coincide with :math:`t_1^\ast`:
@@ -173,6 +175,10 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 .. math::
    \frac{
+     \begin{array}[b]{@{}l@{}}
+     \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok \\
+     \end{array}
+     \quad
      \begin{array}[b]{@{}l@{}}
      \forall S_1, \val^\ast,~
        {\vdashstore S_1 \ok} \wedge