This PR introduces the trait `BoundedArbitrary` which allows for
creation of symbolic values for types up to some bound. This is useful
for doing bounded proofs on types like strings and vecs. I wrote a more
detailed overview of what this PR provides as a new section in the book.

The implementation of BoundedArbitrary for the container types that I
provide are pretty basic and experimental at the moment. Any pointers
here would be useful, and we will probably need to iterate on their
implementations based on actual performance testing.

I added a test case that should fail verification using the `cover!`
macro, however, I'm not sure that I used this correctly. Let me know if
I should make this an expect test, or something else.

I slightly restructured how we deal with the the `std/core` usage in
`kani_core::kani_lib`. Previously we passed in either `std` or `core` to
`kani_core::generate_arbitrary` and `generate_arbitrary` renamed the
import with `use $core as core_path`. However, I couldn't use that same
strategy for `kani_core::generate_bounded_arbitrary` because the import
names would clash. So I lifted the `use $core as core_path` out of the
`kani_core::generate_*` macros.

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

---------

Co-authored-by: Sammy Thomas <[email protected]>