From 606931a1ffa8defe712748cb52e8858427dd3f2b Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Sun, 17 Mar 2024 07:55:12 +0100
Subject: [PATCH] Backport value subsumption

---
 document/core/exec/values.rst    | 20 ++++++++++++++++++++
 document/core/valid/matching.rst |  2 +-
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst
index e0fd90e2..17c68e10 100644
--- a/document/core/exec/values.rst
+++ b/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
diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst
index e6fededd..ff107246 100644
--- a/document/core/valid/matching.rst
+++ b/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`.