History Expressions

[JustusAdam]

Add support for History Expressions. This allows an ensures clause to evaluate expressions before the function runs, bing them to anonymous variables and use them after calculating the result to be able to compare to the state before the function evaluation.

TODO

• Update external documentation with information about how history expressions are used
• Update internal documentation with expanded example of how old is implemented
• Test case. I could use some help here both with implementing test cases as well as with suggestions for other things to test. Here is the list so far
  • Basic pass/fail
  • pass/fail on using clone and not using clone respectively for a reference
  • Using a function call in old
  • Using a block expression (e.g. sequence of statements) as argument to old
  • Denying nesting of old, e.g. old(... old( ) ... )

Resolves #2803

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

[pi314mm]

Maybe this should be

let (history_variables, history_exprs) = history_expressions.iter().unzip();

instead of creating two iters

[JustusAdam]

unzip requires creation of two intermediate vectors though because it doesn't split into an iterator but has to be collected.

[pi314mm]

This seems like it would cause problems with the result ident since all idents are lifted, or in the event of someone making a locally bound variable within a closure, so something like ensures((|a| old(a)) (argument)). Wouldn't it be easier to implement if we require that the argument for old be an ident instead of an expression?

Here is an example of something reasonable that breaks

#[kani::ensures((|a| old(*ptr+a))(1) == *ptr)]
fn modify(ptr: &mut u32) {
    *ptr += 1;
}

Here is another example of something reasonable that breaks

#[kani::ensures(old(*ptr+result) == *ptr)]
fn modify(ptr: &mut u32) -> u32 {
    *ptr += 1;
    1
}