vstd/cell/pcell.rs
1#![allow(unused_imports)]
2
3use super::super::prelude::*;
4use super::CellId;
5use super::pcell_maybe_uninit::*;
6use core::cell::UnsafeCell;
7use core::marker::PhantomData;
8use core::mem::ManuallyDrop;
9
10use verus as verus_skip_verusfmt;
11verus_skip_verusfmt! {
12
13/**
14`PCell<T>` (which stands for "permissioned cell") is the most primitive Verus `Cell` type.
15It can often be used as a replacement for Rust's [`UnsafeCell`], and it can serve
16as a basis for verifying many other interior-mutable types
17(e.g., [`InvCell`](super::invcell::InvCell),
18[`RefCell`](https://github.com/verus-lang/verus/blob/main/examples/state_machines/tutorial/ref_cell.rs)).
19
20`PCell` uses a _ghost permission token_ similar to [`simple_pptr::PPtr`](super::super::simple_pptr) -- see the [`simple_pptr::PPtr`](super::super::simple_pptr)
21documentation for the basics.
22For `PCell`, the associated type of the permission token is [`PointsTo`].
23
24If you want a cell that can be optionally initialized, see [`pcell_maybe_uninit::PCell`](super::pcell_maybe_uninit::PCell).
25
26### Differences from `PPtr`.
27
28Whereas [`simple_pptr::PPtr`](super::super::simple_pptr) represents a fixed address in memory,
29a `PCell` has _no_ fixed address because a `PCell` might be moved.
30As such, the [`pcell.id()`](PCell::id) does not correspond to a memory address; rather,
31it is a unique identifier that is fixed for a given cell, even when it is moved.
32
33The arbitrary ID given by [`pcell.id()`](PCell::id) is of type [`CellId`].
34Despite the fact that it is, in some ways, "like a pointer", note that
35`CellId` does not support any meangingful "pointer arithmetic,"
36has no concept of a "null ID",
37and has no runtime representation.
38
39### Differences from [`UnsafeCell`](core::cell::UnsafeCell).
40
41Though inspired by `UnsafeCell`, `PCell` is not quite the same thing.
42The differences include:
43
44 * `PCell<T>` **does not call the destructor of `T` when it goes out of scope**.
45 Technically speaking, `PCell<T>` is actually implemented via
46 `ManuallyDrop<UnsafeCell<T>>`. This is because dropping the contents is unsound
47 if the `PointsTo<T>` is not also reclaimed. To drop a `PCell<T>` without leaking,
48 call [`into_inner`](Self::into_inner) with the corresponding `PointsTo`.
49
50 * `PCell<T>` _always_ implements `Send` and `Sync`, regardless of the type `T`.
51 Instead, it is `PointsTo<T>` where the marker traits matter.
52 (It doesn't matter if you move the bytes to another thread if you can't access them.)
53
54### Example
55
56```rust,ignore
57use vstd::prelude::*;
58use vstd::cell::pcell as pc;
59
60verus! {
61
62fn example_pcell() {
63 let (cell, Tracked(mut points_to)) = pc::PCell::new(5);
64
65 assert(points_to.id() == cell.id());
66 assert(points_to.value() == 5);
67
68 cell.write(Tracked(&mut points_to), 17);
69
70 assert(points_to.id() == cell.id());
71 assert(points_to.value() == 17);
72
73 let x = cell.into_inner(Tracked(points_to));
74 assert(x == 17);
75}
76
77} // verus!
78```
79*/
80
81#[verifier::external_body]
82#[verifier::accept_recursive_types(T)]
83pub struct PCell<T: ?Sized> {
84 // Unlike UnsafeCell, a PCell's drop should NOT drop the contents (since we do not have
85 // the permissions to access the contents). To prevent this, we need to use ManuallyDrop
86 ucell: ManuallyDrop<UnsafeCell<T>>,
87}
88
89/// `PCell` is _always_ safe to `Send` or `Sync`. Rather, it is the [`PointsTo`] object where `Send` and `Sync` matter.
90/// (It doesn't matter if you move the bytes to another thread if you can't access them.)
91#[verifier::external]
92unsafe impl<T: ?Sized> Sync for PCell<T> { }
93#[verifier::external]
94unsafe impl<T: ?Sized> Send for PCell<T> { }
95
96/// Permission object associated with a [`PCell<T>`].
97///
98/// See the documentation of [`PCell<T>`] for more information.
99#[verifier::external_body]
100#[verifier::reject_recursive_types_in_ground_variants(T)]
101pub tracked struct PointsTo<T: ?Sized> {
102 // Through PhantomData we inherit the Send/Sync marker traits
103 phantom: PhantomData<T>,
104 no_copy: NoCopy,
105}
106
107impl<T: ?Sized> PointsTo<T> {
108 /// The [`CellId`] of the [`PCell`] this permission is associated with.
109 pub uninterp spec fn id(&self) -> CellId;
110
111 // To support ?Sized, the `.value()` has to return a reference.
112 // This restriction is enforced by rust even in spec code.
113
114 /// The contents of the cell.
115 pub uninterp spec fn value(&self) -> &T;
116
117 /// Guarantees that two permissions can not be associated with the same `CellId`.
118 pub axiom fn is_exclusive(tracked &mut self, tracked other: & PointsTo<T>)
119 ensures
120 *final(self) == *old(self),
121 final(self).id() != other.id(),
122 ;
123
124 pub axiom fn borrow(tracked &self) -> (tracked t: &T)
125 ensures t == self.value();
126
127 pub axiom fn borrow_mut(tracked &mut self) -> (tracked t: &mut T)
128 ensures
129 &*t == old(self).value(),
130 final(self).value() == &*final(t),
131 final(self).id() == old(self).id();
132}
133
134impl<T: ?Sized> PCell<T> {
135 /// A unique ID for the cell.
136 pub uninterp spec fn id(&self) -> CellId;
137
138 /// Construct a new `PCell` with a fresh [`id`](Self::id).
139 #[inline(always)]
140 #[verifier::external_body]
141 pub const fn new(v: T) -> (pt: (PCell<T>, Tracked<PointsTo<T>>))
142 where T: Sized
143 ensures
144 pt.1@.id() == pt.0.id() && pt.1@.value() == v
145 opens_invariants none
146 no_unwind
147 {
148 let p = PCell { ucell: ManuallyDrop::new(UnsafeCell::new(v)) };
149 (p, Tracked::assume_new())
150 }
151
152 #[inline(always)]
153 #[verifier::external_body]
154 pub fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<T>>) -> (v: &'a T)
155 requires
156 self.id() == perm.id(),
157 ensures
158 v == perm.value(),
159 opens_invariants none
160 no_unwind
161 {
162 // SAFETY: We can take a shared reference since we have the shared PointsTo
163 unsafe { &(*(*self.ucell).get()) }
164 }
165
166 #[inline(always)]
167 #[verifier::external_body]
168 pub fn borrow_mut<'a>(&'a self, Tracked(perm): Tracked<&'a mut PointsTo<T>>) -> (v: &'a mut T)
169 requires
170 self.id() == perm.id(),
171 ensures
172 &*v == old(perm).value(),
173 &*final(v) == final(perm).value(),
174 final(perm).id() == self.id(),
175 opens_invariants none
176 no_unwind
177 {
178 // SAFETY: We can take a mutable reference since we have the mutable PointsTo
179 unsafe { &mut (*(*self.ucell).get()) }
180 }
181
182 #[inline(always)]
183 #[verifier::external_body]
184 pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<T>>) -> (v: T)
185 where T: Sized
186 requires
187 self.id() == perm.id(),
188 ensures
189 v == *perm.value(),
190 opens_invariants none
191 no_unwind
192 {
193 // Note that for an UnsafeCell, intro_inner is a safe operation, whereas for PCell,
194 // we require the Tracked permission.
195 ManuallyDrop::into_inner(self.ucell).into_inner()
196 }
197
198 ////// Trusted core ends here
199
200 #[inline(always)]
201 pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<T>>, in_v: T) -> (out_v: T)
202 where T: Sized
203 requires
204 self.id() == old(perm).id(),
205 ensures
206 final(perm).id() == old(perm).id(),
207 *final(perm).value() == in_v,
208 out_v == *old(perm).value(),
209 opens_invariants none
210 no_unwind
211 {
212 let mut v = in_v;
213 core::mem::swap(&mut v, self.borrow_mut(Tracked(perm)));
214 v
215 }
216
217 #[inline(always)]
218 pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<T>>, in_v: T)
219 where T: Sized
220 requires
221 self.id() == old(perm).id()
222 ensures
223 final(perm).id() == old(perm).id(),
224 *final(perm).value() == in_v,
225 opens_invariants none
226 no_unwind
227 {
228 let _out = self.replace(Tracked(&mut *perm), in_v);
229 }
230
231 #[inline(always)]
232 pub fn read(&self, Tracked(perm): Tracked<&PointsTo<T>>) -> (out_v: T)
233 where T: Copy + Sized
234 requires
235 self.id() == perm.id()
236 returns
237 *perm.value()
238 opens_invariants none
239 no_unwind
240 {
241 *self.borrow(Tracked(perm))
242 }
243}
244
245}