vstd/std_specs/
vecdeque.rs

1/// This code adds specifications for the standard-library type
2/// `std::collections::VecDeque`.
3use 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
50////// Len (with autospec)
51pub uninterp spec fn spec_vec_dequeue_len<T, A: Allocator>(v: &VecDeque<T, A>) -> usize;
52
53// This axiom is slightly better than defining spec_vec_dequeue_len to just be `v@.len() as usize`
54// (the axiom also shows that v@.len() is in-bounds for usize)
55pub 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> as core::default::Default>::default ]() -> (v: VecDeque<
85    T,
86>)
87    ensures
88        v@ == Seq::<T>::empty(),
89;
90
91pub assume_specification<T>[ VecDeque::<T>::with_capacity ](capacity: usize) -> (v: VecDeque<T>)
92    ensures
93        v@ == Seq::<T>::empty(),
94;
95
96pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::reserve ](
97    v: &mut VecDeque<T, A>,
98    additional: usize,
99)
100    ensures
101        v@ == old(v)@,
102;
103
104pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_back ](
105    v: &mut VecDeque<T, A>,
106    value: T,
107)
108    ensures
109        v@ == old(v)@.push(value),
110;
111
112pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_front ](
113    v: &mut VecDeque<T, A>,
114    value: T,
115)
116    ensures
117        v@ == seq![value] + old(v)@,
118;
119
120pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_back ](
121    v: &mut VecDeque<T, A>,
122) -> (value: Option<T>)
123    ensures
124        match value {
125            Some(x) => {
126                &&& old(v)@.len() > 0
127                &&& x == old(v)@[old(v)@.len() - 1]
128                &&& v@ == old(v)@.subrange(0, old(v)@.len() as int - 1)
129            },
130            None => {
131                &&& old(v)@.len() == 0
132                &&& v@ == old(v)@
133            },
134        },
135;
136
137pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_front ](
138    v: &mut VecDeque<T, A>,
139) -> (value: Option<T>)
140    ensures
141        match value {
142            Some(x) => {
143                &&& old(v)@.len() > 0
144                &&& x == old(v)@[0]
145                &&& v@ == old(v)@.subrange(1, old(v)@.len() as int)
146            },
147            None => {
148                &&& old(v)@.len() == 0
149                &&& v@ == old(v)@
150            },
151        },
152;
153
154pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::append ](
155    v: &mut VecDeque<T, A>,
156    other: &mut VecDeque<T, A>,
157)
158    ensures
159        v@ == old(v)@ + old(other)@,
160        other@ == Seq::<T>::empty(),
161;
162
163pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::insert ](
164    v: &mut VecDeque<T, A>,
165    i: usize,
166    element: T,
167)
168    requires
169        i <= old(v).len(),
170    ensures
171        v@ == old(v)@.insert(i as int, element),
172;
173
174pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::remove ](
175    v: &mut VecDeque<T, A>,
176    i: usize,
177) -> (element: Option<T>)
178    ensures
179        match element {
180            Some(x) => {
181                &&& i < old(v)@.len()
182                &&& x == old(v)@[i as int]
183                &&& v@ == old(v)@.remove(i as int)
184            },
185            None => {
186                &&& old(v)@.len() <= i
187                &&& v@ == old(v)@
188            },
189        },
190;
191
192pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::clear ](v: &mut VecDeque<T, A>)
193    ensures
194        v.view() == Seq::<T>::empty(),
195;
196
197pub assume_specification<T, A: Allocator + core::clone::Clone>[ VecDeque::<T, A>::split_off ](
198    v: &mut VecDeque<T, A>,
199    at: usize,
200) -> (return_value: VecDeque<T, A>)
201    requires
202        at <= old(v)@.len(),
203    ensures
204        v@ == old(v)@.subrange(0, at as int),
205        return_value@ == old(v)@.subrange(at as int, old(v)@.len() as int),
206;
207
208pub open spec fn vec_dequeue_clone_trigger<T, A: Allocator>(
209    v1: VecDeque<T, A>,
210    v2: VecDeque<T, A>,
211) -> bool {
212    true
213}
214
215pub assume_specification<T: Clone, A: Allocator + Clone>[ <VecDeque<T, A> as Clone>::clone ](
216    v: &VecDeque<T, A>,
217) -> (res: VecDeque<T, A>)
218    ensures
219        res.len() == v.len(),
220        forall|i| #![all_triggers] 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]),
221        vec_dequeue_clone_trigger(*v, res),
222        v@ =~= res@ ==> v@ == res@,
223;
224
225pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::truncate ](
226    v: &mut VecDeque<T, A>,
227    len: usize,
228)
229    ensures
230        len <= old(v).len() ==> v@ == old(v)@.subrange(0, len as int),
231        len > old(v).len() ==> v@ == old(v)@,
232;
233
234pub assume_specification<T: Clone, A: Allocator>[ VecDeque::<T, A>::resize ](
235    v: &mut VecDeque<T, A>,
236    len: usize,
237    value: T,
238)
239    ensures
240        len <= old(v).len() ==> v@ == old(v)@.subrange(0, len as int),
241        len > old(v).len() ==> {
242            &&& v@.len() == len
243            &&& v@.subrange(0, old(v).len() as int) == old(v)@
244            &&& forall|i| #![all_triggers] old(v).len() <= i < len ==> cloned::<T>(value, v@[i])
245        },
246;
247
248pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int)
249    requires
250        0 <= i < v.len(),
251    ensures
252        #[trigger] (decreases_to!(v => v[i])),
253{
254    admit();
255}
256
257// The `iter` method of a `VecDeque` returns an iterator of type `Iter`,
258// so we specify that type here.
259#[verifier::external_type_specification]
260#[verifier::external_body]
261#[verifier::accept_recursive_types(T)]
262pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
263
264impl<'a, T: 'a> View for Iter<'a, T> {
265    type V = (int, Seq<T>);
266
267    uninterp spec fn view(self: &Iter<'a, T>) -> (int, Seq<T>);
268}
269
270pub assume_specification<'a, T>[ Iter::<'a, T>::next ](elements: &mut Iter<'a, T>) -> (r: Option<
271    &'a T,
272>)
273    ensures
274        ({
275            let (old_index, old_seq) = old(elements)@;
276            match r {
277                None => {
278                    &&& elements@ == old(elements)@
279                    &&& old_index >= old_seq.len()
280                },
281                Some(element) => {
282                    let (new_index, new_seq) = elements@;
283                    &&& 0 <= old_index < old_seq.len()
284                    &&& new_seq == old_seq
285                    &&& new_index == old_index + 1
286                    &&& element == old_seq[old_index]
287                },
288            }
289        }),
290;
291
292pub struct IterGhostIterator<'a, T> {
293    pub pos: int,
294    pub elements: Seq<T>,
295    pub phantom: Option<&'a T>,
296}
297
298impl<'a, T> super::super::pervasive::ForLoopGhostIteratorNew for Iter<'a, T> {
299    type GhostIter = IterGhostIterator<'a, T>;
300
301    open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T> {
302        IterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
303    }
304}
305
306impl<'a, T: 'a> super::super::pervasive::ForLoopGhostIterator for IterGhostIterator<'a, T> {
307    type ExecIter = Iter<'a, T>;
308
309    type Item = T;
310
311    type Decrease = int;
312
313    open spec fn exec_invariant(&self, exec_iter: &Iter<'a, T>) -> bool {
314        &&& self.pos == exec_iter@.0
315        &&& self.elements == exec_iter@.1
316    }
317
318    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
319        init matches Some(init) ==> {
320            &&& init.pos == 0
321            &&& init.elements == self.elements
322            &&& 0 <= self.pos <= self.elements.len()
323        }
324    }
325
326    open spec fn ghost_ensures(&self) -> bool {
327        self.pos == self.elements.len()
328    }
329
330    open spec fn ghost_decrease(&self) -> Option<int> {
331        Some(self.elements.len() - self.pos)
332    }
333
334    open spec fn ghost_peek_next(&self) -> Option<T> {
335        if 0 <= self.pos < self.elements.len() {
336            Some(self.elements[self.pos])
337        } else {
338            None
339        }
340    }
341
342    open spec fn ghost_advance(&self, _exec_iter: &Iter<'a, T>) -> IterGhostIterator<'a, T> {
343        Self { pos: self.pos + 1, ..*self }
344    }
345}
346
347impl<'a, T> View for IterGhostIterator<'a, T> {
348    type V = Seq<T>;
349
350    open spec fn view(&self) -> Seq<T> {
351        self.elements.take(self.pos)
352    }
353}
354
355// To allow reasoning about the ghost iterator when the executable
356// function `iter()` is invoked in a `for` loop header (e.g., in
357// `for x in it: v.iter() { ... }`), we need to specify the behavior of
358// the iterator in spec mode. To do that, we add
359// `#[verifier::when_used_as_spec(spec_iter)` to the specification for
360// the executable `iter` method and define that spec function here.
361pub uninterp spec fn spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>) -> (r: Iter<'a, T>);
362
363pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>)
364    ensures
365        (#[trigger] spec_iter(v))@ == (0int, v@),
366{
367    admit();
368}
369
370#[verifier::when_used_as_spec(spec_iter)]
371pub assume_specification<'a, T, A: Allocator>[ VecDeque::<T, A>::iter ](
372    v: &'a VecDeque<T, A>,
373) -> (r: Iter<'a, T>)
374    ensures
375        r@ == (0int, v@),
376;
377
378pub broadcast group group_vec_dequeue_axioms {
379    axiom_spec_len,
380    axiom_vec_dequeue_index_decreases,
381    axiom_spec_iter,
382}
383
384} // verus!
vstd/std_specs/vecdeque.rs

vstd/std_specs/
vecdeque.rs
