Fix byte/char index desync in last_two_items_of_path_match

[kasimte]

last_two_items_of_path_match's ::-splitting loop iterated char_indices() (byte
offsets) but guarded with chars().nth(i - 1) (a char count). A multibyte character
in an item path desyncs the two, so the guard fires at the first colon of a :: —
producing a char-boundary panic or a silently dropped path component depending on the
byte layout (both traces are in the issue). Item paths can carry multibyte characters
via unicode identifiers or non-ASCII char const-generics.

The guard now carries the previous character from the loop's own iteration and all
slice bounds stay byte-derived. On pure-ASCII paths byte offsets and char counts
coincide, so the old guard already read exactly the previous character there — the
check is equivalent and behavior is unchanged. Two multibyte regression tests added
to the existing simple_last_two_items_of_path_match module.

Manual test: the original and fixed loops were extracted verbatim into a standalone
binary and compared — identical output on 10 ASCII paths (including this module's
fixture paths and an arrow-bearing form), correct splits on 4 multibyte paths that
previously panicked or mis-split.

Resolves #4827

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

[feliperodri]

Approving — this is a clean fix for a real defect, and the tests earn their place.

Verified rather than read: I extracted the old and new splitting loops into a standalone binary and ran them side by side.

• Both new tests fail on main: café::núm::NonZero::<u32>::unchecked_add panics on the char-boundary slice (0..4), and éa::NonZero::<u32>::unchecked_add silently mis-splits and returns false. So each pins a distinct failure mode, which is what your description claims.
• The existing ASCII fixtures are bit-identical before and after, which is the important non-regression: this function decides every proof_for_contract and stub target.
• Three further multibyte shapes also go from broken to correct: é::… and aé::bé::… panicked, and m::S::<'🦀'>::f and 🦀::S::<u32>::f returned the wrong answer.
• cargo test -p kani-compiler resolve is green on the branch merged with current main (6/6, including your two).

GitHub currently shows this as conflicting, but git merge upstream/main applies cleanly here, so I think that status is stale — a merge or rebase should clear it. Note main has moved to nightly-2026-09-22 since you opened this.

Nothing blocking. Two suggestions inline: a note on why the remaining i - 1 byte arithmetic is still safe, and a third test for the char const-generic shape your description names as the realistic trigger.

One heads-up: #4778 rewrites the same comparison (it adds normalization on both sides of both paths and factors the splitting out). Whichever lands second will need a small rebase, and it would be worth making sure the prev fix survives into the normalized helper rather than being reintroduced from the old code.

[kasimte]

Rebased onto current main, so it should show as mergeable again. The fix itself is unchanged from the commit you approved (53885c9); the rebase just moves it onto the merged base. A second commit addresses your two inline nits (replies in those threads). The only change since your approval is the rebase plus that one commit.

On the merge you flagged: I checked the rebased tree. The ::-splitting loop is byte-identical to main, so the prev fix applies to that same loop. #4778's changes are on the comparison side (normalized_last_two), which I didn't touch. The two are independent, so the fix sits on the live loop and nothing was reintroduced from the old code.

CI runs cargo test -p kani-compiler resolve on the pinned toolchain. Locally I pulled the real function into a standalone binary and ran the three multibyte cases plus an ASCII control and a negative control. All correct. (No CBMC involved; it's a pure string helper.)

The one case this string layer still can't reach, a trait object nested inside another argument, stays tracked in #4830. I left it out to keep this PR focused on the fix.