Set extensionality cannot be proved because type of local variables is not assumed.

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

method SetInclusionHavoc() {
  ghost var A0: set<(object?, int)> := *;
  ghost var A1: set<(object?, int)> := *;
  assume {:axiom} allocated(A0);
  assume {:axiom} allocated(A1);
  assume {:axiom} forall r: (object?, int) :: r in A0 ==> r in A1;
  assert A0 <= A1; // Failing
}
method SetEqualityHavoc() {
  ghost var A0: set<(object?, int)> := *;
  ghost var A1: set<(object?, int)> := *;
  assume {:axiom} allocated(A0);
  assume {:axiom} allocated(A1);
  assume {:axiom} forall r: (object?, int) :: r in A0 <==> r in A1;
  assert A0 == A1; // Failing
}

method Set() returns (s: set<(object?, int)>)
method SetInclusionMethod() {
  ghost var A0: set<(object?, int)> := Set();
  ghost var A1: set<(object?, int)> := Set();
  assume {:axiom} forall r: (object?, int) :: r in A0 ==> r in A1;
  assert A0 <= A1;
}
method SetEqualityMethod() {
  ghost var A0: set<(object?, int)> := Set();
  ghost var A1: set<(object?, int)> := Set();
  assume {:axiom} forall r: (object?, int) :: r in A0 <==> r in A1;
  assert A0 == A1;
}

Command to run and resulting output

dafny verify

What happened?

The first two methods fail.

It often comes up that, despite proving set membership constraints on sets, one has to strangely call a lemma to obtain extensionality of sets, set equality and set inclusion.
I nailed it down to one axiom missing on local variables that does not say what the type of local variables are, but does it for input and output parameters of methods.
This axiom for the example above is the following:

$Is(A0#0, TSet(Tclass._System.Tuple2(Tclass._System.object?(), TInt)))

However that axiom is present in the variable definition under the format:

  var A0#0: Set
     where defass#A0#0
       ==> $Is(A0#0, TSet(Tclass._System.Tuple2(Tclass._System.object?(), TInt)))
         && $IsAlloc(A0#0, TSet(Tclass._System.Tuple2(Tclass._System.object?(), TInt)), $Heap);

Despite that, at the point the axiom is needed, with the following:

havoc A1#0;
    defass#A1#0 := true;
    assert {:id "id0"} defass#A0#0;
    assert defass#A0#0
       ==> $Is(A0#0, TSet(Tclass._System.Tuple2(Tclass._System.object?(), TInt))); // Fails

So it looks like the where clause is either never checked, nor assumable in Boogie. We need to investigate it in Boogie as well.

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

Windows

[RustanLeino]

The problem seems to be that the Dafny-to-Boogie translation emits

    havoc A0#0;
    defass#A0#0 := true;

whereas it should emit

    defass#A0#0 := true;
    havoc A0#0;

The havoc command will assume the variable's where clause, but will do so for the value of defass#A0#0 at the time of the havoc. By assigning defass#A0#0 only after the havoc, the where clause doesn't have the intended effect.

[MikaelMayer]

Excellent remark.
Yes that work, as demonstrated on a minified boogie:

revealed function p(int) : bool;

procedure Test() returns ();

implementation Test() returns () {
  var da: bool;
  var a: int where da ==> p(a);
  da := false;
  havoc a;
  da := true;
  assert p(a);
}

does not verify, but if we exchange the havoc and da := true; statement, it verifies.

[MikaelMayer]

Unfortunately, this seems to not be the end of the story. Looking at this failing test case:

    var a: A := *;
    var b: B := *;

    if * {
      print a, "\n"; // error: A is a possibly empty type, so "a" is subject to definite assignment
    } else {
      print b, "\n"; // error: B is a possibly empty type, so "b" is subject to definite assignment
    }

there is an assignment and it assumes that a is now assigned along with all of its type characteristics (which might be empty).
I'm not sure how havoc assignment works with respect to definite initialization. Could you please elaborate @RustanLeino on what was the intent there?
In general, I remember this issue was there not just for havoc-ing, but for any kind of assignment involving an operation.