Panic on "Procedure contains a loop"

[jmc-figueira]

The following code causes an unexpected panic:

// ghost function to prove sum
#[pure]
#[requires(n < self.len())]
#[ensures(n < self.len())]
#[ensures(result == self.lookup(n) + self.sum_rec(result, n - 1))]
pub(crate) fn sum_rec(&self, accum: u64, n: usize) -> u64 {
    if n == 0 {
        accum
    } else {
        self.sum_rec(accum + self.lookup(n), n - 1)
    }
}

#[pure]
#[ensures(result == self.sum_rec(0, self.len() - 1))]
pub fn sum(&self) -> u64 {
    let mut i = 0usize;
    let mut accumulator = 0u64;

    while i < self.len() {
        body_invariant!(i < self.len());
        body_invariant!(accumulator == self.lookup(i) + self.sum_rec(accumulator, self.len() - (1 + i)));
        accumulator += self.lookup(i);
        i += 1;
    }

    accumulator
}

thread 'rustc' panicked at 'Procedure DefId(0:141 ~ prusti_pset[5a66]::base::vec_wrapper::{impl#0}::sum) contains a loop', prusti-viper/src/encoder/pure_function_encoder.rs:86:14
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.

Full example snippet

[fpoli]

Thanks! The correct error message should be something like "loops are not allowed in pure functions". Usually you can convert the loop to some recursive call, which is supported.

[JonasAlaif]

A simple and full example to trigger this issue is:

use prusti_contracts::*;
#[pure]
pub fn foo() {
    loop { }
}
fn main() {}