Add specs for iterators of HashMap and HashSet

creusot-contracts/src/logic/fset.rs

@@ -114,6 +114,17 @@ impl<T: ?Sized> FSet<T> {
         dead
     }
 
+    /// Returns a new set, which is the union of `self` and `other`.
+    ///
+    /// An element is in the result if it is in `self` _or_ if it is in `other`.
+    #[trusted]
+    #[logic]
+    #[creusot::builtins = "set.Fset.inter"]
+    pub fn intersection(self, other: Self) -> Self {
+        let _ = other;
+        dead
+    }
+
     /// Returns `true` if every element of `self` is in `other`.
     #[trusted]
     #[predicate]

creusot-contracts/src/logic/seq.rs

@@ -376,6 +376,16 @@ impl<T: ?Sized> Seq<T> {
     {
         self.sorted_range(0, self.len())
     }
+
+    #[open]
+    #[logic]
+    #[ensures(forall<a: Seq<T>, b: Seq<T>, x: T>
+        a.concat(b).contains(x) == a.contains(x) || b.contains(x))]
+    pub fn concat_contains()
+    where
+        T: Sized,
+    {
+    }
 }
 
 impl<T: ?Sized> Seq<&T> {

creusot-contracts/src/std.rs

@@ -3,6 +3,10 @@ pub use ::std::*;
 pub mod array;
 pub mod boxed;
 pub mod clone;
+pub mod collections {
+    pub mod hash_map;
+    pub mod hash_set;
+}
 pub mod cmp;
 pub mod default;
 pub mod deque;

creusot-contracts/src/std/collections/hash_map.rs

@@ -0,0 +1,244 @@
+use crate::{
+    logic::FMap,
+    std::iter::{FromIterator, IntoIterator, Iterator},
+    *,
+};
+use ::std::{
+    collections::hash_map::*,
+    default::Default,
+    hash::{BuildHasher, Hash},
+};
+
+impl<K, V, S> View for HashMap<K, V, S> {
+    type ViewTy = FMap<K, V>;
+
+    #[logic]
+    #[trusted]
+    #[open]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+extern_spec! {
+    mod std {
+        mod collections {
+            mod hash_map {
+                impl<K, V, S> HashMap<K, V, S> {
+                    #[ensures(self@ == result@)]
+                    fn iter(&self) -> Iter<'_, K, V>;
+
+                    #[ensures(self.into_iter_post(result))]
+                    fn iter_mut(&mut self) -> IterMut<'_, K, V>;
+                }
+            }
+        }
+    }
+}
+
+impl<'a, K, V> View for Iter<'a, K, V> {
+    type ViewTy = FMap<K, V>;
+
+    #[logic]
+    #[trusted]
+    #[open]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+impl<'a, K, V> Iterator for Iter<'a, K, V> {
+    #[open]
+    #[predicate(prophetic)]
+    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
+        // self@ equals the union of visited (viewed as a fmap) and o@
+        pearlite! {
+            self@.len() == visited.len() + o@.len()
+            && (forall<k: K, v: V> visited.contains((&k, &v))
+                ==> self@.get(k) == Some(v) && o@.get(k) == None)
+            && (forall<k: K, v: V> o@.get(k) == Some(v)
+                ==> self@.get(k) == Some(v) && !(exists<v2: V> visited.contains((&k, &v2))))
+            && (forall<k: K, v: V> self@.get(k) == Some(v)
+                ==> visited.contains((&k, &v)) || (o@.get(k) == Some(v)))
+            && (forall<k: &K, v1: &V, v2: &V, i1: Int, i2: Int>
+                visited.get(i1) == Some((k, v1)) && visited.get(i2) == Some((k, v2))
+                ==> i1 == i2)
+        }
+    }
+
+    #[open]
+    #[predicate(prophetic)]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@.is_empty() }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(self.produces(Seq::EMPTY, self))]
+    fn produces_refl(self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
+        proof_assert! { forall<i: Int> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }
+    }
+}
+
+impl<K, V> View for IntoIter<K, V> {
+    type ViewTy = FMap<K, V>;
+
+    #[logic]
+    #[trusted]
+    #[open]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+impl<K, V> Iterator for IntoIter<K, V> {
+    #[open]
+    #[predicate(prophetic)]
+    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
+        // self@ equals the union of visited (viewed as a fmap) and o@
+        pearlite! {
+            self@.len() == visited.len() + o@.len()
+            && (forall<k: K, v: V> visited.contains((k, v))
+                ==> self@.get(k) == Some(v) && o@.get(k) == None)
+            && (forall<k: K, v: V> o@.get(k) == Some(v)
+                ==> self@.get(k) == Some(v) && !(exists<v2: V> visited.contains((k, v2))))
+            && (forall<k: K, v: V> self@.get(k) == Some(v)
+                ==> visited.contains((k, v)) || (o@.get(k) == Some(v)))
+            && (forall<k: K, v1: V, v2: V, i1: Int, i2: Int>
+                visited.get(i1) == Some((k, v1)) && visited.get(i2) == Some((k, v2))
+                ==> i1 == i2)
+        }
+    }
+
+    #[open]
+    #[predicate(prophetic)]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@.is_empty() }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(self.produces(Seq::EMPTY, self))]
+    fn produces_refl(self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
+        proof_assert! { forall<i: Int> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }
+    }
+}
+
+impl<'a, K, V> View for IterMut<'a, K, V> {
+    type ViewTy = FMap<K, &'a mut V>;
+
+    #[logic]
+    #[trusted]
+    #[open]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+impl<'a, K, V> Iterator for IterMut<'a, K, V> {
+    #[open]
+    #[predicate(prophetic)]
+    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
+        // self@ equals the union of visited (viewed as a fmap) and o@
+        pearlite! {
+            self@.len() == visited.len() + o@.len()
+            && (forall<k: K, v: &mut V> visited.contains((&k, v))
+                ==> self@.get(k) == Some(v) && o@.get(k) == None)
+            && (forall<k: K, v: &mut V> o@.get(k) == Some(v)
+                ==> self@.get(k) == Some(v) && !(exists<v2: &mut V> visited.contains((&k, v2))))
+            && (forall<k: K, v: &mut V> self@.get(k) == Some(v)
+                ==> visited.contains((&k, v)) || (o@.get(k) == Some(v)))
+            && (forall<k: &K, v1: &mut V, v2: &mut V, i1: Int, i2: Int>
+                visited.get(i1) == Some((k, v1)) && visited.get(i2) == Some((k, v2))
+                ==> i1 == i2)
+        }
+    }
+
+    #[open]
+    #[predicate(prophetic)]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@.is_empty() }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(self.produces(Seq::EMPTY, self))]
+    fn produces_refl(self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
+        proof_assert! { forall<i: Int> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }
+    }
+}
+
+impl<K, V, S> IntoIterator for HashMap<K, V, S> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@ }
+    }
+}
+
+impl<K, V, S> IntoIterator for &HashMap<K, V, S> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@ }
+    }
+}
+
+impl<K, V, S> IntoIterator for &mut HashMap<K, V, S> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate(prophetic)]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { forall<k: K> (*self)@.contains(k) == (^self)@.contains(k)
+        && (forall<k: K> (*self)@.contains(k) == res@.contains(k))
+        && forall<k: K> (*self)@.contains(k) ==> (*self)@[k] == *res@[k] && (^self)@[k] == ^res@[k] }
+    }
+}
+
+impl<K: Eq + Hash, V, S: Default + BuildHasher> FromIterator<(K, V)> for HashMap<K, V, S> {
+    #[predicate]
+    #[open]
+    fn from_iter_post(prod: Seq<(K, V)>, res: Self) -> bool {
+        pearlite! { forall<k: K, v: V> (res@.get(k) == Some(v))
+        == (exists<i: Int> 0 <= i && i < prod.len() && prod[i] == (k, v)
+            && forall<j: Int> i < j && j < prod.len() ==> prod[j].0 != k) }
+    }
+}