Fix contract expansion for old

[carolynzech]

Fixes the macro expansion for contracts to properly place history expressions.

Problem

Before this PR, instantiations of "remembers variables" (i.e., the variables that save the value before the function executes) were always put above any statements from previous macro expansions. For example, for this code (from #3359):

#[kani::requires(val < i32::MAX)]
#[kani::ensures(|result| *result == old(val + 1))]
pub fn next(mut val: i32) -> i32 {
    val + 1
}

Kani would first expand the requires attribute and insert kani::assume(val < i32::MAX). The expansion of ensures would then put the remembers variables first, generating this:

let remember_kani_internal_1e725538cd5566b8 = val + 1;
kani::assume(val < i32::MAX);

which causes an integer overflow because we don't restrict the value of val before adding 1. Instead, we want:

kani::assume(val < i32::MAX);
let remember_kani_internal_1e725538cd5566b8 = val + 1;

Solution

The solution is to insert the remembers variables immediately after preconditions--that way, they respect the preconditions but are still declared before the function under contract executes. When we're expanding an ensures clause, we iterate through each of the already-generated statements, find the position where the preconditions end, then insert the remembers variables there. For instance:

kani::assume(x < 100);
kani::assume(y < 10);
kani::assume(x + y < 105);
<-- remembers variables go here -->
let _wrapper_arg = ...

---

Resolves #3359

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Thank you for fixing this!