vstd_extra/
cast_ptr.rs

1use vstd::prelude::*;
2
3use vstd::raw_ptr::MemContents;
4use vstd::simple_pptr::{self, PPtr};
5use vstd::std_specs::convert::{FromSpec, FromSpecImpl};
6
7use core::marker::PhantomData;
8
9verus! {
10
11/// A trait for types that have a concrete representation type `R`.
12pub trait Repr<R: Sized>: Sized {
13    /// If the underlying representation contains cells, the translation may require permission objects that access them.
14    type Perm;
15
16    spec fn wf(r: R, perm: Self::Perm) -> bool;
17
18    spec fn to_repr_spec(self, perm: Self::Perm) -> (R, Self::Perm);
19
20    fn to_repr(self, Tracked(perm): Tracked<&mut Self::Perm>) -> (res: R)
21        ensures
22            res == self.to_repr_spec(*old(perm)).0,
23            *final(perm) == self.to_repr_spec(*old(perm)).1,
24    ;
25
26    spec fn from_repr_spec(r: R, perm: Self::Perm) -> Self;
27
28    fn from_repr(r: R, Tracked(perm): Tracked<&Self::Perm>) -> (res: Self)
29        requires
30            Self::wf(r, *perm),
31        returns
32            Self::from_repr_spec(r, *perm),
33    ;
34
35    fn from_borrowed<'a>(r: &'a R, Tracked(perm): Tracked<&'a Self::Perm>) -> (res: &'a Self)
36        requires
37            Self::wf(*r, *perm),
38        ensures
39            *res == Self::from_repr_spec(*r, *perm),
40    ;
41
42    proof fn from_to_repr(self, perm: Self::Perm)
43        ensures
44            Self::from_repr_spec(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1) == self,
45    ;
46
47    proof fn to_from_repr(r: R, perm: Self::Perm)
48        requires
49            Self::wf(r, perm),
50        ensures
51            Self::from_repr_spec(r, perm).to_repr_spec(perm) == (r, perm),
52    ;
53
54    proof fn to_repr_wf(self, perm: Self::Perm)
55        ensures
56            Self::wf(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1),
57    ;
58}
59
60/// Concrete representation of a pointer to an object of type T with representation type R
61/// The length of the array is not stored in the pointer
62pub struct ReprPtr<R, T: Repr<R>> {
63    pub ptr: PPtr<R>,
64    pub _T: PhantomData<T>,
65}
66
67impl<R, T: Repr<R>> Clone for ReprPtr<R, T> {
68    fn clone(&self) -> Self
69        returns
70            self,
71    {
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, _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, _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, _T: PhantomData }
115    }
116
117    pub fn from_pptr(ptr: PPtr<R>) -> (res: Self)
118        ensures
119            res == Self::new_spec(ptr),
120            res.addr() == ptr.addr(),
121            res.ptr == ptr,
122    {
123        Self { ptr, _T: PhantomData }
124    }
125
126    pub open spec fn to_pptr(self) -> PPtr<R> {
127        self.ptr
128    }
129
130    pub open spec fn addr_spec(self) -> usize {
131        self.ptr.addr()
132    }
133
134    #[verifier::when_used_as_spec(addr_spec)]
135    pub fn addr(self) -> usize
136        returns
137            self.addr(),
138    {
139        self.ptr.addr()
140    }
141
142    pub fn take(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>) -> (v: T)
143        requires
144            old(perm).pptr() == self,
145            old(perm).is_init(),
146            old(perm).wf(&old(perm).inner_perms),
147        ensures
148            final(perm).pptr() == old(perm).pptr(),
149            final(perm).mem_contents() == MemContents::Uninit::<T>,
150            v == old(perm).value(),
151            final(perm).inner_perms == old(perm).inner_perms,
152    {
153        proof {
154            T::from_to_repr(perm.value(), perm.inner_perms);
155        }
156        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)), Tracked(&perm.inner_perms))
157    }
158
159    pub fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
160        requires
161            old(perm).pptr() == self,
162            old(perm).mem_contents() == MemContents::Uninit::<T>,
163        ensures
164            final(perm).pptr() == old(perm).pptr(),
165            final(perm).mem_contents() == MemContents::Init(v),
166            final(perm).wf(&final(perm).inner_perms),
167            final(perm).inner_perms == v.to_repr_spec(old(perm).inner_perms).1,
168            final(perm).points_to.value() == v.to_repr_spec(old(perm).inner_perms).0,
169            final(perm).points_to.is_init(),
170    {
171        proof {
172            v.from_to_repr(perm.inner_perms);
173            v.to_repr_wf(perm.inner_perms);
174        }
175        self.ptr.put(Tracked(&mut perm.points_to), v.to_repr(Tracked(&mut perm.inner_perms)))
176    }
177
178    pub fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<R, T>>) -> (v: &'a T)
179        requires
180            perm.pptr() == self,
181            perm.is_init(),
182            perm.wf(&perm.inner_perms),
183        ensures
184            *v == perm.value(),
185    {
186        T::from_borrowed(self.ptr.borrow(Tracked(&perm.points_to)), Tracked(&perm.inner_perms))
187    }
188
189    /// Borrows the pointed-to `T` mutably for the lifetime of `perm`.
190    ///
191    /// While the returned borrow is live, `perm` is exclusively held and
192    /// cannot be used. The returned borrow is tied to the tracked permission:
193    /// at the return point, the permission's value matches `*v`. Callers must
194    /// preserve any invariants beyond the final initialised/well-formed state
195    /// themselves.
196    ///
197    /// FIXME[SOUNDNESS]: This method is unsound because the caller must ensure the final value of `v` is consistent with the inner permissions.
198    #[verifier::external_body]
199    pub fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<R, T>>) -> (v: &'a mut T)
200        requires
201            old(perm).pptr() == self,
202            old(perm).is_init(),
203            old(perm).wf(&old(perm).inner_perms),
204        ensures
205            *v == old(perm).value(),
206            final(perm).pptr() == old(perm).pptr(),
207            final(perm).is_init(),
208            final(perm).wf(&final(perm).inner_perms),
209            final(perm).value() == *final(v),
210    {
211        // SAFETY: `Repr<R> for T` asserts layout compatibility between R and
212        // T. The tracked `perm` guards against concurrent access.
213        unsafe { &mut *(self.ptr.addr() as *mut T) }
214    }
215}
216
217#[verifier::accept_recursive_types(T)]
218pub tracked struct PointsTo<R, T: Repr<R>> {
219    pub points_to: simple_pptr::PointsTo<R>,
220    pub inner_perms: T::Perm,
221    pub _T: PhantomData<T>,
222}
223
224impl<R, T: Repr<R>> PointsTo<R, T> {
225    pub open spec fn new_spec(points_to: simple_pptr::PointsTo<R>, inner_perms: T::Perm) -> Self {
226        Self { points_to, inner_perms, _T: PhantomData }
227    }
228
229    pub proof fn new(
230        tracked points_to: simple_pptr::PointsTo<R>,
231        tracked inner_perms: T::Perm,
232    ) -> (tracked res: Self)
233        returns
234            Self::new_spec(points_to, inner_perms),
235    {
236        Self { points_to, inner_perms, _T: PhantomData }
237    }
238
239    pub open spec fn wf(self, perm: &T::Perm) -> bool {
240        &&& T::wf(self.points_to.value(), *perm)
241    }
242
243    pub open spec fn addr(self) -> usize {
244        self.points_to.addr()
245    }
246
247    pub open spec fn mem_contents(self) -> MemContents<T> {
248        match self.points_to.mem_contents() {
249            MemContents::<R>::Uninit => MemContents::<T>::Uninit,
250            MemContents::<R>::Init(r) => MemContents::<T>::Init(
251                T::from_repr_spec(r, self.inner_perms),
252            ),
253        }
254    }
255
256    pub open spec fn is_init(self) -> bool {
257        self.mem_contents().is_init()
258    }
259
260    pub open spec fn is_uninit(self) -> bool {
261        self.mem_contents().is_uninit()
262    }
263
264    pub open spec fn value(self) -> T
265        recommends
266            self.is_init(),
267    {
268        self.mem_contents().value()
269    }
270
271    pub open spec fn pptr(self) -> ReprPtr<R, T> {
272        ReprPtr { ptr: self.points_to.pptr(), _T: PhantomData }
273    }
274}
275
276} // verus!
vstd_extra/cast_ptr.rs

vstd_extra/
cast_ptr.rs
