feat: String.Internal.ugetUTF8Byte (#14388)

This PR adds a `String.Internal.ugetUTF8Byte` function.

For now, this function is just for internal use and does not have a
definition. We might also add a public `String.ugetUTF8Byte` function in
the future which has a definition.

Author: TwoFX

src/Init/Data/String/Bootstrap.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.ByteArray.Bootstrap
+public import Init.Data.UInt.BasicAux
 import Init.Data.Char.Basic
 
 public section
@@ -136,6 +137,13 @@ opaque dropRight (s : String) (n : Nat) : String
 @[extern "lean_string_get_byte_fast"]
 opaque getUTF8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
 
+/--
+Variant of `getUTF8Byte` that takes the byte index as a `USize`, which avoids `Nat` boxing
+in tight loops over the bytes of a string.
+-/
+@[extern "lean_string_uget_byte_fast"]
+opaque ugetUTF8Byte (s : @& String) (n : USize) (h : n.toNat < s.utf8ByteSize) : UInt8
+
 end String.Internal
 
 @[extern "lean_string_mk", expose, deprecated String.ofList (since := "2025-10-30")]

src/include/lean/lean.h

@@ -1218,6 +1218,9 @@ static inline uint8_t lean_string_get_byte_fast(b_lean_obj_arg s, b_lean_obj_arg
   size_t idx = lean_unbox(i);
   return str[idx];
 }
+static inline uint8_t lean_string_uget_byte_fast(b_lean_obj_arg s, size_t i) {
+  return (uint8_t)lean_string_cstr(s)[i];
+}
 
 LEAN_EXPORT lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
 LEAN_EXPORT lean_obj_res lean_string_utf8_next_fast_cold(size_t i, unsigned char c);

tests/elab/utf8英語.lean

@@ -1,5 +1,11 @@
 import Lean.Util.TestExtern
 
+/-!
+Tests UTF-8 encoding and decoding: `String.toUTF8`, `String.ofByteArray`,
+`ByteArray.validateUTF8`, and byte access via `String.getUTF8Byte` and
+`String.Internal.ugetUTF8Byte`.
+-/
+
 deriving instance DecidableEq for ByteArray
 
 test_extern String.toUTF8 ""
@@ -13,7 +19,8 @@ macro "test_extern'" t:term " => " v:term : command =>
 def checkGet (s : String) (arr : Array UInt8) :=
   (List.range s.utf8ByteSize).all fun i =>
     let c := if h : _ then s.getUTF8Byte ⟨i⟩ h else unreachable!
-    c == arr[i]!
+    let c' := if h : _ then String.Internal.ugetUTF8Byte s (USize.ofNat i) h else unreachable!
+    c == arr[i]! && c' == arr[i]!
 
 macro "validate" arr:term " => " "↯" : command =>
   `(test_extern' ByteArray.validateUTF8 $arr => false)