I have fixed this problem. However, the solution lies in a tricky region that intersects soundness, usefulness, and acceptable performance, so I made some compromises. In particular, Dafny now knows some additional properties of sets if the sets
are inparameters of methods.
More details:
The problem had to do with the underlying encoding. Dafny sets are represented in Boogie as sets of "boxes". That is, a set<T> in Dafny is essentially represented as a set<Box> in Boogie (I'm taking liberties with syntax). So,
the Dafny statement "S := S + {x};" is encoded in Boogie as:
S := S + { Box(x) };
and the Dafny expression "y in S" is encoded in Boogie as:
Box(y) in S
The postcondition in your example above uses Dafny's builtin subset operator, which gives rise to the encoding:
forall bx: Box :: bx in d2 ==> bx in d1 // (*)
In contrast, the quantifier you wrote yourself above is encoded as:
forall x: int :: Box(x) in d2 ==> Box(x) in d1 // (**)
When the prover tries to prove the postcondition (*) from the precondition (**), it assumes (**) and negates (*) and looks for a counterexample. The negation gives:
bx in d2 && !(bx in d1)
but this is not of the form that would make the verifier think of using (**). More precisely, this does not trigger any instantiation of (**). In my fix, I encoded things to get a property like:
bx in S ==> Box(Unbox(bx)) == bx
This causes the "x" in (**) to be instantiated with x := Unbox(bx), which then completes the argument.
The fix also addresses the issues in the related discussion thread you mention above (where you correctly had suspected that boxing was an issue).
Rustan
