Json.parse does not handle surrogate pairs in string literals

[eric-wieser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The Json parser does not correctly handle surrogate pairs

Context

ASCII-encoded JSON (the default) serialized with Python is sometimes corrupted when loaded in Lean.

Steps to Reproduce

1. Run the following:

import Lean

-- ok: "\u0000\u0000"
#eval Lean.Json.parse "\"\\ud80f\\udf00\""

2. Compare to Python

>>> import json
>>> json.loads("\"\\ud80f\\udf00\"")
'\U00013f00'

Expected behavior: The escaped UTF-16 surrogate pair should be combined into a single unicode codepoint. From the JSON RFC:

To escape an extended character that is not in the Basic Multilingual Plane, the character is represented as a twelve-character sequence, encoding the UTF-16 surrogate pair. So, for example, a string containing only the G clef character (U+1D11E) may be represented as "\uD834\uDD1E".

Actual behavior: The characters become null.

Versions

4.12.0-rc1

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.