[yannickmoy]

and there are actually multiple ways to prove that the result is a permutation of the entry, either by computing a model multiset (a.k.a. bag) of the value on entry and exit and showing they are equal, or by exhibiting the permutation to apply to the entry value to get the exit value (typically by building this permutation as the algorithm swaps value, in ghost code), etc.

but none of this makes a good read for people not already familiar with program proof tools.