Surprising Verification Failures with Nested Datatypes + Classes

[whonore]

Dafny version

4.6.0

Code to produce this issue

class C {
  function Foo(): int { 0 }
}

class Box<T> {
  var inner: T
  constructor(t: T) { inner := t; }
}

datatype Wrap<T> = Wrap(inner: T)

class D {
  method Fail1(c: Box<Wrap<C>>)
    ensures c.inner.inner.Foo() == 0
  {}

  method Fail2(c: Wrap<Wrap<C>>)
    ensures c.inner.inner.Foo() == 0
  {}

  method Ok1(c: Box<Wrap<C>>)
    ensures c.inner.inner.Foo() == 0
  {
    assert c.inner.inner.Foo() == 0;
  }

  method Ok2(c: Box<Wrap<C>>)
    ensures c.inner.inner.Foo() == 0
  {
    assert (c.inner.inner as object) != this;
  }

  method Ok3(c: Box<C>)
    ensures c.inner.Foo() == 0
  {}

  method Ok4(c: Wrap<C>)
    ensures c.inner.Foo() == 0
  {}

  method Ok5(c: Wrap<Box<C>>)
    ensures c.inner.inner.Foo() == 0
  {}

  method Ok6(c: Box<Box<C>>)
    ensures c.inner.inner.Foo() == 0
  {}
}

Command to run and resulting output

$ dafny verify test.dfy

test.dfy(15,2): Error: a postcondition could not be proved on this return path
   |
15 |   {}
   |   ^

test.dfy(14,12): Related location: this is the postcondition that could not be proved
   |
14 |     ensures c.inner.inner.Foo() == 0
   |             ^^^^^^^^^^^^^^^^^^^^^^^^

test.dfy(19,2): Error: a postcondition could not be proved on this return path
   |
19 |   {}
   |   ^

test.dfy(18,12): Related location: this is the postcondition that could not be proved
   |
18 |     ensures c.inner.inner.Foo() == 0
   |             ^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 15 verified, 2 errors

What happened?

I'd expect all of the postconditions to verify without additional hints. I find it especially surprising that the assertion in Ok2 does anything useful.

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

Mac

[keyboardDrummer]

I agree, this is unexpected behavior.

[RustanLeino]

Thanks you for the many useful test cases! (Note from @keyboardDrummer: this is indeed a bug)

Workaround

As a workaround, adding any one of these three statements in the body of Fail1 makes the postcondition verify:

assert c.inner.inner.Foo() == 0;
assert c.inner.Wrap?;
var cc := c.inner.inner;

Notes on fixing the problem in the Dafny verifier

The problem is that the verifier needs the information that c.inner (in Fail1) has type Wrap<C> or, alternatively, that c.inner.Wrap? holds. This assumption is generated by the verifier, but the information is missing since the c.inner appears in a postcondition.

The information is generated into a free ensures postcondition for Impl$$_module.__default.Fail1 in Boogie. However, a free ensures in Boogie is ignored when checking an implementation. The Boogie attribute {:always_assume} that turns a free ensures into an assumption when verifying the implementation. The fix is to add that attribute (to all "assume conditions" generated by TrSplitExpr, both when those condition go into free ensures and when they go into free requires. This fix may have a large impact on other verifications.