perf: speed up JSON serialisation

[hargoniX]

This PR speeds up JSON serialisation by using a lookup table to check whether a string needs to be escaped. The approach is based on https://byroot.github.io/ruby/json/2024/12/15/optimizing-ruby-json-part-1.html.

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1100ca6.
There were significant changes against commit 7e8e22e:

  Benchmark                   Metric             Change
  ================================================================
+ big_do                      branch-misses       -2.9%  (-16.2 σ)
+ bv_decide_inequality.lean   branch-misses       -1.2%  (-12.9 σ)
+ bv_decide_mul               branch-misses       -2.6%  (-64.9 σ)
+ bv_decide_realworld         branch-misses       -1.5%  (-15.7 σ)
- const_fold                  task-clock           1.5%   (13.9 σ)
- const_fold                  wall-clock           1.5%   (13.3 σ)
- ilean roundtrip             branches             1.7%  (180.2 σ)
- ilean roundtrip             instructions         1.7%  (118.0 σ)
- qsort                       task-clock           1.9%   (44.4 σ)
- qsort                       wall-clock           1.9%   (43.5 σ)
+ reduceMatch                 task-clock          -3.3%  (-11.9 σ)
+ reduceMatch                 wall-clock          -3.4%  (-12.6 σ)
+ stdlib                      tactic execution    -1.8%  (-40.3 σ)
+ stdlib                      task-clock          -1.2% (-398.6 σ)

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6098d0c.
There were significant changes against commit 7e8e22e:

  Benchmark          Metric         Change
  ====================================================
+ bv_decide_mul      task-clock      -7.8%   (-19.1 σ)
+ bv_decide_mul      wall-clock      -7.9%   (-15.9 σ)
+ ilean roundtrip    branches       -10.1% (-1184.0 σ)
+ ilean roundtrip    instructions   -10.8% (-6250.3 σ)
- ilean roundtrip    maxrss           3.2%    (66.3 σ)
+ rbmap_fbip         task-clock      -4.8%   (-11.1 σ)
+ rbmap_fbip         wall-clock      -4.8%   (-11.4 σ)
- workspaceSymbols   task-clock       2.1%    (11.2 σ)
- workspaceSymbols   wall-clock       2.1%    (11.7 σ)

[hargoniX]

Notably this also brings a speedup of ilean_roundtrip task and wall clock time by about 6.5%. Looking at the data it contains lots of keys like:

{"{\"c\":{\"n\":\"A.Reasonably.Long.Declaration.Name.foobar9\",\"m\":\"A.Reasonably.Long.Module.Name9\"}}":

Of course we notice these keys need to be escaped very early on so they barely penalize us, we could probably be even faster if we could somehow change the data structure such that it doesn't contain these keys.

If we want this fast path I'll look into fixing the sorry.

CC: @mhuisi