Chapter 8.3. Safety Property Contracts

RAPx verifies safety through explicit contracts declared in source code. A contract is a logical statement about pointer validity, numeric bounds, ownership, and other safety properties that RAPx checks against a function's MIR. This chapter covers the two kinds of contract (§8.3.1), how to attach them to code (§8.3.2), and how to inspect the resolved assertions (§8.3.3).

8.3.1 Contracts

A contract is either a built-in property shipped with RAPx, or a user-defined contract composed from the built-ins.

8.3.1.1 Built-in Properties

The semantics of each property kind are defined in primitive-sp.md. The annotated reference with examples:

Alias(p1, p2)

p1 == p2 — the two places refer to the same memory. Always a hazard: unproved Alias is reported as a [hazard] entry and contributes to UNSOUND. 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

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

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

For ZSTs vacuously true; for non-ZSTs equivalent to Allocated(ptr, Ty, count) ∧ InBound(ptr, Ty, count) — the pointer points to a live allocation and the access range is within bounds. primitive-sp §2.2.

#![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.1.2 User-Defined Contracts

In addition to the built-in tags, you can define new named contracts inside your crate with the pred! macro (from rapx_macros). A user-defined contract is a boolean combination of the primitive properties: it adds no new semantics — it is a pure front-end that expands to ordinary Property objects, so no rapx rebuild is required.

To use pred!, add rapx-macros as a dependency and enable the rapx tool attribute — the same nightly register_tool setup used for every #[rapx::...] attribute (see §8.3.2.1):

[dependencies]
rapx-macros = "0.7.34"

#![allow(unused)]
#![feature(register_tool)]
#![register_tool(rapx)]
fn main() {
}

A def is written as a pred! block of the form Name(params) { body }. Its parameters are typed Ptr (a target place), Ty (a type), Expr (a numeric expression), or Ident (an identifier such as a trait name, enum variant, allocator, or lifetime). By convention the contract name is CamelCase, matching the built-in compounds (ValidPtr, Deref, Ptr2Ref, …):

#![allow(unused)]
fn main() {
use rapx_macros::pred;

pred!(MySafeRead(p: Ptr, T: Ty, n: Expr) { NonNull(p) && Align(p, T) && Allocated(p, T, n) });
}

The block is not compiled as Rust: the macro serializes its source text into a #[rapx::def_contract("...")] tool attribute that the verifier parses at analysis time. Once defined, the name becomes a first-class tag usable wherever a property is expected:

#![allow(unused)]
fn main() {
#[rapx::requires(MySafeRead(ptr, u8, len))]
pub unsafe fn read_byte(ptr: *const u8, len: usize) -> u8 {
    unsafe { *ptr }
}
}

DSL grammar

A def body is parsed by a small pest grammar (the single source of truth, in grammar.pest). The surface:

Boolean composition — the body is a DNF expression: || separates disjuncts, && joins conjuncts, and parentheses group a conjunction into a single disjunct.

def_body = or_expr
or_expr = and_expr ("||" and_expr)*
and_expr = def_leaf ("&&" def_leaf)*
def_leaf = tag_call | "(" or_expr ")"

#![allow(unused)]
fn main() {
pred!(DerefOrNull(p: Ptr, T: Ty, n: Expr) { Null(p) || (Allocated(p, T, n) && InBound(p, T, n)) });
}

Argument expressions — a tag's arguments are numeric/place expressions with the usual operators:

LayerOperators
comparison== != < <= > >=
bitwise\| ^ &
arithmetic+ - * / %
unary! -

Built-in functions — size_of(T), align_of(T), len(x), min(a, b), max(a, b). Turbofish size_of::<T>() is not supported — write size_of(T).

Places and projections — a place is self, return, Arg_N, or an identifier, optionally followed by projections:

  • .0 / .name — field access (self.0, self.ptr).
  • .unwrap_some() — unwrap an Option payload (head.unwrap_some()).
  • .iter() — iterate the elements of a container (buckets.iter()).

Type-level constants — T::MAX, T::MIN (e.g. isize::MAX).

Conditionals — if cond { e1 } else { e2 } is an expression usable in argument (Expr) position, e.g. to special-case ZSTs (as in the std-challenge-18 case study):

#![allow(unused)]
fn main() {
pred!(ZstAwareInBound(ptr: Ptr, T: Ty, end_or_len: Expr) {
    InBound(ptr, T, if size_of(T) == 0 { 0 } else { (end_or_len - ptr) / size_of(T) })
});
}

!x.is_empty() is sugar for len(x) != 0, usable as a condition or ValidNum predicate when x is a slice/container place such as self (e.g. ValidNum(!self.is_empty())) — not for a raw pointer.

A def body may reference other defs as well as primitives. The same mechanism defines RAPx's built-in compound properties (ValidPtr, Deref, Ptr2Ref, …) in std-contracts.rs — using the same Name(params) { body } syntax, so a user can read the bundled compounds and write their own the same way. See tests/verify_units/dsl_custom_def for a complete SOUND example.

8.3.2 Contract Annotation

8.3.2.1 Direct Annotation

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

Three attributes carry contracts:

  • #[rapx::requires(...)] — a precondition on an (usually unsafe) function. Multiple properties can be comma-grouped or the attribute repeated.
  • #[rapx::invariant(...)] — a struct-level invariant that must hold for every instance at all observable points (see Chapter 8.4).
  • #[rapx::verify] — marks a function as a verification entry point for --mode targeted (Chapter 8.1.2).
#![allow(unused)]
fn main() {
#[rapx::requires(ValidPtr(ptr, u32, len))]
#[rapx::requires(Align(ptr, u32))]
#[rapx::requires(ValidNum(index < len))]
pub unsafe fn write_slice(ptr: *mut u32, len: usize, index: usize) {
    // ...
}
}

The any(D1, D2) combinator expresses a null guard: any(Null(p), (P1(p, ...), P2(p, ...))) — the conjunct properties hold when p is non-null, and the whole contract is vacuously satisfied when p is null.

A property may carry kind = "precond" | "hazard" | "option" metadata (e.g. #[rapx::requires(..., kind = "hazard")]); Alias is always classified hazard.

Places accepted in annotations: parameter names (self, ptr, index, len), field names in invariant (ptr, cap, head — no self. prefix), field projections (self.0, self.ptr), length sugar (self.len → len(self)), and const generics (N).

8.3.2.2 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"] }
  ]
}

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.3 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. Note that --prepare-targets and --debug-contracts are mutually exclusive; run them in separate invocations for both views.

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

13:10:58|RAPx|INFO|: ============================================================================
13:10:58|RAPx|INFO|: [rapx::debug-contracts] struct: LinkedList
13:10:58|RAPx|INFO|: ============================================================================
13:10:58|RAPx|INFO|:   [Struct Invariants]:
13:10:58|RAPx|INFO|:   |- Align(head.unwrap_some(), Node<T>)
13:10:58|RAPx|INFO|:   |  (head.unwrap_some() as usize) % align_of::<Node<T>>() == 0
13:10:58|RAPx|INFO|:   |- Allocated(head.unwrap_some(), Node<T>, 1)
13:10:58|RAPx|INFO|:   |  head.unwrap_some() points to a live allocation of size: size_of(Node<T>) * 1
13:10:58|RAPx|INFO|:   |- Typed(head.unwrap_some(), Node<T>)
13:10:58|RAPx|INFO|:   |  *head.unwrap_some() holds TypeInvariant(Node<T>)
13:10:58|RAPx|INFO|:   `- Owning(head.unwrap_some())
13:10:58|RAPx|INFO|:      ownership(*head.unwrap_some()) = none: no live owner aliases the pointee
13:10:58|RAPx|INFO|: 
13:10:58|RAPx|INFO|: |- --- method: pop_front ---------------------------------------------------
13:10:58|RAPx|INFO|: |   fn LinkedList::<T>::pop_front(&mut self: &mut LinkedList<T>) -> std::option::Option<T>
13:10:58|RAPx|INFO|: |   [Unsafe Callees]:
13:10:58|RAPx|INFO|: |   |- fn std::boxed::Box::<T>::from_raw(raw: *mut T) -> std::boxed::Box<T>
13:10:58|RAPx|INFO|: |   | |- Align(raw, T)
13:10:58|RAPx|INFO|: |   | |  (raw as usize) % align_of::<T>() == 0
13:10:58|RAPx|INFO|: |   | |- Allocated(raw, T, 1, global)
13:10:58|RAPx|INFO|: |   | |  raw points to a live allocation of size: size_of(T) * 1
13:10:58|RAPx|INFO|: |   | |- Typed(raw, T)
13:10:58|RAPx|INFO|: |   | |  *raw holds TypeInvariant(T)
13:10:58|RAPx|INFO|: |   | |- Owning(raw)
13:10:58|RAPx|INFO|: |   | |  ownership(*raw) = none: no live owner aliases the pointee
13:10:58|RAPx|INFO|: |   | `- [hazard] Alias(raw, ret)
13:10:58|RAPx|INFO|: |   |    raw and ret alias each other (hazard)
13:10:58|RAPx|INFO|: |   `- fn std::ptr::NonNull::<T>::as_mut::<'a>(&mut self: &mut std::ptr::NonNull<T>) -> &'a mut T
13:10:58|RAPx|INFO|: |     `- Ptr2Ref(self.0, T)
13:10:58|RAPx|INFO|: |        A raw pointer meets all requirements for sound &/&mut conversion: initialized, aligned, no aliasing conflict.
13:10:58|RAPx|INFO|: 
13:10:58|RAPx|INFO|: ... (8 more methods)