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};
8
9use core::marker::PhantomData;
10
11verus! {
12
13pub trait Repr<R: Sized>: Sized {
14    spec fn wf(r: R) -> bool;
15
16    spec fn to_repr_spec(self) -> R;
17
18    #[verifier::when_used_as_spec(to_repr_spec)]
19    fn to_repr(self) -> (res: R)
20        ensures
21            res == self.to_repr_spec(),
22    ;
23
24    spec fn from_repr_spec(r: R) -> Self;
25
26    #[verifier::when_used_as_spec(from_repr_spec)]
27    fn from_repr(r: R) -> (res: Self)
28        requires
29            Self::wf(r),
30        ensures
31            res == Self::from_repr_spec(r),
32    ;
33
34    fn from_borrowed<'a>(r: &'a R) -> (res: &'a Self)
35        requires
36            Self::wf(*r),
37        ensures
38            *res == Self::from_repr_spec(*r),
39    ;
40
41    proof fn from_to_repr(self)
42        ensures
43            Self::from_repr(self.to_repr()) == self,
44    ;
45
46    proof fn to_from_repr(r: R)
47        requires
48            Self::wf(r),
49        ensures
50            Self::from_repr(r).to_repr() == r,
51    ;
52
53    proof fn to_repr_wf(self)
54        ensures
55            Self::wf(self.to_repr()),
56    ;
57}
58
59/// Concrete representation of a pointer to an array
60/// The length of the array is not stored in the pointer
61pub struct ReprPtr<R, T: Repr<R>> {
62    pub addr: usize,
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        Self { addr: self.addr, ptr: self.ptr, _T: PhantomData }
70    }
71}
72
73impl<R, T: Repr<R>> Copy for ReprPtr<R, T> {
74
75}
76
77impl<R, T: Repr<R>> ReprPtr<R, T> {
78    pub open spec fn addr_spec(self) -> usize {
79        self.addr
80    }
81
82    #[verifier::when_used_as_spec(addr_spec)]
83    pub fn addr(self) -> (u: usize)
84        ensures
85            u == self.addr,
86    {
87        self.addr
88    }
89
90    pub exec fn take(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>) -> (v: T)
91        requires
92            old(perm).pptr() == self,
93            old(perm).is_init(),
94            old(perm).wf(),
95        ensures
96            perm.pptr() == old(perm).pptr(),
97            perm.mem_contents() == MemContents::Uninit::<T>,
98            v == old(perm).value(),
99    {
100        proof {
101            T::from_to_repr(perm.value());
102        }
103        T::from_repr(self.ptr.take(Tracked(&mut perm.points_to)))
104    }
105
106    pub exec fn put(self, Tracked(perm): Tracked<&mut PointsTo<R, T>>, v: T)
107        requires
108            old(perm).pptr() == self,
109            old(perm).mem_contents() == MemContents::Uninit::<T>,
110        ensures
111            perm.pptr() == old(perm).pptr(),
112            perm.mem_contents() == MemContents::Init(v),
113            perm.wf(),
114    {
115        proof {
116            v.from_to_repr();
117            v.to_repr_wf();
118        }
119        self.ptr.put(Tracked(&mut perm.points_to), v.to_repr())
120    }
121
122    pub exec fn borrow<'a>(self, Tracked(perm): Tracked<&'a PointsTo<R, T>>) -> (v: &'a T)
123        requires
124            perm.pptr() == self,
125            perm.is_init(),
126            perm.wf(),
127        ensures
128            *v === perm.value(),
129    {
130        T::from_borrowed(self.ptr.borrow(Tracked(&perm.points_to)))
131    }
132}
133
134#[verifier::accept_recursive_types(T)]
135pub tracked struct PointsTo<R, T: Repr<R>> {
136    pub ghost addr: usize,
137    pub points_to: simple_pptr::PointsTo<R>,
138    pub _T: PhantomData<T>,
139}
140
141impl<R, T: Repr<R>> PointsTo<R, T> {
142    pub proof fn new(
143        addr: Ghost<usize>,
144        tracked points_to: simple_pptr::PointsTo<R>,
145    ) -> tracked Self {
146        Self { addr: addr@, points_to: points_to, _T: PhantomData }
147    }
148
149    pub open spec fn wf(self) -> bool {
150        &&& T::wf(self.points_to.value())
151    }
152
153    pub open spec fn addr(self) -> usize {
154        self.addr
155    }
156
157    pub open spec fn mem_contents(self) -> MemContents<T> {
158        match self.points_to.mem_contents() {
159            MemContents::<R>::Uninit => MemContents::<T>::Uninit,
160            MemContents::<R>::Init(r) => MemContents::<T>::Init(T::from_repr(r)),
161        }
162    }
163
164    pub open spec fn is_init(self) -> bool {
165        self.mem_contents().is_init()
166    }
167
168    pub open spec fn is_uninit(self) -> bool {
169        self.mem_contents().is_uninit()
170    }
171
172    pub open spec fn value(self) -> T
173        recommends
174            self.is_init(),
175    {
176        self.mem_contents().value()
177    }
178
179    pub open spec fn pptr(self) -> ReprPtr<R, T> {
180        ReprPtr { addr: self.addr, ptr: self.points_to.pptr(), _T: PhantomData }
181    }
182
183    pub broadcast proof fn pptr_implies_addr(&self)
184        ensures
185            self.addr() == #[trigger] self.pptr().addr(),
186    {
187    }
188}
189
190} // verus!
vstd_extra/cast_ptr.rs

vstd_extra/
cast_ptr.rs
