quantifiers over types that might be heap types

[Chris-Hawblitzel]

If C is a heap-related type (such as a class), then there are restrictions on expressions "forall x:C :: ..." to prohibit quantifying over objects x that aren't yet allocated. However, these restrictions aren't always enforced for type variables T that might later be instantiated with C. In the example below, the function AllP quantifies over all x of type T, even though T is later instantiated with C. Then AllP's frame axiom is used (in M3) to prove something that is not provable directly (as seen in M2). Rustan and I discussed this and tentatively proposed that the rules for quantifying over type variables T should be tightened, unless the programmer annotates T to indicate that T can never be instantiated with a heap-related type.

predicate P<T>(x:T)

predicate AllP<T>() { forall x :: P<T>(x) }

class C {}

method M1()

method M2()
{
  assume (forall x :: P<C>(x));
  M1();
  assert (forall x :: P<C>(x)); // FAILS (perhaps correctly)
}

method M3()
{
  assume (forall x :: P<C>(x));
  M1();
  assert AllP<C>();             // SUCCEEDS (perhaps incorrectly)
  assert (forall x :: P<C>(x)); // SUCCEEDS (perhaps incorrectly)
}

[robin-aws]

It looks like Dafny no longer allows quantifying over such possibly-heap types: trying this on the latest commit yields an error on the second line:

a quantifier involved in a predicate definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'x' (perhaps declare its type, 'T', as 'T(!new)')

Removing this line and the assert statement referencing it inside M3 does still allow the last assert to successfully verify, however.

[RustanLeino]

Here are some further, related test cases:

class Basic {
  var data: int
}

class Cell {
  const x: int
  var y: int
  constructor (x: int, y: int)
    decreases if x == y == 0 then 0 else 1
  {
    this.x, this.y := x, y;
    if !(x == y == 0) {
      var anotherCell := new Cell(0, 0);
    }
  }
}

method P0()
  requires forall c: Basic :: c.data == 8
{
  var o := new Basic;
  o.data := 8;
  assert forall c: Basic :: c.data == 8;  // fine
}

method P1()
  requires forall c: Basic :: c.data == 8
{
  var o := new Basic;
  assert forall c: Basic :: c.data == 8;  // BOGUS: this should not verify -- may not hold for o
}

method Q()
  requires forall c: Basic :: c.data == 8
{
  var o := new object;
  assert forall c: Basic :: c.data == 8;  // BOGUS: this ought not verify (well, it could, but only if o is known not to be a Basic)
}

method M0()
  requires forall c: Cell :: c.x == 8
{
  var o := new Cell(7, 8);
  assert forall c: Cell :: c.x == 8;  // BOGUS: this should not verify -- does not hold for o (or for anotherCell)
}

method M1()
  requires forall c: Cell :: c.x == 8
{
  var o := new Cell(8, 8);
  assert forall c: Cell :: c.x == 8;  // BOGUS: this should not verify -- does not hold for anotherCell
}

method N0()
  requires forall c: Cell :: c.y == 8
{
  var o := new Cell(8, 7);
  assert forall c: Cell :: c.y == 8;  // error: does not hold for o (or for anotherCell)
}

method N1()
  requires forall c: Cell :: c.y == 8
{
  var o := new Cell(8, 8);
  assert forall c: Cell :: c.y == 8;  // error: does not hold for anotherCell
}

[jtristan]

A note, mostly for myself: when we fix this, we need to make sure that the following still checks out:

method P1'()
  requires forall c: Basic :: c.data == 8
{
  var o := new Basic;
  assert forall c: Basic :: c != o ==> c.data == 8;  
}

[MikaelMayer]

I just had a look at the examples for quantifying, and I found a way to prove false, which summarizes well the challenge.

class Cell {
  const x: int
  constructor (x: int) ensures this.x == x {
    this.x := x;
  }
}

method M0()
  requires forall c: Cell :: c.x == 8
{
  var o := new Cell(7);
  assert false;
}

Looking at the generated boogie code, I see that the precondition is encoded as:

requires (forall c#1: ref :: 
    { _module.Cell.x(c#1) } 
    $Is(c#1, Tclass._module.Cell()) ==> _module.Cell.x(c#1) == LitInt(8));

This is wrong, because it does not depend on the heap at all.
The axiom should say that it's not true for all references, it's true for all the references that have already been allocated.

requires (forall c#1: ref  :: 
    { _module.Cell.x(c#1) } 
    $Is(c#1, Tclass._module.Cell()) && read($Heap, c#1, alloc) ==> _module.Cell.x(c#1) == LitInt(8));

Of @RustanLeino 's example, as of today, only P1, Q, M0, and M1 are problematic, the others are correctly handled.
However, fixing the axiom above would exactly fix P1, Q, M0 and M1.
And even if N0 and N1 could be proved, the fix above would still prevent them to verify.

[MikaelMayer]

One problem with the fix above is that, even if we replace 7 with 8, we still cannot prove anymore forall c: Cell :: c.x == 8 after the constructor. This is because we only know that what was allocated before is still allocated afterwards, but we don't know what new references were allocated in the heap.

Fortunately, we can fix that as usual by encoding it in the pre and post condition of the constructor (since, the constructor might allocate new references, it has to check locally that the predicate holds), but there is one caveat.)

class Cell {
  const x: int
  constructor (x: int)
    requires forall c: Cell :: c.x == 8
    decreases if x == 0 then 0 else 1
    ensures this.x == x
    ensures forall c: Cell :: c.x == 8 // Error, cannot prove this, unless we require x == 8 !
    {
      this.x := x;
      if !(x == 0) {
        var anotherCell := new Cell(0); // And if we require x =8, this fails. Yay!
      }
  }
}

method M0()
  requires forall c: Cell :: c.x == 8
{
  var o := new Cell(8);
  assert forall c: Cell :: c.x == 8;
}