From d49fbc24a66d3f806da11bff74842d3107c0be57 Mon Sep 17 00:00:00 2001 From: v3risec Date: Tue, 11 Aug 2026 15:20:19 +0800 Subject: [PATCH 1/2] Add Kani verification code for challenge 16 --- .../core/src/iter/adapters/array_chunks.rs | 91 ++++ library/core/src/iter/adapters/cloned.rs | 108 +++++ library/core/src/iter/adapters/copied.rs | 105 +++++ library/core/src/iter/adapters/enumerate.rs | 68 +++ library/core/src/iter/adapters/filter.rs | 40 ++ library/core/src/iter/adapters/filter_map.rs | 46 ++ library/core/src/iter/adapters/fuse.rs | 66 +++ library/core/src/iter/adapters/map.rs | 127 ++++++ library/core/src/iter/adapters/map_windows.rs | 157 +++++++ library/core/src/iter/adapters/skip.rs | 145 ++++++ library/core/src/iter/adapters/step_by.rs | 19 + library/core/src/iter/adapters/take.rs | 82 ++++ library/core/src/iter/adapters/zip.rs | 419 ++++++++++++++++++ 13 files changed, 1473 insertions(+) diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs index 967136288865c..e56c2df945569 100644 --- a/library/core/src/iter/adapters/array_chunks.rs +++ b/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 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, ()); +} diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs index 0f05260059880..7b298ffc465ed 100644 --- a/library/core/src/iter/adapters/cloned.rs +++ b/library/core/src/iter/adapters/cloned.rs @@ -152,6 +152,8 @@ where I: UncheckedIterator, 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 InPlaceIterable for Cloned { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = 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` 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` 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` 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` 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, ()); +} diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs index 3db6c5dafd400..fd4cdd8f27317 100644 --- a/library/core/src/iter/adapters/copied.rs +++ b/library/core/src/iter/adapters/copied.rs @@ -284,3 +284,108 @@ unsafe impl InPlaceIterable for Copied { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = 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` 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 _ = 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 _ = + as SpecNextChunk<'_, 4, ()>>::spec_next_chunk(&mut iter); + } +} diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs index e7e18d178031f..f9a01555e180e 100644 --- a/library/core/src/iter/adapters/enumerate.rs +++ b/library/core/src/iter/adapters/enumerate.rs @@ -321,3 +321,71 @@ impl Default for Enumerate { Enumerate::new(Default::default()) } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `__iterator_get_unchecked` for enumerate + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + macro_rules! generate_enumerate_get_unchecked_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Generate a symbolic enumeration offset. + let count: usize = kani::any(); + // Generate a symbolic relative access index. + let idx: usize = kani::any(); + // Generate an arbitrary inner item. + let value: $ty = kani::any(); + // Record the absolute position reached by the inner iterator. + let observed_position = crate::cell::Cell::new(usize::MAX); + + // Model the remaining range after `count` items without allocating elements. + let source = (count..usize::MAX).map(|position| { + // Record which inner element the target actually requested. + observed_position.set(position); + value + }); + // Build a valid `Enumerate` state with a symbolic offset. + let mut iter = Enumerate { iter: source, count }; + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < iter.size_hint().0); + // Save observable iterator state before random access. + let count_before = iter.next_index(); + let size_before = iter.size_hint(); + + // Call the target `Enumerate` implementation through the trait path. + let result = + unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + + // Check that the relative `idx` reached the correct absolute position. + assert_eq!(observed_position.get(), count_before + idx); + // Check the enumeration index added by the target. + assert_eq!(result.0, count_before + idx); + // Check that the inner item was forwarded unchanged. + assert_eq!(result.1, value); + // Check that random access did not advance the enumeration count. + assert_eq!(iter.next_index(), count_before); + // Check that random access did not consume the iterator. + assert_eq!(iter.size_hint(), size_before); + } + }; + } + + 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, ()); +} diff --git a/library/core/src/iter/adapters/filter.rs b/library/core/src/iter/adapters/filter.rs index dd08cd6f61c4c..c0b502dcdcf1b 100644 --- a/library/core/src/iter/adapters/filter.rs +++ b/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}; +#[cfg(kani)] +use crate::kani; use crate::num::NonZero; use crate::ops::Try; @@ -214,3 +216,41 @@ unsafe impl InPlaceIterable for Filter { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[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, ()); +} diff --git a/library/core/src/iter/adapters/filter_map.rs b/library/core/src/iter/adapters/filter_map.rs index 24ec6b1741ce1..5dfd7b3977a1f 100644 --- a/library/core/src/iter/adapters/filter_map.rs +++ b/library/core/src/iter/adapters/filter_map.rs @@ -1,5 +1,7 @@ use crate::iter::adapters::SourceIter; use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused}; +#[cfg(kani)] +use crate::kani; use crate::mem::{ManuallyDrop, MaybeUninit}; use crate::num::NonZero; use crate::ops::{ControlFlow, Try}; @@ -211,3 +213,47 @@ unsafe impl InPlaceIterable for FilterMap { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `next_chunk` for FilterMap + macro_rules! generate_next_chunk_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 whether each input is mapped to Some or filtered out as None. + let mut filter_map = + FilterMap::new( + source, + |element: $ty| { + if kani::any::() { Some(element) } else { None } + }, + ); + + // Exercise both the full-chunk and partial-chunk result paths. + let _ = filter_map.next_chunk::<4>(); + } + }; + } + + generate_next_chunk_harness!(harness_next_chunk_i8, i8); + generate_next_chunk_harness!(harness_next_chunk_i16, i16); + generate_next_chunk_harness!(harness_next_chunk_i32, i32); + generate_next_chunk_harness!(harness_next_chunk_i64, i64); + generate_next_chunk_harness!(harness_next_chunk_i128, i128); + generate_next_chunk_harness!(harness_next_chunk_u8, u8); + generate_next_chunk_harness!(harness_next_chunk_u16, u16); + generate_next_chunk_harness!(harness_next_chunk_u32, u32); + generate_next_chunk_harness!(harness_next_chunk_u64, u64); + generate_next_chunk_harness!(harness_next_chunk_u128, u128); + generate_next_chunk_harness!(harness_next_chunk_array, [u8; 4]); + generate_next_chunk_harness!(harness_next_chunk_bool, bool); + generate_next_chunk_harness!(harness_next_chunk_unit, ()); +} diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs index fcad6168d85cd..86008a4f60e68 100644 --- a/library/core/src/iter/adapters/fuse.rs +++ b/library/core/src/iter/adapters/fuse.rs @@ -478,3 +478,69 @@ fn and_then_or_clear(opt: &mut Option, f: impl FnOnce(&mut T) -> Option } x } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `__iterator_get_unchecked` for Fuse + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + macro_rules! generate_fuse_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 inner item. + 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(|position| { + // Record which inner element the target actually requested. + observed_idx.set(position); + value + }); + // Construct an active `Fuse` whose inner state is `Some(source)`. + let mut iter = Fuse::new(source); + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < iter.size_hint().0); + // Save observable iterator state before random access. + let size_before = iter.size_hint(); + assert!(iter.iter.is_some()); + + // Call the target `Fuse` 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 inner item was forwarded unchanged. + assert_eq!(result, value); + // Check that random access kept the inner iterator active. + assert!(iter.iter.is_some()); + // Check that random access did not consume the iterator. + assert_eq!(iter.size_hint(), size_before); + } + }; + } + + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i8, i8); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i16, i16); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i32, i32); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i64, i64); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i128, i128); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u8, u8); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u16, u16); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u32, u32); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u64, u64); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u128, u128); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_array, [u8; 4]); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_bool, bool); + generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_unit, ()); +} diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs index bf9f0c48fec3b..9e657f2342c21 100644 --- a/library/core/src/iter/adapters/map.rs +++ b/library/core/src/iter/adapters/map.rs @@ -134,6 +134,7 @@ where #[inline] #[requires(idx < self.iter.size_hint().0)] + #[cfg_attr(kani, kani::modifies(self))] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> B where Self: TrustedRandomAccessNoCoerce, @@ -205,6 +206,7 @@ where F: FnMut(I::Item) -> B, { #[requires(self.iter.size_hint().0 > 0)] + #[cfg_attr(kani, kani::modifies(self))] unsafe fn next_unchecked(&mut self) -> B { // SAFETY: `Map` is 1:1 with the inner iterator, so if the caller promised // that there's an element left, the inner iterator has one too. @@ -245,3 +247,128 @@ unsafe impl InPlaceIterable for Map { const EXPAND_BY: Option> = I::EXPAND_BY; const MERGE_BY: Option> = I::MERGE_BY; } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `__iterator_get_unchecked` for Map + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + macro_rules! generate_map_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 arbitrary data captured by the mapping closure. + let value: $ty = kani::any(); + // Record the inner item passed to the mapping closure. + let observed_input = crate::cell::Cell::new(usize::MAX); + // Count how many times the target invokes the mapping closure. + let closure_calls = crate::cell::Cell::new(0usize); + + // Use the range item itself as the observable inner position. + let source = 0..len; + // Construct the target with a stateful, type-changing closure. + let mut iter = Map::new(source, |position| { + observed_input.set(position); + closure_calls.set(closure_calls.get() + 1); + (value, position, closure_calls.get()) + }); + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < iter.size_hint().0); + // Save the iterator size before random access. + let size_before = iter.size_hint(); + + // Call the target `Map` implementation through the trait path. + let result = + unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + + // Check that the target forwarded `idx` to the inner range exactly. + assert_eq!(observed_input.get(), idx); + // Check that the target invoked the mapping closure exactly once. + assert_eq!(closure_calls.get(), 1); + // Check the closure input, captured value, and stateful output. + assert_eq!(result, (value, idx, 1)); + // Check that random access did not consume the iterator. + assert_eq!(iter.size_hint(), size_before); + } + }; + } + + generate_map_get_unchecked_harness!(harness_map_get_unchecked_i8, i8); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_i16, i16); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_i32, i32); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_i64, i64); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_i128, i128); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_u8, u8); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_u16, u16); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_u32, u32); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_u64, u64); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_u128, u128); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_array, [u8; 4]); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_bool, bool); + generate_map_get_unchecked_harness!(harness_map_get_unchecked_unit, ()); + + // Harnesses for `next_unchecked` for Map + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + macro_rules! generate_map_next_unchecked_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Generate arbitrary data captured by the mapping closure. + let value: $ty = kani::any(); + // Generate an arbitrary inner item. + let inner_value: usize = kani::any(); + // Generate a symbolic logical length with no explicit upper bound. + let len: usize = kani::any(); + // Record the inner item passed to the mapping closure. + let observed_input = crate::cell::Cell::new(usize::MAX); + // Count how many times the target invokes the mapping closure. + let closure_calls = crate::cell::Cell::new(0usize); + + // Build an exact-length iterator without allocating `len` elements. + let source = crate::iter::repeat_n(inner_value, len); + // Construct the target with a stateful, type-changing closure. + let mut iter = Map::new(source, |item| { + observed_input.set(item); + closure_calls.set(closure_calls.get() + 1); + (value, item, closure_calls.get()) + }); + + // Express the target's non-empty precondition. + kani::assume(iter.size_hint().0 > 0); + + // Call the target `Map` implementation through the trait path. + let result = unsafe { UncheckedIterator::next_unchecked(&mut iter) }; + + // Check that the closure received the consumed inner item. + assert_eq!(observed_input.get(), inner_value); + // Check that the target invoked the mapping closure exactly once. + assert_eq!(closure_calls.get(), 1); + // Check the closure input, captured value, and stateful output. + assert_eq!(result, (value, inner_value, 1)); + // Check that the target consumed exactly one inner element. + assert_eq!(iter.size_hint(), (len - 1, Some(len - 1))); + } + }; + } + + generate_map_next_unchecked_harness!(harness_map_next_unchecked_i8, i8); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_i16, i16); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_i32, i32); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_i64, i64); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_i128, i128); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_u8, u8); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_u16, u16); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_u32, u32); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_u64, u64); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_u128, u128); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_array, [u8; 4]); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_bool, bool); + generate_map_next_unchecked_harness!(harness_map_next_unchecked_unit, ()); +} diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs index 536251a137da0..b02af53890312 100644 --- a/library/core/src/iter/adapters/map_windows.rs +++ b/library/core/src/iter/adapters/map_windows.rs @@ -1,4 +1,6 @@ use crate::iter::FusedIterator; +#[cfg(kani)] +use crate::kani; use crate::mem::MaybeUninit; use crate::ub_checks::Invariant; use crate::{fmt, ptr}; @@ -297,3 +299,158 @@ impl Invariant for Buffer { self.start + N <= 2 * N } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + fn any_buffer() -> (Buffer, [T; N]) { + // Symbolize a valid starting position for the active window. + let start = kani::any_where(|start: &usize| *start <= N); + + // Symbolize the values that occupy the active window. + let values: [T; N] = kani::any(); + let mut storage = [[MaybeUninit::uninit(); N]; 2]; + + // Initialize exactly storage[start .. start + N] without raw pointers. + for offset in 0..N { + let index = start + offset; + if index < N { + storage[0][index].write(values[offset]); + } else { + storage[1][index - N].write(values[offset]); + } + } + + (Buffer { buffer: storage, start }, values) + } + + // Harnesses for `as_array_ref` for Buffer + macro_rules! generate_buffer_as_array_ref_harness { + ($name:ident, $ty:ty, $n:expr) => { + #[kani::proof] + fn $name() { + // Build a symbolic Buffer satisfying its representation invariant. + let (buffer, expected) = any_buffer::<$ty, $n>(); + + // Call the safe function under test. + let window = buffer.as_array_ref(); + } + }; + } + + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u8_n1, u8, 1); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u8_n2, u8, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u8_n4, u8, 4); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u16, u16, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u32, u32, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u64, u64, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u128, u128, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i8, i8, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i16, i16, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i32, i32, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i64, i64, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i128, i128, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_bool, bool, 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_unit, (), 2); + generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_array, [u8; 4], 2); + + // Harnesses for `as_uninit_array_mut` for Buffer + macro_rules! generate_buffer_as_uninit_array_mut_harness { + ($name:ident, $ty:ty, $n:expr) => { + #[kani::proof] + fn $name() { + // Build a valid symbolic Buffer without raw pointers. + let (mut buffer, _) = any_buffer::<$ty, $n>(); + + // Symbolize a fully initialized replacement window. + let replacement: [$ty; $n] = kani::any(); + + // Write through the safe function's returned MaybeUninit reference. + buffer.as_uninit_array_mut().write(replacement); + } + }; + } + + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u8_n1, u8, 1); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u8_n2, u8, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u8_n4, u8, 4); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u16, u16, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u32, u32, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u64, u64, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u128, u128, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i8, i8, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i16, i16, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i32, i32, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i64, i64, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i128, i128, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_bool, bool, 2); + generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_unit, (), 2); + generate_buffer_as_uninit_array_mut_harness!( + harness_buffer_as_uninit_array_mut_array, + [u8; 4], + 2 + ); + + // Harnesses for `push` for Buffer. + macro_rules! generate_buffer_push_harness { + ($name:ident, $ty:ty, $n:expr) => { + #[kani::proof] + fn $name() { + // Build a valid Buffer with a symbolic active-window position. + let (mut buffer, before) = any_buffer::<$ty, $n>(); + // Symbolize the item appended to the window. + let next: $ty = kani::any(); + // Call the safe function under test. + buffer.push(next); + } + }; + } + + generate_buffer_push_harness!(harness_buffer_push_u8_n1, u8, 1); + generate_buffer_push_harness!(harness_buffer_push_u8_n2, u8, 2); + generate_buffer_push_harness!(harness_buffer_push_u8_n4, u8, 4); + generate_buffer_push_harness!(harness_buffer_push_u16, u16, 2); + generate_buffer_push_harness!(harness_buffer_push_u32, u32, 2); + generate_buffer_push_harness!(harness_buffer_push_u64, u64, 2); + generate_buffer_push_harness!(harness_buffer_push_u128, u128, 2); + generate_buffer_push_harness!(harness_buffer_push_i8, i8, 2); + generate_buffer_push_harness!(harness_buffer_push_i16, i16, 2); + generate_buffer_push_harness!(harness_buffer_push_i32, i32, 2); + generate_buffer_push_harness!(harness_buffer_push_i64, i64, 2); + generate_buffer_push_harness!(harness_buffer_push_i128, i128, 2); + generate_buffer_push_harness!(harness_buffer_push_bool, bool, 2); + generate_buffer_push_harness!(harness_buffer_push_unit, (), 2); + generate_buffer_push_harness!(harness_buffer_push_array, [u8; 4], 2); + + // Harnesses for `Drop::drop` for Buffer. + macro_rules! generate_buffer_drop_harness { + ($name:ident, $ty:ty, $n:expr) => { + #[kani::proof] + fn $name() { + // Build a valid Buffer with a symbolic active-window position. + let (buffer, _) = any_buffer::<$ty, $n>(); + + // Invoke Buffer::drop through the safe drop function. + crate::mem::drop(buffer); + } + }; + } + + generate_buffer_drop_harness!(harness_buffer_drop_u8_n1, u8, 1); + generate_buffer_drop_harness!(harness_buffer_drop_u8_n2, u8, 2); + generate_buffer_drop_harness!(harness_buffer_drop_u8_n4, u8, 4); + generate_buffer_drop_harness!(harness_buffer_drop_u16, u16, 2); + generate_buffer_drop_harness!(harness_buffer_drop_u32, u32, 2); + generate_buffer_drop_harness!(harness_buffer_drop_u64, u64, 2); + generate_buffer_drop_harness!(harness_buffer_drop_u128, u128, 2); + generate_buffer_drop_harness!(harness_buffer_drop_i8, i8, 2); + generate_buffer_drop_harness!(harness_buffer_drop_i16, i16, 2); + generate_buffer_drop_harness!(harness_buffer_drop_i32, i32, 2); + generate_buffer_drop_harness!(harness_buffer_drop_i64, i64, 2); + generate_buffer_drop_harness!(harness_buffer_drop_i128, i128, 2); + generate_buffer_drop_harness!(harness_buffer_drop_bool, bool, 2); + generate_buffer_drop_harness!(harness_buffer_drop_unit, (), 2); + generate_buffer_drop_harness!(harness_buffer_drop_array, [u8; 4], 2); +} diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs index ac3cc4c4f1152..c09117bc78ad3 100644 --- a/library/core/src/iter/adapters/skip.rs +++ b/library/core/src/iter/adapters/skip.rs @@ -180,6 +180,18 @@ where // before something is written into the storage used by the prefix unsafe { if Self::MAY_HAVE_SIDE_EFFECT && idx == 0 { + #[cfg(kani)] + let inner_size_hint = self.iter.size_hint(); + // The outer precondition and `idx == 0` imply `self.n < inner_size_hint.0`. + // Random access may mutate the inner iterator, but it must preserve its size. + #[cfg_attr( + kani, + kani::loop_invariant( + kani::index <= self.n + && self.n < inner_size_hint.0 + && self.iter.size_hint() == inner_size_hint + ) + )] for skipped_idx in 0..self.n { drop(try_get_unchecked(&mut self.iter, skipped_idx)); } @@ -293,3 +305,136 @@ where // I: TrustedLen would not. #[unstable(feature = "trusted_len", issue = "37572")] unsafe impl TrustedLen for Skip where I: Iterator + TrustedRandomAccess {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `__iterator_get_unchecked` for Skip + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + macro_rules! generate_skip_get_unchecked_unbounded_harness { + ($name:ident) => { + #[kani::proof] + pub fn $name() { + // Generate a symbolic pending skip count. + let n: usize = kani::any(); + // Generate a symbolic index in the shortened iterator. + let idx: usize = kani::any(); + + // Use a maximal lazy range with no random-access side effects. + let source = 0..usize::MAX; + // Construct the target with a symbolic skip offset. + let mut iter = Skip::new(source, n); + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < iter.size_hint().0); + // Save observable iterator state before random access. + let n_before = iter.n; + let size_before = iter.size_hint(); + + // Call the target `Skip` implementation through the trait path. + let result = + unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + + // Check that `Skip` translated the outer index to `n + idx`. + assert_eq!(result, n + idx); + // Check that random access did not consume the pending skip count. + assert_eq!(iter.n, n_before); + // Check that random access did not consume the iterator. + assert_eq!(iter.size_hint(), size_before); + } + }; + } + + // Cover Copy item types with core's non-side-effecting array iterator + macro_rules! generate_skip_get_unchecked_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Generate a symbolic pending skip count and outer index. + let n: usize = kani::any(); + let idx: usize = kani::any(); + // Generate four independent symbolic values of the selected item type. + let values: [$ty; 4] = kani::any(); + // Keep a Copy snapshot for checking the translated index. + let expected_values = values; + + // Use core's generic trusted-random-access iterator with no side effects. + let source: crate::array::IntoIter<$ty, 4> = values.into_iter(); + // Construct the target with a symbolic skip offset. + let mut iter = Skip::new(source, n); + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < iter.size_hint().0); + // The precondition guarantees that `n + idx` indexes the original array. + let expected = expected_values[n + idx]; + // Save observable iterator state before random access. + let n_before = iter.n; + let size_before = iter.size_hint(); + + // Call the target `Skip` implementation through the trait path. + let result = + unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + + // Check that `Skip` selected the original element at `n + idx`. + assert_eq!(result, expected); + // Check that random access did not consume the adapter state. + assert_eq!(iter.n, n_before); + assert_eq!(iter.size_hint(), size_before); + } + }; + } + + // Cover side-effecting path + macro_rules! generate_skip_get_unchecked_side_effect_harness { + ($name:ident) => { + #[kani::proof] + pub fn $name() { + // Generate a symbolic pending skip count. + let n: usize = kani::any(); + // Generate a symbolic index in the shortened iterator. + let idx: usize = kani::any(); + + // `Map` sets `MAY_HAVE_SIDE_EFFECT = true` for every mapping closure, + // so this selects `Skip`'s side-effecting random-access branch. + // Keep the closure stateless because this harness does not track exact effects. + let source = (0..usize::MAX).map(|position| position); + // Construct the target with a symbolic skip offset. + let mut iter = Skip::new(source, n); + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < iter.size_hint().0); + // Save observable iterator state before random access. + let n_before = iter.n; + let size_before = iter.size_hint(); + + // Call the target `Skip` implementation through the trait path. + let result = + unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + + // Check that `Skip` translated the outer index to `n + idx`. + assert_eq!(result, n + idx); + // Check that random access did not consume the adapter state. + assert_eq!(iter.n, n_before); + assert_eq!(iter.size_hint(), size_before); + } + }; + } + + generate_skip_get_unchecked_unbounded_harness!(harness_skip_get_unchecked_unbounded); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i8, i8); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i16, i16); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i32, i32); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i64, i64); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i128, i128); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u8, u8); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u16, u16); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u32, u32); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u64, u64); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u128, u128); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_array, [u8; 4]); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_bool, bool); + generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_unit, ()); + generate_skip_get_unchecked_side_effect_harness!(harness_skip_get_unchecked_side_effect); +} diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index 32604a07ca40c..bca59ec4117e8 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -589,3 +589,22 @@ spec_int_ranges_r!(u8 u16 u32 usize); spec_int_ranges!(u8 u16 usize); #[cfg(target_pointer_width = "16")] spec_int_ranges_r!(u8 u16 usize); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harness for `original_step` for StepBy. + #[kani::proof] + fn harness_step_by_original_step() { + // StepBy::new requires a nonzero step. + let step = kani::any_where(|step: &usize| *step != 0); + + // The inner iterator is irrelevant to original_step. + let step_by = StepBy::new((), step); + + // Call the safe function under test. + let _ = step_by.original_step(); + } +} diff --git a/library/core/src/iter/adapters/take.rs b/library/core/src/iter/adapters/take.rs index b96335f415257..2a4c98658bf87 100644 --- a/library/core/src/iter/adapters/take.rs +++ b/library/core/src/iter/adapters/take.rs @@ -1,6 +1,8 @@ use crate::cmp; use crate::iter::adapters::SourceIter; use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, TrustedRandomAccess}; +#[cfg(kani)] +use crate::kani; use crate::num::NonZero; use crate::ops::{ControlFlow, Try}; @@ -299,6 +301,7 @@ impl SpecTake for Take { { let mut acc = init; let end = self.n.min(self.iter.size()); + #[cfg_attr(kani, kani::loop_invariant(end <= self.iter.size()))] for i in 0..end { // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end let val = unsafe { self.iter.__iterator_get_unchecked(i) }; @@ -310,6 +313,7 @@ impl SpecTake for Take { #[inline] fn spec_for_each(mut self, mut f: F) { let end = self.n.min(self.iter.size()); + #[cfg_attr(kani, kani::loop_invariant(end <= self.iter.size()))] for i in 0..end { // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end let val = unsafe { self.iter.__iterator_get_unchecked(i) }; @@ -374,3 +378,81 @@ impl A, A> ExactSizeIterator for Take> self.n } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `spec_fold` for Take. + macro_rules! generate_take_spec_fold_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + fn $name() { + // Symbolize the logical iterator length without an explicit bound. + let len: usize = kani::any(); + + // Symbolize the take count independently of the iterator length. + let n: usize = kani::any(); + + // Map retains TrustedRandomAccess while generalizing the item type. + let value: $ty = kani::any(); + let source = (0..len).map(move |_| value); + let taken = Take::new(source, n); + + // Call the specialized safe function under test. + SpecTake::spec_fold(taken, (), |(), _item| ()); + } + }; + } + + generate_take_spec_fold_harness!(harness_take_spec_fold_i8, i8); + generate_take_spec_fold_harness!(harness_take_spec_fold_i16, i16); + generate_take_spec_fold_harness!(harness_take_spec_fold_i32, i32); + generate_take_spec_fold_harness!(harness_take_spec_fold_i64, i64); + generate_take_spec_fold_harness!(harness_take_spec_fold_i128, i128); + generate_take_spec_fold_harness!(harness_take_spec_fold_u8, u8); + generate_take_spec_fold_harness!(harness_take_spec_fold_u16, u16); + generate_take_spec_fold_harness!(harness_take_spec_fold_u32, u32); + generate_take_spec_fold_harness!(harness_take_spec_fold_u64, u64); + generate_take_spec_fold_harness!(harness_take_spec_fold_u128, u128); + generate_take_spec_fold_harness!(harness_take_spec_fold_bool, bool); + generate_take_spec_fold_harness!(harness_take_spec_fold_unit, ()); + generate_take_spec_fold_harness!(harness_take_spec_fold_array, [u8; 4]); + + // Harnesses for `spec_for_each` for Take. + macro_rules! generate_take_spec_for_each_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + fn $name() { + // Symbolize the logical iterator length without an explicit bound. + let len: usize = kani::any(); + + // Symbolize the take count independently of the iterator length. + let n: usize = kani::any(); + + // Map retains TrustedRandomAccess while generalizing the item type. + let value: $ty = kani::any(); + let source = (0..len).map(move |_| value); + let taken = Take::new(source, n); + + // Call the specialized safe function under test. + SpecTake::spec_for_each(taken, |_item| ()); + } + }; + } + + generate_take_spec_for_each_harness!(harness_take_spec_for_each_i8, i8); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_i16, i16); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_i32, i32); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_i64, i64); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_i128, i128); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_u8, u8); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_u16, u16); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_u32, u32); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_u64, u64); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_u128, u128); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_bool, bool); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_unit, ()); + generate_take_spec_for_each_harness!(harness_take_spec_for_each_array, [u8; 4]); +} diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs index e39f1535bd95d..242a84d406d59 100644 --- a/library/core/src/iter/adapters/zip.rs +++ b/library/core/src/iter/adapters/zip.rs @@ -28,6 +28,23 @@ impl Zip { ZipImpl::new(a, b) } fn super_nth(&mut self, mut n: usize) -> Option<(A::Item, B::Item)> { + #[cfg_attr( + kani, + kani::loop_invariant( + self.index <= self.len + && self.len <= self.a.size_hint().0 + && self.len <= self.b.size_hint().0 + ) + )] + #[cfg_attr( + kani, + kani::loop_modifies( + &mut self.a, + &mut self.b, + &mut self.index, + &mut n + ) + )] while let Some(x) = Iterator::next(self) { if n == 0 { return Some(x); @@ -270,6 +287,7 @@ where } #[inline] + #[cfg_attr(kani, kani::requires(idx < TrustedRandomAccessNoCoerce::size(self)))] #[cfg_attr(kani, kani::modifies(self))] unsafe fn get_unchecked(&mut self, idx: usize) -> ::Item { let idx = self.index + idx; @@ -285,6 +303,18 @@ where { let mut accum = init; let len = ZipImpl::size_hint(&self).0; + #[cfg_attr( + kani, + kani::loop_invariant( + kani::index <= len + && len <= ZipImpl::size_hint(&self).0 + && self.index <= self.a.size() + && len <= self.a.size() - self.index + && self.index <= self.b.size() + && len <= self.b.size() - self.index + ) + )] + #[cfg_attr(kani, kani::loop_modifies(&self, &accum, &f))] for i in 0..len { // SAFETY: since Self: TrustedRandomAccessNoCoerce we can trust the size-hint to // calculate the length and then use that to do unchecked iteration. @@ -334,6 +364,19 @@ where fn nth(&mut self, n: usize) -> Option { let delta = cmp::min(n, self.len - self.index); let end = self.index + delta; + #[cfg_attr( + kani, + kani::loop_invariant( + self.index <= end + && end <= self.len + && self.len <= self.a.size() + && self.len <= self.b.size() + ) + )] + #[cfg_attr( + kani, + kani::loop_modifies(&mut self.index, &mut self.a, &mut self.b) + )] while self.index < end { let i = self.index; // since get_unchecked executes code which can panic we increment the counters beforehand @@ -669,6 +712,8 @@ impl SpecFold for Zip { F: FnMut(Acc, Self::Item) -> Acc, { let mut accum = init; + + #[cfg(not(kani))] loop { let (upper, more) = if let Some(upper) = ZipImpl::size_hint(&self).1 { (upper, false) @@ -689,6 +734,380 @@ impl SpecFold for Zip { break; } } + + // Loop stub: choose one arbitrary iteration from a chunk + // and preserve the unchecked-access safety check without a + // writeset over generic iterator structs. + #[cfg(kani)] + { + let upper = ZipImpl::size_hint(&self).1.unwrap_or(usize::MAX); + if upper != 0 { + let index: usize = kani::any(); + kani::assume(index < upper); + let pair = unsafe { + (self.a.nth(index).unwrap_unchecked(), self.b.nth(index).unwrap_unchecked()) + }; + accum = f(accum, pair); + } + } + accum } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Harnesses for `__iterator_get_unchecked` for ZipImpl. + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + // Use core's non-side-effecting `Copied>` for item-type coverage. + macro_rules! generate_zip_iterator_get_unchecked_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Generate independent symbolic values for both sides. + let left: [$ty; 4] = kani::any(); + let right: [$ty; 4] = kani::any(); + // Generate a symbolic reachable offset and remaining-relative index. + let index: usize = kani::any(); + let idx: usize = kani::any(); + + // `Copied>` implements full trusted random access. + let mut zip = Zip::new(left.iter().copied(), right.iter().copied()); + // Specialized `next` changes only `index`, so this models a reachable state. + kani::assume(index <= zip.len); + zip.index = index; + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip)); + let absolute_idx = index + idx; + let expected = (left[absolute_idx], right[absolute_idx]); + // Save observable `Zip` state before random access. + let index_before = zip.index; + let len_before = zip.len; + let size_before = Iterator::size_hint(&zip); + + // Call the outer `Iterator` target through its trait path. + let result = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) }; + + // Check both values at the translated absolute index. + assert_eq!(result, expected); + // Check that random access did not consume the zipped iterator. + assert_eq!(zip.index, index_before); + assert_eq!(zip.len, len_before); + assert_eq!(Iterator::size_hint(&zip), size_before); + } + }; + } + + #[kani::proof] + fn harness_zip_iterator_get_unchecked_unbounded() { + // Generate independent symbolic lengths for both inner iterators. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + // Generate a symbolic reachable offset in the specialized `Zip` state. + let index: usize = kani::any(); + // Generate a symbolic index relative to the remaining zipped iterator. + let idx: usize = kani::any(); + + // Use core ranges to keep both input lengths unbounded by a harness constant. + let mut zip = Zip::new(0..left_len, 0..right_len); + // Specialized `next` reaches this state by changing only `index`. + kani::assume(index <= zip.len); + zip.index = index; + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip)); + let absolute_idx = index + idx; + // Save all observable iterator state before random access. + let index_before = zip.index; + let len_before = zip.len; + let left_size_before = zip.a.size_hint(); + let right_size_before = zip.b.size_hint(); + let size_before = Iterator::size_hint(&zip); + + // Call the outer `Iterator` target, which delegates to `ZipImpl`. + let result = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) }; + + // Check that both sides received the same translated absolute index. + assert_eq!(result, (absolute_idx, absolute_idx)); + // Check that random access did not consume or resize any iterator state. + assert_eq!(zip.index, index_before); + assert_eq!(zip.len, len_before); + assert_eq!(zip.a.size_hint(), left_size_before); + assert_eq!(zip.b.size_hint(), right_size_before); + assert_eq!(Iterator::size_hint(&zip), size_before); + } + + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i8, i8); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i16, i16); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i32, i32); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i64, i64); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i128, i128); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u8, u8); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u16, u16); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u32, u32); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u64, u64); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u128, u128); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_array, [u8; 4]); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_bool, bool); + generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_unit, ()); + + // Harnesses for `get_unchecked` for ZipImpl. + // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + // Use stateless maps to combine unbounded positions with symbolic Copy payloads. + macro_rules! generate_zip_get_unchecked_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Generate independent symbolic lengths and payloads for both sides. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); + let left_expected = left_value; + let right_expected = right_value; + // Generate a symbolic reachable offset and remaining-relative index. + let index: usize = kani::any(); + let idx: usize = kani::any(); + + // Preserve each absolute position while attaching a symbolic payload. + // These closures copy captured values without mutating any state. + let left = (0..left_len).map(move |position| (position, left_value)); + let right = (0..right_len).map(move |position| (position, right_value)); + let mut zip = Zip::new(left, right); + + // Full trusted-random-access `Zip::next` changes only `index`. + kani::assume(index <= zip.len); + zip.index = index; + + // Express the target's `idx < self.size()` precondition. + kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip)); + let absolute_idx = index + idx; + let expected = ((absolute_idx, left_expected), (absolute_idx, right_expected)); + // Save all observable state before the internal random-access call. + let index_before = zip.index; + let len_before = zip.len; + let left_size_before = zip.a.size_hint(); + let right_size_before = zip.b.size_hint(); + let size_before = Iterator::size_hint(&zip); + + // Call the internal target directly rather than the outer `Iterator` method. + let result = unsafe { ZipImpl::get_unchecked(&mut zip, idx) }; + + // Check the shared translated index, both payloads, and state preservation. + assert_eq!(result, expected); + assert_eq!(zip.index, index_before); + assert_eq!(zip.len, len_before); + assert_eq!(zip.a.size_hint(), left_size_before); + assert_eq!(zip.b.size_hint(), right_size_before); + assert_eq!(Iterator::size_hint(&zip), size_before); + } + }; + } + + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i8, i8); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i16, i16); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i32, i32); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i64, i64); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i128, i128); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u8, u8); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u16, u16); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u32, u32); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u64, u64); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u128, u128); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_array, [u8; 4]); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_bool, bool); + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_unit, ()); + + // Harnesses for `fold` for ZipImpl. + macro_rules! generate_zip_fold_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + fn $name() { + // Generate independent symbolic lengths for both sides. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + + // Generate independent symbolic payloads for both sides. + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); + + // Map preserves full trusted random access with unbounded lengths. + let left = (0..left_len).map(move |_| left_value); + let right = (0..right_len).map(move |_| right_value); + let mut zip = Zip::new(left, right); + + // Model any reachable offset in the full trusted-random-access Zip. + let index: usize = kani::any(); + kani::assume(index <= zip.len); + zip.index = index; + + // Call the specialized safe function directly. + ZipImpl::fold(zip, (), |(), _pair| ()); + } + }; + } + + generate_zip_fold_harness!(harness_zip_fold_i8, i8); + generate_zip_fold_harness!(harness_zip_fold_i16, i16); + generate_zip_fold_harness!(harness_zip_fold_i32, i32); + generate_zip_fold_harness!(harness_zip_fold_i64, i64); + generate_zip_fold_harness!(harness_zip_fold_i128, i128); + generate_zip_fold_harness!(harness_zip_fold_u8, u8); + generate_zip_fold_harness!(harness_zip_fold_u16, u16); + generate_zip_fold_harness!(harness_zip_fold_u32, u32); + generate_zip_fold_harness!(harness_zip_fold_u64, u64); + generate_zip_fold_harness!(harness_zip_fold_u128, u128); + generate_zip_fold_harness!(harness_zip_fold_bool, bool); + generate_zip_fold_harness!(harness_zip_fold_unit, ()); + generate_zip_fold_harness!(harness_zip_fold_array, [u8; 4]); + + // Harnesses for `next` for ZipImpl. + macro_rules! generate_zip_next_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + fn $name() { + // Generate independent symbolic lengths for both sides. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + + // Generate independent symbolic payloads for both sides. + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); + + // Map over Range preserves TrustedRandomAccess. + let left = (0..left_len).map(move |_| left_value); + let right = (0..right_len).map(move |_| right_value); + let mut zip = Zip::new(left, right); + + // Model any reachable offset in the full trusted-random-access Zip. + let index: usize = kani::any(); + kani::assume(index <= zip.len); + zip.index = index; + + // Call the specialized safe function directly. + ZipImpl::next(&mut zip); + } + }; + } + + generate_zip_next_harness!(harness_zip_next_i8, i8); + generate_zip_next_harness!(harness_zip_next_i16, i16); + generate_zip_next_harness!(harness_zip_next_i32, i32); + generate_zip_next_harness!(harness_zip_next_i64, i64); + generate_zip_next_harness!(harness_zip_next_i128, i128); + generate_zip_next_harness!(harness_zip_next_u8, u8); + generate_zip_next_harness!(harness_zip_next_u16, u16); + generate_zip_next_harness!(harness_zip_next_u32, u32); + generate_zip_next_harness!(harness_zip_next_u64, u64); + generate_zip_next_harness!(harness_zip_next_u128, u128); + generate_zip_next_harness!(harness_zip_next_bool, bool); + generate_zip_next_harness!(harness_zip_next_unit, ()); + generate_zip_next_harness!(harness_zip_next_array, [u8; 4]); + + // Harnesses for `next` for ZipImpl. + macro_rules! generate_zip_nth_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + fn $name() { + // Generate independent symbolic lengths and the requested index. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + let n: usize = kani::any(); + + // Generate independent symbolic payloads for both sides. + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); + + // Map selects the full trusted-random-access specialization. + let left = (0..left_len).map(move |_| left_value); + let right = (0..right_len).map(move |_| right_value); + let mut zip = Zip::new(left, right); + + // Model any state reachable by prior forward iteration. + let index: usize = kani::any(); + kani::assume(index <= zip.len); + zip.index = index; + + // Call the specialized safe function directly. + ZipImpl::nth(&mut zip, n); + } + }; + } + + generate_zip_nth_harness!(harness_zip_nth_i8, i8); + generate_zip_nth_harness!(harness_zip_nth_i16, i16); + generate_zip_nth_harness!(harness_zip_nth_i32, i32); + generate_zip_nth_harness!(harness_zip_nth_i64, i64); + generate_zip_nth_harness!(harness_zip_nth_i128, i128); + generate_zip_nth_harness!(harness_zip_nth_u8, u8); + generate_zip_nth_harness!(harness_zip_nth_u16, u16); + generate_zip_nth_harness!(harness_zip_nth_u32, u32); + generate_zip_nth_harness!(harness_zip_nth_u64, u64); + generate_zip_nth_harness!(harness_zip_nth_u128, u128); + generate_zip_nth_harness!(harness_zip_nth_bool, bool); + generate_zip_nth_harness!(harness_zip_nth_unit, ()); + generate_zip_nth_harness!(harness_zip_nth_array, [u8; 4]); + + // Harnesses for `next_back` for ZipImpl. + #[kani::proof] + fn harness_zip_next_back() { + // Generate independent unbounded lengths. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + + // Core Range iterators provide trusted random access. + let left = 0..left_len; + let right = 0..right_len; + let mut zip = Zip::new(left, right); + + // Model any state reachable after prior forward iteration. + let index: usize = kani::any(); + kani::assume(index <= zip.len); + zip.index = index; + + // Call the specialized safe function directly. + ZipImpl::next_back(&mut zip); + } + + // Harnesses for `spec_fold` for ZipImpl. + macro_rules! generate_zip_spec_fold_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + fn $name() { + // Generate independent symbolic finite lengths. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + + // Generate independent symbolic values for both sides. + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); + + // Take> preserves full trusted random access. + let left = crate::iter::repeat(left_value).take(left_len); + let right = crate::iter::repeat(right_value).take(right_len); + let zip = Zip::new(left, right); + + // Call the TrustedLen-specialized safe function directly. + SpecFold::spec_fold(zip, (), |(), _pair| ()); + } + }; + } + + generate_zip_spec_fold_harness!(harness_zip_spec_fold_i8, i8); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_i16, i16); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_i32, i32); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_i64, i64); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_i128, i128); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_u8, u8); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_u16, u16); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_u32, u32); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_u64, u64); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_u128, u128); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_bool, bool); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_unit, ()); + generate_zip_spec_fold_harness!(harness_zip_spec_fold_array, [u8; 4]); +} From 28873730ac3377d79b9f9d4cd5cb0b3006c51ce3 Mon Sep 17 00:00:00 2001 From: v3risec Date: Thu, 15 Oct 2026 16:04:55 +0800 Subject: [PATCH 2/2] address review feedback partially --- .../core/src/iter/adapters/array_chunks.rs | 11 +- library/core/src/iter/adapters/cloned.rs | 88 +----- library/core/src/iter/adapters/copied.rs | 45 +--- library/core/src/iter/adapters/enumerate.rs | 58 ++-- library/core/src/iter/adapters/filter.rs | 1 - library/core/src/iter/adapters/fuse.rs | 52 ++-- library/core/src/iter/adapters/map.rs | 115 ++------ library/core/src/iter/adapters/skip.rs | 160 +++++------ library/core/src/iter/adapters/step_by.rs | 2 +- library/core/src/iter/adapters/take.rs | 4 +- library/core/src/iter/adapters/zip.rs | 251 +++++++++--------- 11 files changed, 273 insertions(+), 514 deletions(-) diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs index 3563dc5b44e21..600e64e1d2a47 100644 --- a/library/core/src/iter/adapters/array_chunks.rs +++ b/library/core/src/iter/adapters/array_chunks.rs @@ -289,20 +289,20 @@ mod verify { 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(); } @@ -332,13 +332,10 @@ mod verify { 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); } diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs index f43cd36519a8e..1f1c05c7f243a 100644 --- a/library/core/src/iter/adapters/cloned.rs +++ b/library/core/src/iter/adapters/cloned.rs @@ -187,44 +187,27 @@ 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] + #[kani::proof_for_contract( + > as crate::iter::Iterator>:: + __iterator_get_unchecked + )] 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` from the inner iterator. + let source = (0..len).map(|_| &value); 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` 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); + 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", + ); } }; } @@ -242,47 +225,4 @@ mod verify { 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` 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` 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, ()); } diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs index 7b83a4d01406c..dd15e1e15aaae 100644 --- a/library/core/src/iter/adapters/copied.rs +++ b/library/core/src/iter/adapters/copied.rs @@ -290,41 +290,27 @@ unsafe impl InPlaceIterable for Copied { 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. + // Harnesses for `__iterator_get_unchecked` for Copied. macro_rules! generate_copied_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + > as crate::iter::Iterator>:: + __iterator_get_unchecked + )] 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 source = (0..len).map(|_| &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` 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); + 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", + ); } }; } @@ -352,7 +338,6 @@ mod verify { 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 _ = as SpecNextChunk<'_, 4, $ty>>::spec_next_chunk( &mut iter, @@ -379,11 +364,9 @@ mod verify { // 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 _ = as SpecNextChunk<'_, 4, ()>>::spec_next_chunk(&mut iter); diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs index d152a75e73435..b59687b2986b5 100644 --- a/library/core/src/iter/adapters/enumerate.rs +++ b/library/core/src/iter/adapters/enumerate.rs @@ -327,50 +327,34 @@ impl Default for Enumerate { mod verify { use super::*; - // Harnesses for `__iterator_get_unchecked` for enumerate - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + // Harnesses for `__iterator_get_unchecked` for Enumerate. macro_rules! generate_enumerate_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + , fn(usize) -> $ty>, + > as crate::iter::Iterator>::__iterator_get_unchecked + )] pub fn $name() { - // Generate a symbolic enumeration offset. let count: usize = kani::any(); - // Generate a symbolic relative access index. + let end: usize = kani::any(); let idx: usize = kani::any(); - // Generate an arbitrary inner item. let value: $ty = kani::any(); - // Record the absolute position reached by the inner iterator. - let observed_position = crate::cell::Cell::new(usize::MAX); - - // Model the remaining range after `count` items without allocating elements. - let source = (count..usize::MAX).map(|position| { - // Record which inner element the target actually requested. - observed_position.set(position); - value - }); - // Build a valid `Enumerate` state with a symbolic offset. + let source = (count..end).map(move |_| value); let mut iter = Enumerate { iter: source, count }; - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < iter.size_hint().0); - // Save observable iterator state before random access. - let count_before = iter.next_index(); - let size_before = iter.size_hint(); - - // Call the target `Enumerate` implementation through the trait path. - let result = - unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; - - // Check that the relative `idx` reached the correct absolute position. - assert_eq!(observed_position.get(), count_before + idx); - // Check the enumeration index added by the target. - assert_eq!(result.0, count_before + idx); - // Check that the inner item was forwarded unchanged. - assert_eq!(result.1, value); - // Check that random access did not advance the enumeration count. - assert_eq!(iter.next_index(), count_before); - // Check that random access did not consume the iterator. - assert_eq!(iter.size_hint(), size_before); + 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", + ); } }; } diff --git a/library/core/src/iter/adapters/filter.rs b/library/core/src/iter/adapters/filter.rs index 193a0da21627d..59e568657139b 100644 --- a/library/core/src/iter/adapters/filter.rs +++ b/library/core/src/iter/adapters/filter.rs @@ -291,4 +291,3 @@ mod verify { generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_bool, bool); generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_unit, ()); } - \ No newline at end of file diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs index 50d2e820374df..6f82c8f170983 100644 --- a/library/core/src/iter/adapters/fuse.rs +++ b/library/core/src/iter/adapters/fuse.rs @@ -517,48 +517,28 @@ fn and_then_or_clear(opt: &mut Option, f: impl FnOnce(&mut T) -> Option mod verify { use super::*; - // Harnesses for `__iterator_get_unchecked` for Fuse - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + // Harnesses for `__iterator_get_unchecked` for Fuse. macro_rules! generate_fuse_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + , fn(usize) -> $ty>, + > as crate::iter::Iterator>::__iterator_get_unchecked + )] 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 inner item. 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(|position| { - // Record which inner element the target actually requested. - observed_idx.set(position); - value - }); - // Construct an active `Fuse` whose inner state is `Some(source)`. - let mut iter = Fuse::new(source); - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < iter.size_hint().0); - // Save observable iterator state before random access. - let size_before = iter.size_hint(); - assert!(iter.iter.is_some()); - - // Call the target `Fuse` 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 inner item was forwarded unchanged. - assert_eq!(result, value); - // Check that random access kept the inner iterator active. - assert!(iter.iter.is_some()); - // Check that random access did not consume the iterator. - assert_eq!(iter.size_hint(), size_before); + let source = (0..len).map(move |_| value); + let mut iter = Fuse { iter: if kani::any() { Some(source) } else { None } }; + 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", + ); } }; } diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs index 1c9782f943587..fad965b0622c1 100644 --- a/library/core/src/iter/adapters/map.rs +++ b/library/core/src/iter/adapters/map.rs @@ -238,49 +238,34 @@ unsafe impl InPlaceIterable for Map { mod verify { use super::*; - // Harnesses for `__iterator_get_unchecked` for Map - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. + // Harnesses for `__iterator_get_unchecked` for Map. macro_rules! generate_map_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + , + fn(usize) -> ($ty, usize, usize), + > as crate::iter::Iterator>::__iterator_get_unchecked + )] 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 arbitrary data captured by the mapping closure. let value: $ty = kani::any(); - // Record the inner item passed to the mapping closure. - let observed_input = crate::cell::Cell::new(usize::MAX); - // Count how many times the target invokes the mapping closure. - let closure_calls = crate::cell::Cell::new(0usize); - - // Use the range item itself as the observable inner position. - let source = 0..len; - // Construct the target with a stateful, type-changing closure. - let mut iter = Map::new(source, |position| { - observed_input.set(position); - closure_calls.set(closure_calls.get() + 1); - (value, position, closure_calls.get()) + let initial_calls: usize = kani::any(); + let mut calls = initial_calls; + let mut iter = Map::new(0..len, move |position| { + calls = calls.wrapping_add(1); + (value, position, calls) }); - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < iter.size_hint().0); - // Save the iterator size before random access. - let size_before = iter.size_hint(); - - // Call the target `Map` implementation through the trait path. - let result = - unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; - - // Check that the target forwarded `idx` to the inner range exactly. - assert_eq!(observed_input.get(), idx); - // Check that the target invoked the mapping closure exactly once. - assert_eq!(closure_calls.get(), 1); - // Check the closure input, captured value, and stateful output. - assert_eq!(result, (value, idx, 1)); - // Check that random access did not consume the iterator. - assert_eq!(iter.size_hint(), size_before); + 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(initial_calls == usize::MAX, "wrapping closure state"); + kani::cover( + len == usize::MAX && idx == len - 1, + "last element at the maximum logical length", + ); } }; } @@ -298,62 +283,4 @@ mod verify { generate_map_get_unchecked_harness!(harness_map_get_unchecked_array, [u8; 4]); generate_map_get_unchecked_harness!(harness_map_get_unchecked_bool, bool); generate_map_get_unchecked_harness!(harness_map_get_unchecked_unit, ()); - - // Harnesses for `next_unchecked` for Map - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. - macro_rules! generate_map_next_unchecked_harness { - ($name:ident, $ty:ty) => { - #[kani::proof] - pub fn $name() { - // Generate arbitrary data captured by the mapping closure. - let value: $ty = kani::any(); - // Generate an arbitrary inner item. - let inner_value: usize = kani::any(); - // Generate a symbolic logical length with no explicit upper bound. - let len: usize = kani::any(); - // Record the inner item passed to the mapping closure. - let observed_input = crate::cell::Cell::new(usize::MAX); - // Count how many times the target invokes the mapping closure. - let closure_calls = crate::cell::Cell::new(0usize); - - // Build an exact-length iterator without allocating `len` elements. - let source = crate::iter::repeat_n(inner_value, len); - // Construct the target with a stateful, type-changing closure. - let mut iter = Map::new(source, |item| { - observed_input.set(item); - closure_calls.set(closure_calls.get() + 1); - (value, item, closure_calls.get()) - }); - - // Express the target's non-empty precondition. - kani::assume(iter.size_hint().0 > 0); - - // Call the target `Map` implementation through the trait path. - let result = unsafe { UncheckedIterator::next_unchecked(&mut iter) }; - - // Check that the closure received the consumed inner item. - assert_eq!(observed_input.get(), inner_value); - // Check that the target invoked the mapping closure exactly once. - assert_eq!(closure_calls.get(), 1); - // Check the closure input, captured value, and stateful output. - assert_eq!(result, (value, inner_value, 1)); - // Check that the target consumed exactly one inner element. - assert_eq!(iter.size_hint(), (len - 1, Some(len - 1))); - } - }; - } - - generate_map_next_unchecked_harness!(harness_map_next_unchecked_i8, i8); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_i16, i16); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_i32, i32); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_i64, i64); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_i128, i128); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_u8, u8); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_u16, u16); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_u32, u32); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_u64, u64); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_u128, u128); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_array, [u8; 4]); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_bool, bool); - generate_map_next_unchecked_harness!(harness_map_next_unchecked_unit, ()); } diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs index 040a5f6d42169..5eb3f1f2542ee 100644 --- a/library/core/src/iter/adapters/skip.rs +++ b/library/core/src/iter/adapters/skip.rs @@ -162,7 +162,8 @@ where } #[doc(hidden)] - #[requires(idx + self.n < self.iter.size_hint().0)] + // Express the translated index bound without overflowing in the contract. + #[requires(idx < self.iter.size_hint().0.saturating_sub(self.n))] #[cfg_attr(kani, kani::modifies(self))] unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item where @@ -311,118 +312,78 @@ unsafe impl TrustedLen for Skip where I: Iterator + TrustedRandomAccess {} mod verify { use super::*; - // Harnesses for `__iterator_get_unchecked` for Skip - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. - macro_rules! generate_skip_get_unchecked_unbounded_harness { - ($name:ident) => { - #[kani::proof] - pub fn $name() { - // Generate a symbolic pending skip count. - let n: usize = kani::any(); - // Generate a symbolic index in the shortened iterator. - let idx: usize = kani::any(); - - // Use a maximal lazy range with no random-access side effects. - let source = 0..usize::MAX; - // Construct the target with a symbolic skip offset. - let mut iter = Skip::new(source, n); - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < iter.size_hint().0); - // Save observable iterator state before random access. - let n_before = iter.n; - let size_before = iter.size_hint(); - - // Call the target `Skip` implementation through the trait path. - let result = - unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; - - // Check that `Skip` translated the outer index to `n + idx`. - assert_eq!(result, n + idx); - // Check that random access did not consume the pending skip count. - assert_eq!(iter.n, n_before); - // Check that random access did not consume the iterator. - assert_eq!(iter.size_hint(), size_before); - } - }; + // Harnesses for `__iterator_get_unchecked` for Skip. + #[kani::proof_for_contract( + > as crate::iter::Iterator>::__iterator_get_unchecked + )] + pub fn harness_skip_get_unchecked_unbounded() { + let len: usize = kani::any(); + let n: usize = kani::any(); + let idx: usize = kani::any(); + let mut iter = Skip::new(0..len, n); + let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + let remaining = len - n; + kani::cover(n == 0 && idx == 0, "first element without a skipped prefix"); + kani::cover(n > 0 && idx == 0, "first element after a skipped prefix"); + kani::cover(idx > 0 && idx < remaining - 1, "interior element"); + kani::cover(idx == remaining - 1, "last element"); + kani::cover( + len == usize::MAX && n == 0 && idx == len - 1, + "last element at the maximum logical length", + ); } - // Cover Copy item types with core's non-side-effecting array iterator macro_rules! generate_skip_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + , fn(usize) -> $ty>, + > as crate::iter::Iterator>::__iterator_get_unchecked + )] pub fn $name() { - // Generate a symbolic pending skip count and outer index. + let len: usize = kani::any(); let n: usize = kani::any(); let idx: usize = kani::any(); - // Generate four independent symbolic values of the selected item type. - let values: [$ty; 4] = kani::any(); - // Keep a Copy snapshot for checking the translated index. - let expected_values = values; - - // Use core's generic trusted-random-access iterator with no side effects. - let source: crate::array::IntoIter<$ty, 4> = values.into_iter(); - // Construct the target with a symbolic skip offset. + let value: $ty = kani::any(); + let source = (0..len).map(move |_| value); let mut iter = Skip::new(source, n); - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < iter.size_hint().0); - // The precondition guarantees that `n + idx` indexes the original array. - let expected = expected_values[n + idx]; - // Save observable iterator state before random access. - let n_before = iter.n; - let size_before = iter.size_hint(); - - // Call the target `Skip` implementation through the trait path. - let result = - unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; - - // Check that `Skip` selected the original element at `n + idx`. - assert_eq!(result, expected); - // Check that random access did not consume the adapter state. - assert_eq!(iter.n, n_before); - assert_eq!(iter.size_hint(), size_before); + let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + let remaining = len - n; + kani::cover(n == 0 && idx == 0, "empty skipped prefix"); + kani::cover(n > 0 && idx == 0, "nonempty skipped prefix"); + kani::cover(n > 0 && idx > 0, "access without evaluating the prefix"); + kani::cover(idx == remaining - 1, "last element"); + kani::cover( + len == usize::MAX && n == usize::MAX - 1 && idx == 0, + "maximum skipped prefix", + ); } }; } - // Cover side-effecting path - macro_rules! generate_skip_get_unchecked_side_effect_harness { - ($name:ident) => { - #[kani::proof] - pub fn $name() { - // Generate a symbolic pending skip count. - let n: usize = kani::any(); - // Generate a symbolic index in the shortened iterator. - let idx: usize = kani::any(); - - // `Map` sets `MAY_HAVE_SIDE_EFFECT = true` for every mapping closure, - // so this selects `Skip`'s side-effecting random-access branch. - // Keep the closure stateless because this harness does not track exact effects. - let source = (0..usize::MAX).map(|position| position); - // Construct the target with a symbolic skip offset. - let mut iter = Skip::new(source, n); - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < iter.size_hint().0); - // Save observable iterator state before random access. - let n_before = iter.n; - let size_before = iter.size_hint(); - - // Call the target `Skip` implementation through the trait path. - let result = - unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; - - // Check that `Skip` translated the outer index to `n + idx`. - assert_eq!(result, n + idx); - // Check that random access did not consume the adapter state. - assert_eq!(iter.n, n_before); - assert_eq!(iter.size_hint(), size_before); - } - }; + // Use a regular proof because proof_for_contract cannot name the + // anonymous closure type used by Map. Mirror the target's precondition. + #[kani::proof] + pub fn harness_skip_get_unchecked_side_effect() { + let len: usize = kani::any(); + let n: usize = kani::any(); + let idx: usize = kani::any(); + let mut calls: usize = kani::any(); + let source = (0..usize::MAX).map(|position| position); + let mut iter = Skip::new(source, n); + // Mirror the target's #[requires] contract. + kani::assume(idx < iter.size_hint().0); + kani::cover(true, "the mirrored precondition is satisfiable"); + let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) }; + kani::cover(n == 0 && idx == 0, "empty skipped prefix"); + kani::cover(n > 0 && idx == 0, "stateful nonempty skipped prefix"); + kani::cover(n > 0 && idx > 0, "stateful access without evaluating the prefix"); + kani::cover( + len == usize::MAX && n == usize::MAX - 1 && idx == 0, + "stateful maximum skipped prefix", + ); } - generate_skip_get_unchecked_unbounded_harness!(harness_skip_get_unchecked_unbounded); generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i8, i8); generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i16, i16); generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i32, i32); @@ -436,5 +397,4 @@ mod verify { generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_array, [u8; 4]); generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_bool, bool); generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_unit, ()); - generate_skip_get_unchecked_side_effect_harness!(harness_skip_get_unchecked_side_effect); } diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs index 607748cf297a7..dcc792560ae65 100644 --- a/library/core/src/iter/adapters/step_by.rs +++ b/library/core/src/iter/adapters/step_by.rs @@ -669,4 +669,4 @@ mod verify { // Call the safe function under test. let _ = step_by.original_step(); } -} \ No newline at end of file +} diff --git a/library/core/src/iter/adapters/take.rs b/library/core/src/iter/adapters/take.rs index 6dc925a0ba26e..1230ec912940a 100644 --- a/library/core/src/iter/adapters/take.rs +++ b/library/core/src/iter/adapters/take.rs @@ -314,7 +314,7 @@ impl SpecTake for Take { { let mut acc = init; let end = self.n.min(self.iter.size()); - #[cfg_attr(kani, kani::loop_invariant(end <= self.iter.size()))] + #[cfg_attr(kani, kani::loop_invariant(kani::index <= end))] for i in 0..end { // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end let val = unsafe { self.iter.__iterator_get_unchecked(i) }; @@ -326,7 +326,7 @@ impl SpecTake for Take { #[inline] fn spec_for_each(mut self, mut f: F) { let end = self.n.min(self.iter.size()); - #[cfg_attr(kani, kani::loop_invariant(end <= self.iter.size()))] + #[cfg_attr(kani, kani::loop_invariant(kani::index <= end))] for i in 0..end { // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end let val = unsafe { self.iter.__iterator_get_unchecked(i) }; diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs index 83422d4f127cc..94e877ae30521 100644 --- a/library/core/src/iter/adapters/zip.rs +++ b/library/core/src/iter/adapters/zip.rs @@ -282,7 +282,7 @@ where } #[inline] - #[cfg_attr(kani, kani::requires(idx < TrustedRandomAccessNoCoerce::size(self)))] + #[requires(idx < TrustedRandomAccessNoCoerce::size(self))] #[cfg_attr(kani, kani::modifies(self))] unsafe fn get_unchecked(&mut self, idx: usize) -> ::Item { let idx = self.index + idx; @@ -699,8 +699,6 @@ impl SpecFold for Zip { F: FnMut(Acc, Self::Item) -> Acc, { let mut accum = init; - - #[cfg(not(kani))] loop { let (upper, more) = if let Some(upper) = ZipImpl::size_hint(&self).1 { (upper, false) @@ -721,23 +719,6 @@ impl SpecFold for Zip { break; } } - - // Loop stub: choose one arbitrary iteration from a chunk - // and preserve the unchecked-access safety check without a - // writeset over generic iterator structs. - #[cfg(kani)] - { - let upper = ZipImpl::size_hint(&self).1.unwrap_or(usize::MAX); - if upper != 0 { - let index: usize = kani::any(); - kani::assume(index < upper); - let pair = unsafe { - (self.a.nth(index).unwrap_unchecked(), self.b.nth(index).unwrap_unchecked()) - }; - accum = f(accum, pair); - } - } - accum } } @@ -747,85 +728,67 @@ impl SpecFold for Zip { mod verify { use super::*; - // Harnesses for `__iterator_get_unchecked` for ZipImpl. - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. - // Use core's non-side-effecting `Copied>` for item-type coverage. + // Harnesses for `__iterator_get_unchecked` for Zip. macro_rules! generate_zip_iterator_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + , fn(usize) -> $ty>, + crate::iter::Map, fn(usize) -> $ty>, + > as crate::iter::Iterator>::__iterator_get_unchecked + )] pub fn $name() { - // Generate independent symbolic values for both sides. - let left: [$ty; 4] = kani::any(); - let right: [$ty; 4] = kani::any(); - // Generate a symbolic reachable offset and remaining-relative index. + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); let index: usize = kani::any(); let idx: usize = kani::any(); - - // `Copied>` implements full trusted random access. - let mut zip = Zip::new(left.iter().copied(), right.iter().copied()); - // Specialized `next` changes only `index`, so this models a reachable state. - kani::assume(index <= zip.len); - zip.index = index; - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip)); - let absolute_idx = index + idx; - let expected = (left[absolute_idx], right[absolute_idx]); - // Save observable `Zip` state before random access. - let index_before = zip.index; - let len_before = zip.len; - let size_before = Iterator::size_hint(&zip); - - // Call the outer `Iterator` target through its trait path. - let result = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) }; - - // Check both values at the translated absolute index. - assert_eq!(result, expected); - // Check that random access did not consume the zipped iterator. - assert_eq!(zip.index, index_before); - assert_eq!(zip.len, len_before); - assert_eq!(Iterator::size_hint(&zip), size_before); + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); + let left = (0..left_len).map(move |_| left_value); + let right = (0..right_len).map(move |_| right_value); + let mut zip = Zip::new(left, right); + zip.index = index.min(zip.len); + let _ = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) }; + let remaining = zip.len - zip.index; + kani::cover(zip.index == 0 && idx == 0, "first element"); + kani::cover(zip.index > 0 && idx == 0, "first element after a prefix"); + kani::cover(idx > 0 && idx < remaining - 1, "interior element"); + kani::cover(idx == remaining - 1, "last element"); + kani::cover(left_len < right_len, "left iterator is shorter"); + kani::cover(left_len > right_len, "right iterator is shorter"); + kani::cover( + left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1, + "last element at the maximum logical length", + ); } }; } - #[kani::proof] + #[kani::proof_for_contract( + , + crate::ops::Range, + > as crate::iter::Iterator>::__iterator_get_unchecked + )] fn harness_zip_iterator_get_unchecked_unbounded() { - // Generate independent symbolic lengths for both inner iterators. let left_len: usize = kani::any(); let right_len: usize = kani::any(); - // Generate a symbolic reachable offset in the specialized `Zip` state. let index: usize = kani::any(); - // Generate a symbolic index relative to the remaining zipped iterator. let idx: usize = kani::any(); - - // Use core ranges to keep both input lengths unbounded by a harness constant. let mut zip = Zip::new(0..left_len, 0..right_len); - // Specialized `next` reaches this state by changing only `index`. - kani::assume(index <= zip.len); - zip.index = index; - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip)); - let absolute_idx = index + idx; - // Save all observable iterator state before random access. - let index_before = zip.index; - let len_before = zip.len; - let left_size_before = zip.a.size_hint(); - let right_size_before = zip.b.size_hint(); - let size_before = Iterator::size_hint(&zip); - - // Call the outer `Iterator` target, which delegates to `ZipImpl`. - let result = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) }; - - // Check that both sides received the same translated absolute index. - assert_eq!(result, (absolute_idx, absolute_idx)); - // Check that random access did not consume or resize any iterator state. - assert_eq!(zip.index, index_before); - assert_eq!(zip.len, len_before); - assert_eq!(zip.a.size_hint(), left_size_before); - assert_eq!(zip.b.size_hint(), right_size_before); - assert_eq!(Iterator::size_hint(&zip), size_before); + zip.len = kani::any::().min(zip.len); + zip.index = index.min(zip.len); + let _ = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) }; + let remaining = zip.len - zip.index; + kani::cover(zip.index == 0 && idx == 0, "first element"); + kani::cover(zip.index > 0 && idx == 0, "first element after a prefix"); + kani::cover(idx > 0 && idx < remaining - 1, "interior element"); + kani::cover(idx == remaining - 1, "last element"); + kani::cover(zip.len < left_len.min(right_len), "access after consuming from the back"); + kani::cover( + left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1, + "last element at the maximum logical length", + ); } generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i8, i8); @@ -843,58 +806,77 @@ mod verify { generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_unit, ()); // Harnesses for `get_unchecked` for ZipImpl. - // Use a regular proof because `proof_for_contract` cannot resolve this trait method path. - // Use stateless maps to combine unbounded positions with symbolic Copy payloads. macro_rules! generate_zip_get_unchecked_harness { ($name:ident, $ty:ty) => { - #[kani::proof] + #[kani::proof_for_contract( + , fn(usize) -> (usize, $ty)>, + crate::iter::Map, fn(usize) -> (usize, $ty)>, + > as ZipImpl< + crate::iter::Map, fn(usize) -> (usize, $ty)>, + crate::iter::Map, fn(usize) -> (usize, $ty)>, + >>::get_unchecked + )] pub fn $name() { - // Generate independent symbolic lengths and payloads for both sides. let left_len: usize = kani::any(); let right_len: usize = kani::any(); - let left_value: $ty = kani::any(); - let right_value: $ty = kani::any(); - let left_expected = left_value; - let right_expected = right_value; - // Generate a symbolic reachable offset and remaining-relative index. let index: usize = kani::any(); let idx: usize = kani::any(); - - // Preserve each absolute position while attaching a symbolic payload. - // These closures copy captured values without mutating any state. + let left_value: $ty = kani::any(); + let right_value: $ty = kani::any(); let left = (0..left_len).map(move |position| (position, left_value)); let right = (0..right_len).map(move |position| (position, right_value)); let mut zip = Zip::new(left, right); - - // Full trusted-random-access `Zip::next` changes only `index`. - kani::assume(index <= zip.len); - zip.index = index; - - // Express the target's `idx < self.size()` precondition. - kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip)); - let absolute_idx = index + idx; - let expected = ((absolute_idx, left_expected), (absolute_idx, right_expected)); - // Save all observable state before the internal random-access call. - let index_before = zip.index; - let len_before = zip.len; - let left_size_before = zip.a.size_hint(); - let right_size_before = zip.b.size_hint(); - let size_before = Iterator::size_hint(&zip); - - // Call the internal target directly rather than the outer `Iterator` method. - let result = unsafe { ZipImpl::get_unchecked(&mut zip, idx) }; - - // Check the shared translated index, both payloads, and state preservation. - assert_eq!(result, expected); - assert_eq!(zip.index, index_before); - assert_eq!(zip.len, len_before); - assert_eq!(zip.a.size_hint(), left_size_before); - assert_eq!(zip.b.size_hint(), right_size_before); - assert_eq!(Iterator::size_hint(&zip), size_before); + zip.index = index.min(zip.len); + let _ = unsafe { ZipImpl::get_unchecked(&mut zip, idx) }; + let remaining = zip.len - zip.index; + kani::cover(zip.index == 0 && idx == 0, "first element"); + kani::cover(zip.index > 0 && idx == 0, "first element after a prefix"); + kani::cover(idx > 0 && idx < remaining - 1, "interior element"); + kani::cover(idx == remaining - 1, "last element"); + kani::cover(left_len < right_len, "left iterator is shorter"); + kani::cover(left_len > right_len, "right iterator is shorter"); + kani::cover(zip.index == usize::MAX - 1 && idx == 0, "maximum valid offset"); + kani::cover( + left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1, + "last element at the maximum logical length", + ); } }; } + #[kani::proof_for_contract( + , + crate::ops::Range, + > as ZipImpl< + crate::ops::Range, + crate::ops::Range, + >>::get_unchecked + )] + fn harness_zip_get_unchecked_unbounded() { + let left_len: usize = kani::any(); + let right_len: usize = kani::any(); + let index: usize = kani::any(); + let idx: usize = kani::any(); + let mut zip = Zip::new(0..left_len, 0..right_len); + // For ranges, front/back consumption changes only index/len. + zip.len = kani::any::().min(zip.len); + zip.index = index.min(zip.len); + let _ = unsafe { ZipImpl::get_unchecked(&mut zip, idx) }; + let remaining = zip.len - zip.index; + kani::cover(zip.index == 0 && idx == 0, "first element"); + kani::cover(zip.index > 0 && idx == 0, "first element after a prefix"); + kani::cover(idx > 0 && idx < remaining - 1, "interior element"); + kani::cover(idx == remaining - 1, "last element"); + kani::cover(zip.len < left_len.min(right_len), "access after consuming from the back"); + kani::cover(zip.index == usize::MAX - 1 && idx == 0, "maximum valid offset"); + kani::cover( + left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1, + "last element at the maximum logical length", + ); + } + generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i8, i8); generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i16, i16); generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i32, i32); @@ -1064,22 +1046,29 @@ mod verify { macro_rules! generate_zip_spec_fold_harness { ($name:ident, $ty:ty) => { #[kani::proof] - fn $name() { - // Generate independent symbolic finite lengths. + #[kani::unwind(8)] + pub fn $name() { + // Generate independent symbolic lengths, bounded for unwinding. let left_len: usize = kani::any(); let right_len: usize = kani::any(); - - // Generate independent symbolic values for both sides. + kani::assume(left_len <= 4 && right_len <= 4); + kani::cover(true, "bounded input is satisfiable"); + // Generate independent symbolic payloads. let left_value: $ty = kani::any(); let right_value: $ty = kani::any(); - - // Take> preserves full trusted random access. + // Take> provides a finite TrustedLen iterator. let left = crate::iter::repeat(left_value).take(left_len); let right = crate::iter::repeat(right_value).take(right_len); let zip = Zip::new(left, right); - - // Call the TrustedLen-specialized safe function directly. - SpecFold::spec_fold(zip, (), |(), _pair| ()); + // Exercise the real TrustedLen-specialized implementation. + let count = SpecFold::spec_fold(zip, 0usize, |count, _pair| count + 1); + // The fold must process exactly min(left_len, right_len) pairs. + assert_eq!(count, left_len.min(right_len)); + kani::cover(left_len == 0 || right_len == 0, "empty zip"); + kani::cover(left_len < right_len, "left iterator is shorter"); + kani::cover(left_len > right_len, "right iterator is shorter"); + kani::cover(left_len == right_len && left_len > 0, "equal nonempty lengths"); + kani::cover(left_len == 4 && right_len == 4, "maximum bounded length"); } }; }