FnMut closures with captured mutable slice

[ia0]

#[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 = [0; 10];
    let r = &mut x;
    #[invariant((*r)@.len() == 10)]
    #[invariant(forall<i: Int> 0 <= i && i < produced.len() ==> (*r)@[i]@ == i)]
    for i in 0 .. 10 {
        apply_mut({
            let r = &mut *r;
            #[cfg_attr(creusot, requires(i@ < (*r)@.len()))]
            #[cfg_attr(creusot, requires((*r)@.len() == 10))]
            #[cfg_attr(creusot, ensures((*r)@.len() == (*old(r))@.len()))]
            // #[cfg_attr(creusot, ensures(
            //     forall<k: Int> 0 <= k && k < i@ ==> (*r)@[k] == (*old(r))@[k]))]
            #[cfg_attr(creusot, ensures(
                forall<k: Int> 0 <= k && k < (*r)@.len() && k != i@ ==> (*r)@[k] == (*old(r))@[k]))]
            #[cfg_attr(creusot, ensures((*r)@[i@] == i))]
            #[cfg_attr(creusot, ensures((^r)@ == (^old(r))@))]
            move || r[i] = i
        });
        // This fails with the commented ensures above (which should be enough).
        proof_assert!(forall<k: Int> 0 <= k && k < i@ ==> (*r)@[k]@ == k);
        // This always fails.
        proof_assert!((*r)@[i@] == i);
    }
    proof_assert!(forall<i: Int> 0 <= i && i < 10 ==> x@[i]@ == i);
}

I have 2 questions:

1. Why do I need the ensures with 0 <= k < r.len() && k != i instead of 0 <= k < i which as far as I can tell should be enough to prove the loop invariant.
2. Why can't Why3 prove the second assert. It is literally the post condition.

For context, ultimately I want to prove a program that abstract over the loop:

fn apply_mut<F: FnMut(usize)>(n: usize, f: F) {
    (0..n).for_each(f)
}

[jhjourdan]

Both questions have the same answer: you should add #[ensures(i == old(i))] as an additional postcondition, or not use any specification (i.e., use closure specification inference).

The reason is that because of the move keyword, the variable i in the closure (and its specification) is really a different object than the variable i in the outer function.

[jhjourdan]

Nope, in this case we always have (**dst).len() == (^*dst).len().

[jhjourdan]

This has nothing to do with the mut keyword. The length of the slice a mutable borrow points to cannot change. Recall that the prophecy has been used to set the borrowed variable, which has fixed length.

[ia0]

Nope, in this case we always have (**dst).len() == (^*dst).len().

True, we have both (**dst).len() == (^*dst).len() and (*^dst).len() == (^^dst).len() because both of those simply go through the outer mutable reference, which is where the interesting mutability resides. If you look at dst (i.e. compare *dst and ^dst) instead of looking at *dst and ^dst independently, both the data pointer and the pointer metadata change. It's maybe simpler to see it without going through a function:

    let mut buffer = *b"hello";
    // buffer: Seq<u8> = *b"hello"
    let mut writer = &mut buffer[..];
    // writer: (Seq<u8>, Seq<u8>) = (*b"hello", *b"world")
    writer[.. 3].copy_from_slice(b"wor");
    // writer: (Seq<u8>, Seq<u8>) = (*b"worlo", *b"world")
    writer = &mut writer[3 ..];
    // writer: (Seq<u8>, Seq<u8>) = (*b"lo", *b"ld")
    writer[.. 2].copy_from_slice(b"ld");
    // writer: (Seq<u8>, Seq<u8>) = (*b"ld", *b"ld")
    writer = &mut writer[2 ..];
    // writer: (Seq<u8>, Seq<u8>) = ([], [])

It's true that at every program point we have (^writer)@.len() == (*writer)@.len(), however we don't have (*writer)@.len() == (*old(writer))@.len() between different program points, which is where the mutability of the place holding the mutable reference matters. And this is only because writer (or *dst) is a mutable place (including interior mutability).

Side note: each time we "forget" a part of the mutable reference (by updating the writer variable), we have (*writer)@ == (^writer)@ on the part that gets forgotten, similar to what we need if we would completely drop the mutable reference (to satisfy the prophecy).

[jhjourdan]

Then I don't understand what you mean. I simply said that (*x).len() == (^x).len() is a general law that applies whatever is x, but you said that the immutability of x is crucial for that...

[ia0]

Ah yes my bad. Yes that's true because x is by definition at a given program point on both sides of the equation. I got confused.

[jhjourdan]

In the end, the following works, and is much simpler than your code:

#[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 = [0; 10];
    let r = &mut x;
    let snap_r = snapshot! { r };
    #[invariant((*r)@.len() == 10)]
    #[invariant(forall<i: Int> 0 <= i && i < produced.len() ==> (*r)@[i]@ == i)]
    #[invariant(^r == ^*snap_r)]
    for i in 0 .. 10 {
        apply_mut(|| r[i] = i);
        proof_assert!(forall<k: Int> 0 <= k && k < i@ ==> (*r)@[k]@ == k);
        proof_assert!((*r)@[i@] == i);
    }
    proof_assert!(forall<i: Int> 0 <= i && i < 10 ==> x@[i]@ == i);
}