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_;
11verus_! {
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
125impl<T: ?Sized> PCell<T> {
126 /// A unique ID for the cell.
127 pub uninterp spec fn id(&self) -> CellId;
128
129 /// Construct a new `PCell` with a fresh [`id`](Self::id).
130 #[inline(always)]
131 #[verifier::external_body]
132 pub const fn new(v: T) -> (pt: (PCell<T>, Tracked<PointsTo<T>>))
133 where T: Sized
134 ensures
135 pt.1@.id() == pt.0.id() && pt.1@.value() == v
136 opens_invariants none
137 no_unwind
138 {
139 let p = PCell { ucell: ManuallyDrop::new(UnsafeCell::new(v)) };
140 (p, Tracked::assume_new())
141 }
142
143 #[inline(always)]
144 #[verifier::external_body]
145 pub fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<T>>) -> (v: &'a T)
146 requires
147 self.id() == perm.id(),
148 ensures
149 v == perm.value(),
150 opens_invariants none
151 no_unwind
152 {
153 // SAFETY: We can take a shared reference since we have the shared PointsTo
154 unsafe { &(*(*self.ucell).get()) }
155 }
156
157 #[inline(always)]
158 #[verifier::external_body]
159 pub fn borrow_mut<'a>(&'a self, Tracked(perm): Tracked<&'a mut PointsTo<T>>) -> (v: &'a mut T)
160 requires
161 self.id() == perm.id(),
162 ensures
163 &*v == old(perm).value(),
164 &*final(v) == final(perm).value(),
165 final(perm).id() == self.id(),
166 opens_invariants none
167 no_unwind
168 {
169 // SAFETY: We can take a mutable reference since we have the mutable PointsTo
170 unsafe { &mut (*(*self.ucell).get()) }
171 }
172
173 #[inline(always)]
174 #[verifier::external_body]
175 pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<T>>) -> (v: T)
176 where T: Sized
177 requires
178 self.id() == perm.id(),
179 ensures
180 v == *perm.value(),
181 opens_invariants none
182 no_unwind
183 {
184 // Note that for an UnsafeCell, intro_inner is a safe operation, whereas for PCell,
185 // we require the Tracked permission.
186 ManuallyDrop::into_inner(self.ucell).into_inner()
187 }
188
189 ////// Trusted core ends here
190
191 #[inline(always)]
192 #[verifier::external_body]
193 pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<T>>, in_v: T) -> (out_v: T)
194 where T: Sized
195 requires
196 self.id() == old(perm).id(),
197 ensures
198 final(perm).id() == old(perm).id(),
199 *final(perm).value() == in_v,
200 out_v == *old(perm).value(),
201 opens_invariants none
202 no_unwind
203 {
204 let mut v = in_v;
205 core::mem::swap(&mut v, self.borrow_mut(Tracked(perm)));
206 v
207 }
208
209 #[inline(always)]
210 pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<T>>, in_v: T)
211 where T: Sized
212 requires
213 self.id() == old(perm).id()
214 ensures
215 final(perm).id() == old(perm).id(),
216 *final(perm).value() == in_v,
217 opens_invariants none
218 no_unwind
219 {
220 let _out = self.replace(Tracked(&mut *perm), in_v);
221 }
222
223 #[inline(always)]
224 pub fn read(&self, Tracked(perm): Tracked<&PointsTo<T>>) -> (out_v: T)
225 where T: Copy + Sized
226 requires
227 self.id() == perm.id()
228 returns
229 *perm.value()
230 opens_invariants none
231 no_unwind
232 {
233 *self.borrow(Tracked(perm))
234 }
235}
236
237}