Skip to content

Commit b36dedd

Browse files
xldenisxldenis
committed
Add IndexLogic instance for Range<Int>
1 parent 159a0a7 commit b36dedd

File tree

6 files changed

+274
-4
lines changed

6 files changed

+274
-4
lines changed

‎creusot-contracts-proc/src/pretyping.rs‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,18 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
149149
Ok(quote_spanned! {sp=> (#term) })
150150
}
151151
RT::Path(_) => Ok(quote_spanned! {sp=> #term }),
152-
RT::Range(_) => Err(EncodeError::Unsupported(term.span(), "Range".into())),
152+
RT::Range(TermRange { from, limits, to }) => {
153+
let from = match from {
154+
None => None,
155+
Some(from) => Some(encode_term(from)?),
156+
};
157+
let to = match to {
158+
None => None,
159+
Some(to) => Some(encode_term(to)?),
160+
};
161+
let limits = limits;
162+
Ok(quote_spanned! {sp=>#from #limits #to})
163+
}
153164
RT::Reference(TermReference { mutability, expr, .. }) => {
154165
let term = encode_term(expr)?;
155166
Ok(quote! {

‎creusot-contracts/src/logic/seq.rs‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
use ::std::ops::Range;
2+
13
use crate::{logic::ops::IndexLogic, *};
24

35
#[cfg_attr(creusot, creusot::builtins = "seq.Seq.seq")]
@@ -165,3 +167,14 @@ impl<T> IndexLogic<Int> for Seq<T> {
165167
absurd
166168
}
167169
}
170+
171+
impl<T> IndexLogic<Range<Int>> for Seq<T> {
172+
type Item = Seq<T>;
173+
174+
#[ghost]
175+
#[open]
176+
#[why3::attr = "inline:trivial"]
177+
fn index_logic(self, r: Range<Int>) -> Self::Item {
178+
self.subsequence(r.start, r.end)
179+
}
180+
}

‎creusot-contracts/src/std/deque.rs‎

Lines changed: 127 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
use crate::{logic::IndexLogic, std::alloc::Allocator, *};
1+
use crate::{invariant::Invariant, logic::IndexLogic, std::alloc::Allocator, *};
2+
use ::std::collections::vec_deque::{IntoIter, Iter};
23
pub use ::std::collections::VecDeque;
34

45
impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
@@ -13,6 +14,131 @@ impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
1314
}
1415
}
1516

17+
impl<'a, T> Invariant for Iter<'a, T> {}
18+
19+
impl<T, A: Allocator> ShallowModel for IntoIter<T, A> {
20+
type ShallowModelTy = Seq<T>;
21+
22+
#[open(self)]
23+
#[ghost]
24+
#[trusted]
25+
fn shallow_model(self) -> Self::ShallowModelTy {
26+
absurd
27+
}
28+
}
29+
30+
impl<'a, T> ShallowModel for Iter<'a, T> {
31+
// TODO : This seems wrong
32+
type ShallowModelTy = &'a [T];
33+
34+
#[ghost]
35+
#[open(self)]
36+
#[trusted]
37+
fn shallow_model(self) -> Self::ShallowModelTy {
38+
absurd
39+
}
40+
}
41+
42+
impl<'a, T> Iterator for Iter<'a, T> {
43+
#[predicate]
44+
#[open]
45+
fn completed(&mut self) -> bool {
46+
pearlite! { self.resolve() && (*self)@@ == Seq::EMPTY }
47+
}
48+
49+
#[predicate]
50+
#[open]
51+
fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
52+
pearlite! {
53+
self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
54+
}
55+
}
56+
57+
#[law]
58+
#[open]
59+
#[ensures(a.produces(Seq::EMPTY, a))]
60+
fn produces_refl(a: Self) {}
61+
62+
#[law]
63+
#[open]
64+
#[requires(a.produces(ab, b))]
65+
#[requires(b.produces(bc, c))]
66+
#[ensures(a.produces(ab.concat(bc), c))]
67+
fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
68+
}
69+
70+
impl<T, A: Allocator> Invariant for IntoIter<T, A> {}
71+
72+
impl<T, A: Allocator> Iterator for IntoIter<T, A> {
73+
#[predicate]
74+
#[open]
75+
fn completed(&mut self) -> bool {
76+
pearlite! { self.resolve() && self@ == Seq::EMPTY }
77+
}
78+
79+
#[predicate]
80+
#[open]
81+
fn produces(self, visited: Seq<T>, rhs: Self) -> bool {
82+
pearlite! {
83+
self@ == visited.concat(rhs@)
84+
}
85+
}
86+
87+
#[law]
88+
#[open]
89+
#[ensures(a.produces(Seq::EMPTY, a))]
90+
fn produces_refl(a: Self) {}
91+
92+
#[law]
93+
#[open]
94+
#[requires(a.produces(ab, b))]
95+
#[requires(b.produces(bc, c))]
96+
#[ensures(a.produces(ab.concat(bc), c))]
97+
fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {}
98+
}
99+
100+
impl<T, A: Allocator> IntoIterator for VecDeque<T, A> {
101+
#[predicate]
102+
#[open]
103+
fn into_iter_pre(self) -> bool {
104+
pearlite! { true }
105+
}
106+
107+
#[predicate]
108+
#[open]
109+
fn into_iter_post(self, res: Self::IntoIter) -> bool {
110+
pearlite! { self@ == res@ }
111+
}
112+
}
113+
114+
impl<T, A: Allocator> IntoIterator for &VecDeque<T, A> {
115+
#[predicate]
116+
#[open]
117+
fn into_iter_pre(self) -> bool {
118+
pearlite! { true }
119+
}
120+
121+
#[predicate]
122+
#[open]
123+
fn into_iter_post(self, res: Self::IntoIter) -> bool {
124+
pearlite! { self@ == res@@ }
125+
}
126+
}
127+
128+
// impl<T, A: Allocator> IntoIterator for &mut VecDeque<T, A> {
129+
// #[predicate]
130+
// #[open]
131+
// fn into_iter_pre(self) -> bool {
132+
// pearlite! { true }
133+
// }
134+
135+
// #[predicate]
136+
// #[open]
137+
// fn into_iter_post(self, res: Self::IntoIter) -> bool {
138+
// pearlite! { self@ == res@@ }
139+
// }
140+
// }
141+
16142
impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A> {
17143
type DeepModelTy = Seq<T::DeepModelTy>;
18144

‎creusot-contracts/src/std/ops.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -247,12 +247,12 @@ extern_spec! {
247247
extern_spec! {
248248
mod std {
249249
mod ops {
250-
trait IndexMut<Idx> {
250+
trait IndexMut<Idx> where Self : ?Sized {
251251
#[requires(false)]
252252
fn index_mut(&mut self, _ix : Idx) -> &mut Self::Output;
253253
}
254254

255-
trait Index<Idx> {
255+
trait Index<Idx> where Self : ?Sized {
256256
#[requires(false)]
257257
fn index(&self, _ix : Idx) -> &Self::Output;
258258
}

‎creusot-contracts/src/std/slice.rs‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -231,6 +231,11 @@ impl<T> SliceIndex<[T]> for RangeToInclusive<usize> {
231231

232232
extern_spec! {
233233
impl<T> [T] {
234+
#[requires(self@.len() == src@.len())]
235+
#[ensures((^self)@ == src@)]
236+
fn copy_from_slice(&mut self, src: &[T])
237+
where T : Copy;
238+
234239
#[ensures(self@.len() == result@)]
235240
fn len(&self) -> usize;
236241

‎pearlite-syn/tests/test_term.rs‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,121 @@ mod macros;
44
use pearlite_syn::Term;
55
use quote::quote;
66

7+
#[test]
8+
fn test_range() {
9+
snapshot!(quote!(x[0..]) as Term, @r###"
10+
TermIndex {
11+
expr: TermPath {
12+
inner: ExprPath {
13+
attrs: [],
14+
qself: None,
15+
path: Path {
16+
leading_colon: None,
17+
segments: [
18+
PathSegment {
19+
ident: Ident(
20+
x,
21+
),
22+
arguments: PathArguments::None,
23+
},
24+
],
25+
},
26+
},
27+
},
28+
bracket_token: Bracket,
29+
index: TermRange {
30+
from: Some(
31+
TermLit {
32+
lit: Lit::Int {
33+
token: 0,
34+
},
35+
},
36+
),
37+
limits: RangeLimits::HalfOpen(
38+
DotDot,
39+
),
40+
to: None,
41+
},
42+
}
43+
"###);
44+
snapshot!(quote!(x[0..5]) as Term, @r###"
45+
TermIndex {
46+
expr: TermPath {
47+
inner: ExprPath {
48+
attrs: [],
49+
qself: None,
50+
path: Path {
51+
leading_colon: None,
52+
segments: [
53+
PathSegment {
54+
ident: Ident(
55+
x,
56+
),
57+
arguments: PathArguments::None,
58+
},
59+
],
60+
},
61+
},
62+
},
63+
bracket_token: Bracket,
64+
index: TermRange {
65+
from: Some(
66+
TermLit {
67+
lit: Lit::Int {
68+
token: 0,
69+
},
70+
},
71+
),
72+
limits: RangeLimits::HalfOpen(
73+
DotDot,
74+
),
75+
to: Some(
76+
TermLit {
77+
lit: Lit::Int {
78+
token: 5,
79+
},
80+
},
81+
),
82+
},
83+
}
84+
"###);
85+
snapshot!(quote!(x[..5]) as Term, @r###"
86+
TermIndex {
87+
expr: TermPath {
88+
inner: ExprPath {
89+
attrs: [],
90+
qself: None,
91+
path: Path {
92+
leading_colon: None,
93+
segments: [
94+
PathSegment {
95+
ident: Ident(
96+
x,
97+
),
98+
arguments: PathArguments::None,
99+
},
100+
],
101+
},
102+
},
103+
},
104+
bracket_token: Bracket,
105+
index: TermRange {
106+
from: None,
107+
limits: RangeLimits::HalfOpen(
108+
DotDot,
109+
),
110+
to: Some(
111+
TermLit {
112+
lit: Lit::Int {
113+
token: 5,
114+
},
115+
},
116+
),
117+
},
118+
}
119+
"###);
120+
}
121+
7122
#[test]
8123
fn test_impl() {
9124
snapshot!(quote!(false ==> true) as Term, @r###"

0 commit comments

Comments
 (0)