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