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
11pub trait Repr<R: Sized>: Sized {
12    /// If the underlying representation contains cells, the translation may require permission objects that access them.
13    type Perm;
14
15    spec fn wf(r: R, perm: Self::Perm) -> bool;
16
17    spec fn to_repr_spec(self, perm: Self::Perm) -> (R, Self::Perm);
18
19    fn to_repr(self, Tracked(perm): Tracked<&mut Self::Perm>) -> (res: R)
20        ensures
21            res == self.to_repr_spec(*old(perm)).0,
22            *final(perm) == self.to_repr_spec(*old(perm)).1,
23    ;
24
25    spec fn from_repr_spec(r: R, perm: Self::Perm) -> Self;
26
27    fn from_repr(r: R, Tracked(perm): Tracked<&Self::Perm>) -> (res: Self)
28        requires
29            Self::wf(r, *perm),
30        ensures
31            res == Self::from_repr_spec(r, *perm),
32    ;
33
34    fn from_borrowed<'a>(r: &'a R, Tracked(perm): Tracked<&'a Self::Perm>) -> (res: &'a Self)
35        requires
36            Self::wf(*r, *perm),
37        ensures
38            *res == Self::from_repr_spec(*r, *perm),
39    ;
40
41    proof fn from_to_repr(self, perm: Self::Perm)
42        ensures
43            Self::from_repr_spec(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1) == self,
44    ;
45
46    proof fn to_from_repr(r: R, perm: Self::Perm)
47        requires
48            Self::wf(r, perm),
49        ensures
50            Self::from_repr_spec(r, perm).to_repr_spec(perm) == (r, perm),
51    ;
52
53    proof fn to_repr_wf(self, perm: Self::Perm)
54        ensures
55            Self::wf(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1),
56    ;
57}
58
59/// Concrete representation of a pointer to an object of type T with representation type R
60/// The length of the array is not stored in the pointer
61pub struct ReprPtr<R, T: Repr<R>> {
62    pub ptr: PPtr<R>,
63    pub _T: PhantomData<T>,
64}
65
66impl<R, T: Repr<R>> Clone for ReprPtr<R, T> {
67    fn clone(&self) -> Self {
68        Self { ptr: self.ptr, _T: PhantomData }
69    }
70}
71
72impl<R, T: Repr<R>> Copy for ReprPtr<R, T> {
73
74}
75
76impl<R, T: Repr<R>> FromSpecImpl<PPtr<R>> for ReprPtr<R, T> {
77    open spec fn obeys_from_spec() -> bool {
78        true
79    }
80
81    open spec fn from_spec(ptr: PPtr<R>) -> Self {
82        Self { ptr: ptr, _T: PhantomData }
83    }
84}
85
86impl<R, T: Repr<R>> From<PPtr<R>> for ReprPtr<R, T> {
87    fn from(ptr: PPtr<R>) -> Self {
88        Self { ptr: ptr, _T: PhantomData }
89    }
90}
91
92impl<R, T: Repr<R>> FromSpecImpl<ReprPtr<R, T>> for PPtr<R> {
93    open spec fn obeys_from_spec() -> bool {
94        true
95    }
96
97    open spec fn from_spec(ptr: ReprPtr<R, T>) -> Self {
98        ptr.ptr
99    }
100}
101
102impl<R, T: Repr<R>> From<ReprPtr<R, T>> for PPtr<R> {
103    fn from(ptr: ReprPtr<R, T>) -> Self {
104        ptr.ptr
105    }
106}
107
108impl<R, T: Repr<R>> ReprPtr<R, T> {
109    pub open spec fn new_spec(ptr: PPtr<R>) -> Self {
110        Self { ptr: ptr, _T: PhantomData }
111    }
112
113    #[verifier::external_body]
114    pub fn new_borrowed<'a>(ptr: &'a PPtr<R>) -> (res: &'a Self)
115        ensures
116            *res == Self::new_spec(*ptr),
117    {
118        unimplemented!()
119    }
120
121    pub fn from_pptr(ptr: PPtr<R>) -> (res: Self)
122        ensures
123            res == Self::new_spec(ptr),
124            res.addr() == ptr.addr(),
125            res.ptr == ptr,
126    {
127        Self { ptr: ptr, _T: PhantomData }
128    }
129
130    pub open spec fn to_pptr(self) -> PPtr<R> {
131        self.ptr
132    }
133
134    pub open spec fn addr_spec(self) -> usize {
135        self.ptr.addr()
136    }
137
138    #[verifier::when_used_as_spec(addr_spec)]
139    pub fn addr(self) -> (u: usize)
140        returns
141            self.addr_spec(),
142    {
143        self.ptr.addr()
144    }
145
146    pub exec fn take(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>) -> (v: T)
147        requires
148            old(perm).pptr() == self,
149            old(perm).is_init(),
150            old(perm).wf(&old(perm).inner_perms),
151        ensures
152            final(perm).pptr() == old(perm).pptr(),
153            final(perm).mem_contents() == MemContents::Uninit::<T>,
154            v == old(perm).value(),
155            final(perm).inner_perms == old(perm).inner_perms,
156    {
157        proof {
158            T::from_to_repr(perm.value(), perm.inner_perms);
159        }
160        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)), Tracked(&perm.inner_perms))
161    }
162
163    pub exec fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
164        requires
165            old(perm).pptr() == self,
166            old(perm).mem_contents() == MemContents::Uninit::<T>,
167        ensures
168            final(perm).pptr() == old(perm).pptr(),
169            final(perm).mem_contents() == MemContents::Init(v),
170            final(perm).wf(&final(perm).inner_perms),
171            final(perm).inner_perms == v.to_repr_spec(old(perm).inner_perms).1,
172            final(perm).points_to.value() == v.to_repr_spec(old(perm).inner_perms).0,
173            final(perm).points_to.is_init(),
174    {
175        proof {
176            v.from_to_repr(perm.inner_perms);
177            v.to_repr_wf(perm.inner_perms);
178        }
179        self.ptr.put(Tracked(&mut perm.points_to), v.to_repr(Tracked(&mut perm.inner_perms)))
180    }
181
182    pub exec fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<R, T>>) -> (v: &'a T)
183        requires
184            perm.pptr() == self,
185            perm.is_init(),
186            perm.wf(&perm.inner_perms),
187        ensures
188            *v == perm.value(),
189    {
190        T::from_borrowed(self.ptr.borrow(Tracked(&perm.points_to)), Tracked(&perm.inner_perms))
191    }
192
193    /// Borrows the pointed-to `T` mutably for the lifetime of `perm`.
194    ///
195    /// While the returned borrow is live, `perm` is exclusively held and
196    /// cannot be used. The returned borrow is tied to the tracked permission:
197    /// at the return point, the permission's value matches `*v`. Callers must
198    /// preserve any invariants beyond the final initialised/well-formed state
199    /// themselves.
200    #[verifier::external_body]
201    pub exec fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<R, T>>) -> (v:
202        &'a mut T)
203        requires
204            old(perm).pptr() == self,
205            old(perm).is_init(),
206            old(perm).wf(&old(perm).inner_perms),
207        ensures
208            *v == old(perm).value(),
209            final(perm).pptr() == old(perm).pptr(),
210            final(perm).is_init(),
211            final(perm).wf(&final(perm).inner_perms),
212            final(perm).value() == *final(v),
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(points_to: simple_pptr::PointsTo<R>, inner_perms: T::Perm) -> Self {
229        Self { points_to, inner_perms, _T: PhantomData }
230    }
231
232    pub proof fn new(
233        tracked points_to: simple_pptr::PointsTo<R>,
234        tracked inner_perms: T::Perm,
235    ) -> (tracked res: Self)
236        ensures
237            res == Self::new_spec(points_to, inner_perms),
238    {
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
