Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518//! This module contains [`Seq`]-specific method implementations.use crate::contrib::exec_spec::*;use crate::prelude::*;#[cfg(verus_keep_ghost)]use crate::std_specs::cmp::PartialEqSpec;
verus! {
// Note: the exec translations which use iterators are unverified.broadcast use crate::group_vstd_default;
/// Impls for shared traits/// NOTE: can't implement [`ExecSpecType`] for [`Seq<T>`]/// since it conflicts with [`SpecString`] (i.e., [`Seq<char>`]).impl<'a, T: DeepView> ToRef<&'a [T]> for &'a Vec<T> { #[inline(always)] fn get_ref(self) -> &'a [T] { self.as_slice() }}
impl<'a, T: DeepView + DeepViewClone> ToOwned<Vec<T>> for &'a [T] { /// TODO: verify this #[verifier::external_body] #[inline(always)] fn get_owned(self) -> Vec<T> { self.iter().map(|x| x.deep_clone()).collect() }}
impl<T: DeepViewClone> DeepViewClone for Vec<T> { /// TODO: verify this #[verifier::external_body] #[inline(always)] fn deep_clone(&self) -> Self { self.iter().map(|x| x.deep_clone()).collect() }}
impl<T: ObeysDeepEq> ObeysDeepEq for Vec<T> { proof fn lemma_obeys_deep_eq() { broadcast use crate::std_specs::vec::lemma_vec_obeys_deep_eq;
T::lemma_obeys_deep_eq(); }}
impl<'a, T: ObeysDeepEq> ObeysDeepEq for &'a [T] { proof fn lemma_obeys_deep_eq() { T::lemma_obeys_deep_eq(); reveal(crate::laws_eq::obeys_deep_eq); assert forall|x: &[T], y: &[T]| <&[T] as PartialEqSpec>::eq_spec(&x, &y) <==> x.deep_view() == y.deep_view() by { assert(x.deep_view().len() == x@.len() && y.deep_view().len() == y@.len()); if x.deep_view() == y.deep_view() { assert forall|i: int| 0 <= i < x@.len() implies #[trigger] x@[i].eq_spec( &y@[i], ) by { assert(x.deep_view()[i] == y.deep_view()[i]); } } if <&[T] as PartialEqSpec>::eq_spec(&x, &y) { assert(x.deep_view() =~= y.deep_view()); } } }}
impl<'a, T: DeepView> ExecSpecLen for &'a [T] { #[inline(always)] fn exec_len(self) -> (res: usize) ensures res == self.deep_view().len(), { self.len() }}
impl<'a, T: DeepView> ExecSpecIndex<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_index(self, index: usize) -> (res: Self::Elem) ensures res.deep_view() == self.deep_view()[index as int], { self.get(index).unwrap() }}
//// Trait definitions for methods///// Spec for executable version of [`Seq::add`].pub trait ExecSpecSeqAdd<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> { fn exec_add(self, rhs: Self) -> Out;}
/// Spec for executable version of [`Seq::push`].pub trait ExecSpecSeqPush<'a, Out: Sized + DeepView>: Sized + DeepView + ToOwned<Out> { type Elem: DeepView + DeepViewClone;
fn exec_push(self, a: Self::Elem) -> Out;}
/// Spec for executable version of [`Seq::update`].pub trait ExecSpecSeqUpdate<'a, Out: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>>>: Sized + DeepView + ToOwned<Out> { type Elem: DeepView + DeepViewClone;
fn exec_update(self, i: usize, a: Self::Elem) -> Out requires 0 <= i < self.deep_view().len(), ;}
/// Spec for executable version of [`Seq::subrange`].pub trait ExecSpecSeqSubrange<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_subrange(self, start_inclusive: usize, end_exclusive: usize) -> Self requires 0 <= start_inclusive <= end_exclusive <= self.deep_view().len(), ;}
/// Spec for executable version of [`Seq::empty`].pub trait ExecSpecSeqEmpty: Sized { fn exec_empty() -> Self;}
/// Spec for executable version of [`Seq::to_multiset`].pub trait ExecSpecSeqToMultiset<'a>: Sized { type Elem: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq;
fn exec_to_multiset(self) -> ExecMultiset<Self::Elem>;}
// The implementations here for interp Seq methods (e.g. take) could be streamlined.// Currently, the spec fn definition is copied and translated to the exec version by hand.// A more concise approach would be to apply the exec_spec macro directly to the spec fns on Seq./// Spec for executable version of [`Seq::drop_first`].pub trait ExecSpecSeqDropFirst<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_drop_first(self) -> Self requires self.deep_view().len() >= 1, ;}
/// Spec for executable version of [`Seq::drop_last`].pub trait ExecSpecSeqDropLast<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_drop_last(self) -> Self requires self.deep_view().len() >= 1, ;}
/// Spec for executable version of [`Seq::take`].pub trait ExecSpecSeqTake<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_take(self, n: usize) -> Self requires 0 <= n <= self.deep_view().len(), ;}
/// Spec for executable version of [`Seq::skip`].pub trait ExecSpecSeqSkip<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_skip(self, n: usize) -> Self requires 0 <= n <= self.deep_view().len(), ;}
/// Spec for executable version of [`Seq::last`].pub trait ExecSpecSeqLast<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_last(self) -> Self::Elem requires 0 < self.deep_view().len(), ;}
/// Spec for executable version of [`Seq::first`].pub trait ExecSpecSeqFirst<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> { type Elem: DeepView;
fn exec_first(self) -> Self::Elem requires 0 < self.deep_view().len(), ;}
/// Spec for executable version of [`Seq::is_prefix_of`].pub trait ExecSpecSeqIsPrefixOf<'a>: DeepView + Sized { type Other: DeepView<V = Self::V>;
fn exec_is_prefix_of(self, other: Self::Other) -> (res: bool);}
/// Spec for executable version of [`Seq::is_suffix_of`].pub trait ExecSpecSeqIsSuffixOf<'a>: DeepView + Sized { type Other: DeepView<V = Self::V>;
fn exec_is_suffix_of(self, other: Self::Other) -> (res: bool);}
/// Spec for executable version of [`Seq::contains`].pub trait ExecSpecSeqContains<'a>: Sized + DeepView { type Elem: DeepView;
fn exec_contains(self, needle: Self::Elem) -> bool;}
/// Spec for executable version of [`Seq::index_of`].pub trait ExecSpecSeqIndexOf<'a>: Sized + DeepView { type Elem: DeepView;
fn exec_index_of(self, needle: Self::Elem) -> usize;}
/// Spec for executable version of [`Seq::index_of_first`].pub trait ExecSpecSeqIndexOfFirst<'a>: Sized + DeepView { type Elem: DeepView;
fn exec_index_of_first(self, needle: Self::Elem) -> Option<usize>;}
/// Spec for executable version of [`Seq::index_of_last`].pub trait ExecSpecSeqIndexOfLast<'a>: Sized + DeepView { type Elem: DeepView;
fn exec_index_of_last(self, needle: Self::Elem) -> Option<usize>;}
//// Implementations for Vec and slices//impl<'a, T: DeepView + DeepViewClone> ExecSpecSeqAdd<'a, Vec<T>> for &'a [T] { #[verifier::external_body] #[inline(always)] fn exec_add(self, rhs: Self) -> (res: Vec<T>) ensures res.deep_view() =~= self.deep_view().add(rhs.deep_view()), { self.get_owned().into_iter().chain(rhs.get_owned()).collect() }}
impl<'a, T: DeepView + DeepViewClone> ExecSpecSeqPush<'a, Vec<T>> for &'a [T] { type Elem = T;
#[verifier::external_body] #[inline(always)] fn exec_push(self, a: Self::Elem) -> (res: Vec<T>) ensures res.deep_view() =~= self.deep_view().push(a.deep_view()), { let v = vec![a]; self.get_owned().into_iter().chain(v).collect() }}
impl<'a, T: DeepView + DeepViewClone> ExecSpecSeqUpdate<'a, Vec<T>> for &'a [T] { type Elem = T;
#[verifier::external_body] #[inline(always)] fn exec_update(self, i: usize, a: Self::Elem) -> (res: Vec<T>) ensures res.deep_view() =~= self.deep_view().update(i as int, a.deep_view()), { let mut v: Vec<T> = self.get_owned(); v[i] = a.deep_clone(); v }}
impl<'a, T: DeepView> ExecSpecSeqSubrange<'a> for &'a [T] { type Elem = &'a T;
#[verifier::external_body] #[inline(always)] fn exec_subrange(self, start_inclusive: usize, end_exclusive: usize) -> (res: Self) ensures res.deep_view() =~= self.deep_view()[start_inclusive..end_exclusive], { &self[start_inclusive..end_exclusive] }}
impl<T: DeepView> ExecSpecSeqEmpty for Vec<T> { #[inline(always)] fn exec_empty() -> (res: Self) ensures res.deep_view() =~= Seq::empty(), { Vec::new() }}
impl<'a, T: ObeysDeepEq + DeepViewClone + std::hash::Hash + std::cmp::Eq> ExecSpecSeqToMultiset< 'a,> for &'a [T] { type Elem = T;
#[verifier::external_body] #[inline(always)] fn exec_to_multiset(self) -> (res: ExecMultiset<Self::Elem>) ensures res.deep_view() =~= self.deep_view().to_multiset(), { let mut mset = ExecMultiset { m: HashMap::new() }; for e in self.iter() { match mset.m.remove_entry(e) { Some((k, c)) => { mset.m.insert(k, c + 1); }, None => { mset.m.insert(e.deep_clone(), 1); }, } } mset }}
impl<'a, T: DeepView> ExecSpecSeqDropFirst<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_drop_first(self) -> (res: Self) ensures res.deep_view() =~= self.deep_view().drop_first(), { self.exec_subrange(1, self.exec_len()) }}
impl<'a, T: DeepView> ExecSpecSeqDropLast<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_drop_last(self) -> (res: Self) ensures res.deep_view() =~= self.deep_view().drop_last(), { self.exec_subrange(0, self.exec_len() - 1) }}
impl<'a, T: DeepView> ExecSpecSeqTake<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_take(self, n: usize) -> (res: Self) ensures res.deep_view() =~= self.deep_view()[..n], { self.exec_subrange(0, n) }}
impl<'a, T: DeepView> ExecSpecSeqSkip<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_skip(self, n: usize) -> (res: Self) ensures res.deep_view() =~= self.deep_view()[n..], { self.exec_subrange(n, self.exec_len()) }}
impl<'a, T: DeepView> ExecSpecSeqLast<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_last(self) -> (res: Self::Elem) ensures res.deep_view() == self.deep_view().last(), { &self.exec_index(self.len() - 1) }}
impl<'a, T: DeepView> ExecSpecSeqFirst<'a> for &'a [T] { type Elem = &'a T;
#[inline(always)] fn exec_first(self) -> (res: Self::Elem) ensures res.deep_view() == self.deep_view().first(), { &self.exec_index(0) }}
impl<'a, T: ObeysDeepEq> ExecSpecSeqIsPrefixOf<'a> for &'a [T] where &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>, { type Other = &'a [T];
#[inline(always)] fn exec_is_prefix_of(self, other: Self::Other) -> (res: bool) ensures res == self.deep_view().is_prefix_of(other.deep_view()), { self.exec_len() <= other.exec_len() && deep_eq( self, other.exec_subrange(0, self.exec_len()), ) }}
impl<'a, T: ObeysDeepEq> ExecSpecSeqIsSuffixOf<'a> for &'a [T] where &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>, { type Other = &'a [T];
#[inline(always)] fn exec_is_suffix_of(self, other: Self::Other) -> (res: bool) ensures res == self.deep_view().is_suffix_of(other.deep_view()), { self.exec_len() <= other.exec_len() && deep_eq( self, other.exec_subrange(other.exec_len() - self.exec_len(), other.exec_len()), ) }}
impl<'a, T: ObeysDeepEq> ExecSpecSeqContains<'a> for &'a [T] { type Elem = T;
#[verifier::external_body] #[inline(always)] fn exec_contains(self, needle: Self::Elem) -> (res: bool) ensures res == self.deep_view().contains(needle.deep_view()), { self.contains(&needle) }}
impl<'a, T: ObeysDeepEq> ExecSpecSeqIndexOf<'a> for &'a [T] { type Elem = T;
// hard to verify - index_of contains a choose operator #[verifier::external_body] #[inline(always)] fn exec_index_of(self, needle: Self::Elem) -> (res: usize) ensures res == self.deep_view().index_of(needle.deep_view()), { for i in 0..self.exec_len() { if self[i] == needle { return i; } } self.exec_len() }}
impl<'a, T: ObeysDeepEq> ExecSpecSeqIndexOfFirst<'a> for &'a [T] { type Elem = T;
#[verifier::external_body] fn exec_index_of_first(self, needle: Self::Elem) -> (res: Option<usize>) ensures match res { Some(i) => self.deep_view().index_of_first(needle.deep_view()).is_some() && i as int == self.deep_view().index_of_first(needle.deep_view())->0, None => self.deep_view().index_of_first(needle.deep_view()) == None::<int>, }, { for i in 0..self.exec_len() { if self[i] == needle { return Some(i); } } None }}
impl<'a, T: ObeysDeepEq> ExecSpecSeqIndexOfLast<'a> for &'a [T] { type Elem = T;
#[verifier::external_body] #[inline(always)] fn exec_index_of_last(self, needle: Self::Elem) -> (res: Option<usize>) ensures match res { Some(i) => self.deep_view().index_of_last(needle.deep_view()).is_some() && i as int == self.deep_view().index_of_last(needle.deep_view())->0, None => self.deep_view().index_of_last(needle.deep_view()) == None::<int>, }, { for i in (0..self.exec_len()).rev() { if self[i] == needle { return Some(i); } } None }}
} // verus!