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

vstd/std_specs/
vecdeque.rs
