Why can't I call a (non-static) lemma from a ghost field in Dafny?

Question

On Dafny, a lemma is implemented as a ghost method, thus, it is only useful for the specification.

However, you cannot call a lemma from a ghost field, like this:

class A {
    var i: int;
    lemma sum_is_commutative(i: int, j: int)
        ensures i + j == j + i
    {}
}
class B {
    ghost var a: A;
    lemma a_sum_is_commutative(i: int, j: int)
        ensures i + j == j + i
    { a.sum_is_commutative(i, j); }
    method test() {
        // a.sum_is_commutative(3, 2); // <- Cannot use directly this
        a_sum_is_commutative(3, 2);
    }
}

What is the rationale for this behavior? How can it be worked around? Is the best choice to just repeat the lemma in the inner class and leverage (usually, call) the other class's lemma?

Answer 1

Thanks for discovering and reporting this. It is a bug. I just pushed a fix for it.

Rustan

Answer 2

I'm not familiar with Dafny, but I think you need to declare your test method as ghost as well to be able to use the ghost parameter in it.

Usually in program verification frameworks, ghost means that the definition will be erased at runtime and is here only for proof purposes. Thus your test method should not contain code whose definition will be erased, or it should be marked as erasable (ghost).

Answer 3

I can't comment on the rationale for this behavior (and I will update the selected answer if there is an academic one, not just a bug or lack of implementation).

For working around this issue, it's semantically the same to define

class A {
  lemma sum_commutative(i: int, j: int) {}
}

as something like

class A {
  static lemma sum_commutative(a: A, i: int, j: int) {}
}

So, even if you need access to a this instance, you may be able to pass it as a parameter instead of relying on it implicitly.

Then, you are able to call from any other class your lemma as A.sum_commutative(a, i, j) without running into the issue of calling a ghost method of a ghost-variable from a non-ghost method.