Refine iterator adapter verification harnesses

- Use a subtraction-based, overflow-safe precondition for
  Skip::__iterator_get_unchecked, matching Zip::get_unchecked.
- Add the loop-invariant justification comment to Take::spec_for_each.
- Clarify that the large-array harnesses verify slices up to MAX_LEN.

Author: Kasim Te

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

@@ -162,7 +162,9 @@ where
     }
 
     #[doc(hidden)]
-    #[requires(idx + self.n < self.iter.size_hint().0)]
+    // Subtraction-based bound (avoids `idx + self.n` overflow in the contract,
+    // matching the overflow-safe form used for `Zip::get_unchecked`).
+    #[requires(self.n <= self.iter.size_hint().0 && idx < self.iter.size_hint().0 - self.n)]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where

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

@@ -317,6 +317,10 @@ impl<I: Iterator + TrustedRandomAccess> SpecTake for Take<I> {
     #[inline]
     fn spec_for_each<F: FnMut(Self::Item)>(mut self, mut f: F) {
         let end = self.n.min(self.iter.size());
+        // __iterator_get_unchecked is a read-only operation for TrustedRandomAccess
+        // iterators, so iter.size() is preserved across iterations.
+        // The Kani loop invariant below is intentionally vacuous (`true`) and
+        // is used only to enable loop-contract mode.
         #[cfg_attr(kani, kani::loop_invariant(true))]
         for i in 0..end {
             // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end
@@ -389,8 +393,8 @@ mod verify {
     use super::*;
 
     // spec_fold (TRA specialized — uses __iterator_get_unchecked in a loop)
-    // Loop invariant on source code enables unbounded verification via
-    // loop contracts instead of finite unrolling.
+    // The source-level loop invariant abstracts the get_unchecked loop via loop
+    // contracts instead of finite unrolling; this harness covers slices up to MAX_LEN.
     #[kani::proof]
     fn check_take_spec_fold_u8() {
         const MAX_LEN: usize = 5000;

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

@@ -748,8 +748,8 @@ mod verify {
     // --- Safe abstractions ---
 
     // next (TRA specialized — uses __iterator_get_unchecked internally)
-    // Single call on large array: next() makes one get_unchecked call per invocation,
-    // so a single call at arbitrary slice length suffices for unbounded verification.
+    // next() makes a single get_unchecked call per invocation with no length-dependent
+    // loop, so this harness covers the access over slices up to MAX_LEN.
     #[kani::proof]
     fn check_zip_next_u8() {
         const MAX_LEN: usize = 5000;
@@ -762,10 +762,11 @@ mod verify {
     }
 
     // nth (TRA specialized — uses __iterator_get_unchecked for side effects)
-    // Loop invariants on nth's while loop and super_nth's while-let loop
-    // enable unbounded verification. For slice::Iter, MAY_HAVE_SIDE_EFFECT
-    // is false so nth's loop body is just index increment; super_nth runs
-    // at most once when called from nth.
+    // nth's while loop and super_nth's while-let loop carry vacuous Kani loop
+    // invariants to enable loop-contract mode; this harness covers slices up to
+    // MAX_LEN. For slice::Iter, MAY_HAVE_SIDE_EFFECT is false, so nth's loop body
+    // is just an index increment and super_nth runs at most once when called from
+    // nth (its next()-driven loop does not iterate in this configuration).
     #[kani::proof]
     fn check_zip_nth_u8() {
         const MAX_LEN: usize = 5000;
@@ -792,7 +793,8 @@ mod verify {
     }
 
     // fold (TRANC specialized — uses get_unchecked in a loop)
-    // Loop invariant on source code enables unbounded verification.
+    // The source-level loop invariant abstracts the get_unchecked loop; this
+    // harness covers slices up to MAX_LEN.
     #[kani::proof]
     fn check_zip_fold_u8() {
         const MAX_LEN: usize = 5000;