fix: String.Pos.Raw.extract model/runtime mismatch

[Rob23oba]

This PR the model/runtime mismatch in String.Pos.Raw.extract and adds a faster variant (lean_string_utf8_extract_fast) for String.extract that assumes that the positions are valid positions.

Closes #14684

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 87e7204456bfca901bdc724c996030e13c2f80c6 --onto bd97ed8e35639e17a11d1490cbc46d994e7b4513. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-07 20:36:56)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 87e7204456bfca901bdc724c996030e13c2f80c6 --onto c4e6b62c3d955ef20da94310797072f7c4c5fa2b. You can force reference manual CI using the force-manual-ci label. (2026-08-07 20:36:58)

[TwoFX]

Thanks!