map pair set

src/cbor/spec/CBOR.Spec.API.MapPairSet.fsti

@@ -0,0 +1,103 @@
+module CBOR.Spec.API.MapPairSet
+open CBOR.Spec.API.Type
+open CBOR.Spec.Util
+
+let elt = cbor_map & cbor_map
+
+val t : eqtype
+
+val cardinality (x: t) : Tot nat
+
+val mem (x: elt) (s: t) : Tot bool
+
+let equal (s1 s2: t) : Tot prop =
+  forall x . mem x s1 <==> mem x s2
+
+val ext (s1 s2: t) : Lemma
+  (ensures (equal s1 s2 <==> s1 == s2))
+  [SMTPat (equal s1 s2)]
+
+val empty : t
+
+val mem_empty (x: elt) : Lemma
+  (ensures (~ (mem x (empty))))
+  [SMTPat (mem x (empty))]
+
+val cardinality_empty : squash
+  (cardinality (empty) == 0)
+
+val singleton (x: elt) : Tot (t)
+
+val mem_singleton (x x': elt) : Lemma
+  (ensures (mem x' (singleton x) <==> x' == x))
+  [SMTPat (mem x' (singleton x))]
+
+val cardinality_singleton (x: elt) : Lemma
+  (ensures (cardinality (singleton x) == 1))
+  [SMTPat (cardinality (singleton x))]
+
+val union (s1 s2: t) : Tot (t)
+
+val mem_union (s1 s2: t) (x: elt) : Lemma
+  (ensures (mem x (union s1 s2) <==> (mem x s1 \/ mem x s2)))
+  [SMTPat (mem x (union s1 s2))]
+
+let disjoint (s1 s2: t) : Tot prop =
+  forall x . ~ (mem x s1 /\ mem x s2)
+
+val cardinality_union (s1 s2: t) : Lemma
+  (requires (disjoint s1 s2))
+  (ensures (cardinality (union s1 s2) == cardinality s1 + cardinality s2))
+  [SMTPat (cardinality (union s1 s2))]
+
+val filter (phi: elt -> bool) (s: t) : Tot (t)
+
+val mem_filter (phi: elt -> bool) (s: t) (x: elt) : Lemma
+  (ensures (mem x (filter phi s) <==> (mem x s /\ phi x)))
+  [SMTPat (mem x (filter phi s))]
+
+val as_list (s: t) : GTot (list elt)
+
+val no_repeats_as_list (s: t) : Lemma
+  (ensures (List.Tot.no_repeats_p (as_list s)))
+  [SMTPat (as_list s)]
+
+val mem_as_list (s: t) (x: elt) : Lemma
+  (ensures (List.Tot.memP x (as_list s) <==> mem x s))
+  [SMTPat (List.Tot.memP x (as_list s))]
+
+val length_as_list (s: t) : Lemma
+  (ensures (List.Tot.length (as_list s) == cardinality s))
+  [SMTPat (as_list s)]
+
+val fold (#u: Type) (phi: u -> elt -> u) (x: u) (s: t) : Tot u
+
+val fold_ext
+  (#u: Type) (phi1 phi2: u -> elt -> u) (x: u) (s: t)
+: Lemma
+  (requires (forall x y . mem y s ==> phi1 x y == phi2 x y))
+  (ensures (fold phi1 x s == fold phi2 x s))
+
+val fold_eq
+  (#u: Type) (phi: u -> elt -> u) (x: u) (s: t) (l: list elt)
+: Lemma
+  (requires (
+    op_comm phi /\
+    List.Tot.no_repeats_p l /\
+    (forall x . List.Tot.memP x l <==> mem x s)
+  ))
+  (ensures (
+    fold phi x s == List.Tot.fold_left phi x l
+  ))
+
+val fold_eq_idem
+  (#u: Type) (phi: u -> elt -> u) (x: u) (s: t) (l: list elt)
+: Lemma
+  (requires (
+    op_comm phi /\
+    op_idem phi /\
+    (forall x . List.Tot.memP x l <==> mem x s)
+  ))
+  (ensures (
+    fold phi x s == List.Tot.fold_left phi x l
+  ))

src/cbor/spec/raw/CBOR.Spec.API.MapPairSet.fst

@@ -0,0 +1,52 @@
+module CBOR.Spec.API.MapPairSet
+module S = CBOR.Spec.Raw.Set
+
+let f : S.order elt = CBOR.Spec.Raw.Format.MapPair.map_pair_order
+
+let t = S.t f
+
+let cardinality = S.cardinality
+
+let mem = S.mem
+
+let ext = S.ext
+
+let empty = S.empty _
+
+let mem_empty = S.mem_empty f
+
+let cardinality_empty = S.cardinality_empty f
+
+let singleton = S.singleton _
+
+let mem_singleton = S.mem_singleton f
+
+let cardinality_singleton = S.cardinality_singleton f
+
+let union = S.union
+
+let mem_union = S.mem_union
+
+let cardinality_union = S.cardinality_union
+
+let filter = S.filter
+
+let mem_filter = S.mem_filter
+
+let as_list = S.as_list
+
+let no_repeats_as_list = S.no_repeats_as_list
+
+let mem_as_list = S.mem_as_list
+
+let length_as_list = S.length_as_list
+
+let fold phi = S.fold phi
+
+let fold_ext phi = S.fold_ext phi
+
+let fold_eq phi = S.fold_eq phi
+
+let fold_eq_idem phi = S.fold_eq_idem phi
+
+