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};
8use vstd::std_specs::convert::{FromSpec, FromSpecImpl};
9
10use core::marker::PhantomData;
11use core::ops::Deref;
12
13verus! {
14
15pub trait Repr<R: Sized>: Sized {
16    /// If the underlying representation contains cells, the translation may require permission objects that access them.
17    type Perm;
18
19    spec fn wf(r: R, perm: Self::Perm) -> bool;
20
21    spec fn to_repr_spec(self, perm: Self::Perm) -> (R, Self::Perm);
22
23    fn to_repr(self, Tracked(perm): Tracked<&mut Self::Perm>) -> (res: R)
24        ensures
25            res == self.to_repr_spec(*old(perm)).0,
26            *final(perm) == self.to_repr_spec(*old(perm)).1,
27    ;
28
29    spec fn from_repr_spec(r: R, perm: Self::Perm) -> Self;
30
31    fn from_repr(r: R, Tracked(perm): Tracked<&Self::Perm>) -> (res: Self)
32        requires
33            Self::wf(r, *perm),
34        ensures
35            res == Self::from_repr_spec(r, *perm),
36    ;
37
38    fn from_borrowed<'a>(r: &'a R, Tracked(perm): Tracked<&'a Self::Perm>) -> (res: &'a Self)
39        requires
40            Self::wf(*r, *perm),
41        ensures
42            *res == Self::from_repr_spec(*r, *perm),
43    ;
44
45    proof fn from_to_repr(self, perm: Self::Perm)
46        ensures
47            Self::from_repr_spec(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1) == self,
48    ;
49
50    proof fn to_from_repr(r: R, perm: Self::Perm)
51        requires
52            Self::wf(r, perm),
53        ensures
54            Self::from_repr_spec(r, perm).to_repr_spec(perm) == (r, perm),
55    ;
56
57    proof fn to_repr_wf(self, perm: Self::Perm)
58        ensures
59            Self::wf(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1),
60    ;
61}
62
63/// Concrete representation of a pointer to an object of type T with representation type R
64/// The length of the array is not stored in the pointer
65pub struct ReprPtr<R, T: Repr<R>> { 
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 { 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>> FromSpecImpl<PPtr<R>> for ReprPtr<R, T> {
81    open spec fn obeys_from_spec() -> bool {
82        true
83    }
84
85    open spec fn from_spec(ptr: PPtr<R>) -> Self {
86        Self { ptr: ptr, _T: PhantomData }
87    }
88}
89
90impl<R, T: Repr<R>> From<PPtr<R>> for ReprPtr<R, T> {
91    fn from(ptr: PPtr<R>) -> Self {
92        Self { ptr: ptr, _T: PhantomData }
93    }
94}
95
96impl<R, T: Repr<R>> FromSpecImpl<ReprPtr<R, T>> for PPtr<R> {
97    open spec fn obeys_from_spec() -> bool {
98        true
99    }
100
101    open spec fn from_spec(ptr: ReprPtr<R, T>) -> Self {
102        ptr.ptr
103    }
104}
105
106impl<R, T: Repr<R>> From<ReprPtr<R, T>> for PPtr<R> {
107    fn from(ptr: ReprPtr<R, T>) -> Self {
108        ptr.ptr
109    }
110}
111
112impl<R, T: Repr<R>> ReprPtr<R, T> {
113    pub open spec fn new_spec(ptr: PPtr<R>) -> Self {
114        Self { ptr: ptr, _T: PhantomData }
115    }
116
117    #[verifier::external_body]
118    pub fn new_borrowed<'a>(ptr: &'a PPtr<R>) -> (res: &'a Self)
119        ensures
120            *res == Self::new_spec(*ptr),
121    {
122        unimplemented!()
123    }
124
125    pub fn from_pptr(ptr: PPtr<R>) -> (res: Self)
126        ensures
127            res == Self::new_spec(ptr),
128            res.addr() == ptr.addr(),
129            res.ptr == ptr,
130    {
131        Self { ptr: ptr, _T: PhantomData }
132    }
133
134    pub open spec fn to_pptr(self) -> PPtr<R> {
135        self.ptr
136    }
137
138    pub open spec fn addr_spec(self) -> usize {
139        self.ptr.addr()
140    }
141
142    #[verifier::when_used_as_spec(addr_spec)]
143    pub fn addr(self) -> (u: usize)
144        returns self.addr_spec(),
145    {
146        self.ptr.addr()
147    }
148
149    pub exec fn take(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>) -> (v: T)
150        requires
151            old(perm).pptr() == self,
152            old(perm).is_init(),
153            old(perm).wf(&old(perm).inner_perms),
154        ensures
155            final(perm).pptr() == old(perm).pptr(),
156            final(perm).mem_contents() == MemContents::Uninit::<T>,
157            v == old(perm).value(),
158    {
159        proof {
160            T::from_to_repr(perm.value(), perm.inner_perms);
161        }
162        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)), Tracked(&perm.inner_perms))
163    }
164
165    pub exec fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
166        requires
167            old(perm).pptr() == self,
168            old(perm).mem_contents() == MemContents::Uninit::<T>,
169        ensures
170            final(perm).pptr() == old(perm).pptr(),
171            final(perm).mem_contents() == MemContents::Init(v),
172            final(perm).wf(&final(perm).inner_perms),
173    {
174        proof {
175            v.from_to_repr(perm.inner_perms);
176            v.to_repr_wf(perm.inner_perms);
177        }
178        self.ptr.put(Tracked(&mut perm.points_to), v.to_repr(Tracked(&mut perm.inner_perms)))
179    }
180
181    pub exec fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<R, T>>) -> (v: &'a T)
182        requires
183            perm.pptr() == self,
184            perm.is_init(),
185            perm.wf(&perm.inner_perms),
186        ensures
187            *v === perm.value(),
188    {
189        T::from_borrowed(self.ptr.borrow(Tracked(&perm.points_to)), Tracked(&perm.inner_perms))
190    }
191
192    /// Borrows the pointed-to `T` mutably for the lifetime of `perm`.
193    ///
194    /// While the returned borrow is live, `perm` is exclusively held and
195    /// cannot be used. Mutations made through `*v` are not tracked by the
196    /// Verus model: the postcondition only promises the final `perm` is still
197    /// initialised and well-formed. Callers must preserve any invariants
198    /// beyond that themselves.
199    #[verifier::external_body]
200    pub exec fn borrow_mut<'a>(
201        self,
202        Tracked(perm): Tracked<&'a mut PointsTo<R, T>>,
203    ) -> (v: &'a mut T)
204        requires
205            old(perm).pptr() == self,
206            old(perm).is_init(),
207            old(perm).wf(&old(perm).inner_perms),
208        ensures
209            *v == old(perm).value(),
210            final(perm).pptr() == old(perm).pptr(),
211            final(perm).is_init(),
212            final(perm).wf(&final(perm).inner_perms),
213    {
214        // SAFETY: `Repr<R> for T` asserts layout compatibility between R and
215        // T. The tracked `perm` guards against concurrent access.
216        unsafe { &mut *(self.ptr.addr() as *mut T) }
217    }
218}
219
220#[verifier::accept_recursive_types(T)]
221pub tracked struct PointsTo<R, T: Repr<R>> {
222    pub tracked points_to: simple_pptr::PointsTo<R>,
223    pub tracked inner_perms: T::Perm,
224    pub _T: PhantomData<T>,
225}
226
227impl<R, T: Repr<R>> PointsTo<R, T> {
228    pub open spec fn new_spec(
229        points_to: simple_pptr::PointsTo<R>,
230        inner_perms: T::Perm,
231    ) -> Self {
232        Self { points_to, inner_perms, _T: PhantomData }
233    }
234
235    pub proof fn new(
236        tracked points_to: simple_pptr::PointsTo<R>,
237        tracked inner_perms: T::Perm,
238    ) -> tracked Self {
239        Self { points_to: points_to, inner_perms, _T: PhantomData }
240    }
241
242    pub open spec fn wf(self, perm: &T::Perm) -> bool {
243        &&& T::wf(self.points_to.value(), *perm)
244    }
245
246    pub open spec fn addr(self) -> usize {
247        self.points_to.addr()
248    }
249
250    pub open spec fn mem_contents(self) -> MemContents<T> {
251        match self.points_to.mem_contents() {
252            MemContents::<R>::Uninit => MemContents::<T>::Uninit,
253            MemContents::<R>::Init(r) => MemContents::<T>::Init(
254                T::from_repr_spec(r, self.inner_perms),
255            ),
256        }
257    }
258
259    pub open spec fn is_init(self) -> bool {
260        self.mem_contents().is_init()
261    }
262
263    pub open spec fn is_uninit(self) -> bool {
264        self.mem_contents().is_uninit()
265    }
266
267    pub open spec fn value(self) -> T
268        recommends
269            self.is_init(),
270    {
271        self.mem_contents().value()
272    }
273
274    pub open spec fn pptr(self) -> ReprPtr<R, T> {
275        ReprPtr { ptr: self.points_to.pptr(), _T: PhantomData }
276    }
277
278    pub broadcast proof fn pptr_implies_addr(&self)
279        ensures
280            self.addr() == #[trigger] self.pptr().addr(),
281    {
282    }
283}
284
285impl<R, T: Repr<R>> From<PointsTo<R, T>> for vstd::simple_pptr::PointsTo<R> {
286    #[verifier::external_body]
287    fn from(ptr: PointsTo<R, T>) -> Self {
288        ptr.points_to
289    }
290}
291
292} // verus!
vstd_extra/cast_ptr.rs

vstd_extra/
cast_ptr.rs
