Missing checks for refinement of !new and 00

[cpitclaudel]

Dafny accepts the following program:

abstract module Parent {
  type T(!new)

  twostate lemma L(new t: T)
    ensures old(allocated(t)) // Uses the !new annotation on T
  {}
}

module Child refines Parent {
  class T {
    var a: int
    constructor(a: int) ensures this.a == a { this.a := a; }
  }

  method boom() {
    var c := new T(0);
    assert !old(allocated(c));
    L(c);
    assert old(allocated(c));
    assert false;
  }
}

The problem is that the resolver does not check that !new annotations are preserved by refinement. (At first I thought it was a special case of #1419, but in fact it's a separate issue.)

[cpitclaudel]

The following is another example, this time with 00:

abstract module Parent {
  type U(00)

  lemma Mk() returns (u: U) {
    u :| true;
  }
}

module Child refines Parent {
  type False = x: int | false witness *

  // datatype U = U(f: False) // Correctly rejected

  class U { // Accepted
    var f: False
    constructor(f: False) { this.f := f; }
  }
}

method Main() ensures false {
  ghost var u: Child.U := Child.Mk();
  ghost var f: Child.False := u.f;
}