`fresh` doesn't imply inequality with `--general-traits=datatype`

[dschoepe]

Dafny version

4.6.0

Code to produce this issue

trait Clone {
  method clone() returns (res: Clone)
}

// using this version of `Clone` makes the verification pass:
// trait Clone extends object {
//   method clone() returns (res: Clone)
//     ensures fresh(res)
// }

class A extends Clone {
  method {:axiom} clone() returns (res: Clone)
    ensures res is A
    ensures fresh(res as A)
}

method client(aIn: A, bIn: A)
  requires aIn != bIn
{
  var a := aIn;
  var b := bIn;
  label L1:
  var clone := b.clone();
  assert fresh@L1(clone as A); // verifies
  b := clone as A;
  label L2:
  var clone2 := b.clone();
  assert fresh@L2(clone2 as A); // verifies
  a := clone2 as A;
  assert a != b; // doesn't verify
}

Command to run and resulting output

dafny verify --general-traits=datatype --type-system-refresh

What happened?

The above example verifies both when using the uncommented version of Clone and when running dafny verify --type-system-refresh without --general-traits=datatype. Since we know that clone is A and both clone as A objects are fresh, the example above should verify, also with --general-traits=datatype.

What type of operating system are you experiencing the problem on?

Linux, Mac

[stefan-aws]

I can confirm that --type-system-refresh has an effect on the verification result. What is your take on this @RustanLeino?

[keyboardDrummer]

If you change trait Clone { into trait Clone extends object { then it verifies. There's no need for ensures fresh(res) on the clone method in trait Clone

[dschoepe]

The problem with extends object is that it can then no longer be implemented by datatypes. We're using this to model Rust's Clone trait which is implemented by both value types and pointer types (e.g. Box), so we'd like to use the same Clone trait for both.

More broadly, I think I don't understand why the fresh assertions about clone as A don't also imply that the values are not equal. Are you sure this is intended to fail during verification?

[MikaelMayer]

One way you can encode the Clone method of Rust is to actually include the "Self" type as a type parameter for clone. Hence, the following verifies

trait Clone<T> {
  method clone() returns (res: T)
}

class A extends Clone<A> {
  method {:axiom} clone() returns (res: A)
    ensures fresh(res)
}

method client(aIn: A, bIn: A)
  requires aIn != bIn
{
  var a := aIn;
  var b := bIn;
  label L1:
  var clone := b.clone();
  assert fresh@L1(clone as A); // verifies
  b := clone as A;
  label L2:
  var clone2 := b.clone();
  assert fresh@L2(clone2 as A); // verifies
  a := clone2 as A;
  assert a != b; // doesn't verify
}