Chapter 8.5. Verification Approach

The verifier discharges each safety property by symbolic reasoning over the VM state. This chapter first describes the symbolic VM state (§8.5.1), then the deduction rules that read that state (§8.5.2), and finally the special treatment of Alias, which is a hazard by default but also expresses a no-aliasing precondition (§8.5.3).

8.5.1 The Symbolic VM

VM design

The SymbolicVm (vm/mod.rs) is a semantic MIR executor: it executes the MIR items the backward slicer retained (§8.4.2) and directly builds a symbolic state (VmState) with a Z3 term for every value.

Execution proceeds top-to-bottom through the diagram below. run allocates an empty VmState; execute_items binds the parameters to fresh symbolic values, then walks the retained items in forward path order — each MIR statement or terminator is a transfer function that updates the state. At a checkpoint, the state contains the path conditions and memory effects modeled for the retained items. Unsupported operations and truncated inlining can leave a property unproved.

   ProofGoal { path, items: Vec<RelevantItem> }
   (produced by the backward slicer, §8.4.2)
                    │
                    ▼
   SymbolicVm::run(z3_ctx, tcx, goal)        ← stateless, pure input → state
                    │
                    ▼
   VmState::new(...)                      ← empty state (structure below)
                    │
                    ▼
   execute_items(&items)                  ← forward path order
                    │
                    ├─ init_parameters():  _1.._N ← fresh Z3 constants
                    │
                    └─ for item in items:
                          Statement    → exec_statement
                          Terminator   → exec_terminator
                          CalleeEntry  → handle_callee_entry  (save_frame)
                           CalleeExit   → handle_callee_exit   (restore_frame)
                           ContractFact → assert_contract_fact
                      ▼
   VmState ──► PropertyChecker::check ──► Z3 (assert_all + negation-as-failure)

The SymbolicVm takes the MIR of each path as input and maintains the following state during execution (besides the borrowed z3_ctx/tcx handles):

• Frame-scoped (current_frame: FrameState) — saved/restored on inline entry/exit, so a callee reuses MIR locals freely:

  • current_def_id — the function whose body is being executed.
  • local_alloc — the stack allocation backing each local's place. This is the only name → object binding: a local's whole value lives at path == [] and its field values at path == [i, ..] in the path-scoped MemoryContent::values (keyed by the local's allocation and declared type), so there is no local-keyed value table here.

• Path-scoped (everything else) — accumulates across the whole path, including inlined frames:

  • units — the object space: one MemoryUnit per allocation, each holding its allocation shape and its content (the per-byte byte_array plus the concrete byte_written offset set, the typed-value layer values, and the facts); whole values live at path == [] and field values at path == [i, ..].
  • constraints — accumulated solver assertions and the term term_caches.
  • caller_frames — saved caller frames for path-replay inlining.
  • inline — recursive-inline scratch: inline_depth, inline_truncated_terms, arg_referents, deferred_field_writes.
  • alias_hazard_allocs — the root allocations named by every Alias the caller's contract declares (a hazard like Alias(self, ret) or a Ptr2Ref precondition like Alias(self.0)); the alias checker discharges only these, see §8.5.3.

When the recursive inliner hits MAX_INLINE_DEPTH it no longer proceeds on an unconstrained value: the destination gets a distinguishable placeholder term recorded in inline_truncated_terms, and a property whose target value (or a checkpoint argument it reads, or a pointer provenance offset) depends on that term is reported Unknown (InlineDepthExceeded) rather than a spurious proof or failure.

The deduction rules in §8.5.2 read three things out of this state — values, allocations, and provenance — described in the subsections below.

Values and facts

A MIR local's whole value (its rvalue) and each of its field values are both symbolic values (VmValue), stored in MemoryContent::values keyed by (view_ty, path) within the local's allocation (each MemoryUnit is one allocation, so the AllocId is the unit index, not part of the key) — path == [] is the whole value, path == [i, ..] is field i (viewed as view_ty, so a reinterpret cast resolves to the right field view):

VmValue { z3_term, ty, provenance, facts, source }

• z3_term — a Z3 term. For pointer/reference types (&T, *const T, Box<T>, …) it is the address; for scalar types it is the value; for aggregate types it is the base address of the stack slot backing the aggregate.
• ty — the Rust type, for layout queries.
• provenance — Option<Provenance> (see below); None for a scalar.
• facts — the derived value facts (ValueFacts) that serve as the "fast-path flags" of §8.5.2:
  • non_null: bool, init: bool, in_bounds: bool.
  • align_n: Option<Int> — the pointer's alignment lower bound. Here Int is z3::ast::Int, a Z3 term, not a Rust integer: Some(n) asserts z3_term % n == 0, i.e. the pointer is at least n-aligned (alignments are powers of two, so "at least n" ⇔ "a multiple of n"). For a concrete type n is a constant term (Some(8)); for a generic type n is the symbolic constant align_T — a fresh Z3 constant shared per type — so a generic T is carried as a symbol, not a number. None records no alignment fact (e.g. a raw pointer *mut T), independent of whether T is generic.
• source — a ValueSource carrying any extra semantics beyond z3_term/type/provenance:
  • None — a plain value.
  • FieldOffset — a compile-time offset_of! field offset, propagated to a pointer's provenance when used as an add/byte_add offset.
  • Discriminant(Int) — a symbolic enum variant index (e.g. Iterator::next returns Some(x) iff !is_empty), tying switchInt branches to the real condition instead of a fresh symbol.
  • Comparison { lhs, rhs, op, cond } — a comparison result (Le/Lt/Ge/Gt/Eq/Ne): the operands plus the direct boolean condition (offset <= len), so switchInt/Assert emit a precise path condition instead of ite(cond, 1, 0) != 0.
  • BinaryOp { lhs, rhs, op } — a non-comparison binary-op result (Add/Sub/…/Div/Rem), used for guard inference (tracing a switch/assert guard back to the pointer it null-checks/alignment-checks) and division-axiom injection.

Allocation table

Every allocation a the VM tracks is one MemoryUnit (vm::state::MemoryUnit, stored at VmState::units[a]), split into its shape (allocation) and its contents (content). Its fields, grouped as in the code:

• Shape (always present):
  • base: Int — base address (a fresh Z3 constant).
  • size: Int — byte size (may be symbolic; an external parameter is sized as "unbounded").
  • align: Int — alignment in bytes (may be symbolic for a generic element type).
  • element_ty: ElementTy — the contents' type: Typed(T) for a concrete Ty (or u8 for a raw byte buffer), or Generic for a symbolic T.
  • kind: AllocKind — Object (a single Box<T>/struct/scalar/untyped buffer), Slice { len } (a slice/array buffer, with size == len · size_of(element_ty)), or External (an external raw-pointer parameter or a Vec/CString parameter's heap buffer, of unbounded size i64::MAX or a symbolic unknown size — nullability is tracked on the pointer term, not here).
• Lifecycle facts (allocation.facts: AllocFacts) — cross-cutting per-allocation lifecycle facts, kept apart from the shape metadata above:
  • dead: bool — freed (StorageDead/Drop).
  • liveness: Option<Region> — the region an external allocation is assumed alive for (Alive(p, 'a) contract / 'static); only consulted for external allocations, whose memory is caller-owned (so dead carries no guarantee). None = no assumption.
  • for_each: ForEachFacts — uniform facts about the container's pointer elements (x.iter() for_each invariants), anchored to the allocation so a pointer loaded from it resolves the fact via its provenance: target_ty (Typed), aligned_ty (Align), allocated: (Ty, n) (Allocated, n may be symbolic), owning (Owning).
• Content facts (content.facts: ContentFacts) — per-allocation content facts, kept next to the stored bytes/values rather than on the lifecycle layer:
  • initialized: bool — contents hold a readable value (Box::new/Vec/reference referent/callee return/write/ValidCStr/const data); false for new_uninit/uninit.
  • cstr_trusted: bool — a null-terminated byte buffer (valid C string).
  • utf8_trusted: bool — a valid UTF-8 buffer (ValidString).
  • split_transmute_to: Option<Ty> — the destination element type this allocation is licensed to be re-interpreted into by a SplitTransmute([T], [U]) contract (the slice's data buffer, reached through the slice value's provenance); None = no license.
• Relationships (optional):
  • parent: Option<AllocId> — the source allocation of a sub-view (s[i..j]/get/split_at/align_to/as_chunks/from_raw_parts); root_alloc follows this edge to group aliasing views.

The data allocation of a two-part value (Vec/String/CString) is not stored as an edge: it is re-derived on demand from the header's owning pointer field — the field whose provenance names the heap buffer, located generically by container_ptr_field (Box.0.pointer → [0, 0], Vec.buf.ptr.pointer → [0, 0, 0]). data_alloc_of reads that field's provenance; for a slice view whose header AllocId no longer carries a type key it falls back to header_data_alloc (scan the header's materialized fields for the single owning-pointer provenance). A &[T] reference needs neither — its provenance already names the data.

The entry differs by how the allocation was created:

Provenance

Every pointer value carries the allocation it points into, the byte offset within it, and (when known) the structure of that offset:

provenance(p) = { alloc_id: a, offset: off, offset_kind: k }   ⇔   p points into allocation a at byte offset off

offset_kind classifies the offset so the checker can use a cheaper, more precise proof: Field carries the "field in-bounds" guarantee (offset + size_of(field) <= size_of(container), e.g. Option::as_slice); Element(i) tracks the element index so InBound checks i + count <= slice_len linearly instead of the non-linear byte form (i+count)·S <= len·S (undecidable in Z3 NIA for a generic S); Byte marks a byte-strided (byte_add) or unclassifiable offset. offset_kind is None at the base (offset == 0).

A cast (&mut → *mut, *mut → *const) preserves provenance; a plain copy q = p copies provenance (so p and q are aliases).

Provenance recording rules

The VM maintains provenance in execution order, one transfer per MIR statement/terminator. Below, prov(p) = (a, off) abbreviates the full provenance(p) = { alloc_id: a, offset: off, offset_kind }, and slice_len denotes AllocKind::Slice { len } (read via Allocation::slice_len()):

── Allocation creation (Box::new / Vec::new / …) ──
a := fresh
──────────────────────────────────────────
prov(p) = (a, 0)      a.parent = ⊥         (a.kind = Slice { len } for a Vec/slice)

── View of a pointer (&*p / &mut *p / as_ptr / as_mut_ptr / into_raw) ──
prov(p) = (a, off)
────────────────────────
prov(&*p) = prov(p) = (a, off)          (the view inherits p's provenance)

── Slice view (from_raw_parts(ptr, n)) ──
prov(ptr) = (a, off)
────────────────────────────────────────
b := fresh   prov(s) = (b, 0)   b.kind = Slice { len: n }   b.parent = a

── Split (split_at(s, mid)) ──
prov(s) = (a, 0)   a.kind = Slice { len }   0 ≤ mid ≤ len
──────────────────────────────────────────────────────────────
prov(s[..mid]) = (b₁, 0)   b₁.kind = Slice { len: mid }      b₁.parent = a
prov(s[mid..]) = (b₂, 0)   b₂.kind = Slice { len: len−mid }   b₂.parent = a

── Element arithmetic (p.add(k)) ──
prov(p) = (a, off)
──────────────────────────────
prov(p.add(k)) = (a, off + k·S)      S = sizeof(element)

── Byte arithmetic (p.byte_add(k)) ──
prov(p) = (a, off)
──────────────────────────────
prov(p.byte_add(k)) = (a, off + k)

── Cast reinterprets a buffer (byte ↔ field) ──
A `*mut u8` ↔ `*mut T` cast switches the *view* of an allocation without
changing its bytes.  A *scalar* field round-trips across the two views
(little-endian, concrete size); a *pointer* field does not — provenance is not a
byte, so a byte→field read of a pointer field mints a fresh symbol:

  byte → field:  field(i).z3_term = Σⱼ byte[off(i) + j] · 256ʲ
  field → byte:  byte[off(i) + j]  = (field(i).z3_term ÷ 256ʲ) mod 256

where `off(i)` is field `i`'s byte offset and `256ʲ` is its byte-weight.

Alias rule

Two live reference views p and q alias when they name the same allocation, or sub-allocations of it:

prov(p) = (a, _)    prov(q) = (b, _)
root(a) == root(b)  where root(a) follows parent(a) to the top (⊥)

A view is live when its MIR local is between its StorageLive and StorageDead (and not moved). The parent chain is what makes a slice view (from_raw_parts) or a split_at half count as aliasing its source, even though each has a distinct AllocId — this is why root, not alloc_id alone, is the grouping key.

8.5.2 Deduction Rules

The proof of a property combines two kinds of rule. State-construction axioms describe how the symbolic VM builds the state — model invariants, not obligations. Property discharge rules prove each primitive from that state, through a fast path (a derived flag or layout fact, no solver) or an SMT query (the accumulated constraints plus the negation of the goal). Compound properties are macros over the primitives, and the fast-path flags shortcut the same rules without a query. Notation used throughout:

Notation:  S = sizeof_T,  A = align_T,  s : &[T],  len = s.len()

State-construction axioms

These hold by construction of the symbolic VM — each transfer function records how it updates VmState; none is a property the checker proves.

── Slice type invariant ──
NonNull(s) ∧ Align(s, T) ∧ ValidNum(len·S ≤ isize::MAX) ∧ Allocated(s, T, len) ∧ Init(s, T, len)

── Layout ──
──────────        ──────────        ──────────────────         ────────
S ≥ 0             A ≥ 1             S % A == 0                 len ≥ 0

For a *generic* `T` (no concrete layout), `S` and `A` are the shared symbolic
constants `sizeof_T` / `align_T`.  `size_of::<T>()` / `align_of::<T>()` on such a
`T` bind to these same symbols (not `0`/`1`), so they agree with allocation
sizes and pointer strides; `align_of::<T>() ≥ 1` keeps a cast like
`align as *const T` in `NonNull::dangling` non-null.

── Allocation (s : &[T]) ──
prov(s) = (a, 0)   a.kind = Slice { len }   a.size = len·S   a.align = A   a.initialized = true

── Pointer identity ──
prov(p) = (a, off)
─────────────────────
p.z3_term = a.base + off

── Pointer arithmetic ──
prov(p) = (a, off)                      prov(p) = (a, off)
──────────────────────────────          ──────────────────────────────
prov(p.add(k)) = (a, off + k·S)         (p.add(k)).z3_term = p.z3_term + k·S

── Alignment offset ──
prov(p) = (a, off)    S = sizeof(pointee)    A' = align_of::<U>()
────────────────────────────────────────────────────────────────────────────
align_offset(p, A') = k     (p.z3_term + k·S) % A' == 0      0 ≤ k < A'

`align_offset` is modelled as returning the offset in *elements* of the pointee
type (not bytes), so the aligned address is `p.z3_term + k·S`; a downstream
`p.add(k) as *const U` can then discharge `Align(p, U)`.  The bound `k < A'`
covers successful offsets, but `A' / S` is not their general upper bound:
the stride and requested alignment determine which offsets are reachable.
Rust returns `usize::MAX` when alignment cannot be reached. The current VM
always asserts a successful offset and does not model that failure result;
this can make a feasible path inconsistent and lead to a vacuous proof.

── Byte-range case split (generic S) ──
S = 0                                          S ≥ 1
──────────────────────                        ──────────────────────
x·S = y·S = 0   (byte range vacuous)           x·S ≤ y·S ⟺ x ≤ y

── Integer arithmetic ──
i < len
─────────────
i + 1 ≤ len

Memory-shape properties

Each rule proves one memory-shape primitive from the state built above. Fast paths use the derived flags and layout facts of §8.5.1; otherwise an SMT query asserts the constraints plus the negation of the goal.

── Align(p, T) ──
p.z3_term % align_of(T) == 0
────────────────────────────
Align(p, T)

Fast paths (no query): `align_of(T) == 1`; `align_n(p) ≥ align_of(T)` — compared structurally when both terms
are concrete powers of two, and by a linear SMT query when `align_of(T)` is a
symbolic `align_T` (for a generic `T`, `align_n` and `align_of(T)` are the *same*
shared `align_T` constant, so `align_T ≥ align_T` is trivially discharged);
`align_n` is only a *lower bound* on `p`'s alignment, so it discharges
`Align(p, T)` only when it is at least `align_of(T)`, never below; a
`for_each.aligned_ty(a) = U` fact with `align_of(U) ≥ align_of(T)`; a stack
borrow of a local whose type alignment is `≥ align_of(T)`; an allocation base
with `align(a) ≥ align_of(T)` and `off % align_of(T) == 0`.  Otherwise an SMT
modulo query under `p.z3_term = a.base + off` and `a.base % align(a) == 0`.
The current checker also accepts a concrete zero-sized type without checking
the pointer address. This shortcut is unsound for an aligned ZST, such as
`#[repr(align(8))] struct Z;`: a pointer to `Z` must still be 8-byte aligned.

── NonNull(p) ──
non_null(p)   ∨   in_bounds(p)   ∨   (prov(p) = (a, _) ∧ ¬external(a))   ∨   p.z3_term ≠ 0 (SMT)
─────────────────────────────────────────────────────────────────────────────────────────────────────
NonNull(p)

A tracked stack/heap allocation's base is never zero, so `¬external` implies
non-null; an *external* raw-pointer allocation carries no implied non-nullness
and is discharged only by a `#[rapx::invariant(NonNull(..))]`-derived
`non_null` flag or by proving `p.z3_term ≠ 0` from the path conditions.

── Allocated(p, T, n) ──
prov(p) = (a, off)    ¬dead(a)    off + n·S ≤ size(a)
──────────────────────────────────────────────────────
Allocated(p, T, n)

Vacuous when `n == 0` (any pointer is valid for its 0-byte prefix).  A type
compatibility fast path (element type matches `T`, `MaybeUninit<T>` ≡ `T`,
array/slice element, or a smart-pointer peel) discharges without the byte-range
query; an external "unbounded" allocation (sized `i64::MAX`) auto-passes; a
field-offset pointer checks against the *field's* size.

── InBound(p, T, n) ──
prov(p) = (a, off)    off = k·S (element stride)    a.kind = Slice { len }
────────────────────────────────────────────────────────────────────────────
InBound(p, T, n)  ⟺  k + n ≤ len

The slice form `InBound(s, i)` is the base case (`k = 0, n = 1`): `i < len` (for
a range index, `end ≤ len`).  Without an element-strided offset the check falls
back to the byte form `off + n·S ≤ size(a)` (case-split on `S` for a generic
element size).  Vacuous when `n == 0`; a ZST auto-passes; a field-offset pointer
checks against the field's own size.

── Init(p, T, n) ──
prov(p) = (a, off)    ∀ b ∈ [off, off + n·S) : initialized(a, b)
────────────────────────────────────────────────────────────────────
Init(p, T, n)

Vacuous when `n == 0`.  `Init(p, MaybeUninit<T>, n)` reduces to `Typed` —
`MaybeUninit<T>` carries no validity invariant, so there is nothing to
initialize.  Byte-level coverage is decided by the allocation's `initialized`
flag / per-byte `byte_array` (`byte[i] = select(array, i)`, unwritten offsets read the `UNINIT` sentinel); a byte never written is a confirmed violation.

── Owning(p) ──
prov(p) = (a, _)    ¬∃ live o ≠ dest : needs_drop(o) ∧ prov(o) = (a, _)
──────────────────────────────────────────────────────────────────────
Owning(p)

The check scans the *live* locals for a `needs_drop` owner whose buffer aliases
`a` (excluding the call's own destination and the reconstructed owner), which
would mean a second owner drops the same allocation.  The `for_each.owning` flag
(an `Owning(container.iter())` invariant declaring every element the sole owner
of its pointee) discharges `Owning` directly.

── Alive(p) ──
prov(p) = (a, _)    ¬dead(a)    (a is a tracked allocation, or p is a live reference/owner)
────────────────────────────
Alive(p)

── Alive (assumed for a region) ──
prov(p) = (a, _)    liveness(a) = Some('a)    ¬dead(a)    'a: 'r
───────────────────────────────────────────────────────────────────────
Alive(p, 'r)

`liveness` is only consulted for external raw-pointer allocations (whose memory
is owned by the caller, so `dead` carries no guarantee). `Some('static)` is
set by a `ValidCStr(p, n)` fact, an `Allocated` raw-pointer parameter, or
`'static` const/static data; `Some('a)` by an `Alive(p, 'a)`
contract/invariant. The assumption's region must cover the demanded region
(`'a: 'r`), resolved via rustc's `FreeRegionMap` (declared `where 'a: 'b` bounds
and their transitive closure) or — for a reference parameter `&'r Self<'a>` — by
the implied outlives of the type itself (`'a: 'r`); a wider demand than the
assumption fails.

── Typed(p, T) ──
prov(p) = (a, _)    element_ty(a) = T   (or a field of `T` at `off`; MaybeUninit is vacuously typed)
─────────────────────────────────────────────────────────────────────────────────────────────────
Typed(p, T)

── Typed (pointer container) ──
prov(p) = (a, _)    for_each.target_ty(a) = T
──────────────────────────────────────────────
Typed(p, T)

── Null (guarded branch of any(Null(p), …)) ──
p.z3_term = 0   (or p carries no non-null provenance)
───────────────────────────────────────────────────
Null(p)   (else the other disjunct decides)

── NonOverlap(p, q, n) ──
prov(p) = (a, _)    prov(q) = (b, _)    a ≠ b
─────────────────────────────────────────────
NonOverlap(p, q, n)
(else the byte ranges [p.z3_term, p.z3_term+n·S) and [q.z3_term, q.z3_term+n·S) are disjoint — an SMT query)

Two pointers with the same `alloc_id` fall through to the byte-range query.
The distinct-ID fast path above is an implementation limitation, not a sound
deduction for sub-views: `from_raw_parts` and split operations can give
overlapping views of one allocation different IDs with the same `root`. Their
ranges must be checked before `NonOverlap` can be proved; the current fast path
can otherwise incorrectly accept overlap.

Layout and type-level properties

── Size ──
size_of(T) = n                T: Sized ∧ size_of(T) > 0
──────────────────            ───────────────────────────
Size(T, n)                    Size(T, sized)

── NoPadding ──
T has no padding bytes (scalars/pointers/refs, arrays, tuples, and non-union structs, recursively)
────────────────────────────────────────────────────────────────────────────────────────────────────
NoPadding(T)

── ValidTransmute ──
size_of(src) = size_of(dst)     (a generic size — `0` — trusts the type system, since the call compiled)
──────────────────────────────────────────────────────────────────────────────────────────────────────
ValidTransmute(src, dst)

── SplitTransmute ──
split_transmute_to(receiver_alloc) = dst_elem
  ∨   src_elem = dst_elem   ∨   dst_elem is SIMD with a src lane   ∨   all-bit-patterns-valid(dst_elem)
──────────────────────────────────────────────────────────────────────────────────────────────────────
SplitTransmute([Src], [Dst])

The first disjunct is the caller-declared license: a `requires(SplitTransmute([T],
[U]))` contract records `U` on the slice's data allocation (via the slice value's
provenance), and the check discharges exactly that transmute — not every
transmute — when the receiver slice resolves to the same allocation.

── Trait ──
T: Copy    (or T: Sized; or T: <trait> appears among the caller's where-clauses)
──────────────────────────────────────────────────────────────────────────────────
Trait(T, Copy)

Numeric and byte-string properties

── ValidNum ──
∀ pred :  assert_all ∧ ¬cond(pred) is UNSAT    (with Euclidean-division/NIA axioms)
─────────────────────────────────────────────────────────────────────────────
ValidNum(...)

Each predicate (`index < len`, or the interval form desugared to `lo ≤ v ∧ v ≤ hi`)
is evaluated to a Z3 comparison; the negation is shown unsatisfiable under the path
constraints, with division axioms (`X = (X/N)·N + X%N`) injected to decide non-linear
inequalities.  A `size_of::<T>() · count ≤ isize::MAX`-shaped predicate (the slice
size invariant) is discharged by rule without a query.

── ValidString (UTF-8) ──
n = 0   ∨   the tracked bytes of prov(p)'s allocation form valid UTF-8
─────────────────────────────────────────────────────────────────────
ValidString(p, T, n)

── ValidCStr (nul-terminated) ──
cstr_trusted(a)   ∨   the bytes contain no interior NUL and end with a terminal NUL
─────────────────────────────────────────────────────────────────────────────────────
ValidCStr(p, n)

Compound properties

The compound safety properties are macros over the primitives (Deref reads "in-bounds within a live allocation"; ValidPtr is vacuous for a ZST, where non-nullness alone suffices):

Deref(p, T, n)      = Allocated(p, T, n) ∧ InBound(p, T, n)
ValidPtr(p, T, n)   = NonNull(p) ∧ (Size(T, 0) ∨ Deref(p, T, n))
Ptr2Ref(p, T)       = Init(p, T, 1) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p)
Ptr2RefUninit(p, T) = Typed(p, T) ∧ ValidPtr(p, T, 1) ∧ Align(p, T) ∧ Alias(p)
Drop(p, T)          = ValidPtr(p, T, 1) ∧ Alias(p)

Fast-path flags

The VM's derived value facts shortcut three primitives without an SMT query:

non_null(p)          in_bounds(p)          align_n(p) ≥ align_of(T)      (both powers of two)
────────────        ─────────────────      ────────────────────────────
NonNull(p)          InBound(p, T, 1)       Align(p, T)

non_null proves NonNull; in_bounds proves InBound(p, T, 1) (a single-element bound, established by a prior deref or contract); align_n is a lower bound on p's alignment, so it proves Align(p, T) only when it is at least align_of(T). The value's init flag is not a shortcut for Init(p, T, 1): Init concerns the pointee memory's initialized bytes (the allocation's initialized flag / per-byte byte_array), whereas init marks a value whose content is known initialized — it feeds the Typed fast paths and the MaybeUninit write exceptions, not the Init check.

These flags are sourced, not invented. A raw-pointer field (*mut T / *const T / NonNull<T>) carries no implicit non_null/init/align fact: those must be declared on the struct via #[rapx::invariant(NonNull(..))] / #[rapx::invariant(Init(..))] / #[rapx::invariant(Align(..))] (or discharged at the deref by a null guard). A deref of an unannotated raw field therefore fails NonNull/Init rather than silently assuming it. A concrete Align invariant is additionally recorded as the path condition p.z3_term % A == 0, so it survives pointer arithmetic (p.add(k)) that drops the value-level flag.

8.5.3 The Alias Hazard

Alias is a hazard by default — unproved Alias is reported as a [hazard] entry and contributes to UNSOUND — but it is also the property used to express a no-aliasing precondition: Ptr2Ref(p, T) (and Drop(p, T)) include Alias(p), and a caller discharges the hazard by declaring #[rapx::requires(Ptr2Ref(p, T))]. In both roles it asserts that a reference produced by a deref does not unsafely alias other live references. It applies to any deref that produces a reference (&*p / &mut *p / from_raw_parts, ...); a bare *p read or *p = ... write is Deref/ReadMemory, not Alias.

A caller-declared Alias is anchored to an allocation, not a whole-path flag. assert_contract_fact resolves each Alias source place — a hazard's Alias(self, ret) or a Ptr2Ref's Alias(self.0), following field projections — to the root allocation of the named parameter, and records it in VmState::alias_hazard_allocs. A call-site or escape check then discharges the hazard only when the produced view's origin resolves to one of those allocations, so a contract licensing Alias(self, ret) no longer licenses every other alias on the path.

The check runs five passes over the produced view:

── Alias (hazard) ──
  applies to any deref that produces a reference (&*p / &mut *p / from_raw_parts, ...);
  a bare *p read / *p = ... write is Deref/ReadMemory, not Alias.

  The alias check runs five passes over the produced view:

  1. resolve provenance — resolve_origin(p) → the allocation p points to, and
     its origin kind: &mut → MutRef, & → SharedRef, *const/*mut → RawPtr,
     Box/Vec/NonNull → Owned.

  2. collect the live alias set (flow-sensitive) — walk the VM's *current*
     locals: a live reference view aliases p when it names the same allocation
     (provenance), or a sub-allocation of it (`from_raw_parts` / `split_at`
     keep a `parent` edge back to the allocation they were split from).

  3. callsite check — the caller's contract must discharge the raw-pointer
     provenance's aliasing:
       an `Alias` declaration naming p's allocation (root(p) ∈ alias_hazard_allocs)
         → ✓ (Alias(p) is caller-guaranteed; its Init/NonNull/Allocated/Align parts
         are separate checks)
       otherwise, shared-XOR-mutable over the live alias set (step 2):
         &*p    requires no live &mut to *p   → else ✗
         &mut *p requires no live &    to *p   → else ✗
       a raw-pointer origin without a precondition → alias set unknown, defer.

  4. forward check — while the view is live, the *origin* raw pointer must not
     be accessed again; this is also what rejects a second `&mut *p` while the
     first `&mut` is still live:
       SharedView:  a raw write through the origin → ✗
       UniqueView:  any raw access through the origin → ✗

  5. escape — is the view returned?
     not returned → the borrow ends (steps 3–4 decide).
     returned → the escape hazard must be discharged:
       an `Alias(ptr, ret)` declaration naming the origin's allocation → ✓
         (the caller handles the aliasing)
       a shared view from an encapsulated raw field → ✓ (a per-function
         derivation forest resolves the nested field path, e.g. `self.node.ptr`
         → `[node, ptr]`, to the innermost raw field; a private field not
         written/exposed by safe code upholds the returned `&T`)
       a shared view re-borrowed from a reference parameter → ✓ only when the
         returned region does not outlive the parameter's region (`src: ret`,
         via rustc's outlives relation); returning a `&'b str` as `&'a str`
         with `'a: 'b` is rejected.
       otherwise → ✗

  ✓ = safe   ✗ = violation   Unknown = cannot prove safe (hazard not eliminated)

8.5.3.1 Precision

The alias analysis over-approximates several kinds of overlap:

• Sensitive: allocation identity (provenance alloc_id + parent chain), flow (the VM's current locals and StorageLive/StorageDead liveness), and — for the escape pass — the field path.
• Insensitive: byte offset/range. Two disjoint views of the same allocation (e.g. hand-written &*p and &mut *p.add(1)) may be treated as aliasing. Split operations give their halves separate AllocIds but preserve a common parent, so root-based alias checks can still group them.
• Path/context-insensitive: the forward scan uses CFG-reachable blocks (no path conditions), and the analysis is intra-procedural (cross-function aliasing is discharged by Alias/Ptr2Ref preconditions).

This abstraction can produce false positives on disjoint ranges and reference-parameter provenance. It does not by itself establish a no-missed-aliasing guarantee for the verifier: the NonOverlap distinct-ID shortcut described above can miss overlapping sub-views.