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 ReprPerm;
15
16    spec fn wf(r: R, perm: Self::ReprPerm) -> bool;
17
18    spec fn to_repr_spec(self, perm: Self::ReprPerm) -> (R, Self::ReprPerm);
19
20    fn to_repr(self, Tracked(perm): Tracked<&mut Self::ReprPerm>) -> (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::ReprPerm) -> Self;
27
28    fn from_repr(r: R, Tracked(perm): Tracked<&Self::ReprPerm>) -> (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::ReprPerm>) -> (res: &'a Self)
36        requires
37            Self::wf(*r, *perm),
38        ensures
39            *res == Self::from_repr_spec(*r, *perm),
40    ;
41
42    /// Mutable counterpart of [`Self::from_borrowed`]. Implementations must
43    /// project the same in-place representation as `from_borrowed` and keep
44    /// the representation permission synchronized with mutations through the
45    /// returned reference.
46    fn from_borrowed_mut<'a>(r: &'a mut R, Tracked(perm): Tracked<&'a mut Self::ReprPerm>) -> (res:
47        &'a mut Self)
48        requires
49            Self::wf(*old(r), *old(perm)),
50        ensures
51            *res == Self::from_repr_spec(*old(r), *old(perm)),
52            Self::wf(*final(r), *final(perm)),
53            *final(res) == Self::from_repr_spec(*final(r), *final(perm)),
54    ;
55
56    proof fn from_to_repr(self, perm: Self::ReprPerm)
57        ensures
58            Self::from_repr_spec(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1) == self,
59    ;
60
61    proof fn to_from_repr(r: R, perm: Self::ReprPerm)
62        requires
63            Self::wf(r, perm),
64        ensures
65            Self::from_repr_spec(r, perm).to_repr_spec(perm) == (r, perm),
66    ;
67
68    proof fn to_repr_wf(self, perm: Self::ReprPerm)
69        ensures
70            Self::wf(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1),
71    ;
72}
73
74/// Concrete representation of a pointer to an object of type T with representation type R
75/// The length of the array is not stored in the pointer
76#[verifier::accept_recursive_types(T)]
77pub struct ReprPtr<R, T> {
78    pub ptr: PPtr<R>,
79    pub _T: PhantomData<T>,
80}
81
82impl<R, T> Clone for ReprPtr<R, T> {
83    fn clone(&self) -> Self
84        returns
85            self,
86    {
87        Self { ptr: self.ptr, _T: PhantomData }
88    }
89}
90
91impl<R, T> Copy for ReprPtr<R, T> {
92
93}
94
95impl<R, T> FromSpecImpl<PPtr<R>> for ReprPtr<R, T> {
96    open spec fn obeys_from_spec() -> bool {
97        true
98    }
99
100    open spec fn from_spec(ptr: PPtr<R>) -> Self {
101        Self { ptr, _T: PhantomData }
102    }
103}
104
105impl<R, T> From<PPtr<R>> for ReprPtr<R, T> {
106    fn from(ptr: PPtr<R>) -> Self {
107        Self { ptr, _T: PhantomData }
108    }
109}
110
111impl<R, T> FromSpecImpl<ReprPtr<R, T>> for PPtr<R> {
112    open spec fn obeys_from_spec() -> bool {
113        true
114    }
115
116    open spec fn from_spec(ptr: ReprPtr<R, T>) -> Self {
117        ptr.ptr
118    }
119}
120
121impl<R, T> From<ReprPtr<R, T>> for PPtr<R> {
122    fn from(ptr: ReprPtr<R, T>) -> Self {
123        ptr.ptr
124    }
125}
126
127impl<R, T> ReprPtr<R, T> {
128    pub open spec fn new_spec(ptr: PPtr<R>) -> Self {
129        Self { ptr, _T: PhantomData }
130    }
131
132    pub fn from_pptr(ptr: PPtr<R>) -> (res: Self)
133        ensures
134            res == Self::new_spec(ptr),
135            res.addr() == ptr.addr(),
136            res.ptr == ptr,
137    {
138        Self { ptr, _T: PhantomData }
139    }
140
141    pub open spec fn to_pptr(self) -> PPtr<R> {
142        self.ptr
143    }
144
145    pub open spec fn addr_spec(self) -> usize {
146        self.ptr.addr()
147    }
148
149    #[verifier::when_used_as_spec(addr_spec)]
150    pub fn addr(self) -> usize
151        returns
152            self.addr(),
153    {
154        self.ptr.addr()
155    }
156}
157
158impl<R, T: Repr<R>> ReprPtr<R, T> {
159    pub fn take(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>) -> (v: T)
160        requires
161            old(perm).pptr() == self,
162            old(perm).is_init(),
163            old(perm).wf(&old(perm).inner_perms),
164        ensures
165            final(perm).pptr() == old(perm).pptr(),
166            final(perm).mem_contents() == MemContents::Uninit::<T>,
167            v == old(perm).value(),
168            final(perm).inner_perms == old(perm).inner_perms,
169    {
170        proof {
171            T::from_to_repr(perm.value(), perm.inner_perms);
172        }
173        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)), Tracked(&perm.inner_perms))
174    }
175
176    pub fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
177        requires
178            old(perm).pptr() == self,
179            old(perm).mem_contents() == MemContents::Uninit::<T>,
180        ensures
181            final(perm).pptr() == old(perm).pptr(),
182            final(perm).mem_contents() == MemContents::Init(v),
183            final(perm).wf(&final(perm).inner_perms),
184            final(perm).inner_perms == v.to_repr_spec(old(perm).inner_perms).1,
185            final(perm).points_to.value() == v.to_repr_spec(old(perm).inner_perms).0,
186            final(perm).points_to.is_init(),
187    {
188        proof {
189            v.from_to_repr(perm.inner_perms);
190            v.to_repr_wf(perm.inner_perms);
191        }
192        self.ptr.put(Tracked(&mut perm.points_to), v.to_repr(Tracked(&mut perm.inner_perms)))
193    }
194
195    pub fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<R, T>>) -> (v: &'a T)
196        requires
197            perm.pptr() == self,
198            perm.is_init(),
199            perm.wf(&perm.inner_perms),
200        ensures
201            *v == perm.value(),
202    {
203        T::from_borrowed(self.ptr.borrow(Tracked(&perm.points_to)), Tracked(&perm.inner_perms))
204    }
205
206    /// Borrows the pointed-to `T` mutably for the lifetime of `perm`.
207    ///
208    /// While the returned borrow is live, `perm` is exclusively held and
209    /// cannot be used. The returned borrow is tied to the tracked permission:
210    /// at the return point, the permission's value matches `*v`. Callers must
211    /// preserve any invariants beyond the final initialised/well-formed state
212    /// themselves.
213    ///
214    /// FIXME[SOUNDNESS]: This method is unsound because the caller must ensure the final value of `v` is consistent with the inner permissions.
215    #[verifier::external_body]
216    pub fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<R, T>>) -> (v: &'a mut T)
217        requires
218            old(perm).pptr() == self,
219            old(perm).is_init(),
220            old(perm).wf(&old(perm).inner_perms),
221        ensures
222            *v == old(perm).value(),
223            final(perm).pptr() == old(perm).pptr(),
224            final(perm).is_init(),
225            final(perm).wf(&final(perm).inner_perms),
226            final(perm).value() == *final(v),
227    {
228        // SAFETY: `Repr<R> for T` asserts layout compatibility between R and
229        // T. The tracked `perm` guards against concurrent access.
230        unsafe { &mut *(self.ptr.addr() as *mut T) }
231    }
232}
233
234#[verifier::accept_recursive_types(T)]
235pub tracked struct PointsTo<R, T: Repr<R>> {
236    pub points_to: simple_pptr::PointsTo<R>,
237    pub inner_perms: T::ReprPerm,
238    pub _T: PhantomData<T>,
239}
240
241impl<R, T: Repr<R>> PointsTo<R, T> {
242    pub open spec fn new_spec(
243        points_to: simple_pptr::PointsTo<R>,
244        inner_perms: T::ReprPerm,
245    ) -> Self {
246        Self { points_to, inner_perms, _T: PhantomData }
247    }
248
249    pub proof fn new(
250        tracked points_to: simple_pptr::PointsTo<R>,
251        tracked inner_perms: T::ReprPerm,
252    ) -> (tracked res: Self)
253        returns
254            Self::new_spec(points_to, inner_perms),
255    {
256        Self { points_to, inner_perms, _T: PhantomData }
257    }
258
259    pub open spec fn wf(self, perm: &T::ReprPerm) -> bool {
260        &&& T::wf(self.points_to.value(), *perm)
261    }
262
263    pub open spec fn addr(self) -> usize {
264        self.points_to.addr()
265    }
266
267    pub open spec fn mem_contents(self) -> MemContents<T> {
268        match self.points_to.mem_contents() {
269            MemContents::<R>::Uninit => MemContents::<T>::Uninit,
270            MemContents::<R>::Init(r) => MemContents::<T>::Init(
271                T::from_repr_spec(r, self.inner_perms),
272            ),
273        }
274    }
275
276    pub open spec fn is_init(self) -> bool {
277        self.mem_contents().is_init()
278    }
279
280    pub open spec fn is_uninit(self) -> bool {
281        self.mem_contents().is_uninit()
282    }
283
284    pub open spec fn value(self) -> T
285        recommends
286            self.is_init(),
287    {
288        self.mem_contents().value()
289    }
290
291    pub open spec fn pptr(self) -> ReprPtr<R, T> {
292        ReprPtr { ptr: self.points_to.pptr(), _T: PhantomData }
293    }
294}
295
296} // verus!
vstd_extra/cast_ptr.rs

vstd_extra/
cast_ptr.rs
