Module raw_ptr

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 metadata 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 do not have any semantic difference and Verus treats them as the same; they can be seamlessly cast to and fro.

Structs

Dealloc

Permission to perform a deallocation with the global allocator.

DeallocData

Data associated with a Dealloc permission.

IsExposed

Tracked object that indicates a given provenance has been exposed.

PointsTo

Permission to access possibly-initialized, typed memory.

PointsToData

Data associated with a PointsTo permission. We keep track of both the pointer and the (potentially uninitialized) value it points to.

PointsToRaw

Variable-sized uninitialized memory.

Provenance

Provenance

PtrData

Model of a pointer *mut T or *const T in Rust’s abstract machine. In addition to the address, each pointer has its corresponding provenance and metadata.

SharedReference

This is meant to be a replacement for &'a T that allows Verus to keep track of not just the T value but the pointer as well. It would be better to get rid of this and use normal reference types &'a T, but there are a lot of unsolved implementation questions. The existence of SharedReference<'a, T> is a stop-gap.

Enums

MemContents

Represents (typed) contents of memory.

Functions

_verus_external_fn_specification_3__60__32__42__32_mut_32_T_32_as_32_PartialEq_32__60__32__42__32_mut_32_T_32__62__32__62__32__58__58__32_eq^⚠

_verus_external_fn_specification_4__60__32__42__32_const_32_T_32_as_32_PartialEq_32__60__32__42__32_const_32_T_32__62__32__62__32__58__58__32_eq^⚠

_verus_external_fn_specification_5_core_32__58__58__32_ptr_32__58__58__32_null^⚠

_verus_external_fn_specification_6_core_32__58__58__32_ptr_32__58__58__32_null__mut^⚠

allocate

axiom_ptr_mut_from_data

cast_array_ptr_to_slice_ptr

cast_ptr_to_thin_ptr

cast_ptr_to_usize

deallocate

expose_provenance

group_raw_ptr_axioms

ptr_from_data

ptr_mut_from_data

ptr_mut_read

ptr_mut_write

ptr_null

ptr_null_mut

ptr_ref

ptr_ref2

ptrs_mut_eq

ptrs_mut_eq_sized

spec_cast_array_ptr_to_slice_ptr

spec_cast_ptr_to_thin_ptr

spec_cast_ptr_to_usize

with_exposed_provenance

Type Aliases

Metadata

Metadata