Add support for uninterpreted function stub

[celinval]

Requested feature: Stubs that behave like an uninterpreted function.
Use case: Generating stubs that return the same arbitrary value for multiple invocations if the inputs are the same.
Link to relevant documentation (Rust reference, Nomicon, RFC): http://www.cprover.org/cprover-manual/modeling/nondeterminism/ and https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html#future-possibilities

Example:

/// This harness has some code that is conditional on the value of a few arguments.
/// Check that it behaves for all combination of arguments, however,
/// an argument should always have the same value.
#[kani::proof]
#[kani::stub_uninterpreted(Arg::is_enabled)]
fn check_uninterpreted() {
    /* logic goes here */
}

Note: We will have to figure out the best mechanism to only return valid values.

[celinval]

@nchong-at-aws would that make sense?

[nchong-at-aws]

Yes, exactly right. The behavior I want is a function whose result is non-deterministic but different calls will return the same value if the inputs are the same.