Add IndexLogic instance for Range<Int>

creusot-rs · Sep 21, 2023 · b36dedd · b36dedd
1 parent 159a0a7
commit b36dedd
Show file tree

Hide file tree

Showing 6 changed files with 274 additions and 4 deletions.
diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs
@@ -149,7 +149,18 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
             Ok(quote_spanned! {sp=> (#term) })
         }
         RT::Path(_) => Ok(quote_spanned! {sp=> #term }),
-        RT::Range(_) => Err(EncodeError::Unsupported(term.span(), "Range".into())),
+        RT::Range(TermRange { from, limits, to }) => {
+            let from = match from {
+                None => None,
+                Some(from) => Some(encode_term(from)?),
+            };
+            let to = match to {
+                None => None,
+                Some(to) => Some(encode_term(to)?),
+            };
+            let limits = limits;
+            Ok(quote_spanned! {sp=>#from #limits #to})
+        }
         RT::Reference(TermReference { mutability, expr, .. }) => {
             let term = encode_term(expr)?;
             Ok(quote! {

diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs
@@ -1,3 +1,5 @@
+use ::std::ops::Range;
+
 use crate::{logic::ops::IndexLogic, *};
 
 #[cfg_attr(creusot, creusot::builtins = "seq.Seq.seq")]
@@ -165,3 +167,14 @@ impl<T> IndexLogic<Int> for Seq<T> {
         absurd
     }
 }
+
+impl<T> IndexLogic<Range<Int>> for Seq<T> {
+    type Item = Seq<T>;
+
+    #[ghost]
+    #[open]
+    #[why3::attr = "inline:trivial"]
+    fn index_logic(self, r: Range<Int>) -> Self::Item {
+        self.subsequence(r.start, r.end)
+    }
+}
diff --git a/creusot-contracts/src/std/deque.rs b/creusot-contracts/src/std/deque.rs
@@ -1,4 +1,5 @@
-use crate::{logic::IndexLogic, std::alloc::Allocator, *};
+use crate::{invariant::Invariant, logic::IndexLogic, std::alloc::Allocator, *};
+use ::std::collections::vec_deque::{IntoIter, Iter};
 pub use ::std::collections::VecDeque;
 
 impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
@@ -13,6 +14,131 @@ impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
     }
 }
 
+impl<'a, T> Invariant for Iter<'a, T> {}
+
+impl<T, A: Allocator> ShallowModel for IntoIter<T, A> {
+    type ShallowModelTy = Seq<T>;
+
+    #[open(self)]
+    #[ghost]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        absurd
+    }
+}
+
+impl<'a, T> ShallowModel for Iter<'a, T> {
+    // TODO : This seems wrong
+    type ShallowModelTy = &'a [T];
+
+    #[ghost]
+    #[open(self)]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        absurd
+    }
+}
+
+impl<'a, T> Iterator for Iter<'a, T> {
+    #[predicate]
+    #[open]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && (*self)@@ == Seq::EMPTY }
+    }
+
+    #[predicate]
+    #[open]
+    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
+        pearlite! {
+            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
+        }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(a.produces(Seq::EMPTY, a))]
+    fn produces_refl(a: 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, A: Allocator> Invariant for IntoIter<T, A> {}
+
+impl<T, A: Allocator> Iterator for IntoIter<T, A> {
+    #[predicate]
+    #[open]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@ == Seq::EMPTY }
+    }
+
+    #[predicate]
+    #[open]
+    fn produces(self, visited: Seq<T>, rhs: Self) -> bool {
+        pearlite! {
+            self@ == visited.concat(rhs@)
+        }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(a.produces(Seq::EMPTY, a))]
+    fn produces_refl(a: 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<T>, b: Self, bc: Seq<T>, c: Self) {}
+}
+
+impl<T, A: Allocator> IntoIterator for VecDeque<T, A> {
+    #[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<T, A: Allocator> IntoIterator for &VecDeque<T, A> {
+    #[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<T, A: Allocator> IntoIterator for &mut VecDeque<T, A> {
+//     #[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<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A> {
     type DeepModelTy = Seq<T::DeepModelTy>;
 

diff --git a/creusot-contracts/src/std/ops.rs b/creusot-contracts/src/std/ops.rs
@@ -247,12 +247,12 @@ extern_spec! {
 extern_spec! {
     mod std {
         mod ops {
-            trait IndexMut<Idx>  {
+            trait IndexMut<Idx> where Self : ?Sized  {
                 #[requires(false)]
                 fn index_mut(&mut self, _ix : Idx) -> &mut Self::Output;
             }
 
-            trait Index<Idx> {
+            trait Index<Idx> where Self : ?Sized {
                 #[requires(false)]
                 fn index(&self, _ix : Idx) -> &Self::Output;
             }

diff --git a/creusot-contracts/src/std/slice.rs b/creusot-contracts/src/std/slice.rs
@@ -231,6 +231,11 @@ impl<T> SliceIndex<[T]> for RangeToInclusive<usize> {
 
 extern_spec! {
     impl<T> [T] {
+        #[requires(self@.len() == src@.len())]
+        #[ensures((^self)@ == src@)]
+        fn copy_from_slice(&mut self, src: &[T])
+            where T : Copy;
+
         #[ensures(self@.len() == result@)]
         fn len(&self) -> usize;
 

diff --git a/pearlite-syn/tests/test_term.rs b/pearlite-syn/tests/test_term.rs
@@ -4,6 +4,121 @@ mod macros;
 use pearlite_syn::Term;
 use quote::quote;
 
+#[test]
+fn test_range() {
+    snapshot!(quote!(x[0..]) as Term, @r###"
+    TermIndex {
+        expr: TermPath {
+            inner: ExprPath {
+                attrs: [],
+                qself: None,
+                path: Path {
+                    leading_colon: None,
+                    segments: [
+                        PathSegment {
+                            ident: Ident(
+                                x,
+                            ),
+                            arguments: PathArguments::None,
+                        },
+                    ],
+                },
+            },
+        },
+        bracket_token: Bracket,
+        index: TermRange {
+            from: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 0,
+                    },
+                },
+            ),
+            limits: RangeLimits::HalfOpen(
+                DotDot,
+            ),
+            to: None,
+        },
+    }
+    "###);
+    snapshot!(quote!(x[0..5]) as Term, @r###"
+    TermIndex {
+        expr: TermPath {
+            inner: ExprPath {
+                attrs: [],
+                qself: None,
+                path: Path {
+                    leading_colon: None,
+                    segments: [
+                        PathSegment {
+                            ident: Ident(
+                                x,
+                            ),
+                            arguments: PathArguments::None,
+                        },
+                    ],
+                },
+            },
+        },
+        bracket_token: Bracket,
+        index: TermRange {
+            from: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 0,
+                    },
+                },
+            ),
+            limits: RangeLimits::HalfOpen(
+                DotDot,
+            ),
+            to: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 5,
+                    },
+                },
+            ),
+        },
+    }
+    "###);
+    snapshot!(quote!(x[..5]) as Term, @r###"
+    TermIndex {
+        expr: TermPath {
+            inner: ExprPath {
+                attrs: [],
+                qself: None,
+                path: Path {
+                    leading_colon: None,
+                    segments: [
+                        PathSegment {
+                            ident: Ident(
+                                x,
+                            ),
+                            arguments: PathArguments::None,
+                        },
+                    ],
+                },
+            },
+        },
+        bracket_token: Bracket,
+        index: TermRange {
+            from: None,
+            limits: RangeLimits::HalfOpen(
+                DotDot,
+            ),
+            to: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 5,
+                    },
+                },
+            ),
+        },
+    }
+    "###);
+}
+
 #[test]
 fn test_impl() {
     snapshot!(quote!(false ==> true) as Term, @r###"