Add support to type invariants

[celinval]

Requested feature: Users should be able to specify and verify type safety invariants.
Use case: Users often encode safety of a type as a relationship between its internal variables, and Kani should provide a mechanism for users to specify the invariants and verify them.
Link to relevant documentation (Rust reference, Nomicon, RFC): https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html