Cannot check bubblesort: internal error

[safinaskar]

I use master ( b7565c36809873cb5de739ab98a93d76b824aded ). I use provided Dockerfile. Here is my code:

extern crate prusti_contracts;
use prusti_contracts::*;

fn sort(a: &mut [i32]) {
    let mut i = 0;
    while i + 1 < a.len() {
        body_invariant!(i < usize::MAX - 1);
        let mut j = 0;
        while j < a.len() - 1 {
            if a[j] > a[j + 1] { // A
                let mut sw = a[j]; // A
                a[j] = a[j + 1]; // A
                a[j + 1] = sw; // A
            } // A
            j += 1;
        }
        i += 1;
    }
}

fn main(){ }

I think this is correct bubble sort implementation, but I'm not sure.

Here is output:

root@c968cb0a8081:~# prusti-rustc /tmp/oo.rs
  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  | 
 |      /\   |  \ \__/ .__/  |       /\   | 

Prusti version: commit  <unknown>, built on 2022-04-22 17:10:20 UTC
warning: variable does not need to be mutable
  --> /tmp/oo.rs:11:21
   |
11 |                 let mut sw = a[j];
   |                     ----^^
   |                     |
   |                     help: remove this `mut`
   |
   = note: `#[warn(unused_mut)]` on by default

warning: function is never used: `sort`
 --> /tmp/oo.rs:4:4
  |
4 | fn sort(a: &mut [i32]) {
  |    ^^^^
  |
  = note: `#[warn(dead_code)]` on by default

Verification of 2 items...
error: [Prusti internal error] Prusti encountered an unexpected internal error
  --> /tmp/oo.rs:4:1
   |
4  | / fn sort(a: &mut [i32]) {
5  | |     let mut i = 0;
6  | |     while i + 1 < a.len() {
7  | |         body_invariant!(i < usize::MAX - 1);
...  |
18 | |     }
19 | | }
   | |_^
   |
   = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
   = note: Details: cannot generate fold-unfold Viper statements. The required permission Pred(_21.tuple_0, write) cannot be obtained.
           

Verification failed
error: aborting due to previous error; 2 warnings emitted

The same happens if I comment out lines marked with "A"

[JonasAlaif]

Thanks for reporting this. The issue seems to be with how a.len() - 1 is encoded with overflow checks enabled and with how (maybe?) the loop algorithm fails to figure out the required permissions for the check. @fpoli? @safinaskar I'd recommend using j + 1 < a.len() for now

[fpoli]

I think this is one more instance of https://github.com/viperproject/prusti-dev/issues/389. The permissions computed for the loop body invariant are wrong.

[safinaskar]

Putting body_invariant!(true) in the beginning of every loop (as suggested in https://github.com/viperproject/prusti-dev/issues/389 ) seems to work with current master.

extern crate prusti_contracts;
use prusti_contracts::*;

fn sort(a: &mut [i32]) {
    let mut i = 0;
    while i + 1 < a.len() {
        body_invariant!(true);
        body_invariant!(i < usize::MAX - 1);
        let mut j = 0;
        while j < a.len() - 1 {
            body_invariant!(true);
            if a[j] > a[j + 1] { // A
                let mut sw = a[j]; // A
                a[j] = a[j + 1]; // A
                a[j + 1] = sw; // A
            } // A
            j += 1;
        }
        i += 1;
    }
}

fn main(){ }