Inconsistent printing of unordered collections across backends

[robin-aws]

This is one of those issues that most of us are fully aware of but have lived with for a long time without writing down (unless I just can't find the existing issue).

method Main() {
   print {"abc", "def"}, "\n";
}

% dafny run -t:java src/Scratch.dfy

Dafny program verifier finished with 0 verified, 0 errors
{['a', 'b', 'c'], ['d', 'e', 'f']}
% dafny run -t:cs src/Scratch.dfy

Dafny program verifier finished with 0 verified, 0 errors
{['d', 'e', 'f'], ['a', 'b', 'c']}

Not really a bug per se since the behavior of print is underspecified, but this makes consistent differential testing really annoying, whether testing a user program or the backends themselves.

My proposal for the most beneficial solution: implement the collections such as set, multiset and map in Dafny in the same way we now have a Dafny implementation of seq: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy. This would depend on having a common implementation of hash code functions for all Dafny types, instead of relying on target language runtime hash codes. We'd then have unpredictable but deterministic ordering for these collections. This is also worth doing in order to provide more efficient implementations of these immutable data types, rather than wrapping mutable versions from the target runtimes and making expensive defensive copies everywhere.

See also #2062.

[robin-aws]

Even worse, Python salts its hashes so its orderings are not even deterministic from one run to the next. This makes it effectively impossible to use %testDafnyForEachCompiler for such tests.

[MikaelMayer]

I understand it's an issue for printing, but as you present it, it looks like you are only concerned about tests for now.
For tests, I think it could be solved by doing the following. For every collection where we expect a result for print like this:

...
  print myset;

// expect file
{"abc", "def"}

1. Define a sequence of the expected result
2. Verify that each element of the expected sequence is in the collection (with appropriate value if it's a map
3. Verify that all keys of the sequence are different
4. Verify that the length of the sequence is equal to the length of the map.

...
  var expected := ["abc", "def"];
  for i <- 0 to |expected| {
    if expected[i] !in myset {
      print "bad";
    }
  }
  if |myset| != |expected| || |myset| != |set k <- expected| {
    print "bad"
  }

[robin-aws]

Indeed, I agree that would unblock the immediate testing pain, although not without additional complexity. I suggest the deeper change to implement these unordered collection types in Dafny code for the additional benefits (verified implementations, consistent performance across backends, etc.)

[robin-aws]

Even worse, Python salts its hashes so its orderings are not even deterministic from one run to the next. This makes it effectively impossible to use %testDafnyForEachCompiler for such tests.

Turns out we could use PYTHONHASHSEED=... to make this deterministic at least: https://docs.python.org/3/using/cmdline.html#envvar-PYTHONHASHSEED