Chapter 8.2. Verification Target Collection

When verification starts, RAPx scans the crate to identify verification targets — functions whose safety contracts need to be checked — and resolves the contracts for each target.

8.2.1 What Gets Verified

In scan mode (the default), a function is selected as a verification target if:

• its body contains an unsafe { } block, or
• it is a method on a struct with #[rapx::invariant] annotations.

For each target, the collector gathers:

• Every call to an unsafe fn in the function body, along with the callee's resolved contracts.
• Every raw pointer dereference (*ptr, *ptr = val) in unsafe blocks — these implicitly require ValidPtr + Align + Typed, as if those contracts were declared on a pseudo-callee.
• Every static mut access — treated similarly.
• Entry assumptions — the facts the verifier can assume when the function is entered:
  • The function's own #[rapx::requires] annotations.
  • If the function is a method on a struct with #[rapx::invariant], those invariants are included as entry facts.
  • Type-level invariants for function parameters (e.g. a &[T] parameter automatically supplies ValidPtr + NonNull for the slice's data pointer).

8.2.2 How Contracts Are Resolved

For each unsafe callee, the verifier needs to know what safety properties it requires. Contracts are resolved in four tiers, tried in order:

1. Direct annotation: #[rapx::requires(...)] on the callee itself. See Chapter 8.3.2.

2. Trait method inheritance: If the callee is a trait method impl and has no direct annotation, its contracts are inherited from #[rapx::requires] on the trait's method declaration.

3. JSON database: For standard library functions that can't be annotated upstream, contracts are loaded from a bundled database. See Chapter 8.3.4.

4. Call-chain inheritance: If the unsafe callee still has no contracts, the verifier looks inside its MIR body for the unsafe functions it calls (its own unsafe callees). If any of those have resolved contracts, they are used as the verification target — the caller only needs to satisfy the contracts of the deepest callee in the chain. This follows a bounded depth. For example, if A calls B, B calls C, and C has #[rapx::requires], verifying the call to B checks A's state against C's contracts.

If all four tiers produce nothing, the callee's contracts are left as Unknown — the callsite cannot be verified.

8.2.3 Inspecting Targets with --prepare-targets

The --prepare-targets flag prints every verification target collected by the scanner — a function or method whose unsafe operations need to be checked — along with its resolved contracts:

cargo rapx verify --prepare-targets

For the linked_list_nonnull case study, the collector finds two targets:

Full output (annotations explained below):

14:49:41|RAPx|INFO|: Start analysis with RAPx.
14:49:41|RAPx|INFO|: ============================================================
14:49:41|RAPx|INFO|: [rapx::verify] prepare targets for struct: LinkedList
14:49:41|RAPx|INFO|: ============================================================
14:49:41|RAPx|INFO|:   struct invariants:                              ①
14:49:41|RAPx|INFO|:     - Align(head.unwrap_some(), Node)
14:49:41|RAPx|INFO|:     - Align(tail.unwrap_some(), Node)
14:49:41|RAPx|INFO|:     - Allocated(head.unwrap_some(), Node, 1)
14:49:41|RAPx|INFO|:     - Owning(head.unwrap_some())
14:49:41|RAPx|INFO|:   --- method: from_vec ---------------------------- ②
14:49:41|RAPx|INFO|:       return checkpoints: 1 block(s) [15]           ③
14:49:41|RAPx|INFO|:       unsafe callee: std::ptr::NonNull::<T>::as_mut(…)
14:49:41|RAPx|INFO|:         safety contracts:                           ④
14:49:41|RAPx|INFO|:           - Ptr2Ref(self.head, T)
14:49:41|RAPx|INFO|:       checkpoint paths:                             ⑤
14:49:41|RAPx|INFO|:         #0 core::ptr::non_null::as_mut at bb10
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 11 -> 14 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 10
14:49:41|RAPx|INFO|:         #1 core::ptr::non_null::as_mut at bb12
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 11 -> 14 -> 2 -> 3 -> 5 -> 7 -> 8 -> 9 -> 10 -> 12
14:49:41|RAPx|INFO|:   --- method: drop -------------------------------- ②
14:49:41|RAPx|INFO|:       return checkpoints: 1 block(s) [7]            ③
14:49:41|RAPx|INFO|:       + constructor: LinkedList::from_vec           ⑥
14:49:41|RAPx|INFO|:       unsafe callee: std::boxed::Box::<T>::from_raw(…)
14:49:41|RAPx|INFO|:         safety contracts:                           ④
14:49:41|RAPx|INFO|:           - Allocated(raw, T, 1)
14:49:41|RAPx|INFO|:           - Owning(raw)
14:49:41|RAPx|INFO|:           - Alias(raw, ret)
14:49:41|RAPx|INFO|:       unsafe callee: std::ptr::NonNull::<T>::as_ref(…)
14:49:41|RAPx|INFO|:         safety contracts:
14:49:41|RAPx|INFO|:           - Ptr2Ref(self.head, T)
14:49:41|RAPx|INFO|:       checkpoint paths:                             ⑤
14:49:41|RAPx|INFO|:         #0 core::ptr::non_null::as_ref at bb2
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2
14:49:41|RAPx|INFO|:         #1 alloc::boxed::from_raw at bb4
14:49:41|RAPx|INFO|:           path 0: 0 -> 1 -> 2 -> 3 -> 4
14:49:41|RAPx|INFO|: ============================================================
14:49:41|RAPx|INFO|: [rapx::verify] total: 0 free function(s), 2 method(s), …  ⑦