Add loop_invariant and harness for array reverse (model-checking#430)

This PR adds loop_invariant and harness for array reverse.

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: Michael Tautschnig <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

Author: 3 people

library/core/src/slice/mod.rs

@@ -1011,6 +1011,13 @@ impl<T> [T] {
             let (b, _) = b.split_at_mut(n);
 
             let mut i = 0;
+            #[safety::loop_invariant(i <= n)]
+            #[cfg_attr(kani,
+                       kani::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;
@@ -5495,4 +5502,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 mut a: [u8; 100] = kani::any();
+        a.reverse();
+    }
 }