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

vstd/cell/
pcell.rs
