Debugging loop invariant failure

[zhassan-aws]

On the following program:

use prusti_contracts::*; 

#[ensures((exists(|i: usize| i < s.len() && s[i] == x) <==> result))]
fn search(s: &[u8], x: u8) -> bool {
    let mut i = 0;
    while i < s.len() {
        body_invariant!(i <= s.len());
        body_invariant!(forall(|j: usize| j < i ==> (s[j] != x)));
        if s[i] == x {
            return true;
        }
        i += 1;
    }
    false
}

Prusti reports the following:

[Prusti: verification error] loop invariant might not hold after a loop iteration that preserves the loop condition.

The same occurs with overflow checks turned off.

Any ideas on how to debug the loop invariant failure?

[fpoli]

Thanks for the report. A common technique to debug why a property doesn't hold is to manually assert it with prusti_assert!(...) at various points in the program.

My first guess was that this issue was due to the missing triggers in the annotations (see https://github.com/viperproject/prusti-dev/issues/1285#issuecomment-1406264249), but that was not enough. It turns out that this is an incompleteness of Viper (both with the Carbon and Silicon solvers). To work around that, it's necessary to set use_more_complete_exhale=false in Prusti (i.e. in a Prusti.toml file or with the PRUSTI_USE_MORE_COMPLETE_EXHALE=false environment variable). This way, the following program verifies.

use prusti_contracts::*;

#[ensures(exists(|i: usize| i < s.len() && s[i] == x, triggers=[(s[i],)]) == result)]
fn search(s: &[u8], x: u8) -> bool {
    let mut i = 0;
    while i < s.len() {
        body_invariant!(i < s.len()); // The `<=` is not needed; it's never `i == s.len()` at this program point.
        body_invariant!(forall(|j: usize| j < i ==> (s[j] != x), triggers=[(s[j],)]));
        if s[i] == x {
            return true;
        }
        i += 1;
    }
    false
}

[zhassan-aws]

Cool, thanks!

[Patrick-6]

The following function seems to be related to this issue:

use prusti_contracts::*;

// #[requires(src.len() != 0)] // adding this makes it verify
#[requires(src.len() == dst.len())] 
// This postcondition should verify, but doesn't:
#[ensures(forall(|i: usize|
    // src.len() != 0 && // adding this makes it verify
    i < src.len()
        ==> dst[i] === old(snap(&src))[i]))]
fn copy_slice<T: Copy>(src: &[T], dst: &mut [T]) {
    let mut i = 0;
    while i < src.len() {
        body_invariant!(dst.len() == src.len());
        body_invariant!(forall(|j: usize| j < i ==> dst[j] === old(snap(&src))[j]));
        dst[i] = src[i];
        i += 1;
    }
    // This is needed to prove the last prusti_assert:
    prusti_assert!(i == src.len());

    // Copy of the postcondition (it passes, but the postcondition doesn't):
    prusti_assert!(forall(|i: usize| i < src.len() ==> dst[i] === old(snap(&src))[i]));
}

This verifies with use_more_complete_exhale=false, but not with it set to true. With true, it can still be verified by either adding the precondition #[requires(src.len() != 0)] or by adding the condition src.len() != 0 to the left side of the implication in the quantifier. Interestingly, copying the postcondition into a prusti_assert at the end of the function (and asserting i == src.len()) does not cause an error there, but the postcondition still fails.