Internal error from mutually recursive pure functions

[Patrick-6]

Mutually recursive pure functions cause an error: [Prusti internal error] Prusti encountered an unexpected internal error Details: Rust function m_bug$$mutually_recursive_pure_fn$$f encoded both as a Viper method and function. There are no errors if both are not marked with #[pure]:

use prusti_contracts::*;

#[pure]
#[ensures(result == 0)]
fn f(n: u64) -> u64 {
    if n == 0 {
        0
    } else {
        g(n - 1)
    }
}

#[pure]
#[ensures(result == 0)]
fn g(n: u64) -> u64 {
    if n == 0 {
        0
    } else {
        f(n - 1)
    }
}

[fpoli]

Thank you for the report!

[nokunish]

Hi,

There might be a similar issue with mutually referential specifications. For instance, if we have

#[pure]
#[trusted]
#[ensures(result == nested_fn(_u))]
pub fn is_true(_u: usize) -> bool {
    return true
}

#[pure]
#[trusted]
#[ensures(result == is_true(u))]
pub fn nested_fn(u: usize) -> bool {
    is_true(u)
}

then

1. If neither are trusted, it crashes Prusti
2. If only one of them is trusted, then it produces the error: Details: Rust function m_test_v1$$external_spec$$bug$$spec_bug$$SomeVec$$$openang$T$closeang$$$len encoded both as a Viper method and function
3. If both are trusted, it verifies