Add remaining Ch17/Ch18 harnesses: as_chunks_unchecked, get_disjoint, fold/for_each/position

Ch17 additions (25 total harnesses in mod.rs):
- as_chunks_unchecked, as_chunks_unchecked_mut (N=1,2,4)
- get_disjoint_mut (N=2,3), get_disjoint_unchecked_mut (N=2)

Ch18 additions (52 total harnesses in iter.rs):
- __iterator_get_unchecked for ChunksMut, ChunksExact, RChunks,
  RChunksMut, RChunksExact, RChunksExactMut
- Macro functions: fold, for_each, position, rposition (Iter)
- Macro functions: fold, for_each, position (IterMut)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: jrey8343

library/core/src/slice/iter.rs

@@ -3837,4 +3837,153 @@ mod verify {
             }
         }
     }
+
+    // --- __iterator_get_unchecked for remaining iterator types ---
+    mod verify_get_unchecked {
+        use super::*;
+
+        #[kani::proof]
+        fn check_chunks_mut_get_unchecked() {
+            let mut array: [u8; 64] = kani::any();
+            let slice = any_slice_mut(&mut array);
+            let len = slice.len();
+            if len > 0 {
+                let chunk_size: usize = kani::any_where(|s: &usize| *s > 0 && *s <= 64);
+                let chunks = slice.chunks_mut(chunk_size);
+                if chunks.len() > 0 {
+                    let idx: usize = kani::any_where(|i: &usize| *i < chunks.len());
+                    let _ = unsafe { chunks.__iterator_get_unchecked(idx) };
+                }
+            }
+        }
+
+        #[kani::proof]
+        fn check_chunks_exact_get_unchecked() {
+            let array: [u8; 64] = kani::any();
+            let slice = any_slice(&array);
+            let chunk_size: usize = kani::any_where(|s: &usize| *s > 0 && *s <= 64);
+            let chunks = slice.chunks_exact(chunk_size);
+            if chunks.len() > 0 {
+                let idx: usize = kani::any_where(|i: &usize| *i < chunks.len());
+                let _ = unsafe { chunks.__iterator_get_unchecked(idx) };
+            }
+        }
+
+        #[kani::proof]
+        fn check_rchunks_get_unchecked() {
+            let array: [u8; 64] = kani::any();
+            let slice = any_slice(&array);
+            let chunk_size: usize = kani::any_where(|s: &usize| *s > 0 && *s <= 64);
+            let rchunks = slice.rchunks(chunk_size);
+            if rchunks.len() > 0 {
+                let idx: usize = kani::any_where(|i: &usize| *i < rchunks.len());
+                let _ = unsafe { rchunks.__iterator_get_unchecked(idx) };
+            }
+        }
+
+        #[kani::proof]
+        fn check_rchunks_mut_get_unchecked() {
+            let mut array: [u8; 64] = kani::any();
+            let slice = any_slice_mut(&mut array);
+            let len = slice.len();
+            if len > 0 {
+                let chunk_size: usize = kani::any_where(|s: &usize| *s > 0 && *s <= 64);
+                let rchunks = slice.rchunks_mut(chunk_size);
+                if rchunks.len() > 0 {
+                    let idx: usize = kani::any_where(|i: &usize| *i < rchunks.len());
+                    let _ = unsafe { rchunks.__iterator_get_unchecked(idx) };
+                }
+            }
+        }
+
+        #[kani::proof]
+        fn check_rchunks_exact_get_unchecked() {
+            let array: [u8; 64] = kani::any();
+            let slice = any_slice(&array);
+            let chunk_size: usize = kani::any_where(|s: &usize| *s > 0 && *s <= 64);
+            let rchunks = slice.rchunks_exact(chunk_size);
+            if rchunks.len() > 0 {
+                let idx: usize = kani::any_where(|i: &usize| *i < rchunks.len());
+                let _ = unsafe { rchunks.__iterator_get_unchecked(idx) };
+            }
+        }
+
+        #[kani::proof]
+        fn check_rchunks_exact_mut_get_unchecked() {
+            let mut array: [u8; 64] = kani::any();
+            let slice = any_slice_mut(&mut array);
+            let len = slice.len();
+            if len > 0 {
+                let chunk_size: usize = kani::any_where(|s: &usize| *s > 0 && *s <= 64);
+                let rchunks = slice.rchunks_exact_mut(chunk_size);
+                if rchunks.len() > 0 {
+                    let idx: usize = kani::any_where(|i: &usize| *i < rchunks.len());
+                    let _ = unsafe { rchunks.__iterator_get_unchecked(idx) };
+                }
+            }
+        }
+    }
+
+    // --- Macro-generated functions: fold, for_each, position, rposition ---
+    mod verify_macro_fns {
+        use super::*;
+
+        #[kani::proof]
+        fn check_iter_fold() {
+            let array: [u8; 16] = kani::any();
+            let iter = any_iter(&array);
+            let sum = iter.fold(0u32, |acc, &x| acc.wrapping_add(x as u32));
+            let _ = sum;
+        }
+
+        #[kani::proof]
+        fn check_iter_for_each() {
+            let array: [u8; 16] = kani::any();
+            let iter = any_iter(&array);
+            let mut count = 0usize;
+            iter.for_each(|_| count += 1);
+        }
+
+        #[kani::proof]
+        fn check_iter_position() {
+            let array: [u8; 16] = kani::any();
+            let iter = any_iter(&array);
+            let target: u8 = kani::any();
+            let _ = iter.position(|x| *x == target);
+        }
+
+        #[kani::proof]
+        fn check_iter_rposition() {
+            let array: [u8; 16] = kani::any();
+            let iter = any_iter(&array);
+            let target: u8 = kani::any();
+            let _ = iter.rposition(|x| *x == target);
+        }
+
+        // IterMut variants
+        #[kani::proof]
+        fn check_iter_mut_fold() {
+            let mut array: [u8; 16] = kani::any();
+            let slice = any_slice_mut(&mut array);
+            let iter = slice.iter_mut();
+            let sum = iter.fold(0u32, |acc, x| acc.wrapping_add(*x as u32));
+            let _ = sum;
+        }
+
+        #[kani::proof]
+        fn check_iter_mut_for_each() {
+            let mut array: [u8; 16] = kani::any();
+            let slice = any_slice_mut(&mut array);
+            let mut iter = slice.iter_mut();
+            iter.for_each(|x| *x = 0);
+        }
+
+        #[kani::proof]
+        fn check_iter_mut_position() {
+            let mut array: [u8; 16] = kani::any();
+            let slice = any_slice_mut(&mut array);
+            let target: u8 = kani::any();
+            let _ = slice.iter_mut().position(|x| *x == target);
+        }
+    }
 }

library/core/src/slice/mod.rs

@@ -5833,4 +5833,93 @@ mod verify {
             slice.copy_within(src_start..src_end, dest);
         }
     }
+
+    // --- as_chunks_unchecked / as_chunks_unchecked_mut ---
+    macro_rules! check_as_chunks_unchecked {
+        ($name:ident, $N:expr) => {
+            #[kani::proof]
+            fn $name() {
+                const ARR_SIZE: usize = 64;
+                let arr: [u8; ARR_SIZE] = kani::any();
+                let slice = kani::slice::any_slice_of_array(&arr);
+                // Only call when len is a multiple of N
+                if slice.len() > 0 && slice.len() % $N == 0 {
+                    let chunks = unsafe { slice.as_chunks_unchecked::<$N>() };
+                    assert!(chunks.len() == slice.len() / $N);
+                }
+            }
+        };
+    }
+    check_as_chunks_unchecked!(check_as_chunks_unchecked_1, 1);
+    check_as_chunks_unchecked!(check_as_chunks_unchecked_2, 2);
+    check_as_chunks_unchecked!(check_as_chunks_unchecked_4, 4);
+
+    macro_rules! check_as_chunks_unchecked_mut {
+        ($name:ident, $N:expr) => {
+            #[kani::proof]
+            fn $name() {
+                const ARR_SIZE: usize = 64;
+                let mut arr: [u8; ARR_SIZE] = kani::any();
+                let slice = kani::slice::any_slice_of_array_mut(&mut arr);
+                let len = slice.len();
+                if len > 0 && len % $N == 0 {
+                    let chunks = unsafe { slice.as_chunks_unchecked_mut::<$N>() };
+                    assert!(chunks.len() == len / $N);
+                }
+            }
+        };
+    }
+    check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_1, 1);
+    check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_2, 2);
+    check_as_chunks_unchecked_mut!(check_as_chunks_unchecked_mut_4, 4);
+
+    // --- get_disjoint_mut / get_disjoint_unchecked_mut ---
+    #[kani::proof]
+    fn check_get_disjoint_mut_2() {
+        let mut arr: [u8; 16] = kani::any();
+        let slice = kani::slice::any_slice_of_array_mut(&mut arr);
+        let len = slice.len();
+        if len >= 2 {
+            let i: usize = kani::any();
+            let j: usize = kani::any();
+            kani::assume(i < len);
+            kani::assume(j < len);
+            kani::assume(i != j);
+            let result = slice.get_disjoint_mut([i, j]);
+            assert!(result.is_ok());
+        }
+    }
+
+    #[kani::proof]
+    fn check_get_disjoint_unchecked_mut_2() {
+        let mut arr: [u8; 16] = kani::any();
+        let slice = kani::slice::any_slice_of_array_mut(&mut arr);
+        let len = slice.len();
+        if len >= 2 {
+            let i: usize = kani::any();
+            let j: usize = kani::any();
+            kani::assume(i < len);
+            kani::assume(j < len);
+            kani::assume(i != j);
+            let [a, b] = unsafe { slice.get_disjoint_unchecked_mut([i, j]) };
+            *a = 42;
+            *b = 99;
+        }
+    }
+
+    #[kani::proof]
+    fn check_get_disjoint_mut_3() {
+        let mut arr: [u8; 16] = kani::any();
+        let slice = kani::slice::any_slice_of_array_mut(&mut arr);
+        let len = slice.len();
+        if len >= 3 {
+            let i: usize = kani::any();
+            let j: usize = kani::any();
+            let k: usize = kani::any();
+            kani::assume(i < len && j < len && k < len);
+            kani::assume(i != j && i != k && j != k);
+            let result = slice.get_disjoint_mut([i, j, k]);
+            assert!(result.is_ok());
+        }
+    }
 }