vstd/
view.rs

1use super::prelude::*;
2
3verus! {
4
5/// Types used in executable code can implement View to provide a mathematical abstraction
6/// of the type.
7/// For example, Vec implements a view method that returns a Seq.
8/// For base types like bool and u8, the view V of the type is the type itself.
9/// Types only used in ghost code, such as int, nat, and Seq, do not need to implement View.
10pub trait View {
11    type V;
12
13    spec fn view(&self) -> Self::V;
14}
15
16pub trait DeepView {
17    type V;
18
19    spec fn deep_view(&self) -> Self::V;
20}
21
22impl<A: View + ?Sized> View for &A {
23    type V = A::V;
24
25    #[verifier::inline]
26    open spec fn view(&self) -> A::V {
27        (**self).view()
28    }
29}
30
31impl<A: DeepView + ?Sized> DeepView for &A {
32    type V = A::V;
33
34    #[verifier::inline]
35    open spec fn deep_view(&self) -> A::V {
36        (**self).deep_view()
37    }
38}
39
40#[cfg(feature = "alloc")]
41impl<A: View + ?Sized> View for alloc::boxed::Box<A> {
42    type V = A::V;
43
44    #[verifier::inline]
45    open spec fn view(&self) -> A::V {
46        (**self).view()
47    }
48}
49
50#[cfg(feature = "alloc")]
51impl<A: DeepView + ?Sized> DeepView for alloc::boxed::Box<A> {
52    type V = A::V;
53
54    #[verifier::inline]
55    open spec fn deep_view(&self) -> A::V {
56        (**self).deep_view()
57    }
58}
59
60#[cfg(feature = "alloc")]
61impl<A: View> View for alloc::rc::Rc<A> {
62    type V = A::V;
63
64    #[verifier::inline]
65    open spec fn view(&self) -> A::V {
66        (**self).view()
67    }
68}
69
70#[cfg(feature = "alloc")]
71impl<A: DeepView> DeepView for alloc::rc::Rc<A> {
72    type V = A::V;
73
74    #[verifier::inline]
75    open spec fn deep_view(&self) -> A::V {
76        (**self).deep_view()
77    }
78}
79
80#[cfg(feature = "alloc")]
81impl<A: View> View for alloc::sync::Arc<A> {
82    type V = A::V;
83
84    #[verifier::inline]
85    open spec fn view(&self) -> A::V {
86        (**self).view()
87    }
88}
89
90#[cfg(feature = "alloc")]
91impl<A: DeepView> DeepView for alloc::sync::Arc<A> {
92    type V = A::V;
93
94    #[verifier::inline]
95    open spec fn deep_view(&self) -> A::V {
96        (**self).deep_view()
97    }
98}
99
100// Note: the view for Vec is declared here, not in std_specs/vec.rs,
101// because "pub mod std_specs" is marked #[cfg(verus_keep_ghost)]
102// and we want to keep the View impl regardless of verus_keep_ghost.
103#[cfg(all(feature = "alloc", any(verus_keep_ghost, feature = "allocator")))]
104impl<T, A: core::alloc::Allocator> View for alloc::vec::Vec<T, A> {
105    type V = Seq<T>;
106
107    uninterp spec fn view(&self) -> Seq<T>;
108}
109
110#[cfg(all(feature = "alloc", any(verus_keep_ghost, feature = "allocator")))]
111impl<T: DeepView, A: core::alloc::Allocator> DeepView for alloc::vec::Vec<T, A> {
112    type V = Seq<T::V>;
113
114    open spec fn deep_view(&self) -> Seq<T::V> {
115        let v = self.view();
116        Seq::new(v.len(), |i: int| v[i].deep_view())
117    }
118}
119
120#[cfg(all(feature = "alloc", not(verus_keep_ghost), not(feature = "allocator")))]
121impl<T> View for alloc::vec::Vec<T> {
122    type V = Seq<T>;
123
124    uninterp spec fn view(&self) -> Seq<T>;
125}
126
127#[cfg(all(feature = "alloc", not(verus_keep_ghost), not(feature = "allocator")))]
128impl<T: DeepView> DeepView for alloc::vec::Vec<T> {
129    type V = Seq<T::V>;
130
131    open spec fn deep_view(&self) -> Seq<T::V> {
132        let v = self.view();
133        Seq::new(v.len(), |i: int| v[i].deep_view())
134    }
135}
136
137impl<T> View for Option<T> {
138    type V = Option<T>;
139
140    open spec fn view(&self) -> Option<T> {
141        *self
142    }
143}
144
145impl<T: DeepView> DeepView for Option<T> {
146    type V = Option<T::V>;
147
148    open spec fn deep_view(&self) -> Option<T::V> {
149        match self {
150            Some(t) => Some(t.deep_view()),
151            None => None,
152        }
153    }
154}
155
156macro_rules! declare_identity_view {
157    ($t:ty) => {
158        #[cfg_attr(verus_keep_ghost, verifier::verify)]
159        impl View for $t {
160            type V = $t;
161
162            #[cfg(verus_keep_ghost)]
163            #[verus::internal(spec)]
164            #[verus::internal(open)]
165            #[verifier::inline]
166            fn view(&self) -> $t {
167                *self
168            }
169        }
170
171        #[cfg_attr(verus_keep_ghost, verifier::verify)]
172        impl DeepView for $t {
173            type V = $t;
174
175            #[cfg(verus_keep_ghost)]
176            #[verus::internal(spec)]
177            #[verus::internal(open)]
178            #[verifier::inline]
179            fn deep_view(&self) -> $t {
180                *self
181            }
182        }
183    }
184}
185
186declare_identity_view!(());
187
188declare_identity_view!(bool);
189
190declare_identity_view!(u8);
191
192declare_identity_view!(u16);
193
194declare_identity_view!(u32);
195
196declare_identity_view!(u64);
197
198declare_identity_view!(u128);
199
200declare_identity_view!(usize);
201
202declare_identity_view!(i8);
203
204declare_identity_view!(i16);
205
206declare_identity_view!(i32);
207
208declare_identity_view!(i64);
209
210declare_identity_view!(i128);
211
212declare_identity_view!(isize);
213
214declare_identity_view!(char);
215
216macro_rules! declare_tuple_view {
217    ([$($n:tt)*], [$($a:ident)*]) => {
218        #[cfg_attr(verus_keep_ghost, verifier::verify)]
219        impl<$($a: View, )*> View for ($($a, )*) {
220            type V = ($($a::V, )*);
221            #[cfg(verus_keep_ghost)]
222            #[verus::internal(spec)]
223            #[verus::internal(open)]
224            fn view(&self) -> ($($a::V, )*) {
225                ($(self.$n.view(), )*)
226            }
227        }
228
229        #[cfg_attr(verus_keep_ghost, verifier::verify)]
230        impl<$($a: DeepView, )*> DeepView for ($($a, )*) {
231            type V = ($($a::V, )*);
232            #[cfg(verus_keep_ghost)]
233            #[verus::internal(spec)]
234            #[verus::internal(open)]
235            fn deep_view(&self) -> ($($a::V, )*) {
236                ($(self.$n.deep_view(), )*)
237            }
238        }
239    }
240}
241
242// REVIEW: we can declare more, but let's check the vstd size and overhead first
243declare_tuple_view!([0], [A0]);
244
245declare_tuple_view!([0 1], [A0 A1]);
246
247declare_tuple_view!([0 1 2], [A0 A1 A2]);
248
249declare_tuple_view!([0 1 2 3], [A0 A1 A2 A3]);
250
251} // verus!
vstd/view.rs

vstd/
view.rs
