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

vstd/std_specs/
vec.rs
