Create an API for loop contracts

[qinheping]

Requested feature: Loop contracts
Use case: Verify the provided loop contracts, and use the loop contracts to abstract out the loops from the verification process.
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167

Test case:

#[kani::proof]
fn main() {
    let mut x: u64 = kani::any_where(|i| *i >= 1);

    #[kani::loop_invariant(x >= 1)]
    while x > 1{
        x = x - 1;
    };

    assert!(x == 1);
}