PPtr (which stands for “permissioned pointer”)
is a wrapper around a raw pointer to a heap-allocated V.
This is designed to be simpler to use that Verus’s
more general pointer support,
but also to serve as a better introductory point.
Historically, PPtr was positioned as a “trusted primitive” of Verus,
but now, it is implemented and verified from the more general pointer support,
which operates on similar principles, but which is much precise to Rust’s
pointer semantics.