Framing problem with recursive reads-clause

[jorge-jbs]

Dafny version

4.1.0

Code to produce this issue

trait ADT {
  ghost function ReprFamily(n: nat): set<object>
    decreases n
    ensures n > 0 ==> ReprFamily(n) >= ReprFamily(n-1)
    reads this, if n == 0 then {} else ReprFamily(n-1)
}

class P extends ADT {
  ghost function ReprFamily(n: nat): set<object>
    decreases n
    ensures n > 0 ==> ReprFamily(n) >= ReprFamily(n-1)
    reads this, if n == 0 then {} else ReprFamily(n-1)
}

Command to run and resulting output

Error: function might read an object not in the parent trait context's reads clause

What happened?

In versions prior to 3.13.0 this code was verified by Dafny, but since that version Dafny complains on the P class that implements the trait. It is not straightforward code but it should work. Each call to ReprFamily(n) reads ReprFamily(n-1), until ReprFamily(0) where it reads {}, so it is well-founded recursion. In fact, Dafny accepts the code of the trait, but not the code of the class that implements that trait with exactly the same specification.

I've noticed that in version 3.13.0 a pull request was accepted that changes the checking of traits: #3479. Maybe it has something to do with this problem.

What type of operating system are you experiencing the problem on?

Linux

[fabiomadge]

Thanks for the report. We did indeed slightly change the function encoding to strengthen the override check, but missed this while testing.