From b36deddd749afbcca814bbb447eb6fa0a733140a Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Thu, 21 Sep 2023 16:10:01 +0200 Subject: [PATCH] Add IndexLogic instance for Range --- creusot-contracts-proc/src/pretyping.rs | 13 ++- creusot-contracts/src/logic/seq.rs | 13 +++ creusot-contracts/src/std/deque.rs | 128 +++++++++++++++++++++++- creusot-contracts/src/std/ops.rs | 4 +- creusot-contracts/src/std/slice.rs | 5 + pearlite-syn/tests/test_term.rs | 115 +++++++++++++++++++++ 6 files changed, 274 insertions(+), 4 deletions(-) diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs index 7a85f6c4aa..d61fce197d 100644 --- 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 { 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 index 2d60f8e206..49c7d0820f 100644 --- 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 IndexLogic for Seq { absurd } } + +impl IndexLogic> for Seq { + type Item = Seq; + + #[ghost] + #[open] + #[why3::attr = "inline:trivial"] + fn index_logic(self, r: Range) -> Self::Item { + self.subsequence(r.start, r.end) + } +} diff --git a/creusot-contracts/src/std/deque.rs b/creusot-contracts/src/std/deque.rs index 1f5ca787e1..e654ffb072 100644 --- 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 ShallowModel for VecDeque { @@ -13,6 +14,131 @@ impl ShallowModel for VecDeque { } } +impl<'a, T> Invariant for Iter<'a, T> {} + +impl ShallowModel for IntoIter { + type ShallowModelTy = Seq; + + #[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, 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, b: Self, bc: Seq, c: Self) {} +} + +impl Invariant for IntoIter {} + +impl Iterator for IntoIter { + #[predicate] + #[open] + fn completed(&mut self) -> bool { + pearlite! { self.resolve() && self@ == Seq::EMPTY } + } + + #[predicate] + #[open] + fn produces(self, visited: Seq, 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, b: Self, bc: Seq, c: Self) {} +} + +impl IntoIterator for VecDeque { + #[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 IntoIterator for &VecDeque { + #[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 IntoIterator for &mut VecDeque { +// #[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 DeepModel for VecDeque { type DeepModelTy = Seq; diff --git a/creusot-contracts/src/std/ops.rs b/creusot-contracts/src/std/ops.rs index f4769a50f2..ac01d404e7 100644 --- 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 { + trait IndexMut where Self : ?Sized { #[requires(false)] fn index_mut(&mut self, _ix : Idx) -> &mut Self::Output; } - trait Index { + trait Index 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 index 10f4995799..8830e30890 100644 --- a/creusot-contracts/src/std/slice.rs +++ b/creusot-contracts/src/std/slice.rs @@ -231,6 +231,11 @@ impl SliceIndex<[T]> for RangeToInclusive { extern_spec! { impl [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 index 3f5ff8d780..f4b24af01e 100644 --- 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###"