Missing (!new) check

[RustanLeino]

Dafny version

4.4.0

Code to produce this issue

function F<A(!new)>(): int

class Cell { }

lemma Lemma()
  ensures F<Cell>() < F<Cell>() + 1  // BUG: should complain that A must be (!new)
{
  // assert F<Cell>() < F<Cell>() + 1;
}

Command to run and resulting output

% dafny verify test.dfy

Dafny program verifier finished with 1 verified, 0 errors

What happened?

The type parameter of function F is declared as A(!new), which restricts it to types that do not contain references. Thus, the call F<Cell>() should be flagged as illegal, but it isn't.

Curiously, Dafny does flag the assertion, if uncommented, as illegal. So, it seems this check is just missing in the postcondition (or perhaps in specifications in general).

Here is another test example:

codatatype InfiniteTree<!A> = Node(value: int, next: A -> InfiniteTree)

greatest predicate Bisimilar<A(!new)>(t: InfiniteTree, u: InfiniteTree) {
  && t.value == u.value
  && forall a: A :: Bisimilar(t.next(a), u.next(a))
}

greatest lemma SelfSimilar<A>(t: InfiniteTree<A>)
  ensures Bisimilar<A>(t, t) // BUG: should complain that A must be (!new)
{
}

class Class { }

lemma SelfSimilarForClass(t: InfiniteTree<Class>)
  ensures Bisimilar<Class>(t, t) // BUG: should complain that A must be (!new)
{
  SelfSimilar<Class>(t);
}

lemma SelfSimilarForClassHash(o: ORDINAL, t: InfiniteTree<Class>)
  ensures Bisimilar#<Class>[o](t, t) // BUG: should complain that A must be (!new)
{
  SelfSimilar#<Class>[o](t);
}

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

Mac

[RustanLeino]

For the record, here's an example that (before the bug fix) gave a surprising verification:

predicate True<A>(a: A) {
  true
}

ghost predicate TypeIsEmpty<A(!new)>() {
  !exists a: A :: True(a)
}

class Cell { }

method Test() returns (c: Cell)
  requires TypeIsEmpty<Cell>()
  ensures TypeIsEmpty<Cell>()
{
  c := new Cell;
}

method False()
  requires TypeIsEmpty<Cell>()
  ensures false
{
  var c := Test();
  assert True(c);
}

Method False() is able to prove false as a postcondition, because TypeIsEmpty has an empty reads clause, yet it is affected by the new allocation. If it were possible to establish the precondition of False() from nothing (which it isn't, since Dafny never promises that there aren't any instances of a class that a program can create instances of), then one would be able to prove false from nothing.