`loop_old` in loop contracts

[qinheping]

Requested feature: loop_old similar to old that can refers to historic values in loop contracts Use case:

#[kani::loop_invariants(loop_old(x) == y)]

where loop_old(x) refers to the value of x upon the entrance of the loop. Link to relevant documentation (Rust reference, Nomicon, RFC): #3167

Test case:

let mut x: u8 = kani::any_where(|v| *v < 10);
let mut y: u8 = kani::any();
let mut i = 0;
#[kani::loop_invariants(i == 0 || loop_old(x) == y)]
while i < 5{
  if i == 0{
    y = x
  }
  x += 1;
  i += 1;
}

[qinheping]

This issue blocks https://github.com/model-checking/verify-rust-std/pull/152 and https://github.com/model-checking/verify-rust-std/pull/138.