Closed RustanLeino closed 1 year ago
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.
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. :)
This PR changes
Seq.Filter
's frame specification fromreads f.reads
toreads *
.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 ofSeq.Filter<T>(f: T ~> bool, xs: seq<T>)
, that desugaring wasSince
T
may depend on the allocation state, so does the set comprehension, and that is not allowed in a the declaration of functionFilter
.There are four ways to fix this problem.
f
fromf ~> bool
tof --> bool
(orf -> bool
). This restrictsf
to functions that don't read the heap, and hence thereads
clause ofFilter
can be removed altogether.T
to types that don't include heap references; that is, declareT
withT(!new)
. This will allow the previousreads
clause ofFilter
, but it also restricts the kinds of sequencesFilter
can be applied to.reads
clause ofFilter
toreads *
. This allowsFilter
to read anything in the allocated heap, but also weakens the power of the automatically generated frame axiom forFilter
.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 keeplibraries
verifying.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.