Some thoughts on implementing Stacked Borrows as a borrow checker

In a last post I made a huge mistake of misinterpreting Stacked Borrows as a static borrow checker for unsafe code, even though it is in fact designed to be implemented dynamically. However, I decided to continue in the wrong direction and imagine what Stacked Borrows would look like if it were implemented as a borrow checker.

The concept pointer ID mostly correspond to Rust's lifetimes, but there is a tricky case where it doesn't. Changing that might cause incompatibility, but I believe that it makes sense and gets the logic clearer.

Currently, both of the functions works:

struct Data {
    field: u64,
}
fn deref<'a>(d: &'a mut Data) -> &'a mut Data {
    &mut d
}
fn inc<'a>(d: &'a mut Data) -> &'a mut Data {
    d.field += 1;
    &mut d
}

While the two function signatures are the same, they are subtly different. The first function does not alter or modify the Data at all, while the second function implicitly mutably borrows d.field and alters its value before returning the reference. Even though, in terms of lifetimes they are really the same, they have a different impact on the aliasing model: the first function deref guarantees that the lifetime of 'a is contiguous. The second function inc returns the same lifetime, but it's no longer the same alias; it has to be treated differently.

This means that the following code snippet:

let data = Data { field: 0 };
let ptr = &mut data;
ptr.field = 3;
let ptr2 = deref(ptr);
return ptr2.field

is able to assume that the return value will be 3, while the other:

let data = Data { field: 0 };
let ptr = &mut data;
ptr.field = 3;
let ptr2 = inc(ptr);
return ptr2.field;

can't.

Instead, the above function inc will need to be redeclared this way:

fn inc<'a, 'b>(d: &'a mut Data) -> &'b mut u64 where 'a: 'b {
    d.field += 1; // borrow 1
    &mut d.field // borrow 2
}

This makes it explicit that the input and the output are different variables. In fact, the lifetimes 'a and 'b are not exactly the same; 'a crosses the inc function while 'b can't, because the mark // borrow 1 and // borrow 2 are different mutable borrows and must not coincide with each other.

cc @RalfJung