Verify safety of iterator adapter functions (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,11 @@ 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.
+        // Safety argument: __iterator_get_unchecked is read-only for
+        // TrustedRandomAccessNoCoerce iterators, so iter.size() is preserved.
+        // Safety argument: i tracks the consumed element count and stays within
+        // inner_len. Combined with the while condition (inner_len - i >= N),
+        // this ensures i + local < inner_len = iter.size() for all accesses.
         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 +281,51 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // next_back_remainder (uses unwrap_err_unchecked internally)
+    // Uses Range<u8> instead of slice::Iter to avoid pointer-heavy symbolic
+    // state that causes CBMC to exhaust resources. Range<u8> satisfies
+    // DoubleEndedIterator + ExactSizeIterator and exercises the same
+    // unwrap_err_unchecked path.
+    #[kani::proof]
+    fn check_array_chunks_next_back_remainder_n2() {
+        let len: u8 = kani::any();
+        let mut chunks = ArrayChunks::<_, 2>::new(0..len);
+        let _ = chunks.next_back();
+    }
+
+    #[kani::proof]
+    fn check_array_chunks_next_back_remainder_n3() {
+        let len: u8 = kani::any();
+        let mut chunks = ArrayChunks::<_, 3>::new(0..len);
+        let _ = chunks.next_back();
+    }
+
+    // fold (TRANC specialized — uses __iterator_get_unchecked in a loop)
+    // End-to-end bounded harness: exercises the full TRANC fold path.
+    // The while loop's safety (i + local < inner_len) is enforced by
+    // the condition (inner_len - i >= N) and local < N.
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 2>::new(slice.iter());
+        // Exercises TRANC fold path — proves absence of UB in get_unchecked loop.
+        Iterator::fold(chunks, (), |(), _| ());
+    }
+
+    // Note: only the N=2 u8 fold harness is kept, and it is bounded (unwind 9).
+    // The TRANC fold path's `from_fn` MaybeUninit loop conflicts with
+    // loop-contract mode for other element types and chunk sizes, so no
+    // source-level loop invariant is applied here — the safety argument above
+    // stands in its place. The loop safety logic (i + local < inner_len) is
+    // identical for all N and T, so this single bounded harness suffices to
+    // exercise it.
+}

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

@@ -65,6 +65,11 @@ where
         self.it.map(T::clone).fold(init, f)
     }
 
+    // Contract note: Kani's `proof_for_contract` cannot target trait-impl
+    // methods, so this `#[requires]` is not checked as a contract; it is
+    // normative documentation of the precondition. Verification happens in the
+    // `verify::check_*` harness below, which `kani::assume`s this same
+    // expression before the call. Keep the two in sync when editing either.
     #[requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
@@ -152,6 +157,9 @@ where
     I: UncheckedIterator<Item = &'a T>,
     T: Clone,
 {
+    // Contract note: documentation-only, verified via the mirrored `assume` in
+    // `mod verify` — see the note on the first `#[requires]` in this file.
+    #[requires(self.it.size_hint().0 > 0)]
     unsafe fn next_unchecked(&mut self) -> T {
         // SAFETY: `Cloned` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
@@ -193,3 +201,94 @@ 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::*;
+
+    #[kani::proof]
+    fn check_cloned_get_unchecked_u8() {
+        const MAX_LEN: usize = 5000;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let result = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(result, slice[idx]);
+    }
+
+    #[kani::proof]
+    fn check_cloned_get_unchecked_unit() {
+        const MAX_LEN: usize = isize::MAX as usize;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_cloned_next_unchecked_u8() {
+        const MAX_LEN: usize = 5000;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    fn check_cloned_next_unchecked_unit() {
+        const MAX_LEN: usize = isize::MAX as usize;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    fn check_cloned_get_unchecked_char() {
+        const MAX_LEN: usize = 50;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_cloned_get_unchecked_tup() {
+        const MAX_LEN: usize = 50;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_cloned_next_unchecked_char() {
+        const MAX_LEN: usize = 50;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    fn check_cloned_next_unchecked_tup() {
+        const MAX_LEN: usize = 50;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+}

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

@@ -102,6 +102,11 @@ where
         self.it.advance_by(n)
     }
 
+    // Contract note: Kani's `proof_for_contract` cannot target trait-impl
+    // methods, so this `#[requires]` is not checked as a contract; it is
+    // normative documentation of the precondition. Verification happens in the
+    // `verify::check_*` harness below, which `kani::assume`s this same
+    // expression before the call. Keep the two in sync when editing either.
     #[requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
@@ -284,3 +289,93 @@ 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::*;
+
+    // Phase 0 spike: proof_for_contract doesn't work on trait impl methods,
+    // so we use #[kani::proof] with manual precondition via kani::assume.
+    #[kani::proof]
+    fn check_copied_get_unchecked_u8() {
+        const MAX_LEN: usize = 5000;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let result = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(result, slice[idx]);
+    }
+
+    #[kani::proof]
+    fn check_copied_get_unchecked_unit() {
+        const MAX_LEN: usize = isize::MAX as usize;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    // spec_next_chunk (specialized for slice::Iter, uses ptr::copy_nonoverlapping)
+    #[kani::proof]
+    fn check_spec_next_chunk_n2_u8() {
+        const MAX_LEN: usize = 5000;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<2>();
+    }
+
+    #[kani::proof]
+    fn check_spec_next_chunk_n3_u8() {
+        const MAX_LEN: usize = 5000;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<3>();
+    }
+
+    #[kani::proof]
+    fn check_spec_next_chunk_n2_unit() {
+        const MAX_LEN: usize = isize::MAX as usize;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<2>();
+    }
+
+    #[kani::proof]
+    fn check_copied_get_unchecked_char() {
+        const MAX_LEN: usize = 50;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_copied_get_unchecked_tup() {
+        const MAX_LEN: usize = 50;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_spec_next_chunk_n2_char() {
+        const MAX_LEN: usize = 50;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<2>();
+    }
+}

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

@@ -164,6 +164,11 @@ where
 
     #[rustc_inherit_overflow_checks]
     #[inline]
+    // Contract note: Kani's `proof_for_contract` cannot target trait-impl
+    // methods, so this `#[requires]` is not checked as a contract; it is
+    // normative documentation of the precondition. Verification happens in the
+    // `verify::check_*` harness below, which `kani::assume`s this same
+    // expression before the call. Keep the two in sync when editing either.
     #[requires(idx < self.iter.size_hint().0)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item
@@ -321,3 +326,55 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof]
+    fn check_enumerate_get_unchecked_u8() {
+        const MAX_LEN: usize = 5000;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let (i, val) = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(i, idx);
+        assert_eq!(*val, slice[idx]);
+    }
+
+    #[kani::proof]
+    fn check_enumerate_get_unchecked_unit() {
+        const MAX_LEN: usize = isize::MAX as usize;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_enumerate_get_unchecked_char() {
+        const MAX_LEN: usize = 50;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    fn check_enumerate_get_unchecked_tup() {
+        const MAX_LEN: usize = 50;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+}