Mutable Reference Extensionality

[dewert99]

Currently mutable references are extensional (forall<x: &mut T, y: &mut T> *x == *y && ^x == ^y ==> x == y) I don't think many of the proofs should require this extensionality axiom. Would it be possible to try to remove the extensionality for mutable references (make Prelude.Borrow.borrowed an uninterpreted sort and ( * ) and ( ^ ) be uninterpreted functions)?

Logical reborrowing/unnesting could still use an uninterpreted constructor function that ensures that the current and final values of its result are correct.

[jhjourdan]

That's something we thought about but we were not sure that it was necessary.

Do you have some use case in mind?

[dewert99]

I am currently writing my thesis, which includes a translation from Prusti specifications to Creusot specifications. In order for the translation to preserve the intended semantics for the Prusti specifications the extensionality axiom would need to be removed. I'm curious what effect removing the axiom would have on Creusot, but from my understanding, I would guess it would not affect it too much.

Also as discussed in #869 removing the axiom could potentially also allow equality to soundly be used in ghost functions.

[jhjourdan]

We would like to investigate this quickly. The main issue is the new behaviour of logical reborrowing.

[dewert99]

For the purpose of my thesis the way logical reborrowing doesn't matter since my translation never produces specifications involving it.

For the purposes of ghost soundness, I would think the uninterpreted function used to implement logical reborrowing should in the full mutable reference as one of its parameters: eg.

// this would be an uninterpreted function defined in Why3
#[ensures(*result == curr)]
#[ensures(^result == fin)]
fn mk_mut<T, U>(base: &mut T, curr: U, fin: U) -> &mut U;

&mut x.f := mk_mut(x, (*x).f, (^x).f)

[jhjourdan]

The issue with this approach is that logical reborrowing is never guaranteed to coincide with program reborrowing.

I don't know whether this is an issue in practice, and I neither know whether we can lift this issue in some cases. We need to experiment/think a bit about that.

[voidc]

Some time ago, we experimented with changing the encoding of mutable borrows to not include the final value as a subterm and we came up with the following:

module Borrow
  (* The final field is encoded in the abstract type encoded_fin,
     so that the final component is not a subterm (hence we cannot
     do induction over it). *)
  type encoded_fin
  val function decode_fin (x : encoded_fin) : 'a
  val function encode_fin (x : 'a) : encoded_fin
    ensures { decode_fin result = x }

  type guarded_encoded_fin 'a =
    { inner : encoded_fin }
    invariant { encode_fin (decode_fin inner : 'a) = inner }

  type borrowed 'a = { current : 'a ; final : guarded_encoded_fin 'a; }
  let function ( *_ ) x = x.current
  let function ( ^_ ) (x : borrowed 'a) : 'a = decode_fin x.final.inner
  let function build_borrow (cur : 'a) (fin : 'a) : borrowed 'a =
    { current = cur; final = { inner = encode_fin fin } }
  val borrow_mut (a : 'a) : borrowed 'a
    ensures { *result = a }
end

I recall there were some issues with this encoding but I don't quite remember them. However, I think removing the final value as a subterm would also remove it from the extensionality axiom, thus solving at least the issues with unsound equalities in ghost code.

[xldenis]

@dewert99 do you also have an issue with extensionality between immutable borrows?

[shiatsumat]

Interesting point! I don't think we really need that extensionality. (That's the case for, e.g., the verification examples from the RustHorn paper.) Indeed, we can think of extended mutable borrow models with extra data (e.g., the address), which break the extensionality in question. The equality between model values doesn't mean anything special like the identity as an object.

[shiatsumat]

I like the idea of removing the extensionality. In general, I'm in favor of keeping value models to be "open-ended", i.e., leaving room for extra fields and precluding extensionality laws over a certain set of fields, because that allows for the extensibility of value models (adding low-level data, ghost state, etc.).

[dewert99]

@dewert99 do you also have an issue with extensionality between immutable borrows?

No, the Prusti semantics I'm using for shared references doesn't include the address. However, if Creusot did remove extensionality it wouldn't be an issue either, and the translation might even become valid for a version of Prusti whose semantics did include the address of shared references.

The Prusti semantics need to consider the address of mutable references since this is how changes need to be reflected back since Prusti has no concept of prophecies.

[xldenis]

To recap ongoing work @arnaudgolfouse is working on a way of implementing this.

The current idea is based on giving reborrows new "prophecy identifiers" each time, except when its the final reborrow of a place, in which case it re-uses the parent's identifier.

[jhjourdan]

Fixed by #912.