Prusti panics on `slices in loops not yet implemented`

[hiroki-chen]

Hi there, I am trying to verify the correctness of a selection sort algorithm that contains nested while loops, but Prusti would panic when parsing the following code:

#[allow(unused)]
#[ensures(old(arr.len()) == arr.len())]
#[ensures(sorted(arr))]
fn selection_sort(arr: &mut [i64]) {
    if arr.len() <= 1 {
        return;
    }

    let mut i = 0usize;
    let mut min = i;

    while i < arr.len() {
        body_invariant!(arr.len() > 1);

        let mut j = i + 1;
        min = i;

        while j < arr.len() {
            body_invariant!(j < arr.len() && min <= j);

            if arr[j] < arr[min] {
                min = j;
            }

            j += 1;
        }

        let arr_i = arr[i];
        let arr_min = arr[min];
        arr[i] = arr_min;
        arr[min] = arr_i;

        i += 1;
    }
}

where sorted is defined as

predicate! {
    fn sorted(arr: &[i64]) -> bool {
        arr.len() > 1 ==> forall(|i: usize| 1 <= i && i < arr.len() ==> arr[i - 1] <= arr[i])
    }
}

The output of Prusti is

thread 'rustc' panicked at 'not implemented: slices in loops not yet implemented', prusti-viper/src/encoder/procedure_encoder.rs:5221:78
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

error: internal compiler error: unexpected panic

note: Prusti or the compiler unexpectedly panicked. This is a bug.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: 0.2.2, commit aa8844c82ae 2023-04-06 12:52:39 UTC, built on 2023-04-17 03:07:02 UTC

The bug can be eliminated if I remove

 let arr_i = arr[i];
 let arr_min = arr[min];
 arr[i] = arr_min;
 arr[min] = arr_i;

or the inner while, but doing so is certainly meaningless because the algorithm would be incorrect. Interestingly, however, nested loops in bubble sort can be successfully verified; making the parameter type to sized slice [i64; 100] works too.

Any insights or ideas are greatly appreciated :)