fix: behavior of String.next (#9449)

This PR fix the behavior of `String.next` on the scalar boundary (`2 ^
63 - 1` on 64-bit platforms).

Closes #9440

src/runtime/object.cpp

@@ -2221,9 +2221,9 @@ extern "C" LEAN_EXPORT uint32 lean_string_utf8_get_bang(b_obj_arg s, b_obj_arg i
 
 /* The reference implementation is:
    ```
-   def next (s : @& String) (p : @& Pos) : Ppos :=
-   let c := get s p in
-   p + csize c
+   def next (s : @& String) (p : @& Pos) : Pos :=
+     let c := get s p
+     p + c
    ```
 */
 extern "C" LEAN_EXPORT obj_res lean_string_utf8_next(b_obj_arg s, b_obj_arg i0) {
@@ -2234,8 +2234,8 @@ extern "C" LEAN_EXPORT obj_res lean_string_utf8_next(b_obj_arg s, b_obj_arg i0)
     usize i = lean_unbox(i0);
     char const * str = lean_string_cstr(s);
     usize size       = lean_string_size(s) - 1;
-    /* `csize c` is 1 when `i` is not a valid position in the reference implementation. */
-    if (i >= size) return lean_box(i+1);
+    /* `c.utf8ByteSize` is 1 when `i` is not a valid position in the reference implementation. */
+    if (i >= size) return lean_usize_to_nat(i+1);
     unsigned c = static_cast<unsigned char>(str[i]);
     if ((c & 0x80) == 0)    return lean_box(i+1);
     if ((c & 0xe0) == 0xc0) return lean_box(i+2);

tests/lean/run/string.lean

@@ -147,3 +147,22 @@ Behavior of `String.prev` (`lean_string_utf8_prev`) in special cases (see issue
 #test "L∃∀N".prev ⟨2 ^ 128⟩ = ⟨2 ^ 128 - 1⟩ -- large non-scalar
 #test "L∃∀N".prev ⟨2 ^ 63⟩ = ⟨2 ^ 63 - 1⟩ -- scalar boundary (64-bit)
 #test "L∃∀N".prev ⟨2 ^ 31⟩ = ⟨2 ^ 31 - 1⟩ -- scalar boundary (32-bit)
+
+/-!
+Behavior of `String.next` (`lean_string_utf8_next`) in special cases (see issue #9440).
+-/
+
+#test "L∃∀N".next ⟨0⟩ = ⟨1⟩
+#test "L∃∀N".next ⟨1⟩ = ⟨4⟩
+#test "L∃∀N".next ⟨2⟩ = ⟨3⟩
+#test "L∃∀N".next ⟨3⟩ = ⟨4⟩
+#test "L∃∀N".next ⟨4⟩ = ⟨7⟩
+#test "L∃∀N".next ⟨5⟩ = ⟨6⟩
+#test "L∃∀N".next ⟨6⟩ = ⟨7⟩
+#test "L∃∀N".next ⟨7⟩ = ⟨8⟩
+#test "L∃∀N".next ⟨8⟩ = ⟨9⟩
+#test "L∃∀N".next ⟨9⟩ = ⟨10⟩
+#test "L∃∀N".next ⟨99⟩ = ⟨100⟩ -- small value out of bounds
+#test "L∃∀N".next ⟨2 ^ 128 - 1⟩ = ⟨2 ^ 128⟩ -- large non-scalar
+#test "L∃∀N".next ⟨2 ^ 63 - 1⟩ = ⟨2 ^ 63⟩ -- scalar boundary (64-bit)
+#test "L∃∀N".next ⟨2 ^ 31 - 1⟩ = ⟨2 ^ 31⟩ -- scalar boundary (32-bit)