Clone ghost containers

creusot-contracts/src/logic/fmap.rs

@@ -430,3 +430,25 @@ impl<K, V: ?Sized> FMap<K, V> {
         panic!()
     }
 }
+
+impl<K: Clone + Copy, V: Clone + Copy> Clone for FMap<K, V> {
+    #[pure]
+    #[ensures(result == *self)]
+    #[trusted]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
+impl<K: Clone + Copy, V: Clone + Copy> Copy for FMap<K, V> {}
+
+impl<K, V: ?Sized> Invariant for FMap<K, V> {
+    #[predicate(prophetic)]
+    #[open]
+    #[creusot::trusted_ignore_structural_inv]
+    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
+    fn invariant(self) -> bool {
+        pearlite! { forall<k: K> self.contains(k) ==> inv(k) && inv(self.lookup_unsized(k)) }
+    }
+}

creusot-contracts/src/logic/fset.rs

@@ -304,3 +304,25 @@ impl<T: ?Sized> FSet<T> {
         panic!()
     }
 }
+
+impl<T: Clone + Copy> Clone for FSet<T> {
+    #[pure]
+    #[ensures(result == *self)]
+    #[trusted]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
+impl<T: Clone + Copy> Copy for FSet<T> {}
+
+impl<T: ?Sized> Invariant for FSet<T> {
+    #[predicate(prophetic)]
+    #[open]
+    #[creusot::trusted_ignore_structural_inv]
+    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
+    fn invariant(self) -> bool {
+        pearlite! { forall<x: &T> self.contains(*x) ==> inv(*x) }
+    }
+}

creusot-contracts/src/logic/seq.rs

@@ -602,6 +602,18 @@ impl<T> Seq<T> {
     }
 }
 
+// Having `Copy` guarantees that the operation is pure, even if we decide to change the definition of `Clone`.
+impl<T: Clone + Copy> Clone for Seq<T> {
+    #[pure]
+    #[ensures(result == *self)]
+    #[trusted]
+    fn clone(&self) -> Self {
+        *self
+    }
+}
+
+impl<T: Clone + Copy> Copy for Seq<T> {}
+
 impl<T: ?Sized> Invariant for Seq<T> {
     #[predicate(prophetic)]
     #[open]