matches_map_group_equiv_concat

project-everest · Jan 6, 2025 · 8aaa1ec · 8aaa1ec
1 parent 50e84eb
commit 8aaa1ec
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 1 deletion.
diff --git 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
@@ -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)