`Nat.shiftLeft` by 2^32 or more crashes Lean in `rfl`, `decide`, `simp`, `cbv`, `grind` and the compiler

Run the minimal reproduction examples first to confirm the panic, then read Lean.Meta.reduceNat? in src/Lean/Meta/WHNF.lean and the listed shift call sites in the simproc, evaluator, Grind, and LCNF constant-folder files. Done means oversized nonzero shifts no longer terminate Lean, while ordinary shifts such as 1 << 1000 still evaluate.

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
  (You can also use the settings there to switch to “Lean nightly”)

Description

Several elaborator and compiler procedures evaluate Nat.shiftLeft on literals without checking the shift amount. The runtime's lean_nat_shiftl calls lean_internal_panic("Nat.shiftl exponent is too big") when the shifted value is nonzero and the shift amount does not fit in 32 bits, so a one-line file terminates the whole Lean process (and with it the language server or lake build).

The kernel no longer has this problem: it now refuses such shifts with a kernel exception. Nat.pow is also already protected on the elaborator side by checkExponent. Nat.shiftLeft is not guarded at these call sites:

• Lean.Meta.reduceNat? (src/Lean/Meta/WHNF.lean): reached by rfl, decide, whnf
• Nat.reduceShiftLeft simproc (src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean): simp
• evalShift in src/Lean/Meta/Sym/Simp/EvalGround.lean and src/Lean/Meta/Sym/DSimp/EvalGround.lean (Nat, Int and BitVec shifts): cbv, bv_decide normalization
• propagateNatShiftLeft (src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean): grind
• the LCNF constant folder for Nat.shiftLeft (src/Lean/Compiler/LCNF/Simp/ConstantFold.lean): compiling a definition

Steps to Reproduce

Each of the following files, on its own, crashes Lean:

example : (1 <<< 4294967296 : Nat) = 0 := by rfl

example : (1 <<< 4294967296 : Nat) = 0 := by decide

example : (1 <<< 4294967296 : Nat) = 0 := by simp

example : (1 <<< 4294967296 : Nat) = 0 := by cbv

example : ((1 : Int) <<< (4294967296 : Nat)) = 0 := by cbv

example : ((1#8) <<< (4294967296 : Nat)) = 0#8 := by cbv

example (x : Nat) (h : x = 4294967296) : (1 <<< x : Nat) = 0 := by grind

def f : Nat := 1 <<< 4294967296

Expected behavior: The shift is left unevaluated (or an error or warning is reported, as for 2 ^ 4294967296), and Lean keeps running.

Actual behavior: The process exits with INTERNAL PANIC: Nat.shiftl exponent is too big.

Versions

4.36.0-nightly-2026-09-16 (also reproduced on v4.35.0-rc2 and v4.32.0-rc1)
Linux 6.17.0 aarch64

Additional Information

2 ^ 4294967296 does not crash: checkExponent logs "exponent 4294967296 exceeds the threshold 256" instead. For shifts, the exponentiation threshold would be too restrictive, since evaluating 1 <<< 1000 is cheap and works today. The runtime's actual limit is the one that matters: skip evaluation when the value is nonzero and the shift amount is at least 2^32.

I plan to open a PR implementing that guard at the call sites above. An AI assistant (Claude) found and reduced this bug and drafted this report; each reproduction above was run on the listed versions.

Impact

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