creusot_contracts/std/
deque.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{logic::ops::IndexLogic, *};
4#[cfg(feature = "nightly")]
5use ::std::alloc::Allocator;
6pub use ::std::collections::VecDeque;
7use ::std::{
8    collections::vec_deque::Iter,
9    ops::{Index, IndexMut},
10};
11
12#[cfg(feature = "nightly")]
13impl<T, A: Allocator> View for VecDeque<T, A> {
14    type ViewTy = Seq<T>;
15
16    #[trusted]
17    #[logic(opaque)]
18    #[ensures(result.len() <= usize::MAX@)]
19    fn view(self) -> Seq<T> {
20        dead
21    }
22}
23
24#[cfg(feature = "nightly")]
25impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A> {
26    type DeepModelTy = Seq<T::DeepModelTy>;
27
28    #[trusted]
29    #[logic(opaque)]
30    #[ensures(self.view().len() == result.len())]
31    #[ensures(forall<i> 0 <= i && i < self.view().len()
32              ==> result[i] == self[i].deep_model())]
33    fn deep_model(self) -> Self::DeepModelTy {
34        dead
35    }
36}
37
38#[cfg(feature = "nightly")]
39impl<T, A: Allocator> IndexLogic<Int> for VecDeque<T, A> {
40    type Item = T;
41
42    #[logic(open, inline)]
43    fn index_logic(self, ix: Int) -> Self::Item {
44        pearlite! { self@[ix] }
45    }
46}
47
48#[cfg(feature = "nightly")]
49impl<T, A: Allocator> IndexLogic<usize> for VecDeque<T, A> {
50    type Item = T;
51
52    #[logic(open, inline)]
53    fn index_logic(self, ix: usize) -> Self::Item {
54        pearlite! { self@[ix@] }
55    }
56}
57
58impl<T> Resolve for VecDeque<T> {
59    #[logic(open, prophetic, inline)]
60    fn resolve(self) -> bool {
61        pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }
62    }
63
64    #[trusted]
65    #[logic(prophetic)]
66    #[requires(structural_resolve(self))]
67    #[ensures(self.resolve())]
68    fn resolve_coherence(self) {}
69}
70
71extern_spec! {
72    mod std {
73        mod collections {
74            impl<T> VecDeque<T> {
75                #[check(ghost)]
76                #[ensures(result@.len() == 0)]
77                fn new() -> Self;
78
79                #[check(terminates)] // can OOM
80                #[ensures(result@.len() == 0)]
81                fn with_capacity(capacity: usize) -> Self;
82            }
83
84            impl<T, A: Allocator> VecDeque<T, A> {
85                #[check(ghost)]
86                #[ensures(result@ == self@.len())]
87                fn len(&self) -> usize;
88
89                #[check(ghost)]
90                #[ensures(result == (self@.len() == 0))]
91                fn is_empty(&self) -> bool;
92
93                #[check(ghost)]
94                #[ensures((^self)@.len() == 0)]
95                fn clear(&mut self);
96
97                #[check(ghost)]
98                #[ensures(match result {
99                    Some(t) =>
100                        (^self)@ == self@.subsequence(1, self@.len()) &&
101                        self@ == (^self)@.push_front(t),
102                    None => *self == ^self && self@.len() == 0
103                })]
104                fn pop_front(&mut self) -> Option<T>;
105
106                #[check(ghost)]
107                #[ensures(match result {
108                    Some(t) =>
109                        (^self)@ == self@.subsequence(0, self@.len() - 1) &&
110                        self@ == (^self)@.push_back(t),
111                    None => *self == ^self && self@.len() == 0
112                })]
113                fn pop_back(&mut self) -> Option<T>;
114
115                #[check(terminates)] // can OOM
116                #[ensures((^self)@.len() == self@.len() + 1)]
117                #[ensures((^self)@ == self@.push_front(value))]
118                fn push_front(&mut self, value: T);
119
120                #[check(terminates)] // can OOM
121                #[ensures((^self)@ == self@.push_back(value))]
122                fn push_back(&mut self, value: T);
123            }
124        }
125    }
126
127    impl<T, A: Allocator> Index<usize> for VecDeque<T, A> {
128        #[check(ghost)]
129        #[ensures(*result == self@[i@])]
130        fn index(&self, i: usize) -> &T;
131    }
132
133    impl<T, A: Allocator> IndexMut<usize> for VecDeque<T, A> {
134        #[check(ghost)]
135        #[ensures(*result == (*self)@[i@])]
136        #[ensures(^result == (^self)@[i@])]
137        fn index_mut(&mut self, i: usize) -> &mut T;
138    }
139
140    impl<'a, T, A: Allocator> IntoIterator for &'a VecDeque<T, A> {
141        #[check(ghost)]
142        #[ensures(self@ == result@@)]
143        fn into_iter(self) -> Iter<'a, T>;
144    }
145}
146
147impl<'a, T> View for Iter<'a, T> {
148    type ViewTy = &'a [T];
149
150    #[logic(opaque)]
151    fn view(self) -> Self::ViewTy {
152        dead
153    }
154}
155
156impl<'a, T> Iterator for Iter<'a, T> {
157    #[logic(open, prophetic)]
158    fn completed(&mut self) -> bool {
159        pearlite! { self.resolve() && (*self@)@ == Seq::empty() }
160    }
161
162    #[logic(open)]
163    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
164        pearlite! {
165            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
166        }
167    }
168
169    #[logic(open, law)]
170    #[ensures(self.produces(Seq::empty(), self))]
171    fn produces_refl(self) {}
172
173    #[logic(open, law)]
174    #[requires(a.produces(ab, b))]
175    #[requires(b.produces(bc, c))]
176    #[ensures(a.produces(ab.concat(bc), c))]
177    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
178}
179
180/// Dummy impls that don't use the unstable trait Allocator
181#[cfg(not(feature = "nightly"))]
182mod impls {
183    use super::*;
184    impl<T> View for VecDeque<T> {
185        type ViewTy = Seq<T>;
186    }
187    impl<T: DeepModel> DeepModel for VecDeque<T> {
188        type DeepModelTy = Seq<T::DeepModelTy>;
189    }
190    impl<T> IndexLogic<Int> for VecDeque<T> {
191        type Item = T;
192    }
193    impl<T> IndexLogic<usize> for VecDeque<T> {
194        type Item = T;
195    }
196}
creusot_contracts/std/deque.rs

creusot_contracts/std/
deque.rs
