Contracts & Harnesses for wrapping_shl

[Yenyun035]

Resolves #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 Challenge 11: Safety of Methods for Numeric Primitive Types #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.

[Yenyun035]

Thank you @celinval! Another approval is required to merge this PR. @carolynzech or @feliperodri? Could you please review it? Thank you.

[celinval]

Should we add requires (and ensures) for wrapping_shl given that unchecked_shl already has a requires?

Yes, a harness will only check the contract of the verified function not other functions that are annotated with contract.

[celinval]

Thanks