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

Merged

feliperodri merged 9 commits intomodel-checking:mainfrom

feliperodri:decreases-clause

Apr 22, 2026

Commits on Apr 22, 2026

Add loop_decreases support to CBMC bindings (cprover_bindings)
feliperodri
committed
Add #[kani::loop_decreases] proc macro attribute
feliperodri
committed
Thread loop_decreases through kani-compiler codegen
feliperodri
committed
Add expected-pass tests for loop decreases clauses
feliperodri
committed
Add expected-fail tests for incorrect decreases clauses
feliperodri
committed
Add comprehensive documentation for decreases clauses
feliperodri
committed
Fix CI failures: remove tests exposing known limitations, fix remaining tests
feliperodri
committed
Add fixme tests for known decreases clause limitations
feliperodri
committed
Clear loop_decreases on non-contract path, rename stale measure test, document limitations
feliperodri
committed