How to reason formally about programs using non lexical lifetimes

Question

Consider the following rust program:

fn main()
{
    let mut x = 1;
    let mut r = &x;
    r;
    let y = 1;
    r = &y;
    x = 2;
    r;
}

It compiles without any errors and I agree with that behaviour.

The problem is that I am not able to reach the same conclusion when trying to reason about this formally:

1. The type of the variable r is &'a i32 for some lifetime 'a.
2. The type of &x is &'b i32 for some lifetime 'b.
3. The lifetime 'a includes x = 2;.
4. From let mut r = &x; we know that 'b: 'a.
5. Because of 3 and 4 we know that the lifetime 'b includes x = 2;.
6. Because of 2 and 5 we are doing x = 2; while borrowing x, so the program should be invalid.

What is wrong with the formal reasoning above, and how would the correct reasoning be?

Answer 1

The lifetime 'a includes x = 2;.

Because of 3 and 4 we know that the lifetime 'b includes x = 2;.

They don't. r is reassigned to on line 7, this ends the entire thing as r is thereafter a completely new value independent from the old one -- and yes rustc is smart enough to work at that granularity, that's why if you remove the final x; it will warn that

value assigned to r is never read

at line 7 (whereas you would not get that warning with Go for instance, the compiler doesn't work at that low a granularity).

Rustc can thus infer that the smallest necessary length for 'b stops somewhere between the end of line 5 and the start of line 7.

Since x doesn't need to be updated before line 8, there is no conflict.

If you remove the assignment, however, 'b now has to extend to the last last line of the enclosing function, triggering a conflict.

Your reasoning seems to be that of lexical lifetimes, rather than NLL. You may want to go through the RFC 2094, it is very detailed. But in essence it works in terms of liveness constraints of values, and solving those constraints. In fact the RFC introduces liveness with an example which is a somewhat more complicated version of your situation:

let mut foo: T = ...;
let mut bar: T = ...;
let mut p: &'p T = &foo;
// `p` is live here: its value may be used on the next line.
if condition {
    // `p` is live here: its value will be used on the next line.
    print(*p);
    // `p` is DEAD here: its value will not be used.
    p = &bar;
    // `p` is live here: its value will be used later.
}
// `p` is live here: its value may be used on the next line.
print(*p);
// `p` is DEAD here: its value will not be used.

Also note this quote which very much applies to your misunderstanding:

The key point is that p becomes dead (not live) in the span before it is reassigned. This is true even though the variable p will be used again, because the value that is in p will not be used.

So you really need to reason off of values, not variables. Using SSA in your head probably helps there.

Applying this to your version:

let mut x = 1;
let mut r = &x;
// `r` is live here: its value will be used on the next line
r;
// `r` is DEAD here: its value will never be used
let y = 1;
r = &y;
// `r` is live here: its value will be used later
x = 2;
r;
// `r` is DEAD here: the scope ends