vstd_extra/external/
deref.rs

1use core::hint::spin_loop;
2use core::mem::ManuallyDrop;
3use core::ops::Deref;
4use vstd::prelude::*;
5
6// Assumptions about external functions
7
8verus! {
9
10/// This is a workaround to add an uninterpreted specification of Deref trait, as Deref is included in Verus but does not have spec functions.
11/// It may change if Verus adds native support for spec functions in the Deref trait.
12pub trait DerefSpec: Deref {
13    spec fn deref_spec(&self) -> &<Self as Deref>::Target;
14
15    proof fn deref_spec_eq(&self)
16        ensures
17            forall|output|
18                call_ensures(Self::deref, (self,), output) ==> self.deref_spec() == output,
19    ;
20}
21
22impl<T: Deref> DerefSpec for T {
23    uninterp spec fn deref_spec(&self) -> &<Self as Deref>::Target;
24
25    axiom fn deref_spec_eq(&self);
26}
27
28// Special Cases
29pub broadcast axiom fn ref_deref_spec<T>(r: &T)
30    ensures
31        #[trigger] *(r.deref_spec()) == *r,
32;
33
34pub broadcast axiom fn box_deref_spec<T>(b: Box<T>)
35    ensures
36        #[trigger] *(b.deref_spec()) == *b,
37;
38
39pub broadcast axiom fn rc_deref_spec<T>(r: std::rc::Rc<T>)
40    ensures
41        #[trigger] *(r.deref_spec()) == *r,
42;
43
44pub broadcast axiom fn arc_deref_spec<T>(a: std::sync::Arc<T>)
45    ensures
46        #[trigger] *(a.deref_spec()) == *a,
47;
48
49pub broadcast group group_deref_spec {
50    ref_deref_spec,
51    box_deref_spec,
52    rc_deref_spec,
53    arc_deref_spec,
54}
55
56} // verus!
vstd_extra/external/deref.rs

vstd_extra/external/
deref.rs
