Contracts & Harnesses for wrapping_shl (rust-lang#112)

Towards rust-lang#59 

### Changes
* Added contracts for `wrapping_shl` (located in
`library/core/src/num/int_macros.rs` and `uint_macros.rs`)
* Added a macro for generating wrapping_{shl, shr} harnesses
* Added harnesses for `wrapping_shl` of each integer type
* `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`,
`u128`, `usize` --- 12 harnesses in total.

### Revalidation
1. Per the discussion in rust-lang#59, we have to **build and run Kani from
`feature/verify-rust-std` branch**.
2. 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 1251 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 2.4682913s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```
Example of the unreachable check:
```
Check 123: num::<impl i8>::wrapping_shl.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/num/int_macros.rs:2172:42 in function num::<impl i8>::wrapping_shl
```

### Questions
1. Should we add `requires` (and `ensures`) for `wrapping_shl` given
that `unchecked_shl` already has a `requires`?

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

library/core/src/num/int_macros.rs

@@ -2160,6 +2160,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_shl(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

@@ -1687,6 +1687,19 @@ mod verify {
         }
     }
 
+    // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}`
+    macro_rules! generate_wrapping_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
+
+                let _ = num1.$method(num2);
+            }
+        }
+    }
+
     // `unchecked_add` proofs
     //
     // Target types:
@@ -1905,4 +1918,29 @@ mod verify {
         widening_mul_u64_large, u64::MAX - 10u64, u64::MAX,
         widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64
     );
+
+    // `wrapping_shl` 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_shl(self, rhs: u32) -> Self
+    //
+    // This function performs an panic-free bitwise left shift operation.
+    generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8);
+    generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16);
+    generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32);
+    generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64);
+    generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128);
+    generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize);
+    generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8);
+    generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16);
+    generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32);
+    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);
 }

library/core/src/num/uint_macros.rs

@@ -2138,6 +2138,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_shl(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds