add loop_invariant and harness

Author: thanhnguyen-aws

library/core/src/slice/mod.rs

@@ -1008,6 +1008,8 @@ impl<T> [T] {
             let (b, _) = b.split_at_mut(n);
 
             let mut i = 0;
+            #[safety::loop_invariant(i <= n)]
+            #[safety::loop_modifies(unsafe {slice::from_raw_parts_mut(a.as_mut_ptr(), n)}, unsafe {slice::from_raw_parts_mut(b.as_mut_ptr(), n)}, &i)]
             while i < n {
                 mem::swap(&mut a[i], &mut b[n - 1 - i]);
                 i += 1;
@@ -5565,4 +5567,10 @@ mod verify {
     gen_align_to_mut_harnesses!(align_to_mut_from_bool, bool);
     gen_align_to_mut_harnesses!(align_to_mut_from_char, char);
     gen_align_to_mut_harnesses!(align_to_mut_from_unit, ());
+
+    #[kani::proof]
+    fn check_reverse() {
+        let a: [u8; 100] = kani::any();
+        let b = a.reverse();
+    }
 }