The value of a let-such-that expression must be uniquely determined

[henry-hz]

Thanks for merging the #14 @DavePearce
but we still have this error I couldn't fix.

dafny verify ./src/WrappedEtherModel.dfy                                                                                                                                                                                                      12:25:45
src/WrappedEtherModel.dfy(110,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined
    |
110 |             var pair :| pair in m;
    |             ^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 18 verified, 1 error

[DavePearce]

Hmmm, yeah that is in the model indeed.

[DavePearce]

So, this is strange. This code fails to compile:

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

Whilst on the other hand, this code does indeed compile:

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

Not sure what's going on here.

[DavePearce]

I've raised an issue for this now: dafny-lang/dafny#4564

[henry-hz]

@DavePearce , maybe this is just a feature of how functions should behave, considering the differences below, functions are transparent, so looping inside functions should be a non-transparent behaviour.

// * Functions:
//   - Purely mathematical constructs representing a mapping between input and output values.
//   - Bodies consist of a single expression that calculates and returns the output.
//   - No side effects (no modification of program state).
//   - Visible Implementation: The verifier can inspect the function's body and
//     use its definition during reasoning.
//   - Mathematical Reasoning: Treated as mathematical expressions, allowing symbolic
//     manipulation and equational reasoning.
//   - No State Change: Since functions are pure (no side effects), their behavior is predictable
//     and verifiable based on their definitions alone.
//   - Seamless Integration: Can be substituted directly into other expressions and assertions for reasoning.
//   - Verification Focus: The verifier concentrates on different aspects of methods and functions.
//   - Predictability: Transparent functions enable precise reasoning about their behavior due to their pure nature.
//
//
// * Methods:
//   - Executable code blocks performing actions and potentially modifying program state.
//   - Bodies can contain multiple statements, including assignments, loops,
//     conditionals, and calls to other methods.
//   - Hidden Implementation: The verifier does not examine the internal workings of a method's body.
//   - Trust in Specification: It relies solely on the method's declared pre and postconditions
//     to reason about its behavior.
//   - Reasoning About Effects: Ensures that calls to the method adhere to its specifications without
//     needing to know exact steps involved.
//   - Encapsulation: Fosters modularity and prevents reasoning about code details
//     that might change, simplifying verification.
//   - Modularity: Opaque methods promote modular reasoning and allow implementation changes
//     without affecting verification of other code that calls them.

So this is one case [I found this example] that make the function works:

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
    }
  }
}

Maybe the sum should be implemented only in terms of method instead of function ?

[DavePearce]

Hey @henry-hz,

So, Rustan has responded to this on stackoverflow (see comments). He said this:

The difference is that :| in a method is nondeterministic. That makes it easy to compile. A function has to be deterministic, so if you want to compile :|, the compiler has to ensure that you always get the same value back, which can be quite expensive to do at run time.

Its not clear to me whether he is going to offer an alternative mechanism for iterating sets.

Maybe the sum should be implemented only in terms of method instead of function ?

I understand why you are suggesting this, but it is not a good idea unfortunately. This because method vs function has quite different behaviours in Dafny. Essentially, the former cannot be used within an ensures clause (which is how we are using it now).

There are only a few suggestions I can think of:

1. We add an additional ghost field alongside balanceOf and allowance which has type seq<u160>. This then contains all addresses which are added into the balanceOf map and can be used to iterate in sum()
2. We implement our own version of set<T> which uses a seq<T> underneath and maintains the set invariant.

I guess another option might be to use seq<(u160,u256)> directly instead of set<(u160,u256)>. Not sure whether there is any reason this doesn't work?

[DavePearce]

I guess another option might be to use seq<(u160,u256)> directly instead of set<(u160,u256)>. Not sure whether there is any reason this doesn't work?

The problem here is that I don't see how you can convert from set<T> to seq<T>

[DavePearce]

Actually, in the case of sum you can resolve this by just making it a ghost function as follows:

ghost function sum(m:set<(nat,nat)>) : nat {
   ...

This works because its only used as a specification element. So that is fine!

I should add that, as a general solution, I don't really like it because I always want to be able to run my code. But for this particular case, it seems fine. I hope that the Dafny team provide an alternative in the future.

[henry-hz]

@DavePearce thanks for the solution and sharing the steps to reach it!