Counterexamples involving seqs should present elements ordered by index

[dijkstracula]

I'm working on debugging a particular counterexample involving a sequence (at least in theory - hence the debugging!) of contiguous intervals, like [(0, 4), (5, 9), (10, 20)]. In this case, figuring out where I'm going wrong really means needing to look at sequence elements in the order that they appear. This is the counterexample I'm given (extracted to the clipboard with this IDE patch):

At "{" (file:https:///Users/ntaylor/school/smrt/src/Disks/ZonedDisk.dfy:131):
...
    @1:seq<_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64>> = (Length := 6286, [0] := @3, [6285] := @4, [6283] := @5, [6284] := @6)
    @3:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 0, _1 := 2448)
    @4:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 281, _1 := 6135)
    @5:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 2480, _1 := 2481)
    @6:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 6133, _1 := 6134)

The particulars of the counterexample aren't of interest, save the indices that Boogie/Z3 generates for me in the sequence itself. Only after awhile did I notice that the sequence in the counterexample is actually out of order: @1's indices are 0, 6285, 6283, 6284 (Either it's a coincidence or Boogie is giving us the initial and final elements first?). I would have expected those indices to be in ascending order (i.e. 0, 6283, 6284, 6285) and would expect the intermediate subexpressions to be ordered similarly.

This patch modifies how the Dafny model expands element variables so that index-by-index sequence generation is sorted:

At "{" (file:https:///Users/ntaylor/school/smrt/src/Disks/ZonedDisk.dfy:131):
...
    @1:seq<_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64>> = (Length := 6286, [0] := @3, [6283] := @4, [6284] := @5, [6285] := @6)
    @3:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 0, _1 := 2448)
    @4:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 2480, _1 := 2481)
    @5:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 6133, _1 := 6134)
    @6:_System.Tuple2<NativeTypes.uint64, NativeTypes.uint64> = _#Make2(_0 := 281, _1 := 6135)

I'm not exactly sure of the current behaviour in the "build operator" case, and so I left that code branch unmodified.

(While I was in there, I found an incorrect docstring in an unrelated function related to passing null as an argument, and correspondingly fixed that.)

Fixes #

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Fantastic, yes, that seems like a good fix.
Can you add something for RELEASE_NOTES.md? See the instructions in the file.

[MikaelMayer]

Great, thanks for this feature !