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
234impl<T, E> View for Result<T, E> {
235    type V = Result<T, E>;
236
237    open spec fn view(&self) -> Result<T, E> {
238        *self
239    }
240}
241
242impl<T: DeepView, E: DeepView> DeepView for Result<T, E> {
243    type V = Result<T::V, E::V>;
244
245    open spec fn deep_view(&self) -> Result<T::V, E::V> {
246        match self {
247            Ok(t) => Ok(t.deep_view()),
248            Err(e) => Err(e.deep_view()),
249        }
250    }
251}
252
253macro_rules! declare_identity_view {
254    ($t:ty) => {
255        #[cfg_attr(verus_keep_ghost, verifier::verify)]
256        impl View for $t {
257            type V = $t;
258
259            #[cfg(verus_keep_ghost)]
260            #[verus::internal(spec)]
261            #[verus::internal(open)]
262            #[verifier::inline]
263            fn view(&self) -> $t {
264                *self
265            }
266        }
267
268        #[cfg_attr(verus_keep_ghost, verifier::verify)]
269        impl DeepView for $t {
270            type V = $t;
271
272            #[cfg(verus_keep_ghost)]
273            #[verus::internal(spec)]
274            #[verus::internal(open)]
275            #[verifier::inline]
276            fn deep_view(&self) -> $t {
277                *self
278            }
279        }
280    }
281}
282
283declare_identity_view!(());
284
285declare_identity_view!(bool);
286
287declare_identity_view!(u8);
288
289declare_identity_view!(u16);
290
291declare_identity_view!(u32);
292
293declare_identity_view!(u64);
294
295declare_identity_view!(u128);
296
297declare_identity_view!(usize);
298
299declare_identity_view!(i8);
300
301declare_identity_view!(i16);
302
303declare_identity_view!(i32);
304
305declare_identity_view!(i64);
306
307declare_identity_view!(i128);
308
309declare_identity_view!(isize);
310
311declare_identity_view!(char);
312
313macro_rules! declare_tuple_view {
314    ([$($n:tt)*], [$($a:ident)*]) => {
315        #[cfg_attr(verus_keep_ghost, verifier::verify)]
316        impl<$($a: View, )*> View for ($($a, )*) {
317            type V = ($($a::V, )*);
318            #[cfg(verus_keep_ghost)]
319            #[verus::internal(spec)]
320            #[verus::internal(open)]
321            fn view(&self) -> ($($a::V, )*) {
322                ($(self.$n.view(), )*)
323            }
324        }
325
326        #[cfg_attr(verus_keep_ghost, verifier::verify)]
327        impl<$($a: DeepView, )*> DeepView for ($($a, )*) {
328            type V = ($($a::V, )*);
329            #[cfg(verus_keep_ghost)]
330            #[verus::internal(spec)]
331            #[verus::internal(open)]
332            fn deep_view(&self) -> ($($a::V, )*) {
333                ($(self.$n.deep_view(), )*)
334            }
335        }
336    }
337}
338
339declare_tuple_view!([0], [A0]);
340
341declare_tuple_view!([0 1], [A0 A1]);
342
343declare_tuple_view!([0 1 2], [A0 A1 A2]);
344
345declare_tuple_view!([0 1 2 3], [A0 A1 A2 A3]);
346
347declare_tuple_view!([0 1 2 3 4], [A0 A1 A2 A3 A4]);
348
349declare_tuple_view!([0 1 2 3 4 5], [A0 A1 A2 A3 A4 A5]);
350
351declare_tuple_view!([0 1 2 3 4 5 6], [A0 A1 A2 A3 A4 A5 A6]);
352
353declare_tuple_view!([0 1 2 3 4 5 6 7], [A0 A1 A2 A3 A4 A5 A6 A7]);
354
355declare_tuple_view!([0 1 2 3 4 5 6 7 8], [A0 A1 A2 A3 A4 A5 A6 A7 A8]);
356
357declare_tuple_view!([0 1 2 3 4 5 6 7 8 9], [A0 A1 A2 A3 A4 A5 A6 A7 A8 A9]);
358
359declare_tuple_view!([0 1 2 3 4 5 6 7 8 9 10], [A0 A1 A2 A3 A4 A5 A6 A7 A8 A9 A10]);
360
361declare_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]);
362
363} // verus!
vstd/view.rs

vstd/
view.rs
