From 79df09db8f734f9ce013940e6e4bd4795eed09c5 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Tue, 22 Sep 2026 16:11:19 -0400
Subject: [PATCH 1/2] Fix byte/char index desync in
 last_two_items_of_path_match

---
 kani-compiler/src/kani_middle/resolve.rs | 29 ++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index ef38b1f3adc8..a6745b517ce5 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -916,6 +916,10 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str)
     let mut angle_bracket_depth = 0;
     let mut parts = Vec::new();
     let mut part_start = 0;
+    // `i` is a byte offset, so the previous character is carried from the last
+    // iteration rather than re-counted with `chars().nth` (a char count, which
+    // desyncs on multibyte paths and made the slices below panic or mis-split).
+    let mut prev = None;
 
     for (i, c) in item_path.char_indices() {
         match c {
@@ -925,10 +929,7 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str)
             '>' => {
                 angle_bracket_depth -= 1;
             }
-            ':' if angle_bracket_depth == 0
-                && i > 0
-                && item_path.chars().nth(i - 1) == Some(':') =>
-            {
+            ':' if angle_bracket_depth == 0 && prev == Some(':') => {
                 if part_start < i {
                     parts.push(&item_path[part_start..i - 1]);
                 }
@@ -936,6 +937,7 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str)
             }
             _ => {}
         }
+        prev = Some(c);
     }
     parts.push(&item_path[part_start..]);
 
@@ -1247,5 +1249,24 @@ mod tests {
             assert!(last_two_items_of_path_match(&item_path, "::<(u32,u64),A>", name));
             assert!(!last_two_items_of_path_match(&item_path, "::<u32,u64,A>", name));
         }
+
+        #[test]
+        fn multibyte_path_char_boundary() {
+            // A multibyte char before the first `::` used to desync the splitter's
+            // byte/char indexing (char-boundary panic on the part slice).
+            let generic_args = "::<u32>";
+            let name = "unchecked_add";
+            let item_path = format!("café::núm::NonZero{generic_args}::{name}");
+            assert!(last_two_items_of_path_match(&item_path, generic_args, name))
+        }
+
+        #[test]
+        fn multibyte_path_component_kept() {
+            // Same desync could instead silently drop a path component.
+            let generic_args = "::<u32>";
+            let name = "unchecked_add";
+            let item_path = format!("éa::NonZero{generic_args}::{name}");
+            assert!(last_two_items_of_path_match(&item_path, generic_args, name))
+        }
     }
 }

From b6559d3cc3fea693225ae6cb5e52ed464c4a0a93 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Thu, 24 Sep 2026 12:36:22 -0400
Subject: [PATCH 2/2] Address review: boundary-safety comment + char
 const-generic test

---
 kani-compiler/src/kani_middle/resolve.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index a6745b517ce5..7c24320940e6 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -931,6 +931,8 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str)
             }
             ':' if angle_bracket_depth == 0 && prev == Some(':') => {
                 if part_start < i {
+                    // `i - 1` is the first colon of `::` (ASCII, one byte), so this
+                    // byte slice always ends on a char boundary.
                     parts.push(&item_path[part_start..i - 1]);
                 }
                 part_start = i + 1;
@@ -1268,5 +1270,16 @@ mod tests {
             let item_path = format!("éa::NonZero{generic_args}::{name}");
             assert!(last_two_items_of_path_match(&item_path, generic_args, name))
         }
+
+        #[test]
+        fn multibyte_path_char_const_generic() {
+            // The description's realistic trigger: a non-ASCII `char` const-generic
+            // puts a multibyte char inside the generic-args part (not a leading
+            // component), which desynced the old byte/char guard.
+            let generic_args = "::<'🦀'>";
+            let name = "f";
+            let item_path = format!("m::S{generic_args}::{name}");
+            assert!(last_two_items_of_path_match(&item_path, generic_args, name))
+        }
     }
 }