Handle let-chain conditions in #[kani::loop_invariant]

[kasimte]

Resolves #4943

#[kani::loop_invariant] on a while loop whose condition is a let chain fails to compile: while_let_rewrite only handles a condition that is entirely a let, so a chain falls through to the plain while path, which rebuilds the condition, and the re-emitted let reaches the parser parenthesized, which is not a valid chain operand.

This adds a chain case ahead of that fallthrough: the loop is rewritten to loop { if <chain> { body } else { break } }, and the existing Expr::Loop invariant path handles the result. Label and attributes are preserved on the new loop. Because the rewrite places the original chain verbatim as the if condition, evaluation order and short-circuiting are unchanged; the chain_short_circuits test witnesses this with a side-effecting scrutinee.

Tests are a cargo-kani package (let chains are edition-2024 syntax, which a single-file test cannot express): basic chain, multi-let chain, short-circuit side effect, labeled break, and the cfg_attr spelling, plus two deliberately-failing harnesses — a violated invariant, and a loop_modifies whose assigns check must fail — pinning that both attributes apply to the rewritten loop rather than being silently dropped.

The change is additive: the new path fires only for let-chain conditions (a top-level && chain containing a let), so the existing bare-while let and for rewrites are behaviorally unchanged.

Known limitation: a let-chain loop that runs zero iterations while carrying a prev invariant is subject to the pre-existing zero-iteration prev issue (#4953) — the rewrite produces the same Expr::Loop whose shared loop_guard = true path asserts the invariant even when the loop never ran. It is a spurious failure, never a missed one.

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

[Copilot]

Copilot review overview

🟡 Changes recommended

The rewrite changes zero-iteration behavior for invariants using prev(...).

Review effort: Balanced
Findings: 1

Open (1)

• Preserve chain guard in prev expansion to prevent false-path invariant failure · New

What changed in this PR

Adds let-chain support to #[kani::loop_invariant] by rewriting affected while loops into equivalent loop expressions.

Changes:

• Detects let-chain conditions, including invisible token groups.
• Preserves loop labels and attributes during rewriting.
• Adds Cargo-based regression coverage for chain behavior and invariant enforcement.

File	Description
library/​kani_macros/​src/​sysroot/​loop_contracts/​mod.rs	Implements let-chain detection and rewriting.
tests/​cargo-kani/​loop-invariant-let-chain/​src/​lib.rs	Adds six verification harnesses.
tests/​cargo-kani/​loop-invariant-let-chain/​Cargo.toml	Configures the edition-2024 test package.
tests/​cargo-kani/​loop-invariant-let-chain/​expected	Records expected verification results.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Thanks for this. The rewrite is small and puts the chain back verbatim as an if condition, so rustc keeps doing the semantic work. I'm requesting changes for one test that needs 12.8 GB; the other comments are suggestions, plus one question.

What I checked: the PR's test package fails to compile on main and passes here (with the memory caveat below). The expected loop-contract suite still passes (63/63) with current main merged in. Compiled natively, the original while and the rewritten loop produce identical call and Drop traces, covering short-circuit exits, continue, continue 'l, and break 'l. I also ran about 40 extra harnesses through Kani. The positive ones cover bindings flowing between conjuncts, nested chain loops, prev with continue/break/labels, on_entry, loop_modifies/loop_decreases after the invariant, macro_rules!-built chains, and conditions with let only in a nested position, and all of them verify. The negative ones (false post-conditions, a reachable body assertion, a scrutinee side effect that must run, break 'outer, a violated prev invariant, a loop_modifies that omits a written variable) all fail with the expected check. In an edition 2021 crate the chain is rejected the same way native rustc rejects it.

What I'd like changed:

• Blocking: chain_short_circuits needs 12.8 GB in CBMC because it havocs [1u8].into_iter(), so it will fail on runners with less memory. An Option + take() keeps what it tests at 16 MB.
• expected should pin the failing check of chain_invariant_violated, so an unrelated failure can't satisfy it.
• A failing loop_modifies case would cover the attribute carry-over the description mentions.
• I couldn't find an input that makes unwrap_groups do anything. See the inline question.

I agree with keeping the zero-iteration prev case (#4953) out of this PR. I reproduced it on a chain loop: it reports a spurious failure, not a missed one, and the bare while let path already has the same problem.

One small follow-up, optional here: docs/src/reference/experimental/loop-contracts.md:587 still lists while let loops as unsupported. That was already stale before this PR, and with let chains now handled too, it may be a good moment to fix it.