vstd_extra/
raw_ptr_extra.rs

1use crate::ownership::*;
2use vstd::layout::size_of as layout_size_of;
3use vstd::layout::valid_layout;
4use vstd::prelude::*;
5use vstd::raw_ptr::*;
6
7// NOTE: vstd::layout::size_of and size_of are actually two different functions,
8// See: https://verus-lang.zulipchat.com/#narrow/channel/399078-help/topic/Multiple.20definitions.20of.20.60align_of.60.20and.20.60size_of.60.20in.20raw_ptr/with/563994445
9
10verus! {
11
12pub broadcast proof fn lemma_two_size_of_equal<T>()
13    requires
14        vstd::layout::size_of::<T>() <= usize::MAX,
15    ensures
16        #[trigger] vstd::layout::size_of::<T>() == size_of::<T>(),
17{
18}
19
20pub broadcast proof fn lemma_two_align_of_equal<T>()
21    requires
22        vstd::layout::align_of::<T>() <= usize::MAX,
23    ensures
24        #[trigger] vstd::layout::align_of::<T>() == align_of::<T>(),
25{
26}
27
28// Record Typed access permission along with Dealloc permission.
29// This is similar to PPtr::PointsTo, but we want to make it as low-level and general as possible.
30// Difference with PPtr::PointsTo:
31// 1. Allowing null pointers (addr == 0).
32// 2. Relaxed alignment requirement between Dealloc::align and align_of::<T>().
33// TODO: consider expose_provenance
34pub tracked struct PointsTowithDealloc<T> {
35    pub tracked points_to: PointsTo<T>,
36    // The Dealloc permission is only valid with non-zero size.
37    pub tracked dealloc: Option<Dealloc>,
38}
39
40impl<T> Inv for PointsTowithDealloc<T> {
41    open spec fn inv(self) -> bool {
42        // This alignment is to enable the conversion between PointsTo<T> and PoinstToRaw
43        &&& self.points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0
44        &&& match self.dealloc {
45            Some(dealloc) => {
46                &&& vstd::layout::size_of::<T>() > 0
47                &&& self.points_to.ptr().addr() == dealloc.addr()
48                &&& self.points_to.ptr()@.provenance == dealloc.provenance()
49                &&& dealloc.size() == vstd::layout::size_of::<
50                    T,
51                >()
52                // By definition in raw_ptr, the alignment of Dealloc is determined by alloc and it idoes not need to be equal to the alignment of T.
53                // This alignment requirement is to ensure correctness of allocation and deallocation.
54                &&& valid_layout(size_of::<T>(), dealloc.align() as usize)
55            },
56            None => { vstd::layout::size_of::<T>() == 0 },
57        }
58    }
59}
60
61impl<T> PointsTowithDealloc<T> {
62    pub open spec fn ptr(self) -> *mut T {
63        self.points_to.ptr()
64    }
65
66    pub open spec fn addr(self) -> usize {
67        self.ptr().addr()
68    }
69
70    pub open spec fn is_init(self) -> bool {
71        self.points_to.is_init()
72    }
73
74    pub open spec fn is_uninit(self) -> bool {
75        self.points_to.is_uninit()
76    }
77
78    pub open spec fn value(self) -> T {
79        self.points_to.value()
80    }
81
82    pub open spec fn dealloc_aligned(self) -> bool {
83        match self.dealloc {
84            Some(dealloc) => { dealloc.align() == vstd::layout::align_of::<T>() },
85            None => true,
86        }
87    }
88
89    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &PointsTo<T>)
90        returns
91            &self.points_to,
92    {
93        &self.points_to
94    }
95
96    pub proof fn tracked_get_points_to(tracked self) -> (tracked ret: PointsTo<T>)
97        returns
98            self.points_to,
99    {
100        self.points_to
101    }
102
103    pub proof fn new(
104        tracked points_to: PointsTo<T>,
105        tracked dealloc: Option<Dealloc>,
106    ) -> (tracked ret: Self)
107        requires
108            match dealloc {
109                Some(dealloc) => {
110                    &&& vstd::layout::size_of::<T>() > 0
111                    &&& valid_layout(size_of::<T>(), dealloc.align() as usize)
112                    &&& points_to.ptr().addr() == dealloc.addr()
113                    &&& points_to.ptr()@.provenance == dealloc.provenance()
114                    &&& dealloc.size() == vstd::layout::size_of::<T>()
115                },
116                None => { vstd::layout::size_of::<T>() == 0 },
117            },
118        ensures
119            ret.inv(),
120        returns
121            (PointsTowithDealloc { points_to, dealloc }),
122    {
123        points_to.is_aligned();
124        PointsTowithDealloc { points_to, dealloc }
125    }
126
127    pub proof fn new_non_zero_size(
128        tracked points_to: PointsTo<T>,
129        tracked dealloc: Dealloc,
130    ) -> (tracked ret: Self)
131        requires
132            0 < vstd::layout::size_of::<T>(),
133            valid_layout(size_of::<T>(), dealloc.align() as usize),
134            points_to.ptr().addr() == dealloc.addr(),
135            points_to.ptr()@.provenance == dealloc.provenance(),
136            dealloc.size() == vstd::layout::size_of::<T>() as int,
137            dealloc.align() == vstd::layout::align_of::<T>(),
138        ensures
139            ret.inv(),
140        returns
141            (PointsTowithDealloc { points_to, dealloc: Some(dealloc) }),
142    {
143        points_to.is_aligned();
144        PointsTowithDealloc { points_to, dealloc: Some(dealloc) }
145    }
146
147    pub proof fn new_zero_size(tracked points_to: PointsTo<T>) -> (tracked ret: Self)
148        requires
149            vstd::layout::size_of::<T>() == 0,
150        ensures
151            ret.inv(),
152        returns
153            (PointsTowithDealloc { points_to, dealloc: None }),
154    {
155        points_to.is_aligned();
156        PointsTowithDealloc { points_to, dealloc: None }
157    }
158
159    pub proof fn into_raw(tracked self) -> (tracked ret: (PointsToRaw, Option<Dealloc>))
160        requires
161            self.inv(),
162            self.is_uninit(),
163        ensures
164            match ret.1 {
165                Some(dealloc) => {
166                    &&& vstd::layout::size_of::<T>() > 0
167                    &&& dealloc.addr() == self.addr()
168                    &&& dealloc.addr() as int % vstd::layout::align_of::<T>() as int == 0
169                    &&& dealloc.size() == vstd::layout::size_of::<T>() as int
170                    &&& dealloc.provenance() == ret.0.provenance()
171                    &&& ret.0.is_range(dealloc.addr() as int, vstd::layout::size_of::<T>() as int)
172                },
173                None => { &&& vstd::layout::size_of::<T>() == 0 },
174            },
175    {
176        let tracked points_to_raw = self.points_to.into_raw();
177        (points_to_raw, self.dealloc)
178    }
179}
180
181} // verus!
vstd_extra/raw_ptr_extra.rs

vstd_extra/
raw_ptr_extra.rs
