vstd/std_specs/
vec.rs

1use super::super::prelude::*;
2use verus_builtin::*;
3
4use super::super::slice::SliceIndexSpec;
5use super::core::IndexSpec;
6use alloc::collections::TryReserveError;
7use alloc::vec::{IntoIter, Vec};
8use core::alloc::Allocator;
9use core::clone::Clone;
10use core::marker::PhantomData;
11use core::ops::Index;
12use core::option::Option;
13use core::option::Option::None;
14use core::slice::SliceIndex;
15
16use verus as verus_;
17verus_! {
18
19#[verifier::external_type_specification]
20#[verifier::external_body]
21#[verifier::accept_recursive_types(T)]
22#[verifier::reject_recursive_types(A)]
23pub struct ExVec<T, A: Allocator>(Vec<T, A>);
24
25pub trait VecAdditionalSpecFns<T>: View<V = Seq<T>> {
26    spec fn spec_index(&self, i: int) -> T
27        recommends
28            0 <= i < self.view().len(),
29    ;
30}
31
32impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> {
33    #[verifier::inline]
34    open spec fn spec_index(&self, i: int) -> T {
35        self.view().index(i)
36    }
37}
38
39#[verifier::external_type_specification]
40#[verifier::external_body]
41pub struct ExTryReserveError(alloc::collections::TryReserveError);
42
43// We still have a special case for Vec::index on usize.
44// The general Vec::index case now goes through the Index trait,
45// but this special case is still here because it's more direct and efficient in its SMT encoding,
46// and Vec::index on usize is very common.
47//
48// So this is a bit of a hack, but we just manually redirect
49// `vec[i]` to this function here from rust_to_vir_expr.
50#[verifier::external_body]
51#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::vec::vec_index")]
52pub fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> (element: &T)
53    requires
54        i < vec.view().len(),
55    ensures
56        *element == vec.view().index(i as int),
57    no_unwind
58{
59    &vec[i]
60}
61
62/// This is a specification for the indexing operator `vec[i]` when it expands to the `IndexMut` trait
63#[doc(hidden)]
64#[verifier::ignore_outside_new_mut_ref_experiment]
65#[verifier::external_body]
66#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::vec::vec_index_mut")]
67pub fn vec_index_mut<T, A: Allocator>(vec: &mut Vec<T, A>, i: usize) -> (element: &mut T)
68    requires
69        i < vec.view().len(),
70    ensures
71        *element == old(vec)@.index(i as int),
72        final(vec)@ == old(vec)@.update(i as int, *final(element)),
73
74        *final(element) == final(vec).view().index(i as int),
75    no_unwind
76{
77    &mut vec[i]
78}
79
80////// Len (with autospec)
81pub uninterp spec fn spec_vec_len<T, A: Allocator>(v: &Vec<T, A>) -> usize;
82
83// This axiom is slightly better than defining spec_vec_len to just be `v@.len() as usize`
84// (the axiom also shows that v@.len() is in-bounds for usize)
85pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &Vec<T, A>)
86    ensures
87        #[trigger] spec_vec_len(v) == v@.len(),
88{
89    admit();
90}
91
92#[verifier::when_used_as_spec(spec_vec_len)]
93pub assume_specification<T, A: Allocator>[ Vec::<T, A>::len ](vec: &Vec<T, A>) -> (len: usize)
94    ensures
95        len == spec_vec_len(vec),
96    no_unwind
97;
98
99////// Other functions
100pub assume_specification<T>[ Vec::<T>::new ]() -> (v: Vec<T>)
101    ensures
102        v@ == Seq::<T>::empty(),
103;
104
105pub assume_specification<T>[ <Vec<T> as core::default::Default>::default ]() -> (v: Vec<T>)
106    ensures
107        v@ == Seq::<T>::empty(),
108;
109
110pub assume_specification<T, A: Allocator>[ Vec::<T, A>::new_in ](alloc: A) -> (v: Vec<T, A>)
111    ensures
112        v@ == Seq::<T>::empty(),
113;
114
115pub assume_specification<T>[ Vec::<T>::with_capacity ](capacity: usize) -> (v: Vec<T>)
116    ensures
117        v@ == Seq::<T>::empty(),
118;
119
120pub assume_specification<T, A: Allocator>[ Vec::<T, A>::with_capacity_in ](capacity: usize, alloc: A) -> (v: Vec<T, A>)
121    ensures
122        v@ == Seq::<T>::empty(),
123;
124
125pub assume_specification<T, A: Allocator>[ Vec::<T, A>::reserve ](
126    vec: &mut Vec<T, A>,
127    additional: usize,
128)
129    ensures
130        vec@ == old(vec)@,
131;
132
133pub assume_specification<T, A: Allocator>[ Vec::<T, A>::try_reserve ](
134    vec: &mut Vec<T, A>,
135    additional: usize,
136) -> (result: Result<(), TryReserveError>)
137    ensures
138        vec@ == old(vec)@,
139;
140
141pub assume_specification<T, A: Allocator>[ Vec::<T, A>::push ](vec: &mut Vec<T, A>, value: T)
142    ensures
143        vec@ == old(vec)@.push(value),
144;
145
146pub assume_specification<T, A: Allocator>[ Vec::<T, A>::pop ](vec: &mut Vec<T, A>) -> (value:
147    Option<T>)
148    ensures
149        old(vec)@.len() > 0 ==> value == Some(old(vec)@[old(vec)@.len() - 1]) && vec@ == old(
150            vec,
151        )@.subrange(0, old(vec)@.len() - 1),
152        old(vec)@.len() == 0 ==> value == None::<T> && vec@ == old(vec)@,
153;
154
155pub assume_specification<T, A: Allocator>[ Vec::<T, A>::append ](
156    vec: &mut Vec<T, A>,
157    other: &mut Vec<T, A>,
158)
159    ensures
160        vec@ == old(vec)@ + old(other)@,
161        other@ == Seq::<T>::empty(),
162;
163
164pub assume_specification<T: core::clone::Clone, A: Allocator>[ Vec::<T, A>::extend_from_slice ](
165    vec: &mut Vec<T, A>,
166    other: &[T],
167)
168    ensures
169        vec@.len() == old(vec)@.len() + other@.len(),
170        forall|i: int|
171            #![trigger vec@[i]]
172            0 <= i < vec@.len() ==> if i < old(vec)@.len() {
173                vec@[i] == old(vec)@[i]
174            } else {
175                cloned::<T>(other@[i - old(vec)@.len()], vec@[i])
176            },
177;
178
179impl<T: Sized, I: SliceIndex<[T]>, A: Allocator> super::core::IndexSpecImpl<I> for Vec<T, A> {
180    open spec fn index_req(&self, index: &I) -> bool {
181        forall|s: &[T]| #[trigger] s@ == self@ ==> index.index_req(s)
182    }
183}
184
185pub assume_specification<T, I: SliceIndex<[T]>, A: Allocator>[Vec::<T, A>::index](
186    vec: &Vec<T, A>,
187    i: I,
188) -> (r: &<Vec<T, A> as Index<I>>::Output)
189    ensures
190        exists|s: &[T]| #[trigger] s@ == vec@ && call_ensures(<I as SliceIndex<[T]>>::index, (i, s), r),
191;
192
193pub assume_specification<T, A: Allocator>[ Vec::<T, A>::swap_remove ](
194    vec: &mut Vec<T, A>,
195    i: usize,
196) -> (element: T)
197    requires
198        i < old(vec).len(),
199    ensures
200        element == old(vec)[i as int],
201        vec@ == old(vec)@.update(i as int, old(vec)@.last()).drop_last(),
202;
203
204pub assume_specification<T, A: Allocator>[ Vec::<T, A>::insert ](
205    vec: &mut Vec<T, A>,
206    i: usize,
207    element: T,
208)
209    requires
210        i <= old(vec).len(),
211    ensures
212        vec@ == old(vec)@.insert(i as int, element),
213;
214
215pub assume_specification<T, A: Allocator> [ <Vec<T, A>>::is_empty ](
216    v: &Vec<T, A>,
217) -> (res: bool)
218    ensures res <==> v@.len() == 0,
219;
220
221pub assume_specification<T, A: Allocator>[ Vec::<T, A>::remove ](
222    vec: &mut Vec<T, A>,
223    i: usize,
224) -> (element: T)
225    requires
226        i < old(vec).len(),
227    ensures
228        element == old(vec)[i as int],
229        vec@ == old(vec)@.remove(i as int),
230;
231
232pub assume_specification<T, A: Allocator>[ Vec::<T, A>::clear ](vec: &mut Vec<T, A>)
233    ensures
234        vec.view() == Seq::<T>::empty(),
235;
236
237pub assume_specification<T, A: Allocator>[ Vec::<T, A>::as_slice ](vec: &Vec<T, A>) -> (slice: &[T])
238    ensures
239        slice@ == vec@,
240;
241
242#[doc(hidden)]
243#[verifier::ignore_outside_new_mut_ref_experiment]
244pub assume_specification<T, A: Allocator>[ Vec::<T, A>::as_mut_slice ](vec: &mut Vec<T, A>) -> (slice: &mut [T])
245    ensures
246        slice@ == old(vec)@,
247        final(slice)@ == final(vec)@,
248;
249
250pub assume_specification<T, A: Allocator>[ <Vec<T, A> as core::ops::Deref>::deref ](
251    vec: &Vec<T, A>,
252) -> (slice: &[T])
253    ensures
254        slice@ == vec@,
255;
256
257pub assume_specification<T, A: Allocator + core::clone::Clone>[ Vec::<T, A>::split_off ](
258    vec: &mut Vec<T, A>,
259    at: usize,
260) -> (return_value: Vec<T, A>)
261    requires
262        at <= old(vec)@.len(),
263    ensures
264        vec@ == old(vec)@.subrange(0, at as int),
265        return_value@ == old(vec)@.subrange(at as int, old(vec)@.len() as int),
266;
267
268pub open spec fn vec_clone_trigger<T, A: Allocator>(v1: Vec<T, A>, v2: Vec<T, A>) -> bool {
269    true
270}
271
272pub assume_specification<T: Clone, A: Allocator + Clone>[ <Vec<T, A> as Clone>::clone ](
273    vec: &Vec<T, A>,
274) -> (res: Vec<T, A>)
275    ensures
276        res.len() == vec.len(),
277        forall|i| #![all_triggers] 0 <= i < vec.len() ==> cloned::<T>(vec[i], res[i]),
278        vec_clone_trigger(*vec, res),
279        vec@ =~= res@ ==> vec@ == res@,
280;
281
282pub broadcast proof fn vec_clone_deep_view_proof<T: DeepView, A: Allocator>(
283    v1: Vec<T, A>,
284    v2: Vec<T, A>,
285)
286    requires
287        #[trigger] vec_clone_trigger(v1, v2),
288        v1.deep_view() =~= v2.deep_view(),
289    ensures
290        v1.deep_view() == v2.deep_view(),
291{
292}
293
294pub assume_specification<T, A: Allocator>[ Vec::<T, A>::truncate ](vec: &mut Vec<T, A>, len: usize)
295    ensures
296        len <= old(vec).len() ==> vec@ == old(vec)@.subrange(0, len as int),
297        len > old(vec).len() ==> vec@ == old(vec)@,
298;
299
300pub assume_specification<T: Clone, A: Allocator>[ Vec::<T, A>::resize ](
301    vec: &mut Vec<T, A>,
302    len: usize,
303    value: T,
304)
305    ensures
306        len <= old(vec).len() ==> vec@ == old(vec)@.subrange(0, len as int),
307        len > old(vec).len() ==> {
308            &&& vec@.len() == len
309            &&& vec@.subrange(0, old(vec).len() as int) == old(vec)@
310            &&& forall|i| #![all_triggers] old(vec).len() <= i < len ==> cloned::<T>(value, vec@[i])
311        },
312;
313
314pub broadcast proof fn axiom_vec_index_decreases<A>(v: Vec<A>, i: int)
315    requires
316        0 <= i < v.len(),
317    ensures
318        #[trigger] (decreases_to!(v => v[i])),
319{
320    admit();
321}
322
323impl<T, A: Allocator> super::core::TrustedSpecSealed for Vec<T, A> {
324
325}
326
327impl<T, A: Allocator> super::core::IndexSetTrustedSpec<usize> for Vec<T, A> {
328    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
329        0 <= index < self.len()
330    }
331
332    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
333        new_container@ === self@.update(index as int, val)
334    }
335}
336
337pub assume_specification<T: PartialEq<U>, U, A1: Allocator, A2: Allocator>[ <Vec<T, A1> as PartialEq<Vec<U, A2>>>::eq ](
338    x: &Vec<T, A1>,
339    y: &Vec<U, A2>,
340) -> bool
341;
342
343impl<T: super::cmp::PartialEqSpec<U>, U, A1: Allocator, A2: Allocator> super::cmp::PartialEqSpecImpl<Vec<U, A2>> for Vec<T, A1> {
344    open spec fn obeys_eq_spec() -> bool {
345        T::obeys_eq_spec()
346    }
347
348    open spec fn eq_spec(&self, other: &Vec<U, A2>) -> bool {
349        &&& self.len() == other.len()
350        &&& forall|i: int| #![auto] 0 <= i < self.len() ==> self[i].eq_spec(&other[i])
351    }
352}
353
354// The `into_iter` method of a `Vec` returns an iterator of type `IntoIter`,
355// so we specify that type here.
356#[verifier::external_type_specification]
357#[verifier::external_body]
358#[verifier::accept_recursive_types(T)]
359#[verifier::reject_recursive_types(A)]
360pub struct ExIntoIter<T, A: Allocator>(IntoIter<T, A>);
361
362impl<T, A: Allocator> View for IntoIter<T, A> {
363    type V = (int, Seq<T>);
364
365    uninterp spec fn view(self: &IntoIter<T, A>) -> (int, Seq<T>);
366}
367
368pub assume_specification<T, A: Allocator>[ IntoIter::<T, A>::next ](
369    elements: &mut IntoIter<T, A>,
370) -> (r: Option<T>)
371    ensures
372        ({
373            let (old_index, old_seq) = old(elements)@;
374            match r {
375                None => {
376                    &&& elements@ == old(elements)@
377                    &&& old_index >= old_seq.len()
378                },
379                Some(element) => {
380                    let (new_index, new_seq) = elements@;
381                    &&& 0 <= old_index < old_seq.len()
382                    &&& new_seq == old_seq
383                    &&& new_index == old_index + 1
384                    &&& element == old_seq[old_index]
385                },
386            }
387        }),
388;
389
390pub struct IntoIterGhostIterator<T, A: Allocator> {
391    pub pos: int,
392    pub elements: Seq<T>,
393    pub _marker: PhantomData<A>,
394}
395
396impl<T, A: Allocator> super::super::pervasive::ForLoopGhostIteratorNew for IntoIter<T, A> {
397    type GhostIter = IntoIterGhostIterator<T, A>;
398
399    open spec fn ghost_iter(&self) -> IntoIterGhostIterator<T, A> {
400        IntoIterGhostIterator { pos: self@.0, elements: self@.1, _marker: PhantomData }
401    }
402}
403
404// This is used by `vec![x; n]`
405pub assume_specification<T: Clone>[ alloc::vec::from_elem ](elem: T, n: usize) -> (v: Vec<T>)
406    ensures
407        v.len() == n,
408        forall |i| 0 <= i < n ==> cloned(elem, #[trigger] v@[i]);
409
410impl<T, A: Allocator> super::super::pervasive::ForLoopGhostIterator for IntoIterGhostIterator<
411    T,
412    A,
413> {
414    type ExecIter = IntoIter<T, A>;
415
416    type Item = T;
417
418    type Decrease = int;
419
420    open spec fn exec_invariant(&self, exec_iter: &IntoIter<T, A>) -> bool {
421        &&& self.pos == exec_iter@.0
422        &&& self.elements == exec_iter@.1
423    }
424
425    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
426        init matches Some(init) ==> {
427            &&& init.pos == 0
428            &&& init.elements == self.elements
429            &&& 0 <= self.pos <= self.elements.len()
430        }
431    }
432
433    open spec fn ghost_ensures(&self) -> bool {
434        self.pos == self.elements.len()
435    }
436
437    open spec fn ghost_decrease(&self) -> Option<int> {
438        Some(self.elements.len() - self.pos)
439    }
440
441    open spec fn ghost_peek_next(&self) -> Option<T> {
442        if 0 <= self.pos < self.elements.len() {
443            Some(self.elements[self.pos])
444        } else {
445            None
446        }
447    }
448
449    open spec fn ghost_advance(&self, _exec_iter: &IntoIter<T, A>) -> IntoIterGhostIterator<T, A> {
450        Self { pos: self.pos + 1, ..*self }
451    }
452}
453
454impl<T, A: Allocator> View for IntoIterGhostIterator<T, A> {
455    type V = Seq<T>;
456
457    open spec fn view(&self) -> Seq<T> {
458        self.elements.take(self.pos)
459    }
460}
461
462// To allow reasoning about the ghost iterator when the executable
463// function `into_iter()` is invoked in a `for` loop header (e.g., in
464// `for x in it: v.into_iter() { ... }`), we need to specify the behavior of
465// the iterator in spec mode. To do that, we add
466// `#[verifier::when_used_as_spec(spec_into_iter)` to the specification for
467// the executable `into_iter` method and define that spec function here.
468pub uninterp spec fn spec_into_iter<T, A: Allocator>(v: Vec<T, A>) -> (iter: <Vec<
469    T,
470    A,
471> as core::iter::IntoIterator>::IntoIter);
472
473pub broadcast proof fn axiom_spec_into_iter<T, A: Allocator>(v: Vec<T, A>)
474    ensures
475        (#[trigger] spec_into_iter(v))@ == (0int, v@),
476{
477    admit();
478}
479
480#[verifier::when_used_as_spec(spec_into_iter)]
481pub assume_specification<T, A: Allocator>[ Vec::<T, A>::into_iter ](vec: Vec<T, A>) -> (iter: <Vec<
482    T,
483    A,
484> as core::iter::IntoIterator>::IntoIter)
485    ensures
486        iter@ == (0int, vec@),
487;
488
489pub broadcast proof fn lemma_vec_obeys_eq_spec<T: PartialEq>()
490    requires
491        super::super::laws_eq::obeys_eq::<T>(),
492    ensures
493        #[trigger] super::super::laws_eq::obeys_eq::<Vec<T>>(),
494{
495    broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
496    reveal(super::super::laws_eq::obeys_eq_spec_properties);
497}
498
499pub broadcast proof fn lemma_vec_obeys_view_eq<T: PartialEq + View>()
500    requires
501        super::super::laws_eq::obeys_concrete_eq::<T>(),
502    ensures
503        #[trigger] super::super::laws_eq::obeys_view_eq::<Vec<T>>(),
504{
505    use super::cmp::PartialEqSpec;
506    broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
507    reveal(super::super::laws_eq::obeys_eq_spec_properties);
508    reveal(super::super::laws_eq::obeys_concrete_eq);
509    reveal(super::super::laws_eq::obeys_view_eq);
510    assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x@ == y@);
511}
512
513pub broadcast proof fn lemma_vec_obeys_deep_eq<T: PartialEq + DeepView>()
514    requires
515        super::super::laws_eq::obeys_deep_eq::<T>(),
516    ensures
517        #[trigger] super::super::laws_eq::obeys_deep_eq::<Vec<T>>(),
518{
519    use super::cmp::PartialEqSpec;
520    broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
521    reveal(super::super::laws_eq::obeys_eq_spec_properties);
522    reveal(super::super::laws_eq::obeys_deep_eq);
523    assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x.deep_view() == y.deep_view());
524    assert forall|x: Vec<T>, y: Vec<T>| x.deep_view() == y.deep_view() implies x.eq_spec(&y) by {
525        assert(x.deep_view().len() == y.deep_view().len());
526        assert forall|i: int| #![auto] 0 <= i < x.len() implies x[i].eq_spec(&y[i]) by {
527            assert(x.deep_view()[i] == y.deep_view()[i]);
528        }
529    }
530}
531
532pub broadcast axiom fn axiom_vec_has_resolved<T>(vec: Vec<T>, i: int)
533    ensures
534        0 <= i < vec.len() ==> #[trigger] has_resolved::<Vec<T>>(vec) ==> has_resolved(
535            #[trigger] vec@[i],
536        ),
537;
538
539pub broadcast axiom fn axiom_vec_decreases_to_view<T>(v: Vec<T>)
540    ensures
541        #[trigger] (decreases_to!(v => v@));
542
543pub broadcast group group_vec_axioms {
544    axiom_spec_len,
545    axiom_vec_index_decreases,
546    vec_clone_deep_view_proof,
547    axiom_spec_into_iter,
548    axiom_vec_has_resolved,
549    axiom_vec_decreases_to_view,
550}
551
552} // verus!
vstd/std_specs/vec.rs

vstd/std_specs/
vec.rs
