`#[kani::loop_decreases]` does not support struct field projections or arithmetic expressions

[feliperodri]

The #[kani::loop_decreases] attribute only works with simple variable measures. Arithmetic expressions (e.g., 19 - p) and struct field projections (e.g., state.remaining) fail because:

1. Arithmetic expressions: Rust's checked arithmetic compiles to CheckedBinaryOp which produces a StatementExpression in the GOTO program. By the time the decreases assignment is processed in codegen, the expression has been split across multiple MIR statements — the decreases binding only captures the final field access (_4.0), not the full computation.

2. Struct field projections: Similar MIR decomposition issue — the field access is split into separate statements.

Steps to reproduce

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

#[kani::proof]
fn check_arithmetic_decreases() {
    let mut p: u32 = 0;
    #[kani::loop_invariant(p <= 19)]
    #[kani::loop_decreases(19 - p)]
    while p < 19 {
        p += 1;
    }
}

Expected behavior

Verification succeeds — 19 - p strictly decreases each iteration.

Actual behavior

Failed Checks: Check variant decreases after step for loop

Workaround

Use wrapping_sub instead of -:

#[kani::loop_decreases(19u32.wrapping_sub(p))]

Or restructure the loop to count down so a simple variable suffices:

let mut remaining: u32 = 19;
#[kani::loop_decreases(remaining)]
while remaining > 0 {
    remaining -= 1;
}