Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364use super::prelude::*;
verus! {
/// Types used in executable code can implement View to provide a mathematical abstraction/// of the type./// For example, Vec implements a view method that returns a Seq./// For base types like bool and u8, the view V of the type is the type itself./// Types only used in ghost code, such as int, nat, and Seq, do not need to implement View.pub trait View { type V;
spec fn view(&self) -> Self::V;}
pub trait DeepView { type V;
spec fn deep_view(&self) -> Self::V;}
impl<A: View + ?Sized> View for &A { type V = A::V;
#[verifier::inline] open spec fn view(&self) -> A::V { (**self).view() }}
impl<A: DeepView + ?Sized> DeepView for &A { type V = A::V;
#[verifier::inline] open spec fn deep_view(&self) -> A::V { (**self).deep_view() }}
#[cfg(feature = "alloc")]impl<A: View + ?Sized> View for alloc::boxed::Box<A> { type V = A::V;
#[verifier::inline] open spec fn view(&self) -> A::V { (**self).view() }}
#[cfg(feature = "alloc")]impl<A: DeepView + ?Sized> DeepView for alloc::boxed::Box<A> { type V = A::V;
#[verifier::inline] open spec fn deep_view(&self) -> A::V { (**self).deep_view() }}
#[cfg(feature = "alloc")]impl<A: View> View for alloc::rc::Rc<A> { type V = A::V;
#[verifier::inline] open spec fn view(&self) -> A::V { (**self).view() }}
#[cfg(feature = "alloc")]impl<A: DeepView> DeepView for alloc::rc::Rc<A> { type V = A::V;
#[verifier::inline] open spec fn deep_view(&self) -> A::V { (**self).deep_view() }}
#[cfg(feature = "alloc")]impl<A: View> View for alloc::sync::Arc<A> { type V = A::V;
#[verifier::inline] open spec fn view(&self) -> A::V { (**self).view() }}
#[cfg(feature = "alloc")]impl<A: DeepView> DeepView for alloc::sync::Arc<A> { type V = A::V;
#[verifier::inline] open spec fn deep_view(&self) -> A::V { (**self).deep_view() }}
// Note: the view for Vec is declared here, not in std_specs/vec.rs,// because "pub mod std_specs" is marked #[cfg(verus_keep_ghost)]// and we want to keep the View impl regardless of verus_keep_ghost.#[cfg(all(feature = "alloc", any(verus_keep_ghost, feature = "allocator")))]impl<T, A: core::alloc::Allocator> View for alloc::vec::Vec<T, A> { type V = Seq<T>;
uninterp spec fn view(&self) -> Seq<T>;}
#[cfg(all(feature = "alloc", any(verus_keep_ghost, feature = "allocator")))]impl<T: DeepView, A: core::alloc::Allocator> DeepView for alloc::vec::Vec<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()) }}
#[cfg(all(feature = "alloc", not(verus_keep_ghost), not(feature = "allocator")))]impl<T> View for alloc::vec::Vec<T> { type V = Seq<T>;
uninterp spec fn view(&self) -> Seq<T>;}
#[cfg(all(feature = "alloc", not(verus_keep_ghost), not(feature = "allocator")))]impl<T: DeepView> DeepView for alloc::vec::Vec<T> { 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()) }}
#[cfg(all(feature = "alloc", feature = "std", any(verus_keep_ghost, feature = "allocator")))]impl<Key, Value, S, A: core::alloc::Allocator> View for std::collections::HashMap< Key, Value, S, A,> { type V = Map<Key, Value>;
uninterp spec fn view(&self) -> Map<Key, Value>;}
#[cfg(all(feature = "alloc", feature = "std", any(verus_keep_ghost, feature = "allocator")))]impl< Key: DeepView, Value: DeepView, S, A: core::alloc::Allocator,> DeepView for std::collections::HashMap<Key, Value, S, A> { type V = Map<Key::V, Value::V>;
open spec fn deep_view(&self) -> Map<Key::V, Value::V> { crate::std_specs::hash::hash_map_deep_view_impl(*self) }}
#[cfg(all(feature = "alloc", feature = "std", not(verus_keep_ghost), not(feature = "allocator")))]impl<Key, Value, S> View for std::collections::HashMap<Key, Value, S> { type V = Map<Key, Value>;
uninterp spec fn view(&self) -> Map<Key, Value>;}
#[cfg(all(feature = "alloc", feature = "std", not(verus_keep_ghost), not(feature = "allocator")))]impl<Key: DeepView, Value: DeepView, S> DeepView for std::collections::HashMap<Key, Value, S> { type V = Map<Key::V, Value::V>;
open spec fn deep_view(&self) -> Map<Key::V, Value::V> { crate::std_specs::hash::hash_map_deep_view_impl(*self) }}
#[cfg(all(feature = "alloc", feature = "std", any(verus_keep_ghost, feature = "allocator")))]impl<Key, S, A: core::alloc::Allocator> View for std::collections::HashSet<Key, S, A> { type V = Set<Key>;
uninterp spec fn view(&self) -> Set<Key>;}
#[cfg(all(feature = "alloc", feature = "std", any(verus_keep_ghost, feature = "allocator")))]impl<Key: DeepView, S, A: core::alloc::Allocator> DeepView for std::collections::HashSet< Key, S, A,> { type V = Set<Key::V>;
open spec fn deep_view(&self) -> Set<Key::V> { self@.map(|x: Key| x.deep_view()) }}
#[cfg(all(feature = "alloc", feature = "std", not(verus_keep_ghost), not(feature = "allocator")))]impl<Key, S> View for std::collections::HashSet<Key, S> { type V = Set<Key>;
uninterp spec fn view(&self) -> Set<Key>;}
#[cfg(all(feature = "alloc", feature = "std", not(verus_keep_ghost), not(feature = "allocator")))]impl<Key: DeepView, S> DeepView for std::collections::HashSet<Key, S> { type V = Set<Key::V>;
open spec fn deep_view(&self) -> Set<Key::V> { self@.map(|x: Key| x.deep_view()) }}
impl<T> View for Option<T> { type V = Option<T>;
open spec fn view(&self) -> Option<T> { *self }}
impl<T: DeepView> DeepView for Option<T> { type V = Option<T::V>;
open spec fn deep_view(&self) -> Option<T::V> { match self { Some(t) => Some(t.deep_view()), None => None, } }}
impl<T, E> View for Result<T, E> { type V = Result<T, E>;
open spec fn view(&self) -> Result<T, E> { *self }}
impl<T: DeepView, E: DeepView> DeepView for Result<T, E> { type V = Result<T::V, E::V>;
open spec fn deep_view(&self) -> Result<T::V, E::V> { match self { Ok(t) => Ok(t.deep_view()), Err(e) => Err(e.deep_view()), } }}
macro_rules! declare_identity_view { ($t:ty) => { #[cfg_attr(verus_keep_ghost, verus::internal(verify))] impl View for $t { type V = $t;
#[cfg(verus_keep_ghost)] #[verus::internal(spec)] #[verus::internal(open)] #[verifier::inline] fn view(&self) -> $t { *self } }
#[cfg_attr(verus_keep_ghost, verus::internal(verify))] impl DeepView for $t { type V = $t;
#[cfg(verus_keep_ghost)] #[verus::internal(spec)] #[verus::internal(open)] #[verifier::inline] fn deep_view(&self) -> $t { *self } } }}
declare_identity_view!(());
declare_identity_view!(bool);
declare_identity_view!(u8);
declare_identity_view!(u16);
declare_identity_view!(u32);
declare_identity_view!(u64);
declare_identity_view!(u128);
declare_identity_view!(usize);
declare_identity_view!(i8);
declare_identity_view!(i16);
declare_identity_view!(i32);
declare_identity_view!(i64);
declare_identity_view!(i128);
declare_identity_view!(isize);
declare_identity_view!(char);
macro_rules! declare_tuple_view { ([$($n:tt)*], [$($a:ident)*]) => { #[cfg_attr(verus_keep_ghost, verus::internal(verify))] impl<$($a: View, )*> View for ($($a, )*) { type V = ($($a::V, )*); #[cfg(verus_keep_ghost)] #[verus::internal(spec)] #[verus::internal(open)] fn view(&self) -> ($($a::V, )*) { ($(self.$n.view(), )*) } }
#[cfg_attr(verus_keep_ghost, verus::internal(verify))] impl<$($a: DeepView, )*> DeepView for ($($a, )*) { type V = ($($a::V, )*); #[cfg(verus_keep_ghost)] #[verus::internal(spec)] #[verus::internal(open)] fn deep_view(&self) -> ($($a::V, )*) { ($(self.$n.deep_view(), )*) } } }}
declare_tuple_view!([0], [A0]);
declare_tuple_view!([0 1], [A0 A1]);
declare_tuple_view!([0 1 2], [A0 A1 A2]);
declare_tuple_view!([0 1 2 3], [A0 A1 A2 A3]);
declare_tuple_view!([0 1 2 3 4], [A0 A1 A2 A3 A4]);
declare_tuple_view!([0 1 2 3 4 5], [A0 A1 A2 A3 A4 A5]);
declare_tuple_view!([0 1 2 3 4 5 6], [A0 A1 A2 A3 A4 A5 A6]);
declare_tuple_view!([0 1 2 3 4 5 6 7], [A0 A1 A2 A3 A4 A5 A6 A7]);
declare_tuple_view!([0 1 2 3 4 5 6 7 8], [A0 A1 A2 A3 A4 A5 A6 A7 A8]);
declare_tuple_view!([0 1 2 3 4 5 6 7 8 9], [A0 A1 A2 A3 A4 A5 A6 A7 A8 A9]);
declare_tuple_view!([0 1 2 3 4 5 6 7 8 9 10], [A0 A1 A2 A3 A4 A5 A6 A7 A8 A9 A10]);
declare_tuple_view!([0 1 2 3 4 5 6 7 8 9 10 11], [A0 A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11]);
} // verus!