Chapter 10.1. Verifying core::slice Safety (Challenge 17)

This case study demonstrates how RAPx verifies safety contracts in the Rust standard library's slice module, targeting Challenge 17: Verify the safety of slice functions from the Verify Rust Std Lib project.

10.1.1 Goal

Prove that all 37 challenge-listed functions in library/core/src/slice/mod.rs are free of undefined behavior by:

• Writing #[rapx::requires(...)] safety preconditions on unsafe callees
• Adding #[rapx::verify] annotations to trigger verification
• Running RAPx in targeted mode against the annotated functions

The verification must be unbounded (valid for slices of arbitrary length) and must hold for generic type T without monomorphization.

10.1.2 Tool Integration

Following the same conditional pattern as Kani (#[cfg_attr(kani, ...)]) and Flux (#[cfg(flux)]), the project uses cfg_attr to avoid hard-coding register_tool in source code:

• core/src/lib.rs: No #![register_tool(rapx)] — tool registration is injected via RUSTFLAGS
• core/Cargo.toml: ['cfg(rapx)'] declared in [lints.rust.unexpected_cfgs] to suppress unknown cfg warnings
• Source files: #[cfg_attr(rapx, rapx::verify)] and #[cfg_attr(rapx, rapx::requires(...))] conditionally activate only when RAPx runs

#![allow(unused)]
fn main() {
// Example from core/src/slice/mod.rs
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(a, "[0,self.len())")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(b, "[0,self.len())")))]
pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) { /* ... */ }
}

Run verification:

cd library/core
RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)" \
  cargo rapx verify --module slice --mode targeted

Note: Commands must be run from library/core, not the library workspace root. In the library workspace, core is only a dependency (the members are std, sysroot, coretests, alloctests), and RAPx analyzes a crate only when it is compiled as the primary package. Running from library/core makes core local, so its #[rapx::verify] annotations are visible without needing the --crate core filter.

The RUSTFLAGS environment variable provides three things:

A GitHub Actions workflow (.github/workflows/rapx.yml) runs verification on every push and pull request, using the same RUSTFLAGS setup. It pins a specific RAPx commit via RAPX_VERSION, cds into library/core, and invokes cargo rapx verify --module slice --mode targeted.

10.1.3 Function-by-Function Verification

Slice type invariant. Every target is a method on the primitive [T] (no #[rapx::invariant] struct), so RAPx relies on the slice type invariant declared in std-type-invariants.json under the [T] key. This runs in two independent places:

1. Entry (init_parameters) — for a &[T] / &mut [T] parameter self, the VM establishes the slice's validity as symbolic state:

   • the slice type invariant (re-proved at return): NonNull (flag non_null), Align (flag aligned), the length bound len * size_of(T) <= isize::MAX, and any(len(self) == 0, (Allocated, Init)) — the data allocation itself plus element initialization, required only for non-empty slices;
   • entry fact: the non-negativity bound 0 <= len (the usize length is never negative);
   • the data allocation itself carries align = align_of(T), size = len · sizeof_T, element_ty = T, where sizeof_T is the shared symbolic element size (≥ 1 for a generic T; the invariant's size_of(T) bound is instead the concrete impl-layout size).

2. Return (type-invariant re-proof) — the properties re-proved at the function's Return block are exactly the ones declared by the JSON entry:

"[T]": {
  "invariants": [
    { "tag": "NonNull", "args": ["$self"] },
    { "tag": "Align", "args": ["$self", "$elem"] },
    { "tag": "ValidNum", "args": ["size_of($elem) * len($self) <= isize::MAX"] },
    {
      "any": [
        { "tag": "ValidNum", "args": ["len($self) == 0"] },
        [
          { "tag": "Allocated", "args": ["$self", "$elem", "len($self)"] },
          { "tag": "Init", "args": ["$self", "$elem", "len($self)"] }
        ]
      ]
    }
  ]
}

NonNull and Align hold for every slice — even an empty one, whose dangling data pointer (NonNull::dangling) is still non-null and properly aligned (Rust requires alignment for size-0 access). Allocated and Init hold only for non-empty slices, so they are wrapped in any(len == 0, …). The length bound len * size_of(T) <= isize::MAX is part of the re-proved invariant — for the parameter it is fixed at entry (the reference's address and length are immutable), and for a returned slice it is re-proved at return (and re-enforced at from_raw_parts, whose own contract carries the same ValidNum). The 0 <= len bound is just the usize non-negativity. Align is likewise re-checked at &*ptr (Ptr2Ref = Init + ValidPtr + Align + Alias, where ValidPtr = NonNull + Deref).

10.1.3.1 get_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(InBound(self, index)))]
pub const unsafe fn get_unchecked<I>(&self, index: I) -> &I::Output
where
    I: [const] SliceIndex<Self>,
{
    unsafe { &*index.get_unchecked(self) }
}
}

Verification Targets. The body &*index.get_unchecked(self) desugars into two unsafe operations:

(1) index.get_unchecked(self) — the SliceIndex::get_unchecked trait call, returning a raw pointer *const Output.

(2) &*ptr — the raw-pointer dereference that turns that pointer back into a reference. RAPx models this as a Ptr2Ref(p, T) checkpoint, decomposed into four obligations: Init(p, T, 1) + ValidPtr(p, T, 1) + Align(p, T) + Alias(p), where ValidPtr = NonNull + Deref.

On top of these, the &[T] receiver self carries a slice type invariant (NonNull + Align + ValidNum(size_of(T)·len <= isize::MAX) + any(len == 0, (Allocated, Init))) that init_parameters establishes at entry and that is re-proved at the function's return block.

Path. The two unsafe operations sit on the normal path bb0 → bb1 (get_unchecked in bb0, the &* deref in bb1). The &[T] invariant is re-proved only at the return block bb1 — RAPx re-proves type invariants at Return blocks, not at the cleanup resume in bb2 (the panic-unwind path, never taken here).

MIR (compiled with nightly-2025-11-25; locals _1 = self, _2 = index):

bb0: _5 = move _2;
     _6 = &raw const (*_1);
     _4 = <I as SliceIndex<[T]>>::get_unchecked(move _5, move _6) -> [return: bb1, unwind: bb2];
bb1: _3 = &(*_4);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _0 = &(*_3);   // safe reborrow, no checkpoint
     return;
bb2 (cleanup): resume;

Verification. The VM steps the path statement by statement. For every local it records a symbolic value (VmValue) with three parts:

• term — a Z3 integer: the pointer's address (for references/pointers) or the scalar's value;
• prov — provenance (alloc, offset): which allocation the pointer derives from, at what byte offset;
• flags — known invariants non_null / aligned / init.

alloc(x) is the memory object (Allocation) that local x points into — its prov carries an AllocId into the VM's allocation table, where each entry holds base / size / align and the marks initialized / alive_assumed / dead.

The #[rapx::requires] fact (InBound) is recorded at entry as the numeric bound index < len (a path condition), while the slice type invariant (NonNull/Align/ValidNum(size_of(T)·len <= isize::MAX)/any(len == 0, (Allocated, Init))) is established by init_parameters itself and re-proved at return. Each InBound checkpoint is discharged by SMT over that recorded bound and the allocation's base/size. For a generic T the element size is a shared symbolic constant sizeof_T (≥ 1) rather than a monomorphized byte count: the data allocation's byte size is len·sizeof_T, and the SMT cancels that factor (len·sizeof_T / sizeof_T = len) to recover the element count for InBound. The path, step by step:

entry   _1 = self (&[T]), _2 = index (I)

          init_parameters:
            data alloc: align = align_of(T), size = len · sizeof_T, element_ty = T, initialized = true
            _1: term = data base, prov = (data alloc, 0), flags { non_null, aligned, init }
               slice type invariant (JSON `[T]` entry; entry facts synthesized by `init_parameters`; re-proved at return):
                 NonNull(_1)
                 Align(_1, T)
                 len(_1)·size_of(T) ≤ isize::MAX   (size_of(T) = the concrete impl-layout bound, = 1 for a fully generic T)
                 any(len(_1) == 0, (Allocated(_1, T, len(_1)), Init(_1, T, len(_1))))
               entry fact: 0 ≤ len(_1)  (usize non-negativity)
            _2: term = param_2 (fresh symbolic)

          caller contracts (asserted as facts):
            InBound(_1, _2)      →  _2 < len(_1)

_5 = move _2
          VM  _5: term = _2.term

_6 = &raw const (*_1)
          VM  _6: term = _1.term, prov = _1.prov, flags { non_null }

_4 = get_unchecked(move _5, move _6)                    [checkpoint (1)]
          check  InBound(_6, _5)   ←  _5 < len(_6)         Proved
                              (SMT: _5 = _2 (move _2); _6 aliases _1, so len(_6) = len(_1)
                               = size/sizeof_T = len (cancels sizeof_T);
                               thus _5 < len(_6) ⟺ _2 < len(_1) — the `InBound(_1, _2)` entry fact)
          VM  _4: term = _6.term + _5·sizeof_T, prov = (_6.alloc, _6.offset + _5·sizeof_T)

_3 = &(*_4)                                             [checkpoint (2)]
          check  Init(_4, T, 1)     ←  alloc(_4).initialized         Proved
          check  ValidPtr(_4, T, 1) ←  non-null + in-bounds (within _1's data alloc)   Proved
          check  Align(_4, T)       ←  _6 aligned to T (from _1's data alloc), _5·sizeof_T keeps alignment   Proved
          check  Alias(_4)          ←  (hazard) _4 traces to &self, a shared borrow → aliasing safe   Proved
          VM  _3: term = _4.term, prov = _4.prov, flags { non_null, aligned, init }

_0 = &(*_3)
          VM  _0: term = _3.term, prov = _3.prov, flags { non_null, aligned, init }

return                                                   [type-invariant]
          check  NonNull(_1), Align(_1, T), len(_1)·size_of(T) ≤ isize::MAX,
                 any(len(_1) == 0, (Allocated(_1, T, len), Init(_1, T, len)))  ←  _1 unchanged   Proved

result: SOUND

10.1.3.2 get_unchecked_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(InBound(self, index)))]
pub const unsafe fn get_unchecked_mut<I>(&mut self, index: I) -> &mut I::Output
where
    I: [const] SliceIndex<Self>,
{
    unsafe { &mut *index.get_unchecked_mut(self) }
}
}

Verification Targets. &mut *index.get_unchecked_mut(self) desugars into the same two unsafe callsites, on the mutable receiver:

(1) index.get_unchecked_mut(self) — the SliceIndex::get_unchecked_mut trait call, returning *mut Output.

(2) &mut *ptr — the reference creation from that raw pointer (a Ptr2Ref operation: Init + ValidPtr + Align + Alias, exclusive).

Path. Both callsites sit on the single normal path bb0 → bb1 (get_unchecked_mut in bb0, the &mut * deref in bb1); the cleanup blocks bb3…bb5 are dead on the normal path.

MIR. The statements on that path:

bb0: _8 = &raw mut (*_1);
     _6 = <I as SliceIndex<[T]>>::get_unchecked_mut(move _7, move _8) -> [return: bb1, unwind: bb3];
bb1: _5 = &mut (*_6);   // &mut * — raw-pointer deref (Ptr2Ref checkpoint)
     _4 = &mut (*_5);   // safe reborrows, no checkpoint
     _3 = &mut (*_4);
     _0 = &mut (*_3);
bb2: return

Verification. Same as get_unchecked, on the mutable receiver:

10.1.3.3 swap_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(a, "[0,self.len())")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(b, "[0,self.len())")))]
pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) {
    assert_unsafe_precondition!(
        check_library_ub,
        "slice::swap_unchecked requires that the indices are within the slice",
        (len: usize = self.len(), a: usize = a, b: usize = b,) => a < len && b < len,
    );
    let ptr = self.as_mut_ptr();
    unsafe {
        ptr::swap(ptr.add(a), ptr.add(b));
    }
}
}

Verification Targets. The single unsafe callsite ptr::swap(ptr.add(a), ptr.add(b)):

#![allow(unused)]
fn main() {
// core::ptr::swap
#[rapx::requires(ValidPtr(x, T, 1))]
#[rapx::requires(Align(x, T))]
#[rapx::requires(ValidPtr(y, T, 1))]
#[rapx::requires(Align(y, T))]
}

Path. assert_unsafe_precondition! lowers to a precondition_check panic guard (guarded by UbChecks), which is not an unsafe checkpoint; the single unsafe callsite is reached on the normal path bb0 → bb1 → bb2 → bb3 → bb5 → bb6 → bb7 → bb8.

MIR. The statements on that path:

bb5: _11 = as_mut_ptr(&mut (*_1));
bb6: _14 = ptr.add(copy _11, _2);   // ptr.add(a)
bb7: _17 = ptr.add(copy _11, _3);   // ptr.add(b)
bb8: _13 = ptr::swap(move _14, move _17);   // ← checkpoint

Verification. The pipeline runs Entry → VM execution → property check over the extracted path.

Entry. The preconditions ValidNum(a, "[0,self.len())") and ValidNum(b, "[0,self.len())") (i.e. a < len && b < len), plus the &mut [T] slice invariant.

VM execution.

Property check. ptr.add(a) and ptr.add(b) stay within the slice because a < len and b < len, so both element pointers satisfy ValidPtr + Align (inherited from the slice's data pointer). ptr::swap is defined for a == b, so no overlap obligation arises.

10.1.3.4 as_chunks_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(N, "[1,)")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(len(self) % N == 0)))]
pub const unsafe fn as_chunks_unchecked<const N: usize>(&self) -> &[[T; N]] {
    assert_unsafe_precondition!(
        check_language_ub,
        "slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
        (n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n),
    );
    // SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length
    let new_len = unsafe { exact_div(self.len(), N) };
    // SAFETY: We cast a slice of `new_len * N` elements into
    // a slice of `new_len` many `N` elements chunks.
    unsafe { from_raw_parts(self.as_ptr().cast(), new_len) }
}
}

Verification Targets. Two unsafe callsites:

(1) exact_div(self.len(), N) — requires a non-zero divisor;

(2) from_raw_parts(self.as_ptr().cast(), new_len):

#![allow(unused)]
fn main() {
// core::slice::raw::from_raw_parts
#[rapx::requires(NonNull(data))]
#[rapx::requires(ValidPtr(data, T, len))]
#[rapx::requires(Init(data, T, len))]
#[rapx::requires(Alive(data, 'a))]
#[rapx::requires(Alias(data))]
#[rapx::requires(Align(data, T))]
#[rapx::requires(ValidNum(size_of(T) * len <= isize::MAX))]
}

Path. After the precondition_check guard, the two callsites are reached in order on the normal path … → bb7 → bb8 → bb9 → bb10 (exact_div in bb7, from_raw_parts in bb10).

MIR. The statements on that path:

bb6:  _8 = len(&(*_1));
bb7:  _7 = exact_div(move _8, const N);                  // ← checkpoint (1)
bb8:  _12 = as_ptr(&(*_1));
bb9:  _11 = ptr.cast::<[T; N]>(move _12);
bb10: _10 = raw::from_raw_parts(move _11, copy _7);      // ← checkpoint (2)
bb11: _0 = &(*_10);

Verification.

Entry. The preconditions ValidNum(N, "[1,)") (N != 0) and ValidNum(len(self) % N == 0), plus the &[T] slice invariant.

VM execution.

Property check.

• (1) exact_div's non-zero divisor: discharged by N != 0.
• (2) from_raw_parts's ValidPtr/InBound/ValidNum: len % N == 0 gives len = new_len * N, so the byte size size_of([T; N]) * new_len equals the slice's own size. NonNull/Align/Init/Allocated are inherited from the slice invariant, while ValidPtr/ValidNum/Alive/Alias follow from the slice's full validity established at entry. The cast re-interprets T as [T; N], layout-identical by construction.

10.1.3.5 as_chunks_unchecked_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(N, "[1,)")))]
#[cfg_attr(rapx, rapx::requires(ValidNum(len(self) % N == 0)))]
pub const unsafe fn as_chunks_unchecked_mut<const N: usize>(&mut self) -> &mut [[T; N]] {
    assert_unsafe_precondition!(
        check_language_ub,
        "slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks",
        (n: usize = N, len: usize = self.len()) => n != 0 && len.is_multiple_of(n)
    );
    let new_len = unsafe { exact_div(self.len(), N) };
    unsafe { from_raw_parts_mut(self.as_mut_ptr().cast(), new_len) }
}
}

Verification Targets. Same two callsites as as_chunks_unchecked — exact_div(self.len(), N) and from_raw_parts_mut(self.as_mut_ptr().cast(), new_len) (the _mut variant of the from_raw_parts contract, adding Alias).

Path. … → bb7 → bb8 → bb9 → bb10 (exact_div in bb7, from_raw_parts_mut in bb10).

MIR. The statements on that path:

bb6:  _9 = len(&(*_1));
bb7:  _8 = exact_div(move _9, const N);                  // ← checkpoint (1)
bb8:  _14 = as_mut_ptr(&mut (*_1));
bb9:  _13 = ptr.cast::<[T; N]>(move _14);
bb10: _12 = raw::from_raw_parts_mut(move _13, copy _8);  // ← checkpoint (2)
bb11: _0 = &mut (*_12);

Verification. Identical to as_chunks_unchecked: (1) exact_div's divisor discharged by N != 0; (2) from_raw_parts_mut's ValidPtr/InBound/ValidNum discharged by len % N == 0, and its Alias obligation discharged by the exclusive &mut self receiver.

10.1.3.6 split_at_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(mid, [0,self.len()])))]
pub const unsafe fn split_at_unchecked(&self, mid: usize) -> (&[T], &[T]) {
    let len = self.len();
    let ptr = self.as_ptr();
    assert_unsafe_precondition!(
        check_library_ub,
        "slice::split_at_unchecked requires the index to be within the slice",
        (mid: usize = mid, len: usize = len) => mid <= len,
    );
    // SAFETY: Caller has to check that `0 <= mid <= self.len()`
    unsafe { (from_raw_parts(ptr, mid), from_raw_parts(ptr.add(mid), unchecked_sub(len, mid))) }
}
}

Verification Targets. Two from_raw_parts callsites, each carrying the full slice contract:

#![allow(unused)]
fn main() {
// core::slice::raw::from_raw_parts — required by both calls
#[rapx::requires(NonNull(data))]
#[rapx::requires(ValidPtr(data, T, len))]
#[rapx::requires(Init(data, T, len))]
#[rapx::requires(Alive(data, 'a))]
#[rapx::requires(Alias(data))]
#[rapx::requires(Align(data, T))]
#[rapx::requires(ValidNum(size_of(T) * len <= isize::MAX))]
}

Path. After the precondition_check guard, both callsites are reached on the normal path … → bb6 → bb7 → bb8 (left from_raw_parts in bb6, right one in bb8).

MIR. The statements on that path:

bb0: _3 = len(&(*_1));
bb1: _5 = as_ptr(&(*_1));
bb6: _13 = raw::from_raw_parts(copy _5, copy _2);        // ← checkpoint (1), left [0, mid)
bb7: _18 = ptr.add(copy _5, copy _2);                   // ptr.add(mid)
bb8: _21 = SubUnchecked(copy _3, copy _2);              // len - mid
     _17 = raw::from_raw_parts(move _18, move _21);     // ← checkpoint (2), right [mid, len)

Verification.

Entry. The precondition ValidNum(mid, [0,self.len()]) (0 <= mid <= len), plus the &[T] slice invariant.

VM execution. _5 = as_ptr(_1) carries the slice's provenance; _18 = ptr.add(_5, _2) is the mid pointer; _21 = len - mid the right length.

Property check.

• (1) from_raw_parts(ptr, mid): in bounds by mid <= len → Proved.
• (2) from_raw_parts(ptr.add(mid), len - mid): covers [mid, len), in bounds; SubUnchecked(len, mid) is safe by mid <= len → Proved.

mid == len yields an empty right slice with a one-past-the-end pointer, which is valid.

10.1.3.7 split_at_mut_unchecked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidNum(mid, [0,self.len()])))]
pub const unsafe fn split_at_mut_unchecked(&mut self, mid: usize) -> (&mut [T], &mut [T]) {
    let len = self.len();
    let ptr = self.as_mut_ptr();
    assert_unsafe_precondition!(
        check_library_ub,
        "slice::split_at_mut_unchecked requires the index to be within the slice",
        (mid: usize = mid, len: usize = len) => mid <= len,
    );
    unsafe {
        (
            from_raw_parts_mut(ptr, mid),
            from_raw_parts_mut(ptr.add(mid), unchecked_sub(len, mid)),
        )
    }
}
}

Verification Targets. Two from_raw_parts_mut callsites, each requiring the _mut variant of the from_raw_parts contract (adding Alias for exclusive access).

Path. … → bb6 → bb7 → bb8 (left from_raw_parts_mut in bb6, right one in bb8).

MIR. The statements on that path:

bb0: _3 = len(&(*_1));
bb1: _5 = as_mut_ptr(&mut (*_1));
bb6: _13 = raw::from_raw_parts_mut(copy _5, copy _2);      // ← checkpoint (1), left [0, mid)
bb7: _18 = ptr.add(copy _5, copy _2);                      // ptr.add(mid)
bb8: _21 = SubUnchecked(copy _3, copy _2);                 // len - mid
     _17 = raw::from_raw_parts_mut(move _18, move _21);    // ← checkpoint (2), right [mid, len)

Verification. Same as split_at_unchecked: the bounds are discharged by 0 <= mid <= len; the two halves [0, mid) and [mid, len) are disjoint, so their Alias obligations are discharged by that disjointness plus the exclusive receiver.

10.1.3.8 align_to

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::requires(ValidTransmute(T, U)))]
#[cfg_attr(rapx, rapx::verify)]
pub unsafe fn align_to<U>(&self) -> (&[T], &[U], &[T]) {
    if U::IS_ZST || T::IS_ZST {
        return (self, &[], &[]);
    }
    let ptr = self.as_ptr();
    let offset = unsafe { crate::ptr::align_offset(ptr, align_of::<U>()) };
    if offset > self.len() {
        (self, &[], &[])
    } else {
        let (left, rest) = self.split_at(offset);
        let (us_len, ts_len) = rest.align_to_offsets::<U>();
        unsafe {
            (
                left,
                from_raw_parts(rest.as_ptr() as *const U, us_len),
                from_raw_parts(rest.as_ptr().add(rest.len() - ts_len), ts_len),
            )
        }
    }
}
}

Verification Targets. On the non-ZST, non-empty path: align_offset (effect-modelled) and the two from_raw_parts(rest.as_ptr() as *const U, …) calls. The transmute obligation is expressed by the type-level precondition:

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

Path. The ZST (bb2) and offset > len (bb8) branches return early with no unsafe checkpoint. The unsafe path is … → bb5 → bb9 → bb12 → bb13 → bb17.

MIR. The statements on the unsafe path:

bb5:  _17 = ptr.align_offset(copy _15, mem::align_of::<U>());   // offset
bb9:  _35 = split_at(&(*_1), copy _17);                          // (left, rest)
bb10: _40 = rest.align_to_offsets::<U>();                        // (us_len, ts_len)
bb12: _45 = move _46 as *const U;                                // rest.as_ptr() as *const U
      _44 = raw::from_raw_parts(move _45, copy _38);             // ← checkpoint (1), middle [U]
bb16: _51 = ptr.add(copy _52, copy _54);                         // rest.as_ptr().add(len - ts_len)
bb17: _50 = raw::from_raw_parts(move _51, copy _39);             // ← checkpoint (2), tail [T]

Verification.

Entry. ValidTransmute(T, U) plus the &[T] slice invariant.

Property check. align_offset yields a valid aligned split point; split_at(offset) and the two from_raw_parts keep the three slices contiguous and in bounds — discharged by the range analysis. The essential risk — that the middle bytes form a valid [U] — is delegated to the ValidTransmute(T, U) axiom; RAPx verifies everything around the transmute.

10.1.3.9 align_to_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::requires(ValidTransmute(T, U)))]
#[cfg_attr(rapx, rapx::verify)]
pub unsafe fn align_to_mut<U>(&mut self) -> (&mut [T], &mut [U], &mut [T]) {
    if U::IS_ZST || T::IS_ZST {
        return (self, &mut [], &mut []);
    }
    let ptr = self.as_ptr();
    let offset = unsafe { crate::ptr::align_offset(ptr, align_of::<U>()) };
    if offset > self.len() {
        (self, &mut [], &mut [])
    } else {
        let (left, rest) = self.split_at_mut(offset);
        let (us_len, ts_len) = rest.align_to_offsets::<U>();
        let rest_len = rest.len();
        let mut_ptr = rest.as_mut_ptr();
        unsafe {
            (
                left,
                from_raw_parts_mut(mut_ptr as *mut U, us_len),
                from_raw_parts_mut(mut_ptr.add(rest_len - ts_len), ts_len),
            )
        }
    }
}
}

Verification Targets. Same transmute-based pattern as align_to: align_offset, and two from_raw_parts_mut(mut_ptr as *mut U, …) calls, with:

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

Path. The unsafe path is … → bb5 → bb9 → bb13 → bb16 (mirroring align_to with _mut slices).

MIR. The statements on the unsafe path:

bb5:  _17 = ptr.align_offset(copy _15, mem::align_of::<U>());
bb9:  _35 = split_at_mut(&mut (*_1), copy _17);
bb10: _40 = rest.align_to_offsets::<U>();
bb12: _44 = rest.as_mut_ptr();
bb13: _49 = move _50 as *mut U;
      _48 = raw::from_raw_parts_mut(move _49, copy _38);   // ← checkpoint (1), middle [U]
bb15: _54 = ptr.add(copy _44, copy _56);                   // mut_ptr.add(rest_len - ts_len)
bb16: _53 = raw::from_raw_parts_mut(move _54, copy _39);   // ← checkpoint (2), tail [T]

Verification. The three returned &mut slices are mutually disjoint (proved by the pointer arithmetic) and their Alias obligations are discharged by that disjointness plus the exclusive receiver. The transmute itself is covered by ValidTransmute(T, U).

10.1.3.10 get_disjoint_unchecked_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(InBound(self, indices)))]
#[cfg_attr(rapx, rapx::requires(NonOverlap(indices)))]
pub unsafe fn get_disjoint_unchecked_mut<I, const N: usize>(
    &mut self,
    indices: [I; N],
) -> [&mut I::Output; N]
where
    I: GetDisjointMutIndex + SliceIndex<Self>,
{
    let slice: *mut [T] = self;
    let mut arr: MaybeUninit<[&mut I::Output; N]> = MaybeUninit::uninit();
    let arr_ptr = arr.as_mut_ptr();
    unsafe {
        for i in 0..N {
            let idx = indices.get_unchecked(i).clone();
            arr_ptr.cast::<&mut I::Output>().add(i).write(&mut *slice.get_unchecked_mut(idx));
        }
        arr.assume_init()
    }
}
}

Verification Targets. Inside the for i in 0..N loop, three unsafe callsites per iteration:

(1) indices.get_unchecked(i) — the slice get_unchecked on [I; N], requiring InBound(indices, i);

(2) slice.get_unchecked_mut(idx) — SliceIndex::get_unchecked_mut:

#![allow(unused)]
fn main() {
#[rapx::requires(InBound(slice, self))]
}

(3) the raw-pointer dereference &mut * — a normal Ptr2Ref on the *mut I::Output returned by get_unchecked_mut (the value to be written into the MaybeUninit slot):

#![allow(unused)]
fn main() {
#[rapx::requires(Init(ptr, T, 1))]
#[rapx::requires(ValidPtr(ptr, T, 1))]
#[rapx::requires(Align(ptr, T))]
#[rapx::requires(Alias(ptr))]
}

Path. The loop body bb4 → … → bb14 → bb4 is an SCC, unrolled per iteration; the three callsites sit at bb7 (get_unchecked), bb12 (get_unchecked_mut), and bb13 (&mut * + write).

MIR. The loop-body statements on one iteration:

bb7:  _21 = get_unchecked(&_2 as &[I], copy _24);   // indices.get_unchecked(i)  ← checkpoint (1)
bb10: _27 = ptr.cast::<&mut I::Output>(copy _5);
      _26 = ptr.add(move _27, copy _29);           // arr_ptr.cast().add(i)
bb12: _32 = ptr.get_unchecked_mut::<I>(_33, _34);  // slice.get_unchecked_mut(idx)  ← checkpoint (2)
bb13: _31 = &mut (*_32);                           // &mut *  ← checkpoint (3)
      _25 = ptr.write(move _26, move _30);         // MaybeUninit::write
bb8:  _0 = MaybeUninit::assume_init(...);          // after all N iterations

Verification.

Entry. The preconditions InBound(self, indices) and NonOverlap(indices), plus the &mut [T] slice invariant.

Property check.

• (1) indices.get_unchecked(i): the loop index i is < N by construction → InBound discharged.
• (2) slice.get_unchecked_mut(idx): discharged by InBound(self, indices).
• (3) &mut *: Init/ValidPtr/Align inherited from the slice invariant; the Alias obligation is discharged by NonOverlap(indices) (no two returned references alias).

The MaybeUninit array is fully written before assume_init, so the initialization obligation is discharged by the loop covering all N slots.

10.1.3.11 first_chunk / first_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn first_chunk<const N: usize>(&self) -> Option<&[T; N]> {
    if self.len() < N {
        None
    } else {
        Some(unsafe { &*(self.as_ptr().cast_array()) })
    }
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn first_chunk_mut<const N: usize>(&mut self) -> Option<&mut [T; N]> {
    if self.len() < N {
        None
    } else {
        Some(unsafe { &mut *(self.as_mut_ptr().cast_array()) })
    }
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(self.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on a [T; N] pointer:

#![allow(unused)]
fn main() {
// Ptr2Ref
#[rapx::requires(Init(ptr, [T; N], 1))]
#[rapx::requires(ValidPtr(ptr, [T; N], 1))]
#[rapx::requires(Align(ptr, [T; N]))]
#[rapx::requires(Alias(ptr))]
}

Path. The else branch bb0 → bb1 → bb3 → bb4 → bb5 (the len < N branch bb2 returns None with no checkpoint).

MIR. The statements on the else path:

bb3: _8 = as_ptr(&(*_1));                       // self.as_ptr()
bb4: _7 = ptr.cast_array::<N>(move _8);         // *const T -> *const [T; N]
bb5: _6 = &(*_7);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _5 = &(*_6);   // safe reborrow
     _0 = Option::<&[T; N]>::Some(move _5);

Verification.

Entry. The &[T] / &mut [T] slice invariant.

VM execution. cast_array re-interprets the slice data pointer as *const [T; N]; the &* creates the reference.

Property check. The else branch carries the path condition len >= N, so the N-element array fits inside the slice — discharging Init/InBound. Align follows from the slice invariant ([T; N] has the same alignment as T). Alias is discharged by the shared/exclusive receiver. For N == 0 the empty array is returned, and dereferencing a dangling pointer to a zero-sized array is legal.

10.1.3.12 split_first_chunk / split_first_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn split_first_chunk<const N: usize>(&self) -> Option<(&[T; N], &[T])> {
    let Some((first, tail)) = self.split_at_checked(N) else { return None };
    Some((unsafe { &*(first.as_ptr().cast_array()) }, tail))
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn split_first_chunk_mut<const N: usize>(
    &mut self,
) -> Option<(&mut [T; N], &mut [T])> {
    let Some((first, tail)) = self.split_at_mut_checked(N) else { return None };
    Some((unsafe { &mut *(first.as_mut_ptr().cast_array()) }, tail))
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(first.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on [T; N], same contract as first_chunk.

Path. The Some branch bb0 → bb1 → bb2 → bb4 → bb5 (the None branch bb3 returns with no checkpoint).

MIR. The statements on the Some path:

bb0: _5 = split_at_checked(&(*_1), const N);
bb1: switchInt(discriminant(_5)) -> [1: bb2, otherwise: bb3];
bb2: _3 = copy (((_5 as Some).0).0);   // first
     _4 = copy (((_5 as Some).0).1);   // tail
     _12 = as_ptr(&(*_3));             // first.as_ptr()
bb4: _11 = ptr.cast_array::<N>(move _12);
bb5: _10 = &(*_11);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _9 = &(*_10);    // safe reborrow
     _8 = (move _9, move &(*_4));

Verification.

Entry. The slice invariant.

Property check. split_at_checked(N) returns Some only when N <= len, so first has exactly N elements and the deref is in bounds — Init/Align/Alias discharged as in first_chunk. The tail slice is returned as-is.

10.1.3.13 split_last_chunk / split_last_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn split_last_chunk<const N: usize>(&self) -> Option<(&[T], &[T; N])> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (init, last) = self.split_at(index);
    Some((init, unsafe { &*(last.as_ptr().cast_array()) }))
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn split_last_chunk_mut<const N: usize>(
    &mut self,
) -> Option<(&mut [T], &mut [T; N])> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (init, last) = self.split_at_mut(index);
    Some((init, unsafe { &mut *(last.as_mut_ptr().cast_array()) }))
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(last.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on [T; N].

Path. The Some branch bb0 → bb1 → bb2 → bb3 → bb5 → bb6 → bb7 (the None branch bb4 returns with no checkpoint).

MIR. The statements on the Some path:

bb0: _5 = len(&(*_1));
bb1: _4 = checked_sub(move _5, const N);
bb2: switchInt(discriminant(_4)) -> [1: bb3, otherwise: bb4];
bb3: _3 = copy ((_4 as Some).0);       // index = len - N
     _10 = split_at(&(*_1), copy _3);  // (init, last)
bb5: _8 = copy (_10.0);  _9 = copy (_10.1);
     _18 = as_ptr(&(*_9));             // last.as_ptr()
bb6: _17 = ptr.cast_array::<N>(move _18);
bb7: _16 = &(*_17);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _15 = &(*_16);   // safe reborrow
     _0 = Some((move &(*_8), move _15));

Verification.

Entry. The slice invariant.

Property check. checked_sub(N) returning Some(index) establishes len >= N; split_at(index) (with index = len - N) then yields a trailing slice of exactly N elements, so the deref is in bounds — Init/Align/Alias discharged as in first_chunk.

10.1.3.14 last_chunk / last_chunk_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn last_chunk<const N: usize>(&self) -> Option<&[T; N]> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (_, last) = self.split_at(index);
    Some(unsafe { &*(last.as_ptr().cast_array()) })
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn last_chunk_mut<const N: usize>(&mut self) -> Option<&mut [T; N]> {
    let Some(index) = self.len().checked_sub(N) else { return None };
    let (_, last) = self.split_at_mut(index);
    Some(unsafe { &mut *(last.as_mut_ptr().cast_array()) })
}
}

Verification Targets. The single callsite is the raw-pointer dereference &*(last.as_ptr().cast_array()) (and &mut * for _mut) — a Ptr2Ref on [T; N].

Path. The Some branch bb0 → bb1 → bb2 → bb3 → bb5 → bb6 → bb7.

MIR. The statements on the Some path:

bb3: _3 = copy ((_4 as Some).0);       // index = len - N
     _9 = split_at(&(*_1), copy _3);
bb5: _8 = copy (_9.1);                  // last
     _15 = as_ptr(&(*_8));
bb6: _14 = ptr.cast_array::<N>(move _15);
bb7: _13 = &(*_14);   // &* — raw-pointer deref (Ptr2Ref checkpoint)
     _12 = &(*_13);   // safe reborrow

Verification. Same as split_last_chunk, but only the trailing chunk is returned. checked_sub(N) establishes len >= N, so the N-element deref is in bounds.

10.1.3.15 reverse

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn reverse(&mut self) {
    let half_len = self.len() / 2;
    let Range { start, end } = self.as_mut_ptr_range();

    let (front_half, back_half) =
        unsafe {
            (
                slice::from_raw_parts_mut(start, half_len),
                slice::from_raw_parts_mut(end.sub(half_len), half_len),
            )
        };

    revswap(front_half, back_half, half_len);

    #[inline]
    const fn revswap<T>(a: &mut [T], b: &mut [T], n: usize) {
        let (a, _) = a.split_at_mut(n);
        let (b, _) = b.split_at_mut(n);
        let mut i = 0;
        #[safety::loop_invariant(i <= n)]
        while i < n {
            mem::swap(&mut a[i], &mut b[n - 1 - i]);
            i += 1;
        }
    }
}
}

Verification Targets. Two callsites:

(1) the two from_raw_parts_mut(start, half_len) / from_raw_parts_mut(end.sub(half_len), half_len) calls (the _mut from_raw_parts contract with Alias);

(2) inside revswap, the mem::swap(&mut a[i], &mut b[n - 1 - i]) calls (the ptr::swap contract).

Path. bb0 → bb1 → bb2 → bb3 → bb4 → bb5 → bb6 (the two from_raw_parts_mut at bb3/bb5, then the revswap call at bb6); inside revswap the mem::swap loop is an SCC unrolled per iteration.

MIR. The statements on that path:

bb2: _2 = Div(len(&(*_1)), const 2);        // half_len
     _8 = as_mut_ptr_range(&mut (*_1));     // (start, end)
bb3: _6 = copy (_8.0);  _7 = copy (_8.1);   // start, end
     _13 = from_raw_parts_mut(copy _6, copy _2);   // front_half  ← checkpoint (1)
bb4: _17 = ptr.sub(copy _7, copy _2);       // end.sub(half_len)
bb5: _16 = from_raw_parts_mut(move _17, copy _2);  // back_half   ← checkpoint (1)
bb6: _21 = revswap(&mut (*_10), &mut (*_11), copy _2);   // revswap → mem::swap loop

Verification.

Entry. The &mut [T] slice invariant (including exclusive access).

Property check. With half_len = len / 2, the front half [0, half_len) and back half [len - half_len, len) are disjoint and in bounds (len - half_len >= half_len), discharging ValidPtr/InBound/Alias for both from_raw_parts_mut calls. In revswap, the loop invariant i <= n proves a[i] and b[n - 1 - i] stay in bounds, and the disjoint halves guarantee mem::swap never aliases.

10.1.3.16 as_chunks / as_chunks_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn as_chunks<const N: usize>(&self) -> (&[[T; N]], &[T]) {
    assert!(N != 0, "chunk size must be non-zero");
    let len_rounded_down = self.len() / N * N;
    let (multiple_of_n, remainder) = unsafe { self.split_at_unchecked(len_rounded_down) };
    let array_slice = unsafe { multiple_of_n.as_chunks_unchecked() };
    (array_slice, remainder)
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn as_chunks_mut<const N: usize>(&mut self) -> (&mut [[T; N]], &mut [T]) {
    assert!(N != 0, "chunk size must be non-zero");
    let len_rounded_down = self.len() / N * N;
    let (multiple_of_n, remainder) = unsafe { self.split_at_mut_unchecked(len_rounded_down) };
    let array_slice = unsafe { multiple_of_n.as_chunks_unchecked_mut() };
    (array_slice, remainder)
}
}

Verification Targets. Two chained callsites: split_at_unchecked(len_rounded_down) (contract ValidNum(mid, [0, self.len()])) and as_chunks_unchecked() (contract ValidNum(N, "[1,)") + ValidNum(len % N == 0)).

Path. bb0 → bb3 → bb4 → bb5 → bb6 → bb7 (the assert! branch bb1/bb2 panics); split_at_unchecked at bb6, as_chunks_unchecked at bb7.

MIR. The statements on that path:

bb3: _12 = len(&(*_1));
bb4: _11 = Div(move _12, const N);        // len / N
bb5: _10 = MulWithOverflow(copy _11, const N);   // * N  (= len_rounded_down)
bb6: _18 = split_at_unchecked(&(*_1), copy _10); // ← checkpoint (1)
bb7: _21 = as_chunks_unchecked(&(*_16));         // ← checkpoint (2)

Verification.

Entry. The slice invariant.

Property check. assert!(N != 0) provides the path condition N != 0. len_rounded_down = len / N * N is <= len (discharging split_at_unchecked's mid <= len) and a multiple of N (discharging as_chunks_unchecked's len % N == 0). Both internal unsafe calls are thus covered by facts established in the body.

10.1.3.17 as_rchunks

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn as_rchunks<const N: usize>(&self) -> (&[T], &[[T; N]]) {
    assert!(N != 0, "chunk size must be non-zero");
    let len = self.len() / N;
    let (remainder, multiple_of_n) = self.split_at(self.len() - len * N);
    let array_slice = unsafe { multiple_of_n.as_chunks_unchecked() };
    (remainder, array_slice)
}
}

Verification Targets. A single callsite as_chunks_unchecked() (contract ValidNum(N, "[1,)") + ValidNum(len % N == 0)), reached after a safe split_at.

Path. bb0 → bb3 → bb4 → bb5 → bb8 → bb9 (the assert! branch bb1/bb2 panics); split_at at bb8, as_chunks_unchecked at bb9.

MIR. The statements on that path:

bb3: _11 = len(&(*_1));
bb5: _10 = Div(move _11, const N);                 // len / N
bb8: _18 = SubWithOverflow(copy _11, copy _10 * N); // self.len() - len * N
     _16 = split_at(&(*_1), move _18);
bb9: _25 = as_chunks_unchecked(&(*_15));           // ← checkpoint

Verification.

Entry. The &[T] slice invariant.

Property check. assert!(N != 0) provides N != 0. self.len() - len * N is the remainder len % N, so the right slice multiple_of_n has a length that is a multiple of N, discharging as_chunks_unchecked's len % N == 0. The left remainder has length < N by construction.

10.1.3.18 split_at_checked / split_at_mut_checked

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn split_at_checked(&self, mid: usize) -> Option<(&[T], &[T])> {
    if mid <= self.len() {
        Some(unsafe { self.split_at_unchecked(mid) })
    } else {
        None
    }
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn split_at_mut_checked(&mut self, mid: usize) -> Option<(&mut [T], &mut [T])> {
    if mid <= self.len() {
        Some(unsafe { self.split_at_mut_unchecked(mid) })
    } else {
        None
    }
}
}

Verification Targets. A single callsite split_at_unchecked(mid) / split_at_mut_unchecked(mid) (contract ValidNum(mid, [0, self.len()])), reached only on the mid <= len branch.

Path. bb0 → bb1 → bb2 → bb3 (the Some branch); the else branch bb4 returns None.

MIR. The statements on the Some path:

bb0: _5 = len(&(*_1));
bb1: _3 = Le(copy _2, move _5);
     switchInt(move _3) -> [0: bb4, otherwise: bb2];
bb2: _7 = split_at_unchecked(&(*_1), copy _2);   // ← checkpoint
bb3: _0 = Some(move _7);

Verification.

Entry. The slice invariant.

Property check. The branch condition mid <= self.len() (plus mid: usize >= 0) is exactly the 0 <= mid <= len precondition, so the Some branch is discharged directly; the else branch returns None.

10.1.3.19 binary_search_by

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn binary_search_by<'a, F>(&'a self, mut f: F) -> Result<usize, usize>
where
    F: FnMut(&'a T) -> Ordering,
{
    let mut size = self.len();
    if size == 0 {
        return Err(0);
    }
    let mut base = 0usize;

    while size > 1 {
        let half = size / 2;
        let mid = base + half;
        let cmp = f(unsafe { self.get_unchecked(mid) });
        base = hint::select_unpredictable(cmp == Greater, base, mid);
        size -= half;
    }

    let cmp = f(unsafe { self.get_unchecked(base) });
    if cmp == Equal {
        unsafe { hint::assert_unchecked(base < self.len()) };
        Ok(base)
    } else {
        let result = base + (cmp == Less) as usize;
        unsafe { hint::assert_unchecked(result <= self.len()) };
        Err(result)
    }
}
}

Verification Targets. self.get_unchecked(mid) (inside the loop) and self.get_unchecked(base) (epilogue), each carrying #[rapx::requires(InBound(slice, self))]; plus two hint::assert_unchecked hints.

Path. The loop body bb4 → … → bb12 → bb4 is an SCC, unrolled per iteration; get_unchecked(mid) at bb7, the epilogue get_unchecked(base) at bb13, and the two assert_unchecked at bb18/bb23.

MIR. The loop-body and epilogue statements:

bb7:  _25 = get_unchecked(&(*_1), copy _17);   // self.get_unchecked(mid)  ← checkpoint
bb8:  _21 = call_mut(_22, move _23);           // f(&self[mid])
bb13: _44 = get_unchecked(&(*_1), copy _46);   // self.get_unchecked(base)  ← checkpoint
bb18: _51 = assert_unchecked(move _52);        // base < len
bb23: _65 = assert_unchecked(move _66);        // result <= len

Verification.

Entry. The &[T] slice invariant.

Property check. The loop invariant is base + size == len (initially base = 0, size = len). Each iteration computes mid = base + half with half = size / 2, so mid < base + size == len, discharging get_unchecked(mid)'s InBound. After size -= half the invariant is restored, so the unrolled loop is inductive. On exit size <= 1, hence base < len, discharging the final get_unchecked(base). The two assert_unchecked bounds facts are verified independently.

10.1.3.20 partition_dedup_by

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn partition_dedup_by<F>(&mut self, mut same_bucket: F) -> (&mut [T], &mut [T])
where
    F: FnMut(&mut T, &mut T) -> bool,
{
    let len = self.len();
    if len <= 1 {
        return (self, &mut []);
    }

    let ptr = self.as_mut_ptr();
    let mut next_read: usize = 1;
    let mut next_write: usize = 1;

    unsafe {
        while next_read < len {
            let ptr_read = ptr.add(next_read);
            let prev_ptr_write = ptr.add(next_write - 1);
            if !same_bucket(&mut *ptr_read, &mut *prev_ptr_write) {
                if next_read != next_write {
                    let ptr_write = prev_ptr_write.add(1);
                    mem::swap(&mut *ptr_read, &mut *ptr_write);
                }
                next_write += 1;
            }
            next_read += 1;
        }
    }

    self.split_at_mut(next_write)
}
}

Verification Targets. Inside the while next_read < len loop, the raw-pointer dereferences &mut *ptr_read, &mut *prev_ptr_write, &mut *ptr_write (each requiring Init + ValidPtr + Align + Alias), and mem::swap.

Path. The loop body bb5 → … → bb20 → bb5 is an SCC, unrolled per iteration; the derefs are at bb9 (same_bucket's &mut *) and bb14 (mem::swap's &mut *).

MIR. The loop-body statements on one iteration:

bb5:  _20 = Lt(copy _16, copy _3);            // next_read < len
bb6:  _23 = ptr.add(copy _14, copy _16);      // ptr_read = ptr.add(next_read)
bb8:  _26 = ptr.add(copy _14, copy _28);      // prev_ptr_write = ptr.add(next_write - 1)
bb9:  _32 = call_mut(&mut _2, &mut *(_23), &mut *(_26));   // same_bucket(&mut *ptr_read, &mut *prev_ptr_write)
bb14: _45 = mem::swap(&mut *(_23), &mut *(_43));           // mem::swap(&mut *ptr_read, &mut *ptr_write)

Verification.

Entry. The &mut [T] slice invariant.

Property check. The loop invariant is 1 <= next_write <= next_read < len. This keeps next_read and next_write - 1 in bounds and guarantees next_read > next_write - 1, so ptr_read and prev_ptr_write never point to the same element. When next_read != next_write, ptr_read and ptr_write are distinct, so mem::swap does not alias. RAPx proves these index facts via loop-invariant range analysis.

10.1.3.21 rotate_left / rotate_right

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn rotate_left(&mut self, mid: usize) {
    assert!(mid <= self.len());
    let k = self.len() - mid;
    let p = self.as_mut_ptr();
    unsafe {
        rotate::ptr_rotate(mid, p.add(mid), k);
    }
}

#[cfg_attr(rapx, rapx::verify)]
pub const fn rotate_right(&mut self, k: usize) {
    assert!(k <= self.len());
    let mid = self.len() - k;
    let p = self.as_mut_ptr();
    unsafe {
        rotate::ptr_rotate(mid, p.add(mid), k);
    }
}
}

Verification Targets. Two unsafe callsites:

(1) ptr.add(mid) — the element-strided add:

#![allow(unused)]
fn main() {
// core::ptr::mut_ptr::add
#[rapx::requires(InBound(self, T, count))]
}

(2) rotate::ptr_rotate(mid, p.add(mid), k) — the rotate helper:

#![allow(unused)]
fn main() {
// core::slice::rotate::ptr_rotate
#[rapx::requires(NonNull(mid))]
#[rapx::requires(Align(mid, T))]
#[rapx::requires(ValidPtr(mid, T, right))]
}

Path. bb0 → bb1 → bb2 → bb4 → bb5 → bb6 → bb7 (the assert! branch bb3 panics); ptr.add at bb6, ptr_rotate at bb7.

MIR. The statements on that path:

bb2: _10 = len(&(*_1));
bb4: _9 = SubWithOverflow(copy _10, copy _2);   // k = len - mid
bb5: _14 = as_mut_ptr(&mut (*_1));              // p
bb6: _18 = ptr.add(copy _14, copy _2);          // p.add(mid)  ← checkpoint (1)
bb7: _16 = ptr_rotate(move _17, move _18, move _21);   // ← checkpoint (2)

Verification.

Entry. The &mut [T] slice invariant.

Property check. assert!(mid <= self.len()) gives 0 <= mid <= len (resp. 0 <= k <= len), so k = len - mid >= 0. The two callsites split the range into halves:

• (1) ptr.add(mid) requires the left half [p, p.add(mid)) to be in bounds — discharged by mid <= len.
• (2) ptr_rotate's ValidPtr(mid, T, right) requires the right half [p.add(mid), p.add(mid) + right) = [p.add(mid), p.add(len)) to be valid for right = k = len - mid elements — discharged by the slice invariant and k = len - mid.

Together they span the whole [p, p + len) range that ptr_rotate operates over.

10.1.3.22 copy_from_slice

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn copy_from_slice(&mut self, src: &[T])
where
    T: Copy,
{
    // SAFETY: `T` implements `Copy`.
    unsafe { copy_from_slice_impl(self, src) }
}
}

Verification Targets. A single callsite at the internal helper copy_from_slice_impl, which itself calls copy_nonoverlapping:

#![allow(unused)]
fn main() {
// core::ptr::copy_nonoverlapping
#[rapx::requires(Align(src, T))]
#[rapx::requires(Align(dst, T))]
#[rapx::requires(ValidPtr(src, T, count))]
#[rapx::requires(ValidPtr(dst, T, count))]
#[rapx::requires(NonOverlap(dst, src, T, count))]
#[rapx::requires(ValidNum(size_of(T) * count <= isize::MAX))]
}

Path. bb0 → bb1 → bb2 → bb6 → bb7 → bb8 → bb9 (the length-mismatch branch bb3/bb4/bb5 panics); copy_nonoverlapping at bb9.

MIR. The statements on that path:

bb6: _16 = as_ptr(&(*_2));                  // src.as_ptr()
bb7: _18 = as_mut_ptr(&mut (*_1));          // self.as_mut_ptr()
bb8: _20 = len(&(*_1));
bb9: _15 = ptr.copy_nonoverlapping(move _16, move _18, move _20);   // ← checkpoint

Verification.

Entry. The &mut [T] and &[T] slice invariants, plus the T: Copy bound.

Property check. copy_from_slice_impl first checks dest.len() != src.len() and panics on mismatch, then calls copy_nonoverlapping. The equal-length assertion plus the mutual exclusivity of &mut self and &src discharge ValidPtr / NonOverlap / ValidNum. The T: Copy bound justifies the bitwise copy.

10.1.3.23 copy_within

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn copy_within<R: RangeBounds<usize>>(&mut self, src: R, dest: usize)
where
    T: Copy,
{
    let Range { start: src_start, end: src_end } = slice::range(src, ..self.len());
    let count = src_end - src_start;
    assert!(dest <= self.len() - count, "dest is out of bounds");
    unsafe {
        let ptr = self.as_mut_ptr();
        let src_ptr = ptr.add(src_start);
        let dest_ptr = ptr.add(dest);
        ptr::copy(src_ptr, dest_ptr, count);
    }
}
}

Verification Targets. A single callsite ptr::copy(src_ptr, dest_ptr, count):

#![allow(unused)]
fn main() {
// core::ptr::copy
#[rapx::requires(ValidPtr(src, T, count))]
#[rapx::requires(Align(src, T))]
#[rapx::requires(ValidPtr(dst, T, count))]
#[rapx::requires(Align(dst, T))]
}

Path. bb0 → bb1 → bb2 → bb3 → bb4 → bb5 → bb6 → bb9 → bb10 → bb11 (the dest > len - count branch bb7/bb8 panics); ptr::copy at bb11.

MIR. The statements on that path:

bb2: _11 = SubWithOverflow(copy _5, copy _4);   // count = src_end - src_start
bb6: _29 = as_mut_ptr(&mut (*_1));              // ptr
bb9: _31 = ptr.add(copy _29, copy _4);          // src_ptr = ptr.add(src_start)
bb10: _34 = ptr.add(copy _29, copy _3);         // dest_ptr = ptr.add(dest)
bb11: _38 = move _31 as *const T;
      _37 = ptr::copy(move _38, move _34, move _41);   // ← checkpoint

Verification.

Entry. The &mut [T] slice invariant.

Property check. slice::range(src, ..self.len()) normalizes the source range and enforces src_start <= src_end <= len; assert!(dest <= len - count) enforces dest + count <= len. Both ranges therefore lie within [0, len). ptr::copy permits overlap (memmove), so no NonOverlap obligation arises — only the in-bounds facts, which are discharged.

10.1.3.24 swap_with_slice

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub const fn swap_with_slice(&mut self, other: &mut [T]) {
    assert!(self.len() == other.len(), "destination and source slices have different lengths");
    unsafe {
        ptr::swap_nonoverlapping(self.as_mut_ptr(), other.as_mut_ptr(), self.len());
    }
}
}

Verification Targets. A single callsite ptr::swap_nonoverlapping(self.as_mut_ptr(), other.as_mut_ptr(), self.len()):

#![allow(unused)]
fn main() {
// core::ptr::swap_nonoverlapping
#[rapx::requires(ValidPtr(x, T, count))]
#[rapx::requires(Align(x, T))]
#[rapx::requires(NonOverlap(x, y, T, count))]
}

Path. bb0 → bb1 → bb2 → bb3 → bb6 → bb7 → bb8 (the length-mismatch branch bb4/bb5 panics); swap_nonoverlapping at bb8.

MIR. The statements on that path:

bb3: _16 = as_mut_ptr(&mut (*_1));          // self.as_mut_ptr()
bb6: _18 = as_mut_ptr(&mut (*_2));          // other.as_mut_ptr()
bb7: _20 = len(&(*_1));
bb8: _15 = swap_nonoverlapping(move _16, move _18, move _20);   // ← checkpoint

Verification.

Entry. The two &mut [T] slice invariants.

Property check. assert!(self.len() == other.len()) establishes equal lengths. The two &mut [T] references are mutually exclusive by Rust's borrow rules, discharging swap_nonoverlapping's NonOverlap obligation.

10.1.3.25 as_simd / as_simd_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn as_simd<const LANES: usize>(&self) -> (&[T], &[Simd<T, LANES>], &[T])
where
    Simd<T, LANES>: AsRef<[T; LANES]>,
    T: simd::SimdElement,
    simd::LaneCount<LANES>: simd::SupportedLaneCount,
{
    assert_eq!(size_of::<Simd<T, LANES>>(), size_of::<[T; LANES]>());
    unsafe { self.align_to() }
}

#[cfg_attr(rapx, rapx::verify)]
pub fn as_simd_mut<const LANES: usize>(&mut self) -> (&mut [T], &mut [Simd<T, LANES>], &mut [T])
where
    Simd<T, LANES>: AsMut<[T; LANES]>,
    T: simd::SimdElement,
    simd::LaneCount<LANES>: simd::SupportedLaneCount,
{
    assert_eq!(size_of::<Simd<T, LANES>>(), size_of::<[T; LANES]>());
    unsafe { self.align_to_mut() }
}
}

Verification Targets. A single callsite align_to() / align_to_mut() (whose transmute obligation is ValidTransmute(T, Simd<T, LANES>)).

Path. bb0 → bb1 → bb3 (the size-mismatch branch bb2 panics); align_to at bb1.

MIR. The statements on that path:

bb0: _11 = copy (*_8);  _12 = copy (*_9);       // size_of::<Simd<T, LANES>>(), size_of::<[T; LANES]>()
     _10 = Eq(move _11, move _12);
     switchInt(move _10) -> [0: bb2, otherwise: bb1];
bb1: _0 = align_to::<Simd<T, LANES>>(&(*_1));   // ← checkpoint (transmute)

Verification.

Entry. The slice invariant, plus the assert_eq!-established fact size_of::<Simd<T, LANES>>() == size_of::<[T; LANES]>().

Property check. The size assertion proves the SIMD vector type is layout-identical to [T; LANES], making the align_to transmute sound. All alignment, contiguity, and bounds properties are inherited from the align_to / align_to_mut verification.

10.1.3.26 get_disjoint_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
pub fn get_disjoint_mut<I, const N: usize>(
    &mut self,
    indices: [I; N],
) -> Result<[&mut I::Output; N], GetDisjointMutError>
where
    I: GetDisjointMutIndex + SliceIndex<Self>,
{
    get_disjoint_check_valid(&indices, self.len())?;
    // SAFETY: The `get_disjoint_check_valid()` call checked that all indices
    // are disjunct and in bounds.
    unsafe { Ok(self.get_disjoint_unchecked_mut(indices)) }
}
}

Verification Targets. A single callsite get_disjoint_unchecked_mut(indices), whose two preconditions are InBound(self, indices) and NonOverlap(indices).

Path. bb0 → bb1 → bb2 → bb3 → bb5 → bb8 (the Err branch bb6/bb7 returns early); get_disjoint_unchecked_mut at bb5.

MIR. The statements on the Ok path:

bb1: _5 = get_disjoint_check_valid(&(*_2), len(&(*_1)));   // returns Result
bb3: switchInt(discriminant(_4)) -> [1: bb6, 0: bb5];
bb5: _15 = get_disjoint_unchecked_mut(&mut (*_1), move _17);   // ← checkpoint
bb8: _0 = Ok(move _15);

Verification.

Entry. The &mut [T] slice invariant.

Property check. get_disjoint_check_valid(...)? returning Ok establishes that all indices are in bounds and pairwise non-overlapping, discharging the InBound and NonOverlap preconditions of get_disjoint_unchecked_mut. RAPx connects the Ok result of the checker to the preconditions at the call site.

10.1.3.27 get_disjoint_check_valid

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
fn get_disjoint_check_valid<I: GetDisjointMutIndex, const N: usize>(
    indices: &[I; N],
    len: usize,
) -> Result<(), GetDisjointMutError> {
    for (i, idx) in indices.iter().enumerate() {
        if !idx.is_in_bounds(len) {
            return Err(GetDisjointMutError::IndexOutOfBounds);
        }
        for idx2 in &indices[..i] {
            if idx.is_overlapping(idx2) {
                return Err(GetDisjointMutError::OverlappingIndices);
            }
        }
    }
    Ok(())
}
}

Verification Targets. No unsafe callsites — this is a pure O(n²) validation loop over the indices (is_in_bounds and is_overlapping). It is annotated with #[rapx::verify] so RAPx treats it as the trusted precondition generator for get_disjoint_mut.

MIR. The nested-loop shape (outer next at bb4, is_in_bounds at bb7, inner next at bb14, is_overlapping at bb16):

bb4:  _12 = <Enumerate<Iter<I>>>::next(...);        // (i, idx)
bb7:  _20 = <I as GetDisjointMutIndex>::is_in_bounds(&idx, len);   // idx.is_in_bounds(len)
bb14: _33 = <Iter<I>>::next(...);                   // idx2 in indices[..i]
bb16: _39 = <I as GetDisjointMutIndex>::is_overlapping(&idx, &idx2);

Verification. The nested loops prove that an Ok return implies every index passed is_in_bounds and no pair is_overlapping — the facts that get_disjoint_mut then relies on.

10.1.3.28 as_flattened / as_flattened_mut

#![allow(unused)]
fn main() {
#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidTransmute([T; N], T)))]
pub const fn as_flattened(&self) -> &[T] {
    let len = if T::IS_ZST {
        self.len().checked_mul(N).expect("slice len overflow")
    } else {
        unsafe { self.len().unchecked_mul(N) }
    };
    unsafe { from_raw_parts(self.as_ptr().cast(), len) }
}

#[cfg_attr(rapx, rapx::verify)]
#[cfg_attr(rapx, rapx::requires(ValidTransmute([T; N], T)))]
pub const fn as_flattened_mut(&mut self) -> &mut [T] {
    let len = if T::IS_ZST {
        self.len().checked_mul(N).expect("slice len overflow")
    } else {
        unsafe { self.len().unchecked_mul(N) }
    };
    unsafe { from_raw_parts_mut(self.as_mut_ptr().cast(), len) }
}
}

Verification Targets. A single callsite from_raw_parts(self.as_ptr().cast(), len) (and from_raw_parts_mut for _mut), with the layout-identity axiom:

#![allow(unused)]
fn main() {
#[rapx::requires(ValidTransmute([T; N], T))]
}

Path. bb0 → … → bb8 → bb9 → bb10 (the ZST branch bb1/bb2/bb3/bb4 uses checked_mul; the non-ZST branch bb5/bb6/bb7 uses unchecked_mul); from_raw_parts at bb10.

MIR. The statements on the non-ZST path:

bb5: _9 = len(&(*_1));
bb6: _2 = unchecked_mul(move _9, const N);     // len = self.len() * N
bb8: _13 = as_ptr(&(*_1));
bb9: _12 = ptr.cast::<T>(move _13);            // self.as_ptr().cast()
bb10: _11 = raw::from_raw_parts(move _12, copy _2);   // ← checkpoint

Verification.

Entry. The slice invariant plus ValidTransmute([T; N], T).

Property check. The new length is len * N: for ZSTs checked_mul guards overflow; for non-ZSTs the multiplication cannot overflow because the slice is already in the address space. from_raw_parts requires len * N elements of T (i.e. len * size_of::<[T; N]>() bytes) in bounds, which follows from the slice's own validity. The cast re-interpretation is covered by the ValidTransmute([T; N], T) axiom.

10.1.4 Code Reference

• Source: safer-rust/rapx-verify-rust-std
• Challenge: #281 / 0017-slice