Backport value subsumption

Author: rossberg

document/core/exec/values.rst

@@ -83,6 +83,26 @@ The following auxiliary typing rules specify this typing relation relative to a
      S \vdashval \REFEXTERNADDR~a : (\REF~\EXTERN)
    }
 
+Subsumption
+...........
+
+* The value must be valid with some value type :math:`t`.
+
+* The value type :math:`t` :ref:`matches <match-valtype>` another :ref:`valid <valid-valtype>` type :math:`t'`.
+
+* Then the value is valid with type :math:`t'`.
+
+.. math::
+   \frac{
+     S \vdashval \val : t
+     \qquad
+     \vdashvaltype t' \ok
+     \qquad
+     \vdashvaltypematch t \matchesvaltype t'
+   }{
+     S \vdashval \val : t'
+   }
+
 
 
 .. index:: external value, external type, validation, import, store

document/core/valid/matching.rst

@@ -54,7 +54,7 @@ A :ref:`heap type <syntax-heaptype>` :math:`\heaptype_1` matches a :ref:`heap ty
 
 * Either both :math:`\heaptype_1` and :math:`\heaptype_2` are the same.
 
-* Or :math:`\heaptype_1` is a :ref:`function type <syntax-functype>` and :math:`\heaptype_2` is :math:`FUNC`.
+* Or :math:`\heaptype_1` is a :ref:`function type <syntax-functype>` and :math:`\heaptype_2` is :math:`\FUNC`.
 
 * Or :math:`\heaptype_1` is a :ref:`function type <syntax-functype>` :math:`\functype_1` and :math:`\heaptype_2` is a :ref:`function type <syntax-functype>` :math:`\functype_2`, and :math:`\functype_1` :ref:`matches <match-functype>` :math:`\functype_2`.