Challenge 16: Verify safety of iterator adapter functions with Kani

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

@@ -1,6 +1,8 @@
 use crate::array;
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, NeverShortCircuit, Try};
 
@@ -224,6 +226,15 @@ 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.
+        #[cfg_attr(
+            kani,
+            kani::loop_invariant(
+                N != 0
+                    && self.iter.size() == inner_len
+                    && i <= inner_len
+                    && i % N == 0
+            )
+        )]
         while inner_len - i >= N {
             let chunk = crate::array::from_fn(|local| {
                 // SAFETY: The method consumes the iterator and the loop condition ensures that
@@ -268,3 +279,80 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `next_back_remainder` for ArrayChunks
+    macro_rules! generate_next_back_remainder_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            #[kani::unwind(5)]
+            // The input length remains unbounded. Kani cannot automatically infer that
+            // `array::write` iterates at most `end % 4 <= 3` times, so `unwind(5)`
+            // bounds loop expansion, not input length; unwinding assertions ensure completeness.
+            pub fn $name() {
+                // Generate an unbounded symbolic length and payload.
+                let end: usize = kani::any();
+                let value: $ty = kani::any();
+                // Construct a valid unbounded exact-size, double-ended iterator.
+                let source = (0..end).map(move |position| (position, value));
+                // The safe constructor establishes N != 0.
+                let mut chunks = ArrayChunks::<_, 4>::new(source);
+                // Exercise the main path, including unwrap_err_unchecked.
+                chunks.next_back_remainder();
+                // Exercise the existing-remainder early-return path.
+                chunks.next_back_remainder();
+            }
+        };
+    }
+
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i8, i8);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i16, i16);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i32, i32);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i64, i64);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i128, i128);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u8, u8);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u16, u16);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u32, u32);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u64, u64);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u128, u128);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_array, [u8; 4]);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_bool, bool);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_unit, ());
+
+    // Harnesses for `fold` for ArrayChunks
+    macro_rules! generate_array_chunks_fold_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate an unbounded symbolic length, payload, and accumulator.
+                let end: usize = kani::any();
+                let value: $ty = kani::any();
+                let init: $ty = kani::any();
+                // Map preserves random access while attaching the symbolic payload.
+                let source = (0..end).map(move |position| (position, value));
+                // The safe constructor establishes the N != 0 invariant.
+                let chunks = ArrayChunks::<_, 4>::new(source);
+                // Directly call the specialized safe function under test.
+                let _ = SpecFold::fold(chunks, init, |accum, _chunk| accum);
+            }
+        };
+    }
+
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i8, i8);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i16, i16);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i32, i32);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i64, i64);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i128, i128);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u8, u8);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u16, u16);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u32, u32);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u64, u64);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u128, u128);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_array, [u8; 4]);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_bool, bool);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_unit, ());
+}

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

@@ -180,3 +180,49 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Cloned.
+    macro_rules! generate_cloned_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Cloned<crate::slice::Iter<'static, $ty>> as crate::iter::Iterator>::
+                                __iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (0..len).map(|_| &value);
+                let mut iter = Cloned::new(source);
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                // Place witnesses after the call so they exercise the contract.
+                kani::cover(idx == 0, "first element");
+                kani::cover(idx > 0 && idx < len - 1, "interior element");
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i8, i8);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i16, i16);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i32, i32);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i64, i64);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i128, i128);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u8, u8);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u16, u16);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u32, u32);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u64, u64);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u128, u128);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_array, [u8; 4]);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_bool, bool);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_unit, ());
+}

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

@@ -284,3 +284,91 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Copied.
+    macro_rules! generate_copied_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Copied<crate::slice::Iter<'static, $ty>> as crate::iter::Iterator>::
+                                __iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (0..len).map(|_| &value);
+                let mut iter = Copied::new(source);
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                kani::cover(idx == 0, "first element");
+                kani::cover(idx > 0 && idx < len - 1, "interior element");
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i8, i8);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i16, i16);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i32, i32);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i64, i64);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i128, i128);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u8, u8);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u16, u16);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u32, u32);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u64, u64);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u128, u128);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_array, [u8; 4]);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_bool, bool);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_unit, ());
+
+    // Harnesses for `spec_next_chunk` for Copied
+    macro_rules! generate_copied_spec_next_chunk_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Provide valid symbolic storage for every relevant length around N = 4.
+                let values: [$ty; 5] = kani::any();
+                let slice = kani::slice::any_slice_of_array(&values);
+                let mut iter = slice.iter();
+                // Directly call the specialized safe function under test.
+                let _ = <crate::slice::Iter<'_, $ty> as SpecNextChunk<'_, 4, $ty>>::spec_next_chunk(
+                    &mut iter,
+                );
+            }
+        };
+    }
+
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i8, i8);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i16, i16);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i32, i32);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i64, i64);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i128, i128);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u8, u8);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u16, u16);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u32, u32);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u64, u64);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u128, u128);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_array, [u8; 4]);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_bool, bool);
+
+    #[kani::proof]
+    pub fn harness_copied_spec_next_chunk_unit() {
+        // Generate a truly unbounded symbolic length for the zero-sized type.
+        let len: usize = kani::any();
+        let data = crate::ptr::NonNull::<()>::dangling().as_ptr();
+        // SAFETY: the pointer is non-null and aligned, and `()` occupies zero bytes.
+        let slice = unsafe { crate::slice::from_raw_parts(data, len) };
+        let mut iter = slice.iter();
+        // Directly call the ZST branch of the specialized safe function.
+        let _ =
+            <crate::slice::Iter<'_, ()> as SpecNextChunk<'_, 4, ()>>::spec_next_chunk(&mut iter);
+    }
+}

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

@@ -321,3 +321,55 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Enumerate.
+    macro_rules! generate_enumerate_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Enumerate<
+                                crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> $ty>,
+                            > as crate::iter::Iterator>::__iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let count: usize = kani::any();
+                let end: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (count..end).map(move |_| value);
+                let mut iter = Enumerate { iter: source, count };
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                let len = end - count;
+                kani::cover(count == 0 && idx == 0, "first element");
+                kani::cover(
+                    count > 0 && idx > 0 && idx < len - 1,
+                    "interior element after a prefix",
+                );
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(count == usize::MAX - 1 && idx == 0, "large enumeration offset");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i8, i8);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i16, i16);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i32, i32);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i64, i64);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i128, i128);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u8, u8);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u16, u16);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u32, u32);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u64, u64);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u128, u128);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_array, [u8; 4]);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_bool, bool);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_unit, ());
+}

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

@@ -5,6 +5,8 @@ use core::ops::ControlFlow;
 use crate::fmt;
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
@@ -251,3 +253,41 @@ impl<I: TrustedLen> SpecAssumeCount for I {
         unsafe { crate::hint::assert_unchecked(count <= upper) }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `next_chunk_dropless` for Filter
+    macro_rules! generate_next_chunk_dropless_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Use a fixed-size source so the underlying iterator loop is bounded.
+                let values: [$ty; 4] = kani::any();
+                let source: crate::array::IntoIter<$ty, 4> = values.into_iter();
+
+                // Choose each filtering decision nondeterministically.
+                let mut filter = Filter::new(source, |_: &$ty| kani::any());
+
+                // Exercise both the full-chunk and partial-chunk result paths.
+                let _ = filter.next_chunk_dropless::<4>();
+            }
+        };
+    }
+
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i8, i8);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i16, i16);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i32, i32);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i64, i64);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i128, i128);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u8, u8);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u16, u16);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u32, u32);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u64, u64);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u128, u128);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_array, [u8; 4]);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_bool, bool);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_unit, ());
+}