Harnesses for carrying_mul

[lanfeima]

Towards: Issue #59

Parent branch: main

---

Changes

• Added macros for generating carrying_mul harnesses
• Added harnesses for carrying_mul for the following integer types:
  • u8, u16, u32, u64

Revalidation

Per the discussion in issue #59, we have to build and run Kani from the 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., carrying_mul_u8_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

[celinval]

I was wondering if we can use wider intervals.

[celinval]

Thank you!