Chapter 8.3. Safety Property Contracts

RAPx verifies safety through explicit contracts declared in source code. A contract is a logical statement about pointer validity, numeric bounds, ownership, and other safety properties that RAPx checks against a function's MIR. This chapter covers the two kinds of contract (§8.3.1), how to attach them to code (§8.3.2), and how to inspect the resolved assertions (§8.3.3).

8.3.1 Contracts

A contract is either a built-in property shipped with RAPx, or a user-defined contract composed from the built-ins.

8.3.1.1 Built-in Properties

The semantics of each property kind are defined in primitive-sp.md. The annotated reference with examples:

Primitive properties

`Alias(p1[, p2])`

Alias accepts one or two target places: the two-argument form Alias(p1, p2) declares that p1 and p2 alias each other; the one-argument form Alias(p) declares an aliasing hazard on p alone, used inside the Ptr2Ref / Drop compound definitions where the other aliasing place (the return reference, or a still-live owner) is implicit. A hazard by default: unproved Alias is reported as a [hazard] entry and contributes to UNSOUND. It is also the mechanism for a no-aliasing precondition — Ptr2Ref(p, T) (and Drop(p, T)) include Alias(p), and a caller declares #[rapx::requires(Ptr2Ref(p, T))] to discharge the callee's hazard. Alias itself is not a safety violation, provided it does not also violate Owning or Alive. psp IV.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Alias(ptr, ret))]
#[rapx::requires(Alias(ptr))]
}

`Align(ptr, Ty)`

ptr % alignment(Ty) == 0 — the pointer satisfies the alignment requirement of Ty. psp I.1.

#![allow(unused)]
fn main() {
#[rapx::requires(Align(ptr, u32))]
}

`Alive(ptr, 'a)`

lifetime(*p) >= l — the allocation is still live and not freed across the lifetime 'a. psp IV.3.

#![allow(unused)]
fn main() {
#[rapx::requires(Alive(ptr, 'a))]
}

`Allocated(ptr[, Ty[, count[, allocator]]])`

Memory belongs to a live allocation. Four argument forms are accepted:

Allocated(ptr, Ty, count, allocator) — ptr points to Ty * count memory allocated by the allocator.
Allocated(ptr, Ty, count) — allocator defaults to global.
Allocated(ptr, Ty) — count defaults to 1, allocator global.
Allocated(ptr) — element type inferred from ptr's pointee, count = 1, allocator global.

psp II.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Allocated(ptr, u8, n, Global))]
#[rapx::requires(Allocated(ptr, u8, n))]
#[rapx::requires(Allocated(ptr, u8))]
#[rapx::requires(Allocated(ptr))]
}

`InBound(slice, index)` / `InBound(ptr[, Ty[, count]])`

The accessed memory lies within the bounds of a single allocated object. Two forms are accepted:

InBound(slice, index) — index into a slice/array; index implements std::slice::SliceIndex (usize or a range type such as Range/RangeInclusive/RangeFrom/RangeTo/RangeFull), expanding to the correct bounds check.
InBound(ptr, Ty, count) — count elements of Ty at ptr.
InBound(ptr, Ty) — count defaults to 1.
InBound(ptr) — element type inferred from ptr's pointee, count = 1.

psp II.3.

#![allow(unused)]
fn main() {
#[rapx::requires(InBound(self, i))]
#[rapx::requires(InBound(ptr, u32, len))]
#[rapx::requires(InBound(ptr, u32))]
#[rapx::requires(InBound(ptr))]
}

`Init(ptr[, Ty[, count]])`

Memory is initialized for count elements of Ty. Stronger than Typed: Init implies Typed but not vice versa. Ty and count may be omitted: a missing Ty is inferred from ptr's pointee, a missing count defaults to 1. psp III.4.

#![allow(unused)]
fn main() {
#[rapx::requires(Init(ptr, T, len))]
#[rapx::requires(Init(ptr, T))]
#[rapx::requires(Init(ptr))]
}

`NonNull(ptr)` / `Null(ptr)`

ptr != 0 — the pointer is not null. psp II.1. Null(ptr) is the inverse — the pointer may be null, used inside any(...) for null-guarded contracts.

#![allow(unused)]
fn main() {
#[rapx::requires(NonNull(ptr))]
#[rapx::requires(any(Null(self), (ValidPtr(self, T, 1), Align(self, T))))]
}

`NonOverlap(indices)` / `NonOverlap(a, b[, T[, count]])`

With one argument, indices is an array [I; N]. NonOverlap(indices) requires every pair of its elements to be non-overlapping under I's indexing rules: usize indices must be distinct, while ranges must not overlap. The array length N comes from its type; this form has no T or count argument. It does not assert that the indices are in bounds. The current verifier parses this form but cannot yet prove it, so checks return UNKNOWN.

With two to four arguments, a and b are pointers to the starts of two memory ranges, each of length sizeof(T) * count bytes. These ranges must be disjoint. If T is omitted, RAPx infers it from the pointers' common pointee type and reports an error if their pointee types differ. If count is omitted, it defaults to 1. psp II.4.

#![allow(unused)]
fn main() {
#[rapx::requires(NonOverlap(src, dst, u32, count))]
#[rapx::requires(NonOverlap(src, dst, u32))]
#[rapx::requires(NonOverlap(src, dst))]
#[rapx::requires(NonOverlap(indices))]
}

`NonVolatile(p[, T[, len]])`

Memory is not volatile — no other thread writes to the region (p, sizeof(T) * len). T and len may be omitted: a missing T is inferred from p's pointee, a missing len defaults to 1. Assumed satisfied — the VM does not model volatile access. psp V.2.

#![allow(unused)]
fn main() {
#[rapx::requires(NonVolatile(ptr, T, count))]
#[rapx::requires(NonVolatile(ptr, T))]
#[rapx::requires(NonVolatile(ptr))]
}

`NoPadding(T)`

The type T has no padding bytes — padding(T) == 0. psp I.3.

#![allow(unused)]
fn main() {
#[rapx::requires(NoPadding(T))]
}

`Opened(fd)`

An OS resource (e.g. file descriptor) is valid and open. psp V.3. Declared but not yet verified — the checker returns Unknown.

#![allow(unused)]
fn main() {
#[rapx::requires(Opened(fd))]
}

`Owning(ptr[, T[, count]])`

ownership(*p) == none — the pointer is the sole carrier of ownership; no live owner aliases the pointee. T and count may be omitted: a missing T is inferred from ptr's pointee, a missing count defaults to 1. psp IV.1.

#![allow(unused)]
fn main() {
#[rapx::invariant(Owning(ptr))]
#[rapx::invariant(Owning(ptr, T))]
#[rapx::invariant(Owning(ptr, T, count))]
}

`Pinned(p, l)`

∀t ∈ 0..l, &(*p)_0 = p_t — the target is pinned for lifetime l (its address will not change). psp V.1. Declared but not yet verified — the checker returns Unknown.

#![allow(unused)]
fn main() {
#[rapx::requires(Pinned(ptr, 'a))]
}

`Size(T, c)`

sizeof(T) = c — the type T has the specified byte size. Three forms for c: psp I.2.

Constant: Size(T, 1) — exact byte size (implies T: Sized). Size(T, 0) for ZST.
sized: Size(T, sized) — T: Sized, non-ZST (default for generics).
unsized: Size(T, unsized) — !Sized (for ?Sized bounds).

#![allow(unused)]
fn main() {
#[rapx::requires(Size(T, 1))]
#[rapx::requires(Size(T, sized))]
}

`SplitTransmute([Src], [Dst])`

A Typed variant for slice-level transmutation: every size_of(Dst)-byte window within [Src] is a valid Dst value, without requiring alignment. Both [Src] and [Dst] are slice types.

#![allow(unused)]
fn main() {
#[rapx::requires(SplitTransmute([T], [U]))]
}

`Trait(T, trait)`

The type T implements the specified trait — trait ∈ traitimpl(T). psp V.4.

#![allow(unused)]
fn main() {
#[rapx::requires(Trait(T, Copy))]
}

`Typed(ptr[, Ty[, count]])`

The memory at ptr satisfies TypeInvariant(T) — it was created as type T and has not been type-punned. Weaker than Init: does not require initialized content. Ty and count may be omitted: a missing Ty is inferred from ptr's pointee (a MaybeUninit<T> pointee is trivially "typed"), a missing count defaults to 1. psp III.6.

#![allow(unused)]
fn main() {
#[rapx::requires(Typed(ptr, T, count))]
#[rapx::requires(Typed(ptr, T))]
#[rapx::requires(Typed(ptr))]
}

`Unreachable`

The code path is unreachable. psp V.5. Declared but not yet verified — the checker returns Unknown.

#![allow(unused)]
fn main() {
#[rapx::requires(Unreachable)]
}

`Unwrap(x, variant)`

unwrap(x) = variant — the Option/Result is in the expected variant (Some, Ok, Err). psp III.5. Declared but not yet verified — the checker returns Unknown.

#![allow(unused)]
fn main() {
#[rapx::requires(Unwrap(self, Some))]
#[rapx::requires(Unwrap(self, Ok))]
}

`ValidCStr(ptr, len)`

The C string at ptr is null-terminated at byte position len with no interior null bytes. psp III.3.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidCStr(ptr, 1))]
}

`ValidNum(predicate)` / `ValidNum(value, interval)`

Numeric constraints. Two forms: psp III.1.

ValidNum(predicate) — a comparison expression with operators <, <=, >, >=, ==, !=.
ValidNum(value, interval) — a value constrained to a range. The interval is an array literal [lo, hi] (inclusive both ends), a string "[lo, hi]" where [/] is inclusive and (/) is exclusive (either side may be left empty for an unbounded bound), or a bare integer n (shorthand for value == n).

#![allow(unused)]
fn main() {
#[rapx::requires(ValidNum(index < len))]
#[rapx::requires(ValidNum(size_of::<T>() * len <= isize::MAX))]
#[rapx::requires(ValidNum(mid, [0, len]))]           // 0 <= mid <= len
#[rapx::requires(ValidNum(mid, "[0, self.len]"))]    // 0 <= mid <= self.len
#[rapx::requires(ValidNum(x, "[0, 10)"))]            // 0 <= x < 10
}

`ValidString(ptr, u8, len)` / `ValidString(iter)`

The byte data is valid UTF-8. Two forms: psp III.2.

ValidString(ptr, u8, len) — len bytes at ptr are valid UTF-8.
ValidString(iter) — an Iterator<Item = u8>; the length is derived from the backing byte buffer.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidString(v, u8, 1))]
#[rapx::requires(ValidString(bytes))]
}

`ValidTransmute(Src, Dst)`

A Typed variant for transmutation: memory of type Src satisfies TypeInvariant(Dst) when Dst is structurally composed of Src (exact type equality, array/tuple/simd/transparent decomposition). Both args are types.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTransmute(u32, [u8; 4]))]
}

Compound properties

`Deref(ptr[, Ty[, count]])`

Allocated ∧ InBound — the pointer can be safely dereferenced. Ty and count may be omitted: a missing Ty is inferred from ptr's pointee, a missing count defaults to 1. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Deref(ptr, u32, count))]
#[rapx::requires(Deref(ptr, u32))]
#[rapx::requires(Deref(ptr))]
}

`Drop(ptr[, T])`

ValidPtr(p, T) ∧ Alias(p) — dropping *ptr (e.g. ManuallyDrop::drop(&mut slot)): the pointee is a valid value, and the freed memory must not be used again. T may be omitted and is then inferred from ptr's pointee.

#![allow(unused)]
fn main() {
#[rapx::requires(Drop(ptr, T))]
#[rapx::requires(Drop(ptr))]
}

`Layout(ptr, layout)`

ValidNum(ptr % layout.align == 0) ∧ Allocated(ptr, u8, layout.size, Global) — the pointer matches the layout's size and alignment from a prior allocation. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Layout(ptr, layout))]
}

`Ptr2Ref(ptr, T)`

Init(p, T, 1) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p) — a raw pointer meets all requirements for sound reference conversion. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(Ptr2Ref(ptr, T))]
}

`Ptr2RefUninit(ptr, T)`

Typed(p, T) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p) — a raw pointer meets all requirements for sound &MaybeUninit<T> / &mut MaybeUninit<T> conversion (the content need not be initialized — Init is deliberately absent).

#![allow(unused)]
fn main() {
#[rapx::requires(Ptr2RefUninit(ptr, T))]
}

`ValidPtr(ptr, Ty, count)`

NonNull(ptr) ∧ (Size(Ty, 0) ∨ Deref(ptr, Ty, count)) — the pointer is non-null and dereferenceable (in-bounds within a live allocation). For a ZST the dereference requirement is vacuous, so non-nullness alone suffices; a null pointer is never valid. primitive-sp §2.2.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidPtr(ptr, u32, len))]
}

`ValidTraitObj(ptr)`

NonNull(ptr) — a pointer to an unsized value whose metadata is read (size_of_val, align_of_val, for_value_raw, min_align_of_val). Enforces non-null; the pointee's alignment/validity is not checked because the single-argument form carries no element type.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTraitObj(ptr))]
}

`ZstAwareInBound(ptr, T, end_or_len)` / `ZstAwareInit(ptr, T, end_or_len)`

InBound / Init with ZST-aware element counting: 0 elements when T is zero-sized, otherwise (end_or_len - ptr) / size_of(T) elements.

#![allow(unused)]
fn main() {
#[rapx::requires(ZstAwareInBound(ptr, T, end_or_len))]
}

Send / Sync predicates

The following type-level predicates discharge Send/Sync marker-trait obligations. Send requires ContainNoType(Self, Rc, Ref, …) ∧ (NoRawPtr(Self) || TamedRawPtr(Self)); Sync requires RefSend(Self) ∧ ContainNoType(Self, Rc, Cell, UnsafeCell, …) (the composition is declared in std-trait-ensures.json).

`ContainNoType(T, bad1, ...)`

T does not structurally contain any of the listed types (one or more negative type names). Used to discharge Send/Sync obligations.

#![allow(unused)]
fn main() {
#[rapx::requires(ContainNoType(T, UnsafeCell))]
}

`NoRawPtr(T)`

The type T structurally contains no raw pointers — recursively through its fields, generic arguments, and nested types. Used to discharge Send obligations.

#![allow(unused)]
fn main() {
#[rapx::requires(NoRawPtr(T))]
}

`NoInternalMut(T)`

The type T has no interior mutation through raw pointers.

#![allow(unused)]
fn main() {
#[rapx::requires(NoInternalMut(T))]
}

`UniInternalMut(T)`

The type T has unique interior mutation (an exclusive owner, with no aliasing Clone).

#![allow(unused)]
fn main() {
#[rapx::requires(UniInternalMut(T))]
}

`AtomicUpdate(T)`

The type T updates its raw pointers under synchronization or atomically.

#![allow(unused)]
fn main() {
#[rapx::requires(AtomicUpdate(T))]
}

`RefSend(T)`

&T: Send — the type can be shared across threads: every interior-mutability / raw-pointer field of T is guarded by a synchronization primitive (mutex/rwlock/atomic).

#![allow(unused)]
fn main() {
#[rapx::requires(RefSend(T))]
}

`TamedRawPtr(T, ptr)`

Allocated(ptr, T, 1) ∧ Owning(ptr) ∧ (NoInternalMut(T) || UniInternalMut(T) || AtomicUpdate(T)) — a raw-pointer field that is allocated and owning, and whose updates are read-only, exclusive, or atomic.

Note the argument order: TamedRawPtr is a type-level predicate, so the type T comes first (like NoRawPtr/RefSend); ptr names the struct's raw-pointer field and is normally not written by hand — inside a Send/Sync obligation it is auto-bound from the struct's #[rapx::invariant(Allocated(ptr))] / Owning(ptr), so the usual spelling is TamedRawPtr(Self).

#![allow(unused)]
fn main() {
#[rapx::requires(TamedRawPtr(T, ptr))]
}

8.3.1.2 User-Defined Contracts

In addition to the built-in tags, you can define new named contracts inside your crate with the pred! macro (from rapx_macros). A user-defined contract is a boolean combination of the primitive properties: it adds no new semantics — it is a pure front-end that expands to ordinary Property objects, so no rapx rebuild is required.

To use pred!, add rapx-macros as a dependency and enable the rapx tool attribute — the same nightly register_tool setup used for every #[rapx::...] attribute (see §8.3.2.1):

[dependencies]
rapx-macros = "0.7.53"

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]
fn main() {
}

A def is written as a pred! block of the form Name(params) { body }. Its parameters are typed Ptr (a target place), Ty (a type), Expr (a numeric expression), or Ident (an identifier such as a trait name, enum variant, allocator, or lifetime). A trailing ? marks a parameter optional — omitted trailing optional parameters are dropped from the expanded inner calls, letting the target primitive apply its own default (e.g. an inferred element type, or count = 1), as in the bundled Deref(p: Ptr, T: Ty?, n: Expr?). By convention the contract name is CamelCase, matching the built-in compounds (ValidPtr, Deref, Ptr2Ref, …):

#![allow(unused)]
fn main() {
use rapx_macros::pred;

pred!(MySafeRead(p: Ptr, T: Ty, n: Expr) { NonNull(p) && Align(p, T) && Allocated(p, T, n) });
}

The block is not compiled as Rust: the macro serializes its source text into a #[rapx::def_property("...")] tool attribute that the verifier parses at analysis time. Once defined, the name becomes a first-class tag usable wherever a property is expected:

#![allow(unused)]
fn main() {
#[rapx::requires(MySafeRead(ptr, u8, len))]
pub unsafe fn read_byte(ptr: *const u8, len: usize) -> u8 {
    unsafe { *ptr }
}
}

DSL grammar

A def body is parsed by a small pest grammar (the single source of truth, in grammar.pest). The surface:

Boolean composition — the body is a boolean combination of Tag(args) calls: || separates disjuncts, && joins conjuncts, and parentheses allow arbitrary nesting.

def_body = or_expr
or_expr = and_expr ("||" and_expr)*
and_expr = def_leaf ("&&" def_leaf)*
def_leaf = tag_call | "(" or_expr ")"

#![allow(unused)]
fn main() {
pred!(DerefOrNull(p: Ptr, T: Ty, n: Expr) { Null(p) || (Allocated(p, T, n) && InBound(p, T, n)) });
}

Argument expressions — a tag's arguments are numeric/place expressions with the usual operators:

Layer	Operators
comparison	`==` `!=` `<` `<=` `>` `>=`
bitwise	`\\|` `^` `&`
arithmetic	`+` `-` `*` `/` `%`
unary	`!` `-`

Built-in functions — size_of(T), align_of(T), len(x), min(a, b), max(a, b). The turbofish forms size_of::<T>() / align_of::<T>() (optionally with a std::mem:: / core::mem:: path prefix) are also accepted; size_of(T) remains the preferred shorthand.

Places and projections — a place is self, return, Arg_N, or an identifier, optionally followed by projections:

.0 / .name — field access (self.0, self.ptr).
.unwrap_some() — unwrap an Option payload (head.unwrap_some()).
.iter() — iterate the elements of a container (buckets.iter()).
.len() — query the receiver length (self.len()).

Only these projections and the equivalent length forms len(x) and x.len() are resolved. Both refer to the receiver’s len() method; for a local method whose result RAPx cannot derive, the predicate remains UNKNOWN. Getter-style method calls are not — write the field access instead: layout.size, not layout.size() (the field is size, so the .size form resolves and the .size() form does not).

Type-level constants — T::MAX, T::MIN, T::BITS (e.g. isize::MAX).

Conditionals — if cond { e1 } else { e2 } is an expression usable in argument (Expr) position, e.g. to special-case ZSTs (as in the std-challenge-18 case study):

#![allow(unused)]
fn main() {
pred!(ZstAwareInBound(ptr: Ptr, T: Ty, end_or_len: Expr) {
    InBound(ptr, T, if size_of(T) == 0 { 0 } else { (end_or_len - ptr) / size_of(T) })
});
}

!self.is_empty() requires the local is_empty() method to return false (e.g. ValidNum(!self.is_empty())). RAPx uses the method result when available and does not assume that is_empty() is equivalent to len() == 0. Other receiver forms remain UNKNOWN if their method cannot be resolved.

A def body may reference other defs as well as primitives. The same mechanism defines RAPx's built-in compound properties (ValidPtr, Deref, Ptr2Ref, …) in std-compound-properties.rs — using the same Name(params) { body } syntax, so a user can read the bundled compounds and write their own the same way. See tests/verify_units/dsl_custom_def for a complete SOUND example.

8.3.2 Contract Annotation

8.3.2.1 Direct Annotation

Contracts written in source use register_tool tool attributes; the crate (or module) must enable the tool:

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]
fn main() {
}

Three attributes carry contracts:

#[rapx::requires(...)] — a precondition on an (usually unsafe) function. Each attribute holds one property (optionally with kind = ...); repeat the attribute for multiple properties.
#[rapx::invariant(...)] — a struct-level invariant that must hold for every instance at all observable points (see Chapter 8.4).
#[rapx::verify] — marks a function as a verification entry point for --mode targeted (Chapter 8.1.2).

#![allow(unused)]
fn main() {
#[rapx::requires(ValidPtr(ptr, u32, len))]
#[rapx::requires(Align(ptr, u32))]
#[rapx::requires(ValidNum(index < len))]
pub unsafe fn write_slice(ptr: *mut u32, len: usize, index: usize) {
    // ...
}
}

The any(D1, D2, ...) combinator expresses a null guard: any(Null(p), (P1(p, ...), P2(p, ...))) — the conjunct properties hold when p is non-null, and the whole contract is vacuously satisfied when p is null.

A property may carry kind = "precond" | "hazard" | "option" metadata (e.g. #[rapx::requires(..., kind = "hazard")]); Alias is always classified hazard, and its precondition role is expressed through Ptr2Ref/Drop, which include Alias(p).

Places accepted in annotations: parameter names (self, ptr, index, len), field names in invariant (ptr, cap, head — no self. prefix), field projections (self.0, self.ptr), length calls (self.len() or len(self)), and const generics (N).

8.3.2.2 JSON Contracts

Standard-library functions that cannot be annotated upstream use JSON contracts in std-api-requires.json. Each entry maps a function path to a list of { "tag": ..., "args": [...] } objects:

{
  "core::ptr::const_ptr::add": [
    { "tag": "NonNull", "args": ["self"] },
    { "tag": "Align",   "args": ["self", "T"] },
    { "tag": "InBound", "args": ["self", "T", "count"] }
  ]
}

Argument strings use the same expression grammar as direct annotations. Path lookup first tries an exact match on the cleaned def-path, then falls back to wildcard segment replacement (e.g. core::slice::<impl [T]>::* → core::slice::*).

8.3.3 Inspecting Contracts with `--debug-contracts`

Pass --debug-contracts to see every contract assertion expanded with its semantic meaning. While --prepare-targets (§8.2.3) shows which contracts attach to each verification target, --debug-contracts shows what each contract means — the concrete SMT obligation. Note that --prepare-targets and --debug-contracts are mutually exclusive; run them in separate invocations for both views.

Example output from the linked_list_nonnull case study (continued from §8.2.3):

13:10:58|RAPx|INFO|: ============================================================================
13:10:58|RAPx|INFO|: [rapx::debug-contracts] struct: LinkedList
13:10:58|RAPx|INFO|: ============================================================================
13:10:58|RAPx|INFO|:   [Struct Invariants]:
13:10:58|RAPx|INFO|:   |- Align(head.unwrap_some(), Node<T>)
13:10:58|RAPx|INFO|:   |  (head.unwrap_some() as usize) % align_of::<Node<T>>() == 0
13:10:58|RAPx|INFO|:   |- Allocated(head.unwrap_some(), Node<T>, 1)
13:10:58|RAPx|INFO|:   |  head.unwrap_some() points to a live allocation of size: size_of(Node<T>) * 1
13:10:58|RAPx|INFO|:   |- Typed(head.unwrap_some(), Node<T>)
13:10:58|RAPx|INFO|:   |  *head.unwrap_some() holds TypeInvariant(Node<T>)
13:10:58|RAPx|INFO|:   `- Owning(head.unwrap_some())
13:10:58|RAPx|INFO|:      ownership(*head.unwrap_some()) = none: no live owner aliases the pointee
13:10:58|RAPx|INFO|: 
13:10:58|RAPx|INFO|: |- --- method: pop_front ---------------------------------------------------
13:10:58|RAPx|INFO|: |   fn LinkedList::<T>::pop_front(&mut self: &mut LinkedList<T>) -> std::option::Option<T>
13:10:58|RAPx|INFO|: |   [Unsafe Callees]:
13:10:58|RAPx|INFO|: |   |- fn std::boxed::Box::<T>::from_raw(raw: *mut T) -> std::boxed::Box<T>
13:10:58|RAPx|INFO|: |   | |- Align(raw, T)
13:10:58|RAPx|INFO|: |   | |  (raw as usize) % align_of::<T>() == 0
13:10:58|RAPx|INFO|: |   | |- Allocated(raw, T, 1, Global)
13:10:58|RAPx|INFO|: |   | |  raw points to a live allocation of size: size_of(T) * 1
13:10:58|RAPx|INFO|: |   | |- Typed(raw, T)
13:10:58|RAPx|INFO|: |   | |  *raw holds TypeInvariant(T)
13:10:58|RAPx|INFO|: |   | |- Owning(raw)
13:10:58|RAPx|INFO|: |   | |  ownership(*raw) = none: no live owner aliases the pointee
13:10:58|RAPx|INFO|: |   | `- [hazard] Alias(raw, ret)
13:10:58|RAPx|INFO|: |   |    raw and ret alias each other (hazard)
13:10:58|RAPx|INFO|: |   `- fn std::ptr::NonNull::<T>::as_mut::<'a>(&mut self: &mut std::ptr::NonNull<T>) -> &'a mut T
13:10:58|RAPx|INFO|: |     `- Ptr2Ref(self.0, T)
13:10:58|RAPx|INFO|: |        A raw pointer meets all requirements for sound &/&mut conversion: initialized, aligned, no aliasing conflict.
13:10:58|RAPx|INFO|: 
13:10:58|RAPx|INFO|: ... (8 more methods)

Rust Analysis Platform