Struct PCell Copy item path

PCell<T> (which stands for “permissioned cell”) is the most primitive Verus Cell type. It can often be used as a replacement for Rust’s UnsafeCell, and it can serve as a basis for verifying many other interior-mutable types (e.g., InvCell, RefCell).

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 PointsTo.

If you want a cell that can be optionally initialized, see pcell_maybe_uninit::PCell.

§Differences from PPtr.

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 “pointer arithmetic,” has no concept of a “null ID”, and has no runtime representation.

§Differences from UnsafeCell.

Though inspired by UnsafeCell, PCell is not quite the same thing. The differences include:

• PCell<T> does not call the destructor of T when it goes out of scope. Technically speaking, PCell<T> is actually implemented via ManuallyDrop<UnsafeCell<T>>. This is because dropping the contents is unsound if the PointsTo<T> is not also reclaimed. To drop a PCell<T> without leaking, call into_inner with the corresponding PointsTo.

• PCell<T> always implements Send and Sync, regardless of the type T. Instead, it is PointsTo<T> where the marker traits matter. (It doesn’t matter if you move the bytes to another thread if you can’t access them.)

§Example

use vstd::prelude::*;
use vstd::cell::pcell as pc;

verus! {

fn example_pcell() {
    let (cell, Tracked(mut points_to)) = pc::PCell::new(5);

    assert(points_to.id() == cell.id());
    assert(points_to.value() == 5);

    cell.write(Tracked(&mut points_to), 17);

    assert(points_to.id() == cell.id());
    assert(points_to.value() == 17);

    let x = cell.into_inner(Tracked(points_to));
    assert(x == 17);
}

} // verus!