Fold/unfold error with snapshot equality

[zgrannan]

Triggered by the following:

use prusti_contracts::*;

#[derive(Clone, Copy)]
struct Inner(u32);

#[derive(Clone, Copy)]
struct Outer {
    inner: Inner,
}

#[ensures(out.inner === out.inner)]
fn go(out: Outer) {
}


fn main(){}

Yields:

error: [Prusti internal error] Prusti encountered an unexpected internal error
  --> min.rs:12:1
   |
12 | / fn go(out: Outer) {
13 | | }
   | |_^
   |
   = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
   = note: Details: cannot generate fold-unfold Viper statements. The required permission Pred(old[pre]((unfolding acc(Ref(struct$m_Outer)(_1), write) in _1.f$inner)), read) cannot be obtained.

Some observations:

• The nested struct seems to be part of the problem (changing inner to be just a u32 allows this to pass)
• Changing ensures to requires allows this to pass

I think this is likely related to the old() expression being introduced.

[Aurel300]

Does it work if you spell out the old, i.e. #[ensures(old(&out).inner === old(&out).inner)] (or any variant thereof)?

The === is syntax sugar for snapshot_equality(&out.inner, &out.inner) here, does a similar error happen with any pure function generic over two T arguments?

[zgrannan]

Does it work if you spell out the old, i.e. #[ensures(old(&out).inner === old(&out).inner)] (or any variant thereof)?

That works!

The === is syntax sugar for snapshot_equality(&out.inner, &out.inner) here, does a similar error happen with any pure function generic over two T arguments?

Yes, the same error occurs with the following:

use prusti_contracts::*;

#[derive(Clone, Copy)]
struct Outer<T> {
    inner: T,
}

#[ensures(out.inner === out.inner)]
fn go<T>(out: Outer<T>) {
}


fn main(){}

[Aurel300]

This is a duplicate of #797 then, I think.