vstd_extra/
cast_ptr.rs

1use vstd::prelude::*;
2
3use vstd::layout;
4use vstd::raw_ptr::MemContents;
5use vstd::set;
6use vstd::set_lib;
7use vstd::simple_pptr::{self, PPtr};
8
9use core::marker::PhantomData;
10use core::ops::Deref;
11
12verus! {
13
14pub trait Repr<R: Sized>: Sized {
15    /// If the underlying representation contains cells, the translation may require permission objects that access them.
16    type Perm;
17
18    spec fn wf(r: R, perm: Self::Perm) -> bool;
19
20    spec fn to_repr_spec(self, perm: Self::Perm) -> (R, Self::Perm);
21
22    fn to_repr(self, Tracked(perm): Tracked<&mut Self::Perm>) -> (res: R)
23        ensures
24            res == self.to_repr_spec(*old(perm)).0,
25            *perm == self.to_repr_spec(*old(perm)).1,
26    ;
27
28    spec fn from_repr_spec(r: R, perm: Self::Perm) -> Self;
29
30    fn from_repr(r: R, Tracked(perm): Tracked<&Self::Perm>) -> (res: Self)
31        requires
32            Self::wf(r, *perm),
33        ensures
34            res == Self::from_repr_spec(r, *perm),
35    ;
36
37    fn from_borrowed<'a>(r: &'a R, Tracked(perm): Tracked<&'a Self::Perm>) -> (res: &'a Self)
38        requires
39            Self::wf(*r, *perm),
40        ensures
41            *res == Self::from_repr_spec(*r, *perm),
42    ;
43
44    proof fn from_to_repr(self, perm: Self::Perm)
45        ensures
46            Self::from_repr_spec(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1) == self,
47    ;
48
49    proof fn to_from_repr(r: R, perm: Self::Perm)
50        requires
51            Self::wf(r, perm),
52        ensures
53            Self::from_repr_spec(r, perm).to_repr_spec(perm) == (r, perm),
54    ;
55
56    proof fn to_repr_wf(self, perm: Self::Perm)
57        ensures
58            Self::wf(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1),
59    ;
60}
61
62/// Concrete representation of a pointer to an object of type T with representation type R
63/// The length of the array is not stored in the pointer
64pub struct ReprPtr<R, T: Repr<R>> {
65    pub addr: usize,
66    pub ptr: PPtr<R>,
67    pub _T: PhantomData<T>,
68}
69
70impl<R, T: Repr<R>> Clone for ReprPtr<R, T> {
71    fn clone(&self) -> Self {
72        Self { addr: self.addr, ptr: self.ptr, _T: PhantomData }
73    }
74}
75
76impl<R, T: Repr<R>> Copy for ReprPtr<R, T> {
77
78}
79
80impl<R, T: Repr<R>> From<PPtr<R>> for ReprPtr<R, T> {
81    #[verifier::external_body]
82    fn from(ptr: PPtr<R>) -> Self {
83        Self { addr: ptr.addr(), ptr: ptr, _T: PhantomData }
84    }
85}
86
87impl<R, T: Repr<R>> From<ReprPtr<R, T>> for PPtr<R> {
88    #[verifier::external_body]
89    fn from(ptr: ReprPtr<R, T>) -> Self {
90        ptr.ptr
91    }
92}
93
94impl<R, T: Repr<R>> ReprPtr<R, T> {
95    pub open spec fn new_spec(ptr: PPtr<R>) -> Self {
96        Self { addr: ptr.addr(), ptr: ptr, _T: PhantomData }
97    }
98
99    #[verifier::external_body]
100    pub fn new_borrowed<'a>(ptr: &'a PPtr<R>) -> (res: &'a Self)
101        ensures
102            *res == Self::new_spec(*ptr),
103    {
104        unimplemented!()
105    }
106
107    pub fn from_pptr(ptr: PPtr<R>) -> (res: Self)
108        ensures
109            res == Self::new_spec(ptr),
110            res.addr == ptr.addr(),
111            res.ptr == ptr,
112    {
113        Self { addr: ptr.addr(), ptr: ptr, _T: PhantomData }
114    }
115
116    pub open spec fn to_pptr(self) -> PPtr<R> {
117        self.ptr
118    }
119
120    pub open spec fn addr_spec(self) -> usize {
121        self.addr
122    }
123
124    #[verifier::when_used_as_spec(addr_spec)]
125    pub fn addr(self) -> (u: usize)
126        ensures
127            u == self.addr,
128    {
129        self.addr
130    }
131
132    pub exec fn take(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>) -> (v: T)
133        requires
134            old(perm).pptr() == self,
135            old(perm).is_init(),
136            old(perm).wf(&old(perm).inner_perms),
137        ensures
138            perm.pptr() == old(perm).pptr(),
139            perm.mem_contents() == MemContents::Uninit::<T>,
140            v == old(perm).value(),
141    {
142        proof {
143            T::from_to_repr(perm.value(), perm.inner_perms);
144        }
145        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)), Tracked(&perm.inner_perms))
146    }
147
148    pub exec fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
149        requires
150            old(perm).pptr() == self,
151            old(perm).mem_contents() == MemContents::Uninit::<T>,
152        ensures
153            perm.pptr() == old(perm).pptr(),
154            perm.mem_contents() == MemContents::Init(v),
155            perm.wf(&perm.inner_perms),
156    {
157        proof {
158            v.from_to_repr(perm.inner_perms);
159            v.to_repr_wf(perm.inner_perms);
160        }
161        self.ptr.put(Tracked(&mut perm.points_to), v.to_repr(Tracked(&mut perm.inner_perms)))
162    }
163
164    pub exec fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<R, T>>) -> (v: &'a T)
165        requires
166            perm.pptr() == self,
167            perm.is_init(),
168            perm.wf(&perm.inner_perms),
169        ensures
170            *v === perm.value(),
171    {
172        T::from_borrowed(self.ptr.borrow(Tracked(&perm.points_to)), Tracked(&perm.inner_perms))
173    }
174}
175
176#[verifier::accept_recursive_types(T)]
177pub tracked struct PointsTo<R, T: Repr<R>> {
178    pub ghost addr: usize,
179    pub points_to: simple_pptr::PointsTo<R>,
180    pub inner_perms: T::Perm,
181    pub _T: PhantomData<T>,
182}
183
184impl<R, T: Repr<R>> PointsTo<R, T> {
185    pub open spec fn new_spec(
186        addr: usize,
187        points_to: simple_pptr::PointsTo<R>,
188        inner_perms: T::Perm,
189    ) -> Self {
190        Self { addr: addr@, points_to, inner_perms, _T: PhantomData }
191    }
192
193    pub proof fn new(
194        addr: Ghost<usize>,
195        tracked points_to: simple_pptr::PointsTo<R>,
196        tracked inner_perms: T::Perm,
197    ) -> tracked Self {
198        Self { addr: addr@, points_to: points_to, inner_perms, _T: PhantomData }
199    }
200
201    pub open spec fn wf(self, perm: &T::Perm) -> bool {
202        &&& T::wf(self.points_to.value(), *perm)
203    }
204
205    pub open spec fn addr(self) -> usize {
206        self.addr
207    }
208
209    pub open spec fn mem_contents(self) -> MemContents<T> {
210        match self.points_to.mem_contents() {
211            MemContents::<R>::Uninit => MemContents::<T>::Uninit,
212            MemContents::<R>::Init(r) => MemContents::<T>::Init(
213                T::from_repr_spec(r, self.inner_perms),
214            ),
215        }
216    }
217
218    pub open spec fn is_init(self) -> bool {
219        self.mem_contents().is_init()
220    }
221
222    pub open spec fn is_uninit(self) -> bool {
223        self.mem_contents().is_uninit()
224    }
225
226    pub open spec fn value(self) -> T
227        recommends
228            self.is_init(),
229    {
230        self.mem_contents().value()
231    }
232
233    pub open spec fn pptr(self) -> ReprPtr<R, T> {
234        ReprPtr { addr: self.addr, ptr: self.points_to.pptr(), _T: PhantomData }
235    }
236
237    pub broadcast proof fn pptr_implies_addr(&self)
238        ensures
239            self.addr() == #[trigger] self.pptr().addr(),
240    {
241    }
242
243    pub axiom fn take_inner_perms(tracked &mut self) -> (tracked result: T::Perm)
244        ensures
245            result == old(self).inner_perms,
246            self.addr == old(self).addr,
247            self.points_to == old(self).points_to,
248    ;
249
250    pub axiom fn put_inner_perms(tracked &mut self, tracked perms: T::Perm)
251        ensures
252            self.inner_perms == perms,
253            self.addr == old(self).addr,
254            self.points_to == old(self).points_to,
255    ;
256
257    pub axiom fn take_points_to(tracked &mut self) -> (tracked result: simple_pptr::PointsTo<R>)
258        ensures
259            result == old(self).points_to,
260            self.addr == old(self).addr,
261            self.inner_perms == old(self).inner_perms,
262    ;
263}
264
265impl<R, T: Repr<R>> From<PointsTo<R, T>> for vstd::simple_pptr::PointsTo<R> {
266    #[verifier::external_body]
267    fn from(ptr: PointsTo<R, T>) -> Self {
268        ptr.points_to
269    }
270}
271
272} // verus!
vstd_extra/cast_ptr.rs

vstd_extra/
cast_ptr.rs
