Improvements needed for the 'kani' library

[tedinski]

trafficstars

any, Arbitrary and Invariant

• [ ] The current implementation of Invariant is basically inviting undefined behavior. For instance, an invariant like "this enum must match one of its variants" is something the rust compiler could replace with just true. (It sort of already does: if you do this with pattern matching, it recognizes the wildcard branch as dead code, and Kani helpfully codegen's dead code as assert(false)!)
• [ ] The current implementation of Arbitrary offers essentially nothing useful. For instance, implementing Arbitrary for MyType does not mean you can use any() for Option<MyType> because the implication instances for Option are on Invariant
• [ ] We could move some of these from Invariant to Arbitrary but that starts to eliminate the usefulness of Invariant, and... (next item)
• [ ] In the long term, we DO want Invariant, it's just that we'd want the compiler to synthesize the basic ones for types. (All the invariants that are undefined behavior are the ones we should be able to implement automatically because they're the Rust invariants for types.)
• [ ] We should make any_raw private, users probably shouldn't be using it, and it's mostly UB. It can be mimic'd by getting any bytes and then transmute, with all the obvious UB implications.

any_vec, slices

I don't believe the current API is the one we should consider stabilized.

• [ ] any_slice returns a fairly complicated AnySlice type, because it needs something to own the data. Thing is, the standard library already has a type for that... Vec. I'm not sure why we don't just have any_vec alone here.
• [ ] We should probably mark all raw functions as private.
• [ ] IMO any_slice_of_array should be any_subslice
• [ ] I'm not sure why any_slice and any_vec pass in the bound as a const generic. Seems like it'd be best if it were an ordinary parameter. It makes these hard to use. (I didn't look into the implementations though, so could easily be a reason we have to unfortunately)
• [ ] These implementations should be exported at the top level. i.e. kani::any_vec not kani::vec::any_vec
• [ ] We should add an any_string implementation.

Assertions

• [ ] nondet should be removed or at least doc(hidden)
• [ ] panic should probably be at least doc(hidden). Not something we expect customers to know about.
• [ ] assert should be renamed check
• [ ] expect_fail should be replaced with cover #1197

[celinval]

I tried adding any_string but I either bumped into really poor performance or linking issues. Hopefully we can get back to it once we fix the std lib linking.

[YoshikiTakashima]

I'm not sure why any_slice and any_vec pass in the bound as a const generic. Seems like it'd be best if it were an ordinary parameter. It makes these hard to use. (I didn't look into the implementations though, so could easily be a reason we have to unfortunately)

Generally agreed. I think we will have to move to this direction anyway due to certain protests using this.

Although, one concern is that x : [T;N] = any() has had better performance than the ones I tested with. This is especially true if the bounds are dynamically computed but in a way where there is a clear upper bound.

[celinval]

As discussed offline, regarding the first topic, we will do the following:

• [x] Deprecate Invariant trait and impl Arbitrary for Invariant for now (pending on @YoshikiTakashima potential use case).
• [x] Convert all our implementations of Invariant to Arbitrary.
• [x] Change any_vec to also take an Arbitrary.
• [x] We'll make any_raw private for now.