Verifying Sorting Algorithms in Dafny

heapsort.dfy

module Heap
{

import opened Std.Relations

// Pointer arithmetics

function LeftChild(node: nat): nat { 2 * node + 1 }
function RightChild(node: nat): nat { 2 * (node + 1) }
function Parent(node: nat): nat requires node > 0 { (node - 1) / 2 }

// Tree structure

predicate InSubtree(root: nat, i: nat)
    decreases i - root
{
    root == i || (0 < i && root <= Parent(i) && InSubtree(root, Parent(i)))
}

lemma TransitiveSubtreeCase(x: nat, y: nat, z:nat)
    requires InSubtree(x, y) && InSubtree(y, z)
    ensures InSubtree(x, z)
    decreases z
{
    if y < z
    {
        TransitiveSubtreeCase(x, y, Parent(z));
    }
}

lemma InSubtreeIsTransitive()
    ensures Transitive(InSubtree)
{
    forall x, y, z | InSubtree(x, y) && InSubtree(y, z)
        ensures InSubtree(x, z)
    {
        TransitiveSubtreeCase(x, y, z);
    }
}

lemma SubtreeZero(i: nat)
    ensures InSubtree(0, i)
    decreases i
{
    if i > 0
    {
        SubtreeZero(Parent(i));
    }
}

lemma SubtreeCases(root: nat, i: nat)
    requires InSubtree(root, i)
    ensures root == i ||
            InSubtree(LeftChild(root), i) ||
            InSubtree(RightChild(root), i)
    decreases i
{
    if i > RightChild(root)
    {
        SubtreeCases(root, Parent(i));
    }
}

// Heap invariants

predicate UpInvariant<T(!new)>(h: seq, node: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= node < |h|
{
    node > 0 ==> lessEq(h[Parent(node)], h[node])
}

predicate DownInvariant<T(!new)>(h: seq, node: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= node < |h|
{
    (LeftChild(node) < |h| ==> lessEq(h[node], h[LeftChild(node)])) &&
    (RightChild(node) < |h| ==> lessEq(h[node], h[RightChild(node)]))
}

predicate IsSubHeap<T(!new)>(h: seq, root: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
{
    forall i :: root < i < |h| && InSubtree(root, i) ==> UpInvariant(h, i, lessEq)
}

lemma SubHeapIsRecursive<T(!new)>(h: seq, root: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
    requires IsSubHeap(h, root, lessEq)
    ensures forall i :: 0 <= i < |h| && InSubtree(root, i) ==> IsSubHeap(h, i, lessEq)
{
    InSubtreeIsTransitive();
}

lemma RootLessEq<T(!new)>(h: seq, root: nat, i: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
    requires IsSubHeap(h, root, lessEq)
    requires 0 <= i < |h|
    requires InSubtree(root, i)
    ensures lessEq(h[root], h[i])
    decreases i
{
    if i > root
    {
        RootLessEq(h, root, Parent(i), lessEq);
    }
}

lemma RootIsMin<T(!new)>(h: seq, root: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
    requires IsSubHeap(h, root, lessEq)
    ensures forall i :: 0 <= i < |h| && InSubtree(root, i) ==> lessEq(h[root], h[i])
{
    forall i | 0 <= i < |h| && InSubtree(root, i)
    {
        RootLessEq(h, root, i, lessEq);
    }
}

// A semiheap is almost a subheap, except that the root may violate
// the heap invariant.
ghost predicate IsSemiHeap<T(!new)>(h: seq, root: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
{
    (LeftChild(root) < |h| ==> IsSubHeap(h, LeftChild(root), lessEq)) &&
    (RightChild(root) < |h| ==> IsSubHeap(h, RightChild(root), lessEq))
}

lemma SubHeapImpliesSemiHeap<T(!new)>(h: seq, root: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
    requires IsSubHeap(h, root, lessEq)
    ensures IsSemiHeap(h, root, lessEq)
{
    SubHeapIsRecursive(h, root, lessEq);
}

lemma SemiHeapAndDownInvariantImpliesSubHeap<T(!new)>(h: seq, root: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= root < |h|
    requires IsSemiHeap(h, root, lessEq)
    requires DownInvariant(h, root, lessEq)
    ensures IsSubHeap(h, root, lessEq)
{
    forall i | root < i < |h| && InSubtree(root, i)
        ensures UpInvariant(h, i, lessEq)
    {
        SubtreeCases(root, i);
    }
}

// Need this lemma to prove the following:
// When updating a subheap, the elements in the subheap are shuffled, and
// we want to make sure that any property about the values of those elements
// (e.g., has a lower bound) in the subheap stays unchanged.
// a and b are two heaps, and unchangedIndicies has the indicies outside
// of the mutation.
lemma PartialShufflePreserves<T>(a: seq, b: seq, unchangedIndicies: set<nat>, P: (T) -> bool)
    requires |a| == |b|
    requires multiset(a) == multiset(b)
    requires forall i :: 0 <= i < |a| && i in unchangedIndicies ==> a[i] == b[i]
    requires forall i :: 0 <= i < |a| && i !in unchangedIndicies ==> P(a[i])
    ensures forall i :: 0 <= i < |b| && i !in unchangedIndicies ==> P(b[i])
{
    // t == shuffled, f == not shuffled
    var at := multiset{};
    var bt := multiset{};
    var af := multiset{};
    var bf := multiset{};
    for i := 0 to |a|
        invariant at + af == multiset(a[..i])
        invariant bt + bf == multiset(b[..i])
        invariant af == bf
        invariant forall j :: 0 <= j < i && j !in unchangedIndicies ==> b[j] in bt
        invariant forall x :: x in at ==> P(x)
    {
        assert a[..i] + [a[i]] == a[..i+1];
        assert b[..i] + [b[i]] == b[..i+1];
        if i !in unchangedIndicies
        {
            at := at + multiset{a[i]};
            bt := bt + multiset{b[i]};
        }
        else
        {
            af := af + multiset{a[i]};
            bf := bf + multiset{b[i]};
        }
    }
    assert a == a[..|a|];
    assert b == b[..|b|];
    calc ==
    {
        at;
        multiset(a) - af;
        multiset(b) - bf;
        bt;
    }
    forall i | 0 <= i < |b| && i !in unchangedIndicies
        ensures P(b[i])
    {
        assert b[i] in at;
        assert at <= multiset(a);
        var j :| 0 <= j < |a| && a[j] == b[i];
    }
}

// Special case to above: all elements might have been shuffled.
lemma ShufflePreserves<T>(a: seq, b: seq, P: T -> bool)
    requires |a| == |b|
    requires multiset(a) == multiset(b)
    requires forall i :: 0 <= i < |a| ==> P(a[i])
    ensures forall i :: 0 <= i < |b| ==> P(b[i])
{
    PartialShufflePreserves(a, b, {}, P);
}

method SiftDown<T(!new)>(h: array, len: nat, node: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 <= node < len <= h.Length
    requires IsSemiHeap(h[..len], node, lessEq)
    modifies h
    ensures forall i :: 0 <= i < len && !InSubtree(node, i) ==> h[i] == old(h[i])
    ensures multiset(h[..len]) == old(multiset(h[..len]))
    ensures h[len..] == old(h[len..])
    ensures IsSubHeap(h[..len], node, lessEq)
    decreases len - node
{
    var min := node;
    var l := LeftChild(node);
    if l < len && !lessEq(h[min], h[l])
    {
        min := l;
    }
    var r := RightChild(node);
    if r < len && !lessEq(h[min], h[r])
    {
        min := r;
    }
    if min != node
    {
        SubHeapImpliesSemiHeap(h[..len], min, lessEq);
        RootIsMin(h[..len], min, lessEq);

        h[min], h[node] := h[node], h[min];

        // h[node] is now the previous root at h[min], thus <= all nodes in the subtree.
        ghost var h' := h[..len];
        ghost var nodeVal := h[node];
        SiftDown(h, len, min, lessEq);
        // All nodes in subtree at h[min] are >= nodeVal; this fact doesn't
        // change during SiftDown, because it only shuffles values in the
        // subtree.
        assert DownInvariant(h[..len], node, lessEq) by
        {
            ghost var unchangedIndicies := set i: nat | 0 <= i < len && !InSubtree(min, i);
            PartialShufflePreserves(h', h[..len], unchangedIndicies, (x) => lessEq(nodeVal, x));
        }
        // Only h[node], and the subtree at h[min] changed.
        // therefore outside the subtree at h[node], nothing changed.
        InSubtreeIsTransitive();
    }
    SemiHeapAndDownInvariantImpliesSubHeap(h[..len], node, lessEq);
}

method DeleteMin<T(!new)>(h: array, len: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 < len <= h.Length
    requires IsSubHeap(h[..len], 0, lessEq)
    modifies h
    ensures multiset(h[..len]) == old(multiset(h[..len]))
    ensures h[len..] == old(h[len..])
    ensures h[len-1] == old(h[0])
    ensures var h' := h[..len-1]; |h'| == 0 || IsSubHeap(h', 0, lessEq)
{
    // Nothing to do if len == 1; heap becomes empty.
    if len > 1
    {
        SubHeapImpliesSemiHeap(h[..len-1], 0, lessEq);
        h[0], h[len-1] := h[len-1], h[0];
        SiftDown(h, len-1, 0, lessEq);
    }
}

method Init<T(!new)>(h: array, len: nat, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    requires 0 < len <= h.Length
    modifies h
    ensures IsSubHeap(h[..len], 0, lessEq)
    ensures multiset(h[..len]) == old(multiset(h[..len]))
    ensures h[len..] == old(h[len..])
{
    if len <= 1
    {
        // Nothing to do.
        return;
    }
    var i := Parent(len - 1);
    while i > 0
        invariant 0 <= i < len
        invariant multiset(h[..len]) == old(multiset(h[..len]))
        invariant h[len..] == old(h[len..])
        invariant forall j :: RightChild(i) < j < len ==> UpInvariant(h[..len], j, lessEq)
    {
        ghost var l := LeftChild(i);
        ghost var r := RightChild(i);

        ghost var h' := h[..];
        SiftDown(h, len, i, lessEq);
        forall j | l <= j < len
            ensures UpInvariant(h[..len], j, lessEq)
        {
            if !InSubtree(i, j)
            {
                // Outside the subtree everything is unchanged.
                assert j > r;
                assert h[j] == h'[j];
                assert h[Parent(j)] == h'[Parent(j)];
                assert UpInvariant(h'[..len], j, lessEq);
            }
        }
        // So the last loop invariant works.
        assert RightChild(i-1) + 1 == l;
        i := i - 1;
    }
    SiftDown(h, len, i, lessEq);
}

method Sort<T(!new)>(h:array, lessEq: (T, T) -> bool)
    requires TotalOrdering(lessEq)
    modifies h
    ensures SortedBy(lessEq, h[..])
    ensures multiset(h[..]) == old(multiset(h[..]))
{
    if h.Length <= 1
    {
        // Nothing to do.
        return;
    }
    var greaterEq := (x, y) => lessEq(y, x);

    assert h[..] == h[..h.Length];
    Init(h, h.Length, greaterEq);
    assert h[..] == h[..h.Length];

    var len := h.Length;
    while len > 0
        invariant 0 <= len <= h.Length
        invariant len > 0 ==> IsSubHeap(h[..len], 0, greaterEq)
        invariant len < h.Length ==> SortedBy(lessEq, h[len..])
        //invariant 0 < len < h.Length ==> greaterEq(h[len], h[0])
        invariant forall i :: len <= i < h.Length ==> greaterEq(h[i], h[0])
        invariant multiset(h[..]) == old(multiset(h[..]))
    {
        ghost var rootVal := h[0];
        RootIsMin(h[..len], 0, greaterEq);
        forall i | 0 <= i < len
            ensures greaterEq(rootVal, h[i])
        {
            SubtreeZero(i);
        }
        ghost var h' := h[..];
        DeleteMin(h, len, greaterEq);
        calc ==
        {
            multiset(h[..]);
            { assert h[..] == h[..len] + h[len..]; }
            multiset(h[..len]) + multiset(h[len..]);
            multiset(h'[..len]) + multiset(h'[len..]);
            { assert h'[..] == h'[..len] + h'[len..]; }
            multiset(h'[..]);
        }
        ShufflePreserves(h'[..len], h[..len], (x) => greaterEq(rootVal, x));
        assert forall i :: len <= i < h.Length ==> greaterEq(h[i], h[len]);
        len := len - 1;
    }
}

}

merge-sort.dfy

ghost predicate Sorted(a: seq<int>)
{
    forall i, j :: 0 <= i <= j < |a| ==> a[i] <= a[j]
}

method MergeInPlace(a: array<int>, aBegin: nat, aEnd: nat,
                    b: array<int>, bBegin: nat, bEnd: nat,
                    r: array<int>)
    requires a != r && b != r
    requires 0 <= aBegin <= aEnd <= a.Length
    requires 0 <= bBegin <= bEnd <= b.Length
    requires Sorted(a[aBegin..aEnd])
    requires Sorted(b[bBegin..bEnd])
    requires (aEnd - aBegin) + (bEnd - bBegin) <= r.Length
    modifies r
    ensures multiset(a[aBegin..aEnd]) + multiset(b[bBegin..bEnd])
            == multiset(r[..(aEnd-aBegin)+(bEnd-bBegin)])
    ensures Sorted(r[..(aEnd-aBegin)+(bEnd-bBegin)])
{
    var n := (aEnd - aBegin) + (bEnd - bBegin);
    var i := aBegin;
    var j := bBegin;
    var k := 0;

    while k < n
        invariant aBegin <= i <= aEnd
        invariant bBegin <= j <= bEnd
        invariant (i - aBegin) + (j - bBegin) == k
        invariant multiset(a[aBegin..i]) + multiset(b[bBegin..j]) == multiset(r[..k])
        invariant forall u, v :: 0 <= u < k && i <= v < aEnd ==> r[u] <= a[v]
        invariant forall u, v :: 0 <= u < k && j <= v < bEnd ==> r[u] <= b[v]
        invariant Sorted(r[..k])
    {
        if i == aEnd || (j < bEnd && b[j] < a[i]) {
            r[k] := b[j];
            j := j + 1;
        } else {
            r[k] := a[i];
            i := i + 1;
        }
        assert forall l :: 0 <= l < k ==> r[k] >= r[l];
        k := k + 1;
    }
    assert a[aBegin..i] == a[aBegin..aEnd];
    assert b[bBegin..j] == b[bBegin..bEnd];
}

method CopyBack(a:array<int>, begin: nat, end: nat, tmp:array<int>)
    requires a != tmp
    requires 0 <= begin <= end <= a.Length
    requires end - begin <= tmp.Length
    modifies a
    ensures a[begin..end] == tmp[..end-begin]
    // Only modifies a[begin..end]
    ensures forall i, j :: 0 <= i <= j <= begin ==> a[i..j] == old(a[i..j])
    ensures forall i, j :: end <= i <= j <= a.Length ==> a[i..j] == old(a[i..j])
{
    forall i | begin <= i < end
    {
        a[i] := tmp[i - begin];
    }
}

method MergeSortAux(a: array<int>, begin: nat, end: nat, tmp: array<int>)
    requires a != tmp
    requires 0 <= begin <= end <= a.Length
    requires end - begin <= tmp.Length
    modifies a
    modifies tmp
    decreases end - begin
    ensures Sorted(a[begin..end])
    ensures multiset(a[begin..end]) == old(multiset(a[begin..end]))
    // Only modifies a[begin..end]
    ensures forall i, j :: 0 <= i <= j <= begin ==> a[i..j] == old(a[i..j])
    ensures forall i, j :: end <= i <= j <= a.Length ==> a[i..j] == old(a[i..j])
{
    var n := end - begin;
    if n < 2 {
        return;
    }
    var mid := begin + n / 2;
    assert begin < mid < end;
    MergeSortAux(a, begin, mid, tmp);
    MergeSortAux(a, mid, end, tmp);
    MergeInPlace(a, begin, mid, a, mid, end, tmp);
    CopyBack(a, begin, end, tmp);
    calc == {
        multiset(a[begin..end]);
        old(multiset(a[begin..mid])) + old(multiset(a[mid..end]));
        old(multiset(a[begin..mid] + a[mid..end]));
        { assert old(a[begin..mid] + a[mid..end]) == old(a[begin..end]); }
        old(multiset(a[begin..end]));
    }
}

method MergeSort(a: array<int>)
    modifies a
    ensures Sorted(a[..])
    ensures multiset(a[..]) == old(multiset(a[..]))
{
    var tmp := new int[a.Length];
    assert a[..] == a[0..a.Length];
    MergeSortAux(a, 0, a.Length, tmp);
    assert a[..] == a[0..a.Length];
}

naive-sort.dfy

ghost predicate Sorted(a: seq<int>)
{
    forall i, j :: 0 <= i <= j < |a| ==> a[i] <= a[j]
}

method BubbleSort(a: array<int>)
    modifies a
    ensures Sorted(a[..])
    ensures multiset(a[..]) == old(multiset(a[..]))
{
    var i := 0;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant multiset(a[..]) == old(multiset(a[..]))
        invariant forall k, l :: 0 <= k < i <= l < a.Length ==> a[k] <= a[l]
        invariant Sorted(a[..i])
    {
        var j := a.Length - 1;
        while j > i
            invariant i <= j <= a.Length
            invariant multiset(a[..]) == old(multiset(a[..]))
            invariant Sorted(a[..i])
            invariant forall k :: j < k < a.Length ==> a[j] <= a[k]
            invariant forall k, l :: 0 <= k < i <= l < a.Length ==> a[k] <= a[l]
        {
            if a[j-1] > a[j]
            {
                a[j-1], a[j] := a[j], a[j-1];
            }
            j := j - 1;
        }
        i := i + 1;
    }
}

method SelectionSort(a: array<int>)
    modifies a
    ensures Sorted(a[..])
    ensures multiset(a[..]) == old(multiset(a[..]))
{
    var i := 0;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant multiset(a[..]) == old(multiset(a[..]))
        invariant Sorted(a[..i])
        invariant forall k, l :: 0 <= k < i <= l < a.Length ==> a[k] <= a[l]
    {
        var m := i;
        var j := i + 1;
        while j < a.Length
            invariant i < j <= a.Length
            invariant i <= m < a.Length
            invariant forall k :: i <= k < j ==> a[m] <= a[k]
        {
            if a[m] > a[j] {
                m := j;
            }
            j := j + 1;
        }
        a[i], a[m] := a[m], a[i];
        i := i + 1;
    }
}

method InsertionSort(a: array<int>)
    modifies a
    ensures Sorted(a[..])
    ensures multiset(a[..]) == old(multiset(a[..]))
{
    var i := 0;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant multiset(a[..]) == old(multiset(a[..]))
        invariant Sorted(a[..i])
    {
        var j := i;
        var tmp := a[i];
        ghost var a' := a[..];
        while j > 0 && a[j-1] > tmp
            invariant 0 <= j <= i < a.Length
            invariant forall k :: j < k <= i ==> a[k] >= tmp
            invariant multiset(a[..]) - multiset{a[j]} + multiset{tmp} == multiset(a'[..])
            invariant a[..j] == a'[..j]
            invariant a[j+1..i+1] == a'[j..i]
        {
            a[j] := a[j-1];
            j := j - 1;
        }
        a[j] := tmp;
        assert Sorted(a[..j]);
        i := i + 1;
    }
}

quicksort.dfy

ghost predicate Sorted(a: seq<int>)
{
    forall i, j :: 0 <= i <= j < |a| ==> a[i] <= a[j]
}

method Partition(a: array<int>, l: nat, r: nat) returns (i: nat)
    requires 0 <= l < r <= a.Length
    modifies a
    ensures l <= i < r
    // Partition property
    ensures forall k :: l <= k <= i ==> a[k] <= old(a[l])
    ensures forall k :: i <= k < r ==> a[k] >= old(a[l])
    // Only order is changed in a[l..r]
    ensures multiset(a[l..r]) == old(multiset(a[l..r]))
    // No change outside of a[l..r]
    ensures a[..l] == old(a[..l])
    ensures a[r..] == old(a[r..])
{
    var pivot := a[l];
    i := l;
    var j := r - 1;
    ghost var allMinusPivot := multiset(a[l..r]) - multiset{pivot};
    while true
        invariant l <= i <= j < r
        invariant forall k :: l <= k < i ==> a[k] <= pivot
        invariant forall k :: j < k < r ==> a[k] >= pivot
        invariant multiset(a[l..r]) - multiset{a[i]} == allMinusPivot
        decreases j - i
    {
        while i < j && a[j] >= pivot
            invariant i <= j
            invariant forall k :: j < k < r ==> a[k] >= pivot
        {
            j := j - 1;
        }
        if i == j { break; }
        a[i] := a[j];
        assert multiset(a[l..r]) - multiset{a[j]} == allMinusPivot;

        while i < j && a[i] <= pivot
            invariant i <= j
            invariant forall k :: l <= k < i ==> a[k] <= pivot
        {
            i := i + 1;
        }
        if i == j { break; }
        a[j] := a[i];
        assert multiset(a[l..r]) - multiset{a[i]} == allMinusPivot;
    }
    a[i] := pivot;
}

lemma SplitPartitioned(a: seq, l: nat, m: nat, r: nat)
    requires 0 <= l <= m < r <= |a|
    ensures a[l..m] + [a[m]] + a[m+1..r] == a[l..r]
{
    calc == {
        a[l..r];
        a[l..m] + a[m..r];
        { assert [a[m]] + a[m+1..r] == a[m..r]; }
        a[l..m] + [a[m]] + a[m+1..r];
    }
}

lemma SubArraySorted(a: array<int>, l: nat, r:nat)
    requires 0 <= l <= r <= a.Length
    requires Sorted(a[l..r])
    ensures forall i, j :: l <= i <= j < r ==> a[i] <= a[j]
{
}

lemma SortedJoin(a: array<int>, l: nat, m: nat, r: nat)
    requires 0 <= l <= m < r <= a.Length
    requires Sorted(a[l..m])
    requires Sorted(a[m+1..r])
    requires forall i :: l <= i < m ==> a[i] <= a[m]
    requires forall i :: m < i < r ==> a[m] <= a[i]
    ensures Sorted(a[l..r])
{
    forall i, j | l <= i <= j < r
        ensures a[i] <= a[j]
    {
        if j < m {
            SubArraySorted(a, l, m);
        } else if i > m {
            SubArraySorted(a, m, r);
        } else {
            assert a[i] <= a[m] <= a[j];
        }
    }
}

lemma ShufflePreserves<T>(a: seq, b: seq, P: T -> bool)
    requires multiset(a) == multiset(b)
    requires forall i :: 0 <= i < |a| ==> P(a[i])
    ensures forall i :: 0 <= i < |b| ==> P(b[i])
{
    forall i | 0 <= i < |b|
        ensures P(b[i])
    {
        if !P(b[i]) {
            assert multiset(b)[b[i]] > 0;
            assert multiset(a)[b[i]] > 0;
            var j :| 0 <= j < |a| && a[j] == b[i];
            assert !P(a[j]);
            assert false;
        }
    }
}

method QuickSortAux(a: array<int>, l: nat, r: nat)
    requires 0 <= l <= r <= a.Length
    modifies a
    decreases r - l
    // Sorting property
    ensures Sorted(a[l..r])
    ensures multiset(a[l..r]) == old(multiset(a[l..r]))
    // No change outside of a[l..r]
    ensures a[..l] == old(a[..l])
    ensures a[r..] == old(a[r..])
{
    if r - l < 2 {
        return;
    }
    ghost var pivot := a[l];
    var m := Partition(a, l, r);
    assert a[m] == pivot;

    ghost var a' := a[..];
    QuickSortAux(a, l, m);
    assert a[m] == pivot;
    assert multiset(a[l..m]) == multiset(a'[l..m]);
    assert a[m+1..r] == a'[m+1..r];

    ghost var a'' := a[..];
    QuickSortAux(a, m+1, r);
    assert a[m] == pivot;
    assert a[l..m] == a''[l..m];
    assert multiset(a[m+1..r]) == multiset(a'[m+1..r]);

    ShufflePreserves(a'[l..m], a[l..m], (x) => x <= pivot);
    ShufflePreserves(a'[m+1..r], a[m+1..r], (x) => x >= pivot);
    SortedJoin(a, l, m, r);
    calc == {
        multiset(a[l..r]);
        { SplitPartitioned(a[..], l, m, r); }
        multiset(a[l..m]) + multiset{pivot} + multiset(a[m+1..r]);
        multiset(a'[l..m]) + multiset{pivot} + multiset(a'[m+1..r]);
        { SplitPartitioned(a', l, m, r); }
        multiset(a'[l..r]);
    }
}

method QuickSort(a: array<int>)
    modifies a
    ensures Sorted(a[..])
    ensures multiset(a[..]) == old(multiset(a[..]))
{
    assert(a[..] == a[0..a.Length]);
    QuickSortAux(a, 0, a.Length);
    assert(a[..] == a[0..a.Length]);
}