Sometimes `prusti_assert` needed that exactly repeats the branch condition

[Stef-Gijsberts]

I noticed that to prove some statements, it is necessary to add a prusti_assert that exactly repeats a known fact.

In particular, this seems to happen if:

• The statement to prove has an existential quantifier, and
• tuples are involved.

I encountered this problem in a bigger function. For the purpose of demonstration, I reduced it to a minimal example.

First example

This fails:

#[requires(pairs.len() > 0)]
#[ensures(result ==> exists(|i: usize| pairs[i].0 == key))]
pub fn head_match_first(pairs: &[(i32, char)], key: i32) -> bool {
    if pairs[0].0 == key {
        true
    } else {
        false
    }
}

But to my surprise the following does not fail, although only the prusti_assert was added which exactly matches the branch condition:

#[requires(pairs.len() > 0)]
#[ensures(result ==> exists(|i: usize| pairs[i].0 == key))]
pub fn head_match_first(pairs: &[(i32, char)], key: i32) -> bool {
    if pairs[0].0 == key {
        prusti_assert!(pairs[0].0 == key);
        true
    } else {
        false
    }
}

Second example

This second example is the same function written differently, without the if-statement. Again, this fails:

#[requires(pairs.len() > 0)]
#[ensures(result ==> exists(|i: usize| pairs[i].0 == key))]
pub fn head_match_first(pairs: &[(i32, char)], key: i32) -> bool {
    pairs[0].0 == key
}

But this does not fail:

#[requires(pairs.len() > 0)]
#[ensures(result ==> exists(|i: usize| pairs[i].0 == key))]
pub fn head_match_first(pairs: &[(i32, char)], key: i32) -> bool {
    let result = pairs[0].0 == key;
    prusti_assert!(result == (pairs[0].0 == key));
    result
}

[fpoli]

This is a triggering issue. If you do not specify triggers, Prusti will try to automatically choose something on its own, but the choice is not always good and you can get this surprising behavior where the repeated code manages to match the automatically chosen trigger. It is always better to be explicit and write the triggers, as in the programs below.

use prusti_contracts::*;

#[requires(pairs.len() > 0)]
#[ensures(result ==> exists(|i: usize| pairs[i].0 == key, triggers=[(pairs[i],)]))]
pub fn head_match_first(pairs: &[(i32, char)], key: i32) -> bool {
    if pairs[0].0 == key {
        true
    } else {
        false
    }
}

fn main() {}

use prusti_contracts::*;

#[requires(pairs.len() > 0)]
#[ensures(result ==> exists(|i: usize| pairs[i].0 == key, triggers=[(pairs[i],)]))]
pub fn head_match_first(pairs: &[(i32, char)], key: i32) -> bool {
    pairs[0].0 == key
}

fn main() {}

To close this issue, I believe we should document triggers in the user guide.