Taking a mutable slice not supported

[Omar0Tarek]

In the code below, the function insertion_sort loops over the input array v from the end to the start (v.len() - 2 to 0), inserting the element v[i] every loop in its correct position in the subarray v[i..].

The function insert_head moves the first element in the array to its correct position, as the rest of the array v[1..] is sorted, and returns a completely sorted array.

#[trusted]
#[requires(v.len() > 1)]
#[requires(forall(|x: usize, y: usize| (1 <= x && x <= y && y < v.len()) ==> v[x] <= v[y]))] // this pre-condition might not hold
#[ensures(forall(|x: usize, y: usize| (0 <= x && x <= y && y < v.len()) ==> v[x] <= v[y]))]
#[ensures(v.len() == old(v.len()))]
fn insert_head(v: &mut [i32]) {}

#[requires(v.len() > 1)]
#[ensures(forall(|x: usize, y: usize| ((0 <= x && x <= y && y < v.len()) ==> v[x] <= v[y])))]
fn insertion_sort(v: &mut [i32]) {
    let mut i = v.len() - 2;
    loop {
        body_invariant!(i >= 0 && i < v.len() - 1);
        body_invariant!(forall(|x: usize, y: usize| (i + 1 <= x && x <= y && y < v.len()) ==> v[x] <= v[y]));
        insert_head(&mut v[i..]); // error when calling the function here
        if i == 0 {
            break;
        } else {
            i -= 1;
        }
    }
}

When running Prusti, verification fails with an error that the pre-condition #[requires(forall(|x: usize, y: usize| (1 <= x && x <= y && y < v.len()) ==> v[x] <= v[y]))] of the function insert_head might not hold when the function is called from inside the loop in the function insertion_sort (check comments in above code). The error happens because we are passing an array slice to insert_head.

This was fixed when the array slice was replaced with passing the whole array, along with the slice's starting index, as shown in the code below which was verified successfully.

#[trusted]
#[requires(v.len() > 1)]
#[requires(i < v.len() - 1)]
#[requires(forall(|x: usize, y: usize| (i + 1 <= x && x <= y && y < v.len()) ==> v[x] <= v[y]))]
#[ensures(forall(|x: usize, y: usize| (i <= x && x <= y && y < v.len()) ==> v[x] <= v[y]))]
#[ensures(v.len() == old(v.len()))]
fn insert_head(v: &mut [i32], i: usize) {}

#[requires(v.len() > 1)]
#[ensures(forall(|x: usize, y: usize| ((0 <= x && x <= y && y < v.len()) ==> v[x] <= v[y])))]
fn insertion_sort(v: &mut [i32]) {
    let mut i = v.len() - 2;
    loop {
        body_invariant!(i >= 0 && i < v.len() - 1);
        body_invariant!(forall(|x: usize, y: usize| (i + 1 <= x && x <= y && y < v.len()) ==> v[x] <= v[y]));
        insert_head(v, i);
        if i == 0 {
            break;
        } else {
            i -= 1;
        }
    }
}

[JonasAlaif]

Mutably slicing in not supported atm, so Prusti has no idea how the base sequence will be updated from any changes to the slice. I would recommend writing your own wrapper function, e.g.:

#[truested]
#[requires(...)]
#[ensures(...)]
fn take_mut_slice(s: &mut [i32], start: usize) -> &mut [i32] { &mut s[start..] }

with an appropriate contract (e.g. using a pledge in the postcondition)

[vakaras]

Reopening since we should support this eventually.