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

vstd/
view.rs
