Expand description
Tools and reasoning principles for raw pointers. The tools here are meant to address “real Rust pointers, including all their subtleties on the Rust Abstract Machine, to the largest extent that is reasonable.”
For a gentler introduction to some of the concepts here, see PPtr, which uses a much-simplified pointer model.
Pointer model
A pointer consists of an address (ptr.addr() or ptr as usize), a provenance ptr@.provenance,
and a ptr@.metadata (which is trivial except for pointers to non-sized types).
Note that in spec code, pointer equality requires all 3 to be equal, whereas runtime equality (eq)
only compares addresses and metadata.
*mut T vs. *const T doesn’t have any semantic different and Verus treats them as the same;
they can be seamlessly cast to and fro.
Structs
- Permission to perform a deallocation with the global allocator
- Permission to access possibly-initialized, typed memory.
- PointsToRaw Variable-sized uninitialized memory.
- Model of a pointer
*mut Tor*const Tin Rust’s abstract machine
Enums
- Represents (typed) contents of memory.
- Metadata