Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332/// This code adds specifications for the standard-library type/// `std::collections::VecDeque`.use super::super::prelude::*;use super::iter::IteratorSpec;
use alloc::collections::vec_deque::Iter;use alloc::collections::vec_deque::VecDeque;use core::alloc::Allocator;use core::clone::Clone;use core::ops::{Index, IndexMut};use core::option::Option;use core::option::Option::None;
verus! {
#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]#[verifier::reject_recursive_types(A)]pub struct ExVecDeque<T, A: Allocator>(VecDeque<T, A>);
impl<T, A: Allocator> View for VecDeque<T, A> { type V = Seq<T>;
uninterp spec fn view(&self) -> Seq<T>;}
impl<T: DeepView, A: Allocator> DeepView for VecDeque<T, A> { type V = Seq<T::V>;
open spec fn deep_view(&self) -> Seq<T::V> { let v = self.view(); Seq::new(v.len(), |i: int| v[i].deep_view()) }}
pub trait VecDequeAdditionalSpecFns<T>: View<V = Seq<T>> { spec fn spec_index(&self, i: int) -> T recommends 0 <= i < self.view().len(), ;}
impl<T, A: Allocator> VecDequeAdditionalSpecFns<T> for VecDeque<T, A> { #[verifier::inline] open spec fn spec_index(&self, i: int) -> T { self.view().index(i) }}
////// Len (with autospec)pub uninterp spec fn spec_vec_dequeue_len<T, A: Allocator>(v: &VecDeque<T, A>) -> usize;
// This axiom is slightly better than defining spec_vec_dequeue_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: &VecDeque<T, A>) ensures #[trigger] spec_vec_dequeue_len(v) == v@.len(),{ admit();}
impl<T, A: Allocator> super::core::IndexSpecImpl<usize> for VecDeque<T, A> { open spec fn index_req(&self, index: &usize) -> bool { *index < self.len() }}
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::index ]( v: &VecDeque<T, A>, i: usize,) -> (output: &T) ensures output == v.spec_index(i as int),;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::index_mut ]( v: &mut VecDeque<T, A>, i: usize,) -> (output: &mut T) ensures *output == old(v).spec_index(i as int), final(v)@ == old(v)@.update(i as int, *final(output)),;
#[verifier::when_used_as_spec(spec_vec_dequeue_len)]pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::len ](v: &VecDeque<T, A>) -> (len: usize) ensures len == spec_vec_dequeue_len(v),;
pub assume_specification<T>[ VecDeque::<T>::new ]() -> (v: VecDeque<T>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T>[ <VecDeque<T> as core::default::Default>::default ]() -> (v: VecDeque< T,>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T>[ VecDeque::<T>::with_capacity ](capacity: usize) -> (v: VecDeque<T>) ensures v@ == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::reserve ]( v: &mut VecDeque<T, A>, additional: usize,) ensures final(v)@ == old(v)@,;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_back ]( v: &mut VecDeque<T, A>, value: T,) ensures final(v)@ == old(v)@.push(value),;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::push_front ]( v: &mut VecDeque<T, A>, value: T,) ensures final(v)@ == seq![value] + old(v)@,;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_back ]( v: &mut VecDeque<T, A>,) -> (value: Option<T>) ensures match value { Some(x) => { &&& old(v)@.len() > 0 &&& x == old(v)@[old(v)@.len() - 1] &&& final(v)@ == old(v)@[..old(v)@.len() - 1] }, None => { &&& old(v)@.len() == 0 &&& final(v)@ == old(v)@ }, },;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::pop_front ]( v: &mut VecDeque<T, A>,) -> (value: Option<T>) ensures match value { Some(x) => { &&& old(v)@.len() > 0 &&& x == old(v)@[0] &&& final(v)@ == old(v)@[1..] }, None => { &&& old(v)@.len() == 0 &&& final(v)@ == old(v)@ }, },;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::append ]( v: &mut VecDeque<T, A>, other: &mut VecDeque<T, A>,) ensures final(v)@ == old(v)@ + old(other)@, final(other)@ == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::insert ]( v: &mut VecDeque<T, A>, i: usize, element: T,) requires i <= old(v).len(), ensures final(v)@ == old(v)@.insert(i as int, element),;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::remove ]( v: &mut VecDeque<T, A>, i: usize,) -> (element: Option<T>) ensures match element { Some(x) => { &&& i < old(v)@.len() &&& x == old(v)@[i as int] &&& final(v)@ == old(v)@.remove(i as int) }, None => { &&& old(v)@.len() <= i &&& final(v)@ == old(v)@ }, },;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::clear ](v: &mut VecDeque<T, A>) ensures final(v).view() == Seq::<T>::empty(),;
pub assume_specification<T, A: Allocator + core::clone::Clone>[ VecDeque::<T, A>::split_off ]( v: &mut VecDeque<T, A>, at: usize,) -> (return_value: VecDeque<T, A>) requires at <= old(v)@.len(), ensures final(v)@ == old(v)@[..at], return_value@ == old(v)@[at..],;
pub open spec fn vec_dequeue_clone_trigger<T, A: Allocator>( v1: VecDeque<T, A>, v2: VecDeque<T, A>,) -> bool { true}
pub assume_specification<T: Clone, A: Allocator + Clone>[ <VecDeque<T, A> as Clone>::clone ]( v: &VecDeque<T, A>,) -> (res: VecDeque<T, A>) ensures res.len() == v.len(), forall|i| #![all_triggers] 0 <= i < v.len() ==> cloned::<T>(v[i], res[i]), vec_dequeue_clone_trigger(*v, res), v@ =~= res@ ==> v@ == res@,;
pub assume_specification<T, A: Allocator>[ VecDeque::<T, A>::truncate ]( v: &mut VecDeque<T, A>, len: usize,) ensures len <= old(v).len() ==> final(v)@ == old(v)@[..len], len > old(v).len() ==> final(v)@ == old(v)@,;
pub assume_specification<T: Clone, A: Allocator>[ VecDeque::<T, A>::resize ]( v: &mut VecDeque<T, A>, len: usize, value: T,) ensures len <= old(v).len() ==> final(v)@ == old(v)@[..len], len > old(v).len() ==> { &&& final(v)@.len() == len &&& final(v)@[..old(v).len()] == old(v)@ &&& forall|i| #![all_triggers] old(v).len() <= i < len ==> cloned::<T>(value, final(v)@[i]) },;
pub broadcast proof fn axiom_vec_dequeue_index_decreases<A>(v: VecDeque<A>, i: int) requires 0 <= i < v.len(), ensures #[trigger] (decreases_to!(v => v[i])),{ admit();}
// The `iter` method of a `VecDeque` returns an iterator of type `Iter`,// so we specify that type here.#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
// To allow reasoning about the "contents" of the VecDeque 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<'a, T: 'a>(i: Iter<'a, T>) -> Seq<&'a T>;
impl<'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> { 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<'a, T: 'a> super::iter::DoubleEndedIteratorSpecImpl for Iter<'a, T> { open spec fn peek_back(&self, index: int) -> Option<Self::Item> { if 0 <= index < into_iter_elts(*self).len() { Some(&into_iter_elts(*self)[into_iter_elts(*self).len() - index - 1]) } else { None } }}
pub assume_specification<'a, T, A: Allocator>[ VecDeque::<T, A>::iter ]( v: &'a VecDeque<T, A>,) -> (iter: Iter<'a, T>) ensures IteratorSpec::remaining(&iter) == v@.as_ref(), into_iter_elts(iter) == IteratorSpec::remaining(&iter), IteratorSpec::decrease(&iter) is Some,;
pub broadcast group group_vec_dequeue_axioms { axiom_spec_len, axiom_vec_dequeue_index_decreases,}
} // verus!