Unsupported constant string in println

[MathieuSoysal]

Current code:

use prusti_contracts::*;

const MAX_FIBONACCI: u32 = 2_971_215_073;

pub fn play_game(n: u32) {
    println!("{}", fizz_buzz_fibonacci(n));
}

#[trusted]
fn is_fibonacci_number(n: u32) -> bool {
    let (mut previous, mut current) = (0, 1);
    while current < n && n <= MAX_FIBONACCI {
        let next = previous + current;
        previous = current;
        current = next;
    }
    current == n
}

pub fn fizz_buzz_fibonacci(n: u32) -> String {
    if is_fibonacci_number(n) {
        "Fibonacci".to_string()
    } else {
        match (n % 3, n % 5) {
            (0, 0) => "FizzBuzz".to_string(),
            (0, _) => "Fizz".to_string(),
            (_, 0) => "Buzz".to_string(),
            (_, _) => n.to_string(),
        }
    }
}

But I obtain this error:

[Prusti: unsupported feature] unsupported constant type &'?11 [&'?12 str; Const { ty: usize, kind: Leaf(0x0000000000000002) }]

Someone know how to fix it ?

[fpoli]

The error message is reporting that the string used in the println! is not supported. At the moment, there is not much that we do to veryify I/O or string properties. To work around the error you could mark play_game as #[trusted], meaning that it won't be verified.

If you still want to prove some properties about it you could, for example, add a parameter to counts how many times the play_game function has been executed. This makes it possible to prove properties in the code that calls play_game. However, it depends a lot on what you want to do.

#[trusted]
#[ensures(*counter == old(*counter) + 1)]
pub fn play_game(n: u32, counter: &mut usize) {
    println!("{}", fizz_buzz_fibonacci(n));
    counter += 1;
}