[denotational]

The original code (which desugars to the snippet you posted) is:

    fn two_phase(mut x: Vec<usize>) {
        x.push(x.len());
    }

This should clearly be accepted (this is self evident in my opinion); if you need to jump through loops to write code like this then the language is too restrictive to write normal code.

The standard implementation of Rust does indeed accept this, and there is no soundness hole here.

The existing semantics for aliasing and borrowing from MPI (Stacked Borrows) don’t allow this, which means the semantics are overly restrictive; we want this to be accepted.

This work “fixes” this issue by extending the semantics to admit the behaviour exhibited by the standard implementation.

The rules for the borrow checker are not fully formalised and to some extent the rustc implementation is the specification; formalising the rules (i.e. RustBelt, Stacked Borrows, etc.) is important, but we don’t want to formalise something that is strictly more restrictive than the reference implementation, especially if there’s no soundness hole.