LLM-generated contracts for __iterator_get_unchecked (model-checking#435)

Preconditions generated by Claude for files containing
`__iterator_get_unchecked`.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Fedor Ryabinin <[email protected]>
Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

Author: 4 people

library/alloc/src/collections/vec_deque/iter.rs

@@ -1,8 +1,12 @@
 use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use core::kani;
 use core::num::NonZero;
 use core::ops::Try;
 use core::{fmt, mem, slice};
 
+use safety::requires;
+
 /// An iterator over the elements of a `VecDeque`.
 ///
 /// This `struct` is created by the [`iter`] method on [`super::VecDeque`]. See its
@@ -144,6 +148,8 @@ impl<'a, T> Iterator for Iter<'a, T> {
     }
 
     #[inline]
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // Safety: The TrustedRandomAccess contract requires that callers only pass an index
         // that is in bounds.

library/alloc/src/collections/vec_deque/iter_mut.rs

@@ -1,8 +1,12 @@
 use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use core::kani;
 use core::num::NonZero;
 use core::ops::Try;
 use core::{fmt, mem, slice};
 
+use safety::requires;
+
 /// A mutable iterator over the elements of a `VecDeque`.
 ///
 /// This `struct` is created by the [`iter_mut`] method on [`super::VecDeque`]. See its
@@ -208,6 +212,8 @@ impl<'a, T> Iterator for IterMut<'a, T> {
     }
 
     #[inline]
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // Safety: The TrustedRandomAccess contract requires that callers only pass an index
         // that is in bounds.

library/alloc/src/vec/into_iter.rs

@@ -2,6 +2,8 @@ use core::iter::{
     FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen,
     TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use core::kani;
 use core::marker::PhantomData;
 use core::mem::{ManuallyDrop, MaybeUninit, SizedTypeProperties};
 use core::num::NonZero;
@@ -11,6 +13,8 @@ use core::ptr::{self, NonNull};
 use core::slice::{self};
 use core::{array, fmt};
 
+use safety::requires;
+
 #[cfg(not(no_global_oom_handling))]
 use super::AsVecIntoIter;
 use crate::alloc::{Allocator, Global};
@@ -354,6 +358,8 @@ impl<T, A: Allocator> Iterator for IntoIter<T, A> {
         R::from_output(accum)
     }
 
+    #[requires(i < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, i: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,

library/core/src/array/iter.rs

@@ -1,7 +1,11 @@
 //! Defines the `IntoIter` owned iterator for arrays.
 
+use safety::requires;
+
 use crate::intrinsics::transmute_unchecked;
 use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::MaybeUninit;
 use crate::num::NonZero;
 use crate::ops::{IndexRange, Range, Try};
@@ -138,6 +142,8 @@ impl<T, const N: usize> IntoIter<T, N> {
     /// ```
     #[unstable(feature = "array_into_iter_constructors", issue = "91583")]
     #[inline]
+    #[requires(initialized.start <= initialized.end)]
+    #[requires(initialized.end <= N)]
     pub const unsafe fn new_unchecked(
         buffer: [MaybeUninit<T>; N],
         initialized: Range<usize>,
@@ -279,6 +285,8 @@ impl<T, const N: usize> Iterator for IntoIter<T, N> {
     }
 
     #[inline]
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // SAFETY: The caller must provide an idx that is in bound of the remainder.
         let elem_ref = unsafe { self.as_mut_slice().get_unchecked_mut(idx) };

library/core/src/char/mod.rs

@@ -24,6 +24,8 @@ mod convert;
 mod decode;
 mod methods;
 
+use safety::requires;
+
 // stable re-exports
 #[rustfmt::skip]
 #[stable(feature = "try_from", since = "1.34.0")]
@@ -47,6 +49,8 @@ use crate::error::Error;
 use crate::escape::{AlwaysEscaped, EscapeIterInner, MaybeEscaped};
 use crate::fmt::{self, Write};
 use crate::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 
 // UTF-8 ranges and tags for encoding characters
@@ -138,6 +142,7 @@ pub const fn from_u32(i: u32) -> Option<char> {
 #[rustc_const_stable(feature = "const_char_from_u32_unchecked", since = "1.81.0")]
 #[must_use]
 #[inline]
+#[requires(i <= 0x10FFFF && (i < 0xD800 || i > 0xDFFF))]
 pub const unsafe fn from_u32_unchecked(i: u32) -> char {
     // SAFETY: the safety contract must be upheld by the caller.
     unsafe { self::convert::from_u32_unchecked(i) }
@@ -399,6 +404,7 @@ macro_rules! casemappingiter_impls {
                 self.0.advance_by(n)
             }
 
+            #[requires(idx < self.0.len())]
             unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                 // SAFETY: just forwarding requirements to caller
                 unsafe { self.0.__iterator_get_unchecked(idx) }
@@ -533,6 +539,8 @@ impl Iterator for CaseMappingIter {
         self.0.advance_by(n)
     }
 
+    #[requires(idx < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
         // SAFETY: just forwarding requirements to caller
         unsafe { self.0.__iterator_get_unchecked(idx) }

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

@@ -1,8 +1,12 @@
 use core::num::NonZero;
 
+use safety::requires;
+
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedLen, UncheckedIterator};
+#[cfg(kani)]
+use crate::kani;
 use crate::ops::Try;
 
 /// An iterator that clones the elements of an underlying iterator.
@@ -61,6 +65,7 @@ where
         self.it.map(T::clone).fold(init, f)
     }
 
+    #[requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
         Self: TrustedRandomAccessNoCoerce,

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

@@ -1,6 +1,10 @@
+use safety::requires;
+
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::{MaybeUninit, SizedTypeProperties};
 use crate::num::NonZero;
 use crate::ops::Try;
@@ -92,6 +96,7 @@ where
         self.it.advance_by(n)
     }
 
+    #[requires(idx < self.it.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
     where
         Self: TrustedRandomAccessNoCoerce,

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

@@ -1,6 +1,10 @@
+use safety::requires;
+
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
@@ -160,6 +164,8 @@ where
 
     #[rustc_inherit_overflow_checks]
     #[inline]
+    #[requires(idx < self.iter.size_hint().0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item
     where
         Self: TrustedRandomAccessNoCoerce,

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

@@ -1,9 +1,13 @@
+use safety::requires;
+
 use crate::intrinsics;
 use crate::iter::adapters::SourceIter;
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::{
     FusedIterator, TrustedFused, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::ops::Try;
 
 /// An iterator that yields `None` forever after the underlying iterator
@@ -109,6 +113,8 @@ where
     }
 
     #[inline]
+    #[requires(self.iter.is_some() && idx < self.iter.as_ref().unwrap().size_hint().0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
         Self: TrustedRandomAccessNoCoerce,

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

@@ -1,7 +1,11 @@
+use safety::requires;
+
 use crate::fmt;
 use crate::iter::adapters::zip::try_get_unchecked;
 use crate::iter::adapters::{SourceIter, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, UncheckedIterator};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
@@ -129,6 +133,7 @@ where
     }
 
     #[inline]
+    #[requires(idx < self.iter.size_hint().0)]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> B
     where
         Self: TrustedRandomAccessNoCoerce,