Create a proper notion of equality for Prusti

[vakaras]

We want a way to express that two objects have the same byte representation and use this notion for equality for pure functions (if a and b are equal, then f(a) and f(b) are equal for any pure function f).

[vakaras]

I am assigning myself to mark that this is the next thing I am going to work on once I am done with the compiler upgrade. However, since the upgrade is going to take some time, feel free to steal this issue.

[cmatheja]

Update: a == b implies f(a) == f(b) is supported for structs and tuples since 5295a58.
Enums are not supported yet.

[FabianWolff]

May I suggest that this enhanced notion of equality should also involve an extension of the old() operator? To illustrate the need for this, consider this example:

#[ensures(*x == old(*x))]
fn test (x: &mut i32) {}

This works, but

#[ensures(x == old(x))]

fails, even though they are equivalent from Rust's perspective (because "reference equality" is actually "deep equality" in Rust).

Now, this is obviously not a big issue for i32, but consider this:

#[ensures(t == old(t))]
fn test<T: PartialEq> (t: &mut T) {}

The postcondition is obviously true, because the function never even touches the reference, but rustc thinks that t is being moved out in old(t), and so this doesn't pass the borrow checker. Writing *t == old(*t) won't help here, either.

I apologize if this has been discussed before, but I couldn't find it during a quick look at the existing issues.

[cmatheja]

I agree that we eventually also want to support old in equalities involving ADTs; that's on the list besides a few other features that have not been implemented yet.

#[ensures(x == old(x))]

fails, even though they are equivalent from Rust's perspective (because "reference equality" is actually "deep equality" in Rust).

This is interesting as the "new equality" is only concerned with ADTs (structs, enums, tuples). I agree that we should fix this, but it should probably be moved into a separate issue.

[FabianWolff]

This is interesting as the "new equality" is only concerned with ADTs (structs, enums, tuples). I agree that we should fix this, but it should probably be moved into a separate issue.

Is it, though? What if a struct has a mutable reference as a field? You'll have to recursively check that for equality, too. Or do you mean by "ADT" that this is explicitly not supported?

[cmatheja]

Is it, though? What if a struct has a mutable reference as a field? You'll have to recursively check that for equality, too. Or do you mean by "ADT" that this is explicitly not supported?

At the moment, we explicitly check whether the outermost type is an ADT (or a tuple). If this is not the case, then the old notion of equality is applied. Once we detected that we are dealing with equality between ADTs, we indeed recursively check whether all fields are supported and also dereference fields accordingly.
There is, in principle, nothing that prevents us from doing the same if the outermost type is not an ADT.

[Aurel300]

The "notion of equality" now exists thanks to snapshots etc. We are planning to further extend it, by using snapshots for old. See also #403.