Postconditiosn on FnOnce closures

[xldenis]

Quoting from an email conversation (with permission) with @boulme:

Maintenant, je me demande comment écrire une spécification de ce genre de fonctions ci-dessous qui n'appellent pas la clôture en argument dans certains cas...

fn skip<F:FnOnce() -> ()>(run: F) {

}

fn test<F:FnOnce() -> ()>(b: bool, run: F) {
if b { run() };
}

J'ai essayé les deux méthodes ci-jointes... Dans les deux cas, il y a échec de la preuve sur la postcondition de "example".

Comment faut-il faire ?

The issue was figuring out how to specify a function which didn't call the closure and ensure that we can prove that any mutable captured variables are changed.

extern crate creusot_contracts;
use creusot_contracts::*;

#[ensures(run==old(run))]
fn skip<F:FnOnce() -> ()>(run: F) {
    
}

#[ensures(result == 0i32)]
fn example() -> i32 {
    let mut r = 0i32;
    let run =
        #[ensures (r == 2i32)]
        || { r = 2 };
    skip(run); 
    r
}
    
fn main(){
    example();
}

[xldenis]

In short the answer is to add #[ensures(run.resolve())] to the specification of skip.

The full answer is a bit longer.

Unlike many traditional verification tools, Creusot doesn't really have a notion of 'post-state', it views Rust functions as affine functions which consume their arguments, meaning run no longer exists after the function call.
The only way to have inter-procedure mutations / side-effects is through &mut and thus through propecies.

If we write a function fn drop_mut(x :&mut u32) { } , we specify that x is unchanged by adding the postcondition ^x == *x.

Naturally we can ask ourselves how this can generalize to an arbitrary type, potentially containing mutable borrows (and thus propheties)? well we do it via the Resolve trait. This trait captures the prophetic information that is obtained when a value is dropped, and is available for any type.

In the case of skip we could add a post condition stating that run is resolved, thus that it was dropped while unchanged.