Compiler or Prusti unexpectedly panicked

[ramsdell]

The enclosed log was generated when trying to verify an iterative version of a function that computes the sum of the first n integers. My installed system verifies the code in the Fibbonacci example, so the installation does something.

John

sum_of_ints.log sum_of_ints.rs.txt

[fpoli]

Hi! Thanks for the report and sorry for the late answer. I disabled Github notifications for a while.

Here is what I did to verify your program:

1. The #[invariant = "..."] attribute has to be placed before the while, not inside. We should add some checks to provide a proper error message instead of panicking, thus I marked this issue as bug.
2. iter_form(n) cannot be used in a specification because that function is not marked as pure, but in this case you can just use result. Again, we should add some checks to provide a proper error message instead of panicking.
3. Now Prusti works fine, but the program does not verify. The reason is that there is no invariant on i, so you can add an invariant 1 <= i && i <= n + 1.
4. The type of n is unsigned, but Prusti automatically encodes value ranges only when checking for integer overflows (disabled by default). So, you can either
   • add n >= 0 preconditions to every function, or
   • enable overflow checks and add preconditions such as n <= 999999 to make sure that the result does not overflow. For some reason, Prusti also needs a n == old(n) loop invariant to verify the program. This shouldn't be needed, so it seems a Prusti bug. I'll investigate.

To enable overflow checks (and encoding of value ranges)

If you are using Prusti from the IDE, create a file named Prusti.toml containing CHECK_BINARY_OPERATIONS=true in the same folder of the program that you want to verify.

If you are running Prusti from the command line, place the Prusti.toml in the folder from which you run Prusti or set the PRUSTI_CHECK_BINARY_OPERATIONS=true environment variable.

Working examples

Without implicit value ranges and overflow checks:

extern crate prusti_contracts;

#[pure]
#[requires="n >= 0"]
fn closed_form(n: u64) -> u64 {
    n * (n + 1) / 2
}

#[pure]
#[requires="n >= 0"]
#[ensures = "rec_form(n) == closed_form(n)"]
fn rec_form(n: u64) -> u64 {
    if n == 0 {
        0
    } else {
        n + rec_form(n - 1)
    }
}

#[requires="n >= 0"]
#[ensures = "result == closed_form(n)"]
fn iter_form(n: u64) -> u64 {
    let mut i = 1;
    let mut acc = 0;
    #[invariant = "1 <= i && i <= n + 1"]
    #[invariant = "acc == closed_form(i - 1)"]
    while i <= n {
        acc += i;
        i += 1;
    }
    acc
}

#[trusted]
fn main() {
    let n = 5;
    println!("Closed form {}", closed_form(n));
    println!("Recursive form {}", rec_form(n));
    println!("Iterative form {}", iter_form(n));
}

---

With implicit value ranges and overflow checks:

extern crate prusti_contracts;

#[pure]
#[requires="n <= 999999"]
fn closed_form(n: u64) -> u64 {
    n * (n + 1) / 2
}

#[pure]
#[requires="n <= 999999"]
#[ensures = "rec_form(n) == closed_form(n)"]
fn rec_form(n: u64) -> u64 {
    if n == 0 {
        0
    } else {
        n + rec_form(n - 1)
    }
}

#[requires="n <= 999999"]
#[ensures = "result == closed_form(n)"]
fn iter_form(n: u64) -> u64 {
    let mut i = 1;
    let mut acc = 0;
    #[invariant = "n == old(n)"] // workaround
    #[invariant = "1 <= i && i <= n + 1"]
    #[invariant = "acc == closed_form(i - 1)"]
    while i <= n {
        acc += i;
        i += 1;
    }
    acc
}

#[trusted]
fn main() {
    let n = 5;
    println!("Closed form {}", closed_form(n));
    println!("Recursive form {}", rec_form(n));
    println!("Iterative form {}", iter_form(n));
}

[fpoli]

I split this issue into #10, #11, #12.

[zgrannan]

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf

[zgrannan]

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf