feat: Optimize sort by Below
#1457
Conversation
|
Dafny Verifier crashed on |
| @@ -148,11 +148,89 @@ module SortCanon { | |||
| } | |||
| } | |||
|
|
|||
| predicate method Below(x: seq<uint8>, y: seq<uint8>) { | |||
| predicate Below(x: seq<uint8>, y: seq<uint8>) { | |||
There was a problem hiding this comment.
Forgive me, but I cannot figure out, based on the context available, what the contract of this method is.
What are the requirements for a seq<uint8> to be below another seq<uint8>?
If |x| == 0 and |y| != 0, is x below y?
x is certainly shorter.
But the sum of a thousand zeros is than one one.
So... in that case,
if y is a 1k zeros, and x is 1 one,
is x really below y?
I take it the heuristic is not summation,
but some other criteria.
But I cannot figure out what that criteria is.
There was a problem hiding this comment.
This is a kind of ordering.
assert Below([1,2,3], [1,2,4])
assert !Below([1,2,3], [1,2])
There was a problem hiding this comment.
So... is [1] below [0,0,0]?
There was a problem hiding this comment.
Or does it not matter, so long as the ordering is consistent?
There was a problem hiding this comment.
TBH, the ordering being consistent is key. I think that it would be assert Below([1], [0,0,0]).
This is like lex ordering since !(1 < 0)
The `Below` function is in the hot path. The slice (x[1..]) operation is not optimized in Dafny. This optimizes this function by turning the recursive slice into a loop over an index into the seq. Further, a bounded integer version is also included.
The `MergeSort` function is in the hot path. The slice (x[1..]) operation is not optimized in Dafny. This optimizes this function by turning the recursive slice into a loop over an index into the seq. Further, a bounded integer version is also included. It also limits the total amount of data copied.
seebees
force-pushed
the
seebees/optimize-below
branch
from
7dc718c
to
ea794cc
Compare
The
Belowfunction is in the hot path.The slice (x[1..]) operation is not optimized in Dafny. This optimizes this function by turning the recursive slice into a loop over an index into the seq.
Further, a bounded integer version is also included.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.