Final borrow

[arnaudgolfouse]

Experiment to repair proofs when using a third field in mutable borrows.

In short, in the following code:

let mut x = 0i32;
let mut y = 0i32;
let ref_x_1 = &mut x;
let ref_x_2 = &mut *ref_x_1;
let ref_y_1 = &mut y;
let ref_y_2 = &mut *ref_y_1;

// ref_x_1 is never used here

let z = *ref_y_1;

Then:

• The third field of ref_x_1 and ref_x_2 should be the same, because ref_x_1 is "dead" after the reborrow (we say that this reborrow is final)
• This is not the case for ref_y_1, so the third field of ref_y_1 and ref_y_2 is not the same.

[arnaudgolfouse]

Some tests had their source (.rs) changed:

• iterators/02_iter_mut:

  • in completed: self.resolve() becomes (*self).inner@ == (^self).inner@
  • in produces, rather than comparing the two sequences directly, we need to compare each borrow by their current/final value.

• iterators/06_map_precond: remove let _ = self;

• take_first_mut: replace ^self == *self with (*^self_)@.len() == 0 && (^*self_)@.len() == 0

  We cannot prove ^self == *self, because we used std::mem::take, and the new borrow may not have the same id.

[jhjourdan]

Good !

First, CI is failing, which is indicating some of the sessions need to be updated. And indeed, it says that the iter_mut session is obsolete. Could you please update it?

in completed: self.resolve() becomes (*self).inner@ == (^self).inner@

This is suspicious. Why is this necessary? It should be equivalent, right?

iterators/06_map_precond: remove let _ = self;

I confirm that this is OK. This dates from the time where we had an assertion that we needed to prove the invariant. This assertion disappeared, so we can remove this hack.

That being being said, this is a real problem: we may need a way to reliably delay resolution without breaking final reborrows...

[xldenis]

That being being said, this is a real problem: we may need a way to reliably delay resolution without breaking final reborrows...

Let's not complicate an already complicated change with hypothetical edge-cases. The day when this becomes necessary we can revisit it.

[xldenis]

This is suspicious. Why is this necessary? It should be equivalent, right?

That's really weird, if this is breaking it also would indicate deeper issues to me. since ^self = *self should imply that.

[jhjourdan]

Let's not complicate an already complicated change with hypothetical edge-cases. The day when this becomes necessary we can revisit it.

Yes, of course! I was mentioning this simply because we may need to do something at some point.

[jhjourdan]

That's really weird, if this is breaking it also would indicate deeper issues to me. since ^self = *self should imply that.

Actually it does not imply this, because @arnaudgolfouse's version does not say anything about the inner tag. And I think @arnaudgolfouse is right: his change is necessary because of the change of the specification of take_first_mut.

That being said, (^self).inner@ == Seq::EMPTY would have been clearer (same remark for take_first_mut, BTW).

[arnaudgolfouse]

This should be good to go

[jhjourdan]

Could you please do a pass on each of my comments, check you have indeed handle them, and mark them as resolved? Thanks !