Chapter 8.4. The Verification Pipeline

This chapter walks through the verification pipeline using the linked_list_nonnull case study — a doubly-linked list built with NonNull<Node> pointers:

#![allow(unused)]
fn main() {
#[rapx::invariant(Align(head.unwrap_some(), Node))]
#[rapx::invariant(Allocated(head.unwrap_some(), Node, 1))]
#[rapx::invariant(Owning(head.unwrap_some()))]
struct LinkedList { head: Option<NonNull<Node>>, tail: Option<NonNull<Node>> }
}

Running cargo rapx verify on the case study produces:

12:00:18|RAPx|INFO|: Start analysis with RAPx.
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|: [rapx::verify] function: LinkedList::from_vec
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|:   --- unsafe checkpoints ---
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb10 -> core::ptr::non_null::as_mut
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb12 -> core::ptr::non_null::as_mut
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:   --- struct invariants ---
12:00:19|RAPx|INFO|:       checkpoint bb15:
12:00:19|RAPx|INFO|:         path 0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 6, 15:
12:00:19|RAPx|INFO|:           Align | Proved (x2)
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:         path 0, 1, 2, 3, 6, 15:
12:00:19|RAPx|INFO|:           Align | Proved (x2)
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:   result: SOUND
12:00:19|RAPx|INFO|:
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|: [rapx::verify] function: <LinkedList as std::ops::Drop>::drop
12:00:19|RAPx|INFO|: ============================================================
12:00:19|RAPx|INFO|:   --- unsafe checkpoints ---
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb2 -> core::ptr::non_null::as_ref
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2]:
12:00:19|RAPx|INFO|:           Ptr2Ref | Proved
12:00:19|RAPx|INFO|:       unsafe checkpoint: bb4 -> alloc::boxed::from_raw
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:           [hazard] Alias | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:           [hazard] Alias | Proved
12:00:19|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
12:00:19|RAPx|INFO|:           Allocated | Proved
12:00:19|RAPx|INFO|:           Owning | Proved
12:00:19|RAPx|INFO|:           [hazard] Alias | Proved
12:00:19|RAPx|INFO|:   result: SOUND
12:00:19|RAPx|INFO|:

The report shows two targets:

For each target the pipeline runs: path extraction → backward slicing → forward verification → SMT check. The sections below use from_vec as the example.

8.4.1 Path Extraction

The first stage enumerates acyclic paths from function entry to each unsafe callsite using PathGraph's SCC decomposition (see §5.1 Path Analysis for the full algorithm). Each path is a sequence of basic block IDs.

The for value in values { … } loop contains an SCC with two branches (tail is None or Some). The path extractor unrolls this SCC according to the repeat budget, producing paths for the first iteration (both branches) and subsequent iterations (each branch repeated). The sections below use the first Ptr2Ref path as the single running example:

path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10]   →   Ptr2Ref | Proved

This path represents a two-element input: the first iteration (empty list, bb11 initialises head and tail), then the second iteration where _2.1 is Some and as_mut() is called at bb10.

Paths are stored in a PathTree per callsite and capped at 1024. By default, auto mode chooses the repeat budget before path extraction. With --postfix-repeat=N, verification uses the fixed repeat count N.

8.4.2 Backward Slicing

Take the path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10] — two-element input, first iteration initialises the empty list, second iteration calls tail.as_mut() at bb10. The relevant MIR blocks:

bb0:  {
    _2 = LinkedList { head: None, tail: None }   // empty list
}
bb1:  {
    _8 = <Vec<i32> as IntoIterator>::into_iter(move _1) → bb2
}
bb2:  {
    _11 = <IntoIter<i32> as Iterator>::next(&mut _8) → bb3   // for loop body
}
bb3:  {
    switchInt(discriminant(_11)) → [0: bb6, 1: bb5]   // None → exit, Some → process
}
bb5:  {
    _17 = Box::<Node>::new(move _18) → bb7             // heap allocate
}
bb7:  {
    _24 = move _17
    _23 = Box::<Node>::leak(move _24) → bb8            // transfer ownership
}
bb8:  {
    _22 = NonNull::<Node>::from(move _23) → bb9        // wrap in NonNull
}
bb9:  {
    _25 = discriminant((_2.1: Option<NonNull<Node>>))
    switchInt(move _25) → [0: bb11, 1: bb10]           // tail is None? Some?
}
bb10: {
    _30 = copy ((_2.1 as Some).0: NonNull<Node>)       // extract stored NonNull
    _34 = &mut _30
    _33 = NonNull::<Node>::as_mut(move _34) → bb12     // ← CHECKPOINT
}
bb11: {
    (_2.0) = Some(_27)                                  // set head
    (_2.1) = Some(_29)  // _29 = copy _22              // set tail
}
bb14: {
    goto → bb2                                          // loop back
}

The example path reaches bb10 on the second iteration: the first iteration went through bb11 (tail was None, initialised), then bb14 loops back, bb2-5-7-8 allocates a second node, bb9 dispatches again — this time tail is Some, so control flows to bb10.

The BackwardSlicer extracts only the MIR statements that contribute to the target place's value — everything else is dropped.

Walk backward from _33 = as_mut(move _34):

The collected chain is _34 → _30 → _2.1 → _22 → _23 → _17(where _2.1 is the tail field of LinkedList). The slicer recognises standard-library calls by their effects: Box::new → BoxAllocation, NonNull::from → ReturnPointerFromArg.

No ContractFact items are injected — from_vec has no #[rapx::requires] of its own.

8.4.3 Forward Verification

The ForwardVerifier performs two distinct analyses:

• Fact accumulation (8.4.3.1): abstract interpretation along a single extracted path from function entry to the checkpoint, gathering facts that feed into SMT checks.
• Hazard tracking (8.4.3.2): a full-CFG flow-sensitive scan from the checkpoint through all reachable branches, checking for alias/ownership conflicts.

Per primitive-sp, Ptr2Ref is Init(p, T, 1) && Align(p, T) && Alias(p, ret). Init and Align are checked together by the SMT solver against accumulated path facts; Alias is handled by the full-CFG hazard tracking phase below.

8.4.3.1 Fact accumulation before the checkpoint

At the checkpoint, the verifier resolves the value chain _34 → _30 → _2.1 → _22 → _23 → _17. At the origin (Box::new), two facts are available for Ptr2Ref:

8.4.3.2 Hazard tracking after the checkpoint

Unlike fact accumulation which follows a single path, the hazard scan operates on the full function CFG, traversing all branches reachable from the checkpoint.

as_mut declares the Alias(p, ret) hazard: _33 aliases _17, violating Rust's exclusive mutability. The verifier must check that this alias causes no UB in the remainder of the function.

The scan checks two things on the full CFG:

1. Exclusive mutability — any raw read/write through the origin(_17, _30, _34)while _33 is live? No conflicts found.
2. Hazard cross function boundary — does _33 escape the function(returned or stored in a surviving field)or remain live at any exit? No: used only locally to set prev/next in bb12-13, dies at scope end. If it did escape(e.g. fn get_tail_mut(&mut self) -> &mut Node { unsafe { self.tail.as_mut() } }), the caller would inherit the obligation.

8.4.4 SMT Check

Each accumulated fact lowers to an SMT constraint:

• Value-definition chain. MIR assignments like _34 = &mut _30 create a definition: _34 is a reference to _30. The SMT model follows this chain, so _34 and _30(and ultimately _17)map to the same Z3 address variable — no separate equality assertion needed.
• PointsTo declares two pointers share provenance, and asserts each is aligned: addr % align_of::<pointee_ty>() = 0.
• KnownAllocated records the allocation's element count(1 for Box<Node>). Used to recover allocation bounds (base, len) during SMT checks.
• KnownInit marks the origin as holding initialized(non-MaybeUninit)memory, enabling the Init range check.

The check uses negation-as-failure: assert all constraints, assert the negated goal, solve — Unsat → Proved, Sat → Failed.

For Ptr2Ref on _17, two obligations are checked:

Align

constraints ∧ ¬(_17 % align_of::<Node>() = 0)

The negated goal contradicts the alignment constraint from PointsTo → Unsat → Align | Proved.

Init

Init means _17 points to initialized(non-MaybeUninit)memory whose access fits within the allocation bounds.

• Initialized? Yes: KnownInit from Box::new marks _17's origin as initialized.
• Fits within allocation? Box::new allocates one Node at _17. The allocation has len = 1(element), the access is 1 element starting at offset = 0:

offset + access ≤ len  →  0 + 1 ≤ 1

Trying to assert 0 + 1 > 1 contradicts the known allocation bounds → Unsat → Init | Proved.

8.4.5 Auto-Repeat Planner

For the checkpoint bb10 -> as_mut, Ptr2Ref requires two preconditions: Init and Align. In default auto mode, the planner notices that this checkpoint depends on loop-carried state and chooses a deeper repeat budget. The path extractor therefore produces two paths reaching bb10:

repeat 1:
  path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
    Init  | Proved
    Align | Proved

repeat 2:
  path [0, 1, 2, 3, 5, 7, 8, 9, 11, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10, 12, 13, 14, 2, 3, 5, 7, 8, 9, 10]:
    Init  | Proved
    Align | Proved

The Proved set (Init and Align) is identical across these repeat depths. In this case, deeper paths do not reveal a violating state, and the final verdict remains SOUND.

The repeat planner only decides how many loop repetitions should be explored. The backward slicer, forward verifier, and SMT checker then run on the extracted paths as usual.