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    {
156        proof {
157            T::from_to_repr(perm.value(), perm.inner_perms);
158        }
159        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)), Tracked(&perm.inner_perms))
160    }
161
162    pub exec fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
163        requires
164            old(perm).pptr() == self,
165            old(perm).mem_contents() == MemContents::Uninit::<T>,
166        ensures
167            final(perm).pptr() == old(perm).pptr(),
168            final(perm).mem_contents() == MemContents::Init(v),
169            final(perm).wf(&final(perm).inner_perms),
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 exec 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. Mutations made through `*v` are not tracked by the
193    /// Verus model: the postcondition only promises the final `perm` is still
194    /// initialised and well-formed. Callers must preserve any invariants
195    /// beyond that themselves.
196    #[verifier::external_body]
197    pub exec fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<R, T>>) -> (v:
198        &'a mut T)
199        requires
200            old(perm).pptr() == self,
201            old(perm).is_init(),
202            old(perm).wf(&old(perm).inner_perms),
203        ensures
204            *v == old(perm).value(),
205            final(perm).pptr() == old(perm).pptr(),
206            final(perm).is_init(),
207            final(perm).wf(&final(perm).inner_perms),
208    {
209        // SAFETY: `Repr<R> for T` asserts layout compatibility between R and
210        // T. The tracked `perm` guards against concurrent access.
211        unsafe { &mut *(self.ptr.addr() as *mut T) }
212    }
213}
214
215#[verifier::accept_recursive_types(T)]
216pub tracked struct PointsTo<R, T: Repr<R>> {
217    pub tracked points_to: simple_pptr::PointsTo<R>,
218    pub tracked inner_perms: T::Perm,
219    pub _T: PhantomData<T>,
220}
221
222impl<R, T: Repr<R>> PointsTo<R, T> {
223    pub open spec fn new_spec(points_to: simple_pptr::PointsTo<R>, inner_perms: T::Perm) -> Self {
224        Self { points_to, inner_perms, _T: PhantomData }
225    }
226
227    pub proof fn new(
228        tracked points_to: simple_pptr::PointsTo<R>,
229        tracked inner_perms: T::Perm,
230    ) -> tracked Self {
231        Self { points_to: points_to, inner_perms, _T: PhantomData }
232    }
233
234    pub open spec fn wf(self, perm: &T::Perm) -> bool {
235        &&& T::wf(self.points_to.value(), *perm)
236    }
237
238    pub open spec fn addr(self) -> usize {
239        self.points_to.addr()
240    }
241
242    pub open spec fn mem_contents(self) -> MemContents<T> {
243        match self.points_to.mem_contents() {
244            MemContents::<R>::Uninit => MemContents::<T>::Uninit,
245            MemContents::<R>::Init(r) => MemContents::<T>::Init(
246                T::from_repr_spec(r, self.inner_perms),
247            ),
248        }
249    }
250
251    pub open spec fn is_init(self) -> bool {
252        self.mem_contents().is_init()
253    }
254
255    pub open spec fn is_uninit(self) -> bool {
256        self.mem_contents().is_uninit()
257    }
258
259    pub open spec fn value(self) -> T
260        recommends
261            self.is_init(),
262    {
263        self.mem_contents().value()
264    }
265
266    pub open spec fn pptr(self) -> ReprPtr<R, T> {
267        ReprPtr { ptr: self.points_to.pptr(), _T: PhantomData }
268    }
269
270    pub broadcast proof fn pptr_implies_addr(&self)
271        ensures
272            self.addr() == #[trigger] self.pptr().addr(),
273    {
274    }
275}
276
277impl<R, T: Repr<R>> From<PointsTo<R, T>> for vstd::simple_pptr::PointsTo<R> {
278    #[verifier::external_body]
279    fn from(ptr: PointsTo<R, T>) -> Self {
280        ptr.points_to
281    }
282}
283
284} // verus!
vstd_extra/cast_ptr.rs

vstd_extra/
cast_ptr.rs
