Escape NUL before decimal digits unambiguously

[muneikh]

A NUL character followed by a decimal digit is currently encoded as \01 (or another digit), which JSON5 does not allow and loads() cannot read back. Use \^@ before decimal digits while retaining \0 elsewhere.

Regression tests round-trip all 10 digits through four quoting modes and both ASCII settings. All 80 new subtests fail before the fix; the full suite passes (80 tests, 100 subtests), and changed-file Ruff lint/format checks pass on Python 3.13. The complete supported Python/OS matrix has not been run.

[dpranke]

Ah, whoops ... I didn't realize your commit message was so terse (just the one line). In the future, please write a description that explains the problem and the fix more fully so that someone reading the change history doesn't necessarily have to go look at the PR or the actual diff to get a more detailed understanding of the change.

I would've written something like:

JSON5 (like Javascript but unlike JSON) allows \0 as an escape sequence in a string as an alternative to \u0000, but only if the following character is not a decimal digit. The current implementation was not enforcing that in json.dumps(), and always using \0 and so json.dumps("\x001') would be encoded as "\01", which was illegal. This fix makes it return "\u00001" in this situation instead (though json.dumps("\x00foo") will still return "\0foo".

Not a big deal, though. Thanks again :).