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;
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) -> (result: &T)
73    ensures
74        result == v.spec_index(i as int),
75;
76
77#[verifier::when_used_as_spec(spec_vec_dequeue_len)]
78pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::len ](v: &VecDeque<T, A>) -> (len:
79    usize)
80    ensures
81        len == spec_vec_dequeue_len(v),
82;
83
84pub assume_specification<T>[ VecDeque::<T>::new ]() -> (v: VecDeque<T>)
85    ensures
86        v@ == Seq::<T>::empty(),
87;
88
89pub assume_specification<T>[ <VecDeque<T> as core::default::Default>::default ]() -> (v: VecDeque<
90    T,
91>)
92    ensures
93        v@ == Seq::<T>::empty(),
94;
95
96pub assume_specification<T>[ VecDeque::<T>::with_capacity ](capacity: usize) -> (v: VecDeque<T>)
97    ensures
98        v@ == Seq::<T>::empty(),
99;
100
101pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::reserve ](
102    v: &mut VecDeque<T, A>,
103    additional: usize,
104)
105    ensures
106        final(v)@ == old(v)@,
107;
108
109pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_back ](
110    v: &mut VecDeque<T, A>,
111    value: T,
112)
113    ensures
114        final(v)@ == old(v)@.push(value),
115;
116
117pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_front ](
118    v: &mut VecDeque<T, A>,
119    value: T,
120)
121    ensures
122        final(v)@ == seq![value] + old(v)@,
123;
124
125pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_back ](
126    v: &mut VecDeque<T, A>,
127) -> (value: Option<T>)
128    ensures
129        match value {
130            Some(x) => {
131                &&& old(v)@.len() > 0
132                &&& x == old(v)@[old(v)@.len() - 1]
133                &&& final(v)@ == old(v)@.subrange(0, old(v)@.len() as int - 1)
134            },
135            None => {
136                &&& old(v)@.len() == 0
137                &&& final(v)@ == old(v)@
138            },
139        },
140;
141
142pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_front ](
143    v: &mut VecDeque<T, A>,
144) -> (value: Option<T>)
145    ensures
146        match value {
147            Some(x) => {
148                &&& old(v)@.len() > 0
149                &&& x == old(v)@[0]
150                &&& final(v)@ == old(v)@.subrange(1, old(v)@.len() as int)
151            },
152            None => {
153                &&& old(v)@.len() == 0
154                &&& final(v)@ == old(v)@
155            },
156        },
157;
158
159pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::append ](
160    v: &mut VecDeque<T, A>,
161    other: &mut VecDeque<T, A>,
162)
163    ensures
164        final(v)@ == old(v)@ + old(other)@,
165        final(other)@ == Seq::<T>::empty(),
166;
167
168pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::insert ](
169    v: &mut VecDeque<T, A>,
170    i: usize,
171    element: T,
172)
173    requires
174        i <= old(v).len(),
175    ensures
176        final(v)@ == old(v)@.insert(i as int, element),
177;
178
179pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::remove ](
180    v: &mut VecDeque<T, A>,
181    i: usize,
182) -> (element: Option<T>)
183    ensures
184        match element {
185            Some(x) => {
186                &&& i < old(v)@.len()
187                &&& x == old(v)@[i as int]
188                &&& final(v)@ == old(v)@.remove(i as int)
189            },
190            None => {
191                &&& old(v)@.len() <= i
192                &&& final(v)@ == old(v)@
193            },
194        },
195;
196
197pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::clear ](v: &mut VecDeque<T, A>)
198    ensures
199        final(v).view() == Seq::<T>::empty(),
200;
201
202pub assume_specification<T, A: Allocator + core::clone::Clone>[ VecDeque::<T, A>::split_off ](
203    v: &mut VecDeque<T, A>,
204    at: usize,
205) -> (return_value: VecDeque<T, A>)
206    requires
207        at <= old(v)@.len(),
208    ensures
209        final(v)@ == old(v)@.subrange(0, at as int),
210        return_value@ == old(v)@.subrange(at as int, old(v)@.len() as int),
211;
212
213pub open spec fn vec_dequeue_clone_trigger<T, A: Allocator>(
214    v1: VecDeque<T, A>,
215    v2: VecDeque<T, A>,
216) -> bool {
217    true
218}
219
220pub assume_specification<T: Clone, A: Allocator + Clone>[ <VecDeque<T, A> as Clone>::clone ](
221    v: &VecDeque<T, A>,
222) -> (res: VecDeque<T, A>)
223    ensures
224        res.len() == v.len(),
225        forall|i| #![all_triggers] 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]),
226        vec_dequeue_clone_trigger(*v, res),
227        v@ =~= res@ ==> v@ == res@,
228;
229
230pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::truncate ](
231    v: &mut VecDeque<T, A>,
232    len: usize,
233)
234    ensures
235        len <= old(v).len() ==> final(v)@ == old(v)@.subrange(0, len as int),
236        len > old(v).len() ==> final(v)@ == old(v)@,
237;
238
239pub assume_specification<T: Clone, A: Allocator>[ VecDeque::<T, A>::resize ](
240    v: &mut VecDeque<T, A>,
241    len: usize,
242    value: T,
243)
244    ensures
245        len <= old(v).len() ==> final(v)@ == old(v)@.subrange(0, len as int),
246        len > old(v).len() ==> {
247            &&& final(v)@.len() == len
248            &&& final(v)@.subrange(0, old(v).len() as int) == old(v)@
249            &&& forall|i|
250                #![all_triggers]
251                old(v).len() <= i < len ==> cloned::<T>(value, final(v)@[i])
252        },
253;
254
255pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int)
256    requires
257        0 <= i < v.len(),
258    ensures
259        #[trigger] (decreases_to!(v => v[i])),
260{
261    admit();
262}
263
264// The `iter` method of a `VecDeque` returns an iterator of type `Iter`,
265// so we specify that type here.
266#[verifier::external_type_specification]
267#[verifier::external_body]
268#[verifier::accept_recursive_types(T)]
269pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
270
271// To allow reasoning about the "contents" of the VecDeque iterator, without using
272// a prophecy, we need a function that gives us the underlying sequence of the original vec.
273pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<&'a T>;
274
275impl<'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
276    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
277        true
278    }
279
280    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
281
282    uninterp spec fn will_return_none(&self) -> bool;
283
284    #[verifier::prophetic]
285    open spec fn initial_value_relation(&self, init: &Self) -> bool {
286        &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
287        &&& into_iter_elts(*self) == IteratorSpec::remaining(self)
288    }
289
290    uninterp spec fn decrease(&self) -> Option<nat>;
291
292    open spec fn peek(&self, index: int) -> Option<Self::Item> {
293        if 0 <= index < into_iter_elts(*self).len() {
294            Some(&into_iter_elts(*self)[index])
295        } else {
296            None
297        }
298    }
299}
300
301impl<'a, T: 'a> super::iter::DoubleEndedIteratorSpecImpl for Iter<'a, T> {
302    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
303        if 0 <= index < into_iter_elts(*self).len() {
304            Some(&into_iter_elts(*self)[into_iter_elts(*self).len() - index - 1])
305        } else {
306            None
307        }
308    }
309}
310
311// To allow reasoning about the ghost iterator when the executable
312// function `iter()` is invoked in a `for` loop header (e.g., in
313// `for x in it: v.iter() { ... }`), we need to specify the behavior of
314// the iterator in spec mode. To do that, we add
315// `#[verifier::when_used_as_spec(spec_iter)` to the specification for
316// the executable `iter` method and define that spec function here.
317pub uninterp spec fn spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>) -> (r: Iter<'a, T>);
318
319pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>)
320    ensures
321        #[trigger] spec_iter(v).remaining() == v@.as_ref(),
322{
323    admit();
324}
325
326#[verifier::when_used_as_spec(spec_iter)]
327pub assume_specification<'a, T, A: Allocator>[ VecDeque::<T, A>::iter ](
328    v: &'a VecDeque<T, A>,
329) -> (iter: Iter<'a, T>)
330    ensures
331        iter == spec_iter(v),
332        IteratorSpec::decrease(&iter) is Some,
333        IteratorSpec::initial_value_relation(&iter, &iter),
334;
335
336pub broadcast group group_vec_dequeue_axioms {
337    axiom_spec_len,
338    axiom_vec_dequeue_index_decreases,
339    axiom_spec_iter,
340}
341
342} // verus!
vstd/std_specs/vecdeque.rs

vstd/std_specs/
vecdeque.rs
