Challenge 16: Verify safety of iterator adapter functions with Kani

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,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
@@ -274,3 +285,83 @@ 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]
+            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

@@ -152,6 +152,8 @@ where
     I: UncheckedIterator<Item = &'a T>,
     T: Clone,
 {
+    #[cfg_attr(kani, kani::requires(self.size_hint().0 != 0))]
+    #[cfg_attr(kani, kani::modifies(self))]
     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 +195,109 @@ 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.
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_cloned_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Generate a symbolic access index.
+                let idx: usize = kani::any();
+                // Generate an arbitrary element to clone.
+                let value: $ty = kani::any();
+                // Record the index actually received by the inner iterator.
+                let observed_idx = crate::cell::Cell::new(usize::MAX);
+
+                // Build a lazy iterator of length `len` without allocating `len` elements.
+                let source = (0..len).map(|i| {
+                    // Save the index forwarded by the random-access operation.
+                    observed_idx.set(i);
+                    // Make the inner iterator's item type `&T`.
+                    &value
+                });
+                // Construct the target `Cloned<I>` from the inner iterator.
+                let mut iter = Cloned::new(source);
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save the iterator size before the call.
+                let size_before = iter.size_hint();
+
+                // Call the target `Cloned<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that the target forwarded `idx` exactly.
+                assert_eq!(observed_idx.get(), idx);
+                // Check that the returned value is the correct clone of the inner `&T`.
+                assert_eq!(result, value);
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    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, ());
+
+    // Harnesses for `next_unchecked` for Cloned.
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_cloned_next_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate an arbitrary element to clone.
+                let value: $ty = kani::any();
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Build an exact-length iterator without allocating `len` elements.
+                let source = crate::iter::repeat_n(&value, len);
+                // Construct the target `Cloned<I>` from the inner iterator.
+                let mut iter = Cloned::new(source);
+
+                // Express the target's `self.size_hint().0 != 0` precondition.
+                kani::assume(iter.size_hint().0 != 0);
+
+                // Call the target `Cloned<I>` implementation through the trait path.
+                let result = unsafe { UncheckedIterator::next_unchecked(&mut iter) };
+
+                // Check that the returned value is the correct clone of the inner `&T`.
+                assert_eq!(result, value);
+                // Check that the call consumed exactly one element.
+                assert_eq!(iter.size_hint(), (len - 1, Some(len - 1)));
+            }
+        };
+    }
+
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i8, i8);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i16, i16);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i32, i32);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i64, i64);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i128, i128);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u8, u8);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u16, u16);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u32, u32);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u64, u64);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u128, u128);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_array, [u8; 4]);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_bool, bool);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_unit, ());
+}

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

@@ -284,3 +284,108 @@ 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
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_copied_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate symbolic inputs with no explicit length bound.
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+
+                // Record the index received by the inner iterator.
+                let observed_idx = crate::cell::Cell::new(usize::MAX);
+
+                // Build a lazy trusted-random-access iterator yielding `&T`.
+                let source = (0..len).map(|i| {
+                    observed_idx.set(i);
+                    &value
+                });
+                let mut iter = Copied::new(source);
+
+                // Express `idx < self.size()`.
+                kani::assume(idx < iter.size_hint().0);
+                let size_before = iter.size_hint();
+
+                // Call the target `Copied<I>` implementation.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check exact index forwarding.
+                assert_eq!(observed_idx.get(), idx);
+                // Check the copied result.
+                assert_eq!(result, value);
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    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);
+    }
+}