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        *self == *old(self),
121        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    // TODO: this should be replaced with borrow_mut
158    #[inline(always)]
159    #[verifier::external_body]
160    pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<T>>, in_v: T) -> (out_v: T)
161        where T: Sized
162        requires
163            self.id() === old(perm).id(),
164        ensures
165            perm.id() === old(perm).id(),
166            *perm.value() === in_v,
167            out_v === *old(perm).value(),
168        opens_invariants none
169        no_unwind
170    {
171        let mut m = in_v;
172        // SAFETY: We can take a mutable reference since we have the mutable PointsTo
173        unsafe {
174            core::mem::swap(&mut m, &mut *(*self.ucell).get());
175        }
176        m
177    }
178
179    #[inline(always)]
180    #[verifier::external_body]
181    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<T>>) -> (v: T)
182        where T: Sized
183        requires
184            self.id() === perm.id(),
185        ensures
186            v === *perm.value(),
187        opens_invariants none
188        no_unwind
189    {
190        // Note that for an UnsafeCell, intro_inner is a safe operation, whereas for PCell,
191        // we require the Tracked permission.
192        ManuallyDrop::into_inner(self.ucell).into_inner()
193    }
194
195    ////// Trusted core ends here
196
197    #[inline(always)]
198    pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<T>>, in_v: T)
199        where T: Sized
200        requires
201            self.id() === old(perm).id()
202        ensures
203            perm.id() === old(perm).id(),
204            *perm.value() === in_v,
205        opens_invariants none
206        no_unwind
207    {
208        let _out = self.replace(Tracked(&mut *perm), in_v);
209    }
210
211    #[inline(always)]
212    pub fn read(&self, Tracked(perm): Tracked<&PointsTo<T>>) -> (out_v: T)
213        where T: Copy + Sized
214        requires
215            self.id() === perm.id()
216        returns
217            *perm.value()
218        opens_invariants none
219        no_unwind
220    {
221        *self.borrow(Tracked(perm))
222    }
223}
224
225}
vstd/cell/pcell.rs

vstd/cell/
pcell.rs
