Struct PCellCopy item path

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)