Unable to Iterate set in function

[DavePearce]

Dafny version

4.2.0

Code to produce this issue

function f(items: set<nat>) : (r:nat)
requires |items| > 0 {
    var item :| item in items;
    item
}

method m(items: set<nat>) returns (r:nat)
requires |items| > 0 {
    var item :| item in items;
    return item;
}

Command to run and resulting output

dafny build test.dfy
test.dfy(5,4): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
  |
5 |     var item :| item in items;
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^

What happened?

The term var item :| item in items compiles when in a method, but reports an error within a function. This seems inconsistent to me, and it previously worked in earlier versions of Dafny that supported function method syntax.

Furthermore, I don't know any other way to iterate a set<T> --- which would imply you can't currently iterate sets from within a function? That seems unexpected to me.

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

Linux

[henry-hz]

This bug still persists in the dafny 4.4.0+707b18acee078b3aa4d84c0590a980966bf22428
is there any special limitation for functions that is not present in methods ?
I found that this one below passes:

function f(s: set<int>) : (z:int)
  requires s != {}  {
  has_minimum(s);
  var z :| z in s && forall y :: y in s ==> z <= y;
  z
}

lemma has_minimum(s: set<int>)
  requires s != {}
  ensures exists z :: z in s && forall y :: y in s ==> z <= y {
  var z :| z in s;
  if s == {z} {
    // the mimimum of a singleton set is its only element
  } else if forall y :: y in s ==> z <= y {
    // we happened to pick the minimum of s
  } else {
    // s-{z} is a smaller, nonempty set and it has a minimum
    var s' := s - {z};
    has_minimum(s');
    var z' :| z' in s' && forall y :: y in s' ==> z' <= y;
    // the minimum of s' is the same as the miminum of s
    forall y | y in s
      ensures z' <= y {
      if
      case y in s' =>
        assert z' <= y;  // because z' in minimum in s'
      case y == z =>
        var k :| k in s && k < z;  // because z is not minimum in s
        assert k in s';  // because k != z
    }
  }
}

[keyboardDrummer]

The term var item :| item in items compiles when in a method, but reports an error within a function. This seems inconsistent to me, and it previously worked in earlier versions of Dafny that supported function method syntax.

The current behavior is intentional. Functions must be deterministic, so when using the :| operator, the element to select must be unique. This requirement has been in Dafny for a long time, and I do not believe that it changed with the syntactic change of function method becoming function.

@DavePearce I'm closing this, but please reopen it if you have a remaining question or believe something is incorrect.

[DavePearce]

I do not believe that it changed with the syntactic change

Well, the behaviour definitely did change because I was using it and it broke!!

In the end, this means that sets have a fairly limited utility. Still I can build my own using a seq<T> and keeping it e.g. in sorted order.

so when using the :| operator, the element to select must be unique

Well, in many cases, it is possible to select a unique element. For sets which contain ordered elements, you can select the least element, etc.

Anyways, if that is the intended behaviour then that is fine. I can work around it, as discussed with seq, when needed.

[keyboardDrummer]

Well, the behaviour definitely did change because I was using it and it broke!!

Ah, sorry I failed to see how it broke. If you change your function into ghost function, then it verifies again, because it no longer needs to be compilable. It's not a change in the behavior of :|, but what was previously function method is now function, and what was previously function is now ghost function.

What to me is a bit magical, is that even if you don't prove that :| finds a unique element, in a ghost context Dafny is still able to guarantee that. More information on that is in the section "determinism" in this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml252.pdf

Well, in many cases, it is possible to select a unique element. For sets which contain ordered elements, you can select the least element, etc.

Yes, if you use the :| operator to select the least element, then Dafny will accept it even if you use a function instead of a ghost function. However, I'm not sure how to do that outside of a ghost context. Let me ask around.

[robin-aws]

What to me is a bit magical, is that even if you don't prove that :| finds a unique element, in a ghost context Dafny is still able to guarantee that.

The key point is that in a ghost context, it's sound to just assume that a deterministic interpretation of a particular :| usage exists. So you don't have to constrain the :| range such that there's a unique solution. But it's compiled, there has to be a concrete interpretation that actually picks the same value on the same input every time, so you do have to constrain it further.

Yes, if you use the :| operator to select the least element, then Dafny will accept it even if you use a function instead of a ghost function. However, I'm not sure how to do that outside of a ghost context. Let me ask around.

@henry-hz's comment above is a good example: #4564 (comment). You have to constrain the RHS of the :| enough to make the answer unique, often by specifying that you require the smallest valid solution according to some ordering.

is there any special limitation for functions that is not present in methods ?

Yup, it's the fact that statements in a method (and methods in general) are allowed to be non-deterministic, so :| statements without a unique solution can be compiled. But functions have to be deterministic, so as above they have to be uniquely constrained.

I cut a documentation enhancement request to cover this more explicitly in the reference manual, since it's a frequent point of confusion: #5372 :)

[MikaelMayer]

But it's compiled, there has to be a concrete interpretation that actually picks the same value on the same input every time, so you do have to constrain it further.

I was confused by that until @RustanLeino made me realize that the same Dafny value could have different run-time representations. For example, {1, 2, 3} is the same as {3, 2, 1} but they could be stored in a different order, which makes it impossible to have var x :| s; always return the same value for the same value even if the code is deterministic.

[RustanLeino]

This Dafny Power User Note provides some explanation and guidance on iterating over collections.

[robin-aws]

More importantly https://dafny.org/dafny/DafnyRef/DafnyRef#555-iterating-over-collections has some of that content.

I cut #5372 because the core documentation really needs to address this more directly.

[DavePearce]

So, the comments above are helping! I wasn't aware that Dafny would actually try to establish that the selected element is unique. So, eventually, I managed to get this to compile / verify:

lemma ThereIsAMinimum(s: set<int>)
  requires s != {}
  ensures exists x :: x in s && forall y :: y in s ==> x <= y

function g(items: set<nat>) : (r:nat) 
requires |items| > 0 {
    ThereIsAMinimum(items);
    var item :| item in items && (forall k :: k in items ==> item <= k);
    item
}

That does actually solve the original problem we were having.

[MikaelMayer]

I looked into your "trivial" lemma and after curating the proof, I came up with this solution as well:

lemma ThereIsAMinimum(s: set<int>) returns (x: int)
  requires s != {}
  ensures x in s && forall y <- s :: x <= y
{
  x :| x in s;
  if forall y :: y in s ==> x <= y {
  } else {
    var notXButSmaller :| notXButSmaller in s && notXButSmaller < x;
    assert notXButSmaller in s - {x};
    var z := ThereIsAMinimum(s - {x});
    forall y <- s ensures z <= y {
      if y != x {
        assert y in s - {x};
      }
    }
    x := z;
  }
}

[DavePearce]

Haha, thanks @MikaelMayer !! I hadn't looked into that yet, but figured it could be done :)