t_map_ext

project-everest · Jan 4, 2025 · 4acf799 · 4acf799
1 parent 3e5254f
commit 4acf799
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 1 deletion.
diff --git a/src/cddl/spec/CDDL.Spec.MapGroup.Base.fst b/src/cddl/spec/CDDL.Spec.MapGroup.Base.fst
@@ -2001,12 +2001,21 @@ let matches_map_group (g: map_group) (m: cbor_map) : Tot bool =
 let matches_map_group_det (g: map_group) m
 = ()
 
-let t_map g = fun x ->
+let t_map'
+  (g: map_group)
+  (x: Cbor.cbor)
+: Tot bool
+=
   match unpack x with
   | CMap m ->
     matches_map_group g m
   | _ -> false
 
+let t_map g = FE.on_dom Cbor.cbor (t_map' g)
+
 let t_map_eq
   g x
 = ()
+
+let t_map_ext g1 g2 =
+  assert (FE.feq (t_map' g1) (t_map' g2))
diff --git a/src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti b/src/cddl/spec/CDDL.Spec.MapGroup.Base.fsti
@@ -535,3 +535,16 @@ val t_map_eq
     | _ -> False
   end)
   [SMTPat (t_map g x)]
+
+val t_map_ext
+  (g1 g2: map_group)
+: Lemma
+  (requires (forall m . matches_map_group g1 m <==> matches_map_group g2 m))
+  (ensures (t_map g1 == t_map g2))
+
+let t_map_concat_cut_r
+  (g: det_map_group)
+  (k: typ)
+: Lemma
+  (t_map (map_group_concat g (map_group_cut k)) == t_map g)
+= t_map_ext (map_group_concat g (map_group_cut k)) g