#[kani::loop_decreases] currently only supports a single expression as the termination measure. Multi-dimensional measures using lexicographic ordering (e.g., #[kani::loop_decreases(n - i, n - j)] for nested loops) are rejected at compile time with an error.
The proc macro accepts comma-separated expressions syntactically but CBMC does not correctly process tuple-valued decreases measures through Kani's irep encoding. To prevent unsound results, a compile-time error was added in #4564.
Desired behavior
Support lexicographic ordering for multi-dimensional decreases, matching the semantics of Dafny's decreases and Verus's decreases clauses:
#[kani::loop_invariant(i <= n && j <= n)]
#[kani::loop_decreases(n - i, n - j)]
while i < n {
j = 0;
while j < n {
j += 1;
}
i += 1;
}The tuple (n - i, n - j) should decrease lexicographically: either the first component decreases, or the first stays the same and the second decreases.
Implementation notes
This requires encoding the lexicographic comparison in the irep serialization (to_irep.rs), either as a nested conditional expression or by using CBMC's native support for lexicographic decreases (if available in the CBMC version Kani targets).
#[kani::loop_decreases]currently only supports a single expression as the termination measure. Multi-dimensional measures using lexicographic ordering (e.g.,#[kani::loop_decreases(n - i, n - j)]for nested loops) are rejected at compile time with an error.The proc macro accepts comma-separated expressions syntactically but CBMC does not correctly process tuple-valued decreases measures through Kani's irep encoding. To prevent unsound results, a compile-time error was added in #4564.
Desired behavior
Support lexicographic ordering for multi-dimensional decreases, matching the semantics of Dafny's
decreasesand Verus'sdecreasesclauses:The tuple
(n - i, n - j)should decrease lexicographically: either the first component decreases, or the first stays the same and the second decreases.Implementation notes
This requires encoding the lexicographic comparison in the irep serialization (
to_irep.rs), either as a nested conditional expression or by using CBMC's native support for lexicographic decreases (if available in the CBMC version Kani targets).