fix: Change reads clause of filter to *

[RustanLeino]

This PR changes Seq.Filter's frame specification from reads f.reads to reads *.

The reason for the change is that there are problems with using a function (here, the function f.reads) in a frame specification, because such a function desugars to, essentially, a big union and, depending on the parameters of the function, that big union may depend on the allocation state. In the case of Seq.Filter<T>(f: T ~> bool, xs: seq<T>), that desugaring was

set t: T, obj: object | obj in f.reads(t) :: obj

Since T may depend on the allocation state, so does the set comprehension, and that is not allowed in a the declaration of function Filter.

There are four ways to fix this problem.

• Change the type of f from f ~> bool to f --> bool (or f -> bool). This restricts f to functions that don't read the heap, and hence the reads clause of Filter can be removed altogether.
• Restrict the type parameter T to types that don't include heap references; that is, declare T with T(!new). This will allow the previous reads clause of Filter, but it also restricts the kinds of sequences Filter can be applied to.
• Change the reads clause of Filter to reads *. This allows Filter to read anything in the allocated heap, but also weakens the power of the automatically generated frame axiom for Filter.
• Declare more than one Filter function, each accommodating one of the possible fixes above.

This PR implements the third fix, reads *.

To date, Dafny erroneously didn't complain about the reads f.reads. That is currently being fixed, so this PR is needed to keep libraries verifying.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[robin-aws]

Great catch, and I think this option is the best tradeoff among the options you listed.

One thing to be careful about in the future: this looks like it would be a breaking change for code that specifically depended on the tighter reads clause. In this case since it's fixing a soundness issue and it's hard to imagine code that couldn't be quickly fixed if affected, I think it's reasonable, but otherwise we're relying on the fact that this codebase is still marked as subject to change, which we can't get away with forever.

In other words, the next time we hit this kind of issue we may need to pick your last option of forking code to avoid unbounded work for consumers to upgrade. :)

[atomb]

I agree with @robin-aws that this is the most pragmatic step to take at the moment. While we're at it, I notice that there are a few other instances of reads f.reads in the repository. Should we fix those, too?

[RustanLeino]

Thanks for the comments and quick reviews.

@atomb I took a look at the others (in Sets.dfy and ISets.dfy). Those instances are okay, because the element type is already declared as X(!new) (as required also by the quantifications in the preconditions of those functions). So, I think we can just leave those as they are.

I also looked at Map and MapWithResult in Seq.dfy (I hadn't looked at those before, because they didn't give errors with my new checking). Those are also okay, because they quantify over the sequence index. That made me realize that the reads f.reads I changed to reads * has yet another possible fix:

reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o

This is exact and has none of the drawbacks. (I should have thought of this obvious fix before.) I updated the PR to use this reads clause instead of the reads *.

While I was at it, I also removed many manual :trigger attributes from Seq.dfy, in the cases where auto-triggers would compute the same trigger. So, this change in Seq.dfy should not affect any verification.

[robin-aws]

Nice, even better!

So, this change in Seq.dfy should not affect any verification.

Another phrase that triggers (ha!) my worries about eventual backwards compatibility. I think we'll need a mechanism to verify your assertion in the future. :)

[atomb]

This looks very nice now. I like the reduction in {:trigger ...} annotations.