Verify iter adapter unsafe methods + safe abstractions (challenge #16)

library/core/src/iter/adapters/array_chunks.rs

@@ -274,3 +274,65 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // `next_back_remainder` pulls the final `len % N` elements off the back via
+    // `rev().take(rem).next_chunk()`, then reverses them in place, relying on
+    // `unwrap_err_unchecked` (sound because `rem < N`).
+    macro_rules! check_next_back_remainder {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it: ArrayChunks<_, N> = ArrayChunks::new(any_slice(&array).iter());
+                it.next_back_remainder();
+                let _ = &it.remainder;
+            }
+        };
+    }
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_unit, (), 2, 8);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_u8, u8, 2, 8);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_char, char, 3, 9);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_tup, (char, u8), 2, 8);
+
+    // `fold` on a `TrustedRandomAccessNoCoerce` source builds each chunk with
+    // `array::from_fn` calling `__iterator_get_unchecked(i + local)` under an
+    // `inner_len - i >= N` guard; this proves those indexes stay in bounds.
+    macro_rules! check_fold {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr, $unwind:literal) => {
+            #[kani::proof]
+            #[kani::unwind($unwind)]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let it: ArrayChunks<_, N> = ArrayChunks::new(any_slice(&array).iter());
+                // Disambiguate from the in-scope internal `SpecFold::fold`.
+                let _ = crate::iter::Iterator::fold(it, 0usize, |acc, _chunk| acc.wrapping_add(1));
+            }
+        };
+    }
+    check_fold!(check_array_chunks_fold_unit, (), 2, 4, 5);
+    check_fold!(check_array_chunks_fold_u8, u8, 2, 4, 5);
+    check_fold!(check_array_chunks_fold_char, char, 3, 6, 7);
+    check_fold!(check_array_chunks_fold_tup, (char, u8), 2, 4, 5);
+}

library/core/src/iter/adapters/cloned.rs

@@ -193,3 +193,62 @@ unsafe impl<I: InPlaceIterable> InPlaceIterable for Cloned<I> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_cloned_iter<'a, T: Clone>(orig_slice: &'a [T]) -> Cloned<crate::slice::Iter<'a, T>> {
+        Cloned::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_cloned_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.it.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_cloned_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_cloned_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_cloned_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_cloned_get_unchecked_tup, (char, u8), 50);
+
+    // `next_unchecked` (UncheckedIterator): the precondition is that the iterator
+    // is non-empty; establish it by construction.
+    macro_rules! check_cloned_next_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_cloned_iter::<$elem_ty>(&array);
+                kani::assume(it.it.size_hint().0 > 0);
+                let _ = unsafe { it.next_unchecked() };
+            }
+        };
+    }
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_unit, (), isize::MAX as usize);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_u8, u8, u32::MAX as usize);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_char, char, 50);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_tup, (char, u8), 50);
+}

library/core/src/iter/adapters/copied.rs

@@ -278,3 +278,66 @@ unsafe impl<I: InPlaceIterable> InPlaceIterable for Copied<I> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_adapter_iter<'a, T>(orig_slice: &'a [T]) -> Copied<crate::slice::Iter<'a, T>> {
+        Copied::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_adapter_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.it.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_copied_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_copied_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_copied_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_copied_get_unchecked_tup, (char, u8), 50);
+
+    // `spec_next_chunk` on the `slice::Iter` specialization bulk-copies `N` (or
+    // `len`) elements into a `MaybeUninit<[T; N]>` and then either
+    // `array_assume_init`s the full array or returns a `0..len` `IntoIter`; this
+    // proves the `copy_nonoverlapping` lengths and the init range stay in bounds.
+    // `N` is a trait generic, so it is pinned via the result type annotation.
+    macro_rules! check_spec_next_chunk {
+        ($harness:ident, $elem_ty:ty, $n:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = 16;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_slice(&array).iter();
+                let _result: Result<[$elem_ty; N], crate::array::IntoIter<$elem_ty, N>> =
+                    it.spec_next_chunk();
+            }
+        };
+    }
+    check_spec_next_chunk!(check_copied_spec_next_chunk_unit, (), 2);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_u8, u8, 3);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_char, char, 2);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_tup, (char, u8), 2);
+}

library/core/src/iter/adapters/enumerate.rs

@@ -321,3 +321,67 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+/// Verification harnesses for `Enumerate`'s `unsafe`/contract-bearing methods
+/// (verify-rust-std challenge #16).
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    /// An arbitrary-length sub-slice of `orig_slice` (mirrors
+    /// `slice::iter::verify::any_slice`).  This is what makes the proof
+    /// *unbounded*: the backing array is a fixed Kani constant, but the slice
+    /// handed to the iterator has a symbolic length, so the proof covers every
+    /// shorter configuration at once.
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            // SAFETY: `ptr` is non-null and aligned; length 0 makes the slice trivially valid.
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    /// Wrap an arbitrary sub-slice in `Enumerate<slice::Iter<'_, T>>`.  We build
+    /// the inner `slice::Iter` via `(&[T]).iter()` because `slice::Iter::new` is
+    /// `pub(super)` to the `slice` module and unreachable from here.
+    fn any_enumerate_iter<'a, T>(orig_slice: &'a [T]) -> Enumerate<crate::slice::Iter<'a, T>> {
+        Enumerate::new(any_slice(orig_slice).iter())
+    }
+
+    /// One `proof_for_contract` harness per concrete element type; the contract
+    /// itself stays generic.  `slice::Iter<T>` is `TrustedRandomAccessNoCoerce`
+    /// for every `T`, satisfying the method's `Self: TrustedRandomAccessNoCoerce`.
+    // NOTE: `__iterator_get_unchecked` is a trait method on the *generic* impl
+    // `impl<I> Iterator for Enumerate<I>`, and Kani cannot attach a
+    // `proof_for_contract` to a generic trait method (kani#1997).  So instead of
+    // the contract machinery we use a plain `#[kani::proof]` that establishes the
+    // method's precondition by construction (`idx < self.iter.size_hint().0`) and
+    // lets Kani prove the body introduces no UB -- the same safety property the
+    // contract expresses.
+    macro_rules! check_enumerate_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut enumerate = any_enumerate_iter::<$elem_ty>(&array);
+                // The method's precondition: `idx < self.iter.size_hint().0`.
+                let idx = kani::any_where(|i: &usize| *i < enumerate.iter.size_hint().0);
+                let _ = unsafe { enumerate.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+
+    // Representative element types: ZST, byte, 4-byte-align niche type, composite.
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_unit, (), isize::MAX as usize);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_u8, u8, u32::MAX as usize);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_char, char, 50);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_tup, (char, u8), 50);
+}

library/core/src/iter/adapters/filter.rs

@@ -214,3 +214,52 @@ unsafe impl<I: InPlaceIterable, P> InPlaceIterable for Filter<I, P> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // `Filter`'s predicate is `FnMut(&Self::Item)`; for `slice::Iter<T>` that is
+    // `FnMut(&&T)`. A nondeterministic predicate exercises both the kept and the
+    // filtered branch. A named fn pointer keeps the helper return type nameable.
+    fn maybe_keep<T>(_: &&T) -> bool {
+        kani::any()
+    }
+
+    // `next_chunk_dropless` writes every element (branchlessly) into a
+    // `MaybeUninit<[_; N]>` and bumps `initialized` only for kept elements,
+    // breaking once `initialized == N`; this proves the `get_unchecked_mut(idx)`
+    // writes and the final `array_assume_init` / `IntoIter` range stay in bounds.
+    macro_rules! check_next_chunk_dropless {
+        ($harness:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            #[kani::unwind(7)]
+            fn $harness() {
+                const MAX_LEN: usize = 6;
+                const N: usize = 4;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it =
+                    Filter::new(any_slice(&array).iter(), maybe_keep::<$elem_ty> as fn(&&$elem_ty) -> bool);
+                let _ = it.next_chunk_dropless::<N>();
+            }
+        };
+    }
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_unit, ());
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_u8, u8);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_char, char);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_tup, (char, u8));
+}

library/core/src/iter/adapters/filter_map.rs

@@ -211,3 +211,53 @@ unsafe impl<I: InPlaceIterable, F> InPlaceIterable for FilterMap<I, F> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // Maps `&T -> Option<usize>` nondeterministically to exercise both the
+    // "element kept" and "element filtered" paths of the chunk-fill loop.
+    fn maybe_map<T>(_: &T) -> Option<usize> {
+        kani::any::<bool>().then_some(0)
+    }
+
+    // `next_chunk` fills a `MaybeUninit<[B; N]>` via a `Guard`-protected loop
+    // that byte-copies each mapped value's payload and bumps `initialized` only
+    // when the map yields `Some`; this proves the copies, the `array_assume_init`,
+    // and the partial-fill `IntoIter` range all stay in bounds.
+    macro_rules! check_next_chunk {
+        ($harness:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $harness() {
+                const MAX_LEN: usize = 5;
+                const N: usize = 3;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = FilterMap::new(
+                    any_slice(&array).iter(),
+                    maybe_map::<$elem_ty> as fn(&$elem_ty) -> Option<usize>,
+                );
+                let _ = it.next_chunk::<N>();
+            }
+        };
+    }
+    check_next_chunk!(check_filter_map_next_chunk_unit, ());
+    check_next_chunk!(check_filter_map_next_chunk_u8, u8);
+    check_next_chunk!(check_filter_map_next_chunk_char, char);
+    check_next_chunk!(check_filter_map_next_chunk_tup, (char, u8));
+}