Loop Contract Issue: Check some_var is assignable

[MinghuaWang]

I tried this code:

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

fn func(x: usize) {
    let mut j = 0;
    const CHUNK_SIZE: usize = 32;
    #[kani::loop_invariant(j <=x )]
    while j < x {
        let mut i = 0;
        let mut sum = 0_usize;
        #[kani::loop_invariant(i <= CHUNK_SIZE && prev(i) <= CHUNK_SIZE && prev(i) + 1 == i && sum <= CHUNK_SIZE && on_entry(sum) + i >= sum )]
        while i < CHUNK_SIZE {
            sum += kani::any::<bool>() as usize;
            i += 1;
        }

        j += 1;
    }
}

#[kani::proof]
fn harness() {
    let _ = func(10);
}

fn main() {}

using the following command line invocation:

kani src/main.rs -Z -loop-contracts -Z function-contracts 

with Kani version: 0.63.0 (branch main, commit: 8d18568)

I expected to see this happen: verification success

Instead, this happened:

 ** 3 of 235 failed (3 unreachable)
Failed Checks: Check assigns clause inclusion for loop func.0
 File: "src/main.rs", line 11, in func
Failed Checks: Check that *var_9 is assignable
 File: "src/main.rs", line 13, in func::{closure#1}
Failed Checks: Check that *var_12 is assignable
 File: "src/main.rs", line 14, in func::{closure#1}

VERIFICATION:- FAILED
Verification Time: 0.15695447s

The code has nested loops, and the errors are associated with the inner loop. From my understanding, var_9 represents sum, and var_12 represents i. I don't know how to resolve these errors. Perhaps a loop_modifies clause is required for this loop invariant?

[tautschnig]

loop_modifies is still work-in-progress, cf. #3871.

[thanhnguyen-aws]

Thanks for reporting this issue. This is not a problem of user specified loop_assign (loop_modifies) clause, but that of handling lifetime of variables that are declared in a loop-body, then modified inside an inner loop, which makes CBMC unable to infer the loop_assign clause. Here is a simple example, which has the same issue.

#[kani::proof]
fn main() {
    let mut i = 2;
    #[kani::loop_invariant(i <= 5)]
    while i < 5 {
        let mut j = 0;
        #[kani::loop_invariant(j <= 5)]
        while j < 5 {
            j =  j + 1;
        }
    }
}

But, there is no issue like that when we change the code into:

#[kani::proof]
fn main() {
    let mut i = 2;
    let mut j = 0;
    #[kani::loop_invariant(i <= 5)]
    while i < 5 {
        #[kani::loop_invariant(j <= 5)]
        while j < 5 {
            j =  j + 1;
        }
    }
}

I am trying to fix it shortly.