vstd/std_specs/
vec.rs

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

vstd/std_specs/
vec.rs
