Incompleteness: const initialized from function with empty reads

[erniecohen]

The following fails to verify in 3.5.0.40314:

const p:()->bool
const c := p()
method test() {
    assert c == p(); // fails
}

[cpitclaudel]

Debugging notes: the defining axiom for c in Boogie is this:

axiom _module.__default.c()
   == $Unbox(Apply0(TBool, $OneHeap, _module.__default.p()));

Method test is translated to this:

implementation Impl$$_module.__default.test() returns ($_reverifyPost: bool)
{
  var $_Frame: <beta>[ref,Field beta]bool;

    // AddMethodImpl: test, Impl$$_module.__default.test
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
      $o != null && read($Heap, $o, alloc) ==> false);
    $_reverifyPost := false;
    // ----- assert statement ----- c:/Users/cpitcla/git/dafny/master/tmp2.dfy(4,5)
    assume true;
    assert _module.__default.c()
       == $Unbox(Apply0(TBool, $Heap, _module.__default.p())): bool;
}

Things verify if you add assume $HeapSucc($OneHeap, $Heap); before the assert.

BTW, the following also works; are there cases where the const containing a lambda is preferable?

function method p() : bool
const c := p()
method test() {
    assert c == p(); // fails
}

[erniecohen]

The problem came up inside an inductive datatype definition, where p was a field of the datatype. So it couldn't be declared as a function. I removed the context to present the underlying issue. In the datatype context, I worked around it by adding an explicit invariant that c==p().

As you indicate, there is a missing assumption that should be generated. It is very important to fix these sorts of deductive holes, not because they are hard to work around, but because it causes people to either waste time looking for bugs in other places.

In an ideal world, the verifier should have a relative completeness proof. Relative completeness here means not that there is some annotation that will get your code to prove, but that it can actually prove what it should be able to prove, with an appropriately defined customer-friendly notion of "should", and a perfect deductive engine. Doing this for a toy Dafny sounds like a good PhD project.