iter: add kani proof for next_unchecked (rust-lang#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

@@ -31,7 +31,7 @@ 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)]
+    #[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();
@@ -40,3 +40,17 @@ pub(crate) trait UncheckedIterator: TrustedLen {
         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() };
+}