Invariant set may vary

Question

A method that copies the negative elements of an array of integers into another array has the property that the set of elements in the result is a subset of the elements in the original array, which stays the same during the copy.

The problem in the code below is that, as soon as we write something in the result array, Dafny somehow forgets that the original set is unchanged. How to fix this?

method copy_neg (a: array<int>, b: array<int>)
  requires a != null && b != null && a != b
  requires a.Length == b.Length
  modifies b
{
  var i := 0;
  var r := 0;
  ghost var sa := set j | 0 <= j < a.Length :: a[j];
  while i < a.Length
    invariant 0 <= r <= i <= a.Length
    invariant sa == set j | 0 <= j < a.Length :: a[j]
  {
    if a[i] < 0 {
      assert sa == set j | 0 <= j < a.Length :: a[j]; // OK
      b[r] := a[i];
      assert sa == set j | 0 <= j < a.Length :: a[j]; // KO!
      r := r + 1;
    }
    i := i + 1;
  }
}

Edit

Following James Wilcox's answer, replacing inclusions of sets with predicates on sequences is what works the best.

Here is the complete specification (for an array with distinct elements). The post-condition has to be detailed a bit in the loop invariant and a dumb assert remains in the middle of the loop, but all ghost variables are gone, which is great.

method copy_neg (a: array<int>, b: array<int>)
  returns (r: nat)
  requires a != null && b != null && a != b
  requires a.Length <= b.Length
  modifies b
  ensures 0 <= r <= a.Length
  ensures forall x | x in a[..] :: x < 0 <==> x in b[..r]
{
  r := 0;
  var i := 0;
  while i < a.Length
    invariant 0 <= r <= i <= a.Length
    invariant forall x | x in b[..r] :: x < 0
    invariant forall x | x in a[..i] && x < 0 :: x in b[..r]
  {
    if a[i] < 0 {
      b[r] := a[i];
      assert forall x | x in b[..r] :: x < 0;
      r := r + 1;
    }
    i := i + 1;
  }
}

Answer 1

This is indeed confusing. I will explain why Dafny has trouble proving this below, but first let me give a few ways to make it go through.

First workaround

One way to make the proof go through is to insert the following forall statement after the line b[r] := a[i];.

forall x | x in sa
  ensures x in set j | 0 <= j < a.Length :: a[j]
{
  var j :| 0 <= j < a.Length && x == old(a[j]);
  assert x == a[j];
}

The forall statement is a proof that sa <= set j | 0 <= j < a.Length :: a[j]. I will come back to why this works below.

Second workaround

In general, when reasoning about arrays in Dafny, it is best to use the a[..] syntax to convert the array to a mathematical sequence, and then work with that sequence. If you really need to work with the set of elements, you can use set x | x in a[..], and you will have a better time than if you use set j | 0 <= j < a.Length :: a[j].

Systematically replacing set j | 0 <= j < a.Length :: a[j] with set x | x in a[..] causes your program to verify.

Third solution

Popping up a level to specifying your method, it seems like you don't actually need to mention the set of all elements. Instead, you can get away with saying something like "every element of b is an element of a". Or, more formally forall x | x in b[..] :: x in a[..]. This is not quite a valid postcondition for your method, because your method may not fill out all of b. Since I'm not sure what your other constraints are, I'll leave that to you.

Explanations

Dafny's sets with elements of type A are translated to Boogie maps [A]Bool, where an element maps to true iff it is in the set. Comprehensions such as set j | 0 <= j < a.Length :: a[j] are translated to Boogie maps whose definition involves an existential quantifier. This particular comprehension translates to a map that maps x to

exists j | 0 <= j < a.Length :: x == read($Heap, a, IndexField(j))

where the read expression is the Boogie translation of a[j], which, in particular, makes the heap explicit.

So, to prove that an element is in the set defined by the comprehension, Z3 needs to prove an existential quantifier, which is hard. Z3 uses triggers to prove such quantifiers, and Dafny tells Z3 to use the trigger read($Heap, a, IndexField(j)) when trying to prove this quantifier. This turns out to not be a great trigger choice, because it mentions the current value of the heap. Thus, when the heap changes (ie, after updating b[r]), the trigger may not fire, and you get a failing proof.

Dafny lets you customize the trigger it uses for set comprehensions using a {:trigger} attribute. Unfortunately, there is no great choice of trigger at the Dafny level. However, a reasonable trigger for this program at the Boogie/Z3 level would be just IndexField(j) (though this is likely a bad trigger for such expressions in general, since it is overly general). Z3 itself will infer this trigger if Dafny doesn't tell it otherwise. You can Dafny to get out of the way by saying {:autotriggers false}, like this

invariant sa == set j {:autotriggers false} | 0 <= j < a.Length :: a[j]

This solution is unsatisfying and requires detailed knowledge of Dafny's internals. But now that we've understood it, we can also understand the other workarounds I proposed.

For the first workaround, the proof goes through because the forall statement mentions a[j], which is the trigger. This causes Z3 to successfully prove the existential.

For the second workaround, we have simplified the set comprehension expression so that it no longer introduces an existential quantifier. Instead the comprehension set x | x in a[..], is translated to a map that maps x to

x in a[..]

(ignoring details of how a[..] is translated). This means that Z3 never has to prove an existential, so the otherwise very similar proof goes through.

The third solution works for similar reasons, since it uses no comprehensions and thus no problematic existential quantifiers/