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

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

@@ -3,6 +3,8 @@ use crate::iter::adapters::SourceIter;
 use crate::iter::{
     ByRefSized, FusedIterator, InPlaceIterable, TrustedFused, TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, NeverShortCircuit, Try};
 
@@ -230,6 +232,14 @@ where
         let inner_len = self.iter.size();
         let mut i = 0;
         // Use a while loop because (0..len).step_by(N) doesn't optimize well.
+        // Kani: the loop writes only `accum` and `i`, so `inner_len` keeps
+        // its entry value `self.iter.size()`; the invariant bounds `i`, which
+        // also guards the `inner_len - i` subtraction in the loop condition
+        // against underflow. The frame is stated explicitly because the
+        // `from_fn` closure borrows `self` mutably, and the inferred frame
+        // would otherwise havoc the whole adapter, `remainder` included.
+        #[safety::loop_invariant(i <= inner_len)]
+        #[cfg_attr(kani, kani::loop_modifies(&accum, &i))]
         while inner_len - i >= N {
             let chunk = crate::array::from_fn(|local| {
                 // SAFETY: The method consumes the iterator and the loop condition ensures that
@@ -274,3 +284,68 @@ 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.
+    // The chunking loop carries a Kani loop invariant, so no unwind bound is
+    // necessary and `MAX_LEN` mirrors the accessor harness menu: `u32::MAX`
+    // for `u8`, `isize::MAX` for the ZST, moderate bounds for the wider
+    // element types.
+    macro_rules! check_fold {
+        ($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 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, isize::MAX as usize);
+    check_fold!(check_array_chunks_fold_u8, u8, 2, u32::MAX as usize);
+    check_fold!(check_array_chunks_fold_char, char, 3, 10);
+    check_fold!(check_array_chunks_fold_tup, (char, u8), 2, 10);
+}

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,69 @@ 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.
+    // The `MAX_LEN` menu mirrors `check_get_unchecked` above: the `u8`/ZST
+    // harnesses raise the bound very high (there is no per-iteration loop, only
+    // a bulk copy, so the cost stays flat), the wider types use a moderate one.
+    macro_rules! check_spec_next_chunk {
+        ($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 = 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, isize::MAX as usize);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_u8, u8, 3, u32::MAX as usize);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_char, char, 2, 50);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_tup, (char, u8), 2, 50);
+}

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

@@ -321,3 +321,70 @@ 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`).  The slice handed to the iterator
+    /// has a symbolic length in `0..=MAX_LEN`, so one proof covers every
+    /// length up to the backing array's size at once.  The proof is still
+    /// bounded by `MAX_LEN`: the `u8`/ZST harnesses raise `MAX_LEN` to
+    /// `u32::MAX`/`isize::MAX`, far beyond practical slice lengths, while the
+    /// wider element types use smaller bounds.
+    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 plain `#[kani::proof]` harness per concrete element type (the NOTE
+    /// below explains why this is not `proof_for_contract`).  `slice::Iter<T>`
+    /// is `TrustedRandomAccessNoCoerce` for every `T`, satisfying the method's
+    /// `Self: TrustedRandomAccessNoCoerce` bound.
+    // 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,76 @@ 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.
+    //
+    // Boundedness: the chunk fill iterates through the generic default
+    // `Iterator::try_fold` (a while-let loop that calls a generic closure in
+    // iterator.rs), so this adapter cannot attach a loop contract to it. A
+    // fixed `MAX_LEN` is still a complete state-space cover, not a truncation:
+    // every reachable value of `initialized` is in 0..=N for every slice
+    // length, so any `MAX_LEN >= N + 2` exercises every reachable
+    // configuration (empty source, saturation before exhaustion, and
+    // exhaustion before saturation).
+    //
+    // N = 0 is excluded on purpose. The current upstream implementation has a
+    // latent N = 0 defect: the closure writes through
+    // `array.get_unchecked_mut(idx)` before it compares `initialized < N`, so
+    // `next_chunk::<0>()` on a source that yields at least one element writes
+    // out of bounds into the zero-length array. Repo rules
+    // (doc/src/general-rules.md) do not permit a local change to the runtime
+    // logic, so the fix must land upstream. An upstream report is prepared.
+    // These harnesses cover N >= 1.
+    macro_rules! check_next_chunk_dropless {
+        ($harness:ident, $elem_ty:ty, $n:expr) => {
+            #[kani::proof]
+            #[kani::unwind(7)]
+            fn $harness() {
+                const MAX_LEN: usize = 6;
+                const N: usize = $n;
+                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, (), 4);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_u8, u8, 4);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_char, char, 4);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_tup, (char, u8), 4);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_unit_n1, (), 1);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_u8_n1, u8, 1);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_char_n1, char, 1);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_tup_n1, (char, u8), 1);
+}