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
Check the unsafe operations in the 37 challenge-listed functions in library/core/src/slice/mod.rs by:
- Writing
#[rapx::requires(...)]safety preconditions on unsafe callees - Adding
#[rapx::verify]annotations to trigger verification - Running RAPx in
targetedmode against the annotated functions
RAPx represents slice length and generic type T symbolically, without monomorphization. Its path analysis still enumerates finitely many paths and loop repetitions, subject to a path limit. A SOUND result in this chapter means that the obligations on those enumerated paths were discharged; it does not establish an inductive proof for every iteration of an arbitrary-length loop. The loop invariants mentioned below explain the source-level safety argument and are not assumptions or induction results supplied by RAPx.
10.1.2 Tool Integration
Like Kani (#[cfg_attr(kani, ...)]), RAPx annotations use cfg_attr so they only activate when the tool runs — register_tool is injected via RUSTFLAGS, never hard-coded in source:
#![allow(unused)] fn main() { // 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 from library/core (not the workspace root — core must be the primary package, not a dependency, for its annotations to be visible):
cd library/core
RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)" \
cargo rapx verify --module slice --mode targeted
--cfg=rapxactivates thecfg_attr(rapx, ...)expansion.-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)registersrapxas a tool namespace.
A GitHub Actions workflow (.github/workflows/rapx.yml) runs the command on pushes and PRs. It currently installs the published RAPx crate version 0.7.56 through RAPX_VERSION, rather than pinning a Git commit or following RAPx main. Its pass condition only rejects lines containing result: UNSOUND; UNKNOWN results are allowed. The command is piped through tee without pipefail, so the workflow also does not reliably propagate a nonzero RAPx exit status. The individual SOUND traces below describe verifier output, not a guarantee enforced by this CI job.
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 — established by init_parameters at entry and re-proved at return:
"[T]": {
"invariants": [
{ "tag": "NonNull", "args": ["$self"] },
{ "tag": "Align", "args": ["$self", "$elem"] },
{ "tag": "ValidNum", "args": ["size_of($elem) * $self.len() <= isize::MAX"] },
{ "tag": "Allocated", "args": ["$self", "$elem", "$self.len()"] },
{ "tag": "Init", "args": ["$self", "$elem", "$self.len()"] }
]
}
Symbolic resolution. $self instantiates to the slice reference and $elem to the element type T. For a generic T, its size and alignment are unknown, so RAPx represents them symbolically as sizeof_T and align_T (sizeof_T ≥ 0 — T may be a ZST — and align_T ≥ 1, linked by the layout constraint sizeof_T % align_T == 0); the slice length is likewise symbolic, written len. The atoms therefore resolve to:
NonNull($self)→self.term ≠ 0Align($self, $elem)→self.term % align_T == 0ValidNum(size_of($elem) * $self.len() <= isize::MAX)→len * sizeof_T ≤ isize::MAXAllocated($self, $elem, $self.len())→Allocated(self, T, len)Init($self, $elem, $self.len())→Init(self, T, len)
The following traces cite these symbolic forms directly. 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 also hold unconditionally: an empty slice (len == 0) has zero elements, so both are vacuous.
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.
Besides these, the &[T] receiver's slice type invariant 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 call's unwind edge to bb2 (resume, the panic path) is also part of the CFG, so RAPx's path graph enumerates it — but bb2 holds no unsafe checkpoint, so it adds no obligation. The &[T] invariant is re-proved only at the return block bb1 — a type invariant is a normal-return postcondition, so the panic-unwind path carries none.
MIR (compiled with nightly-2026-02-05; 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. Each local is a symbolic VmValue (term = address/value, prov = (alloc, offset), plus flags non_null/aligned/init); alloc(x) is the Allocation a local points into, holding base/size/align.
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)/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 (≥ 0, so T may be a ZST) rather than a monomorphized byte count, so the data allocation's byte size is len*sizeof_T; the element alignment is likewise a shared symbolic align_T (≥ 1), tied to the size by the layout constraint sizeof_T % align_T == 0. The slice length is materialized on the allocation as slice_len (mirroring the fat pointer's metadata word), with size = slice_len * sizeof_T, so len() reads it directly. The path, step by step:
entry _1 = self (&[T]), _2 = index (I)
init_parameters:
data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
_1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
slice type invariant (JSON `[T]` entry):
NonNull(_1) : _1.term ≠ 0
Align(_1, T) : _1.term % align_T == 0
ValidNum(..) : len * sizeof_T ≤ isize::MAX
Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
Init(_1, T, len) : data_alloc.initialized = true (whole slice data initialized)
entry fact: len ≥ 0 (usize non-negativity)
_2.term = param_2 (fresh symbolic)
caller contracts (asserted as facts):
InBound(_1, _2) → _2.term < len
_5 = move _2
VM _5.term = _2.term
_6 = &raw const (*_1)
VM _6.term = _1.term, _6.prov = _1.prov, _6.flags = { non_null, in_bounds }, _6.align_n = data_alloc.align = align_T
_4 = get_unchecked(move _5, move _6) [checkpoint (1)]
check InBound(_6, _5) ← SMT: assert entry `_2.term < len`; assert ¬(`_5.term < len`); `_5.term` ≡ `_2.term` ⇒ UNSAT Proved
VM _4.term = _6.term + _5.term*sizeof_T, _4.prov = (data_alloc, _6.offset + _5.term*sizeof_T), _4.flags = { non_null, in_bounds }
_3 = &(*_4) [checkpoint (2)]
check Init(_4, T, 1) ← data_alloc.initialized = true Proved
check NonNull(_4) ← non_null ∈ _4.flags Proved
check Allocated(_4, T, 1) ← SMT: assert ¬(`(_5.term+1)*sizeof_T ≤ len*sizeof_T`)
— case split on `sizeof_T`: ZST (`= 0`, both sides 0) and
non-ZST (`≥ 1`, unsat by `_5.term < len`) ⇒ UNSAT Proved
check InBound(_4, T, 1) ← in_bounds ∈ _4.flags, count == 1 (single-element fast-path) Proved
check Align(_4, T) ← required align = align_T; real align_n = align_T ⇒ proved Proved
check Alias(_4) ← (hazard) resolve_origin(_4) → _1 (&self, shared) ⇒ shared view safe Proved
VM _3.term = _4.term, _3.prov = _4.prov, _3.flags = { non_null, aligned, init, in_bounds }
_0 = &(*_3)
VM _0.term = _3.term, _0.prov = _3.prov, _0.flags = { non_null, aligned, init, in_bounds }
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
Formal reasoning rules. The deduction rules for discharging each property (Layout, Allocation, pointer arithmetic, slice bounds, fast-path flags, Ptr2Ref) are given in §8.5.
Alias hazard. Alias is a hazard by default, but it also expresses a no-aliasing precondition through Ptr2Ref/Drop. Its five-pass check — provenance resolution, the flow-sensitive alias set, shared-XOR-mutable, the forward check, and escape — is described in §8.5.
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) } } }
MIR. On the mutable receiver the shape is the same as get_unchecked (§10.1.3.1) — one InBound checkpoint at get_unchecked_mut, then the &mut * deref (Ptr2Ref checkpoint) — except the mutable reference reborrows into a longer chain: each &mut * is a distinct borrow edge through the opaque I::Output projection, and only the first is a checkpoint.
bb0: _7 = move _2;
_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. Identical to get_unchecked, with two differences: the &mut [T] receiver, and the Alias hazard resolving to &mut self (exclusive) instead of &self (shared). Both checkpoints discharge the same way; the trailing _4/_3/_0 = &mut (*…) are safe reborrows.
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. Three unsafe callsites — the two ptr.add pointer-arithmetic calls and ptr::swap:
#![allow(unused)] fn main() { // core::ptr::mut_ptr::add #[rapx::requires(InBound(self, T, count))] // 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 three unsafe callsites are reached on the normal path bb0 → bb1 → bb2 → bb3 → bb5 → bb6 (ptr.add(a)) → bb7 (ptr.add(b)) → bb8 (ptr::swap).
MIR. The statements on that path:
bb5: _11 = as_mut_ptr(&mut (*_1));
bb6: _14 = ptr.add(copy _11, _2); // ptr.add(a) ← checkpoint (1)
bb7: _17 = ptr.add(copy _11, _3); // ptr.add(b) ← checkpoint (2)
bb8: _13 = ptr::swap(move _14, move _17); // ← checkpoint (3)
Verification.
entry _1 = self (&mut [T]), _2 = a (usize), _3 = b (usize)
init_parameters:
data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
_1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
slice type invariant (JSON `[T]` entry):
NonNull(_1) : _1.term ≠ 0
Align(_1, T) : _1.term % align_T == 0
ValidNum(..) : len * sizeof_T ≤ isize::MAX
Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
Init(_1, T, len) : data_alloc.initialized = true
caller contracts (asserted as facts):
ValidNum(a, [0, len)) → _2.term < len
ValidNum(b, [0, len)) → _3.term < len
_11 = as_mut_ptr(&mut (*_1))
VM _11.term = _1.term, _11.prov = _1.prov, _11.align_n = align_T
_14 = ptr.add(copy _11, _2) [checkpoint (1)]
check InBound(_11, T, _2) ← _2.term < len (caller `ValidNum(a, [0, len))`) Proved
VM _14.term = _11.term + _2.term*sizeof_T, _14.prov = (data_alloc, _2.term*sizeof_T), _14.align_n = align_T
_17 = ptr.add(copy _11, _3) [checkpoint (2)]
check InBound(_11, T, _3) ← _3.term < len (caller `ValidNum(b, [0, len))`) Proved
VM _17.term = _11.term + _3.term*sizeof_T, _17.prov = (data_alloc, _3.term*sizeof_T), _17.align_n = align_T
_13 = ptr::swap(move _14, move _17) [checkpoint (3)]
check ValidPtr(_14, T, 1) ← NonNull (flag) + Allocated/InBound by `_2.term < len` Proved
check Align(_14, T) ← required align = align_T; real align_n = align_T ⇒ proved Proved
check ValidPtr(_17, T, 1) ← NonNull (flag) + Allocated/InBound by `_3.term < len` Proved
check Align(_17, T) ← required align = align_T; real align_n = align_T ⇒ proved Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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(self.len() % 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 _1 = self (&[T])
init_parameters:
data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
_1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
slice type invariant (JSON `[T]` entry):
NonNull(_1) : _1.term ≠ 0
Align(_1, T) : _1.term % align_T == 0
ValidNum(..) : len * sizeof_T ≤ isize::MAX
Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
Init(_1, T, len) : data_alloc.initialized = true
caller contracts (asserted as facts):
ValidNum(N, [1, ∞)) → N ≠ 0
ValidNum(len % N == 0) → len % N == 0
_8 = len(&(*_1))
VM _8.term = len
_7 = exact_div(move _8, const N) [checkpoint (1)]
check non-zero divisor ← N ≠ 0 Proved
VM _7.term = len / N (= new_len)
_12 = as_ptr(&(*_1))
VM _12.term = _1.term, _12.prov = _1.prov
_11 = ptr.cast::<[T; N]>(move _12)
VM re-interpret *const T as *const [T; N] (layout-identical)
_10 = raw::from_raw_parts(move _11, copy _7) [checkpoint (2)]
check NonNull + Align + Init + Allocated ← inherited from the slice invariant Proved
check ValidPtr + ValidNum + Alive + Alias ← slice's full validity at entry Proved
check InBound + ValidNum ← len % N == 0 ⇒ len = new_len*N, so
new_len * size_of([T; N]) = len * sizeof_T Proved
VM _10 = (&[T; N]) of new_len elements over data_alloc
_0 = &(*_10)
VM safe reborrow → return slot
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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(self.len() % 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, on the mutable receiver:
entry _1 = self (&mut [T]) [slice invariant]
fact: N ≠ 0, len % N == 0
_8 = exact_div(len, N) [checkpoint (1)]
check non-zero divisor ← N ≠ 0 Proved
_12 = from_raw_parts_mut(cast::<[T; N]>(as_mut_ptr(_1)), _8) [checkpoint (2)]
check ValidPtr/InBound/ValidNum ← len % N == 0 Proved
check Alias ← exclusive &mut self receiver Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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. The ptr.add(mid) pointer-arithmetic call, then two from_raw_parts callsites:
#![allow(unused)] fn main() { // core::ptr::const_ptr::add #[rapx::requires(InBound(self, T, count))] // 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, the three callsites are reached on the normal path … → bb6 (left from_raw_parts) → bb7 (ptr.add) → bb8 (right from_raw_parts).
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) ← checkpoint (2)
bb8: _21 = SubUnchecked(copy _3, copy _2); // len - mid
_17 = raw::from_raw_parts(move _18, move _21); // ← checkpoint (3), right [mid, len)
Verification.
entry _1 = self (&[T]), _2 = mid (usize)
init_parameters:
data_alloc.align = align_T, data_alloc.slice_len = len, data_alloc.size = len * sizeof_T, data_alloc.element_ty = T
_1.term = data_alloc.base, _1.prov = (data_alloc, 0), _1.flags = { non_null, aligned, init, in_bounds }
slice type invariant (JSON `[T]` entry):
NonNull(_1) : _1.term ≠ 0
Align(_1, T) : _1.term % align_T == 0
ValidNum(..) : len * sizeof_T ≤ isize::MAX
Allocated(_1, T, len) : len·sizeof_T ≤ data_alloc.size
Init(_1, T, len) : data_alloc.initialized = true
caller contracts (asserted as facts):
ValidNum(mid, [0, len]) → 0 ≤ _2.term ≤ len
_3 = len(&(*_1))
VM _3.term = len
_5 = as_ptr(&(*_1))
VM _5.term = _1.term, _5.prov = _1.prov
_13 = raw::from_raw_parts(copy _5, copy _2) [checkpoint (1), left [0, mid)]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← mid ≤ len ⇒ [0, mid) ⊆ [0, len) Proved
VM _13 = (&[T]) of mid elements over data_alloc
_18 = ptr.add(copy _5, copy _2) [checkpoint (2)]
check InBound(_5, T, _2) ← _2.term ≤ len (caller `ValidNum(mid, [0, len])`) Proved
VM _18.term = _5.term + _2.term*sizeof_T, _18.prov = (data_alloc, _2.term*sizeof_T)
_21 = SubUnchecked(copy _3, copy _2)
VM _21.term = len − mid
_17 = raw::from_raw_parts(move _18, move _21) [checkpoint (3), right [mid, len)]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← mid ≤ len ⇒ [mid, len) ⊆ [0, len) Proved
VM _17 = (&[T]) of len−mid elements at data_alloc + mid*sizeof_T
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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. The ptr.add(mid) pointer-arithmetic call, then two from_raw_parts_mut callsites, each requiring the _mut variant of the from_raw_parts contract (adding Alias for exclusive access).
Path. … → bb6 (left from_raw_parts_mut) → bb7 (ptr.add) → bb8 (right from_raw_parts_mut).
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) ← checkpoint (2)
bb8: _21 = SubUnchecked(copy _3, copy _2); // len - mid
_17 = raw::from_raw_parts_mut(move _18, move _21); // ← checkpoint (3), right [mid, len)
Verification. Same as split_at_unchecked, on the mutable receiver:
entry _1 = self (&mut [T]), _2 = mid (usize) [slice invariant]
fact: 0 ≤ _2.term ≤ len
_13 = from_raw_parts_mut(as_mut_ptr(_1), _2) [checkpoint (1), left [0, mid)]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← mid ≤ len Proved
_18 = ptr.add(as_mut_ptr(_1), _2) [checkpoint (2)]
check InBound(_5, T, _2) ← _2.term ≤ len (caller `ValidNum(mid, [0, len])`) Proved
_21 = SubUnchecked(len, _2)
_17 = from_raw_parts_mut(ptr.add(as_mut_ptr(_1), _2), _21) [checkpoint (3), right [mid, len)]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← mid ≤ len Proved
check Alias ← [0, mid) and [mid, len) disjoint + exclusive receiver Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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, no contract obligations), the ptr.add pointer-arithmetic call, 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) ← checkpoint (2)
bb17: _50 = raw::from_raw_parts(move _51, copy _39); // ← checkpoint (3), tail [T]
Verification.
entry _1 = self (&[T]) [slice invariant]
fact: ValidTransmute(T, U)
_17 = ptr.align_offset(as_ptr(_1), align_of::<U>())
VM _17.term = offset (aligned split point)
_35 = split_at(&(*_1), _17)
VM _35 = (left, rest); left = [0, offset), rest = [offset, len)
_40 = rest.align_to_offsets::<U>()
VM _40 = (us_len, ts_len)
_45 = rest.as_ptr() as *const U
_44 = raw::from_raw_parts(_45, _38) [checkpoint (1), middle [U]]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← range analysis: middle in bounds Proved
_51 = ptr.add(rest.as_ptr(), len − ts_len) [checkpoint (2)]
check InBound(rest.as_ptr(), T, len − ts_len) ← range analysis Proved
_50 = raw::from_raw_parts(_51, _39) [checkpoint (3), tail [T]]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← range analysis: tail in bounds Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 (effect-modelled), the ptr.add pointer-arithmetic call, 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) ← checkpoint (2)
bb16: _53 = raw::from_raw_parts_mut(move _54, copy _39); // ← checkpoint (3), tail [T]
Verification. Same as align_to, on the mutable receiver:
entry _1 = self (&mut [T]) [slice invariant]
fact: ValidTransmute(T, U)
_48 = from_raw_parts_mut(rest.as_mut_ptr() as *mut U, us_len) [checkpoint (1), middle [U]]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← range analysis Proved
_54 = ptr.add(rest.as_mut_ptr(), rest_len − ts_len) [checkpoint (2)]
check InBound(rest.as_mut_ptr(), T, rest_len − ts_len) ← range analysis Proved
_53 = from_raw_parts_mut(rest.as_mut_ptr().add(rest_len − ts_len), ts_len) [checkpoint (3), tail [T]]
check NonNull + ValidPtr + Init + Alive + Alias + Align + ValidNum ← range analysis Proved
check Alias ← three &mut slices mutually disjoint + exclusive receiver Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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, four unsafe callsites per iteration:
(1) indices.get_unchecked(i) — the slice get_unchecked on [I; N], requiring InBound(indices, i);
(2) arr_ptr.cast().add(i) — the element-strided add over the MaybeUninit<[&mut I::Output; N]> slot array, requiring InBound(arr_ptr, &mut I::Output, i);
(3) slice.get_unchecked_mut(idx) — SliceIndex::get_unchecked_mut:
#![allow(unused)] fn main() { #[rapx::requires(InBound(slice, self))] }
(4) 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 four callsites sit at bb7 (get_unchecked), bb10 (ptr.add), 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) ← checkpoint (2)
bb12: _32 = ptr.get_unchecked_mut::<I>(_33, _34); // slice.get_unchecked_mut(idx) ← checkpoint (3)
bb13: _31 = &mut (*_32); // &mut * ← checkpoint (4)
_25 = ptr.write(move _26, move _30); // MaybeUninit::write
bb8: _0 = MaybeUninit::assume_init(...); // after all N iterations
Verification.
entry _1 = self (&mut [T]), _2 = indices ([I; N]) [slice invariant]
fact: InBound(self, indices), NonOverlap(indices)
# one loop iteration (unrolled):
_21 = indices.get_unchecked(i) [checkpoint (1)]
check InBound(indices, i) ← loop index i < N Proved
_26 = ptr.add(arr_ptr.cast(), i) [checkpoint (2)]
check InBound(arr_ptr.cast(), &mut I::Output, i) ← i < N Proved
_32 = slice.get_unchecked_mut(idx) [checkpoint (3)]
check InBound(slice, idx) ← InBound(self, indices) Proved
VM _32 = element pointer (data_alloc, idx*sizeof_T)
_31 = &mut (*_32) [checkpoint (4)]
check Init + ValidPtr + Align ← inherited from the slice invariant Proved
check Alias ← NonOverlap(indices): no two refs alias Proved
_25 = ptr.write(arr_ptr.cast().add(i), _31) // MaybeUninit slot write
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
The source-level argument is that the loop writes all N slots before assume_init. The trace above checks the enumerated loop iterations; it does not independently prove full initialization for arbitrary N by induction.
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 _1 = self (&[T]) / (&mut [T]) [slice invariant]
# else branch path condition: len ≥ N
_8 = as_ptr(&(*_1))
VM _8.term = _1.term, _8.prov = _1.prov
_7 = ptr.cast_array::<N>(move _8)
VM re-interpret *const T as *const [T; N] (layout-identical)
_6 = &(*_7) [Ptr2Ref checkpoint]
check Init + InBound ← len ≥ N ⇒ N-element array fits in the slice Proved
check Align ← slice invariant ([T; N] aligns as T) Proved
check Alias ← shared / exclusive receiver Proved
VM _6 = &[T; N] over data_alloc
_5 = &(*_6)
VM safe reborrow
_0 = Option::<&[T; N]>::Some(_5)
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) / (&mut [T]) [slice invariant]
_5 = split_at_checked(_1, N)
VM _5 = Some((first, tail)) iff N ≤ len // path condition N ≤ len
_3 = first, _4 = tail
_12 = as_ptr(&(*_3)); _11 = ptr.cast_array::<N>(_12)
_10 = &(*_11) [Ptr2Ref checkpoint]
check Init + Align + Alias ← as in first_chunk (N ≤ len) Proved
VM _10 = &[T; N] over data_alloc
_8 = (reborrow(_10), &(*_4)) // tail returned as-is
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) / (&mut [T]) [slice invariant]
_4 = checked_sub(len, N) // path condition: len ≥ N
_3 = index = len − N
_10 = split_at(_1, _3) // (init, last); last has exactly N elements
_18 = as_ptr(&last); _17 = ptr.cast_array::<N>(_18)
_16 = &(*_17) [Ptr2Ref checkpoint]
check Init + Align + Alias ← as in first_chunk (last has N elements) Proved
VM _16 = &[T; N] over data_alloc + (len−N)*sizeof_T
_0 = Some((&init, reborrow(_16)))
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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:
entry _1 = self (&[T]) / (&mut [T]) [slice invariant]
path condition: len ≥ N (from checked_sub)
_13 = &(*cast_array::<N>(as_ptr(&last))) [Ptr2Ref checkpoint]
check Init + Align + Alias ← last has exactly N elements Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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. Three callsites:
(1) end.sub(half_len) — the mut_ptr::sub pointer arithmetic:
#![allow(unused)] fn main() { // core::ptr::mut_ptr::sub #[rapx::requires(InBound(self, T, count))] }
(2) 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);
(3) 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) ← checkpoint (2)
bb5: _16 = from_raw_parts_mut(move _17, copy _2); // back_half ← checkpoint (3)
bb6: _21 = revswap(&mut (*_10), &mut (*_11), copy _2); // revswap → mem::swap loop
Verification.
entry _1 = self (&mut [T]) [slice invariant]
_2 = Div(len, 2) // half_len
_8 = as_mut_ptr_range(&mut (*_1)) // (start, end)
_13 = from_raw_parts_mut(start, _2) [checkpoint (1), front_half]
check ValidPtr + InBound + Alias ← front [0, half_len) in bounds, disjoint Proved
_17 = ptr.sub(end, _2) [checkpoint (2)]
check InBound(end, T, half_len) ← len − half_len ≥ 0 (half_len ≤ len) Proved
_16 = from_raw_parts_mut(_17, _2) [checkpoint (3), back_half]
check ValidPtr + InBound + Alias ← back [len−half_len, len) in bounds; len−half_len ≥ half_len ⇒ disjoint Proved
_21 = revswap(front_half, back_half, half_len)
# source-level invariant i ≤ n; RAPx checks enumerated iterations
check mem::swap(&mut a[i], &mut b[n−1−i]) ← disjoint halves ⇒ no alias Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) / (&mut [T]) [slice invariant]
path condition: N ≠ 0 (from assert!)
_10 = (len / N) * N // len_rounded_down
_18 = split_at_unchecked(_1, _10) [checkpoint (1)]
check ValidNum(mid, [0, len]) ← len_rounded_down = len/N*N ≤ len Proved
_21 = as_chunks_unchecked(_16) [checkpoint (2)]
check ValidNum(N, [1, ∞)) + ValidNum(len % N == 0) ← N ≠ 0; len_rounded_down multiple of N Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) [slice invariant]
path condition: N ≠ 0 (from assert!)
_18 = len − (len / N) * N // = len % N (remainder)
_16 = split_at(_1, _18) // (remainder, multiple_of_n)
_25 = as_chunks_unchecked(&multiple_of_n) [checkpoint]
check ValidNum(N, [1, ∞)) + ValidNum(len % N == 0) ← N ≠ 0; multiple_of_n length is a multiple of N Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) / (&mut [T]), _2 = mid (usize) [slice invariant]
_3 = Le(_2, len) // branch condition: mid ≤ len
_7 = split_at_unchecked(_1, _2) [checkpoint, Some branch only]
check ValidNum(mid, [0, len]) ← mid ≤ len ∧ mid: usize ≥ 0 Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) [slice invariant]
source-level invariant: base + size == len (not assumed by RAPx)
# loop iteration (unrolled):
_25 = self.get_unchecked(mid) [checkpoint]
check InBound(slice, mid) ← mid = base + size/2 < base + size == len Proved
# epilogue:
_44 = self.get_unchecked(base) [checkpoint]
check InBound(slice, base) ← size ≤ 1 ⇒ base < len Proved
_51 = assert_unchecked(base < len) ← base < len Proved
_65 = assert_unchecked(result ≤ len) ← verified independently Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 three ptr.add pointer-arithmetic calls (each requiring InBound(self, T, count)), 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) ← checkpoint
bb8: _26 = ptr.add(copy _14, copy _28); // prev_ptr_write = ptr.add(next_write - 1) ← checkpoint
bb9: _32 = call_mut(&mut _2, &mut *(_23), &mut *(_26)); // same_bucket(&mut *ptr_read, &mut *prev_ptr_write)
bb13: _43 = ptr.add(copy _14, copy _28); // ptr_write = prev_ptr_write.add(1) ← checkpoint
bb14: _45 = mem::swap(&mut *(_23), &mut *(_43)); // mem::swap(&mut *ptr_read, &mut *ptr_write)
Verification.
entry _1 = self (&mut [T]) [slice invariant]
source-level relation: 1 ≤ next_write ≤ next_read < len (not assumed by RAPx)
# loop iteration (unrolled):
_23 = ptr.add(as_mut_ptr(_1), next_read) [checkpoint] // ptr_read
check InBound(ptr, T, next_read) ← next_read < len Proved
_26 = ptr.add(as_mut_ptr(_1), next_write − 1) [checkpoint] // prev_ptr_write
check InBound(ptr, T, next_write − 1) ← next_write − 1 < len Proved
_32 = same_bucket(&mut *_23, &mut *_26) [Ptr2Ref checkpoint]
check Init + ValidPtr + Align + Alias ← next_read, next_write−1 in bounds; next_read > next_write−1 ⇒ no alias Proved
_43 = ptr.add(as_mut_ptr(_1), next_write) [checkpoint] // ptr_write = prev_ptr_write.add(1)
check InBound(ptr, T, next_write) ← next_write < len Proved
_45 = mem::swap(&mut *_23, &mut *_43) [Ptr2Ref checkpoint]
check Init + ValidPtr + Align + Alias ← in bounds; next_read ≠ next_write ⇒ ptr_read, ptr_write distinct Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&mut [T]), _2 = mid (usize) [slice invariant]
path condition: 0 ≤ mid ≤ len (from assert!)
_9 = SubWithOverflow(len, _2) // k = len − mid ≥ 0
_14 = as_mut_ptr(&mut (*_1)) // p
_18 = ptr.add(_14, _2) [checkpoint (1)]
check InBound(p, T, mid) ← left half [p, p+mid) in bounds; mid ≤ len Proved
VM _18 = (data_alloc, mid*sizeof_T)
_16 = ptr_rotate(mid, _18, _9) [checkpoint (2)]
check NonNull + Align + ValidPtr(mid, T, k) ← right half [p+mid, p+len) valid; k = len − mid Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&mut [T]), _2 = src (&[T]) [slice invariants]
path condition: dest.len() == src.len() (from the mismatch panic)
_16 = as_ptr(&(*_2)); _18 = as_mut_ptr(&mut (*_1)); _20 = len
_15 = ptr.copy_nonoverlapping(_16, _18, _20) [checkpoint]
check ValidPtr(src, T, n) + ValidPtr(dst, T, n) ← equal lengths Proved
check Align(src) + Align(dst) ← slice invariant Proved
check NonOverlap(dst, src, T, n) ← &mut self and &src are exclusive Proved
check ValidNum(n * sizeof_T ≤ isize::MAX) ← slice validity Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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. The two ptr.add pointer-arithmetic calls (src_ptr = ptr.add(src_start), dest_ptr = ptr.add(dest)), then 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) ← checkpoint (1)
bb10: _34 = ptr.add(copy _29, copy _3); // dest_ptr = ptr.add(dest) ← checkpoint (2)
bb11: _38 = move _31 as *const T;
_37 = ptr::copy(move _38, move _34, move _41); // ← checkpoint (3)
Verification.
entry _1 = self (&mut [T]) [slice invariant]
path conditions: src_start ≤ src_end ≤ len; dest + count ≤ len
_11 = src_end − src_start // count
_29 = as_mut_ptr(&mut (*_1)) // ptr
_31 = ptr.add(_29, src_start) [checkpoint (1)] // src_ptr
check InBound(ptr, T, src_start) ← src_start ≤ src_end ≤ len Proved
_34 = ptr.add(_29, dest) [checkpoint (2)] // dest_ptr
check InBound(ptr, T, dest) ← dest + count ≤ len ⇒ dest ≤ len Proved
_37 = ptr::copy(_31, _34, count) [checkpoint (3)]
check ValidPtr(src, T, n) + ValidPtr(dst, T, n) ← both ranges ⊆ [0, len) Proved
check Align(src) + Align(dst) ← slice invariant Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
ptr::copy permits overlap (memmove), so no NonOverlap obligation arises.
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 _1 = self (&mut [T]), _2 = other (&mut [T]) [slice invariants]
path condition: self.len() == other.len() (from assert!)
_16 = as_mut_ptr(&mut (*_1)); _18 = as_mut_ptr(&mut (*_2)); _20 = len
_15 = ptr::swap_nonoverlapping(_16, _18, _20) [checkpoint]
check ValidPtr(x, T, n) + Align(x) ← equal lengths + slice invariant Proved
check ValidPtr(y, T, n) + Align(y) ← equal lengths + slice invariant Proved
check NonOverlap(x, y, T, n) ← &mut self and &mut other exclusive Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&[T]) / (&mut [T]) [slice invariant]
path condition: size_of::<Simd<T, LANES>>() == size_of::<[T; LANES]>() (from assert_eq!)
_0 = align_to::<Simd<T, LANES>>(&(*_1)) [checkpoint (transmute)]
check ValidTransmute(T, Simd<T, LANES>) ← layout-identical by the size assertion Proved
# all alignment / contiguity / bounds properties inherited from align_to verification
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
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 _1 = self (&mut [T]), _2 = indices ([I; N]) [slice invariant]
_5 = get_disjoint_check_valid(indices, len) // inlined helper branches on the enumerated Ok paths
_15 = get_disjoint_unchecked_mut(_1, indices) [checkpoint]
check InBound(self, indices) ← inlined Ok-path conditions Proved
check NonOverlap(indices) ← inlined Ok-path conditions Proved
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
These results concern the enumerated paths through the helper and the unsafe call. They do not constitute a separately verified postcondition for get_disjoint_check_valid over every loop iteration.
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). Its #[rapx::verify] annotation yields a SOUND (no unsafe checkpoints) result. The annotation does not turn its Ok return into a trusted postcondition; RAPx analyzes the helper's inlined branches when checking 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.
entry _1 = indices (&[I; N]), _2 = len (usize)
# outer loop: for (i, idx) in indices.iter().enumerate()
_20 = idx.is_in_bounds(len)
# inner loop: for idx2 in indices[..i]
_39 = idx.is_overlapping(idx2)
result: SOUND (no unsafe checkpoints; pure validation loop)
By inspection, the source returns Ok only after every index passes is_in_bounds and every compared pair passes is_overlapping. The helper's own SOUND result does not prove that postcondition. The caller check uses conditions from the helper paths it enumerates.
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 _1 = self (&[T]) / (&mut [T]) [slice invariant]
fact: ValidTransmute([T; N], T)
_2 = unchecked_mul(len, N) // new length = len * N
_12 = ptr.cast::<T>(as_ptr(_1)) // re-interpret *const [T; N] as *const T
_11 = raw::from_raw_parts(_12, _2) [checkpoint]
check NonNull + ValidPtr + Init + Alive + Alias + Align ← inherited from the slice invariant Proved
check ValidNum(new_len * sizeof_T ≤ isize::MAX) ← slice already in the address space Proved
# cast re-interpretation covered by ValidTransmute([T; N], T)
return [type-invariant]
check NonNull + Align + ValidNum + Allocated + Init ← _1 unchanged Proved
result: SOUND
10.1.4 Code Reference
- Source:
safer-rust/rapx-verify-rust-std - Challenge: #281 / 0017-slice