creusot_contracts/std/
deque.rs

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

creusot_contracts/std/
deque.rs
