creusot_std/std/
deque.rs

1#[cfg(feature = "nightly")]
2use crate::logic::ops::IndexLogic;
3#[cfg(creusot)]
4use crate::{invariant::inv, resolve::structural_resolve};
5use crate::{prelude::*, std::iter::ExactSizeIteratorSpec};
6
7#[cfg(feature = "nightly")]
8use std::alloc::Allocator;
9#[cfg(feature = "nightly")]
10use std::collections::VecDeque;
11use std::collections::vec_deque::Iter;
12#[cfg(creusot)]
13use std::ops::{Index, IndexMut};
14
15#[cfg(feature = "nightly")]
16impl<T, A: Allocator> View for VecDeque<T, A> {
17    type ViewTy = Seq<T>;
18
19    #[trusted]
20    #[logic(opaque)]
21    #[ensures(result.len() <= usize::MAX@)]
22    fn view(self) -> Seq<T> {
23        dead
24    }
25}
26
27#[cfg(feature = "nightly")]
28impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A> {
29    type DeepModelTy = Seq<T::DeepModelTy>;
30
31    #[trusted]
32    #[logic(opaque)]
33    #[ensures(self.view().len() == result.len())]
34    #[ensures(forall<i> 0 <= i && i < self.view().len()
35              ==> result[i] == self[i].deep_model())]
36    fn deep_model(self) -> Self::DeepModelTy {
37        dead
38    }
39}
40
41#[cfg(feature = "nightly")]
42impl<T, A: Allocator> IndexLogic<Int> for VecDeque<T, A> {
43    type Item = T;
44
45    #[logic(open, inline)]
46    fn index_logic(self, ix: Int) -> Self::Item {
47        pearlite! { self@[ix] }
48    }
49}
50
51#[cfg(feature = "nightly")]
52impl<T, A: Allocator> IndexLogic<usize> for VecDeque<T, A> {
53    type Item = T;
54
55    #[logic(open, inline)]
56    fn index_logic(self, ix: usize) -> Self::Item {
57        pearlite! { self@[ix@] }
58    }
59}
60
61#[cfg(feature = "nightly")]
62impl<T, A: Allocator> Resolve for VecDeque<T, A> {
63    #[logic(open, prophetic, inline)]
64    #[creusot::trusted_trivial_if_param_trivial]
65    fn resolve(self) -> bool {
66        pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }
67    }
68
69    #[trusted]
70    #[logic(prophetic)]
71    #[requires(structural_resolve(self))]
72    #[ensures(self.resolve())]
73    fn resolve_coherence(self) {}
74}
75
76#[cfg(feature = "nightly")]
77impl<T, A: Allocator> Invariant for VecDeque<T, A> {
78    #[logic(open, prophetic)]
79    #[creusot::trusted_trivial_if_param_trivial]
80    fn invariant(self) -> bool {
81        pearlite! { inv(self@) }
82    }
83}
84
85extern_spec! {
86    impl<T> VecDeque<T> {
87        #[check(ghost)]
88        #[ensures(result@.len() == 0)]
89        fn new() -> Self;
90
91        #[check(terminates)] // can OOM
92        #[ensures(result@.len() == 0)]
93        fn with_capacity(capacity: usize) -> Self;
94    }
95
96    impl<T, A: Allocator> VecDeque<T, A> {
97        #[check(ghost)]
98        #[ensures(result@ == self@.len())]
99        fn len(&self) -> usize;
100
101        #[check(ghost)]
102        #[ensures(result == (self@.len() == 0))]
103        fn is_empty(&self) -> bool;
104
105        #[check(ghost)]
106        #[ensures((^self)@.len() == 0)]
107        fn clear(&mut self);
108
109        #[check(ghost)]
110        #[ensures(match result {
111            Some(t) =>
112                (^self)@ == self@.subsequence(1, self@.len()) &&
113                self@ == (^self)@.cons(t),
114            None => *self == ^self && self@.len() == 0
115        })]
116        fn pop_front(&mut self) -> Option<T>;
117
118        #[check(ghost)]
119        #[ensures(match result {
120            Some(t) =>
121                (^self)@ == self@.subsequence(0, self@.len() - 1) &&
122                self@ == (^self)@.snoc(t),
123            None => *self == ^self && self@.len() == 0
124        })]
125        fn pop_back(&mut self) -> Option<T>;
126
127        #[check(terminates)] // can OOM
128        #[ensures((^self)@.len() == self@.len() + 1)]
129        #[ensures((^self)@ == self@.cons(value))]
130        fn push_front(&mut self, value: T);
131
132        #[check(terminates)] // can OOM
133        #[ensures((^self)@ == self@.snoc(value))]
134        fn push_back(&mut self, value: T);
135    }
136
137    impl<T, A: Allocator> Index<usize> for VecDeque<T, A> {
138        #[check(ghost)]
139        #[ensures(*result == self@[i@])]
140        fn index(&self, i: usize) -> &T;
141    }
142
143    impl<T, A: Allocator> IndexMut<usize> for VecDeque<T, A> {
144        #[check(ghost)]
145        #[ensures(*result == (*self)@[i@])]
146        #[ensures(^result == (^self)@[i@])]
147        #[ensures((^self)@.len() == (*self)@.len())]
148        #[ensures(forall<j> 0 <= j && j < (*self)@.len() && j != i@ ==> (^self)@[j] == (*self)@[j])]
149        fn index_mut(&mut self, i: usize) -> &mut T;
150    }
151
152    impl<'a, T, A: Allocator> IntoIterator for &'a VecDeque<T, A> {
153        #[check(ghost)]
154        #[ensures(self@ == result@.to_owned_seq())]
155        fn into_iter(self) -> Iter<'a, T>;
156    }
157}
158
159impl<'a, T> View for Iter<'a, T> {
160    type ViewTy = Seq<&'a T>;
161
162    #[logic(opaque)]
163    fn view(self) -> Self::ViewTy {
164        dead
165    }
166}
167
168impl<'a, T> IteratorSpec for Iter<'a, T> {
169    #[logic(open, prophetic)]
170    fn completed(&mut self) -> bool {
171        pearlite! { resolve(self) && self@ == Seq::empty() }
172    }
173
174    #[logic(open)]
175    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
176        pearlite! {
177            self@ == visited.concat(tl@)
178        }
179    }
180
181    #[logic(law)]
182    #[ensures(self.produces(Seq::empty(), self))]
183    fn produces_refl(self) {
184        let _ = Seq::<Self::Item>::concat_empty;
185    }
186
187    #[logic(law)]
188    #[requires(a.produces(ab, b))]
189    #[requires(b.produces(bc, c))]
190    #[ensures(a.produces(ab.concat(bc), c))]
191    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
192        let _ = Seq::<Self::Item>::concat_assoc;
193    }
194}
195
196extern_spec! {
197    impl<'a, T> Iterator for Iter<'a, T> {
198        #[ensures(result.0@ == self@.len())]
199        #[ensures(result.1 == Some(result.0))]
200        fn size_hint(&self) -> (usize, Option<usize>);
201    }
202}
203
204impl<'a, T> ExactSizeIteratorSpec for Iter<'a, T> {
205    #[logic(law)]
206    #[requires(Self::size_hint.postcondition((self,), r))]
207    #[ensures(r.1 == Some(r.0))]
208    #[allow(unused_variables)]
209    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
210}
211
212impl<'a, T> DoubleEndedIteratorSpec for Iter<'a, T> {
213    #[logic(open)]
214    fn produces_back(self, visited: Seq<Self::Item>, tl: Self) -> bool {
215        pearlite! {
216          self@ == tl@.concat(visited.reverse())
217        }
218    }
219
220    #[logic(open, prophetic)]
221    fn completed_back(&mut self) -> bool {
222        self.completed()
223    }
224
225    #[logic(law)]
226    #[ensures(self.produces_back(Seq::empty(), self))]
227    fn produces_back_refl(self) {
228        let _ = Seq::<Self::Item>::reverse_empty();
229        let _ = Seq::<Self::Item>::concat_empty;
230    }
231
232    #[logic(law)]
233    #[requires(a.produces_back(ab, b))]
234    #[requires(b.produces_back(bc, c))]
235    #[ensures(a.produces_back(ab.concat(bc), c))]
236    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
237        let _ = ab.reverse_concat(bc);
238        let _ = Seq::<Self::Item>::concat_assoc;
239    }
240
241    #[logic(law)]
242    #[requires(Self::size_hint.postcondition((self,), r))]
243    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
244        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
245    #[ensures(match r.1 {
246        Some(r) => {
247            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
248        }
249        None => true
250    })]
251    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
252}
253
254/// Dummy impls that don't use the unstable trait Allocator
255#[cfg(not(feature = "nightly"))]
256mod impls {
257    use crate::{logic::ops::IndexLogic, prelude::*};
258    use std::collections::VecDeque;
259
260    impl<T> Resolve for VecDeque<T> {}
261    impl<T> Invariant for VecDeque<T> {}
262    impl<T> View for VecDeque<T> {
263        type ViewTy = Seq<T>;
264    }
265    impl<T: DeepModel> DeepModel for VecDeque<T> {
266        type DeepModelTy = Seq<T::DeepModelTy>;
267    }
268    impl<T> IndexLogic<Int> for VecDeque<T> {
269        type Item = T;
270    }
271    impl<T> IndexLogic<usize> for VecDeque<T> {
272        type Item = T;
273    }
274}
creusot_std/std/deque.rs

creusot_std/std/
deque.rs
