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
137#[cfg(all(feature = "std"))]
138impl<Key, Value, S> View for std::collections::HashMap<Key, Value, S> {
139    type V = Map<Key, Value>;
140
141    uninterp spec fn view(&self) -> Map<Key, Value>;
142}
143
144#[cfg(all(feature = "std"))]
145impl<Key: DeepView, Value: DeepView, S> DeepView for std::collections::HashMap<Key, Value, S> {
146    type V = Map<Key::V, Value::V>;
147
148    open spec fn deep_view(&self) -> Map<Key::V, Value::V> {
149        crate::std_specs::hash::hash_map_deep_view_impl(*self)
150    }
151}
152
153#[cfg(all(feature = "std"))]
154impl<Key, S> View for std::collections::HashSet<Key, S> {
155    type V = Set<Key>;
156
157    uninterp spec fn view(&self) -> Set<Key>;
158}
159
160#[cfg(all(feature = "std"))]
161impl<Key: DeepView, S> DeepView for std::collections::HashSet<Key, S> {
162    type V = Set<Key::V>;
163
164    open spec fn deep_view(&self) -> Set<Key::V> {
165        self@.map(|x: Key| x.deep_view())
166    }
167}
168
169impl<T> View for Option<T> {
170    type V = Option<T>;
171
172    open spec fn view(&self) -> Option<T> {
173        *self
174    }
175}
176
177impl<T: DeepView> DeepView for Option<T> {
178    type V = Option<T::V>;
179
180    open spec fn deep_view(&self) -> Option<T::V> {
181        match self {
182            Some(t) => Some(t.deep_view()),
183            None => None,
184        }
185    }
186}
187
188macro_rules! declare_identity_view {
189    ($t:ty) => {
190        #[cfg_attr(verus_keep_ghost, verifier::verify)]
191        impl View for $t {
192            type V = $t;
193
194            #[cfg(verus_keep_ghost)]
195            #[verus::internal(spec)]
196            #[verus::internal(open)]
197            #[verifier::inline]
198            fn view(&self) -> $t {
199                *self
200            }
201        }
202
203        #[cfg_attr(verus_keep_ghost, verifier::verify)]
204        impl DeepView for $t {
205            type V = $t;
206
207            #[cfg(verus_keep_ghost)]
208            #[verus::internal(spec)]
209            #[verus::internal(open)]
210            #[verifier::inline]
211            fn deep_view(&self) -> $t {
212                *self
213            }
214        }
215    }
216}
217
218declare_identity_view!(());
219
220declare_identity_view!(bool);
221
222declare_identity_view!(u8);
223
224declare_identity_view!(u16);
225
226declare_identity_view!(u32);
227
228declare_identity_view!(u64);
229
230declare_identity_view!(u128);
231
232declare_identity_view!(usize);
233
234declare_identity_view!(i8);
235
236declare_identity_view!(i16);
237
238declare_identity_view!(i32);
239
240declare_identity_view!(i64);
241
242declare_identity_view!(i128);
243
244declare_identity_view!(isize);
245
246declare_identity_view!(char);
247
248macro_rules! declare_tuple_view {
249    ([$($n:tt)*], [$($a:ident)*]) => {
250        #[cfg_attr(verus_keep_ghost, verifier::verify)]
251        impl<$($a: View, )*> View for ($($a, )*) {
252            type V = ($($a::V, )*);
253            #[cfg(verus_keep_ghost)]
254            #[verus::internal(spec)]
255            #[verus::internal(open)]
256            fn view(&self) -> ($($a::V, )*) {
257                ($(self.$n.view(), )*)
258            }
259        }
260
261        #[cfg_attr(verus_keep_ghost, verifier::verify)]
262        impl<$($a: DeepView, )*> DeepView for ($($a, )*) {
263            type V = ($($a::V, )*);
264            #[cfg(verus_keep_ghost)]
265            #[verus::internal(spec)]
266            #[verus::internal(open)]
267            fn deep_view(&self) -> ($($a::V, )*) {
268                ($(self.$n.deep_view(), )*)
269            }
270        }
271    }
272}
273
274// REVIEW: we can declare more, but let's check the vstd size and overhead first
275declare_tuple_view!([0], [A0]);
276
277declare_tuple_view!([0 1], [A0 A1]);
278
279declare_tuple_view!([0 1 2], [A0 A1 A2]);
280
281declare_tuple_view!([0 1 2 3], [A0 A1 A2 A3]);
282
283} // verus!
vstd/view.rs

vstd/
view.rs
