vstd/std_specs/
vecdeque.rs

1/// This code adds specifications for the standard-library type
2/// `std::collections::VecDeque`.
3use super::super::prelude::*;
4use super::iter::IteratorSpec;
5
6use alloc::collections::vec_deque::Iter;
7use alloc::collections::vec_deque::VecDeque;
8use core::alloc::Allocator;
9use core::clone::Clone;
10use core::ops::{Index, IndexMut};
11use core::option::Option;
12use core::option::Option::None;
13
14use verus as verus_skip_verusfmt; // verusfmt doesn't handle s[..e] yet
15verus_skip_verusfmt! {
16
17#[verifier::external_type_specification]
18#[verifier::external_body]
19#[verifier::accept_recursive_types(T)]
20#[verifier::reject_recursive_types(A)]
21pub struct ExVecDeque<T, A: Allocator>(VecDeque<T, A>);
22
23impl<T, A: Allocator> View for VecDeque<T, A> {
24    type V = Seq<T>;
25
26    uninterp spec fn view(&self) -> Seq<T>;
27}
28
29impl<T: DeepView, A: Allocator> DeepView for VecDeque<T, A> {
30    type V = Seq<T::V>;
31
32    open spec fn deep_view(&self) -> Seq<T::V> {
33        let v = self.view();
34        Seq::new(v.len(), |i: int| v[i].deep_view())
35    }
36}
37
38pub trait VecDequeAdditionalSpecFns<T>: View<V = Seq<T>> {
39    spec fn spec_index(&self, i: int) -> T
40        recommends
41            0 <= i < self.view().len(),
42    ;
43}
44
45impl<T, A: Allocator> VecDequeAdditionalSpecFns<T> for VecDeque<T, A> {
46    #[verifier::inline]
47    open spec fn spec_index(&self, i: int) -> T {
48        self.view().index(i)
49    }
50}
51
52////// Len (with autospec)
53pub uninterp spec fn spec_vec_dequeue_len<T, A: Allocator>(v: &VecDeque<T, A>) -> usize;
54
55// This axiom is slightly better than defining spec_vec_dequeue_len to just be `v@.len() as usize`
56// (the axiom also shows that v@.len() is in-bounds for usize)
57pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &VecDeque<T, A>)
58    ensures
59        #[trigger] spec_vec_dequeue_len(v) == v@.len(),
60{
61    admit();
62}
63
64impl<T, A: Allocator> super::core::IndexSpecImpl<usize> for VecDeque<T, A> {
65    open spec fn index_req(&self, index: &usize) -> bool {
66        *index < self.len()
67    }
68}
69
70pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::index ](
71    v: &VecDeque<T, A>,
72    i: usize,
73) -> (output: &T)
74    ensures
75        output == v.spec_index(i as int),
76;
77
78pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::index_mut ](
79    v: &mut VecDeque<T, A>,
80    i: usize,
81) -> (output: &mut T)
82    ensures
83        *output == old(v).spec_index(i as int),
84        final(v)@ == old(v)@.update(i as int, *final(output)),
85;
86
87#[verifier::when_used_as_spec(spec_vec_dequeue_len)]
88pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::len ](v: &VecDeque<T, A>) -> (len:
89    usize)
90    ensures
91        len == spec_vec_dequeue_len(v),
92;
93
94pub assume_specification<T>[ VecDeque::<T>::new ]() -> (v: VecDeque<T>)
95    ensures
96        v@ == Seq::<T>::empty(),
97;
98
99pub assume_specification<T>[ <VecDeque<T> as core::default::Default>::default ]() -> (v: VecDeque<
100    T,
101>)
102    ensures
103        v@ == Seq::<T>::empty(),
104;
105
106pub assume_specification<T>[ VecDeque::<T>::with_capacity ](capacity: usize) -> (v: VecDeque<T>)
107    ensures
108        v@ == Seq::<T>::empty(),
109;
110
111pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::reserve ](
112    v: &mut VecDeque<T, A>,
113    additional: usize,
114)
115    ensures
116        final(v)@ == old(v)@,
117;
118
119pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_back ](
120    v: &mut VecDeque<T, A>,
121    value: T,
122)
123    ensures
124        final(v)@ == old(v)@.push(value),
125;
126
127pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_front ](
128    v: &mut VecDeque<T, A>,
129    value: T,
130)
131    ensures
132        final(v)@ == seq![value] + old(v)@,
133;
134
135pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_back ](
136    v: &mut VecDeque<T, A>,
137) -> (value: Option<T>)
138    ensures
139        match value {
140            Some(x) => {
141                &&& old(v)@.len() > 0
142                &&& x == old(v)@[old(v)@.len() - 1]
143                &&& final(v)@ == old(v)@[..old(v)@.len() - 1]
144            },
145            None => {
146                &&& old(v)@.len() == 0
147                &&& final(v)@ == old(v)@
148            },
149        },
150;
151
152pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_front ](
153    v: &mut VecDeque<T, A>,
154) -> (value: Option<T>)
155    ensures
156        match value {
157            Some(x) => {
158                &&& old(v)@.len() > 0
159                &&& x == old(v)@[0]
160                &&& final(v)@ == old(v)@[1..]
161            },
162            None => {
163                &&& old(v)@.len() == 0
164                &&& final(v)@ == old(v)@
165            },
166        },
167;
168
169pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::append ](
170    v: &mut VecDeque<T, A>,
171    other: &mut VecDeque<T, A>,
172)
173    ensures
174        final(v)@ == old(v)@ + old(other)@,
175        final(other)@ == Seq::<T>::empty(),
176;
177
178pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::insert ](
179    v: &mut VecDeque<T, A>,
180    i: usize,
181    element: T,
182)
183    requires
184        i <= old(v).len(),
185    ensures
186        final(v)@ == old(v)@.insert(i as int, element),
187;
188
189pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::remove ](
190    v: &mut VecDeque<T, A>,
191    i: usize,
192) -> (element: Option<T>)
193    ensures
194        match element {
195            Some(x) => {
196                &&& i < old(v)@.len()
197                &&& x == old(v)@[i as int]
198                &&& final(v)@ == old(v)@.remove(i as int)
199            },
200            None => {
201                &&& old(v)@.len() <= i
202                &&& final(v)@ == old(v)@
203            },
204        },
205;
206
207pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::clear ](v: &mut VecDeque<T, A>)
208    ensures
209        final(v).view() == Seq::<T>::empty(),
210;
211
212pub assume_specification<T, A: Allocator + core::clone::Clone>[ VecDeque::<T, A>::split_off ](
213    v: &mut VecDeque<T, A>,
214    at: usize,
215) -> (return_value: VecDeque<T, A>)
216    requires
217        at <= old(v)@.len(),
218    ensures
219        final(v)@ == old(v)@[..at],
220        return_value@ == old(v)@[at..],
221;
222
223pub open spec fn vec_dequeue_clone_trigger<T, A: Allocator>(
224    v1: VecDeque<T, A>,
225    v2: VecDeque<T, A>,
226) -> bool {
227    true
228}
229
230pub assume_specification<T: Clone, A: Allocator + Clone>[ <VecDeque<T, A> as Clone>::clone ](
231    v: &VecDeque<T, A>,
232) -> (res: VecDeque<T, A>)
233    ensures
234        res.len() == v.len(),
235        forall|i| #![all_triggers] 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]),
236        vec_dequeue_clone_trigger(*v, res),
237        v@ =~= res@ ==> v@ == res@,
238;
239
240pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::truncate ](
241    v: &mut VecDeque<T, A>,
242    len: usize,
243)
244    ensures
245        len <= old(v).len() ==> final(v)@ == old(v)@[..len],
246        len > old(v).len() ==> final(v)@ == old(v)@,
247;
248
249pub assume_specification<T: Clone, A: Allocator>[ VecDeque::<T, A>::resize ](
250    v: &mut VecDeque<T, A>,
251    len: usize,
252    value: T,
253)
254    ensures
255        len <= old(v).len() ==> final(v)@ == old(v)@[..len],
256        len > old(v).len() ==> {
257            &&& final(v)@.len() == len
258            &&& final(v)@[..old(v).len()] == old(v)@
259            &&& forall|i|
260                #![all_triggers]
261                old(v).len() <= i < len ==> cloned::<T>(value, final(v)@[i])
262        },
263;
264
265pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int)
266    requires
267        0 <= i < v.len(),
268    ensures
269        #[trigger] (decreases_to!(v => v[i])),
270{
271    admit();
272}
273
274// The `iter` method of a `VecDeque` returns an iterator of type `Iter`,
275// so we specify that type here.
276#[verifier::external_type_specification]
277#[verifier::external_body]
278#[verifier::accept_recursive_types(T)]
279pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
280
281// To allow reasoning about the "contents" of the VecDeque iterator, without using
282// a prophecy, we need a function that gives us the underlying sequence of the original vec.
283pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<&'a T>;
284
285impl<'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
286    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
287        true
288    }
289
290    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
291
292    uninterp spec fn will_return_none(&self) -> bool;
293
294    uninterp spec fn decrease(&self) -> Option<nat>;
295
296    open spec fn peek(&self, index: int) -> Option<Self::Item> {
297        if 0 <= index < into_iter_elts(*self).len() {
298            Some(&into_iter_elts(*self)[index])
299        } else {
300            None
301        }
302    }
303}
304
305impl<'a, T: 'a> super::iter::DoubleEndedIteratorSpecImpl for Iter<'a, T> {
306    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
307        if 0 <= index < into_iter_elts(*self).len() {
308            Some(&into_iter_elts(*self)[into_iter_elts(*self).len() - index - 1])
309        } else {
310            None
311        }
312    }
313}
314
315pub assume_specification<'a, T, A: Allocator>[ VecDeque::<T, A>::iter ](
316    v: &'a VecDeque<T, A>,
317) -> (iter: Iter<'a, T>)
318    ensures
319        IteratorSpec::remaining(&iter) == v@.as_ref(),
320        into_iter_elts(iter) == IteratorSpec::remaining(&iter),
321        IteratorSpec::decrease(&iter) is Some,
322;
323
324pub broadcast group group_vec_dequeue_axioms {
325    axiom_spec_len,
326    axiom_vec_dequeue_index_decreases,
327}
328
329} // verus!
vstd/std_specs/vecdeque.rs

vstd/std_specs/
vecdeque.rs
