feat: Array.qsort_sorted

[digama0]

This was a surprisingly challenging proof. It really highlights some of the pain involved in verifying programs which perform many array modifications without something isomorphic to separation logic, because one has to hold on to information about the rest of the array across many function calls that could potentially modify any part of the array.

I tried using invariants based on indexes, describing sorting in the form i < j -> as[i] <= as[j] with various restrictions on i,j in the algorithm, but this turned out to be quite painful (some remnant of this still remains in the definition of PermStabilizing). What worked better is lemmas like swap_of_append which just relate the array to a list expression like A ++ a :: B ++ b :: C where A.length = i and (A ++ a :: B).length = j, because this way the lists don't interfere with each other (there is only one A preserved before and after the operation), by comparison to array ops like set and swap which turn into if statements and arithmetic goals after every operation.

[nomeata]

Have you considered writing List.qsort, prove this correct, and then show how they are related? I found that that is often easier, at least when I verified a Trie data structure.

[digama0]

Yes, I did. My original goal was to verify the sorting functions in Std.Data.Array.Merge, and all of the functions have natural list counterparts except Array.qsort, which uses Array.swap, index-based manipulation, and fixed size arrays heavily.

[nomeata]

I see, in that case a list-based reference implementation probably won't help that much.

[somombo]

I'll leave this here for anyone interested; I have independently completed a specification and verification of Quicksort .. I basically just bruteforced through many of the types of issues highlighted above, so I could get an initial proof. I have been working on refactoring to improve the style and elaboration time.