iter: add kani proof for next_unchecked (#280)

Adds `kani` proof and function contract for
`UncheckedIterator::next_unchecked`.

Ensures that the safety invariants are held using the model checker.

Author: 0xllx0

library/core/src/iter/traits/unchecked_iterator.rs

@@ -1,4 +1,8 @@
+use safety::requires;
+
 use crate::iter::TrustedLen;
+#[cfg(kani)]
+use crate::kani;
 
 /// [`TrustedLen`] cannot have methods, so this allows augmenting it.
 ///
@@ -27,10 +31,26 @@ pub(crate) trait UncheckedIterator: TrustedLen {
     /// point you might want to implement this manually instead.
     #[unstable(feature = "trusted_len_next_unchecked", issue = "37572")]
     #[inline]
+    #[requires(self.size_hint().0 != 0 && self.size_hint().1 != Some(0))]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> Self::Item {
         let opt = self.next();
         // SAFETY: The caller promised that we're not empty, and
         // `Self: TrustedLen` so we can actually trust the `size_hint`.
         unsafe { opt.unwrap_unchecked() }
     }
 }
+
+#[cfg(kani)]
+#[kani::proof]
+fn verify_next_unchecked() {
+    let arr: [u8; 1] = [kani::any(); 1];
+
+    let mut it = arr.iter();
+    let (lo_hint, hi_hint) = it.size_hint();
+
+    kani::assume(lo_hint != 0);
+    kani::assume(hi_hint != Some(0));
+
+    let _ = unsafe { it.next_unchecked() };
+}