Gnome sort

Important

Get the starting code for this tutorial in the creusot-rs/tutorial repository.

Open the file src/ex1_gnome_sort.rs.

Gnome sort is a sorting algorithm with the simplicity of a single while loop.

pub fn gnome_sort(v: &mut [usize])
{
    let mut n = 0;
    while n < v.len() {
        if n == 0 || v[n - 1] <= v[n] {
            n += 1;
        } else {
            v.swap(n - 1, n);
            n -= 1;
        }
    }
}

Starting from index n = 0, we increment n as long as we encounter successive elements in increasing order. When we find an element v[n] out of order (v[n] < v[n-1]), we insert it into the preceding sorted prefix by repeated swaps of adjacent elements.

Step 1: Specification

Write the contract of gnome_sort, using the #[ensures] attribute.

There are two postconditions to formalize:

1. The final slice ^v contains elements in increasing order.
2. The final slice ^v contains the same elements as the initial slice v.

After having written your specification, you should be able to compile the project (with the command cargo creusot --only=coma). But of course the proof attempt will fail (with the command cargo creusot).

Tip

• Universal quantification is written as forall<i> (or with a type annotation, forall<i: Int>). Implication is written as ==>.
• To access the elements of a slice in logic, use the view operator @. The term v@ denotes the finite sequence of elements contained in the slice v, and v@[i] denotes the i-th element of that sequence.
• The second postcondition is just (^v)@.permutation_of(v@). (Actually spelling this out is rather complicated and besides the point of this tutorial.)

#[ensures(forall<i,j> 0 <= i && i < j && j < v@.len() ==> (^v)@[i] <= (^v)@[j])]
#[ensures((^v)@.permutation_of(v@))]

Step 2: Loop invariant

To help Creusot prove that the contract is valid, we want to write a suitable loop invariant. There will be two clauses to the invariant, mirroring the desired postconditions we just wrote:

1. The first n elements of v are in increasing order.
2. The current slice v contains the same elements as the old slice (i.e., the initial value of the slice).

To be able to refer to the old slice, take a snapshot of v before entering the loop:

let old_v = snapshot!{ v };

A snapshot is a purely logical construct. Its value can only be accessed in specifications. During execution, a snapshot behaves like the unit ().

Now, old_v has type Snapshot<&mut [usize]>, so we can refer to the initial value as **old_v in Pearlite (one * for Snapshot, and one * for &mut).

Annotate the while loop with its invariant(s), using the #[invariant] attribute.

With this, the command cargo creusot should succeed. You have formally verified the functional correctness of a sorting function.

#[invariant(forall<i,j> 0 <= i && i < j && j < n@ ==> v@[i] <= v@[j])]
#[invariant(v@.permutation_of((**old_v)@))]

Step 3: Polymorphism

The function gnome_sort is currently restricted to elements of type usize. Let’s generalize gnome_sort to elements of any type that implements the comparison operation (<=). In other words, we can sort slices of any totally ordered type.

In Rust, totally ordered types implement the Ord trait. In Creusot, we also require such types T to implement the trait DeepModel, and for the associated type T::DeepModelTy to implement OrdLogic, which is the “logical” equivalent of Ord: OrdLogic defines the meaning of <= in Pearlite.

Although this looks convoluted, this makes it easier to specify and verify implementations of Ord for complex data structures.

With this generalization, we will also need to modify the #[ensures] and #[invariant] clauses. Instead of directly comparing elements of the slice (v@[i] <= v@[j]), we will compare their deep models (v@[i].deep_model() <= v@[j].deep_model()).

pub fn gnome_sort<T>(v: &mut [T])
where
    T: Ord + DeepModel,
    T::DeepModelTy: OrdLogic,
{
    /* ... */
}

Conclusion

We have proved the functional correctness of Gnome sort. Then we generalized it to sort elements of arbitrary ordered types.

Bonus challenge (non-trivial!): prove the termination of gnome_sort. See the Termination chapter for more information.