Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517use super::super::prelude::*;use super::iter::{FromIteratorSpecImpl, IteratorSpec};use verus_builtin::*;
use super::super::slice::SliceIndexSpec;use super::core::IndexSpec;use alloc::collections::TryReserveError;use alloc::vec::{IntoIter, Vec};use core::alloc::Allocator;use core::clone::Clone;use core::marker::PhantomData;use core::ops::Index;use core::option::Option;use core::option::Option::None;use core::slice::SliceIndex;
use verus as verus_skip_verusfmt;verus_skip_verusfmt! {
#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]#[verifier::reject_recursive_types(A)]pub struct ExVec<T, A: Allocator>(Vec<T, A>);
pub trait VecAdditionalSpecFns<T>: View<V = Seq<T>> { spec fn spec_index(&self, i: int) -> T recommends 0 <= i < self.view().len(), ;}
impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> { #[verifier::inline] open spec fn spec_index(&self, i: int) -> T { self.view().index(i) }}
#[verifier::external_type_specification]#[verifier::external_body]pub struct ExTryReserveError(alloc::collections::TryReserveError);
// We still have a special case for Vec::index on usize.// The general Vec::index case now goes through the Index trait,// but this special case is still here because it's more direct and efficient in its SMT encoding,// and Vec::index on usize is very common.//// So this is a bit of a hack, but we just manually redirect// `vec[i]` to this function here from rust_to_vir_expr.#[verifier::external_body]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::vec::vec_index")]pub fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> (element: &T) requires i < vec.view().len(), ensures *element == vec.view().index(i as int), no_unwind{ &vec[i]}
/// This is a specification for the indexing operator `vec[i]` when it expands to the `IndexMut` trait#[doc(hidden)]#[verifier::external_body]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::vec::vec_index_mut")]pub fn vec_index_mut<T, A: Allocator>(vec: &mut Vec<T, A>, i: usize) -> (element: &mut T) requires i < vec.view().len(), ensures *element == old(vec)@.index(i as int), final(vec)@ == old(vec)@.update(i as int, *final(element)),
*final(element) == final(vec).view().index(i as int), no_unwind{ &mut vec[i]}
////// Len (with autospec)pub uninterp spec fn spec_vec_len<T, A: Allocator>(v: &Vec<T, A>) -> usize;
// This axiom is slightly better than defining spec_vec_len to just be `v@.len() as usize`// (the axiom also shows that v@.len() is in-bounds for usize)pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &Vec<T, A>) ensures #[trigger] spec_vec_len(v) == v@.len(),{ admit();}
#[verifier::when_used_as_spec(spec_vec_len)]pub assume_specification<T, A: Allocator>[ Vec::<T, A>::len ](vec: &Vec<T, A>) -> (len: usize) ensures len == spec_vec_len(vec), no_unwind;
////// Other functionspub assume_specification<T>[ Vec::<T>::new ]() -> (v: Vec<T>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T>[ <Vec<T> as core::default::Default>::default ]() -> (v: Vec<T>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::new_in ](alloc: A) -> (v: Vec<T, A>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T>[ Vec::<T>::with_capacity ](capacity: usize) -> (v: Vec<T>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::with_capacity_in ](capacity: usize, alloc: A) -> (v: Vec<T, A>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::reserve ]( vec: &mut Vec<T, A>, additional: usize,) ensures final(vec)@ == old(vec)@,;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::try_reserve ]( vec: &mut Vec<T, A>, additional: usize,) -> (result: Result<(), TryReserveError>) ensures final(vec)@ == old(vec)@,;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::try_reserve_exact ]( vec: &mut Vec<T, A>, additional: usize,) -> (result: Result<(), TryReserveError>) ensures final(vec)@ == old(vec)@,;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::push ](vec: &mut Vec<T, A>, value: T) ensures final(vec)@ == old(vec)@.push(value),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::pop ](vec: &mut Vec<T, A>) -> (value: Option<T>) ensures old(vec)@.len() > 0 ==> value == Some(old(vec)@[old(vec)@.len() - 1]) && final(vec)@ == old(vec)@[..old(vec)@.len() - 1], old(vec)@.len() == 0 ==> value == None::<T> && final(vec)@ == old(vec)@,;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::append ]( vec: &mut Vec<T, A>, other: &mut Vec<T, A>,) ensures final(vec)@ == old(vec)@ + old(other)@, final(other)@ == Seq::<T>::empty(),;
pub assume_specification<T: core::clone::Clone, A: Allocator>[ Vec::<T, A>::extend_from_slice ]( vec: &mut Vec<T, A>, other: &[T],) ensures final(vec)@.len() == old(vec)@.len() + other@.len(), forall|i: int| #![trigger final(vec)@[i]] 0 <= i < final(vec)@.len() ==> if i < old(vec)@.len() { final(vec)@[i] == old(vec)@[i] } else { cloned::<T>(other@[i - old(vec)@.len()], final(vec)@[i]) },;
impl<T: Sized, I: SliceIndex<[T]>, A: Allocator> super::core::IndexSpecImpl<I> for Vec<T, A> { open spec fn index_req(&self, index: &I) -> bool { forall|s: &[T]| #[trigger] s@ == self@ ==> index.in_bounds(s) }}
pub assume_specification<T, I: SliceIndex<[T]>, A: Allocator>[Vec::<T, A>::index]( vec: &Vec<T, A>, i: I,) -> (r: &<Vec<T, A> as Index<I>>::Output) ensures exists|s: &[T]| #[trigger] s@ == vec@ && call_ensures(<I as SliceIndex<[T]>>::index, (i, s), r),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::swap_remove ]( vec: &mut Vec<T, A>, i: usize,) -> (element: T) requires i < old(vec).len(), ensures element == old(vec)[i as int], final(vec)@ == old(vec)@.update(i as int, old(vec)@.last()).drop_last(),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::insert ]( vec: &mut Vec<T, A>, i: usize, element: T,) requires i <= old(vec).len(), ensures final(vec)@ == old(vec)@.insert(i as int, element),;
pub assume_specification<T, A: Allocator> [ <Vec<T, A>>::is_empty ]( v: &Vec<T, A>,) -> (res: bool) ensures res <==> v@.len() == 0, opens_invariants none no_unwind;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::remove ]( vec: &mut Vec<T, A>, i: usize,) -> (element: T) requires i < old(vec).len(), ensures element == old(vec)[i as int], final(vec)@ == old(vec)@.remove(i as int),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::clear ](vec: &mut Vec<T, A>) ensures final(vec).view() == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::as_slice ](vec: &Vec<T, A>) -> (slice: &[T]) ensures slice@ == vec@, opens_invariants none no_unwind;
pub assume_specification<T, A: Allocator>[ <Vec<T, A> as core::convert::AsRef<[T]>>::as_ref ]( vec: &Vec<T, A>,) -> (slice: &[T]) ensures slice@ == vec@, opens_invariants none no_unwind;
#[doc(hidden)]pub assume_specification<T, A: Allocator>[ Vec::<T, A>::as_mut_slice ](vec: &mut Vec<T, A>) -> (slice: &mut [T]) ensures slice@ == old(vec)@, final(slice)@ == final(vec)@, opens_invariants none no_unwind;
pub assume_specification<T, A: Allocator>[ <Vec<T, A> as core::ops::Deref>::deref ]( vec: &Vec<T, A>,) -> (slice: &[T]) ensures slice@ == vec@,;
pub assume_specification<T, A: Allocator>[ <Vec<T, A> as core::ops::DerefMut>::deref_mut ]( vec: &mut Vec<T, A>,) -> (slice: &mut [T]) ensures slice@ == old(vec)@, final(slice)@ == final(vec)@,;
pub assume_specification<T, A: Allocator + core::clone::Clone>[ Vec::<T, A>::split_off ]( vec: &mut Vec<T, A>, at: usize,) -> (return_value: Vec<T, A>) requires at <= old(vec)@.len(), ensures final(vec)@ == old(vec)@[..at], return_value@ == old(vec)@[at..],;
pub open spec fn vec_clone_trigger<T, A: Allocator>(v1: Vec<T, A>, v2: Vec<T, A>) -> bool { true}
pub assume_specification<T: Clone, A: Allocator + Clone>[ <Vec<T, A> as Clone>::clone ]( vec: &Vec<T, A>,) -> (res: Vec<T, A>) ensures res.len() == vec.len(), forall|i| #![all_triggers] 0 <= i < vec.len() ==> cloned::<T>(vec[i], res[i]), vec_clone_trigger(*vec, res), vec@ =~= res@ ==> vec@ == res@,;
pub broadcast proof fn vec_clone_deep_view_proof<T: DeepView, A: Allocator>( v1: Vec<T, A>, v2: Vec<T, A>,) requires #[trigger] vec_clone_trigger(v1, v2), v1.deep_view() =~= v2.deep_view(), ensures v1.deep_view() == v2.deep_view(),{}
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::truncate ](vec: &mut Vec<T, A>, len: usize) ensures len <= old(vec).len() ==> final(vec)@ == old(vec)@[..len], len > old(vec).len() ==> final(vec)@ == old(vec)@,;
pub assume_specification<T: Clone, A: Allocator>[ Vec::<T, A>::resize ]( vec: &mut Vec<T, A>, len: usize, value: T,) ensures len <= old(vec).len() ==> final(vec)@ == old(vec)@[..len], len > old(vec).len() ==> { &&& final(vec)@.len() == len &&& final(vec)@[..old(vec).len()] == old(vec)@ &&& forall|i| #![all_triggers] old(vec).len() <= i < len ==> cloned::<T>(value, final(vec)@[i]) },;
pub broadcast proof fn axiom_vec_index_decreases<A>(v: Vec<A>, i: int) requires 0 <= i < v.len(), ensures #[trigger] (decreases_to!(v => v[i])),{ admit();}
pub assume_specification<T: PartialEq<U>, U, A1: Allocator, A2: Allocator>[ <Vec<T, A1> as PartialEq<Vec<U, A2>>>::eq ]( x: &Vec<T, A1>, y: &Vec<U, A2>,) -> bool;
impl<T: super::cmp::PartialEqSpec<U>, U, A1: Allocator, A2: Allocator> super::cmp::PartialEqSpecImpl<Vec<U, A2>> for Vec<T, A1> { open spec fn obeys_eq_spec() -> bool { T::obeys_eq_spec() }
open spec fn eq_spec(&self, other: &Vec<U, A2>) -> bool { &&& self.len() == other.len() &&& forall|i: int| #![auto] 0 <= i < self.len() ==> self[i].eq_spec(&other[i]) }}
// The `into_iter` method of a `Vec` returns an iterator of type `IntoIter`,// so we specify that type here.#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]#[verifier::reject_recursive_types(A)]pub struct ExIntoIter<T, A: Allocator>(IntoIter<T, A>);
// To allow reasoning about the "contents" of the Vec iterator, without using// a prophecy, we need a function that gives us the underlying sequence of the original vec.pub uninterp spec fn into_iter_elts<T, A: Allocator>(i: IntoIter<T, A>) -> Seq<T>;
impl <T, A: Allocator> super::iter::IteratorSpecImpl for IntoIter<T, A> { open spec fn obeys_prophetic_iter_laws(&self) -> bool { true }
uninterp spec fn remaining(&self) -> Seq<Self::Item>; #[verifier::prophetic] open spec fn produces(&self) -> Seq<bool> { Seq::new(IteratorSpec::remaining(self).len(), |i: int| true) } uninterp spec fn decrease(&self) -> Option<nat>;
open spec fn peek(&self, index: int) -> Option<Self::Item> { if 0 <= index < into_iter_elts(*self).len() { Some(into_iter_elts(*self)[index]) } else { None } }}
impl <T, A: Allocator> super::iter::DoubleEndedIteratorSpecImpl for IntoIter<T, A> { open spec fn peek_back(&self, index: int) -> Option<Self::Item> { let len = into_iter_elts(*self).len(); if 0 <= index < len { Some(into_iter_elts(*self)[len - index - 1]) } else { None } }}
// This is used by `vec![x; n]`pub assume_specification<T: Clone>[ alloc::vec::from_elem ](elem: T, n: usize) -> (v: Vec<T>) ensures v.len() == n, forall |i| 0 <= i < n ==> cloned(elem, #[trigger] v@[i]);
pub assume_specification<T, A: Allocator>[ Vec::<T, A>::into_iter ](vec: Vec<T, A>) -> (iter: <Vec< T, A,> as core::iter::IntoIterator>::IntoIter) ensures IteratorSpec::remaining(&iter) == vec@, into_iter_elts(iter) == IteratorSpec::remaining(&iter), IteratorSpec::decrease(&iter) is Some,;
pub assume_specification<'a, T, A: Allocator> [<&'a Vec<T, A> as core::iter::IntoIterator>::into_iter] (vec: &'a Vec<T, A>) -> (iter: <&'a Vec<T, A> as core::iter::IntoIterator>::IntoIter) ensures IteratorSpec::remaining(&iter) == vec@.as_ref(), super::slice::into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(), IteratorSpec::decrease(&iter) is Some,;
impl<T> FromIteratorSpecImpl<T> for Vec<T> { open spec fn from_iter_ensures(remaining: Seq<T>, produces: Seq<bool>, s: Self) -> bool { &&& produces.len() == remaining.len() &&& produces.all(|p: bool| p) &&& remaining == s@ }}
pub broadcast proof fn lemma_vec_obeys_eq_spec<T: PartialEq>() requires super::super::laws_eq::obeys_eq::<T>(), ensures #[trigger] super::super::laws_eq::obeys_eq::<Vec<T>>(),{ broadcast use {axiom_spec_len, super::super::seq::group_seq_lemmas}; reveal(super::super::laws_eq::obeys_eq_spec_properties);}
pub broadcast proof fn lemma_vec_obeys_view_eq<T: PartialEq + View>() requires super::super::laws_eq::obeys_concrete_eq::<T>(), ensures #[trigger] super::super::laws_eq::obeys_view_eq::<Vec<T>>(),{ use super::cmp::PartialEqSpec; broadcast use {axiom_spec_len, super::super::seq::group_seq_lemmas}; reveal(super::super::laws_eq::obeys_eq_spec_properties); reveal(super::super::laws_eq::obeys_concrete_eq); reveal(super::super::laws_eq::obeys_view_eq); assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x@ == y@);}
pub broadcast proof fn lemma_vec_obeys_deep_eq<T: PartialEq + DeepView>() requires super::super::laws_eq::obeys_deep_eq::<T>(), ensures #[trigger] super::super::laws_eq::obeys_deep_eq::<Vec<T>>(),{ use super::cmp::PartialEqSpec; broadcast use {axiom_spec_len, super::super::seq::group_seq_lemmas}; reveal(super::super::laws_eq::obeys_eq_spec_properties); reveal(super::super::laws_eq::obeys_deep_eq); assert(forall|x: Vec<T>, y: Vec<T>| x.eq_spec(&y) ==> x.deep_view() == y.deep_view()); assert forall|x: Vec<T>, y: Vec<T>| x.deep_view() == y.deep_view() implies x.eq_spec(&y) by { assert(x.deep_view().len() == y.deep_view().len()); assert forall|i: int| #![auto] 0 <= i < x.len() implies x[i].eq_spec(&y[i]) by { assert(x.deep_view()[i] == y.deep_view()[i]); } }}
pub broadcast axiom fn axiom_vec_has_resolved<T>(vec: Vec<T>, i: int) ensures 0 <= i < vec.len() ==> #[trigger] has_resolved::<Vec<T>>(vec) ==> has_resolved( #[trigger] vec@[i], ),;
pub broadcast axiom fn axiom_vec_decreases_to_view<T>(v: Vec<T>) ensures #[trigger] (decreases_to!(v => v@));
pub broadcast group group_vec_axioms { axiom_spec_len, axiom_vec_index_decreases, vec_clone_deep_view_proof, axiom_vec_has_resolved, axiom_vec_decreases_to_view,}
pub axiom fn tracked_borrow_slice<T, A: Allocator>(tracked vec: &Vec<T, A>) -> (tracked t: &[T]) ensures t@ == vec@;
pub axiom fn tracked_borrow_mut_slice<T, A: Allocator>(tracked vec: &mut Vec<T, A>) -> (tracked t: &mut [T]) ensures (*t)@ == old(vec)@, (*t).len() == final(t).len(), final(vec)@ == final(t)@;
} // verus!