Add support for loop-contract historic values

[thanhnguyen-aws]

Add support for old and prev to refers to historic values in loop contracts where

• old(expr) refers to the value of the expr before the loop.
• prev(expr) refers to the value of the expr at the previous iteration.

Resolves#3697

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

[tautschnig]

Looks like you want to run kani-fmt.sh to address the test failure.

[remi-delmas-3000]

Could we use on_entry(...) instead of old(...) ? The doc itself says "old(...) denotes the value on loop entry".

Some documentation describing the transformation at a high level would help the review.

[qinheping]

I am a bit confused about the semantics of prev. How do we check the loop invariant for the first case where there is no prev valuation?

[qinheping]

LGTM. Thank you!