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(Typed(head.unwrap_some(), Node))]
#[rapx::invariant(Owning(head.unwrap_some()))]
#[rapx::invariant(Align(tail.unwrap_some(), Node))]
#[rapx::invariant(Allocated(tail.unwrap_some(), Node, 1))]
#[rapx::invariant(Typed(tail.unwrap_some(), Node))]
#[rapx::invariant(Owning(tail.unwrap_some()))]
struct LinkedList { head: Option<NonNull<Node>>, tail: Option<NonNull<Node>> }
}

Running cargo rapx verify on the case study produces:

02:43:07|RAPx|INFO|: Start analysis with RAPx.
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|: [rapx::verify] function: LinkedList::<T>::new
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|:   --- struct invariants ---
02:43:07|RAPx|INFO|:       checkpoint bb0:
02:43:07|RAPx|INFO|:         path 0:
02:43:07|RAPx|INFO|:           ├── Align | Proved (x2)
02:43:07|RAPx|INFO|:           ├── Allocated | Proved (x2)
02:43:07|RAPx|INFO|:           ├── Typed | Proved (x2)
02:43:07|RAPx|INFO|:           └── Owning | Proved (x2)
02:43:07|RAPx|INFO|:   result: SOUND
02:43:07|RAPx|INFO|:
...
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|: [rapx::verify] function: <LinkedList<T> as std::ops::Drop>::drop
02:43:07|RAPx|INFO|: ============================================================
02:43:07|RAPx|INFO|:   --- unsafe checkpoints ---
02:43:07|RAPx|INFO|:       unsafe checkpoint: bb2 -> core::ptr::non_null::as_ref
02:43:07|RAPx|INFO|:         path [0, 1, 2]:
02:43:07|RAPx|INFO|:           Ptr2Ref | Proved
02:43:07|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2]:
02:43:07|RAPx|INFO|:           Ptr2Ref | Proved
02:43:07|RAPx|INFO|:         ... (2 deeper paths, all Proved)
02:43:07|RAPx|INFO|:       unsafe checkpoint: bb4 -> alloc::boxed::from_raw
02:43:07|RAPx|INFO|:         path [0, 1, 2, 3, 4]:
02:43:07|RAPx|INFO|:           ├── Align | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Allocated | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Typed | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Owning | Proved (x3)
02:43:07|RAPx|INFO|:           └── [hazard] Alias | Proved (x3)
02:43:07|RAPx|INFO|:         path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]:
02:43:07|RAPx|INFO|:           ├── Align | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Allocated | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Typed | Proved (x3)
02:43:07|RAPx|INFO|:           ├── Owning | Proved (x3)
02:43:07|RAPx|INFO|:           └── [hazard] Alias | Proved (x3)
02:43:07|RAPx|INFO|:         ... (2 deeper paths, all Proved)
02:43:07|RAPx|INFO|:   result: SOUND
02:43:07|RAPx|INFO|:

The report covers 13 targets:

For each target the pipeline runs: path extraction → backward slicing → symbolic VM execution → SMT check. The sections below use <LinkedList as Drop>::drop as the running example — it has two unsafe callsites (as_ref for Ptr2Ref, Box::from_raw for Allocated/Owning/Alias) inside a while let loop, making it a compact but representative walkthrough.

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 drop function contains a while let loop over the linked list nodes:

#![allow(unused)]
fn main() {
fn drop(&mut self) {
    let mut current = self.head;
    unsafe {
        while let Some(node) = current {
            current = node.as_ref().next;        // ← Ptr2Ref at as_ref
            drop(Box::from_raw(node.as_ptr())); // ← Allocated/Owning/Alias at from_raw
        }
    }
}
}

The while let body forms an SCC (bb2 → bb3 → bb4 → bb5 → bb6 → bb1 → bb2). Depending on the repeat budget, the path extractor unrolls this SCC, producing one path per loop iteration depth:

Checkpoint bb2 -> as_ref (Ptr2Ref):

path [0, 1, 2]                                  → 1 element, 1st iteration
path [0, 1, 2, 3, 4, 5, 6, 1, 2]               → 2 elements, 2nd iteration
path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2]  → 3 elements, 3rd iteration

Checkpoint bb4 -> from_raw (Allocated/Owning/Alias):

path [0, 1, 2, 3, 4]                            → 1 element
path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]         → 2 elements
path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]  → 3 elements

Each path records exactly one visit to the target callsite after the prescribed number of loop iterations. The sections below use the shortest from_raw path as the running example:

path [0, 1, 2, 3, 4]   →   Allocated/Typed/Owning | Proved, Alias | Proved

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, 4] — a single-element list: self.head is Some, the while let enters once, as_ref at bb2 exposes the node, and Box::from_raw at bb4 frees it. The relevant MIR blocks:

bb0:  {
    _2 = move (_1.0: Option<NonNull<Node<T>>>)   // current = self.head
}
bb1:  {
    _3 = discriminant(_2)
    switchInt(move _3) → [0: bb7, 1: bb2]         // None → exit, Some → loop
}
bb2:  {
    _4 = copy ((_2 as Some).0)                    // extract NonNull from Option
    _6 = &mut _4
    _5 = NonNull::<Node<T>>::as_ref(move _6)      // ← CHECKPOINT: Ptr2Ref
}
bb3:  {
    _7 = &(*_5).next
    _2 = move _7                                  // current = node.next
}
bb4:  {
    _8 = NonNull::<Node<T>>::as_ptr(copy _4)
    _9 = Box::<Node<T>>::from_raw(move _8)        // ← CHECKPOINT
}
bb5:  {
    drop(_9)                                      // free the Box
}
bb6:  {
    goto → bb1                                    // loop back
}
bb7:  {
    return
}

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

Walk backward from _9 = Box::from_raw(move _8):

The collected chain is _9 → _8 → _4 → _2 → _1.0 (where _1.0 is the head field of LinkedList). The slicer recognises standard-library calls by their effects: NonNull::as_ptr → returns a raw pointer to the same allocation; ((_2 as Some).0) → projection from Option to inner NonNull.

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

8.4.3 Symbolic VM Execution

The SymbolicVm (vm/mod.rs) is a semantic MIR executor that replaces the earlier pattern-matching forward verifier. Instead of deriving ad-hoc facts from MIR patterns, it executes the retained MIR items from the backward slicer and directly builds symbolic state (VmState) with Z3 terms for every value.

8.4.3.1 Building symbolic state before the checkpoint

The VM executes retained MIR items in forward path order. Each MIR statement and terminator is translated into a transfer function that updates VmState:

At execution time, the VM tracks:

• local_addresses: The numeric address bound to each MIR local
• allocations: All known memory allocations with their size, element count, type, and provenance
• init_allocations: Allocations that have been written to (initialized)
• path_conditions: Accumulated branch constraints from SwitchInt and Assert terminators

At the from_raw checkpoint, the verifier resolves the value chain _9 → _8 → _4 → _2 → _1.0 through the VM's provenance tracking. The origin _1.0 (self.head) is a NonNull<Node<T>> pointer stored in the struct — its provenance was tracked from the struct invariant that guarantees Allocated(head.unwrap_some(), Node, 1).

8.4.3.2 Hazard tracking (Alias)

Box::from_raw declares the Alias(p, ret) hazard: _9 takes ownership of the allocation at _8, and the verifier must prove that no other live pointer aliases the same memory at this point. The PropertyChecker checks that the origin pointer's allocation is not referenced by any other live local or field.

In drop, after _2 is updated to node.next in bb3, the original _4 pointer is the only remaining handle to the old node's allocation. The verifier confirms no conflicting alias exists → Alias | Proved.

8.4.4 SMT Check

The PropertyChecker (property_checker) translates the VM state into Z3 assertions and checks each safety property:

• Value-definition chain. MIR assignments create symbolic Z3 terms for each local. _8 is defined as the raw pointer from _4, which projects from _2, which originates from self.head. The Z3 model follows this value chain — no separate equality assertion needed.
• Allocation model. Each allocation records its base address, element size (from sizeof(T)), and element count. The VM asserts that the address range is within the allocation bounds.
• Initialization tracking. The struct invariant Allocated(head.unwrap_some(), Node, 1) tells the verifier that self.head's allocation holds one initialized Node<T>. The VM propagates this to _4 → _8.
• Path conditions. The switchInt at bb1 constrains the solver: _2 is Some.

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

For Box::from_raw on _8, five obligations are checked:

Align

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

The struct invariant Align(head.unwrap_some(), Node) guarantees self.head is aligned. The VM propagates alignment through the value chain _1.0 → _2 → _4 → _8. The negated goal contradicts the invariant → Unsat → Align | Proved.

Allocated

Allocated means _8 points to a live heap allocation of size sizeof(Node<T>).

• Is it heap-allocated? The struct invariant Allocated(head.unwrap_some(), Node, 1) guarantees self.head owns a heap allocation.
• Fits within bounds? The allocation has element_count = 1, and Box::from_raw consumes exactly 1 element.

The negated goal contradicts the invariant → Unsat → Allocated | Proved.

Typed

Typed(p, T) means the allocation at p holds valid data of type T. The struct invariant Typed(head.unwrap_some(), Node) is propagated through the value chain. Negating it contradicts the invariant → Typed | Proved.

Owning

Owning(p) means the current function holds unique ownership of allocation p — no other code can access it. When drop takes &mut self, it has exclusive access to the struct's fields, including head. The invariant Owning(head.unwrap_some()) confirms the struct owns the allocation, and the &mut self receiver transfers that ownership to drop. Negating → Unsat → Owning | Proved.

Alias

constraints ∧ (another live pointer aliases _8)

After _2 is updated to node.next in bb3, the VM confirms _4 is the only handle to the old node's allocation. No other local or field points to the same memory → Unsat → Alias | Proved.

8.4.5 Auto-Repeat Planner

For the bb4 -> from_raw checkpoint, Box::from_raw requires Allocated, Owning, and Alias (plus Align/Typed propagated from the struct invariants). The SCC in drop (the while let loop) means the pointer's origin — self.head — remains valid across iterations: after freeing the first node, current advances to node.next, which is also covered by the head invariant.

The planner recognises that deeper unrolling still satisfies the same invariants and produces increasing path depths. The shortest path (depth 0) contains a single loop iteration:

depth 0:  path [0, 1, 2, 3, 4]               — 1  body iteration
depth 1:  path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]    — 2  body iterations
depth 2:  path [0, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4, 5, 6, 1, 2, 3, 4]  — 3  body iterations

All five properties (Align, Allocated, Typed, Owning, Alias) are proved at each depth, with the shortest path covered by multiple rounds (producing Proved (x3) in the output). The Proved set is identical across all three depths — 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, symbolic VM, and SMT checker then run on the extracted paths as usual.