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#[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
56pub uninterp spec fn spec_vec_len<T, A: Allocator>(v: &Vec<T, A>) -> usize;
58
59pub 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
75pub 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
132pub 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
274pub assume_specification<T: PartialEq<U>, U, A1: Allocator, A2: Allocator>[ <Vec<T, A1> as PartialEq<Vec<U, A2>>>::eq ](
275 x: &Vec<T, A1>,
276 y: &Vec<U, A2>,
277) -> bool
278;
279
280impl<T: super::cmp::PartialEqSpec<U>, U, A1: Allocator, A2: Allocator> super::cmp::PartialEqSpecImpl<Vec<U, A2>> for Vec<T, A1> {
281 open spec fn obeys_eq_spec() -> bool {
282 T::obeys_eq_spec()
283 }
284
285 open spec fn eq_spec(&self, other: &Vec<U, A2>) -> bool {
286 &&& self.len() == other.len()
287 &&& forall|i: int| #![auto] 0 <= i < self.len() ==> self[i].eq_spec(&other[i])
288 }
289}
290
291#[verifier::external_type_specification]
294#[verifier::external_body]
295#[verifier::accept_recursive_types(T)]
296#[verifier::reject_recursive_types(A)]
297pub struct ExIntoIter<T, A: Allocator>(IntoIter<T, A>);
298
299impl<T, A: Allocator> View for IntoIter<T, A> {
300 type V = (int, Seq<T>);
301
302 uninterp spec fn view(self: &IntoIter<T, A>) -> (int, Seq<T>);
303}
304
305pub assume_specification<T, A: Allocator>[ IntoIter::<T, A>::next ](
306 elements: &mut IntoIter<T, A>,
307) -> (r: Option<T>)
308 ensures
309 ({
310 let (old_index, old_seq) = old(elements)@;
311 match r {
312 None => {
313 &&& elements@ == old(elements)@
314 &&& old_index >= old_seq.len()
315 },
316 Some(element) => {
317 let (new_index, new_seq) = elements@;
318 &&& 0 <= old_index < old_seq.len()
319 &&& new_seq == old_seq
320 &&& new_index == old_index + 1
321 &&& element == old_seq[old_index]
322 },
323 }
324 }),
325;
326
327pub struct IntoIterGhostIterator<T, A: Allocator> {
328 pub pos: int,
329 pub elements: Seq<T>,
330 pub _marker: PhantomData<A>,
331}
332
333impl<T, A: Allocator> super::super::pervasive::ForLoopGhostIteratorNew for IntoIter<T, A> {
334 type GhostIter = IntoIterGhostIterator<T, A>;
335
336 open spec fn ghost_iter(&self) -> IntoIterGhostIterator<T, A> {
337 IntoIterGhostIterator { pos: self@.0, elements: self@.1, _marker: PhantomData }
338 }
339}
340
341impl<T, A: Allocator> super::super::pervasive::ForLoopGhostIterator for IntoIterGhostIterator<
342 T,
343 A,
344> {
345 type ExecIter = IntoIter<T, A>;
346
347 type Item = T;
348
349 type Decrease = int;
350
351 open spec fn exec_invariant(&self, exec_iter: &IntoIter<T, A>) -> bool {
352 &&& self.pos == exec_iter@.0
353 &&& self.elements == exec_iter@.1
354 }
355
356 open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
357 init matches Some(init) ==> {
358 &&& init.pos == 0
359 &&& init.elements == self.elements
360 &&& 0 <= self.pos <= self.elements.len()
361 }
362 }
363
364 open spec fn ghost_ensures(&self) -> bool {
365 self.pos == self.elements.len()
366 }
367
368 open spec fn ghost_decrease(&self) -> Option<int> {
369 Some(self.elements.len() - self.pos)
370 }
371
372 open spec fn ghost_peek_next(&self) -> Option<T> {
373 if 0 <= self.pos < self.elements.len() {
374 Some(self.elements[self.pos])
375 } else {
376 None
377 }
378 }
379
380 open spec fn ghost_advance(&self, _exec_iter: &IntoIter<T, A>) -> IntoIterGhostIterator<T, A> {
381 Self { pos: self.pos + 1, ..*self }
382 }
383}
384
385impl<T, A: Allocator> View for IntoIterGhostIterator<T, A> {
386 type V = Seq<T>;
387
388 open spec fn view(&self) -> Seq<T> {
389 self.elements.take(self.pos)
390 }
391}
392
393pub uninterp spec fn spec_into_iter<T, A: Allocator>(v: Vec<T, A>) -> (iter: <Vec<
400 T,
401 A,
402> as core::iter::IntoIterator>::IntoIter);
403
404pub broadcast proof fn axiom_spec_into_iter<T, A: Allocator>(v: Vec<T, A>)
405 ensures
406 (#[trigger] spec_into_iter(v))@ == (0int, v@),
407{
408 admit();
409}
410
411#[verifier::when_used_as_spec(spec_into_iter)]
412pub assume_specification<T, A: Allocator>[ Vec::<T, A>::into_iter ](vec: Vec<T, A>) -> (iter: <Vec<
413 T,
414 A,
415> as core::iter::IntoIterator>::IntoIter)
416 ensures
417 iter@ == (0int, vec@),
418;
419
420pub broadcast proof fn lemma_vec_obeys_eq_spec<T: PartialEq>()
421 requires
422 super::super::laws_eq::obeys_eq_spec::<T>(),
423 ensures
424 #[trigger] super::super::laws_eq::obeys_eq_spec::<Vec<T>>(),
425{
426 broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
427 reveal(super::super::laws_eq::obeys_eq_spec_properties);
428}
429
430pub broadcast proof fn lemma_vec_obeys_view_eq<T: PartialEq + View>()
431 requires
432 super::super::laws_eq::obeys_concrete_eq::<T>(),
433 ensures
434 #[trigger] super::super::laws_eq::obeys_view_eq::<Vec<T>>(),
435{
436 use super::cmp::PartialEqSpec;
437 broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
438 reveal(super::super::laws_eq::obeys_eq_spec_properties);
439 reveal(super::super::laws_eq::obeys_concrete_eq);
440 reveal(super::super::laws_eq::obeys_view_eq);
441 assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x@ == y@);
442}
443
444pub broadcast proof fn lemma_vec_obeys_deep_eq<T: PartialEq + DeepView>()
445 requires
446 super::super::laws_eq::obeys_deep_eq::<T>(),
447 ensures
448 #[trigger] super::super::laws_eq::obeys_deep_eq::<Vec<T>>(),
449{
450 use super::cmp::PartialEqSpec;
451 broadcast use {axiom_spec_len, super::super::seq::group_seq_axioms};
452 reveal(super::super::laws_eq::obeys_eq_spec_properties);
453 reveal(super::super::laws_eq::obeys_deep_eq);
454 assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x.deep_view() == y.deep_view());
455 assert forall|x: Vec<T>, y: Vec<T>| x.deep_view() == y.deep_view() implies x.eq_spec(&y) by {
456 assert(x.deep_view().len() == y.deep_view().len());
457 assert forall|i: int| #![auto] 0 <= i < x.len() implies x[i].eq_spec(&y[i]) by {
458 assert(x.deep_view()[i] == y.deep_view()[i]);
459 }
460 }
461}
462
463pub broadcast group group_vec_axioms {
464 axiom_spec_len,
465 axiom_vec_index_decreases,
466 vec_clone_deep_view_proof,
467 axiom_spec_into_iter,
468}
469
470}