Contracts & Harnesses for widening_mul

[rajathkotyal]

Towards : issue #59

Parent branch : main

Revalidation :
Per the discussion in #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. widening_mul_u16_small) to run a specific harness.

kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates

[rajathkotyal]

Thanks @celinval! , Need another approval on this before merge. @carolynzech could you please review it?