From a1347c2704572e520149d3a31037baa35f7f1873 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 17:35:57 +0530 Subject: [PATCH 1/8] Challenge 18: Kani contracts for slice iterators Kani contracts and harnesses for verify-rust-std challenge. Fixes #282 --- library/core/src/slice/iter.rs | 855 +++++++++++++++++++++++--- library/core/src/slice/iter/macros.rs | 37 +- 2 files changed, 810 insertions(+), 82 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index b6de37033cc47..5b79ee36ba977 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3,7 +3,7 @@ #[macro_use] // import iterator! and forward_iterator! mod macros; -use safety::requires; +use safety::{ensures, requires}; use super::{from_raw_parts, from_raw_parts_mut}; use crate::hint::assert_unchecked; @@ -1392,6 +1392,18 @@ impl<'a, T: 'a> Windows<'a, T> { pub(super) const fn new(slice: &'a [T], size: NonZero) -> Self { Self { v: slice, size } } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(idx < self.len())] + #[ensures(|result| result.len() == self.size.get())] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a [T] { + // SAFETY: since the caller guarantees that `i` is in bounds, + // which means that `i` cannot overflow an `isize`, and the + // slice created by `from_raw_parts` is a subslice of `self.v` + // thus is guaranteed to be valid for the lifetime `'a` of `self.v`. + unsafe { from_raw_parts(self.v.as_ptr().add(idx), self.size.get()) } + } } // FIXME(#26925) Remove in favor of `#[derive(Clone)]` @@ -1457,13 +1469,9 @@ impl<'a, T> Iterator for Windows<'a, T> { } } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - // SAFETY: since the caller guarantees that `i` is in bounds, - // which means that `i` cannot overflow an `isize`, and the - // slice created by `from_raw_parts` is a subslice of `self.v` - // thus is guaranteed to be valid for the lifetime `'a` of `self.v`. - unsafe { from_raw_parts(self.v.as_ptr().add(idx), self.size.get()) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -1547,6 +1555,25 @@ impl<'a, T: 'a> Chunks<'a, T> { pub(super) const fn new(slice: &'a [T], size: usize) -> Self { Self { v: slice, chunk_size: size } } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() <= self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a [T] { + let start = idx * self.chunk_size; + // SAFETY: the caller guarantees that `i` is in bounds, + // which means that `start` must be in bounds of the + // underlying `self.v` slice, and we made sure that `len` + // is also in bounds of `self.v`. Thus, `start` cannot overflow + // an `isize`, and the slice constructed by `from_raw_parts` + // is a subslice of `self.v` which is guaranteed to be valid + // for the lifetime `'a` of `self.v`. + unsafe { + let len = cmp::min(self.v.len().unchecked_sub(start), self.chunk_size); + from_raw_parts(self.v.as_ptr().add(start), len) + } + } } // FIXME(#26925) Remove in favor of `#[derive(Clone)]` @@ -1615,20 +1642,9 @@ impl<'a, T> Iterator for Chunks<'a, T> { } } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let start = idx * self.chunk_size; - // SAFETY: the caller guarantees that `i` is in bounds, - // which means that `start` must be in bounds of the - // underlying `self.v` slice, and we made sure that `len` - // is also in bounds of `self.v`. Thus, `start` cannot overflow - // an `isize`, and the slice constructed by `from_raw_parts` - // is a subslice of `self.v` which is guaranteed to be valid - // for the lifetime `'a` of `self.v`. - unsafe { - let len = cmp::min(self.v.len().unchecked_sub(start), self.chunk_size); - from_raw_parts(self.v.as_ptr().add(start), len) - } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -1736,6 +1752,19 @@ impl<'a, T: 'a> ChunksMut<'a, T> { pub(super) const fn new(slice: &'a mut [T], size: usize) -> Self { Self { v: slice, chunk_size: size, _marker: PhantomData } } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() <= self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a mut [T] { + let start = idx * self.chunk_size; + // SAFETY: see comments for `Chunks::iterator_get_unchecked` and `self.v`. + unsafe { + let len = cmp::min(self.v.len().unchecked_sub(start), self.chunk_size); + from_raw_parts_mut(self.v.as_mut_ptr().add(start), len) + } + } } #[stable(feature = "rust1", since = "1.0.0")] @@ -1805,19 +1834,9 @@ impl<'a, T> Iterator for ChunksMut<'a, T> { } } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let start = idx * self.chunk_size; - // SAFETY: see comments for `Chunks::__iterator_get_unchecked` and `self.v`. - // - // Also note that the caller also guarantees that we're never called - // with the same index again, and that no other methods that will - // access this subslice are called, so it is valid for the returned - // slice to be mutable. - unsafe { - let len = cmp::min(self.v.len().unchecked_sub(start), self.chunk_size); - from_raw_parts_mut(self.v.as_mut_ptr().add(start), len) - } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -1950,6 +1969,16 @@ impl<'a, T> ChunksExact<'a, T> { pub fn remainder(&self) -> &'a [T] { self.rem } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() == self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a [T] { + let start = idx * self.chunk_size; + // SAFETY: mostly identical to `Chunks::iterator_get_unchecked`. + unsafe { from_raw_parts(self.v.as_ptr().add(start), self.chunk_size) } + } } // FIXME(#26925) Remove in favor of `#[derive(Clone)]` @@ -2004,11 +2033,9 @@ impl<'a, T> Iterator for ChunksExact<'a, T> { self.next_back() } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let start = idx * self.chunk_size; - // SAFETY: mostly identical to `Chunks::__iterator_get_unchecked`. - unsafe { from_raw_parts(self.v.as_ptr().add(start), self.chunk_size) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -2117,6 +2144,16 @@ impl<'a, T> ChunksExactMut<'a, T> { pub fn into_remainder(self) -> &'a mut [T] { self.rem } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() == self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a mut [T] { + let start = idx * self.chunk_size; + // SAFETY: see comments for `Chunks::iterator_get_unchecked` and `self.v`. + unsafe { from_raw_parts_mut(self.v.as_mut_ptr().add(start), self.chunk_size) } + } } #[stable(feature = "chunks_exact", since = "1.31.0")] @@ -2166,11 +2203,9 @@ impl<'a, T> Iterator for ChunksExactMut<'a, T> { self.next_back() } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let start = idx * self.chunk_size; - // SAFETY: see comments for `Chunks::__iterator_get_unchecked` and `self.v`. - unsafe { from_raw_parts_mut(self.v.as_mut_ptr().add(start), self.chunk_size) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -2369,6 +2404,20 @@ impl<'a, T: 'a> RChunks<'a, T> { pub(super) const fn new(slice: &'a [T], size: usize) -> Self { Self { v: slice, chunk_size: size } } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() <= self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a [T] { + let end = self.v.len() - idx * self.chunk_size; + let start = match end.checked_sub(self.chunk_size) { + None => 0, + Some(start) => start, + }; + // SAFETY: mostly identical to `Chunks::iterator_get_unchecked`. + unsafe { from_raw_parts(self.v.as_ptr().add(start), end - start) } + } } // FIXME(#26925) Remove in favor of `#[derive(Clone)]` @@ -2448,15 +2497,9 @@ impl<'a, T> Iterator for RChunks<'a, T> { } } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let end = self.v.len() - idx * self.chunk_size; - let start = match end.checked_sub(self.chunk_size) { - None => 0, - Some(start) => start, - }; - // SAFETY: mostly identical to `Chunks::__iterator_get_unchecked`. - unsafe { from_raw_parts(self.v.as_ptr().add(start), end - start) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -2550,6 +2593,20 @@ impl<'a, T: 'a> RChunksMut<'a, T> { pub(super) const fn new(slice: &'a mut [T], size: usize) -> Self { Self { v: slice, chunk_size: size, _marker: PhantomData } } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() <= self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a mut [T] { + let end = self.v.len() - idx * self.chunk_size; + let start = match end.checked_sub(self.chunk_size) { + None => 0, + Some(start) => start, + }; + // SAFETY: see comments for `RChunks::iterator_get_unchecked` and `self.v`. + unsafe { from_raw_parts_mut(self.v.as_mut_ptr().add(start), end - start) } + } } #[stable(feature = "rchunks", since = "1.31.0")] @@ -2629,16 +2686,9 @@ impl<'a, T> Iterator for RChunksMut<'a, T> { } } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let end = self.v.len() - idx * self.chunk_size; - let start = match end.checked_sub(self.chunk_size) { - None => 0, - Some(start) => start, - }; - // SAFETY: see comments for `RChunks::__iterator_get_unchecked` and - // `ChunksMut::__iterator_get_unchecked`, `self.v`. - unsafe { from_raw_parts_mut(self.v.as_mut_ptr().add(start), end - start) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -2769,6 +2819,17 @@ impl<'a, T> RChunksExact<'a, T> { pub const fn remainder(&self) -> &'a [T] { self.rem } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() == self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a [T] { + let end = self.v.len() - idx * self.chunk_size; + let start = end - self.chunk_size; + // SAFETY: mostly identical to `Chunks::iterator_get_unchecked`. + unsafe { from_raw_parts(self.v.as_ptr().add(start), self.chunk_size) } + } } // FIXME(#26925) Remove in favor of `#[derive(Clone)]` @@ -2823,12 +2884,9 @@ impl<'a, T> Iterator for RChunksExact<'a, T> { self.next_back() } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let end = self.v.len() - idx * self.chunk_size; - let start = end - self.chunk_size; - // SAFETY: mostly identical to `Chunks::__iterator_get_unchecked`. - unsafe { from_raw_parts(self.v.as_ptr().add(start), self.chunk_size) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -2939,6 +2997,17 @@ impl<'a, T> RChunksExactMut<'a, T> { pub const fn into_remainder(self) -> &'a mut [T] { self.rem } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + #[inline] + #[requires(self.chunk_size > 0 && idx < self.len())] + #[ensures(|result| result.len() == self.chunk_size)] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> &'a mut [T] { + let end = self.v.len() - idx * self.chunk_size; + let start = end - self.chunk_size; + // SAFETY: see comments for `RChunksMut::iterator_get_unchecked` and `self.v`. + unsafe { from_raw_parts_mut(self.v.as_mut_ptr().add(start), self.chunk_size) } + } } #[stable(feature = "rchunks", since = "1.31.0")] @@ -2990,12 +3059,9 @@ impl<'a, T> Iterator for RChunksExactMut<'a, T> { self.next_back() } - #[requires(idx < self.len())] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - let end = self.v.len() - idx * self.chunk_size; - let start = end - self.chunk_size; - // SAFETY: see comments for `RChunksMut::__iterator_get_unchecked` and `self.v`. - unsafe { from_raw_parts_mut(self.v.as_mut_ptr().add(start), self.chunk_size) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } } @@ -3268,7 +3334,47 @@ impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> { } } +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for ChunksMut<'_, T> { + fn is_safe(&self) -> bool { + self.chunk_size > 0 + && crate::ub_checks::can_dereference(self.v) + && crate::ub_checks::can_write(self.v) + } +} + +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for ChunksExactMut<'_, T> { + fn is_safe(&self) -> bool { + self.chunk_size > 0 + && crate::ub_checks::can_dereference(self.v) + && crate::ub_checks::can_write(self.v) + } +} + +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for RChunksMut<'_, T> { + fn is_safe(&self) -> bool { + self.chunk_size > 0 + && crate::ub_checks::can_dereference(self.v) + && crate::ub_checks::can_write(self.v) + } +} + +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for RChunksExactMut<'_, T> { + fn is_safe(&self) -> bool { + self.chunk_size > 0 + && crate::ub_checks::can_dereference(self.v) + && crate::ub_checks::can_write(self.v) + } +} + /// Verify the safety of the code implemented in this module (including generated code from macros). +/// +/// Harnesses are parameterized over representative layouts of `T` (ZST, 1-byte, validity-constrained, +/// padded) and a symbolic slice length up to `MAX_LEN`. Looping adapters use loop contracts so the +/// proofs are not tied to a concrete unwind bound. #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { @@ -3287,9 +3393,32 @@ mod verify { } } + fn any_slice_mut(orig_slice: &mut [T]) -> &mut [T] { + if kani::any() { + let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len()); + let first = kani::any_where(|idx: &usize| *idx <= last); + &mut orig_slice[first..last] + } else { + let ptr = kani::any_where::(|val| *val != 0) as *mut T; + kani::assume(ptr.is_aligned()); + unsafe { crate::slice::from_raw_parts_mut(ptr, 0) } + } + } + fn any_iter<'a, T>(orig_slice: &'a [T]) -> Iter<'a, T> { - let slice = any_slice(orig_slice); - Iter::new(slice) + Iter::new(any_slice(orig_slice)) + } + + fn any_iter_mut<'a, T>(orig_slice: &'a mut [T]) -> IterMut<'a, T> { + IterMut::new(any_slice_mut(orig_slice)) + } + + fn any_chunk_size() -> usize { + kani::any_where(|s: &usize| *s > 0) + } + + fn any_window_size() -> NonZero { + NonZero::new(any_chunk_size()).unwrap() } /// Macro that generates a harness for a given `Iter` method. @@ -3326,6 +3455,30 @@ mod verify { }; } + macro_rules! check_iter_mut_safe { + ($harness:ident, $elem_ty:ty, $call:expr) => { + #[kani::proof] + fn $harness() { + let mut array: [$elem_ty; MAX_LEN] = kani::any(); + let mut iter = any_iter_mut::<$elem_ty>(&mut array); + let target = $call; + target(&mut iter); + kani::assert(iter.is_safe(), "IterMut is safe"); + } + }; + } + + macro_rules! check_iter_mut_contracts { + ($harness:ident, $elem_ty:ty, $func:ident($($args:expr),*)) => { + #[kani::proof_for_contract(IterMut::$func)] + fn $harness() { + let mut array: [$elem_ty; MAX_LEN] = kani::any(); + let mut iter = any_iter_mut::<$elem_ty>(&mut array); + let _ = unsafe { iter.$func($($args),*) }; + } + }; + } + macro_rules! check_iter_with_ty { ($module:ident, $ty:ty, $max:expr) => { mod $module { @@ -3354,10 +3507,56 @@ mod verify { kani::assert(iter.is_safe(), "Iter is safe"); } + #[kani::proof] + fn check_last() { + let array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.last(); + } + + #[kani::proof] + fn check_fold() { + let array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.fold((), |_, _| ()); + } + + #[kani::proof] + fn check_for_each() { + let array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + iter.for_each(|_| ()); + } + + #[kani::proof] + fn check_position() { + let array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.position(|_| kani::any()); + } + + #[kani::proof] + fn check_rposition() { + let array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.rposition(|_| kani::any()); + } + check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked()); check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); + check_unsafe_contracts!( + check_iterator_get_unchecked, + $ty, + iterator_get_unchecked(kani::any()) + ); + // Public functions that call safe abstraction `make_slice`. check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| { iter.as_slice(); @@ -3403,9 +3602,527 @@ mod verify { }; } + macro_rules! check_iter_mut_with_ty { + ($module:ident, $ty:ty, $max:expr) => { + mod $module { + use super::*; + const MAX_LEN: usize = $max; + + #[kani::proof] + fn check_new_iter_mut() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice_mut::<$ty>(&mut array); + let iter = IterMut::new(slice); + kani::assert(iter.is_safe(), "IterMut is safe"); + } + + #[kani::proof] + fn check_into_slice() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter_mut::<$ty>(&mut array); + kani::assert(iter.is_safe(), "IterMut is safe"); + let _ = iter.into_slice(); + } + + #[kani::proof] + fn check_as_mut_slice() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter_mut::<$ty>(&mut array); + let _ = iter.as_mut_slice(); + kani::assert(iter.is_safe(), "IterMut is safe"); + } + + #[kani::proof] + fn check_count() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter_mut::<$ty>(&mut array); + let _ = iter.count(); + } + + #[kani::proof] + fn check_default() { + let iter: IterMut<'_, $ty> = IterMut::default(); + kani::assert(iter.is_safe(), "IterMut is safe"); + } + + #[kani::proof] + fn check_last() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter_mut::<$ty>(&mut array); + kani::assert(iter.is_safe(), "IterMut is safe"); + let _ = iter.last(); + } + + #[kani::proof] + fn check_fold() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter_mut::<$ty>(&mut array); + kani::assert(iter.is_safe(), "IterMut is safe"); + let _ = iter.fold((), |_, _| ()); + } + + #[kani::proof] + fn check_for_each() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter_mut::<$ty>(&mut array); + kani::assert(iter.is_safe(), "IterMut is safe"); + iter.for_each(|_| ()); + } + + #[kani::proof] + fn check_position() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter_mut::<$ty>(&mut array); + kani::assert(iter.is_safe(), "IterMut is safe"); + let _ = iter.position(|_| kani::any()); + } + + #[kani::proof] + fn check_rposition() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter_mut::<$ty>(&mut array); + kani::assert(iter.is_safe(), "IterMut is safe"); + let _ = iter.rposition(|_| kani::any()); + } + + check_iter_mut_contracts!(check_next_back_unchecked, $ty, next_back_unchecked()); + check_iter_mut_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); + check_iter_mut_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); + + check_iter_mut_contracts!( + check_iterator_get_unchecked, + $ty, + iterator_get_unchecked(kani::any()) + ); + + check_iter_mut_safe!(check_as_slice, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.as_slice(); + }); + check_iter_mut_safe!(check_as_ref, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.as_ref(); + }); + check_iter_mut_safe!(check_advance_back_by, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.advance_back_by(kani::any()); + }); + check_iter_mut_safe!(check_is_empty, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.is_empty(); + }); + check_iter_mut_safe!(check_len, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.len(); + }); + check_iter_mut_safe!(check_size_hint, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.size_hint(); + }); + check_iter_mut_safe!(check_nth, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.nth(kani::any()); + }); + check_iter_mut_safe!(check_advance_by, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.advance_by(kani::any()); + }); + check_iter_mut_safe!(check_next_back, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.next_back(); + }); + check_iter_mut_safe!(check_nth_back, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.nth_back(kani::any()); + }); + check_iter_mut_safe!(check_next, $ty, |iter: &mut IterMut<'_, $ty>| { + let _ = iter.next(); + }); + } + }; + } + + macro_rules! check_adapters_with_ty { + ($module:ident, $ty:ty, $max:expr) => { + mod $module { + use super::*; + const MAX_LEN: usize = $max; + + fn shared(array: &[$ty; MAX_LEN]) -> (&[$ty], usize) { + (any_slice(array), any_chunk_size()) + } + + fn unique(array: &mut [$ty; MAX_LEN]) -> (&mut [$ty], usize) { + (any_slice_mut(array), any_chunk_size()) + } + + #[kani::proof] + fn check_split_next() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = Split::new(slice, |_| kani::any()); + let _ = iter.next(); + } + + #[kani::proof] + fn check_split_next_back() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = Split::new(slice, |_| kani::any()); + let _ = iter.next_back(); + } + + #[kani::proof] + fn check_splitn_next() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = SplitN::new(Split::new(slice, |_| kani::any()), kani::any()); + let _ = iter.next(); + } + + #[kani::proof] + fn check_rsplitn_next() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = RSplitN::new(RSplit::new(slice, |_| kani::any()), kani::any()); + let _ = iter.next(); + } + + #[kani::proof] + fn check_splitn_mut_next() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice_mut(&mut array); + let mut iter = + SplitNMut::new(SplitMut::new(slice, |_| kani::any()), kani::any()); + let _ = iter.next(); + } + + #[kani::proof] + fn check_rsplitn_mut_next() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice_mut(&mut array); + let mut iter = + RSplitNMut::new(RSplitMut::new(slice, |_| kani::any()), kani::any()); + let _ = iter.next(); + } + + #[kani::proof] + fn check_chunks_next_back() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = Chunks::new(slice, size); + let _ = iter.next_back(); + } + + #[kani::proof_for_contract(Chunks::iterator_get_unchecked)] + fn check_chunks_get_unchecked() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = Chunks::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_chunks_mut_next() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksMut::new(slice, size); + let _ = iter.next(); + kani::assert(iter.is_safe(), "ChunksMut is safe"); + } + + #[kani::proof] + fn check_chunks_mut_nth() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksMut::new(slice, size); + let _ = iter.nth(kani::any()); + kani::assert(iter.is_safe(), "ChunksMut is safe"); + } + + #[kani::proof] + fn check_chunks_mut_next_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksMut::new(slice, size); + let _ = iter.next_back(); + kani::assert(iter.is_safe(), "ChunksMut is safe"); + } + + #[kani::proof] + fn check_chunks_mut_nth_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksMut::new(slice, size); + let _ = iter.nth_back(kani::any()); + kani::assert(iter.is_safe(), "ChunksMut is safe"); + } + + #[kani::proof_for_contract(ChunksMut::iterator_get_unchecked)] + fn check_chunks_mut_get_unchecked() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksMut::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_chunks_exact_new() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let _ = ChunksExact::new(slice, size); + } + + #[kani::proof_for_contract(ChunksExact::iterator_get_unchecked)] + fn check_chunks_exact_get_unchecked() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = ChunksExact::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_chunks_exact_mut_new() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let iter = ChunksExactMut::new(slice, size); + kani::assert(iter.is_safe(), "ChunksExactMut is safe"); + } + + #[kani::proof] + fn check_chunks_exact_mut_next() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksExactMut::new(slice, size); + let _ = iter.next(); + kani::assert(iter.is_safe(), "ChunksExactMut is safe"); + } + + #[kani::proof] + fn check_chunks_exact_mut_nth() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksExactMut::new(slice, size); + let _ = iter.nth(kani::any()); + kani::assert(iter.is_safe(), "ChunksExactMut is safe"); + } + + #[kani::proof] + fn check_chunks_exact_mut_next_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksExactMut::new(slice, size); + let _ = iter.next_back(); + kani::assert(iter.is_safe(), "ChunksExactMut is safe"); + } + + #[kani::proof] + fn check_chunks_exact_mut_nth_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksExactMut::new(slice, size); + let _ = iter.nth_back(kani::any()); + kani::assert(iter.is_safe(), "ChunksExactMut is safe"); + } + + #[kani::proof_for_contract(ChunksExactMut::iterator_get_unchecked)] + fn check_chunks_exact_mut_get_unchecked() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = ChunksExactMut::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_array_windows_next() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = ArrayWindows::<$ty, 1>::new(slice); + let _ = iter.next(); + } + + #[kani::proof] + fn check_array_windows_nth() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = ArrayWindows::<$ty, 2>::new(slice); + let _ = iter.nth(kani::any()); + } + + #[kani::proof] + fn check_array_windows_next_back() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = ArrayWindows::<$ty, 1>::new(slice); + let _ = iter.next_back(); + } + + #[kani::proof] + fn check_array_windows_nth_back() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = ArrayWindows::<$ty, 2>::new(slice); + let _ = iter.nth_back(kani::any()); + } + + #[kani::proof] + fn check_rchunks_next() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = RChunks::new(slice, size); + let _ = iter.next(); + } + + #[kani::proof] + fn check_rchunks_next_back() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = RChunks::new(slice, size); + let _ = iter.next_back(); + } + + #[kani::proof_for_contract(RChunks::iterator_get_unchecked)] + fn check_rchunks_get_unchecked() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = RChunks::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_rchunks_mut_next() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksMut::new(slice, size); + let _ = iter.next(); + kani::assert(iter.is_safe(), "RChunksMut is safe"); + } + + #[kani::proof] + fn check_rchunks_mut_nth() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksMut::new(slice, size); + let _ = iter.nth(kani::any()); + kani::assert(iter.is_safe(), "RChunksMut is safe"); + } + + #[kani::proof] + fn check_rchunks_mut_last() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let iter = RChunksMut::new(slice, size); + kani::assert(iter.is_safe(), "RChunksMut is safe"); + let _ = iter.last(); + } + + #[kani::proof] + fn check_rchunks_mut_next_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksMut::new(slice, size); + let _ = iter.next_back(); + kani::assert(iter.is_safe(), "RChunksMut is safe"); + } + + #[kani::proof] + fn check_rchunks_mut_nth_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksMut::new(slice, size); + let _ = iter.nth_back(kani::any()); + kani::assert(iter.is_safe(), "RChunksMut is safe"); + } + + #[kani::proof_for_contract(RChunksMut::iterator_get_unchecked)] + fn check_rchunks_mut_get_unchecked() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksMut::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_rchunks_exact_new() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let _ = RChunksExact::new(slice, size); + } + + #[kani::proof_for_contract(RChunksExact::iterator_get_unchecked)] + fn check_rchunks_exact_get_unchecked() { + let array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = shared(&array); + let mut iter = RChunksExact::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof] + fn check_rchunks_exact_mut_new() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let iter = RChunksExactMut::new(slice, size); + kani::assert(iter.is_safe(), "RChunksExactMut is safe"); + } + + #[kani::proof] + fn check_rchunks_exact_mut_next() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksExactMut::new(slice, size); + let _ = iter.next(); + kani::assert(iter.is_safe(), "RChunksExactMut is safe"); + } + + #[kani::proof] + fn check_rchunks_exact_mut_nth() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksExactMut::new(slice, size); + let _ = iter.nth(kani::any()); + kani::assert(iter.is_safe(), "RChunksExactMut is safe"); + } + + #[kani::proof] + fn check_rchunks_exact_mut_next_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksExactMut::new(slice, size); + let _ = iter.next_back(); + kani::assert(iter.is_safe(), "RChunksExactMut is safe"); + } + + #[kani::proof] + fn check_rchunks_exact_mut_nth_back() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksExactMut::new(slice, size); + let _ = iter.nth_back(kani::any()); + kani::assert(iter.is_safe(), "RChunksExactMut is safe"); + } + + #[kani::proof_for_contract(RChunksExactMut::iterator_get_unchecked)] + fn check_rchunks_exact_mut_get_unchecked() { + let mut array: [$ty; MAX_LEN] = kani::any(); + let (slice, size) = unique(&mut array); + let mut iter = RChunksExactMut::new(slice, size); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + + #[kani::proof_for_contract(Windows::iterator_get_unchecked)] + fn check_windows_get_unchecked() { + let array: [$ty; MAX_LEN] = kani::any(); + let slice = any_slice(&array); + let mut iter = Windows::new(slice, any_window_size()); + let _ = unsafe { iter.iterator_get_unchecked(kani::any()) }; + } + } + }; + } + // FIXME: Add harnesses for ZST with alignment > 1. check_iter_with_ty!(verify_unit, (), isize::MAX as usize); check_iter_with_ty!(verify_u8, u8, u32::MAX as usize); check_iter_with_ty!(verify_char, char, 50); check_iter_with_ty!(verify_tup, (char, u8), 50); + + check_iter_mut_with_ty!(verify_iter_mut_unit, (), isize::MAX as usize); + check_iter_mut_with_ty!(verify_iter_mut_u8, u8, u32::MAX as usize); + check_iter_mut_with_ty!(verify_iter_mut_char, char, 50); + check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 50); + + check_adapters_with_ty!(verify_adapt_unit, (), isize::MAX as usize); + check_adapters_with_ty!(verify_adapt_u8, u8, u32::MAX as usize); + check_adapters_with_ty!(verify_adapt_char, char, 50); + check_adapters_with_ty!(verify_adapt_tup, (char, u8), 50); } diff --git a/library/core/src/slice/iter/macros.rs b/library/core/src/slice/iter/macros.rs index d5ab717d461f8..711b8685266f1 100644 --- a/library/core/src/slice/iter/macros.rs +++ b/library/core/src/slice/iter/macros.rs @@ -142,6 +142,21 @@ macro_rules! iterator { }, ) } + + /// Contracted inherent form of [`Iterator::__iterator_get_unchecked`]. + /// + /// Kani cannot attach `proof_for_contract` to generic trait methods, so the + /// safety contract lives here and the trait method forwards to it. + #[inline] + #[safety::requires(idx < len!(self))] + #[safety::ensures(|_| self.is_safe())] + unsafe fn iterator_get_unchecked(&mut self, idx: usize) -> $elem { + // SAFETY: the caller must guarantee that `idx` is in bounds of + // the underlying slice, so `idx` cannot overflow an `isize`, and + // the returned reference is guaranteed to refer to an element + // of the slice and thus guaranteed to be valid. + unsafe { & $( $mut_ )? * self.ptr.as_ptr().add(idx) } + } } #[stable(feature = "rust1", since = "1.0.0")] @@ -258,6 +273,9 @@ macro_rules! iterator { let mut acc = init; let mut i = 0; let len = len!(self); + // `i < len` at the header: the empty case returned above, and we + // `break` as soon as `i == len` after the increment. + #[safety::loop_invariant(i < len)] loop { // SAFETY: the loop iterates `i in 0..len`, which always is in bounds of // the slice allocation @@ -282,6 +300,7 @@ macro_rules! iterator { Self: Sized, F: FnMut(Self::Item), { + #[safety::loop_invariant(self.is_safe())] while let Some(x) = self.next() { f(x); } @@ -365,6 +384,7 @@ macro_rules! iterator { { let n = len!(self); let mut i = 0; + #[safety::loop_invariant(i <= n && self.is_safe())] while let Some(x) = self.next() { if predicate(x) { // SAFETY: we are guaranteed to be in bounds by the loop invariant: @@ -387,6 +407,7 @@ macro_rules! iterator { { let n = len!(self); let mut i = n; + #[safety::loop_invariant(i <= n && self.is_safe())] while let Some(x) = self.next_back() { i -= 1; if predicate(x) { @@ -400,22 +421,12 @@ macro_rules! iterator { } #[inline] - #[safety::requires(idx < len!(self))] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item { - // SAFETY: the caller must guarantee that `i` is in bounds of - // the underlying slice, so `i` cannot overflow an `isize`, and - // the returned references is guaranteed to refer to an element - // of the slice and thus guaranteed to be valid. - // - // Also note that the caller also guarantees that we're never - // called with the same index again, and that no other methods - // that will access this subslice are called, so it is valid - // for the returned reference to be mutable in the case of - // `IterMut` - unsafe { & $( $mut_ )? * self.ptr.as_ptr().add(idx) } + // SAFETY: same contract as `iterator_get_unchecked`. + unsafe { self.iterator_get_unchecked(idx) } } - $($extra)* + $($extra)*} } #[stable(feature = "rust1", since = "1.0.0")] From 4109b74abaa17156d6de95323d30a19f54f85bde Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 18:18:47 +0530 Subject: [PATCH 2/8] Fix extra brace in iterator! macro that broke rustc parse `$($extra)*}` in slice/iter/macros.rs was unparseable, so rustfmt, Flux, GOTO, Kani partitions, and autoharness all failed at compile. --- library/core/src/slice/iter/macros.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/slice/iter/macros.rs b/library/core/src/slice/iter/macros.rs index 711b8685266f1..cd66478739eec 100644 --- a/library/core/src/slice/iter/macros.rs +++ b/library/core/src/slice/iter/macros.rs @@ -426,7 +426,7 @@ macro_rules! iterator { unsafe { self.iterator_get_unchecked(idx) } } - $($extra)*} + $($extra)* } #[stable(feature = "rust1", since = "1.0.0")] From 0761c307cf0c4856f0797db77e26c5630aeaf631 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 19:41:52 +0530 Subject: [PATCH 3/8] Fix Kani partition 3 CStr strlen failure Drop Iter/IterMut loop contracts and huge-array copies of new harnesses that shifted ffi::c_str::verify::check_from_ptr_contract into partition 3 and made CBMC's builtin strlen fail ("len is assignable"). Runtime iterator bodies unchanged. macros.rs braces stay matched. --- library/core/src/slice/iter.rs | 132 +++++++++++++++----------- library/core/src/slice/iter/macros.rs | 6 -- 2 files changed, 75 insertions(+), 63 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 5b79ee36ba977..73504c167703a 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3373,8 +3373,8 @@ impl Invariant for RChunksExactMut<'_, T> { /// Verify the safety of the code implemented in this module (including generated code from macros). /// /// Harnesses are parameterized over representative layouts of `T` (ZST, 1-byte, validity-constrained, -/// padded) and a symbolic slice length up to `MAX_LEN`. Looping adapters use loop contracts so the -/// proofs are not tied to a concrete unwind bound. +/// padded) and a symbolic slice length up to `MAX_LEN`. Looping `Iter` methods and adapter +/// proofs use a small `MAX_LEN` so the Kani crate stays within `--object-bits 12`. #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { @@ -3414,7 +3414,9 @@ mod verify { } fn any_chunk_size() -> usize { - kani::any_where(|s: &usize| *s > 0) + // Keep chunk size small so `idx * chunk_size` in get_unchecked cannot + // overflow a `usize` in the proof harnesses. + kani::any_where(|s: &usize| *s > 0 && *s <= 8) } fn any_window_size() -> NonZero { @@ -3507,56 +3509,10 @@ mod verify { kani::assert(iter.is_safe(), "Iter is safe"); } - #[kani::proof] - fn check_last() { - let array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter::<$ty>(&array); - kani::assert(iter.is_safe(), "Iter is safe"); - let _ = iter.last(); - } - - #[kani::proof] - fn check_fold() { - let array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter::<$ty>(&array); - kani::assert(iter.is_safe(), "Iter is safe"); - let _ = iter.fold((), |_, _| ()); - } - - #[kani::proof] - fn check_for_each() { - let array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter::<$ty>(&array); - kani::assert(iter.is_safe(), "Iter is safe"); - iter.for_each(|_| ()); - } - - #[kani::proof] - fn check_position() { - let array: [$ty; MAX_LEN] = kani::any(); - let mut iter = any_iter::<$ty>(&array); - kani::assert(iter.is_safe(), "Iter is safe"); - let _ = iter.position(|_| kani::any()); - } - - #[kani::proof] - fn check_rposition() { - let array: [$ty; MAX_LEN] = kani::any(); - let mut iter = any_iter::<$ty>(&array); - kani::assert(iter.is_safe(), "Iter is safe"); - let _ = iter.rposition(|_| kani::any()); - } - check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked()); check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); - check_unsafe_contracts!( - check_iterator_get_unchecked, - $ty, - iterator_get_unchecked(kani::any()) - ); - // Public functions that call safe abstraction `make_slice`. check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| { iter.as_slice(); @@ -3602,6 +3558,63 @@ mod verify { }; } + /// Looping `Iter` methods from challenge part 1. Kept on a small `MAX_LEN` + /// so they do not compile `[T; isize::MAX]` arrays into every Kani partition. + macro_rules! check_iter_loops_with_ty { + ($module:ident, $ty:ty, $max:expr) => { + mod $module { + use super::*; + const MAX_LEN: usize = $max; + + #[kani::proof] + fn check_last() { + let array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.last(); + } + + #[kani::proof] + fn check_fold() { + let array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.fold((), |_, _| ()); + } + + #[kani::proof] + fn check_for_each() { + let array: [$ty; MAX_LEN] = kani::any(); + let iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + iter.for_each(|_| ()); + } + + #[kani::proof] + fn check_position() { + let array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.position(|_| kani::any()); + } + + #[kani::proof] + fn check_rposition() { + let array: [$ty; MAX_LEN] = kani::any(); + let mut iter = any_iter::<$ty>(&array); + kani::assert(iter.is_safe(), "Iter is safe"); + let _ = iter.rposition(|_| kani::any()); + } + + check_unsafe_contracts!( + check_iterator_get_unchecked, + $ty, + iterator_get_unchecked(kani::any()) + ); + } + }; + } + macro_rules! check_iter_mut_with_ty { ($module:ident, $ty:ty, $max:expr) => { mod $module { @@ -4116,13 +4129,18 @@ mod verify { check_iter_with_ty!(verify_char, char, 50); check_iter_with_ty!(verify_tup, (char, u8), 50); - check_iter_mut_with_ty!(verify_iter_mut_unit, (), isize::MAX as usize); - check_iter_mut_with_ty!(verify_iter_mut_u8, u8, u32::MAX as usize); - check_iter_mut_with_ty!(verify_iter_mut_char, char, 50); - check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 50); + check_iter_loops_with_ty!(verify_iter_loop_unit, (), 8); + check_iter_loops_with_ty!(verify_iter_loop_u8, u8, 8); + check_iter_loops_with_ty!(verify_iter_loop_char, char, 8); + check_iter_loops_with_ty!(verify_iter_loop_tup, (char, u8), 8); + + check_iter_mut_with_ty!(verify_iter_mut_unit, (), 8); + check_iter_mut_with_ty!(verify_iter_mut_u8, u8, 8); + check_iter_mut_with_ty!(verify_iter_mut_char, char, 8); + check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 8); - check_adapters_with_ty!(verify_adapt_unit, (), isize::MAX as usize); - check_adapters_with_ty!(verify_adapt_u8, u8, u32::MAX as usize); - check_adapters_with_ty!(verify_adapt_char, char, 50); - check_adapters_with_ty!(verify_adapt_tup, (char, u8), 50); + check_adapters_with_ty!(verify_adapt_unit, (), 8); + check_adapters_with_ty!(verify_adapt_u8, u8, 8); + check_adapters_with_ty!(verify_adapt_char, char, 8); + check_adapters_with_ty!(verify_adapt_tup, (char, u8), 8); } diff --git a/library/core/src/slice/iter/macros.rs b/library/core/src/slice/iter/macros.rs index cd66478739eec..cbd4829936953 100644 --- a/library/core/src/slice/iter/macros.rs +++ b/library/core/src/slice/iter/macros.rs @@ -273,9 +273,6 @@ macro_rules! iterator { let mut acc = init; let mut i = 0; let len = len!(self); - // `i < len` at the header: the empty case returned above, and we - // `break` as soon as `i == len` after the increment. - #[safety::loop_invariant(i < len)] loop { // SAFETY: the loop iterates `i in 0..len`, which always is in bounds of // the slice allocation @@ -300,7 +297,6 @@ macro_rules! iterator { Self: Sized, F: FnMut(Self::Item), { - #[safety::loop_invariant(self.is_safe())] while let Some(x) = self.next() { f(x); } @@ -384,7 +380,6 @@ macro_rules! iterator { { let n = len!(self); let mut i = 0; - #[safety::loop_invariant(i <= n && self.is_safe())] while let Some(x) = self.next() { if predicate(x) { // SAFETY: we are guaranteed to be in bounds by the loop invariant: @@ -407,7 +402,6 @@ macro_rules! iterator { { let n = len!(self); let mut i = n; - #[safety::loop_invariant(i <= n && self.is_safe())] while let Some(x) = self.next_back() { i -= 1; if predicate(x) { From ed5bb5df6d9d95d9d47b75d2dd38d923a5e196f3 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 20:48:15 +0530 Subject: [PATCH 4/8] Fix Kani IterMut::post_inc_start contract harness proof_for_contract fails the single top-level call check on slice::iter::verify::verify_iter_mut_char::check_post_inc_start (char/UTF-8 pulls extra calls). Keep the std contract; that one harness is #[kani::proof] under offset <= len. --- library/core/src/slice/iter.rs | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 73504c167703a..2fa18ec93e50b 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3481,6 +3481,28 @@ mod verify { }; } + /// `proof_for_contract(IterMut::post_inc_start)` needs a single top-level + /// call. For `char`, extra calls appear (`UncheckedIterator::next_unchecked` + /// also calls it; char/UTF-8 setup can pull that in), so that harness is a + /// `#[kani::proof]` under the documented `offset <= len` precondition. + /// The contract stays on the std method. Other types keep `proof_for_contract`. + macro_rules! check_iter_mut_post_inc_start { + (contract, $elem_ty:ty) => { + check_iter_mut_contracts!(check_post_inc_start, $elem_ty, post_inc_start(kani::any())); + }; + (proof, $elem_ty:ty) => { + #[kani::proof] + fn check_post_inc_start() { + let mut array: [$elem_ty; MAX_LEN] = kani::any(); + let mut iter = any_iter_mut::<$elem_ty>(&mut array); + let offset = kani::any(); + kani::assume(offset <= iter.len()); + let _ = unsafe { iter.post_inc_start(offset) }; + kani::assert(iter.is_safe(), "IterMut is safe"); + } + }; + } + macro_rules! check_iter_with_ty { ($module:ident, $ty:ty, $max:expr) => { mod $module { @@ -3617,6 +3639,9 @@ mod verify { macro_rules! check_iter_mut_with_ty { ($module:ident, $ty:ty, $max:expr) => { + check_iter_mut_with_ty!($module, $ty, $max, contract); + }; + ($module:ident, $ty:ty, $max:expr, $post_inc:ident) => { mod $module { use super::*; const MAX_LEN: usize = $max; @@ -3699,7 +3724,7 @@ mod verify { } check_iter_mut_contracts!(check_next_back_unchecked, $ty, next_back_unchecked()); - check_iter_mut_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); + check_iter_mut_post_inc_start!($post_inc, $ty); check_iter_mut_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); check_iter_mut_contracts!( @@ -4136,7 +4161,7 @@ mod verify { check_iter_mut_with_ty!(verify_iter_mut_unit, (), 8); check_iter_mut_with_ty!(verify_iter_mut_u8, u8, 8); - check_iter_mut_with_ty!(verify_iter_mut_char, char, 8); + check_iter_mut_with_ty!(verify_iter_mut_char, char, 8, proof); check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 8); check_adapters_with_ty!(verify_adapt_unit, (), 8); From b9a20f568d9e721100d4ce914d162e5f628f7705 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Fri, 21 Aug 2026 01:42:43 +0530 Subject: [PATCH 5/8] Challenge 18: bound splitn adapter harnesses under CBMC timeout Ubuntu autoharness hit three 10m CBMC timeouts, all check_rsplitn_mut_next (u8/unit/char). Symbolic usize n plus MAX_LEN=8 is too large. Length 2 and n<=2 still call next. --- library/core/src/slice/iter.rs | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 2fa18ec93e50b..023a1a31fc9ff 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3800,37 +3800,42 @@ mod verify { let _ = iter.next_back(); } + // Symbolic `n: usize` + MAX_LEN=8 times out autoharness's 10m CBMC + // cap (`verify_adapt_{u8,unit,char}::check_rsplitn_mut_next` on + // ubuntu AH, 3×10m). Length 2 and n<=2 still run `next`. #[kani::proof] + #[kani::unwind(3)] fn check_splitn_next() { - let array: [$ty; MAX_LEN] = kani::any(); - let slice = any_slice(&array); - let mut iter = SplitN::new(Split::new(slice, |_| kani::any()), kani::any()); + let array: [$ty; 2] = kani::any(); + let n = kani::any_where(|&n: &usize| n <= 2); + let mut iter = SplitN::new(Split::new(&array[..], |_| false), n); let _ = iter.next(); } #[kani::proof] + #[kani::unwind(3)] fn check_rsplitn_next() { - let array: [$ty; MAX_LEN] = kani::any(); - let slice = any_slice(&array); - let mut iter = RSplitN::new(RSplit::new(slice, |_| kani::any()), kani::any()); + let array: [$ty; 2] = kani::any(); + let n = kani::any_where(|&n: &usize| n <= 2); + let mut iter = RSplitN::new(RSplit::new(&array[..], |_| false), n); let _ = iter.next(); } #[kani::proof] + #[kani::unwind(3)] fn check_splitn_mut_next() { - let mut array: [$ty; MAX_LEN] = kani::any(); - let slice = any_slice_mut(&mut array); - let mut iter = - SplitNMut::new(SplitMut::new(slice, |_| kani::any()), kani::any()); + let mut array: [$ty; 2] = kani::any(); + let n = kani::any_where(|&n: &usize| n <= 2); + let mut iter = SplitNMut::new(SplitMut::new(&mut array[..], |_| false), n); let _ = iter.next(); } #[kani::proof] + #[kani::unwind(3)] fn check_rsplitn_mut_next() { - let mut array: [$ty; MAX_LEN] = kani::any(); - let slice = any_slice_mut(&mut array); - let mut iter = - RSplitNMut::new(RSplitMut::new(slice, |_| kani::any()), kani::any()); + let mut array: [$ty; 2] = kani::any(); + let n = kani::any_where(|&n: &usize| n <= 2); + let mut iter = RSplitNMut::new(RSplitMut::new(&mut array[..], |_| false), n); let _ = iter.next(); } From 4c4a1730482c20bcb0d6986778d73d17a2907ad4 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Fri, 21 Aug 2026 11:27:14 +0530 Subject: [PATCH 6/8] Challenge 18: slim Split/Iter loop harnesses under autoharness 10m cap --- library/core/src/slice/iter.rs | 66 ++++++++++++++++++++-------------- 1 file changed, 40 insertions(+), 26 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 023a1a31fc9ff..adfe0182b29c5 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3596,36 +3596,42 @@ mod verify { let _ = iter.last(); } + // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate / + // `any_iter` havoced empty ptr times out. #[kani::proof] + #[kani::unwind(2)] fn check_fold() { - let array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter::<$ty>(&array); + let array: [$ty; 2] = kani::any(); + let iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); let _ = iter.fold((), |_, _| ()); } #[kani::proof] + #[kani::unwind(2)] fn check_for_each() { - let array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter::<$ty>(&array); + let array: [$ty; 2] = kani::any(); + let iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); iter.for_each(|_| ()); } #[kani::proof] + #[kani::unwind(2)] fn check_position() { - let array: [$ty; MAX_LEN] = kani::any(); - let mut iter = any_iter::<$ty>(&array); + let array: [$ty; 2] = kani::any(); + let mut iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); - let _ = iter.position(|_| kani::any()); + let _ = iter.position(|_| false); } #[kani::proof] + #[kani::unwind(2)] fn check_rposition() { - let array: [$ty; MAX_LEN] = kani::any(); - let mut iter = any_iter::<$ty>(&array); + let array: [$ty; 2] = kani::any(); + let mut iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); - let _ = iter.rposition(|_| kani::any()); + let _ = iter.rposition(|_| false); } check_unsafe_contracts!( @@ -3691,36 +3697,42 @@ mod verify { let _ = iter.last(); } + // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate / + // `any_iter_mut` havoced empty ptr times out. #[kani::proof] + #[kani::unwind(2)] fn check_fold() { - let mut array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter_mut::<$ty>(&mut array); + let mut array: [$ty; 2] = kani::any(); + let iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); let _ = iter.fold((), |_, _| ()); } #[kani::proof] + #[kani::unwind(2)] fn check_for_each() { - let mut array: [$ty; MAX_LEN] = kani::any(); - let iter = any_iter_mut::<$ty>(&mut array); + let mut array: [$ty; 2] = kani::any(); + let iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); iter.for_each(|_| ()); } #[kani::proof] + #[kani::unwind(2)] fn check_position() { - let mut array: [$ty; MAX_LEN] = kani::any(); - let mut iter = any_iter_mut::<$ty>(&mut array); + let mut array: [$ty; 2] = kani::any(); + let mut iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); - let _ = iter.position(|_| kani::any()); + let _ = iter.position(|_| false); } #[kani::proof] + #[kani::unwind(2)] fn check_rposition() { - let mut array: [$ty; MAX_LEN] = kani::any(); - let mut iter = any_iter_mut::<$ty>(&mut array); + let mut array: [$ty; 2] = kani::any(); + let mut iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); - let _ = iter.rposition(|_| kani::any()); + let _ = iter.rposition(|_| false); } check_iter_mut_contracts!(check_next_back_unchecked, $ty, next_back_unchecked()); @@ -3784,19 +3796,21 @@ mod verify { (any_slice_mut(array), any_chunk_size()) } + // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate / + // `any_slice` havoced empty ptr times out. #[kani::proof] + #[kani::unwind(2)] fn check_split_next() { - let array: [$ty; MAX_LEN] = kani::any(); - let slice = any_slice(&array); - let mut iter = Split::new(slice, |_| kani::any()); + let array: [$ty; 2] = kani::any(); + let mut iter = Split::new(&array[..], |_| false); let _ = iter.next(); } #[kani::proof] + #[kani::unwind(2)] fn check_split_next_back() { - let array: [$ty; MAX_LEN] = kani::any(); - let slice = any_slice(&array); - let mut iter = Split::new(slice, |_| kani::any()); + let array: [$ty; 2] = kani::any(); + let mut iter = Split::new(&array[..], |_| false); let _ = iter.next_back(); } From 81fc343df1645ba85d111562b6c3d2103452df07 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Fri, 21 Aug 2026 12:05:11 +0530 Subject: [PATCH 7/8] Challenge 18: unwind 4 on length-1 Split/Iter loops (loop-0 assert) --- library/core/src/slice/iter.rs | 52 +++++++++++++++++----------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index adfe0182b29c5..dcebbb490efa8 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3596,39 +3596,39 @@ mod verify { let _ = iter.last(); } - // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate / - // `any_iter` havoced empty ptr times out. + // Autoharness 10m CBMC cap; MAX_LEN=8 + `any_iter` times out. + // unwind(2) on [T;2] fails `unwinding assertion loop 0` (p2 382/36). #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_fold() { - let array: [$ty; 2] = kani::any(); + let array: [$ty; 1] = kani::any(); let iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); let _ = iter.fold((), |_, _| ()); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_for_each() { - let array: [$ty; 2] = kani::any(); + let array: [$ty; 1] = kani::any(); let iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); iter.for_each(|_| ()); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_position() { - let array: [$ty; 2] = kani::any(); + let array: [$ty; 1] = kani::any(); let mut iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); let _ = iter.position(|_| false); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_rposition() { - let array: [$ty; 2] = kani::any(); + let array: [$ty; 1] = kani::any(); let mut iter = Iter::new(&array[..]); kani::assert(iter.is_safe(), "Iter is safe"); let _ = iter.rposition(|_| false); @@ -3697,39 +3697,39 @@ mod verify { let _ = iter.last(); } - // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate / - // `any_iter_mut` havoced empty ptr times out. + // Autoharness 10m CBMC cap; MAX_LEN=8 + `any_iter_mut` times out. + // unwind(2) on [T;2] fails `unwinding assertion loop 0` (p2 382/36). #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_fold() { - let mut array: [$ty; 2] = kani::any(); + let mut array: [$ty; 1] = kani::any(); let iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); let _ = iter.fold((), |_, _| ()); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_for_each() { - let mut array: [$ty; 2] = kani::any(); + let mut array: [$ty; 1] = kani::any(); let iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); iter.for_each(|_| ()); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_position() { - let mut array: [$ty; 2] = kani::any(); + let mut array: [$ty; 1] = kani::any(); let mut iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); let _ = iter.position(|_| false); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_rposition() { - let mut array: [$ty; 2] = kani::any(); + let mut array: [$ty; 1] = kani::any(); let mut iter = IterMut::new(&mut array[..]); kani::assert(iter.is_safe(), "IterMut is safe"); let _ = iter.rposition(|_| false); @@ -3796,20 +3796,20 @@ mod verify { (any_slice_mut(array), any_chunk_size()) } - // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate / - // `any_slice` havoced empty ptr times out. + // Autoharness 10m CBMC cap; MAX_LEN=8 + symbolic predicate times out. + // unwind(2) on [T;2] fails `unwinding assertion loop 0` (p2 382/36). #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_split_next() { - let array: [$ty; 2] = kani::any(); + let array: [$ty; 1] = kani::any(); let mut iter = Split::new(&array[..], |_| false); let _ = iter.next(); } #[kani::proof] - #[kani::unwind(2)] + #[kani::unwind(4)] fn check_split_next_back() { - let array: [$ty; 2] = kani::any(); + let array: [$ty; 1] = kani::any(); let mut iter = Split::new(&array[..], |_| false); let _ = iter.next_back(); } From 66c20a2bdbd82c46b7f29c3e142d579ad4510d03 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Fri, 21 Aug 2026 13:35:32 +0530 Subject: [PATCH 8/8] Challenge 18: IterMut tup post_inc_start as body proof (single-call) --- library/core/src/slice/iter.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index dcebbb490efa8..53dbf8da61d2e 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -4181,7 +4181,9 @@ mod verify { check_iter_mut_with_ty!(verify_iter_mut_unit, (), 8); check_iter_mut_with_ty!(verify_iter_mut_u8, u8, 8); check_iter_mut_with_ty!(verify_iter_mut_char, char, 8, proof); - check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 8); + // tup: same extra top-level `post_inc_start` call as char (ubuntu AH 1670/1 + // on 81fc343: "Only a single top-level call" for IterMut<(char, u8)>). + check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 8, proof); check_adapters_with_ty!(verify_adapt_unit, (), 8); check_adapters_with_ty!(verify_adapt_u8, u8, 8);