From 8aaa1ec6b95f72cfe69a9f618be979ed9487ac10 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Sun, 5 Jan 2025 18:48:13 -0800
Subject: [PATCH] matches_map_group_equiv_concat

---
 src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti |  7 +++-
 src/cddl/spec/CDDL.Spec.MapGroup.fsti      | 44 ++++++++++++++++++++++
 2 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti b/src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti
index 83b1972be..d982e31d1 100644
--- a/src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti
+++ b/src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti
@@ -548,10 +548,15 @@ val t_map_eq
   end)
   [SMTPat (t_map g x)]
 
+let matches_map_group_equiv
+  (g1 g2: map_group)
+: Tot prop
+= forall m . matches_map_group g1 m <==> matches_map_group g2 m
+
 val t_map_ext
   (g1 g2: map_group)
 : Lemma
-  (requires (forall m . matches_map_group g1 m <==> matches_map_group g2 m))
+  (requires (matches_map_group_equiv g1 g2))
   (ensures (t_map g1 == t_map g2))
 
 let t_map_concat_cut_r
diff --git a/src/cddl/spec/CDDL.Spec.MapGroup.fsti b/src/cddl/spec/CDDL.Spec.MapGroup.fsti
index 1d421f318..da7df7888 100644
--- a/src/cddl/spec/CDDL.Spec.MapGroup.fsti
+++ b/src/cddl/spec/CDDL.Spec.MapGroup.fsti
@@ -741,6 +741,50 @@ let map_group_footprint_concat_consumes_all_recip'
 = let (_, _) = map_group_footprint_concat_consumes_all_recip g1 g2 f1 f2 m in
   ()
 
+#restart-solver
+let matches_map_group_equiv_concat'
+  (g1 g1' g2 g2': det_map_group)
+  (f1 f1' f2 f2': typ)
+  (m: cbor_map)
+: Lemma
+  (requires (
+    map_group_footprint g1 f1 /\
+    map_group_footprint g1' f1' /\
+    map_group_footprint g2 f2 /\
+    map_group_footprint g2'  f2' /\
+    matches_map_group_equiv g1 g1' /\
+    matches_map_group_equiv g2 g2' /\
+    typ_disjoint f1 f2 /\
+    typ_disjoint f1' f2' /\
+    matches_map_group (map_group_concat g1 g2) m
+  ))
+  (ensures (
+    matches_map_group (map_group_concat g1' g2') m
+  ))
+= let (m1, m2) = map_group_footprint_concat_consumes_all_recip g1 g2 f1 f2 m in
+  map_group_footprint_concat_consumes_all g1' g2' f1' f2' m1 m2
+
+#restart-solver
+let matches_map_group_equiv_concat
+  (g1 g1' g2 g2': det_map_group)
+  (f1 f1' f2 f2': typ)
+: Lemma
+  (requires (
+    map_group_footprint g1 f1 /\
+    map_group_footprint g1' f1' /\
+    map_group_footprint g2 f2 /\
+    map_group_footprint g2'  f2' /\
+    matches_map_group_equiv g1 g1' /\
+    matches_map_group_equiv g2 g2' /\
+    typ_disjoint f1 f2 /\
+    typ_disjoint f1' f2'
+  ))
+  (ensures (
+    matches_map_group_equiv (map_group_concat g1 g2) (map_group_concat g1' g2')
+  ))
+= Classical.forall_intro (Classical.move_requires (matches_map_group_equiv_concat' g1 g1' g2 g2' f1 f1' f2 f2'));
+  Classical.forall_intro (Classical.move_requires (matches_map_group_equiv_concat' g1' g1 g2' g2 f1' f1 f2' f2))
+
 #restart-solver
 let map_group_choice_compatible_match_item_for_concat_right
   (k: cbor)