Add #[kani::loop_decreases] for proving loop termination

[feliperodri]

Add #[kani::loop_decreases] for proving loop termination via Floyd's method. Loop invariants alone prove partial correctness, they don't guarantee the loop terminates. A decreases clause specifies a measure that must strictly decrease on each iteration, proving total correctness.

Maps to CBMC's #spec_decreases annotation via goto-instrument.

Problem

Without a decreases clause, a loop invariant can verify properties on code after the loop, but if the loop never terminates, that code is unreachable and the property is vacuously true. This is a soundness gap for total correctness proofs.

Solution

Proc macro (kani_macros)

• #[kani::loop_decreases(expr)] attribute generates a let kani_loop_decreases = (expr,); binding before the loop
• Validates the attribute is applied to a loop statement (while, loop, for)
• Rejects multi-dimensional measures (loop_decreases(a, b)) with a compile error — lexicographic ordering is not yet supported (#[kani::loop_decreases] does not support struct field projections or arithmetic expressions #4585)

CBMC bindings (cprover_bindings)

• loop_decreases: Option<Expr> field in StmtBody::Goto
• with_loop_decreases() builder, mirroring with_loop_invariants() and with_loop_modifies()
• CSpecDecreases irep serialization

Compiler codegen (kani-compiler)

• Detects kani_loop_decreases assignments in MIR and stores the expression
• Attaches the decreases expression to the loop's goto statement
• Emits a warning when #[kani::loop_decreases] is used without -Z loop-contracts

Example

#[kani::proof]
fn binary_search_terminates() {
    let arr: [i32; 8] = kani::any();
    let target: i32 = kani::any();
    let mut lo: usize = 0;
    let mut hi: usize = arr.len();

    #[kani::loop_invariant(lo <= hi && hi <= arr.len())]
    #[kani::loop_decreases(hi - lo)]
    while lo < hi {
        let mid = lo + (hi - lo) / 2;
        if arr[mid] == target { break; }
        else if arr[mid] < target { lo = mid + 1; }
        else { hi = mid; }
    }
}

Testing

8 passing expected tests:

• simple_while_loop_decreases — basic countdown
• loop_loop_decreases — loop { ... break } with decreases
• decreases_expr — expression-based measure
• decreases_binary_search — binary search termination
• decreases_loop_max — function with loop + decreases
• decreases_with_function_contract — combined with #[kani::requires]/#[kani::ensures]
• decreases_with_old — using on_entry() in decreases
• decreases_no_flag — warning emitted without -Z loop-contracts

2 expected-fail tests:

• decreases_fail_wrong_measure — incorrect measure (increasing instead of decreasing)
• decreases_fail_stale_measure — stale measure (variable not modified by loop)

4 fixme tests (known limitations, tracked as issues):

• fixme_decreases_struct_field — struct field projections (#[kani::loop_decreases] combined with #[kani::loop_modifies] causes verification failure #4584)
• fixme_multi_dim_decreases — multi-dimensional measures (#[kani::loop_decreases] does not support struct field projections or arithmetic expressions #4585)
• fixme_decreases_with_modifies — combined with loop_modifies (Support multi-dimensional (lexicographic) decreases clauses in #[kani::loop_decreases] #4586)
• fixme_nested_loops_decreases — nested loops with assigns conflict (Support multi-dimensional (lexicographic) decreases clauses in #[kani::loop_decreases] #4586)

Known Limitations

The following limitations are tracked as separate issues:

• Arithmetic expressions in decreases clauses (e.g., 19 - p) fail due to Rust's checked arithmetic producing StatementExpression nodes. Workaround: use wrapping_sub. (#[kani::loop_decreases] combined with #[kani::loop_modifies] causes verification failure #4584)
• Multi-dimensional decreases (#[kani::loop_decreases(a, b)]) is rejected at compile time; lexicographic ordering is not yet supported. (#[kani::loop_decreases] does not support struct field projections or arithmetic expressions #4585)
• Combining loop_decreases with loop_modifies causes spurious verification failures. Workaround: use loop_decreases + loop_invariant without loop_modifies. (Support multi-dimensional (lexicographic) decreases clauses in #[kani::loop_decreases] #4586)

---

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.