Matching pattern uses Unbox as outermost expression

[RustanLeino]

Dafny version

4.8.0

Code to produce this issue

trait Thing extends object {
  var owner: Thing
}

lemma TestProof(things: set<Thing>)
{
  assume forall o: Thing | o in things :: o.owner in things;
  assert forall o: Thing | o in things :: o.owner in things;
}

Command to run and resulting output

% dafny verify test.dfy --show-snippets=false
test.dfy(7,2): Warning: assume statement has no {:axiom} annotation
test.dfy(8,9): Error: assertion might not hold

Dafny program verifier finished with 0 verified, 1 error

What happened?

One expects a assert to verify given an immediately preceding assume of the same condition. The reason this doesn't happen here is that the matching pattern, o.owner, is translated into Boogie as

{ $Unbox(read($Heap, o#1, _module.Thing.owner)): ref }

The outermost $Unbox expression makes this matching pattern more restrictive than necessary or expected. If it instead is translated as just

{ read($Heap, o#1, _module.Thing.owner) } 

then the assert in the example goes through.

I think the fix is to always remove any outermost $Unbox in a matching-pattern term, be it an automatically computed matching pattern or a manually supplied matching pattern. (It's conceivable that we should also look for and remove any outermost $Box application, but I'm not sure if that can ever occur.)

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

Mac

[RustanLeino]

This error was discovered in https://github.com/dafny-lang/dafny/pull/5738/files#diff-7e6d69cbc2127f4be3b340c36691b46c5392f38907af95a5290da9fe715c9a78. The workaround there was to add this. to one place 06-ThreadOwnership.dfy. After fixing this bug, that this. workaround can be removed.

And why did adding this. work around the problem? Without it, Dafny's matching-pattern generation detects a possible cycle (o in content being triggered by o.owner in content, where content is a member of this). But by making the latter of these into o.owner in this.content, the matching-pattern generation doesn't realize the possible cycle, and therefore adds another matching pattern. This matching patterns lets the solver find the proof. So, a separate issue (which I have not reported separately) is that the matching-pattern generation ought to treat an implicit this. the same way as it treats an explicit .this. If that issue were fixed, then the workaround for 06-ThreadOwnership.dfy wouldn't work anymore, but fixing Issue 5751 will eliminate the need for that workaround in the first place.