Print huge natVal literals in sub-quadratic time

[lordwilsonDev]

Problem

natVal literals are printed with s!"{i}", i.e. Nat.repr, which converts one digit at a time with a division of the whole number: quadratic in the number of digits. A proof term that contains a literal with millions of digits makes the exporter sit at 100% CPU with no output (sample shows Nat.reprFast → toDigitsCore → __gmpz_tdiv_q/_r → __gmpn_divrem_1).

Real example: results_eliahou_theorem_1_1 in tangentstorm/eliahou-collatz-bounds @ db804ce6305ea99a817f067869607f8b677d895a (Lean v4.28.0, lake env lean4export Results -- results_eliahou_theorem_1_1). The closure contains literals of up to 25,628,966 digits (81 literals over 50 digits). Unpatched: the output stops at 71 MB and then makes no progress for 8+ minutes of CPU (I killed it; I have not shown it never finishes). It looks like a hang, and I first misdiagnosed it as a memoization problem until I sampled it.

Change

natToDecStr splits the number by 10^(18·2^k) recursively, so GMP's sub-quadratic division does the work, and pads the low parts to a fixed width. The output is identical to Nat.repr. Only the natVal case in dumpExprAux changes (+26/−1 lines, Export.lean only).

Evidence

• With the patch the same export finishes in about 60–120 s: 187,326,147 bytes, complete.
• The patched output is byte-identical to the unpatched output over the 71,147,000 bytes the unpatched exporter reached.
• Equivalence test: natToDecStr n == toString n on ~3,000 pseudo-random numbers (up to 40th powers of 64-bit values) plus edge cases (0, 10^18−1, 10^18, 10^36±1, 2^200, 2^5000, 10^100−1): 0 mismatches.
• The resulting export was type-checked by nanoda (17,464 declarations, no errors) using a companion patch for nanoda's own (also quadratic) decimal parser — see Parse huge decimal nat literals in sub-quadratic time ammkrn/nanoda_lib#36.

What I did not test

I built and tested this on Lean v4.28.0 and v4.34.0. master is on v4.35.0-rc2, which I could not install locally (disk); the patch applies cleanly to master and uses only Array, String.pushn, Nat division/modulo and Id.run, but CI is the first real build on that toolchain. If a newer Lean's Nat.repr is already sub-quadratic for big numbers, this may be unnecessary — I have not checked.

🤖 Generated with Claude Code

[nomeata]

Related issue: leanprover/lean4#5771