Lean.Json.parse panics with "Nat.pow exponent is too big" on large exponents

Prerequisites

• 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

Description

Lean.Json.parse crashes the whole program with INTERNAL PANIC: Nat.pow exponent is too big when given a JSON number with a large positive exponent such as 3E9999999993. This is not a recoverable parse error — the panic cannot be caught via the Except result, so the program aborts even though the caller handles both the .ok and .error cases. Since JSON input often comes from untrusted sources, this can be used to crash any program that parses external JSON.

Context

3E9999999993 is in fact valid JSON; Python and JavaScript both parse it to Infinity. Interestingly, an even larger exponent like 3E99999999999999999999999999999 does not crash and is correctly rejected with Invalid JSON: offset 31: exp too large, so only exponents in a specific range trigger the panic.

Steps to Reproduce

import Lean.Data.Json

def main : IO Unit := do
  let input := "3E9999999993"
  match Lean.Json.parse input with
  | .ok _    => IO.println "Valid JSON"
  | .error e => IO.println s!"Invalid JSON: {e}"
  -- This line should always be reached
  IO.println "End of program reached"

Expected behavior: Lean.Json.parse either succeeds or returns an .error, so that "End of program reached" is always printed.

Actual behavior: The program aborts with INTERNAL PANIC: Nat.pow exponent is too big and the final IO.println is never reached.

Versions

Lean 4.30.0, reproduced on latest nightly (live.lean-lang.org).

Additional Information

The cause appears to be in Lean.Json's exponent parsing. In exponent, positive exponents are bounded only by:

if n > USize.size then fail "exp too large"

For 3E9999999993 we have n = 9999999993, which is far below USize.size = 2^64, so the check passes and value.shiftl n is executed:

protected def shiftl : JsonNumber → Nat → JsonNumber
  | ⟨m, e⟩, s => ⟨m * (10 ^ (s - e) : Nat), e - s⟩

This evaluates 3 * 10 ^ 9999999993, and Nat.pow panics because the exponent exceeds its internal limit. (This also explains why a much larger exponent works: it exceeds USize.size and is rejected by the bounds check before shiftl is ever reached.)

The bound n > USize.size is far too loose. It should be checked against a realistic limit — either the actual Nat.pow limit, or, preferably, a much smaller threshold, since a JSON parser should not spend time and memory materializing numbers like 10 ^ 10000 even when Nat.pow could in principle handle them. For comparison, CPython caps the exponent at roughly n = 308.

Start in Lean.Json exponent parsing, particularly exponent and JsonNumber.shiftl, using the provided 3E9999999993 reproduction. Trace how the current USize.size check permits the panic and add coverage for large positive exponents. Done means Lean.Json.parse returns an error or succeeds without aborting, and the caller reaches the final output.