creusot_std/std/
deque.rs

1#[cfg(feature = "nightly")]
2use crate::logic::ops::IndexLogic;
3use crate::prelude::*;
4#[cfg(creusot)]
5use crate::{invariant::inv, resolve::structural_resolve};
6
7#[cfg(feature = "nightly")]
8use core::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    mod std {
87        mod collections {
88            impl<T> VecDeque<T> {
89                #[check(ghost)]
90                #[ensures(result@.len() == 0)]
91                fn new() -> Self;
92
93                #[check(terminates)] // can OOM
94                #[ensures(result@.len() == 0)]
95                fn with_capacity(capacity: usize) -> Self;
96            }
97
98            impl<T, A: Allocator> VecDeque<T, A> {
99                #[check(ghost)]
100                #[ensures(result@ == self@.len())]
101                fn len(&self) -> usize;
102
103                #[check(ghost)]
104                #[ensures(result == (self@.len() == 0))]
105                fn is_empty(&self) -> bool;
106
107                #[check(ghost)]
108                #[ensures((^self)@.len() == 0)]
109                fn clear(&mut self);
110
111                #[check(ghost)]
112                #[ensures(match result {
113                    Some(t) =>
114                        (^self)@ == self@.subsequence(1, self@.len()) &&
115                        self@ == (^self)@.push_front(t),
116                    None => *self == ^self && self@.len() == 0
117                })]
118                fn pop_front(&mut self) -> Option<T>;
119
120                #[check(ghost)]
121                #[ensures(match result {
122                    Some(t) =>
123                        (^self)@ == self@.subsequence(0, self@.len() - 1) &&
124                        self@ == (^self)@.push_back(t),
125                    None => *self == ^self && self@.len() == 0
126                })]
127                fn pop_back(&mut self) -> Option<T>;
128
129                #[check(terminates)] // can OOM
130                #[ensures((^self)@.len() == self@.len() + 1)]
131                #[ensures((^self)@ == self@.push_front(value))]
132                fn push_front(&mut self, value: T);
133
134                #[check(terminates)] // can OOM
135                #[ensures((^self)@ == self@.push_back(value))]
136                fn push_back(&mut self, value: T);
137            }
138        }
139    }
140
141    impl<T, A: Allocator> Index<usize> for VecDeque<T, A> {
142        #[check(ghost)]
143        #[ensures(*result == self@[i@])]
144        fn index(&self, i: usize) -> &T;
145    }
146
147    impl<T, A: Allocator> IndexMut<usize> for VecDeque<T, A> {
148        #[check(ghost)]
149        #[ensures(*result == (*self)@[i@])]
150        #[ensures(^result == (^self)@[i@])]
151        fn index_mut(&mut self, i: usize) -> &mut T;
152    }
153
154    impl<'a, T, A: Allocator> IntoIterator for &'a VecDeque<T, A> {
155        #[check(ghost)]
156        #[ensures(self@ == result@@)]
157        fn into_iter(self) -> Iter<'a, T>;
158    }
159}
160
161impl<'a, T> View for Iter<'a, T> {
162    type ViewTy = &'a [T];
163
164    #[logic(opaque)]
165    fn view(self) -> Self::ViewTy {
166        dead
167    }
168}
169
170impl<'a, T> IteratorSpec for Iter<'a, T> {
171    #[logic(open, prophetic)]
172    fn completed(&mut self) -> bool {
173        pearlite! { resolve(self) && (*self@)@ == Seq::empty() }
174    }
175
176    #[logic(open)]
177    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
178        pearlite! {
179            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
180        }
181    }
182
183    #[logic(open, law)]
184    #[ensures(self.produces(Seq::empty(), self))]
185    fn produces_refl(self) {}
186
187    #[logic(open, 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}
193
194/// Dummy impls that don't use the unstable trait Allocator
195#[cfg(not(feature = "nightly"))]
196mod impls {
197    use crate::{logic::ops::IndexLogic, prelude::*};
198    use std::collections::VecDeque;
199
200    impl<T> Resolve for VecDeque<T> {}
201    impl<T> Invariant for VecDeque<T> {}
202    impl<T> View for VecDeque<T> {
203        type ViewTy = Seq<T>;
204    }
205    impl<T: DeepModel> DeepModel for VecDeque<T> {
206        type DeepModelTy = Seq<T::DeepModelTy>;
207    }
208    impl<T> IndexLogic<Int> for VecDeque<T> {
209        type Item = T;
210    }
211    impl<T> IndexLogic<usize> for VecDeque<T> {
212        type Item = T;
213    }
214}
creusot_std/std/deque.rs

creusot_std/std/
deque.rs
