No inv in iterators (#1291)

creusot-rs · Dec 5, 2024 · 9c87f9c · 9c87f9c
2 parents 5737d8f + 13fe73c
commit 9c87f9c
Show file tree

Hide file tree

Showing 124 changed files with 6,803 additions and 14,361 deletions.
diff --git a/creusot-contracts/src/std/iter.rs b/creusot-contracts/src/std/iter.rs
@@ -1,4 +1,4 @@
-use crate::{invariant::*, *};
+use crate::*;
 pub use ::std::iter::*;
 
 mod cloned;
@@ -35,22 +35,18 @@ pub trait Iterator: ::std::iter::Iterator {
     fn completed(&mut self) -> bool;
 
     #[law]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self);
 
     #[law]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[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);
 
     // FIXME: remove `trusted`
     #[trusted]
-    #[requires(forall<e : Self::Item, i2 : Self> inv(e) && inv(i2) ==>
+    #[requires(forall<e : Self::Item, i2 : Self>
                     self.produces(Seq::singleton(e), i2) ==>
                     func.precondition((e, Snapshot::new(Seq::EMPTY))))]
     #[requires(MapInv::<Self, _, F>::reinitialize())]
@@ -131,7 +127,7 @@ extern_spec! {
                         Self: Sized + Iterator<Item = &'a T>;
 
                 #[pure]
-                #[requires(forall<e : _, i2 : _> inv(e) && inv(i2) ==>
+                #[requires(forall<e : _, i2 : _>
                                 self.produces(Seq::singleton(e), i2) ==>
                                 f.precondition((e,)))]
                 #[requires(map::reinitialize::<Self_, B, F>())]
@@ -151,10 +147,8 @@ extern_spec! {
 
                 #[pure]
                 // These two requirements are here only to prove the absence of overflows
-                #[requires(forall<i: &mut Self_> inv(i) && i.completed() ==> i.produces(Seq::EMPTY, ^i))]
-                #[requires(forall<s: Seq<Self_::Item>, i: Self_>
-                            inv(s) && inv(i) && self.produces(s, i) ==>
-                            s.len() < std::usize::MAX@)]
+                #[requires(forall<i: &mut Self_> i.completed() ==> i.produces(Seq::EMPTY, ^i))]
+                #[requires(forall<s: Seq<Self_::Item>, i: Self_> self.produces(s, i) ==> s.len() < std::usize::MAX@)]
                 #[ensures(result.iter() == self && result.n() == 0)]
                 fn enumerate(self) -> Enumerate<Self>;
 
@@ -170,8 +164,7 @@ extern_spec! {
 
                 // TODO: Investigate why Self_ needed
                 #[ensures(exists<done : &mut Self_, prod: Seq<_>>
-                    inv(done) && inv(prod) && resolve(&^done) && done.completed() &&
-                    self.produces(prod, *done) && B::from_iter_post(prod, result))]
+                    resolve(&^done) && done.completed() && self.produces(prod, *done) && B::from_iter_post(prod, result))]
                 fn collect<B>(self) -> B
                     where B: FromIterator<Self::Item>;
             }
@@ -190,7 +183,6 @@ extern_spec! {
 
                 #[requires(iter.into_iter_pre())]
                 #[ensures(exists<into_iter: T::IntoIter, done: &mut T::IntoIter, prod: Seq<A>>
-                            inv(into_iter) && inv(done) && inv(prod) &&
                             iter.into_iter_post(into_iter) &&
                             into_iter.produces(prod, *done) && done.completed() && resolve(&^done) &&
                             Self_::from_iter_post(prod, result))]

diff --git a/creusot-contracts/src/std/iter/cloned.rs b/creusot-contracts/src/std/iter/cloned.rs
@@ -37,35 +37,28 @@ where
     #[predicate(prophetic)]
     fn completed(&mut self) -> bool {
         pearlite! {
-            exists<inner : &mut _> inv(inner)
-                && *inner == self.iter()
-                && ^inner == (^self).iter()
-                && inner.completed()
+            exists<inner : &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed()
         }
     }
 
     #[open]
     #[predicate(prophetic)]
     fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
         pearlite! {
-            exists<s: Seq<&'a T>> inv(s)
-                && self.iter().produces(s, o.iter())
+            exists<s: Seq<&'a T>>
+                   self.iter().produces(s, o.iter())
                 && visited.len() == s.len()
                 && forall<i: Int> 0 <= i && i < s.len() ==> visited[i] == *s[i]
         }
     }
 
     #[law]
     #[open(self)]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open(self)]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]

diff --git a/creusot-contracts/src/std/iter/copied.rs b/creusot-contracts/src/std/iter/copied.rs
@@ -37,35 +37,28 @@ where
     #[predicate(prophetic)]
     fn completed(&mut self) -> bool {
         pearlite! {
-            exists<inner : &mut _> inv(inner)
-                && *inner == self.iter()
-                && ^inner == (^self).iter()
-                && inner.completed()
+            exists<inner : &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed()
         }
     }
 
     #[open]
     #[predicate(prophetic)]
     fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
         pearlite! {
-            exists<s: Seq<&'a T>> inv(s)
-                && self.iter().produces(s, o.iter())
+            exists<s: Seq<&'a T>>
+                   self.iter().produces(s, o.iter())
                 && visited.len() == s.len()
                 && forall<i: Int> 0 <= i && i < s.len() ==> visited[i] == *s[i]
         }
     }
 
     #[law]
     #[open(self)]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open(self)]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]

diff --git a/creusot-contracts/src/std/iter/empty.rs b/creusot-contracts/src/std/iter/empty.rs
@@ -1,4 +1,4 @@
-use crate::{invariant::*, std::iter::Empty, *};
+use crate::{std::iter::Empty, *};
 
 impl<T> Iterator for Empty<T> {
     #[open]
@@ -15,15 +15,11 @@ impl<T> Iterator for Empty<T> {
 
     #[law]
     #[open(self)]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open(self)]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]

diff --git a/creusot-contracts/src/std/iter/enumerate.rs b/creusot-contracts/src/std/iter/enumerate.rs
@@ -44,7 +44,7 @@ impl<I: Iterator> Invariant for Enumerate<I> {
         pearlite! {
             (forall<s: Seq<I::Item>, i: I>
                 #![trigger self.iter().produces(s, i)]
-                inv(s) && inv(i) && self.iter().produces(s, i) ==>
+                self.iter().produces(s, i) ==>
                 self.n() + s.len() < std::usize::MAX@)
             && (forall<i: &mut I> i.completed() ==> i.produces(Seq::EMPTY, ^i))
         }
@@ -59,9 +59,7 @@ where
     #[predicate(prophetic)]
     fn completed(&mut self) -> bool {
         pearlite! {
-            exists<inner : &mut _> inv(inner)
-                && *inner == self.iter()
-                && ^inner == (^self).iter()
+            exists<inner : &mut _> *inner == self.iter() && ^inner == (^self).iter()
                 && inner.completed()
                 && self.n() == (^self).n()
         }
@@ -72,24 +70,20 @@ where
     fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
         pearlite! {
             visited.len() == o.n() - self.n()
-            && exists<s: Seq<I::Item>> inv(s)
-                && self.iter().produces(s, o.iter())
+            && exists<s: Seq<I::Item>>
+                   self.iter().produces(s, o.iter())
                 && visited.len() == s.len()
                 && forall<i: Int> 0 <= i && i < s.len() ==> visited[i].0@ == self.n() + i && visited[i].1 == s[i]
         }
     }
 
     #[law]
     #[open(self)]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open(self)]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]

diff --git a/creusot-contracts/src/std/iter/filter.rs b/creusot-contracts/src/std/iter/filter.rs
@@ -84,6 +84,7 @@ where
     #[predicate(prophetic)]
     fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
         pearlite! {
+            self.invariant() ==>
             self.func().unnest(succ.func()) &&
             // f here is a mapping from indices of `visited` to those of `s`, where `s` is the whole sequence produced by the underlying iterator
             // Interestingly, Z3 guesses `f` quite readily but gives up *totally* on `s`. However, the addition of the final assertions on the correctness of the values
@@ -101,15 +102,11 @@ where
 
     #[law]
     #[open(self)]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open(self)]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]

diff --git a/creusot-contracts/src/std/iter/fuse.rs b/creusot-contracts/src/std/iter/fuse.rs
@@ -1,4 +1,4 @@
-use crate::{invariant::*, std::iter::Fuse, *};
+use crate::{std::iter::Fuse, *};
 
 impl<I: Iterator> View for Fuse<I> {
     type ViewTy = Option<I>;
@@ -17,7 +17,7 @@ impl<I: Iterator> Iterator for Fuse<I> {
     #[predicate(prophetic)]
     fn completed(&mut self) -> bool {
         pearlite! {
-            (self@ == None || exists<it:&mut I> inv(it) && it.completed() && self@ == Some(*it)) &&
+            (self@ == None || exists<it:&mut I> it.completed() && self@ == Some(*it)) &&
             (^self)@ == None
         }
     }
@@ -38,15 +38,11 @@ impl<I: Iterator> Iterator for Fuse<I> {
 
     #[law]
     #[open]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]
@@ -55,9 +51,6 @@ impl<I: Iterator> Iterator for Fuse<I> {
 
 pub trait FusedIterator: ::std::iter::FusedIterator + Iterator {
     #[law]
-    #[requires(inv(self))]
-    #[requires(inv(next))]
-    #[requires(inv(steps))]
     #[requires(self.completed())]
     #[requires((^self).produces(steps, next))]
     #[ensures(steps == Seq::EMPTY && ^self == next)]
@@ -67,9 +60,6 @@ pub trait FusedIterator: ::std::iter::FusedIterator + Iterator {
 impl<I: Iterator> FusedIterator for Fuse<I> {
     #[law]
     #[open]
-    #[requires(inv(self))]
-    #[requires(inv(next))]
-    #[requires(inv(steps))]
     #[requires(self.completed())]
     #[requires((^self).produces(steps, next))]
     #[ensures(steps == Seq::EMPTY && ^self == next)]

diff --git a/creusot-contracts/src/std/iter/map.rs b/creusot-contracts/src/std/iter/map.rs
@@ -50,8 +50,9 @@ where
     #[predicate(prophetic)]
     fn completed(&mut self) -> bool {
         pearlite! {
-        (exists<inner : &mut _> inv(inner) && *inner == self.iter() && ^inner == (^self).iter()
-            && inner.completed()) && (*self).func() == (^self).func() }
+            (exists<inner : &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed())
+            && (*self).func() == (^self).func()
+        }
     }
 
     #[open]
@@ -60,10 +61,10 @@ where
     fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
         pearlite! {
             self.func().unnest(succ.func())
-            && exists<fs: Seq<&mut F>> inv(fs) && fs.len() == visited.len()
+            && exists<fs: Seq<&mut F>> fs.len() == visited.len()
             && exists<s : Seq<I::Item>>
                 #![trigger self.iter().produces(s, succ.iter())]
-                inv(s) && s.len() == visited.len() && self.iter().produces(s, succ.iter())
+                s.len() == visited.len() && self.iter().produces(s, succ.iter())
             && (forall<i : Int> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == *fs[i])
             && if visited.len() == 0 { self.func() == succ.func() }
                else { *fs[0] == self.func() &&  ^fs[visited.len() - 1] == succ.func() }
@@ -76,15 +77,11 @@ where
 
     #[law]
     #[open(self)]
-    #[requires(inv(self))]
     #[ensures(self.produces(Seq::EMPTY, self))]
     fn produces_refl(self) {}
 
     #[law]
     #[open(self)]
-    #[requires(inv(a))]
-    #[requires(inv(b))]
-    #[requires(inv(c))]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]
@@ -101,7 +98,6 @@ where
     pearlite! {
         forall<e: I::Item, i: I>
             #![trigger iter.produces(Seq::singleton(e), i)]
-            inv(e) && inv(i) ==>
             iter.produces(Seq::singleton(e), i) ==>
             func.precondition((e,))
     }
@@ -117,7 +113,7 @@ where
     pearlite! {
         forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
             #![trigger iter.produces(s.push_back(e1).push_back(e2), i), (*f).postcondition_mut((e1,), ^f, b)]
-            inv(s) && inv(e1) && inv(e2) && inv(f) && inv(i) && func.unnest(*f) ==>
+            func.unnest(*f) ==>
             iter.produces(s.push_back(e1).push_back(e2), i) ==>
             (*f).precondition((e1,)) ==>
             (*f).postcondition_mut((e1,), ^f, b) ==>
@@ -134,8 +130,6 @@ where
 {
     pearlite! {
         forall<iter: &mut I, func: F>
-            inv(iter) && inv(func) ==>
-            iter.completed() ==>
-            next_precondition(^iter, func) && preservation(^iter, func)
+            iter.completed() ==> next_precondition(^iter, func) && preservation(^iter, func)
     }
 }