Help with FnMut closures capturing mutable references

[ia0]

Consider the following example:

#[requires(f.precondition(()))]
#[ensures(f.postcondition_once((), ()))]
fn apply_once<F: FnOnce()>(f: F) {
    f()
}

#[requires(f.precondition(()))]
#[ensures(exists<g: F> f.postcondition_mut((), g, ()) && resolve(&g))]
fn apply_mut<F: FnMut()>(mut f: F) {
    f()
}

fn foo() {
    let mut x = 13;
    let r = &mut x;
    #[invariant((*r)@ == 13 + produced.len())]
    for _ in 0 .. 42 - 13 {
        // BEGIN loop body
        let r = &mut *r;
        apply_once(
            #[cfg_attr(creusot, requires((*r)@ < 42))]
            #[cfg_attr(creusot, ensures((^old(r))@ == (*old(r))@ + 1))]
            move || *r += 1,
        );
        // END loop body
    }
    proof_assert!(x@ == 42);
}

As written it passes cargo creusot prove. I would like to know how to annotate the closure in the following 3 alternatives for the loop body:

• let r = &mut *r; apply_mut(move || *r += 1); (solved)
• apply_once(|| *r += 1);
• apply_mut(|| *r += 1);

Thanks!

[ia0]

• let r = &mut *r; apply_mut(move || *r += 1);

This works (needs to relate the mutable reference of the capture before and after the call):

            #[cfg_attr(creusot, requires((*r)@ < 42))]
            #[cfg_attr(creusot, ensures((*r)@ == (*old(r))@ + 1))]
            #[cfg_attr(creusot, ensures((^r)@ == (^old(r))@))]

[ia0]

It seems to me the problem is that variables in the contract don't refer to the captured field in the closure but to the captured variable outside the closure. Maybe the problem is that non-move closures are not supported yet in Creusot?

[jhjourdan]

Your example reveals several problems in Creusot, thanks!

1- The annotation we would like to write is:

#[requires((*r)@ < 42)]
#[ensures((*old(r))@ == (*r)@ + 1)]
|| *r += 1

However, for some reason, the borrow checker refuses it. It seems like variables used in old are not ignored by the borrow checker. I just reported it as #1396.

But in fact, in this simple case, we don't need an annotation, Creusot can infer the specification of he closure. So we can simply remove requires/ensures. But it does not work in you example because...

2- We usually have a static analysis which proves that prophecies of borrows in local variables are constant. But when a borrow is captured in a closure, then this analysis fails. Thus we need to insert the invariant manually:

    let snap_r = snapshot!{ r };
    #[invariant((*r)@ == 13 + produced.len())]
    #[invariant(^*snap_r == ^r)]
    for _ in 0 .. 42 - 13 {

And then, this works both with apply_once and apply_mut.

[xldenis]

We usually have a static analysis which proves that prophecies of borrows in local variables are constant. But when a borrow is captured in a closure, then this analysis fails

Shouldn't that be guaranteed by the behavior of closure captures? ie: we should be easily able to extend the analysis to account for this? alternatively it could add an invariant talking about unnest of the closure since this is what's missing.

[jhjourdan]

Sure, this may not be too difficult to implement.

[ia0]

alternatively it could add an invariant talking about unnest of the closure since this is what's missing.

That's actually another question I had. There's no documentation about what unnest is for. From the laws I can guess that if the postcondition holds from f to g, then f.unnest(g). So it must be something that Coma needs, but I don't know what.