pub struct PCell<V> { /* private fields */ }Expand description
PCell<V> (which stands for “permissioned call”) is the primitive Verus Cell type.
Technically, it is a wrapper around
core::cell::UnsafeCell<core::mem::MaybeUninit<V>>, and thus has the same runtime
properties: there are no runtime checks (as there would be for Rust’s traditional
core::cell::RefCell).
Its data may be uninitialized.
Furthermore (and unlike both
core::cell::Cell and
core::cell::RefCell),
a PCell<V> may be Sync (depending on V).
Thanks to verification, Verus ensures that access to the cell is data-race-free.
PCell uses a ghost permission token similar to simple_pptr::PPtr – see the simple_pptr::PPtr
documentation for the basics.
For PCell, the associated type of the permission token is cell::PointsTo.
Differences from PPtr.
The key difference is that, whereas simple_pptr::PPtr represents a fixed address in memory,
a PCell has no fixed address because a PCell might be moved.
As such, the pcell.id() does not correspond to a memory address; rather,
it is a unique identifier that is fixed for a given cell, even when it is moved.
The arbitrary ID given by pcell.id() is of type CellId.
Despite the fact that it is, in some ways, “like a pointer”, note that
CellId does not support any meangingful arithmetic,
has no concept of a “null ID”,
and has no runtime representation.
Also note that the PCell might be dropped before the PointsTo token is dropped,
although in that case it will no longer be possible to use the PointsTo in exec code
to extract data from the cell.
Example (TODO)
Implementations§
source§impl<V> PCell<V>
impl<V> PCell<V>
sourcepub const exec fn empty() -> pt : (PCell<V>, Tracked<PointsTo<V>>)
pub const exec fn empty() -> pt : (PCell<V>, Tracked<PointsTo<V>>)
pt.1@@ === pcell_opt![pt.0.id() => Option::None],Return an empty (“uninitialized”) cell.
sourcepub const exec fn new(v: V) -> pt : (PCell<V>, Tracked<PointsTo<V>>)
pub const exec fn new(v: V) -> pt : (PCell<V>, Tracked<PointsTo<V>>)
(pt.1@@
=== PointsToData {
pcell: pt.0.id(),
value: Option::Some(v),
}),sourcepub exec fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
pub exec fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, v: V)
old(perm)@ === pcell_opt![self.id() => Option::None],perm@ === pcell_opt![self.id() => Option::Some(v)],sourcepub exec fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> v : V
pub exec fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> v : V
self.id() === old(perm)@.pcell,old(perm)@.value.is_Some(),perm@.pcell === old(perm)@.pcell,perm@.value === Option::None,v === old(perm)@.value.get_Some_0(),sourcepub exec fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> out_v : V
pub exec fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> out_v : V
self.id() === old(perm)@.pcell,old(perm)@.value.is_Some(),perm@.pcell === old(perm)@.pcell,perm@.value === Option::Some(in_v),out_v === old(perm)@.value.get_Some_0(),sourcepub exec fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> v : &'a V
pub exec fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> v : &'a V
self.id() === perm@.pcell,perm@.value.is_Some(),*v === perm@.value.get_Some_0(),sourcepub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> v : V
pub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> v : V
self.id() === perm@.pcell,perm@.value.is_Some(),v === perm@.value.get_Some_0(),