vstd/std_specs/
vec.rs

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

vstd/std_specs/
vec.rs
