Chapter 8.3. Safety Property Contracts

RAPx verifies safety through explicit contracts declared in source code. This chapter covers how to write contracts using the available property kinds, and how to inspect resolved contracts with --debug-contracts.

Contracts are declared in two ways:

Direct annotation — #[rapx::requires(...)], #[rapx::invariant(...)] attributes in Rust source (§8.3.2).
JSON database — pre-written contracts for standard-library functions that cannot be annotated upstream (§8.3.4).

8.3.1 Property Kinds

The semantics of each property kind are defined in primitive-sp.md. An annotated reference with examples for each kind is in §8.3.3.

8.3.2 Direct Annotation Syntax

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() {
}

`#[rapx::requires(...)]`

Declares a precondition on an (usually unsafe) function. Each attribute holds one property; group with commas or repeat the attribute:

#![allow(unused)]
fn main() {
// Repeated attributes …
#[rapx::requires(ValidPtr(ptr, u32, 1))]
#[rapx::requires(Align(ptr, u32))]

// … are equivalent to a single grouped attribute
#[rapx::requires(ValidPtr(ptr, u32, 1), Align(ptr, u32))]
}

A complete example:

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

`#[rapx::verify]`

Marks a function as a verification entry point for --mode targeted (Chapter 8.1.2). It takes no arguments and is orthogonal to #[rapx::requires].

`#[rapx::invariant(...)]`

Declares a struct-level invariant that must hold for every instance at all observable points (see Chapter 8.4):

#![allow(unused)]
fn main() {
#[rapx::invariant(ValidPtr(ptr, T, cap))]
#[rapx::invariant(Align(ptr, T))]
pub struct MyBuf<T> {
    ptr: *mut T,
    len: usize,
    cap: usize,
}
}

`any(...)` Combinator

The any(...) combinator represents logical OR between disjuncts, where commas inside each parenthesized disjunct mean logical AND:

any((Null(p)), (P1(p, ...), P2(p, ...), ...))

The currently supported shape is a null guard: exactly two disjuncts, one being Null(p) alone, the other a conjunction of properties over the same place p. The semantics: the conjunct properties hold whenever p is non-null, and the whole contract is satisfied when p is null. This works in both #[rapx::requires] and #[rapx::invariant] positions:

In requires: The SMT solver encodes (p == 0) ∨ (P1 ∧ P2). If the caller's state satisfies either branch, the contract is proved. This is useful for functions like ptr::as_ref() that accept null pointers — the contract declares the pointer may be null, but must be valid and aligned when non-null:

#![allow(unused)]
fn main() {
#[rapx::requires(any(Null(self), (ValidPtr(self, T, 1), Align(self, T))))]
pub unsafe fn as_ref<'a, T>(self: *const T) -> Option<&'a T> { /* ... */ }
}

In invariant: Used for struct fields that may be null (e.g., linked list tail pointers). Combined with dominance information from null checks in user code (if ptr.is_null() { return; }), the verifier determines which branch to prove:

#![allow(unused)]
fn main() {
#[rapx::invariant(any((Null(next)), (ValidPtr(next, Node, 1), Align(next, Node))))]
pub struct Node {
    value: u32,
    next: *mut Node,
}
}

In both cases, any(Null(p), (P1, P2)) expands to individual Property objects for P1 and P2, each tagged with the null-guard place. The SMT checker then asserts p != 0 before proving each conjunct, which is equivalent to proving (p == 0) ∨ P_i_holds.

Contract Kind Metadata

A property may carry a trailing kind = "<string>" tag inside the same attribute. Two ContractKind values are recognized:

kind = "precond" (default): A normal safety precondition. An Unproved verdict for this kind contributes to the UNSOUND result.
kind = "hazard": An advisory warning about a known unsafety pattern. An Unproved verdict for this kind does not contribute to the UNSOUND count — it is printed as an informational [hazard] entry. Set via kind = "hazard" inside #[rapx::requires]:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidNum(size_of::<T>() * len <= isize::MAX), kind = "hazard")]
pub unsafe fn from_raw_parts<T>(ptr: *const T, len: usize) -> *const [T] {
    // ...
}
}

The Alias property is always classified as hazard automatically. Hazard contracts are also used in std-public-contracts.json to flag known but currently unprovable constraints.

Places accepted in annotations

Parameter names in requires: self, ptr, index, len.
Field names in invariant: ptr, cap, head — no self. prefix.
Field projections in requires (via self): self.0, self.ptr.
Length sugar: self.len is read as len(self).
Const generics: N resolves to the enclosing item's const parameter.

8.3.3 Property Reference

`Alias(p1, p2)`

p1 == p2 — the two places refer to the same memory. Always a hazard: unproved Alias does not block SOUND, but is reported as a [hazard] entry. 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))]
}

`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. The fourth argument (allocator) defaults to global when omitted. psp II.2.

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

`Deref(ptr, Ty, count)`

Allocated ∧ InBound — the pointer can be safely dereferenced. primitive-sp §2.2.

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

`InBound` / `InBounded`

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

Form	Example
`InBound(slice, index)`	`#[rapx::requires(InBound(self, i))]`
`InBound(ptr, Ty, count)`	`#[rapx::requires(InBound(ptr, u32, len))]`

The slice form supports all SliceIndex types and expands to the correct bounds check. psp II.3.

`Init(ptr, Ty, count)`

Memory is initialized for count elements of Ty. Stronger than Typed: Init implies Typed but not vice versa. psp III.4.

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

`Layout(ptr, layout)`

ValidNum(rem(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))]
}

`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(a, b, T, count)`

The memory ranges (a, sizeof(T) * count) and (b, sizeof(T) * count) are pairwise disjoint. psp II.4.

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

`NonVolatile(p, T, len)`

Memory is not volatile — no other thread writes to the region (p, sizeof(T) * len). psp V.2.

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

`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.

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

`Owning(ptr)`

ownership(*p) == none — the pointer is the sole carrier of ownership; no live owner aliases the pointee. psp IV.1.

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

`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.

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

`Ptr2Ref(ptr, T)`

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

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

`Size(T, c)` / `NonSize(T, c)`

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

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).

NonSize is an alias for Size. psp I.2.

#![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)`

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. psp III.6.

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

`Unreachable`

The code path is unreachable. psp V.5.

#![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.

#![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.

1-arg predicate form — a comparison expression. Supported operators: <, <=, >, >=, ==, !=. A bare identifier is treated as != 0.

#![allow(unused)]
fn main() {
#[rapx::requires(ValidNum(index < len))]
#[rapx::requires(ValidNum(size_of::<T>() * len <= isize::MAX))]
}

2-arg interval form — a value constrained to a range. The interval can be an array literal [lo, hi] (inclusive both ends) or a string using bracket notation "[lo, hi]" where [/] means inclusive and (/) means exclusive:

#![allow(unused)]
fn main() {
#[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
}

`ValidPtr(ptr, Ty, count)`

(ptr as usize) % align_of::<Ty>() != 0 — the pointer is valid for reading and writing count elements of Ty. Defined in primitive-sp §2.2: for ZSTs vacuously true; for non-ZSTs equivalent to Allocated ∧ InBound.

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

`ValidString(ptr, u8, len)`

The byte data at ptr for len bytes is valid UTF-8. psp III.2.

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

`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]))]
}

8.3.4 JSON Contracts

Standard-library functions that cannot be annotated upstream use JSON contracts in std-public-contracts.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"] }
  ]
}

The 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.5 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. Run them together for both views.

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

14:43:38|RAPx|INFO|: [rapx::debug-contracts] Expanded Contract Assertions
14:43:38|RAPx|INFO|: ============================================================
14:43:38|RAPx|INFO|: 
14:43:38|RAPx|INFO|: fn LinkedList::from_vec(values: std::vec::Vec<i32>) -> LinkedList
14:43:38|RAPx|INFO|: -------------------------------------------------------------------
14:43:38|RAPx|INFO|:   Safety Tag: Align(head.unwrap_some(), Node)
14:43:38|RAPx|INFO|:     Meaning:   (head.unwrap_some() as usize) % align_of::<Node>() == 0
14:43:38|RAPx|INFO|:   Safety Tag: Allocated(head.unwrap_some(), Node, 1)
14:43:38|RAPx|INFO|:     Meaning:   head.unwrap_some() points to live heap/stack allocation, Node, 1
14:43:38|RAPx|INFO|:   Safety Tag: Owning(head.unwrap_some())
14:43:38|RAPx|INFO|:     Meaning:   ownership(*head.unwrap_some()) = none
14:43:38|RAPx|INFO|: 
14:43:38|RAPx|INFO|: fn std::ptr::NonNull::<T>::as_mut::<'a>(&mut self: &mut std::ptr::NonNull<T>) -> &'a mut T
14:43:38|RAPx|INFO|: -------------------------------------------------------------------
14:43:38|RAPx|INFO|:   Safety Tag: Ptr2Ref(self.0, T)
14:43:38|RAPx|INFO|:     Meaning:   can soundly convert self.0 to &/&mut reference
14:43:38|RAPx|INFO|: 
14:43:38|RAPx|INFO|: fn std::boxed::Box::<T>::from_raw(raw: *mut T) -> std::boxed::Box<T>
14:43:38|RAPx|INFO|: -------------------------------------------------------------------
14:43:38|RAPx|INFO|:   Safety Tag: [hazard] Alias(raw, ret)
14:43:38|RAPx|INFO|:     Meaning:   raw and ret alias each other (hazard)

Use --debug-contracts together with --prepare-targets to see both contract resolution and their semantics in one pass.

Rust Analysis Platform