1use super::super::prelude::*;
4
5use alloc::collections::vec_deque::Iter;
6use alloc::collections::vec_deque::VecDeque;
7use core::alloc::Allocator;
8use core::clone::Clone;
9use core::ops::Index;
10use core::option::Option;
11use core::option::Option::None;
12
13verus! {
14
15#[verifier::external_type_specification]
16#[verifier::external_body]
17#[verifier::accept_recursive_types(T)]
18#[verifier::reject_recursive_types(A)]
19pub struct ExVecDeque<T, A: Allocator>(VecDeque<T, A>);
20
21impl<T, A: Allocator> View for VecDeque<T, A> {
22 type V = Seq<T>;
23
24 uninterp spec fn view(&self) -> Seq<T>;
25}
26
27impl<T: DeepView, A: Allocator> DeepView for VecDeque<T, A> {
28 type V = Seq<T::V>;
29
30 open spec fn deep_view(&self) -> Seq<T::V> {
31 let v = self.view();
32 Seq::new(v.len(), |i: int| v[i].deep_view())
33 }
34}
35
36pub trait VecDequeAdditionalSpecFns<T>: View<V = Seq<T>> {
37 spec fn spec_index(&self, i: int) -> T
38 recommends
39 0 <= i < self.view().len(),
40 ;
41}
42
43impl<T, A: Allocator> VecDequeAdditionalSpecFns<T> for VecDeque<T, A> {
44 #[verifier::inline]
45 open spec fn spec_index(&self, i: int) -> T {
46 self.view().index(i)
47 }
48}
49
50pub uninterp spec fn spec_vec_dequeue_len<T, A: Allocator>(v: &VecDeque<T, A>) -> usize;
52
53pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &VecDeque<T, A>)
56 ensures
57 #[trigger] spec_vec_dequeue_len(v) == v@.len(),
58{
59 admit();
60}
61
62pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::index ](
63 v: &VecDeque<T, A>,
64 i: usize,
65) -> (result: &T)
66 requires
67 i < v.len(),
68 ensures
69 result == v.spec_index(i as int),
70;
71
72#[verifier::when_used_as_spec(spec_vec_dequeue_len)]
73pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::len ](v: &VecDeque<T, A>) -> (len:
74 usize)
75 ensures
76 len == spec_vec_dequeue_len(v),
77;
78
79pub assume_specification<T>[ VecDeque::<T>::new ]() -> (v: VecDeque<T>)
80 ensures
81 v@ == Seq::<T>::empty(),
82;
83
84pub assume_specification<T>[ VecDeque::<T>::with_capacity ](capacity: usize) -> (v: VecDeque<T>)
85 ensures
86 v@ == Seq::<T>::empty(),
87;
88
89pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::reserve ](
90 v: &mut VecDeque<T, A>,
91 additional: usize,
92)
93 ensures
94 v@ == old(v)@,
95;
96
97pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_back ](
98 v: &mut VecDeque<T, A>,
99 value: T,
100)
101 ensures
102 v@ == old(v)@.push(value),
103;
104
105pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_front ](
106 v: &mut VecDeque<T, A>,
107 value: T,
108)
109 ensures
110 v@ == seq![value] + old(v)@,
111;
112
113pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_back ](
114 v: &mut VecDeque<T, A>,
115) -> (value: Option<T>)
116 ensures
117 match value {
118 Some(x) => {
119 &&& old(v)@.len() > 0
120 &&& x == old(v)@[old(v)@.len() - 1]
121 &&& v@ == old(v)@.subrange(0, old(v)@.len() as int - 1)
122 },
123 None => {
124 &&& old(v)@.len() == 0
125 &&& v@ == old(v)@
126 },
127 },
128;
129
130pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_front ](
131 v: &mut VecDeque<T, A>,
132) -> (value: Option<T>)
133 ensures
134 match value {
135 Some(x) => {
136 &&& old(v)@.len() > 0
137 &&& x == old(v)@[0]
138 &&& v@ == old(v)@.subrange(1, old(v)@.len() as int)
139 },
140 None => {
141 &&& old(v)@.len() == 0
142 &&& v@ == old(v)@
143 },
144 },
145;
146
147pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::append ](
148 v: &mut VecDeque<T, A>,
149 other: &mut VecDeque<T, A>,
150)
151 ensures
152 v@ == old(v)@ + old(other)@,
153 other@ == Seq::<T>::empty(),
154;
155
156pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::insert ](
157 v: &mut VecDeque<T, A>,
158 i: usize,
159 element: T,
160)
161 requires
162 i <= old(v).len(),
163 ensures
164 v@ == old(v)@.insert(i as int, element),
165;
166
167pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::remove ](
168 v: &mut VecDeque<T, A>,
169 i: usize,
170) -> (element: Option<T>)
171 ensures
172 match element {
173 Some(x) => {
174 &&& i < old(v)@.len()
175 &&& x == old(v)@[i as int]
176 &&& v@ == old(v)@.remove(i as int)
177 },
178 None => {
179 &&& old(v)@.len() <= i
180 &&& v@ == old(v)@
181 },
182 },
183;
184
185pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::clear ](v: &mut VecDeque<T, A>)
186 ensures
187 v.view() == Seq::<T>::empty(),
188;
189
190pub assume_specification<T, A: Allocator + core::clone::Clone>[ VecDeque::<T, A>::split_off ](
191 v: &mut VecDeque<T, A>,
192 at: usize,
193) -> (return_value: VecDeque<T, A>)
194 requires
195 at <= old(v)@.len(),
196 ensures
197 v@ == old(v)@.subrange(0, at as int),
198 return_value@ == old(v)@.subrange(at as int, old(v)@.len() as int),
199;
200
201pub open spec fn vec_dequeue_clone_trigger<T, A: Allocator>(
202 v1: VecDeque<T, A>,
203 v2: VecDeque<T, A>,
204) -> bool {
205 true
206}
207
208pub assume_specification<T: Clone, A: Allocator + Clone>[ <VecDeque<T, A> as Clone>::clone ](
209 v: &VecDeque<T, A>,
210) -> (res: VecDeque<T, A>)
211 ensures
212 res.len() == v.len(),
213 forall|i| #![all_triggers] 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]),
214 vec_dequeue_clone_trigger(*v, res),
215 v@ =~= res@ ==> v@ == res@,
216;
217
218pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::truncate ](
219 v: &mut VecDeque<T, A>,
220 len: usize,
221)
222 ensures
223 len <= old(v).len() ==> v@ == old(v)@.subrange(0, len as int),
224 len > old(v).len() ==> v@ == old(v)@,
225;
226
227pub assume_specification<T: Clone, A: Allocator>[ VecDeque::<T, A>::resize ](
228 v: &mut VecDeque<T, A>,
229 len: usize,
230 value: T,
231)
232 ensures
233 len <= old(v).len() ==> v@ == old(v)@.subrange(0, len as int),
234 len > old(v).len() ==> {
235 &&& v@.len() == len
236 &&& v@.subrange(0, old(v).len() as int) == old(v)@
237 &&& forall|i| #![all_triggers] old(v).len() <= i < len ==> cloned::<T>(value, v@[i])
238 },
239;
240
241pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int)
242 requires
243 0 <= i < v.len(),
244 ensures
245 #[trigger] (decreases_to!(v => v[i])),
246{
247 admit();
248}
249
250#[verifier::external_type_specification]
253#[verifier::external_body]
254#[verifier::accept_recursive_types(T)]
255pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
256
257impl<'a, T: 'a> View for Iter<'a, T> {
258 type V = (int, Seq<T>);
259
260 uninterp spec fn view(self: &Iter<'a, T>) -> (int, Seq<T>);
261}
262
263pub assume_specification<'a, T>[ Iter::<'a, T>::next ](elements: &mut Iter<'a, T>) -> (r: Option<
264 &'a T,
265>)
266 ensures
267 ({
268 let (old_index, old_seq) = old(elements)@;
269 match r {
270 None => {
271 &&& elements@ == old(elements)@
272 &&& old_index >= old_seq.len()
273 },
274 Some(element) => {
275 let (new_index, new_seq) = elements@;
276 &&& 0 <= old_index < old_seq.len()
277 &&& new_seq == old_seq
278 &&& new_index == old_index + 1
279 &&& element == old_seq[old_index]
280 },
281 }
282 }),
283;
284
285pub struct IterGhostIterator<'a, T> {
286 pub pos: int,
287 pub elements: Seq<T>,
288 pub phantom: Option<&'a T>,
289}
290
291impl<'a, T> super::super::pervasive::ForLoopGhostIteratorNew for Iter<'a, T> {
292 type GhostIter = IterGhostIterator<'a, T>;
293
294 open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T> {
295 IterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
296 }
297}
298
299impl<'a, T: 'a> super::super::pervasive::ForLoopGhostIterator for IterGhostIterator<'a, T> {
300 type ExecIter = Iter<'a, T>;
301
302 type Item = T;
303
304 type Decrease = int;
305
306 open spec fn exec_invariant(&self, exec_iter: &Iter<'a, T>) -> bool {
307 &&& self.pos == exec_iter@.0
308 &&& self.elements == exec_iter@.1
309 }
310
311 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
312 init matches Some(init) ==> {
313 &&& init.pos == 0
314 &&& init.elements == self.elements
315 &&& 0 <= self.pos <= self.elements.len()
316 }
317 }
318
319 open spec fn ghost_ensures(&self) -> bool {
320 self.pos == self.elements.len()
321 }
322
323 open spec fn ghost_decrease(&self) -> Option<int> {
324 Some(self.elements.len() - self.pos)
325 }
326
327 open spec fn ghost_peek_next(&self) -> Option<T> {
328 if 0 <= self.pos < self.elements.len() {
329 Some(self.elements[self.pos])
330 } else {
331 None
332 }
333 }
334
335 open spec fn ghost_advance(&self, _exec_iter: &Iter<'a, T>) -> IterGhostIterator<'a, T> {
336 Self { pos: self.pos + 1, ..*self }
337 }
338}
339
340impl<'a, T> View for IterGhostIterator<'a, T> {
341 type V = Seq<T>;
342
343 open spec fn view(&self) -> Seq<T> {
344 self.elements.take(self.pos)
345 }
346}
347
348pub uninterp spec fn spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>) -> (r: Iter<'a, T>);
355
356pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>)
357 ensures
358 (#[trigger] spec_iter(v))@ == (0int, v@),
359{
360 admit();
361}
362
363#[verifier::when_used_as_spec(spec_iter)]
364pub assume_specification<'a, T, A: Allocator>[ VecDeque::<T, A>::iter ](
365 v: &'a VecDeque<T, A>,
366) -> (r: Iter<'a, T>)
367 ensures
368 r@ == (0int, v@),
369;
370
371pub broadcast group group_vec_dequeue_axioms {
372 axiom_spec_len,
373 axiom_vec_dequeue_index_decreases,
374 axiom_spec_iter,
375}
376
377}