creusot-contracts: Add Iterator impls for [T;N], &mut I (#1290)

creusot-rs · Dec 11, 2024 · b23abd7 · b23abd7
2 parents 8dd770c + 677c50d
commit b23abd7
Show file tree

Hide file tree

Showing 18 changed files with 7,992 additions and 6,591 deletions.
diff --git a/creusot-contracts/src/std/array.rs b/creusot-contracts/src/std/array.rs
@@ -1,4 +1,9 @@
-use crate::{invariant::*, *};
+use crate::{
+    invariant::*,
+    std::iter::{IntoIterator, Iterator},
+    *,
+};
+use ::std::array::*;
 
 impl<T, const N: usize> Invariant for [T; N] {
     #[predicate(prophetic)]
@@ -37,3 +42,54 @@ impl<T: DeepModel, const N: usize> DeepModel for [T; N] {
         dead
     }
 }
+
+impl<T, const N: usize> View for IntoIter<T, N> {
+    type ViewTy = Seq<T>;
+
+    #[logic]
+    #[trusted]
+    #[open]
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+}
+
+impl<T, const N: usize> Iterator for IntoIter<T, N> {
+    #[open]
+    #[predicate(prophetic)]
+    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
+        pearlite! { self@ == visited.concat(o@) }
+    }
+
+    #[open]
+    #[predicate(prophetic)]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@ == Seq::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) {}
+}
+
+impl<T, const N: usize> IntoIterator for [T; N] {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate(prophetic)]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@ }
+    }
+}
diff --git a/creusot-contracts/src/std/iter.rs b/creusot-contracts/src/std/iter.rs
@@ -147,7 +147,7 @@ extern_spec! {
 
                 #[pure]
                 // These two requirements are here only to prove the absence of overflows
-                #[requires(forall<i: &mut Self_> i.completed() ==> i.produces(Seq::EMPTY, ^i))]
+                #[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>;
@@ -203,3 +203,29 @@ extern_spec! {
         }
     }
 }
+
+impl<I: Iterator + ?Sized> Iterator for &mut I {
+    #[open]
+    #[predicate(prophetic)]
+    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
+        pearlite! { (*self).produces(visited, *o) && ^self == ^o }
+    }
+
+    #[open]
+    #[predicate(prophetic)]
+    fn completed(&mut self) -> bool {
+        pearlite! { (*self).completed() && ^*self == ^^self }
+    }
+
+    #[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) {}
+}
diff --git a/creusot-contracts/src/std/iter/enumerate.rs b/creusot-contracts/src/std/iter/enumerate.rs
@@ -46,7 +46,7 @@ impl<I: Iterator> Invariant for Enumerate<I> {
                 #![trigger 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))
+            && (forall<i: &mut I> (*i).completed() ==> (*i).produces(Seq::EMPTY, ^i))
         }
     }
 }

diff --git a/creusot-contracts/src/std/iter/zip.rs b/creusot-contracts/src/std/iter/zip.rs
@@ -33,8 +33,8 @@ impl<A: Iterator, B: Iterator> Iterator for Zip<A, B> {
                    *a == (*self).itera() && *b == (*self).iterb()
                 && ^a == (^self).itera() && ^b == (^self).iterb()
                 && (a.completed() && resolve(&b)
-                    || exists<x: A::Item> inv(x) && a.produces(Seq::singleton(x), ^a) &&
-                                          resolve(&x) && b.completed())
+                    || exists<x: A::Item> inv(x) && (*a).produces(Seq::singleton(x), ^a) &&
+                                          resolve(&x) && (*b).completed())
         }
     }