Contracts & Harnesses for wrapping_shr (model-checking#123)

Towards model-checking#59

Changes
Added contracts for wrapping_shr (located in
library/core/src/num/int_macros.rs and uint_macros.rs)
Added harnesses for wrapping_shr of each integer type
i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize --- 12
harnesses in total.
Revalidation
Per the discussion in
model-checking#59, we have to
build and run Kani from feature/verify-rust-std branch.
To revalidate the verification results, run the following command.
<harness_to_run> can be either num::verify to run all harnesses or
num::verify::<harness_name> (e.g. checked_wrapping_shl_i8) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```
All harnesses should pass the default checks (1251 checks where 1
unreachable).

```
SUMMARY:
 ** 0 of 161 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.32086188s

Complete - 12 successfully verified harnesses, 0 failures, 12 total.
```

Example of the unreachable check:
```
Check 9: num::<impl i8>::wrapping_shr.assertion.1
	 - Status: UNREACHABLE
	 - Description: "attempt to subtract with overflow"
	 - Location: library/core/src/num/int_macros.rs:2199:42 in function num::<impl i8>::wrapping_shr
```

---------

Co-authored-by: Yenyun035 <[email protected]>

Author: MWDZ

library/core/src/num/int_macros.rs

@@ -2191,6 +2191,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[rustc_allow_const_fn_unstable(unchecked_shifts)]
+        #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
         pub const fn wrapping_shr(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds

library/core/src/num/mod.rs

@@ -1943,4 +1943,28 @@ mod verify {
     generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64);
     generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128);
     generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize);
+
+    // `wrapping_shr` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
+    // Target function:
+    // pub const fn wrapping_shr(self, rhs: u32) -> Self {
+    //
+    // This function performs an panic-free bitwise right shift operation.
+    generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8);
+    generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16);
+    generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32);
+    generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64);
+    generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128);
+    generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize);
+    generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8);
+    generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16);
+    generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32);
+    generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
+    generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
+    generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
 }

library/core/src/num/uint_macros.rs

@@ -2172,6 +2172,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[rustc_allow_const_fn_unstable(unchecked_shifts)]
+        #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
         pub const fn wrapping_shr(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds