Start the verification of slice::Iter

There are a few harnesses failing that needs further debugging.
I commented them out for now.

library/core/src/slice/iter.rs

@@ -14,6 +14,11 @@ use crate::num::NonZero;
 use crate::ptr::{self, without_provenance, without_provenance_mut, NonNull};
 use crate::{cmp, fmt};
 
+#[cfg(kani)]
+use crate::kani;
+
+use crate::ub_checks::Invariant;
+
 #[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<T> !Iterator for [T] {}
 
@@ -157,6 +162,23 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
     }
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> crate::ub_checks::Invariant for Iter<'_, T> {
+    fn is_safe(&self) -> bool {
+        let ty_size = crate::mem::size_of::<T>();
+        let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
+        if ty_size == 0 || distance == 0 {
+            self.ptr.is_aligned()
+        } else {
+            let slice_ptr: *const [T] = crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
+            crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
+                && self.ptr.addr().get() <= self.end_or_len as usize
+                && distance % ty_size == 0
+                && crate::ub_checks::can_dereference(slice_ptr)
+        }
+    }
+}
+
 /// Mutable slice iterator.
 ///
 /// This struct is created by the [`iter_mut`] method on [slices].
@@ -196,6 +218,24 @@ pub struct IterMut<'a, T: 'a> {
     _marker: PhantomData<&'a mut T>,
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> crate::ub_checks::Invariant for IterMut<'_, T> {
+    fn is_safe(&self) -> bool {
+        let size = crate::mem::size_of::<T>();
+        if size == 0 {
+            self.ptr.is_aligned()
+        } else {
+            let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
+            let slice_ptr: *mut [T] = crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
+            crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
+                && self.ptr.addr().get() <= self.end_or_len as usize
+                && distance % size == 0
+                && crate::ub_checks::can_dereference(slice_ptr)
+                && crate::ub_checks::can_write(slice_ptr)
+        }
+    }
+}
+
 #[stable(feature = "core_impl_debug", since = "1.9.0")]
 impl<T: fmt::Debug> fmt::Debug for IterMut<'_, T> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
@@ -3464,3 +3504,123 @@ impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> {
         f.debug_struct("ChunkByMut").field("slice", &self.slice).finish()
     }
 }
+
+/// Verify the safety of the code implemented in this module (including generated code from macros).
+#[unstable(feature = "kani", issue="none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let first = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let last = kani::any_where(|idx: &usize| *idx >= first && *idx <= orig_slice.len());
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_iter<'a, T>(orig_slice: &'a [T]) -> Iter<'a, T> {
+        let slice = any_slice(orig_slice);
+        Iter::new(slice)
+    }
+
+    /// Macro that generates a harness for a given `Iter` method.
+    ///
+    /// Takes the name of the harness, the element type, and an expression to check.
+    macro_rules! check_safe_abstraction {
+        ($harness:ident, $elem_ty:ty, $call:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut iter = any_iter::<$elem_ty>(&array);
+                let target = $call;
+                target(&mut iter);
+                kani::assert(iter.is_safe(), "Iter is safe");
+            }
+        };
+    }
+
+    /// Macro that generates a harness for a given unsafe `Iter` method.
+    ///
+    /// Takes:
+    /// 1. The name of the harness
+    /// 2. the element type
+    /// 3. the target function
+    /// 4. the optional arguments.
+    macro_rules! check_unsafe_contracts {
+        ($harness:ident, $elem_ty:ty, $func:ident($($args:expr),*)) => {
+            #[kani::proof_for_contract(Iter::$func)]
+            fn $harness() {
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut iter = any_iter::<$elem_ty>(&array);
+                let _ = unsafe { iter.$func($($args),*) };
+            }
+        };
+    }
+
+    macro_rules! check_iter_with_ty {
+        ($module:ident, $ty:ty, $max:expr) => {
+            mod $module {
+                use super::*;
+                const MAX_LEN: usize = $max;
+
+                #[kani::proof]
+                fn check_new_iter() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_slice::<$ty>(&array);
+                    let mut iter = Iter::new(slice);
+                    kani::assert(iter.is_safe(), "Iter is safe");
+                }
+
+                /// Count consumes the value, thus, invoke it directly.
+                #[kani::proof]
+                fn check_count() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter::<$ty>(&array);
+                    iter.count();
+                }
+
+                #[kani::proof]
+                fn check_default() {
+                    let iter: Iter<'_, $ty> = Iter::default();
+                    kani::assert(iter.is_safe(), "Iter is safe");
+                }
+
+                check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked());
+                //check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
+                //check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
+
+                // FIXME: The functions that are commented out are currently failing verification.
+                // Debugging the issue is currently blocked by:
+                // https://github.com/model-checking/kani/issues/3670
+                //
+                // Public functions that call safe abstraction `make_slice`.
+                // check_safe_abstraction!(check_as_slice, $ty, as_slice);
+                // check_safe_abstraction!(check_as_ref, $ty, as_ref);
+
+                // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
+
+                check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.is_empty(); });
+                check_safe_abstraction!(check_len, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.len(); });
+                check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.size_hint(); });
+                //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
+                //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
+                //check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); });
+                //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
+                check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next(); });
+
+                // Ensure that clone always generates a safe object.
+                check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| { kani::assert(iter.clone().is_safe(), "Clone is safe"); });
+            }
+        };
+    }
+
+    check_iter_with_ty!(verify_unit, (), isize::MAX as usize);
+    check_iter_with_ty!(verify_u8, u8, u32::MAX as usize);
+    check_iter_with_ty!(verify_char, char, 50);
+    check_iter_with_ty!(verify_tup, (char, u8), 50);
+}

library/core/src/slice/iter/macros.rs

@@ -77,6 +77,9 @@ macro_rules! iterator {
             ///
             /// The iterator must not be empty
             #[inline]
+            #[cfg_attr(kani, kani::modifies(self))]
+            #[safety::requires(!is_empty!(self))]
+            #[safety::ensures(|_| self.is_safe())]
             unsafe fn next_back_unchecked(&mut self) -> $elem {
                 // SAFETY: the caller promised it's not empty, so
                 // the offsetting is in-bounds and there's an element to return.
@@ -96,6 +99,9 @@ macro_rules! iterator {
             // returning the old start.
             // Unsafe because the offset must not exceed `self.len()`.
             #[inline(always)]
+            #[cfg_attr(kani, kani::modifies(self))]
+            #[safety::requires(offset <= len!(self))]
+            #[safety::ensures(|_| self.is_safe())]
             unsafe fn post_inc_start(&mut self, offset: usize) -> NonNull<T> {
                 let old = self.ptr;
 
@@ -115,6 +121,9 @@ macro_rules! iterator {
             // returning the new end.
             // Unsafe because the offset must not exceed `self.len()`.
             #[inline(always)]
+            #[cfg_attr(kani, kani::modifies(self))]
+            #[safety::requires(offset <= len!(self))]
+            #[safety::ensures(|_| self.is_safe())]
             unsafe fn pre_dec_end(&mut self, offset: usize) -> NonNull<T> {
                 if_zst!(mut self,
                     // SAFETY: By our precondition, `offset` can be at most the
@@ -369,6 +378,7 @@ macro_rules! iterator {
             }
 
             #[inline]
+            #[safety::requires(idx < len!(self))]
             unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                 // SAFETY: the caller must guarantee that `i` is in bounds of
                 // the underlying slice, so `i` cannot overflow an `isize`, and
@@ -437,6 +447,7 @@ macro_rules! iterator {
 
         impl<'a, T> UncheckedIterator for $name<'a, T> {
             #[inline]
+            #[safety::requires(!is_empty!(self))]
             unsafe fn next_unchecked(&mut self) -> $elem {
                 // SAFETY: The caller promised there's at least one more item.
                 unsafe {

library/core/src/ub_checks.rs

@@ -162,11 +162,17 @@ pub(crate) const fn is_nonoverlapping(
     const_eval_select((src, dst, size, count), comptime, runtime)
 }
 
+pub trait Invariant {
+    /// Specify the type's safety invariants
+    fn is_safe(&self) -> bool;
+}
+
 pub use predicates::*;
 
 /// Provide a few predicates to be used in safety contracts.
 ///
 /// At runtime, they are no-op, and always return true.
+/// FIXME: In some cases, we could do better, for example check if not null and aligned.
 #[cfg(not(kani))]
 mod predicates {
     /// Checks if a pointer can be dereferenced, ensuring:
@@ -203,9 +209,16 @@ mod predicates {
         let _ = dst;
         true
     }
+
+    /// Checks if two pointers point to the same allocation.
+    pub fn same_allocation<T>(src: *const T, dst: *const T) -> bool {
+        let _ = (src, dst);
+        true
+    }
 }
 
 #[cfg(kani)]
 mod predicates {
-    pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned};
+    pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned,
+    same_allocation};
 }