vstd/std_specs/
vec.rs

1use super::super::prelude::*;
2use super::iter::{FromIteratorSpecImpl, IteratorSpec};
3use verus_builtin::*;
4
5use super::super::slice::SliceIndexSpec;
6use super::core::IndexSpec;
7use alloc::collections::TryReserveError;
8use alloc::vec::{IntoIter, Vec};
9use core::alloc::Allocator;
10use core::clone::Clone;
11use core::marker::PhantomData;
12use core::ops::Index;
13use core::option::Option;
14use core::option::Option::None;
15use core::slice::SliceIndex;
16
17use verus as verus_;
18verus_! {
19
20#[verifier::external_type_specification]
21#[verifier::external_body]
22#[verifier::accept_recursive_types(T)]
23#[verifier::reject_recursive_types(A)]
24pub struct ExVec<T, A: Allocator>(Vec<T, A>);
25
26pub trait VecAdditionalSpecFns<T>: View<V = Seq<T>> {
27    spec fn spec_index(&self, i: int) -> T
28        recommends
29            0 <= i < self.view().len(),
30    ;
31}
32
33impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> {
34    #[verifier::inline]
35    open spec fn spec_index(&self, i: int) -> T {
36        self.view().index(i)
37    }
38}
39
40#[verifier::external_type_specification]
41#[verifier::external_body]
42pub struct ExTryReserveError(alloc::collections::TryReserveError);
43
44// We still have a special case for Vec::index on usize.
45// The general Vec::index case now goes through the Index trait,
46// but this special case is still here because it's more direct and efficient in its SMT encoding,
47// and Vec::index on usize is very common.
48//
49// So this is a bit of a hack, but we just manually redirect
50// `vec[i]` to this function here from rust_to_vir_expr.
51#[verifier::external_body]
52#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::vec::vec_index")]
53pub fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> (element: &T)
54    requires
55        i < vec.view().len(),
56    ensures
57        *element == vec.view().index(i as int),
58    no_unwind
59{
60    &vec[i]
61}
62
63/// This is a specification for the indexing operator `vec[i]` when it expands to the `IndexMut` trait
64#[doc(hidden)]
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        final(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        final(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        final(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])
150            && final(vec)@ == old(vec)@.subrange(0, old(vec)@.len() - 1),
151        old(vec)@.len() == 0 ==> value == None::<T> && final(vec)@ == old(vec)@,
152;
153
154pub assume_specification<T, A: Allocator>[ Vec::<T, A>::append ](
155    vec: &mut Vec<T, A>,
156    other: &mut Vec<T, A>,
157)
158    ensures
159        final(vec)@ == old(vec)@ + old(other)@,
160        final(other)@ == Seq::<T>::empty(),
161;
162
163pub assume_specification<T: core::clone::Clone, A: Allocator>[ Vec::<T, A>::extend_from_slice ](
164    vec: &mut Vec<T, A>,
165    other: &[T],
166)
167    ensures
168        final(vec)@.len() == old(vec)@.len() + other@.len(),
169        forall|i: int|
170            #![trigger final(vec)@[i]]
171            0 <= i < final(vec)@.len() ==> if i < old(vec)@.len() {
172                final(vec)@[i] == old(vec)@[i]
173            } else {
174                cloned::<T>(other@[i - old(vec)@.len()], final(vec)@[i])
175            },
176;
177
178impl<T: Sized, I: SliceIndex<[T]>, A: Allocator> super::core::IndexSpecImpl<I> for Vec<T, A> {
179    open spec fn index_req(&self, index: &I) -> bool {
180        forall|s: &[T]| #[trigger] s@ == self@ ==> index.index_req(s)
181    }
182}
183
184pub assume_specification<T, I: SliceIndex<[T]>, A: Allocator>[Vec::<T, A>::index](
185    vec: &Vec<T, A>,
186    i: I,
187) -> (r: &<Vec<T, A> as Index<I>>::Output)
188    ensures
189        exists|s: &[T]| #[trigger] s@ == vec@ && call_ensures(<I as SliceIndex<[T]>>::index, (i, s), r),
190;
191
192pub assume_specification<T, A: Allocator>[ Vec::<T, A>::swap_remove ](
193    vec: &mut Vec<T, A>,
194    i: usize,
195) -> (element: T)
196    requires
197        i < old(vec).len(),
198    ensures
199        element == old(vec)[i as int],
200        final(vec)@ == old(vec)@.update(i as int, old(vec)@.last()).drop_last(),
201;
202
203pub assume_specification<T, A: Allocator>[ Vec::<T, A>::insert ](
204    vec: &mut Vec<T, A>,
205    i: usize,
206    element: T,
207)
208    requires
209        i <= old(vec).len(),
210    ensures
211        final(vec)@ == old(vec)@.insert(i as int, element),
212;
213
214pub assume_specification<T, A: Allocator> [ <Vec<T, A>>::is_empty ](
215    v: &Vec<T, A>,
216) -> (res: bool)
217    ensures res <==> v@.len() == 0,
218;
219
220pub assume_specification<T, A: Allocator>[ Vec::<T, A>::remove ](
221    vec: &mut Vec<T, A>,
222    i: usize,
223) -> (element: T)
224    requires
225        i < old(vec).len(),
226    ensures
227        element == old(vec)[i as int],
228        final(vec)@ == old(vec)@.remove(i as int),
229;
230
231pub assume_specification<T, A: Allocator>[ Vec::<T, A>::clear ](vec: &mut Vec<T, A>)
232    ensures
233        final(vec).view() == Seq::<T>::empty(),
234;
235
236pub assume_specification<T, A: Allocator>[ Vec::<T, A>::as_slice ](vec: &Vec<T, A>) -> (slice: &[T])
237    ensures
238        slice@ == vec@,
239;
240
241#[doc(hidden)]
242pub assume_specification<T, A: Allocator>[ Vec::<T, A>::as_mut_slice ](vec: &mut Vec<T, A>) -> (slice: &mut [T])
243    ensures
244        slice@ == old(vec)@,
245        final(slice)@ == final(vec)@,
246;
247
248pub assume_specification<T, A: Allocator>[ <Vec<T, A> as core::ops::Deref>::deref ](
249    vec: &Vec<T, A>,
250) -> (slice: &[T])
251    ensures
252        slice@ == vec@,
253;
254
255pub assume_specification<T, A: Allocator>[ <Vec<T, A> as core::ops::DerefMut>::deref_mut ](
256    vec: &mut Vec<T, A>,
257) -> (slice: &mut [T])
258    ensures
259        slice@ == old(vec)@,
260        final(slice)@ == final(vec)@,
261;
262
263pub assume_specification<T, A: Allocator + core::clone::Clone>[ Vec::<T, A>::split_off ](
264    vec: &mut Vec<T, A>,
265    at: usize,
266) -> (return_value: Vec<T, A>)
267    requires
268        at <= old(vec)@.len(),
269    ensures
270        final(vec)@ == old(vec)@.subrange(0, at as int),
271        return_value@ == old(vec)@.subrange(at as int, old(vec)@.len() as int),
272;
273
274pub open spec fn vec_clone_trigger<T, A: Allocator>(v1: Vec<T, A>, v2: Vec<T, A>) -> bool {
275    true
276}
277
278pub assume_specification<T: Clone, A: Allocator + Clone>[ <Vec<T, A> as Clone>::clone ](
279    vec: &Vec<T, A>,
280) -> (res: Vec<T, A>)
281    ensures
282        res.len() == vec.len(),
283        forall|i| #![all_triggers] 0 <= i < vec.len() ==> cloned::<T>(vec[i], res[i]),
284        vec_clone_trigger(*vec, res),
285        vec@ =~= res@ ==> vec@ == res@,
286;
287
288pub broadcast proof fn vec_clone_deep_view_proof<T: DeepView, A: Allocator>(
289    v1: Vec<T, A>,
290    v2: Vec<T, A>,
291)
292    requires
293        #[trigger] vec_clone_trigger(v1, v2),
294        v1.deep_view() =~= v2.deep_view(),
295    ensures
296        v1.deep_view() == v2.deep_view(),
297{
298}
299
300pub assume_specification<T, A: Allocator>[ Vec::<T, A>::truncate ](vec: &mut Vec<T, A>, len: usize)
301    ensures
302        len <= old(vec).len() ==> final(vec)@ == old(vec)@.subrange(0, len as int),
303        len > old(vec).len() ==> final(vec)@ == old(vec)@,
304;
305
306pub assume_specification<T: Clone, A: Allocator>[ Vec::<T, A>::resize ](
307    vec: &mut Vec<T, A>,
308    len: usize,
309    value: T,
310)
311    ensures
312        len <= old(vec).len() ==> final(vec)@ == old(vec)@.subrange(0, len as int),
313        len > old(vec).len() ==> {
314            &&& final(vec)@.len() == len
315            &&& final(vec)@.subrange(0, old(vec).len() as int) == old(vec)@
316            &&& forall|i| #![all_triggers] old(vec).len() <= i < len ==> cloned::<T>(value, final(vec)@[i])
317        },
318;
319
320pub broadcast proof fn axiom_vec_index_decreases<A>(v: Vec<A>, i: int)
321    requires
322        0 <= i < v.len(),
323    ensures
324        #[trigger] (decreases_to!(v => v[i])),
325{
326    admit();
327}
328
329impl<T, A: Allocator> super::core::TrustedSpecSealed for Vec<T, A> {
330
331}
332
333impl<T, A: Allocator> super::core::IndexSetTrustedSpec<usize> for Vec<T, A> {
334    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
335        0 <= index < self.len()
336    }
337
338    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
339        new_container@ == self@.update(index as int, val)
340    }
341}
342
343pub assume_specification<T: PartialEq<U>, U, A1: Allocator, A2: Allocator>[ <Vec<T, A1> as PartialEq<Vec<U, A2>>>::eq ](
344    x: &Vec<T, A1>,
345    y: &Vec<U, A2>,
346) -> bool
347;
348
349impl<T: super::cmp::PartialEqSpec<U>, U, A1: Allocator, A2: Allocator> super::cmp::PartialEqSpecImpl<Vec<U, A2>> for Vec<T, A1> {
350    open spec fn obeys_eq_spec() -> bool {
351        T::obeys_eq_spec()
352    }
353
354    open spec fn eq_spec(&self, other: &Vec<U, A2>) -> bool {
355        &&& self.len() == other.len()
356        &&& forall|i: int| #![auto] 0 <= i < self.len() ==> self[i].eq_spec(&other[i])
357    }
358}
359
360// The `into_iter` method of a `Vec` returns an iterator of type `IntoIter`,
361// so we specify that type here.
362#[verifier::external_type_specification]
363#[verifier::external_body]
364#[verifier::accept_recursive_types(T)]
365#[verifier::reject_recursive_types(A)]
366pub struct ExIntoIter<T, A: Allocator>(IntoIter<T, A>);
367
368// To allow reasoning about the "contents" of the Vec iterator, without using
369// a prophecy, we need a function that gives us the underlying sequence of the original vec.
370pub uninterp spec fn into_iter_elts<T, A: Allocator>(i: IntoIter<T, A>) -> Seq<T>;
371
372impl <T, A: Allocator> super::iter::IteratorSpecImpl for IntoIter<T, A> {
373    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
374        true
375    }
376
377    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
378    uninterp spec fn will_return_none(&self) -> bool;
379
380    #[verifier::prophetic]
381    open spec fn initial_value_relation(&self, init: &Self) -> bool {
382        &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
383        &&& into_iter_elts(*self) == IteratorSpec::remaining(self)
384    }
385
386    uninterp spec fn decrease(&self) -> Option<nat>;
387
388    open spec fn peek(&self, index: int) -> Option<Self::Item> {
389        if 0 <= index < into_iter_elts(*self).len() {
390            Some(into_iter_elts(*self)[index])
391        } else {
392            None
393        }
394    }
395}
396
397impl <T, A: Allocator> super::iter::DoubleEndedIteratorSpecImpl for IntoIter<T, A> {
398    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
399        let len = into_iter_elts(*self).len();
400        if 0 <= index < len {
401            Some(into_iter_elts(*self)[len - index - 1])
402        } else {
403            None
404        }
405    }
406}
407
408// This is used by `vec![x; n]`
409pub assume_specification<T: Clone>[ alloc::vec::from_elem ](elem: T, n: usize) -> (v: Vec<T>)
410    ensures
411        v.len() == n,
412        forall |i| 0 <= i < n ==> cloned(elem, #[trigger] v@[i]);
413
414// To allow reasoning about the returned iterator when the executable
415// function `into_iter()` is invoked in a `for` loop header (e.g., in
416// `for x in it: v.into_iter() { ... }`), we need to specify the behavior of
417// the iterator in spec mode. To do that, we add
418// `#[verifier::when_used_as_spec(spec_into_iter)` to the specification for
419// the executable `into_iter` method and define that spec function here.
420pub uninterp spec fn spec_into_iter<T, A: Allocator>(v: Vec<T, A>) -> (iter: <Vec<
421    T,
422    A,
423> as core::iter::IntoIterator>::IntoIter);
424
425pub uninterp spec fn spec_into_iter_borrowed<T, A: Allocator>(v: &Vec<T, A>) -> (iter: <&Vec<
426    T,
427    A,
428> as core::iter::IntoIterator>::IntoIter);
429
430
431pub broadcast proof fn axiom_spec_into_iter<T, A: Allocator>(v: Vec<T, A>)
432    ensures
433        #[trigger] spec_into_iter(v).remaining() == v@,
434{
435    admit();
436}
437
438pub broadcast proof fn axiom_spec_into_iter_borrowed<T, A: Allocator>(v: &Vec<T, A>)
439    ensures
440        #[trigger] spec_into_iter_borrowed(v).remaining() == v@.as_ref(),
441{
442    admit();
443}
444
445#[verifier::when_used_as_spec(spec_into_iter)]
446pub assume_specification<T, A: Allocator>[ Vec::<T, A>::into_iter ](vec: Vec<T, A>) -> (iter: <Vec<
447    T,
448    A,
449> as core::iter::IntoIterator>::IntoIter)
450    ensures
451        iter == spec_into_iter(vec),
452        IteratorSpec::decrease(&iter) is Some,
453        IteratorSpec::initial_value_relation(&iter, &iter),
454;
455
456#[verifier::when_used_as_spec(spec_into_iter_borrowed)]
457pub assume_specification<'a, T, A: Allocator> [<&'a Vec<T, A> as core::iter::IntoIterator>::into_iter] (vec: &'a Vec<T, A>) ->
458    (iter: <&'a Vec<T, A> as core::iter::IntoIterator>::IntoIter)
459    ensures
460        iter == spec_into_iter_borrowed(vec),
461        IteratorSpec::decrease(&iter) is Some,
462        IteratorSpec::initial_value_relation(&iter, &iter),
463;
464
465impl<T>  FromIteratorSpecImpl<T> for Vec<T> {
466    open spec fn from_iter_ensures(remaining: Seq<T>, s: Self) -> bool {
467        remaining == s@
468    }
469}
470
471pub broadcast proof fn lemma_vec_obeys_eq_spec<T: PartialEq>()
472    requires
473        super::super::laws_eq::obeys_eq::<T>(),
474    ensures
475        #[trigger] super::super::laws_eq::obeys_eq::<Vec<T>>(),
476{
477    broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
478    reveal(super::super::laws_eq::obeys_eq_spec_properties);
479}
480
481pub broadcast proof fn lemma_vec_obeys_view_eq<T: PartialEq + View>()
482    requires
483        super::super::laws_eq::obeys_concrete_eq::<T>(),
484    ensures
485        #[trigger] super::super::laws_eq::obeys_view_eq::<Vec<T>>(),
486{
487    use super::cmp::PartialEqSpec;
488    broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
489    reveal(super::super::laws_eq::obeys_eq_spec_properties);
490    reveal(super::super::laws_eq::obeys_concrete_eq);
491    reveal(super::super::laws_eq::obeys_view_eq);
492    assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x@ == y@);
493}
494
495pub broadcast proof fn lemma_vec_obeys_deep_eq<T: PartialEq + DeepView>()
496    requires
497        super::super::laws_eq::obeys_deep_eq::<T>(),
498    ensures
499        #[trigger] super::super::laws_eq::obeys_deep_eq::<Vec<T>>(),
500{
501    use super::cmp::PartialEqSpec;
502    broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
503    reveal(super::super::laws_eq::obeys_eq_spec_properties);
504    reveal(super::super::laws_eq::obeys_deep_eq);
505    assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x.deep_view() == y.deep_view());
506    assert forall|x: Vec<T>, y: Vec<T>| x.deep_view() == y.deep_view() implies x.eq_spec(&y) by {
507        assert(x.deep_view().len() == y.deep_view().len());
508        assert forall|i: int| #![auto] 0 <= i < x.len() implies x[i].eq_spec(&y[i]) by {
509            assert(x.deep_view()[i] == y.deep_view()[i]);
510        }
511    }
512}
513
514pub broadcast axiom fn axiom_vec_has_resolved<T>(vec: Vec<T>, i: int)
515    ensures
516        0 <= i < vec.len() ==> #[trigger] has_resolved::<Vec<T>>(vec) ==> has_resolved(
517            #[trigger] vec@[i],
518        ),
519;
520
521pub broadcast axiom fn axiom_vec_decreases_to_view<T>(v: Vec<T>)
522    ensures
523        #[trigger] (decreases_to!(v => v@));
524
525pub broadcast group group_vec_axioms {
526    axiom_spec_len,
527    axiom_vec_index_decreases,
528    vec_clone_deep_view_proof,
529    axiom_spec_into_iter,
530    axiom_spec_into_iter_borrowed,
531    axiom_vec_has_resolved,
532    axiom_vec_decreases_to_view,
533}
534
535} // verus!
vstd/std_specs/vec.rs

vstd/std_specs/
vec.rs
