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

vstd/std_specs/
vecdeque.rs
