Change ensures into closures

[pi314mm]

This change now separates the front facing "result" name and the internal facing "result_kani_internal" ident where the user can specify with the keyword "result" but then the system replaces this with the internal representation.

If the user chooses to use a different variable name than result, this now supports the syntax of
#[kani::ensures(|result_var| expr)]
where result_var can be any arbitrary name.

For example, the following test now works:

#[kani::ensures(|banana : &u32| *banana == a.wrapping_add(b))]
fn simple_addition(a: u32, b: u32) -> u32 {
    return a.wrapping_add(b);
}

In addition, the string "result_kani_internal" is now a global constant and can be updated in a single place if needed.

Resolves #2597 since the user can specify the variable name they want within the ensures binding

An important change is that the result is now a pass by reference instead, so as in the example an &u32 instead of u32

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

[JustusAdam]

Hey @pi314mm, thanks a lot for contributing to fix this. I also had some ideas on how to fix it and I wonder what you think about it. The issue is that while currently result is the only "contract special" thing, in the future we will also need some way to express history expressions, for which we intended to add a special old(...) function to postconditions that returns a pre-function-execution version of whatever value was passed.

Now this function suffers from the same problem as result in that a user may have some other old in scope. I was thinking a way to solve this is to use the @ operator to prefix such intrinsics, e.g. it would be @result and @old(...).

Alternatively we could do it like the stdlib which as a use std::prelude::* but you can override that and use an explicit import instead. So in our case this could mean that there is an implicit use kani::{old, result} which the user can override by having an explicit use kani::result as my_result, which would cause kani to use my_result but not result as the return variable. And this would function for old as well and the further benefit is that this does not require any new syntax, though the macro code required to make this happen is a bit more involved (and involves scoping).

What do we think about this?

[pi314mm]

I believe we should remove the functionality which defaults the "result" variable to "result" and require that the user specify the result variable for every ensures statement. The ensures statement should be thought of as a closure rather than a statement where the argument to the function is the result of the computation. This can be achieved by changing this if statement into an error statement. It would require modifying currently existing ensures statements to kani::ensures(result => _) since this would make the variable name explicit. This way leaves no room for error, since the user must specify the name themselves, and leaving no room for error is definitely good from a formal verification perspective.

For the case of "old" variables, it is best to think of it as a kani function, so using "kani::old(argument)" would be a good way to parse it. Since we specify that this is the kani::old instead of just "old" we avoid collisions that way. Or it may be reasonable to do "argument@old" without spaces to represent the same concept. But regardless, this issue is tangential to the result variable.

[JustusAdam]

I can see an argument for the likeness to a closure, but if that is the way we want to go, I would actually use closure syntax instead of introducing a new one. Sure the => is used in match, but this is not a match expression.

[pi314mm]

That is a great idea and a lot easier and cleaner to implement! This new commit now expects a closure, then applies the internal kani result variable to this function, essentially an eta expansion.

Since we are now using the built-in support for parsing closures, we can do pattern matching on the result variable. For example, the following code works:

#[kani::ensures(|(orange, banana)| orange == 5 && banana == a.wrapping_add(b))]
fn simple_addition(a: u32, b: u32) -> (u32, u32) {
    return (5, a.wrapping_add(b));
}

[JustusAdam]

That is a great idea and a lot easier and cleaner to implement! This new commit now expects a closure, then applies the internal kani result variable to this function, essentially an eta expansion.

Nice. This should also make it quite easy to explain. The idea of providing a closure that gets applied to the result is quite intuitive.

[celinval]

I like the idea of using a closure. @pnkfelix, what do you think about that?

@pi314mm can you please fix the CI.

[pnkfelix]

I like the idea of using a closure. @pnkfelix, what do you think about that?

I'm in favor of the change.

I had in fact thought I had seen precedent for #[ensures(|result| { pred(result) })] elsewhere, but a quick skim of my usual suspects (Verus, Creusot, Prusti, Aeneas) has not yielded fruit. So I'm not sure where I had seen it before...

[pi314mm]

It seems as this was harder to implement than expected.

Changing the variable names to _renamed no longer seems to be working as it was before. Will look into it. Edit: fixed

Additionally, the pass of the result to the closure must be a pass by reference.

[pnkfelix]

Additionally, the pass of the result to the closure must be a pass by reference.

Hmm. I'm surprised by this. I might want to locally check out your work prior to 8e2e610 and try to understand why this is necessary.

Update: Oh, I bet I know why; its probably because the closure isn't set up to return the result back to the caller after the predicate runs. (You could consider injecting code into the end of the closure to do that, but then the return type would have to be something like (bool, ResultType) instead of just bool ...)

(We actually encountered something similar to this internally within the compiler itself, in that match-arm-guards, we treat uses of identifiers bound by the match-pattern as implicitly borrowed, and automatically inject derefs of them, see rust-lang/rust#49870 for that context ...)

[celinval]

I don't think passing a reference is a bad thing though. We do want to restrict the result access to be read only and passing a constant reference is a clear indication of that.

[JustusAdam]

Please also make sure to update the following public documentation

• for the usage of ensures specifically

  kani/library/kani_macros/src/lib.rs

  Line 144 in 4a88939

  #[proc_macro_attribute]

• for high-level contracts overview (and examples) https://github.com/model-checking/kani/blob/main/library/kani/src/contracts.rs

as well as the internal "desugaring" documentation in https://github.com/model-checking/kani/blob/main/library/kani_macros/src/sysroot/contracts/mod.rs

[feliperodri]

Thanks for this contribution! Could you also update our RFC to reflect this change?