Support for Primitive Proptests

[YoshikiTakashima]

Description of changes:

Adds support for running proptests with primitive inputs using kani.

Resolved issues:

Resolves #1363

Call-outs:

• Feature only runs with cargo kani.
• Since we are only merging a small portion of proptest, we cannot support proptests like tests/cargo-kani/rectangle-example. This means we disable the proptest import in that test case.

Testing:

• How is this change tested? tests/cargo-kani/proptest

• Is this a refactor change? No.

Checklist

• [x] Each commit message has a non-empty body, explaining why the change was made
• [x] Methods or procedures are documented
• [x] Regression or unit tests are included, or existing tests cover the modified code
• [x] My PR is restricted to a single feature or bugfix

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

[YoshikiTakashima]

As recommended by @danielsn, this PR will be split into the following parts. Only 1 will be under this PR.

1. Build toolchain + proptest Strategy
2. Arbitrary, boolean and tuple
3. numbers and ranges

[danielsn]

We now have a fork of propest. What's the best way to maintain this.

[YoshikiTakashima]

Until the ticket for approving the separate repository goes through, code review for proptests will be managed through the features/proptest branch. The proptest fork will be imported through submodules.

[YoshikiTakashima]

Closing in favor of the following approaches.

1. The following proptest injection scheme works fine once proptest's kanilib dependency is under [target.'cfg(not(kani))'.dependencies] to avoid clash.

proptest = { path = "$PATH_TO/STUBBED/proptest"}

2. Long-term, we probably can support injection done by appending the following to Cargo.toml. We cannot immidately use this b/c the patch feature requires that the offered features of the overriding library match up with the original library. While the override is cleaner, there is no good way to condition this on being specific to cfg(kani).

[patch.crates-io]
proptest = { path = "$PATH_TO/STUBBED/proptest"}