Add #[kani::loop_decreases] for proving loop termination (#4564)

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 (#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

```rust
#[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 (#4584)
- `fixme_multi_dim_decreases` — multi-dimensional measures (#4585)
- `fixme_decreases_with_modifies` — combined with `loop_modifies`
(#4586)
- `fixme_nested_loops_decreases` — nested loops with assigns conflict
(#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`. (#4584)
- **Multi-dimensional decreases** (`#[kani::loop_decreases(a, b)]`) is
rejected at compile time; lexicographic ordering is not yet supported.
(#4585)
- **Combining `loop_decreases` with `loop_modifies`** causes spurious
verification failures. Workaround: use `loop_decreases` +
`loop_invariant` without `loop_modifies`. (#4586)

---

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

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

cprover_bindings/src/goto_program/stmt.rs

@@ -86,6 +86,7 @@ pub enum StmtBody {
         // applied as loop contracts in CBMC if it is a backward goto.
         loop_invariants: Option<Expr>,
         loop_modifies: Option<Vec<Expr>>,
+        loop_decreases: Option<Expr>,
     },
     /// `if (i) { t } else { e }`
     Ifthenelse {
@@ -282,7 +283,7 @@ impl Stmt {
     pub fn goto<T: Into<InternedString>>(dest: T, loc: Location) -> Self {
         let dest = dest.into();
         assert!(!dest.is_empty());
-        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None }, loc)
+        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None, loop_decreases: None }, loc)
     }
 
     /// `if (i) { t } else { e }` or `if (i) { t }`
@@ -327,13 +328,14 @@ impl Stmt {
 
     /// `goto dest;` with loop invariant
     pub fn with_loop_contracts(self, inv: Expr) -> Self {
-        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
             assert!(loop_invariants.is_none());
             stmt!(
                 Goto {
                     dest: *dest,
                     loop_invariants: Some(inv),
-                    loop_modifies: loop_modifies.clone()
+                    loop_modifies: loop_modifies.clone(),
+                    loop_decreases: loop_decreases.clone()
                 },
                 *self.location()
             )
@@ -343,20 +345,38 @@ impl Stmt {
     }
 
     pub fn with_loop_modifies(self, asg: Vec<Expr>) -> Self {
-        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
             assert!(loop_modifies.is_none());
             stmt!(
                 Goto {
                     dest: *dest,
                     loop_invariants: loop_invariants.clone(),
-                    loop_modifies: Some(asg)
+                    loop_modifies: Some(asg),
+                    loop_decreases: loop_decreases.clone()
                 },
                 *self.location()
             )
         } else {
             unreachable!("Loop assigns should be annotated only to goto stmt")
         }
     }
+
+    pub fn with_loop_decreases(self, decreases: Expr) -> Self {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
+            assert!(loop_decreases.is_none());
+            stmt!(
+                Goto {
+                    dest: *dest,
+                    loop_invariants: loop_invariants.clone(),
+                    loop_modifies: loop_modifies.clone(),
+                    loop_decreases: Some(decreases)
+                },
+                *self.location()
+            )
+        } else {
+            unreachable!("Loop decreases should be annotated only to goto stmt")
+        }
+    }
 }
 
 /// Predicates

cprover_bindings/src/irep/irep_id.rs

@@ -595,6 +595,7 @@ pub enum IrepId {
     Used,
     IsUsed,
     CSpecLoopInvariant,
+    CSpecDecreases,
     CSpecRequires,
     CSpecEnsures,
     CSpecAssigns,
@@ -1485,6 +1486,7 @@ impl IrepId {
             IrepId::Used => "used",
             IrepId::IsUsed => "is_used",
             IrepId::CSpecLoopInvariant => "#spec_loop_invariant",
+            IrepId::CSpecDecreases => "#spec_decreases",
             IrepId::CSpecRequires => "#spec_requires",
             IrepId::CSpecEnsures => "#spec_ensures",
             IrepId::CSpecAssigns => "#spec_assigns",

cprover_bindings/src/irep/to_irep.rs

@@ -556,7 +556,7 @@ impl ToIrep for StmtBody {
                     arguments_irep(arguments.iter(), mm),
                 ],
             ),
-            StmtBody::Goto { dest, loop_invariants, loop_modifies } => {
+            StmtBody::Goto { dest, loop_invariants, loop_modifies, loop_decreases } => {
                 let inv = loop_invariants
                     .clone()
                     .map(|inv| inv.clone().and(Expr::bool_true()).to_irep(mm));
@@ -565,10 +565,12 @@ impl ToIrep for StmtBody {
                         assigns.iter().map(|assign| assign.to_irep(mm)).collect(),
                     )])
                 });
+                let decreases = loop_decreases.clone().map(|dec| dec.to_irep(mm));
                 code_irep(IrepId::Goto, vec![])
                     .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()))
                     .with_named_sub_option(IrepId::CSpecLoopInvariant, inv)
                     .with_named_sub_option(IrepId::CSpecAssigns, assigns.clone())
+                    .with_named_sub_option(IrepId::CSpecDecreases, decreases)
             }
             StmtBody::Ifthenelse { i, t, e } => code_irep(
                 IrepId::Ifthenelse,

docs/src/reference/attributes.md

@@ -248,6 +248,6 @@ There are numerous attributes for function and loop contracts. At present, these
 - Proof harness for contracts: `#[kani::proof_for_contract(name-of-function)]`
 - Verified stubbing: `#[kani::stub_verified]`
 - Function contract specification: `#[kani::requires]`, `#[kani::modifies]`, `#[kani::ensures]`, `#[kani::recursion]`
-- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`.
+- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`, `#[kani::loop_decreases]`.
 
 See the documentation on [function contracts](./experimental/contracts.md) and [loop contracts](./experimental/loop-contracts.md) for details.