Address Copilot review feedback on PR model-checking#549

- Remove unused `loop_invariant` import in take.rs and zip.rs
  (#[cfg_attr(kani, kani::loop_invariant(...))] does not require it)
- Rewrite `Zip::get_unchecked` `#[requires(...)]` to avoid `self.index + idx`
  overflow, using subtraction-based bounds
- Clarify "vacuous loop invariant" comments in take.rs and zip.rs — note
  that `true` is intentional and only enables loop-contract mode
- Reword "Loop invariant:" to "Safety argument:" in array_chunks.rs to
  avoid implying a verified invariant where there is none (bounded harness)

Author: Kasim Te

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

@@ -232,9 +232,9 @@ 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.
-        // Loop invariant: __iterator_get_unchecked is read-only for
+        // Safety argument: __iterator_get_unchecked is read-only for
         // TrustedRandomAccessNoCoerce iterators, so iter.size() is preserved.
-        // Loop invariant: i tracks the consumed element count and stays within
+        // Safety argument: i tracks the consumed element count and stays within
         // inner_len. Combined with the while condition (inner_len - i >= N),
         // this ensures i + local < inner_len = iter.size() for all accesses.
         while inner_len - i >= N {

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

@@ -1,5 +1,3 @@
-use safety::loop_invariant;
-
 use crate::cmp;
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, TrustedRandomAccess};
@@ -303,8 +301,10 @@ impl<I: Iterator + TrustedRandomAccess> SpecTake for Take<I> {
     {
         let mut acc = init;
         let end = self.n.min(self.iter.size());
-        // Loop invariant: __iterator_get_unchecked is a read-only operation for
-        // TrustedRandomAccess iterators, so iter.size() is preserved across iterations.
+        // __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

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

@@ -1,4 +1,4 @@
-use safety::{loop_invariant, requires};
+use safety::requires;
 
 use crate::cmp;
 use crate::fmt::{self, Debug};
@@ -271,7 +271,12 @@ where
     }
 
     #[inline]
-    #[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]
+    #[requires(
+        self.index <= self.a.size()
+            && idx < self.a.size() - self.index
+            && self.index <= self.b.size()
+            && idx < self.b.size() - self.index
+    )]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item {
         let idx = self.index + idx;
@@ -287,12 +292,14 @@ where
     {
         let mut accum = init;
         let len = ZipImpl::size_hint(&self).0;
-        // Loop invariant: get_unchecked is a read-only operation for
-        // TrustedRandomAccessNoCoerce iterators, so sizes are preserved.
-        // Loop invariant enables loop contracts for unbounded verification.
+        // For TrustedRandomAccessNoCoerce iterators, get_unchecked is a
+        // read-only operation, so sizes are preserved.
         // Safety of get_unchecked(i) is established by the pre-loop state:
         // len = min(a.size(), b.size()) - index, and get_unchecked adds index
         // back, so the actual index is always < both sizes.
+        // The Kani loop invariant below is intentionally vacuous (`true`) and
+        // is used only to enable loop-contract mode, not to encode these
+        // bounds or size properties directly.
         #[cfg_attr(kani, kani::loop_invariant(true))]
         for i in 0..len {
             // SAFETY: since Self: TrustedRandomAccessNoCoerce we can trust the size-hint to