perf: make kernel reduction of `String.toList` linear

This PR makes kernel reduction of `String.toList` on a string literal take time linear in its length. Previously, `decide +kernel` on `s.toList.length = 400` took about 8 s, and long literals hit the kernel's recursion limit.

`String.toList` is now defined with `String.Internal.utf8DecodeList`, a structurally recursive UTF-8 decoder on `List UInt8`. It replaces `ByteArray.utf8Decode?`, whose `size`, indexing and `push` operations each walk a list in the kernel. `List.utf8Encode` now wraps the encoded byte list directly instead of building it with one `ByteArray.push` per byte. It is `noncomputable`, so compiled code is unchanged. Proofs that unfold `List.utf8Encode` should use the new `List.utf8Encode_eq_toByteArray`.

Closes #16012

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>