Adds validation for exception results.

Uses the "current" version of exception results, as it will be changed by WebAssembly#226.

Author: ioannad

document/core/appendix/properties.rst

@@ -58,8 +58,29 @@ Results
      S \vdashresult \TRAP : [t^\ast]
    }
 
-.. todo::
-   Add validation for exception results.
+
+:ref:`Results <syntax-result>` :math:`\val^\ast~(\THROWadm~\tagaddr)`
+.....................................................................
+
+* The :ref:`tag address <syntax-tagaddr>` :math:`\tagaddr` must be in :math:`\moduleinst.\MITAGS`.
+
+* The :ref:`external value <syntax-externval>` :math:`\EVTAG~\tagaddr` must be :ref:`valid <valid-externval-tag>` with some :ref:`external type <syntax-externtype>` :math:`\ETTAG~\tagtype`.
+
+* Let :math:`[t_1^\ast]\to[]` be the :ref:`tag type <syntax-tagtype>` |tagtype|.
+
+* The values :math:`\val^\ast` must be :ref:`valid <valid-val>` with types :math:`[t_1^\ast]`.
+
+* Then the result is valid with :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]`, for any sequence :math:`t_2^\ast` of :ref:`value types <syntax-valtype>`.
+
+
+.. math::
+   \frac{
+     \vdashexterntype \ETTAG~[t_1^\ast]\to[]~\ok
+     \qquad
+     (S \vdashval \val : t_1)^\ast
+   }{
+     S \vdashresult \val^\ast~(\THROWadm~\tagaddr) : [t_2^\ast]
+   }
 
 
 .. _module-context: