feat: add model implementation for UTF8 enc/dec

[digama0]

• Depends on: feat: UTF-8 string validation #3958
• Depends on: fix: don't use modulo for UInt upcasting #3960

This makes the UTF-8 encode and decode functions have lean definitions, so that we can prove properties about them downstream.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-3961 build failed against this PR. (2024-04-20 16:04:46) View Log
• 💥 Mathlib branch lean-pr-testing-3961 build failed against this PR. (2024-04-20 16:25:20) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e4daca8d6b02677115282abff8515a9afb6a2a29 --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-22 04:40:21)

[kim-em]

Could you add a basic test file using test_extern, e.g. starting with

import Lean.Util.TestExtern

instance : BEq ByteArray where
  beq x y := x.data == y.data

test_extern String.toUTF8 "$£€𐍈" -- representative sample of 1-4 byte characters

and then similarly for the other functions?

[kim-em]

LGTM, but I'm not the one to merge changes to UTF8 handling!

[nomeata]

Good stuff, minor comments only.

[nomeata]

Looks good. test_extern improvement can be generalized in a separate PR. Happy to merge if you are happy with this.