Add various specs for HashSet, FSet, and iterators (ranges, filter_ma…

…p, rev)

- Also strengthen the spec of filter

Note: the spec for `Borrow` is required for `HashSet::contains`

creusot-contracts/src/logic.rs

@@ -5,7 +5,7 @@
 #![cfg_attr(not(creusot), allow(unused_imports))]
 
 mod fmap;
-mod fset;
+pub mod fset;
 mod int;
 mod mapping;
 pub mod ops;

creusot-contracts/src/logic/fset.rs

@@ -1,4 +1,4 @@
-use crate::*;
+use crate::{logic::Mapping, *};
 
 /// A finite set type usable in pearlite and `ghost!` blocks.
 ///
@@ -143,6 +143,15 @@ impl<T: ?Sized> FSet<T> {
         Self::is_subset(other, self)
     }
 
+    /// Returns `true` if `self` and `other` are disjoint.
+    #[trusted]
+    #[predicate]
+    #[creusot::builtins = "set.Fset.disjoint"]
+    pub fn disjoint(self, other: Self) -> bool {
+        let _ = other;
+        dead
+    }
+
     /// Returns the number of elements in the set, also called its length.
     #[trusted]
     #[logic]
@@ -172,8 +181,6 @@ impl<T: ?Sized> FSet<T> {
     /// Returns `true` if `self` and `other` contain exactly the same elements.
     ///
     /// This is in fact equivalent with normal equality.
-    // FIXME: remove `trusted`
-    #[trusted]
     #[open]
     #[predicate]
     #[ensures(result ==> self == other)]
@@ -187,6 +194,119 @@ impl<T: ?Sized> FSet<T> {
     }
 }
 
+impl<T> FSet<T> {
+    /// Returns the set containing only `x`.
+    #[logic]
+    #[open]
+    #[ensures(forall<y: T> result.contains(y) == (x == y))]
+    pub fn singleton(x: T) -> Self {
+        FSet::EMPTY.insert(x)
+    }
+
+    /// Returns the union of sets `f(t)` over all `t: T`.
+    #[logic]
+    #[open]
+    #[ensures(forall<y: U> result.contains(y) == exists<x: T> self.contains(x) && f.get(x).contains(y))]
+    #[variant(self.len())]
+    pub fn unions<U>(self, f: Mapping<T, FSet<U>>) -> FSet<U> {
+        if self.len() == 0 {
+            FSet::EMPTY
+        } else {
+            let x = self.peek();
+            f.get(x).union(self.remove(x).unions(f))
+        }
+    }
+
+    /// Flipped `map`.
+    #[logic]
+    #[trusted]
+    #[creusot::builtins = "set.Fset.map"]
+    pub fn fmap<U>(_: Mapping<T, U>, _: Self) -> FSet<U> {
+        dead
+    }
+
+    /// Returns the image of a set by a function.
+    #[logic]
+    #[open]
+    pub fn map<U>(self, f: Mapping<T, U>) -> FSet<U> {
+        FSet::fmap(f, self)
+    }
+
+    /// Returns the subset of elements of `self` which satisfy the predicate `f`.
+    #[logic]
+    #[trusted]
+    #[creusot::builtins = "set.Fset.filter"]
+    pub fn filter(self, f: Mapping<T, bool>) -> Self {
+        let _ = f;
+        dead
+    }
+
+    /// Returns the set of sequences whose head is in `s` and whose tail is in `ss`.
+    #[logic]
+    #[trusted] // TODO: remove. Needs support for closures in logic functions with constraints
+    #[open]
+    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (0 < xs.len() && s.contains(xs[0]) && ss.contains(xs.tail())))]
+    pub fn cons(s: FSet<T>, ss: FSet<Seq<T>>) -> FSet<Seq<T>> {
+        s.unions(|x| ss.map(|xs: Seq<_>| xs.push_front(x)))
+    }
+
+    /// Returns the set of concatenations of a sequence in `s` and a sequence in `t`.
+    #[logic]
+    #[trusted] // TODO: remove. Needs support for closures in logic functions with constraints
+    #[open]
+    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (exists<ys: Seq<T>, zs: Seq<T>> s.contains(ys) && t.contains(zs) && xs == ys.concat(zs)))]
+    pub fn concat(s: FSet<Seq<T>>, t: FSet<Seq<T>>) -> FSet<Seq<T>> {
+        s.unions(|ys: Seq<_>| t.map(|zs| ys.concat(zs)))
+    }
+
+    /// Returns the set of sequences of length `n` whose elements are in `self`.
+    #[open]
+    #[logic]
+    #[requires(n >= 0)]
+    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (xs.len() == n && forall<x: T> xs.contains(x) ==> self.contains(x)))]
+    #[variant(n)]
+    pub fn replicate(self, n: Int) -> FSet<Seq<T>> {
+        pearlite! {
+            if n == 0 {
+                proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::EMPTY };
+                FSet::singleton(Seq::EMPTY)
+            } else {
+                proof_assert! { forall<xs: Seq<T>, i: Int> 0 < i && i < xs.len() ==> xs[i] == xs.tail()[i-1] };
+                FSet::cons(self, self.replicate(n - 1))
+            }
+        }
+    }
+
+    /// Returns the set of sequences of length at most `n` whose elements are in `self`.
+    #[open]
+    #[logic]
+    #[requires(n >= 0)]
+    #[ensures(forall<xs: Seq<T>> result.contains(xs) == (xs.len() <= n && forall<x: T> xs.contains(x) ==> self.contains(x)))]
+    #[variant(n)]
+    pub fn replicate_up_to(self, n: Int) -> FSet<Seq<T>> {
+        pearlite! {
+            if n == 0 {
+                proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::EMPTY };
+                FSet::singleton(Seq::EMPTY)
+            } else {
+                self.replicate_up_to(n - 1).union(self.replicate(n))
+            }
+        }
+    }
+}
+
+impl FSet<Int> {
+    /// Return the interval of integers in `[i, j)`.
+    #[logic]
+    #[open]
+    #[trusted]
+    #[creusot::builtins = "set.FsetInt.interval"]
+    pub fn interval(i: Int, j: Int) -> FSet<Int> {
+        let _ = (i, j);
+        dead
+    }
+}
+
 /// Ghost definitions
 impl<T: ?Sized> FSet<T> {
     /// Create a new, empty set on the ghost heap.
@@ -338,3 +458,84 @@ impl<T: ?Sized> Invariant for FSet<T> {
         pearlite! { forall<x: &T> self.contains(*x) ==> inv(*x) }
     }
 }
+
+// Properties
+
+/// Distributivity of `unions` over `union`.
+#[logic]
+#[open]
+#[ensures(forall<s1: FSet<T>, s2: FSet<T>, f: Mapping<T, FSet<U>>> s1.union(s2).unions(f) == s1.unions(f).union(s2.unions(f)))]
+#[ensures(forall<s: FSet<T>, f: Mapping<T, FSet<U>>, g: Mapping<T, FSet<U>>>
+    s.unions(|x| f.get(x).union(g.get(x))) == s.unions(f).union(s.unions(g)))]
+pub fn unions_union<T, U>() {}
+
+/// Distributivity of `map` over `union`.
+#[logic]
+#[open]
+#[ensures(forall<s: FSet<T>, t: FSet<T>, f: Mapping<T, U>> s.union(t).map(f) == s.map(f).union(t.map(f)))]
+pub fn map_union<T, U>() {}
+
+/// Distributivity of `concat` over `union`.
+#[logic]
+#[open]
+#[ensures(forall<s1: FSet<Seq<T>>, s2: FSet<Seq<T>>, t: FSet<Seq<T>>>
+    FSet::concat(s1.union(s2), t) == FSet::concat(s1, t).union(FSet::concat(s2, t)))]
+#[ensures(forall<s: FSet<Seq<T>>, t1: FSet<Seq<T>>, t2: FSet<Seq<T>>>
+    FSet::concat(s, t1.union(t2)) == FSet::concat(s, t1).union(FSet::concat(s, t2)))]
+pub fn concat_union<T>() {}
+
+/// Distributivity of `cons` over `union`.
+#[logic]
+#[open]
+#[ensures(forall<s: FSet<T>, t: FSet<Seq<T>>, u: FSet<Seq<T>>> FSet::concat(FSet::cons(s, t), u) == FSet::cons(s, FSet::concat(t, u)))]
+pub fn cons_concat<T>() {
+    proof_assert! { forall<x: T, xs: Seq<T>, ys: Seq<T>> xs.push_front(x).concat(ys) == xs.concat(ys).push_front(x) };
+    proof_assert! { forall<x: T, ys: Seq<T>> ys.push_front(x).tail() == ys };
+    proof_assert! { forall<ys: Seq<T>> 0 < ys.len() ==> ys == ys.tail().push_front(ys[0]) };
+}
+
+/// Distributivity of `replicate` over `union`.
+#[logic]
+#[open]
+#[requires(0 <= n && 0 <= m)]
+#[ensures(s.replicate(n + m) == FSet::concat(s.replicate(n), s.replicate(m)))]
+#[variant(n)]
+pub fn concat_replicate<T>(n: Int, m: Int, s: FSet<T>) {
+    pearlite! {
+        if n == 0 {
+            concat_empty(s.replicate(m));
+        } else {
+            cons_concat::<T>();
+            concat_replicate(n - 1, m, s);
+        }
+    }
+}
+
+/// The neutral element of `FSet::concat` is `FSet::singleton(Seq::EMPTY)`.
+#[logic]
+#[open]
+#[ensures(FSet::concat(FSet::singleton(Seq::EMPTY), s) == s)]
+#[ensures(FSet::concat(s, FSet::singleton(Seq::EMPTY)) == s)]
+pub fn concat_empty<T>(s: FSet<Seq<T>>) {
+    proof_assert! { forall<xs: Seq<T>> xs.concat(Seq::EMPTY) == xs };
+    proof_assert! { forall<xs: Seq<T>> Seq::EMPTY.concat(xs) == xs };
+}
+
+/// An equation relating `s.replicate_up_to(m)` and `s.replicate_up_to(n)`.
+#[logic]
+#[open]
+#[requires(0 <= n && n < m)]
+#[ensures(s.replicate_up_to(m) == s.replicate_up_to(n).union(
+    FSet::concat(s.replicate(n + 1), s.replicate_up_to(m - n - 1))))]
+#[variant(m)]
+pub fn concat_replicate_up_to<T>(n: Int, m: Int, s: FSet<T>) {
+    pearlite! {
+        if n + 1 == m {
+            concat_empty(s.replicate(n + 1));
+        } else {
+            concat_union::<T>();
+            concat_replicate(n, m - n - 1, s);
+            concat_replicate_up_to(n, m - 1, s);
+        }
+    }
+}

creusot-contracts/src/std.rs

@@ -1,6 +1,7 @@
 pub use ::std::*;
 
 pub mod array;
+pub mod borrow;
 pub mod boxed;
 pub mod clone;
 pub mod collections {

creusot-contracts/src/std/borrow.rs

@@ -0,0 +1,22 @@
+use crate::*;
+use ::std::borrow::Borrow;
+
+// "In particular Eq, Ord and Hash must be equivalent for borrowed and owned values:
+// x.borrow() == y.borrow() should give the same result as x == y."
+// https://doc.rust-lang.org/std/borrow/trait.Borrow.html
+
+extern_spec! {
+    mod std {
+        mod borrow {
+            trait Borrow<Borrowed>
+            where Borrowed: ?Sized
+            {
+                #[ensures(result.deep_model() == self.deep_model())]
+                fn borrow(&self) -> &Borrowed
+                where
+                    Self: DeepModel,
+                    Borrowed: DeepModel<DeepModelTy = Self::DeepModelTy>;
+            }
+        }
+    }
+}

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

@@ -3,7 +3,7 @@ use crate::{
     std::iter::{FromIterator, IntoIterator, Iterator},
     *,
 };
-use ::std::{collections::hash_set::*, hash::*};
+use ::std::{borrow::Borrow, collections::hash_set::*, hash::*};
 
 impl<T: DeepModel, S> View for HashSet<T, S> {
     type ViewTy = FSet<T::DeepModelTy>;
@@ -31,6 +31,12 @@ extern_spec! {
                 {
                     #[ensures(result@ == self@.intersection(other@))]
                     fn intersection<'a>(&'a self, other: &'a HashSet<T,S>) -> Intersection<'a, T, S>;
+
+                    #[ensures(result == self@.contains(value.deep_model()))]
+                    fn contains<Q: ?Sized>(&self, value: &Q) -> bool
+                    where
+                        T: Borrow<Q>,
+                        Q: Eq + Hash + DeepModel<DeepModelTy = T::DeepModelTy>;
                 }
             }
         }

creusot-contracts/src/std/iter.rs

@@ -6,12 +6,14 @@ mod copied;
 mod empty;
 mod enumerate;
 mod filter;
+mod filter_map;
 mod fuse;
 mod map;
 mod map_inv;
 mod once;
 mod range;
 mod repeat;
+mod rev;
 mod skip;
 mod take;
 mod zip;
@@ -20,9 +22,11 @@ pub use cloned::ClonedExt;
 pub use copied::CopiedExt;
 pub use enumerate::EnumerateExt;
 pub use filter::FilterExt;
+pub use filter_map::FilterMapExt;
 pub use fuse::FusedIterator;
 pub use map::MapExt;
 pub use map_inv::MapInv;
+pub use rev::RevExt;
 pub use skip::SkipExt;
 pub use take::TakeExt;
 pub use zip::ZipExt;
@@ -94,6 +98,21 @@ pub trait FromIterator<A>: ::std::iter::FromIterator<A> {
     fn from_iter_post(prod: Seq<A>, res: Self) -> bool;
 }
 
+pub trait DoubleEndedIterator: ::std::iter::DoubleEndedIterator + Iterator {
+    #[predicate(prophetic)]
+    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool;
+
+    #[law]
+    #[ensures(self.produces_back(Seq::EMPTY, self))]
+    fn produces_back_refl(self);
+
+    #[law]
+    #[requires(a.produces_back(ab, b))]
+    #[requires(b.produces_back(bc, c))]
+    #[ensures(a.produces_back(ab.concat(bc), c))]
+    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self);
+}
+
 extern_spec! {
     mod std {
         mod iter {
@@ -144,6 +163,13 @@ extern_spec! {
                 fn filter<P>(self, f: P) -> Filter<Self, P>
                     where  P : for<'a> FnMut(&Self_::Item) -> bool;
 
+                #[pure]
+                #[requires(filter_map::immutable(f))]
+                #[requires(filter_map::no_precondition(f))]
+                #[requires(filter_map::precise(f))]
+                #[ensures(result.iter() == self && result.func() == f)]
+                fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>
+                    where F : for<'a> FnMut(Self_::Item) -> Option<B>;
 
                 #[pure]
                 // These two requirements are here only to prove the absence of overflows
@@ -167,6 +193,11 @@ extern_spec! {
                     resolve(&^done) && done.completed() && self.produces(prod, *done) && B::from_iter_post(prod, result))]
                 fn collect<B>(self) -> B
                     where B: FromIterator<Self::Item>;
+
+                #[pure]
+                #[ensures(result.iter() == self)]
+                fn rev(self) -> Rev<Self>
+                    where Self: Sized + DoubleEndedIterator;
             }
 
             trait IntoIterator
@@ -200,6 +231,15 @@ extern_spec! {
             #[pure]
             #[ensures(result@ == elt)]
             fn repeat<T: Clone>(elt: T) -> Repeat<T>;
+
+            trait DoubleEndedIterator
+                where Self: DoubleEndedIterator {
+                #[ensures(match result {
+                    None => self.completed(),
+                    Some(v) => (*self).produces_back(Seq::singleton(v), ^self)
+                })]
+                fn next_back(&mut self) -> Option<Self::Item>;
+            }
         }
     }
 }