Failed to use loop contracts to prove contracts harness for proofs with nested loops

[qinheping]

I tried this code:

#[kani::modifies(x, y)]
#[kani::requires(*x >= 10 && *y >= 10)]
#[kani::ensures(|result|*x ==2)]
fn simple_while_loops(x: &mut u8, y: &mut u8) {
    #[kani::loop_invariant(*x >= 2)]
    while *x > 2 {
        *x = *x - 1;
        #[kani::loop_invariant(*y >= 2)]
        while *y > 2 {
            *y = *y - 1;
        }
    }
}

#[kani::proof_for_contract(simple_while_loops)]
fn multiple_loops_harness() {
    let mut x: u8 = kani::any_where(|i| *i >= 10);
    let mut y: u8 = kani::any_where(|i| *i >= 10);
    // multiple_loops();
    simple_while_loops(&mut x, &mut y);
}

using the following command line invocation:

kani multiple_loops.rs -Z loop-contracts --enable-unstable -Zfunction-contracts --cbmc-args --object-bits 8

with Kani version:

I expected to see this happen: VERIFICATION:- SUCCESSFUL

Instead, this happened:

SUMMARY:
 ** 1 of 420 failed (3 unreachable)
Failed Checks: Check assigns clause inclusion for loop simple_while_loops::{closure#2}::{closure#1}.0
 File: "multiple_loops.rs", line 39, in simple_while_loops::{closure#2}::{closure#1}

The cause of the failure is that when the function simple_while_loop is wrapped in a closure by function contracts, all user variables are hidden behind a struct in MIR, which fails the loop assigns inference in CBMC. So we need to specify the accurate loop modifies for the loops.

For reference, the following standard harness can be correctly proved:

fn simple_while_loops(x: &mut u8, y: &mut u8) {
    #[kani::loop_invariant(*x >= 2)]
    while *x > 2 {
        *x = *x - 1;
        #[kani::loop_invariant(*y >= 2)]
        while *y > 2 {
            *y = *y - 1;
        }
    }
}

#[kani::proof]
fn multiple_loops_harness() {
    let mut x: u8 = kani::any_where(|i| *i >= 10);
    let mut y: u8 = kani::any_where(|i| *i >= 10);
    // multiple_loops();
    simple_while_loops(&mut x, &mut y);

    assert!(x == 2);
}