From 875442367b1364ce5d9732244afb5737a523294a Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Wed, 17 Jun 2026 00:28:19 -0700 Subject: [PATCH 1/7] Verify slice split_at/swap unchecked fns (challenge #17) Safety contracts + Kani proof_for_contract harnesses for split_at_unchecked, split_at_mut_unchecked, and swap_unchecked (12 harnesses, all pass) via the proof_for_contract(<[T]>::method) + kani::slice::any_slice_of_array pattern. --- library/core/src/slice/mod.rs | 65 +++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 07a1ccc00011f..4bd88b10a10ab 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -945,6 +945,8 @@ impl [T] { /// [undefined behavior]: https://doc.rust-lang.org/reference/behavior-considered-undefined.html #[unstable(feature = "slice_swap_unchecked", issue = "88539")] #[track_caller] + #[requires(a < self.len() && b < self.len())] + #[cfg_attr(kani, kani::modifies(self))] pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) { assert_unsafe_precondition!( check_library_ub, @@ -2040,6 +2042,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(mid <= self.len())] pub const unsafe fn split_at_unchecked(&self, mid: usize) -> (&[T], &[T]) { // FIXME(const-hack): the const function `from_raw_parts` is used to make this // function const; previously the implementation used @@ -2094,6 +2097,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(mid <= 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(); @@ -5508,4 +5512,65 @@ mod verify { let mut a: [u8; 100] = kani::any(); a.reverse(); } + + // ---- Challenge 17: O(1) unsafe split/swap fns ---- + // These are bounds-geometry proofs (no element-value dependence and no loop), + // so they need no `#[kani::unwind]`; the symbolic-length sub-slice over a fixed + // backing array is the accepted "unbounded" encoding. + + macro_rules! check_split_at_unchecked { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(<[$ty]>::split_at_unchecked)] + fn $harness() { + const ARR_SIZE: usize = 100; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let mid: usize = kani::any(); + let _ = unsafe { slice.split_at_unchecked(mid) }; + } + }; + } + check_split_at_unchecked!(check_split_at_unchecked_unit, ()); + check_split_at_unchecked!(check_split_at_unchecked_u8, u8); + check_split_at_unchecked!(check_split_at_unchecked_u64, u64); + check_split_at_unchecked!(check_split_at_unchecked_char, char); + + macro_rules! check_split_at_mut_unchecked { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(<[$ty]>::split_at_mut_unchecked)] + fn $harness() { + const ARR_SIZE: usize = 100; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let mid: usize = kani::any(); + let _ = unsafe { slice.split_at_mut_unchecked(mid) }; + } + }; + } + check_split_at_mut_unchecked!(check_split_at_mut_unchecked_unit, ()); + check_split_at_mut_unchecked!(check_split_at_mut_unchecked_u8, u8); + check_split_at_mut_unchecked!(check_split_at_mut_unchecked_u64, u64); + check_split_at_mut_unchecked!(check_split_at_mut_unchecked_char, char); + + macro_rules! check_swap_unchecked { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(<[$ty]>::swap_unchecked)] + fn $harness() { + const ARR_SIZE: usize = 100; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let a: usize = kani::any(); + let b: usize = kani::any(); + unsafe { slice.swap_unchecked(a, b) }; + } + }; + } + // NOTE: no ZST (`()`) instantiation for `swap_unchecked`: `kani::modifies(self)` + // over a zero-size slice region trips a CBMC contracts-library limitation + // (`car_set_insert`). Swapping ZSTs moves zero bytes, so it is trivially safe; + // the non-ZST instantiations below exercise the actual `ptr::swap` memory writes. + check_swap_unchecked!(check_swap_unchecked_u8, u8); + check_swap_unchecked!(check_swap_unchecked_u16, u16); + check_swap_unchecked!(check_swap_unchecked_u64, u64); + check_swap_unchecked!(check_swap_unchecked_char, char); } From 777ad1cccdf342181a0da849d586fee2060ae7bd Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Wed, 17 Jun 2026 02:09:41 -0700 Subject: [PATCH 2/7] Verify slice get_unchecked/as_chunks_unchecked/get_disjoint unsafe fns (challenge #17) Completes the unsafe-function half of challenge #17: get_unchecked/_mut (#[requires(N != 0 && len % N == 0)] via proof_for_contract per concrete (T,N)), and get_disjoint_unchecked_mut (plain proof + assume: in-bounds + pairwise distinct). 39 harnesses, all pass. With tranche 1 and the existing align_to/ align_to_mut, all 10 unsafe slice functions in the challenge now verify. Signed-off-by: Onyeka Obi --- library/core/src/slice/mod.rs | 158 ++++++++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 4bd88b10a10ab..ed39ff53c17ff 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -1344,6 +1344,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(N != 0 && self.len() % N == 0)] pub const unsafe fn as_chunks_unchecked(&self) -> &[[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -1504,6 +1505,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(N != 0 && self.len() % N == 0)] pub const unsafe fn as_chunks_unchecked_mut(&mut self) -> &mut [[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -5573,4 +5575,160 @@ mod verify { check_swap_unchecked!(check_swap_unchecked_u16, u16); check_swap_unchecked!(check_swap_unchecked_u64, u64); check_swap_unchecked!(check_swap_unchecked_char, char); + + // ---- get_unchecked / get_unchecked_mut ---- + // These are generic over the `SliceIndex` type `I`, and the safety precondition + // is index-type-specific (`idx < len` for `usize`; `start <= end <= len` for a + // range). It therefore cannot be written as a single fn-level `#[requires]` over + // the generic `I` (a contract closure only borrows its args, so it cannot consume + // `index` to call a checked accessor, and there is no generic in-bounds predicate + // on `SliceIndex`). We prove no-UB at the two concrete index shapes with the + // documented caller obligation established by `kani::assume` -- the same approach + // challenge 16 used for non-contractable generic unsafe methods. O(1): no loop, + // so no `#[kani::unwind]`. + + macro_rules! check_get_unchecked { + ($usize_h:ident, $range_h:ident, $ty:ty) => { + #[kani::proof] + fn $usize_h() { + const ARR_SIZE: usize = 100; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let idx: usize = kani::any(); + kani::assume(idx < slice.len()); + let _ = unsafe { slice.get_unchecked(idx) }; + } + #[kani::proof] + fn $range_h() { + const ARR_SIZE: usize = 100; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let start: usize = kani::any(); + let end: usize = kani::any(); + kani::assume(start <= end && end <= slice.len()); + let _ = unsafe { slice.get_unchecked(start..end) }; + } + }; + } + check_get_unchecked!(check_get_unchecked_usize_unit, check_get_unchecked_range_unit, ()); + check_get_unchecked!(check_get_unchecked_usize_u8, check_get_unchecked_range_u8, u8); + check_get_unchecked!(check_get_unchecked_usize_u64, check_get_unchecked_range_u64, u64); + check_get_unchecked!(check_get_unchecked_usize_char, check_get_unchecked_range_char, char); + + macro_rules! check_get_unchecked_mut { + ($usize_h:ident, $range_h:ident, $ty:ty) => { + #[kani::proof] + fn $usize_h() { + const ARR_SIZE: usize = 100; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let idx: usize = kani::any(); + kani::assume(idx < slice.len()); + let _ = unsafe { slice.get_unchecked_mut(idx) }; + } + #[kani::proof] + fn $range_h() { + const ARR_SIZE: usize = 100; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let start: usize = kani::any(); + let end: usize = kani::any(); + kani::assume(start <= end && end <= slice.len()); + let _ = unsafe { slice.get_unchecked_mut(start..end) }; + } + }; + } + check_get_unchecked_mut!( + check_get_unchecked_mut_usize_unit, check_get_unchecked_mut_range_unit, () + ); + check_get_unchecked_mut!(check_get_unchecked_mut_usize_u8, check_get_unchecked_mut_range_u8, u8); + check_get_unchecked_mut!( + check_get_unchecked_mut_usize_u64, check_get_unchecked_mut_range_u64, u64 + ); + check_get_unchecked_mut!( + check_get_unchecked_mut_usize_char, check_get_unchecked_mut_range_char, char + ); + + // ---- as_chunks_unchecked / as_chunks_unchecked_mut ---- + // Reinterpret `[T]` as `[[T; N]]`; precondition `N != 0 && len % N == 0` is + // expressible generically, so these carry real `#[requires]` contracts and are + // checked per concrete (T, N) monomorphization. O(1) (no loop): exact_div + a + // single from_raw_parts cast. No writes -> no `modifies`. + + macro_rules! check_as_chunks_unchecked { + ($harness:ident, $ty:ty, $n:literal) => { + #[kani::proof_for_contract(<[$ty]>::as_chunks_unchecked::<$n>)] + fn $harness() { + const ARR_SIZE: usize = 64; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let _ = unsafe { slice.as_chunks_unchecked::<$n>() }; + } + }; + } + check_as_chunks_unchecked!(check_as_chunks_unchecked_u8_2, u8, 2); + check_as_chunks_unchecked!(check_as_chunks_unchecked_u8_3, u8, 3); + check_as_chunks_unchecked!(check_as_chunks_unchecked_u64_2, u64, 2); + check_as_chunks_unchecked!(check_as_chunks_unchecked_char_3, char, 3); + + macro_rules! check_as_chunks_unchecked_mut { + ($harness:ident, $ty:ty, $n:literal) => { + #[kani::proof_for_contract(<[$ty]>::as_chunks_unchecked_mut::<$n>)] + fn $harness() { + const ARR_SIZE: usize = 64; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = unsafe { slice.as_chunks_unchecked_mut::<$n>() }; + } + }; + } + check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_u8_2, u8, 2); + check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_u8_3, u8, 3); + check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_u64_2, u64, 2); + check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_char_3, char, 3); + + // ---- get_disjoint_unchecked_mut ---- + // Generic over the index type `I` and const `N`, with a two-part precondition: + // every index in bounds AND the indices pairwise disjoint. As with get_unchecked + // (index-type-specific, non-contractable over generic `I`), we prove no-UB at + // concrete `I = usize` and small `N` with the obligation set by `kani::assume` + // (each `idx < len`; pairwise distinct). The body loops `0..N` with concrete `N`, + // so the loop bound is concrete and needs no `#[kani::unwind]`. + + #[kani::proof] + fn check_get_disjoint_unchecked_mut_2_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + kani::assume(i0 < slice.len() && i1 < slice.len()); + kani::assume(i0 != i1); + let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1]) }; + } + + #[kani::proof] + fn check_get_disjoint_unchecked_mut_2_u64() { + const ARR_SIZE: usize = 100; + let mut arr: [u64; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + kani::assume(i0 < slice.len() && i1 < slice.len()); + kani::assume(i0 != i1); + let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1]) }; + } + + #[kani::proof] + fn check_get_disjoint_unchecked_mut_3_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + let i2: usize = kani::any(); + kani::assume(i0 < slice.len() && i1 < slice.len() && i2 < slice.len()); + kani::assume(i0 != i1 && i0 != i2 && i1 != i2); + let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1, i2]) }; + } } From b3b5abb3157566a6a802aaedacf6b53a4f5cb9d1 Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Wed, 17 Jun 2026 02:22:17 -0700 Subject: [PATCH 3/7] No-UB harnesses for the constant-time safe slice abstractions: first_chunk/ first_chunk_mut, last_chunk/last_chunk_mut, split_first_chunk/_mut, split_last_chunk/_mut, split_at_checked/split_at_mut_checked. 24 harnesses over representative element types and chunk sizes (incl. the N=0 edge), all pass; each uses a symbolic-length slice so both the None and cast/split branches are covered. No loops, so no unwind bounds. Signed-off-by: Onyeka Obi --- library/core/src/slice/mod.rs | 85 +++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index ed39ff53c17ff..8a803f5b726fd 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -5731,4 +5731,89 @@ mod verify { kani::assume(i0 != i1 && i0 != i2 && i1 != i2); let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1, i2]) }; } + + // ---- Safe chunk accessors (first/last/split_first/split_last _chunk) ---- + // Safe abstractions: prove the internal unsafe (a bounded `cast_array` ptr cast + // guarded by a `len < N` / `split_at_checked(N)` check) is UB-free for a slice of + // any (symbolic) length. O(1), no loop -> no `#[kani::unwind]`. The symbolic + // length exercises both the `None` (too short) and `Some` (cast) branches. + + macro_rules! check_chunk_accessor { + ($harness:ident, $ty:ty, $n:literal, $method:ident) => { + #[kani::proof] + fn $harness() { + const ARR_SIZE: usize = 64; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let _ = slice.$method::<$n>(); + } + }; + } + macro_rules! check_chunk_accessor_mut { + ($harness:ident, $ty:ty, $n:literal, $method:ident) => { + #[kani::proof] + fn $harness() { + const ARR_SIZE: usize = 64; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = slice.$method::<$n>(); + } + }; + } + + check_chunk_accessor!(check_first_chunk_u8_0, u8, 0, first_chunk); + check_chunk_accessor!(check_first_chunk_u8_2, u8, 2, first_chunk); + check_chunk_accessor!(check_first_chunk_char_3, char, 3, first_chunk); + check_chunk_accessor!(check_split_first_chunk_u8_2, u8, 2, split_first_chunk); + check_chunk_accessor!(check_split_first_chunk_char_3, char, 3, split_first_chunk); + check_chunk_accessor!(check_split_last_chunk_u8_2, u8, 2, split_last_chunk); + check_chunk_accessor!(check_split_last_chunk_char_3, char, 3, split_last_chunk); + check_chunk_accessor!(check_last_chunk_u8_0, u8, 0, last_chunk); + check_chunk_accessor!(check_last_chunk_u8_2, u8, 2, last_chunk); + check_chunk_accessor!(check_last_chunk_char_3, char, 3, last_chunk); + + check_chunk_accessor_mut!(check_first_chunk_mut_u8_2, u8, 2, first_chunk_mut); + check_chunk_accessor_mut!(check_first_chunk_mut_char_3, char, 3, first_chunk_mut); + check_chunk_accessor_mut!(check_split_first_chunk_mut_u8_2, u8, 2, split_first_chunk_mut); + check_chunk_accessor_mut!(check_split_first_chunk_mut_char_3, char, 3, split_first_chunk_mut); + check_chunk_accessor_mut!(check_split_last_chunk_mut_u8_2, u8, 2, split_last_chunk_mut); + check_chunk_accessor_mut!(check_split_last_chunk_mut_char_3, char, 3, split_last_chunk_mut); + check_chunk_accessor_mut!(check_last_chunk_mut_u8_2, u8, 2, last_chunk_mut); + check_chunk_accessor_mut!(check_last_chunk_mut_char_3, char, 3, last_chunk_mut); + + // ---- split_at_checked / split_at_mut_checked ---- + // Safe wrappers over split_at_unchecked guarded by `mid <= len`; symbolic `mid` + // exercises both the `Some` and `None` branches. O(1), no loop. + + macro_rules! check_split_at_checked { + ($harness:ident, $ty:ty) => { + #[kani::proof] + fn $harness() { + const ARR_SIZE: usize = 64; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let mid: usize = kani::any(); + let _ = slice.split_at_checked(mid); + } + }; + } + check_split_at_checked!(check_split_at_checked_u8, u8); + check_split_at_checked!(check_split_at_checked_u64, u64); + check_split_at_checked!(check_split_at_checked_char, char); + + macro_rules! check_split_at_mut_checked { + ($harness:ident, $ty:ty) => { + #[kani::proof] + fn $harness() { + const ARR_SIZE: usize = 64; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let mid: usize = kani::any(); + let _ = slice.split_at_mut_checked(mid); + } + }; + } + check_split_at_mut_checked!(check_split_at_mut_checked_u8, u8); + check_split_at_mut_checked!(check_split_at_mut_checked_u64, u64); + check_split_at_mut_checked!(check_split_at_mut_checked_char, char); } From 4daabfce1a20ddbdfe73cb1ecbab9bff99c47f73 Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Wed, 17 Jun 2026 02:52:56 -0700 Subject: [PATCH 4/7] Verify slice chunking/flatten/simd/search/disjoint safe abstractions (challenge #17) No-UB harnesses for the O(1)/log/N-bounded safe abstractions: as_chunks/_mut/ as_rchunks, as_flattened/_mut, as_simd/_mut (replay align_to), binary_search_by (logarithmic loop, unwind 7), get_disjoint_mut + get_disjoint_check_valid (const-N loops). 19 harnesses, all pass. Brings challenge #17 to 30/37 (all 10 unsafe + 20 of 26 safe). Signed-off-by: Onyeka Obi --- library/core/src/slice/mod.rs | 153 ++++++++++++++++++++++++++++++++++ 1 file changed, 153 insertions(+) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 8a803f5b726fd..9c90c3a618e07 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -5816,4 +5816,157 @@ mod verify { check_split_at_mut_checked!(check_split_at_mut_checked_u8, u8); check_split_at_mut_checked!(check_split_at_mut_checked_u64, u64); check_split_at_mut_checked!(check_split_at_mut_checked_char, char); + + // ---- as_chunks / as_chunks_mut / as_rchunks (O(1), no loop) ---- + // Split into a slice of `[T; N]` plus a remainder via split_at_unchecked + + // as_chunks_unchecked; pure pointer/length arithmetic, no loops -> no unwind. + + macro_rules! check_as_chunks_fam { + ($h:ident, $ty:ty, $n:literal, $m:ident) => { + #[kani::proof] + fn $h() { + const ARR_SIZE: usize = 64; + let arr: [$ty; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&arr); + let _ = s.$m::<$n>(); + } + }; + } + check_as_chunks_fam!(check_as_chunks_u8_2, u8, 2, as_chunks); + check_as_chunks_fam!(check_as_chunks_char_3, char, 3, as_chunks); + check_as_chunks_fam!(check_as_rchunks_u8_2, u8, 2, as_rchunks); + check_as_chunks_fam!(check_as_rchunks_char_3, char, 3, as_rchunks); + + #[kani::proof] + fn check_as_chunks_mut_u8_2() { + const ARR_SIZE: usize = 64; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = s.as_chunks_mut::<2>(); + } + #[kani::proof] + fn check_as_chunks_mut_char_3() { + const ARR_SIZE: usize = 64; + let mut arr: [char; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = s.as_chunks_mut::<3>(); + } + + // ---- as_flattened / as_flattened_mut (receiver is `[[T; N]]`) ---- + macro_rules! check_as_flattened { + ($h:ident, $ty:ty, $n:literal) => { + #[kani::proof] + fn $h() { + const ARR_SIZE: usize = 64; + let arr: [[$ty; $n]; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&arr); + let _ = s.as_flattened(); + } + }; + } + check_as_flattened!(check_as_flattened_u8_2, u8, 2); + check_as_flattened!(check_as_flattened_char_3, char, 3); + + macro_rules! check_as_flattened_mut { + ($h:ident, $ty:ty, $n:literal) => { + #[kani::proof] + fn $h() { + const ARR_SIZE: usize = 64; + let mut arr: [[$ty; $n]; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = s.as_flattened_mut(); + } + }; + } + check_as_flattened_mut!(check_as_flattened_mut_u8_2, u8, 2); + check_as_flattened_mut!(check_as_flattened_mut_char_3, char, 3); + + // ---- as_simd / as_simd_mut (delegate to the already-verified align_to) ---- + // Plain proof replays align_to's body (no contract assertion at the call site), + // so the real transmute is verified. T must be a SimdElement; LANES supported. + + macro_rules! check_as_simd { + ($h:ident, $ty:ty, $lanes:literal) => { + #[kani::proof] + fn $h() { + const ARR_SIZE: usize = 64; + let arr: [$ty; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&arr); + let _ = s.as_simd::<$lanes>(); + } + }; + } + check_as_simd!(check_as_simd_u8_4, u8, 4); + check_as_simd!(check_as_simd_u32_8, u32, 8); + + macro_rules! check_as_simd_mut { + ($h:ident, $ty:ty, $lanes:literal) => { + #[kani::proof] + fn $h() { + const ARR_SIZE: usize = 64; + let mut arr: [$ty; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = s.as_simd_mut::<$lanes>(); + } + }; + } + check_as_simd_mut!(check_as_simd_mut_u8_4, u8, 4); + check_as_simd_mut!(check_as_simd_mut_u32_8, u32, 8); + + // ---- binary_search_by (loop count is logarithmic in len) ---- + // A nondeterministic (possibly inconsistent) comparator still must keep every + // probe index in bounds. `size` halves each iteration, so unwind = log2(len)+2. + #[kani::proof] + #[kani::unwind(7)] + fn check_binary_search_by_u8() { + const ARR_SIZE: usize = 32; + let arr: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&arr); + let _ = s.binary_search_by(|_probe: &u8| match kani::any::() % 3 { + 0 => crate::cmp::Ordering::Less, + 1 => crate::cmp::Ordering::Equal, + _ => crate::cmp::Ordering::Greater, + }); + } + + // ---- get_disjoint_mut / get_disjoint_check_valid (loops bounded by const N) ---- + // get_disjoint_mut validates (bounds + pairwise-disjoint) then calls the unchecked + // path; fully symbolic indices exercise both the Ok and Err branches with no UB. + // Loops are `0..N` and the O(N^2) overlap check, both const-N bounded -> no unwind. + + #[kani::proof] + fn check_get_disjoint_mut_2_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + let _ = s.get_disjoint_mut([i0, i1]); + } + #[kani::proof] + fn check_get_disjoint_mut_3_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + let i2: usize = kani::any(); + let _ = s.get_disjoint_mut([i0, i1, i2]); + } + + #[kani::proof] + fn check_get_disjoint_check_valid_2() { + let len: usize = kani::any(); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + let _ = get_disjoint_check_valid::(&[i0, i1], len); + } + #[kani::proof] + fn check_get_disjoint_check_valid_3() { + let len: usize = kani::any(); + let i0: usize = kani::any(); + let i1: usize = kani::any(); + let i2: usize = kani::any(); + let _ = get_disjoint_check_valid::(&[i0, i1, i2], len); + } } From c956389b8bd96425c6b2f65c55c9b981a3dde370 Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Wed, 17 Jun 2026 03:43:23 -0700 Subject: [PATCH 5/7] Verify slice rotate/copy/swap/dedup safe abstractions (challenge #17) -- 37/37 copy_from_slice, copy_within, swap_with_slice, partition_dedup_by (symbolic length, small backing + #[kani::unwind]); rotate_left, rotate_right (concrete (length, amount) configs with symbolic values -- a symbolic rotation amount makes ptr_rotate's symbolic-size memcpy intractable >6GB here, so rotate is proven per-config). 16 harnesses, all pass. Completes all 37 functions in challenge #17 (10 unsafe + 27 safe abstractions). Signed-off-by: Onyeka Obi --- library/core/src/slice/mod.rs | 91 +++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 9c90c3a618e07..ab37c098c8abf 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -5969,4 +5969,95 @@ mod verify { let i2: usize = kani::any(); let _ = get_disjoint_check_valid::(&[i0, i1, i2], len); } + + // ---- Heavy linear-loop safe abstractions (small backing + tuned unwind) ---- + // These iterate over the slice length, so they need an explicit `#[kani::unwind]` + // (per the challenge-16 lesson) and a deliberately small backing array to keep + // the symbolic-length unrolling tractable. + + // rotate_left/right: proven over representative CONCRETE (length, amount) + // configurations with symbolic element values. A *symbolic* rotation amount is + // intractable here: `ptr_rotate` performs symbolic-size memcpys at a symbolic + // split point (and explores its block-swap/juggling paths), exceeding the 6GB + // CBMC budget on this machine even at length 3. With concrete (len, amount) the + // function takes a single concrete path whose bounds safety verifies cheaply; + // the spread of lengths/amounts exercises the early-return, buffer, and + // block-swap branches. (Disclosed bound: rotate coverage is per-config, not + // symbolic-length, unlike the rest of this challenge.) + macro_rules! check_rotate_cfg { + ($lh:ident, $rh:ident, $len:literal, $amt:literal, $uw:literal) => { + #[kani::proof] + #[kani::unwind($uw)] + fn $lh() { + let mut arr: [u8; $len] = kani::any(); + arr.rotate_left($amt); + } + #[kani::proof] + #[kani::unwind($uw)] + fn $rh() { + let mut arr: [u8; $len] = kani::any(); + arr.rotate_right($amt); + } + }; + } + check_rotate_cfg!(check_rotate_left_2_1, check_rotate_right_2_1, 2, 1, 4); + check_rotate_cfg!(check_rotate_left_3_1, check_rotate_right_3_1, 3, 1, 5); + check_rotate_cfg!(check_rotate_left_3_2, check_rotate_right_3_2, 3, 2, 5); + check_rotate_cfg!(check_rotate_left_4_2, check_rotate_right_4_2, 4, 2, 6); + check_rotate_cfg!(check_rotate_left_5_2, check_rotate_right_5_2, 5, 2, 7); + check_rotate_cfg!(check_rotate_left_8_3, check_rotate_right_8_3, 8, 3, 10); + + // src and dst come from SEPARATE backing arrays (disjoint, as copy_from_slice + // requires) with a shared symbolic length so the equal-length precondition holds. + #[kani::proof] + #[kani::unwind(9)] + fn check_copy_from_slice_u8() { + const ARR_SIZE: usize = 8; + let mut dst_arr: [u8; ARR_SIZE] = kani::any(); + let src_arr: [u8; ARR_SIZE] = kani::any(); + let len: usize = kani::any(); + kani::assume(len <= ARR_SIZE); + let dst = &mut dst_arr[..len]; + let src = &src_arr[..len]; + dst.copy_from_slice(src); + } + + #[kani::proof] + #[kani::unwind(9)] + fn check_copy_within_u8() { + const ARR_SIZE: usize = 8; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let start: usize = kani::any(); + let end: usize = kani::any(); + let dest: usize = kani::any(); + kani::assume(start <= end && end <= s.len()); + let count = end - start; + kani::assume(dest <= s.len() - count); + s.copy_within(start..end, dest); + } + + #[kani::proof] + #[kani::unwind(9)] + fn check_swap_with_slice_u8() { + const ARR_SIZE: usize = 8; + let mut a_arr: [u8; ARR_SIZE] = kani::any(); + let mut b_arr: [u8; ARR_SIZE] = kani::any(); + let len: usize = kani::any(); + kani::assume(len <= ARR_SIZE); + let a = &mut a_arr[..len]; + let b = &mut b_arr[..len]; + a.swap_with_slice(b); + } + + // Heaviest: the dedup loop runs `next_read` from 1 to len with two &mut creations + // and a swap per iteration. Nondeterministic `same_bucket` exercises all branches. + #[kani::proof] + #[kani::unwind(6)] + fn check_partition_dedup_by_u8() { + const ARR_SIZE: usize = 5; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut arr); + let _ = s.partition_dedup_by(|_a, _b| kani::any()); + } } From 312bcc7f6d6f083f431114cbb526bb8cd2c3ecd1 Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Sun, 21 Jun 2026 19:53:02 -0700 Subject: [PATCH 6/7] Format challenge #17 harnesses to satisfy upstream rustfmt upstream_test's ./x fmt --check rejected the check_get_unchecked_mut! invocations; one macro argument per line under style_edition 2024. Formatting only. Signed-off-by: Onyeka Obi --- library/core/src/slice/mod.rs | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index ab37c098c8abf..e4b7abfae21f7 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -5639,14 +5639,24 @@ mod verify { }; } check_get_unchecked_mut!( - check_get_unchecked_mut_usize_unit, check_get_unchecked_mut_range_unit, () + check_get_unchecked_mut_usize_unit, + check_get_unchecked_mut_range_unit, + () ); - check_get_unchecked_mut!(check_get_unchecked_mut_usize_u8, check_get_unchecked_mut_range_u8, u8); check_get_unchecked_mut!( - check_get_unchecked_mut_usize_u64, check_get_unchecked_mut_range_u64, u64 + check_get_unchecked_mut_usize_u8, + check_get_unchecked_mut_range_u8, + u8 ); check_get_unchecked_mut!( - check_get_unchecked_mut_usize_char, check_get_unchecked_mut_range_char, char + check_get_unchecked_mut_usize_u64, + check_get_unchecked_mut_range_u64, + u64 + ); + check_get_unchecked_mut!( + check_get_unchecked_mut_usize_char, + check_get_unchecked_mut_range_char, + char ); // ---- as_chunks_unchecked / as_chunks_unchecked_mut ---- From 35de93a89d8d785858d442cb9421400f5322741e Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Sun, 16 Aug 2026 20:40:48 -0700 Subject: [PATCH 7/7] Add contracts for get_unchecked, get_unchecked_mut, and get_disjoint_unchecked_mut (challenge 17 review) Address the challenge 17 review: the three remaining unsafe functions now carry real fn-level safety contracts verified by proof_for_contract, instead of assume-guarded plain proofs. Kani cannot attach contracts to trait functions (model-checking/kani#1997), so the SliceIndex impls cannot carry them directly. Instead: - New kani-only predicate SliceIndex::kani_in_bounds(&self, len): the documented in-bounds precondition of each impl, overridden by all 13 SliceIndex<[T]> impls. The default is true, so a missing override makes proof_for_contract fail loudly instead of pass vacuously. - <[T]>::get_unchecked and <[T]>::get_unchecked_mut gain #[requires(index.kani_in_bounds(self.len()))]. - <[T]>::get_disjoint_unchecked_mut gains #[requires(get_disjoint_check_valid(&indices, self.len()).is_ok())], the same GetDisjointMutIndex predicate the safe get_disjoint_mut gates on. - The assume-guarded plain proofs are replaced by proof_for_contract harnesses that drive the contracted wrappers through the real body of every SliceIndex<[T]> impl: usize, IndexRange, Range, RangeTo, RangeFrom, RangeFull, RangeInclusive, RangeToInclusive, their core::range counterparts, and (Bound, Bound). RangeInclusive inputs include iteration-exhausted values, so the exhausted arm of its predicate is exercised. get_disjoint_unchecked_mut is verified for usize (N = 2, 3) and all four GetDisjointMutIndex range impls (ops and core::range flavors of Range and RangeInclusive). Local verification with the pinned Kani (415ca503): 46/46 harnesses successful. Contract liveness confirmed by mutation: weakening the usize predicate (< to <=), dropping the end <= len conjunct of the Range predicate, and inverting the disjoint contract each make the matching harness fail. rustfmt is clean under the upstream rust-lang/rust config. Signed-off-by: Onyeka Obi --- library/core/src/slice/index.rs | 81 ++++++++ library/core/src/slice/mod.rs | 339 +++++++++++++++++++++++--------- 2 files changed, 332 insertions(+), 88 deletions(-) diff --git a/library/core/src/slice/index.rs b/library/core/src/slice/index.rs index de220e7e38a4b..86fc343cb4aa6 100644 --- a/library/core/src/slice/index.rs +++ b/library/core/src/slice/index.rs @@ -201,6 +201,22 @@ pub unsafe trait SliceIndex: private_slice_index::Sealed { #[unstable(feature = "slice_index_methods", issue = "none")] #[track_caller] fn index_mut(self, slice: &mut T) -> &mut Self::Output; + + /// Returns `true` if `self` is an in-bounds index for a container of + /// length `len`. This is the documented safety precondition of + /// [`get_unchecked`](SliceIndex::get_unchecked) and + /// [`get_unchecked_mut`](SliceIndex::get_unchecked_mut). + /// + /// Every impl used through a contracted caller must override this with the + /// exact documented precondition. The default imposes no restriction, so a + /// missing override makes `proof_for_contract` fail loudly instead of pass + /// vacuously. + #[cfg(kani)] + #[unstable(feature = "kani", issue = "none")] + fn kani_in_bounds(&self, len: usize) -> bool { + let _ = len; + true + } } /// The methods `index` and `index_mut` panic if the index is out of bounds. @@ -272,6 +288,11 @@ unsafe impl const SliceIndex<[T]> for usize { // N.B., use intrinsic indexing &mut (*slice)[self] } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + *self < len + } } /// Because `IndexRange` guarantees `start <= end`, fewer checks are needed here @@ -347,6 +368,11 @@ unsafe impl const SliceIndex<[T]> for ops::IndexRange { slice_index_fail(self.start(), self.end(), slice.len()) } } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.start() <= self.end() && self.end() <= len + } } /// The methods `index` and `index_mut` panic if: @@ -451,6 +477,11 @@ unsafe impl const SliceIndex<[T]> for ops::Range { slice_index_fail(self.start, self.end, slice.len()) } } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.start <= self.end && self.end <= len + } } #[unstable(feature = "new_range_api", issue = "125687")] @@ -489,6 +520,11 @@ unsafe impl const SliceIndex<[T]> for range::Range { fn index_mut(self, slice: &mut [T]) -> &mut [T] { ops::Range::from(self).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.start <= self.end && self.end <= len + } } /// The methods `index` and `index_mut` panic if the end of the range is out of bounds. @@ -528,6 +564,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeTo { fn index_mut(self, slice: &mut [T]) -> &mut [T] { (0..self.end).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.end <= len + } } /// The methods `index` and `index_mut` panic if the start of the range is out of bounds. @@ -575,6 +616,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeFrom { // SAFETY: `self` is checked to be valid and in bounds above. unsafe { &mut *self.get_unchecked_mut(slice) } } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.start <= len + } } #[unstable(feature = "new_range_api", issue = "125687")] @@ -613,6 +659,11 @@ unsafe impl const SliceIndex<[T]> for range::RangeFrom { fn index_mut(self, slice: &mut [T]) -> &mut [T] { ops::RangeFrom::from(self).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.start <= len + } } #[stable(feature = "slice_get_slice_impls", since = "1.15.0")] @@ -649,6 +700,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeFull { fn index_mut(self, slice: &mut [T]) -> &mut [T] { slice } + + #[cfg(kani)] + fn kani_in_bounds(&self, _len: usize) -> bool { + true + } } /// The methods `index` and `index_mut` panic if: @@ -711,6 +767,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { } slice_index_fail(start, end, slice.len()) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.end < len && (self.exhausted || self.start <= self.end + 1) + } } #[unstable(feature = "new_range_api", issue = "125687")] @@ -749,6 +810,11 @@ unsafe impl const SliceIndex<[T]> for range::RangeInclusive { fn index_mut(self, slice: &mut [T]) -> &mut [T] { ops::RangeInclusive::from(self).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.last < len && self.start <= self.last + 1 + } } /// The methods `index` and `index_mut` panic if the end of the range is out of bounds. @@ -788,6 +854,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeToInclusive { fn index_mut(self, slice: &mut [T]) -> &mut [T] { (0..=self.end).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.end < len + } } /// The methods `index` and `index_mut` panic if the end of the range is out of bounds. @@ -827,6 +898,11 @@ unsafe impl const SliceIndex<[T]> for range::RangeToInclusive { fn index_mut(self, slice: &mut [T]) -> &mut [T] { (0..=self.last).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + self.last < len + } } /// Performs bounds checking of a range. @@ -1087,4 +1163,9 @@ unsafe impl SliceIndex<[T]> for (ops::Bound, ops::Bound) { fn index_mut(self, slice: &mut [T]) -> &mut Self::Output { into_slice_range(slice.len(), self).index_mut(slice) } + + #[cfg(kani)] + fn kani_in_bounds(&self, len: usize) -> bool { + into_range(len, *self).is_some_and(|r| r.start <= r.end && r.end <= len) + } } diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index e4b7abfae21f7..d18e39e370d2f 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -638,6 +638,7 @@ impl [T] { #[must_use] #[track_caller] #[rustc_const_unstable(feature = "const_index", issue = "143775")] + #[requires(index.kani_in_bounds(self.len()))] pub const unsafe fn get_unchecked(&self, index: I) -> &I::Output where I: [const] SliceIndex, @@ -683,6 +684,7 @@ impl [T] { #[must_use] #[track_caller] #[rustc_const_unstable(feature = "const_index", issue = "143775")] + #[requires(index.kani_in_bounds(self.len()))] pub const unsafe fn get_unchecked_mut(&mut self, index: I) -> &mut I::Output where I: [const] SliceIndex, @@ -4781,6 +4783,7 @@ impl [T] { #[stable(feature = "get_many_mut", since = "1.86.0")] #[inline] #[track_caller] + #[requires(get_disjoint_check_valid(&indices, self.len()).is_ok())] pub unsafe fn get_disjoint_unchecked_mut( &mut self, indices: [I; N], @@ -5577,86 +5580,198 @@ mod verify { check_swap_unchecked!(check_swap_unchecked_char, char); // ---- get_unchecked / get_unchecked_mut ---- - // These are generic over the `SliceIndex` type `I`, and the safety precondition - // is index-type-specific (`idx < len` for `usize`; `start <= end <= len` for a - // range). It therefore cannot be written as a single fn-level `#[requires]` over - // the generic `I` (a contract closure only borrows its args, so it cannot consume - // `index` to call a checked accessor, and there is no generic in-bounds predicate - // on `SliceIndex`). We prove no-UB at the two concrete index shapes with the - // documented caller obligation established by `kani::assume` -- the same approach - // challenge 16 used for non-contractable generic unsafe methods. O(1): no loop, - // so no `#[kani::unwind]`. - - macro_rules! check_get_unchecked { - ($usize_h:ident, $range_h:ident, $ty:ty) => { - #[kani::proof] - fn $usize_h() { - const ARR_SIZE: usize = 100; - let arr: [$ty; ARR_SIZE] = kani::any(); - let slice = kani::slice::any_slice_of_array(&arr); - let idx: usize = kani::any(); - kani::assume(idx < slice.len()); - let _ = unsafe { slice.get_unchecked(idx) }; - } - #[kani::proof] - fn $range_h() { - const ARR_SIZE: usize = 100; - let arr: [$ty; ARR_SIZE] = kani::any(); - let slice = kani::slice::any_slice_of_array(&arr); - let start: usize = kani::any(); - let end: usize = kani::any(); - kani::assume(start <= end && end <= slice.len()); - let _ = unsafe { slice.get_unchecked(start..end) }; - } - }; + // These are generic over the `SliceIndex` type `I`. Kani does not support + // contracts on trait functions (model-checking/kani#1997), so the + // `SliceIndex` impls cannot carry them. Instead, the kani-only trait + // predicate `SliceIndex::kani_in_bounds` (implemented by every + // `SliceIndex<[T]>` impl with that impl's documented in-bounds + // precondition) gives the generic inherent wrappers + // `<[T]>::get_unchecked{,_mut}` a real fn-level `#[requires]` contract. + // Each `proof_for_contract` harness verifies the wrapper through the real + // body of one concrete index-type impl; together they cover every + // `SliceIndex<[T]>` impl. O(1): no loop, so no `#[kani::unwind]`. + // `RangeInclusive` inputs come from `any_range_inclusive`, which also + // exhausts the range by iteration on a nondet branch, so the `exhausted` + // arm of its `kani_in_bounds` predicate is exercised too. + + use crate::ops::{Bound, IndexRange}; + + fn any_range_inclusive() -> crate::ops::RangeInclusive { + let mut range = kani::any::()..=kani::any::(); + let exhaust: bool = kani::any(); + if exhaust { + let _ = range.next(); + } + range } - check_get_unchecked!(check_get_unchecked_usize_unit, check_get_unchecked_range_unit, ()); - check_get_unchecked!(check_get_unchecked_usize_u8, check_get_unchecked_range_u8, u8); - check_get_unchecked!(check_get_unchecked_usize_u64, check_get_unchecked_range_u64, u64); - check_get_unchecked!(check_get_unchecked_usize_char, check_get_unchecked_range_char, char); - macro_rules! check_get_unchecked_mut { - ($usize_h:ident, $range_h:ident, $ty:ty) => { - #[kani::proof] - fn $usize_h() { + fn any_bound() -> Bound { + let selector: u8 = kani::any(); + match selector % 3 { + 0 => Bound::Included(kani::any()), + 1 => Bound::Excluded(kani::any()), + 2..=u8::MAX => Bound::Unbounded, + } + } + + macro_rules! check_get_unchecked_contract { + ($h:ident, $h_mut:ident, $ity:ty, $ty:ty, $mk:expr) => { + #[kani::proof_for_contract(<[$ty]>::get_unchecked::<$ity>)] + fn $h() { const ARR_SIZE: usize = 100; - let mut arr: [$ty; ARR_SIZE] = kani::any(); - let slice = kani::slice::any_slice_of_array_mut(&mut arr); - let idx: usize = kani::any(); - kani::assume(idx < slice.len()); - let _ = unsafe { slice.get_unchecked_mut(idx) }; + let arr: [$ty; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&arr); + let index: $ity = $mk; + let _ = unsafe { slice.get_unchecked(index) }; } - #[kani::proof] - fn $range_h() { + #[kani::proof_for_contract(<[$ty]>::get_unchecked_mut::<$ity>)] + fn $h_mut() { const ARR_SIZE: usize = 100; let mut arr: [$ty; ARR_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array_mut(&mut arr); - let start: usize = kani::any(); - let end: usize = kani::any(); - kani::assume(start <= end && end <= slice.len()); - let _ = unsafe { slice.get_unchecked_mut(start..end) }; + let index: $ity = $mk; + let _ = unsafe { slice.get_unchecked_mut(index) }; } }; } - check_get_unchecked_mut!( + check_get_unchecked_contract!( + check_get_unchecked_usize_unit, check_get_unchecked_mut_usize_unit, - check_get_unchecked_mut_range_unit, - () + usize, + (), + kani::any() ); - check_get_unchecked_mut!( + check_get_unchecked_contract!( + check_get_unchecked_usize_u8, check_get_unchecked_mut_usize_u8, - check_get_unchecked_mut_range_u8, - u8 + usize, + u8, + kani::any() ); - check_get_unchecked_mut!( + check_get_unchecked_contract!( + check_get_unchecked_usize_u64, check_get_unchecked_mut_usize_u64, - check_get_unchecked_mut_range_u64, - u64 + usize, + u64, + kani::any() ); - check_get_unchecked_mut!( + check_get_unchecked_contract!( + check_get_unchecked_usize_char, check_get_unchecked_mut_usize_char, + usize, + char, + kani::any() + ); + check_get_unchecked_contract!( + check_get_unchecked_index_range_u8, + check_get_unchecked_mut_index_range_u8, + IndexRange, + u8, + { + let start: usize = kani::any(); + let end: usize = kani::any(); + kani::assume(start <= end); + // SAFETY: `start <= end` is the constructor's documented precondition. + unsafe { IndexRange::new_unchecked(start, end) } + } + ); + check_get_unchecked_contract!( + check_get_unchecked_range_unit, + check_get_unchecked_mut_range_unit, + crate::ops::Range, + (), + kani::any::()..kani::any::() + ); + check_get_unchecked_contract!( + check_get_unchecked_range_u8, + check_get_unchecked_mut_range_u8, + crate::ops::Range, + u8, + kani::any::()..kani::any::() + ); + check_get_unchecked_contract!( + check_get_unchecked_range_u64, + check_get_unchecked_mut_range_u64, + crate::ops::Range, + u64, + kani::any::()..kani::any::() + ); + check_get_unchecked_contract!( + check_get_unchecked_range_char, check_get_unchecked_mut_range_char, - char + crate::ops::Range, + char, + kani::any::()..kani::any::() + ); + check_get_unchecked_contract!( + check_get_unchecked_new_range_u8, + check_get_unchecked_mut_new_range_u8, + crate::range::Range, + u8, + crate::range::Range { start: kani::any(), end: kani::any() } + ); + check_get_unchecked_contract!( + check_get_unchecked_range_to_u8, + check_get_unchecked_mut_range_to_u8, + crate::ops::RangeTo, + u8, + ..kani::any::() + ); + check_get_unchecked_contract!( + check_get_unchecked_range_from_u8, + check_get_unchecked_mut_range_from_u8, + crate::ops::RangeFrom, + u8, + kani::any::().. + ); + check_get_unchecked_contract!( + check_get_unchecked_new_range_from_u8, + check_get_unchecked_mut_new_range_from_u8, + crate::range::RangeFrom, + u8, + crate::range::RangeFrom { start: kani::any() } + ); + check_get_unchecked_contract!( + check_get_unchecked_range_full_u8, + check_get_unchecked_mut_range_full_u8, + crate::ops::RangeFull, + u8, + .. + ); + check_get_unchecked_contract!( + check_get_unchecked_range_inclusive_u8, + check_get_unchecked_mut_range_inclusive_u8, + crate::ops::RangeInclusive, + u8, + any_range_inclusive() + ); + check_get_unchecked_contract!( + check_get_unchecked_new_range_inclusive_u8, + check_get_unchecked_mut_new_range_inclusive_u8, + crate::range::RangeInclusive, + u8, + crate::range::RangeInclusive { start: kani::any(), last: kani::any() } + ); + check_get_unchecked_contract!( + check_get_unchecked_range_to_inclusive_u8, + check_get_unchecked_mut_range_to_inclusive_u8, + crate::ops::RangeToInclusive, + u8, + ..=kani::any::() + ); + check_get_unchecked_contract!( + check_get_unchecked_new_range_to_inclusive_u8, + check_get_unchecked_mut_new_range_to_inclusive_u8, + crate::range::RangeToInclusive, + u8, + crate::range::RangeToInclusive { last: kani::any() } + ); + check_get_unchecked_contract!( + check_get_unchecked_bound_pair_u8, + check_get_unchecked_mut_bound_pair_u8, + (Bound, Bound), + u8, + (any_bound(), any_bound()) ); // ---- as_chunks_unchecked / as_chunks_unchecked_mut ---- @@ -5698,48 +5813,96 @@ mod verify { check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_char_3, char, 3); // ---- get_disjoint_unchecked_mut ---- - // Generic over the index type `I` and const `N`, with a two-part precondition: - // every index in bounds AND the indices pairwise disjoint. As with get_unchecked - // (index-type-specific, non-contractable over generic `I`), we prove no-UB at - // concrete `I = usize` and small `N` with the obligation set by `kani::assume` - // (each `idx < len`; pairwise distinct). The body loops `0..N` with concrete `N`, - // so the loop bound is concrete and needs no `#[kani::unwind]`. - - #[kani::proof] + // Generic over the index type `I` and const `N`, with a two-part safety + // precondition: every index in bounds AND the indices pairwise disjoint. + // `get_disjoint_check_valid` (the checker the safe `get_disjoint_mut` + // gates on) is exactly that predicate over the `GetDisjointMutIndex` + // methods, so it is the fn-level `#[requires]` contract, and these + // harnesses verify it per concrete `I` and `N`: element indices (`usize`) + // plus all four `GetDisjointMutIndex` range impls (`ops` and `core::range` + // flavors of `Range` and `RangeInclusive`; `RangeInclusive` inputs include + // iteration-exhausted values via `any_range_inclusive`). The body loops + // `0..N` with concrete `N`, so the loop bound is concrete and needs no + // `#[kani::unwind]`. + + #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut::)] fn check_get_disjoint_unchecked_mut_2_u8() { const ARR_SIZE: usize = 100; let mut arr: [u8; ARR_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array_mut(&mut arr); - let i0: usize = kani::any(); - let i1: usize = kani::any(); - kani::assume(i0 < slice.len() && i1 < slice.len()); - kani::assume(i0 != i1); - let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1]) }; + let indices: [usize; 2] = kani::any(); + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; } - #[kani::proof] + #[kani::proof_for_contract(<[u64]>::get_disjoint_unchecked_mut::)] fn check_get_disjoint_unchecked_mut_2_u64() { const ARR_SIZE: usize = 100; let mut arr: [u64; ARR_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array_mut(&mut arr); - let i0: usize = kani::any(); - let i1: usize = kani::any(); - kani::assume(i0 < slice.len() && i1 < slice.len()); - kani::assume(i0 != i1); - let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1]) }; + let indices: [usize; 2] = kani::any(); + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; } - #[kani::proof] + #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut::)] fn check_get_disjoint_unchecked_mut_3_u8() { const ARR_SIZE: usize = 100; let mut arr: [u8; ARR_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array_mut(&mut arr); - let i0: usize = kani::any(); - let i1: usize = kani::any(); - let i2: usize = kani::any(); - kani::assume(i0 < slice.len() && i1 < slice.len() && i2 < slice.len()); - kani::assume(i0 != i1 && i0 != i2 && i1 != i2); - let _ = unsafe { slice.get_disjoint_unchecked_mut([i0, i1, i2]) }; + let indices: [usize; 3] = kani::any(); + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; + } + + #[kani::proof_for_contract( + <[u8]>::get_disjoint_unchecked_mut::, 2> + )] + fn check_get_disjoint_unchecked_mut_2_range_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let indices = [ + kani::any::()..kani::any::(), + kani::any::()..kani::any::(), + ]; + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; + } + + #[kani::proof_for_contract( + <[u8]>::get_disjoint_unchecked_mut::, 2> + )] + fn check_get_disjoint_unchecked_mut_2_range_inclusive_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let indices = [any_range_inclusive(), any_range_inclusive()]; + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; + } + + #[kani::proof_for_contract( + <[u8]>::get_disjoint_unchecked_mut::, 2> + )] + fn check_get_disjoint_unchecked_mut_2_new_range_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let indices = [ + crate::range::Range { start: kani::any(), end: kani::any() }, + crate::range::Range { start: kani::any(), end: kani::any() }, + ]; + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; + } + + #[kani::proof_for_contract( + <[u8]>::get_disjoint_unchecked_mut::, 2> + )] + fn check_get_disjoint_unchecked_mut_2_new_range_inclusive_u8() { + const ARR_SIZE: usize = 100; + let mut arr: [u8; ARR_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut arr); + let indices = [ + crate::range::RangeInclusive { start: kani::any(), last: kani::any() }, + crate::range::RangeInclusive { start: kani::any(), last: kani::any() }, + ]; + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; } // ---- Safe chunk accessors (first/last/split_first/split_last _chunk) ----