[kasimte]

Resolves #4955.

A for i in a..b loop with a loop contract fails with attempt to subtract with overflow inside Kani's own loop model whenever the range is empty with start > end. <Range<_> as KaniIter>::len computed (self.end - self.start) as usize, an unchecked subtraction, so any empty range underflows; a concrete for _ in 5u32..3 reproduces it, not only symbolic bounds. It is the sole failing check.

This makes the Range model total and correct across the full value range, matching Rust Range semantics:

• Empty ranges (start >= end) have length zero, so len() returns 0 instead of underflowing.
• Spans wider than the element type no longer overflow: len() uses abs_diff (the generate_impl_range! macro also instantiates signed types, where a wide end - start would overflow).
• Spans wider than usize are reported as unsupported rather than truncated. A 128-bit range can hold more than usize::MAX elements; as usize would truncate the span (i128::MIN..0 to 0, 0..2^64 to 0) and verify the loop vacuously. len() widens to u128 and calls kani::unsupported when the span does not fit usize.
• nth uses wrapping_add: start + i as $t overflowed for a signed span wider than T::MAX, so those loops failed in nth one step after the len fix. Since i < len(), the true start + i is representable and wrapping arithmetic computes it exactly.

fn nth(&self, i: usize) -> Self::Item {
    self.start.wrapping_add(i as $t)
}
fn len(&self) -> usize {
    if self.end > self.start {
        let span = self.end.abs_diff(self.start) as u128;
        if span > usize::MAX as u128 {
            crate::kani::unsupported("loop contracts: a `for` loop over a range with more than `usize::MAX` elements");
        }
        span as usize
    } else {
        0
    }
}

assumption() is deliberately left as true: constraining it (self.start <= self.end) was measured ineffective, since len() is computed once from the user's range before the loop, so the overflow is reached independently of the injected kani::assume.

Tests (tests/expected/loop-contract/):

• for_loop_symbolic_range.rs / for_loop_symbolic_range_signed.rs: symbolic Range<usize> / fully-symbolic Range<i8> with start <= end not assumed; the signed one exercises the abs_diff span and the nth wrapping.
• for_loop_range_span_exceeds_usize.rs: spans over usize::MAX (including 0..2^64, which truncates to 0 and verifies vacuously on main) must fail the span check; the expected file pins 0 successes, 3 failures.

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

Large signed spans can truncate to zero when cast to usize, unsoundly modeling non-empty ranges as empty.

Review effort: Balanced
Findings: 1

Open (1)

• Reject signed range spans that overflow usize before casting · New

What changed in this PR

Makes loop-contract range length calculation total for symbolic empty ranges, resolving #4955.

Changes:

• Uses abs_diff for non-empty range lengths.
• Adds a symbolic-range regression test.

File	Description
library/​kani_core/​src/​iter.rs	Updates Range length modeling.
tests/​expected/​loop-contract/​for_loop_symbolic_range.rs	Adds the regression harness.
tests/​expected/​loop-contract/​for_loop_symbolic_range.expected	Records successful verification.

---

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

[feliperodri]

Thanks for tracking this down. Today a contracted for loop over a range with start > end fails inside Kani's own model, even with concrete bounds (5u32..3 reproduces it on main), so the model rejects valid code that is common in practice. The new len matches Range semantics: I checked symbolic usize and u64 ranges against if end > start { end - start } else { 0 }, plus last-iteration and empty-range assertions that must fail, and they do. The fix also covers rev, step_by, chain, enumerate and take over ranges, which all went through the same len.

The span check closes a soundness hole on main as well: for _ in 0u128..(1u128 << 64) { assert!(false) } verifies there today because the as usize cast truncates the length to 0. With this PR it fails.

One gap remains in the signed case. abs_diff gives the right length for signed spans wider than T::MAX, but nth still computes self.start + i as $t, so -100i8..100 or a fully symbolic Range<i32> now fails in nth instead of len. I tried self.start.wrapping_add(i as $t) and it fixes those without hiding any of the negative probes; details inline. I'm requesting changes for this one, since without it the signed half of the change has no effect for wide spans. The other suggestions (unsupported instead of assert!, a test harness that shows the truncation hole) are small.

The PR description still shows the first version of len and says it relies on havoc to reach start > end; worth refreshing before merge since it becomes the squash commit message.

What I ran: the loop-contract expected suite on the PR (66 passed) and on main's iter.rs (the three new tests fail, everything else passes), fmt and clippy, and about 30 probe harnesses across signed and unsigned widths, extremes, empty ranges and adapters. I did not check the core instantiation used by verify-rust-std or a 32-bit target.

[kasimte]

Pushed new changes and refreshed the PR description to the current len (dropped the havoc wording as suggested). Threads resolved.

[feliperodri]

Thanks for the quick turnaround. Everything from the last round is in, and I re-ran each point on 8120f0675 (merged with current main) instead of relying on the replies. Wide signed ranges now iterate correctly through nth, including isize::MIN..isize::MAX and fully symbolic i8/i16/i64 ranges. The over-usize case reports a named unsupported check. Pinning 0 successfully verified harnesses in the span test's .expected file is a good catch: each harness there fails with the same message, so without that line a single harness passing vacuously would still have matched.

I also probed shapes the tests don't cover, and every one agreed with native Range: empty and start == end ranges, ranges at the top and bottom of u128/i128, a span of exactly usize::MAX (accepted) and exactly 2^64 (rejected), rev, step_by, enumerate, take, nested loops, and the new loop_decreases over a symbolic range. Each "must fail" probe failed on the intended assertion and nothing else. One of these turned up another vacuous case on main: for _ in -(1i128 << 63)..(1i128 << 63) { assert!(false) } verifies there today, and fails with this PR.

The one inline suggestion is a post-loop count assertion in for_loop_symbolic_range.rs, so the unsigned test checks the length and not only the absence of an overflow. It doesn't block.

What I ran: the loop-contract expected suite (75 passed on the PR; the three new tests fail with main's iter.rs), fmt and clippy, and about 30 probe harnesses. The red perf-benchcomp job is a symex_runtime jump on hashset/check_contains, a benchmark that doesn't use loop contracts. I did not test a 32-bit target.

[kasimte]

@feliperodri Thanks for the review. I added the native-count assertion you suggested (146b8b2). The new head just needs a CI run-approval.