Add Kani verification harnesses for iterator adapter unsafe functions and safe abstractions (Challenge 16)

Author: Kasim Te

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};
 
@@ -274,3 +276,77 @@ 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]
+    #[kani::unwind(5)]
+    fn check_array_chunks_next_back_remainder_n2() {
+        let len: u8 = kani::any();
+        kani::assume(len <= 4);
+        let mut chunks = ArrayChunks::<_, 2>::new(0..len);
+        let _ = chunks.next_back();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn check_array_chunks_next_back_remainder_n3() {
+        let len: u8 = kani::any();
+        kani::assume(len <= 4);
+        let mut chunks = ArrayChunks::<_, 3>::new(0..len);
+        let _ = chunks.next_back();
+    }
+
+    // fold (TRANC specialized — uses __iterator_get_unchecked in a loop)
+    #[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());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 2);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n2_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 2>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 2);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n3_u8() {
+        const MAX_LEN: usize = 6;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 3>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 3);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n2_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 2>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 2);
+    }
+}

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

@@ -152,6 +152,7 @@ where
     I: UncheckedIterator<Item = &'a T>,
     T: Clone,
 {
+    #[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 +194,102 @@ 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]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        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

@@ -278,3 +278,101 @@ 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]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n2_u8() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n3_u8() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n2_unit() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n2_char() {
+        const MAX_LEN: usize = 8;
+        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

@@ -321,3 +321,59 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        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]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        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) };
+    }
+}