diff --git a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean
index 47a902b16107..f2aa41992417 100644
--- a/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean
+++ b/src/Lean/Compiler/LCNF/Simp/ConstantFold.lean
@@ -9,6 +9,7 @@ prelude
 public import Init.Data.UInt.Log2
 public import Lean.Compiler.LCNF.InferType
 import Init.Data.UInt.Lemmas
+import Lean.Util.SafeExponentiation
 
 public section
 
@@ -225,6 +226,17 @@ def Folder.mkBinary [Literal α] [Literal β] [Literal γ] (folder : α → β 
   let some arg₂ ← getLit fvarId₂ | return none
   mkLit <| folder arg₁ arg₂
 
+/--
+Folds `Nat.shiftLeft` on literals, unless the runtime cannot evaluate the shift
+(see `canEvalNatShiftLeft`).
+-/
+def Folder.natShiftLeft : Folder := fun args => do
+  let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
+  let some (arg₁ : Nat) ← getLit fvarId₁ | return none
+  let some (arg₂ : Nat) ← getLit fvarId₂ | return none
+  unless canEvalNatShiftLeft arg₁ arg₂ do return none
+  mkLit (arg₁ <<< arg₂)
+
 def Folder.mkBinaryDecisionProcedure [Literal α] [Literal β] {r : α → β → Prop} (folder : (a : α) → (b : β) → Decidable (r a b)) : Folder := fun args => do
   let #[.fvar fvarId₁, .fvar fvarId₂] := args | return none
   let some arg₁ ← getLit fvarId₁ | return none
@@ -530,7 +542,7 @@ def arithmeticFolders : List (Name × Folder) := [
   (``UInt64.div,  Folder.first #[Folder.mkBinary UInt64.div, Folder.rightNeutral (1 : UInt64) (· / ·), Folder.divShift ``UInt64.shiftRight (UInt64.shiftLeft 1 ·) UInt64.log2]),
   (``USize.div,  Folder.first #[Folder.mkBinaryUSize UInt64.div UInt32.div, Folder.rightNeutralUSize 1 1, Folder.divShiftUSize]),
 
-  (``Nat.shiftLeft, Folder.first #[Folder.mkBinary Nat.shiftLeft, Folder.rightNeutral 0 Nat.shiftLeft (by intros; rfl)]),
+  (``Nat.shiftLeft, Folder.first #[Folder.natShiftLeft, Folder.rightNeutral 0 Nat.shiftLeft (by intros; rfl)]),
   (``UInt8.shiftLeft, Folder.first #[Folder.mkBinary UInt8.shiftLeft, Folder.rightNeutral 0 UInt8.shiftLeft @UInt8.shiftLeft_zero]),
   (``UInt16.shiftLeft, Folder.first #[Folder.mkBinary UInt16.shiftLeft, Folder.rightNeutral 0 UInt16.shiftLeft @UInt16.shiftLeft_zero]),
   (``UInt32.shiftLeft, Folder.first #[Folder.mkBinary UInt32.shiftLeft, Folder.rightNeutral 0 UInt32.shiftLeft @UInt32.shiftLeft_zero]),
diff --git a/src/Lean/Meta/Sym/DSimp/EvalGround.lean b/src/Lean/Meta/Sym/DSimp/EvalGround.lean
index 60bdf7b1a243..df45e6c7e634 100644
--- a/src/Lean/Meta/Sym/DSimp/EvalGround.lean
+++ b/src/Lean/Meta/Sym/DSimp/EvalGround.lean
@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.DSimp.DSimpM
 import Lean.Meta.Sym.LitValues
 import Lean.Meta.Offset
+import Lean.Util.SafeExponentiation
 namespace Lean.Meta.Sym.DSimp
 
 /-!
@@ -243,7 +244,27 @@ def evalPow (maxExponent : Nat) (α β : Expr) (a b : Expr) : DSimpM Result :=
 abbrev shift [ShiftLeft α] [ShiftRight α] (left : Bool) (a b : α) : α :=
   if left then a <<< b else a >>> b
 
+/--
+Returns `false` if `a <<< b` has literal arguments that the runtime cannot shift
+(see `canEvalNatShiftLeft`).
+-/
+def canEvalShiftLeft (α β : Expr) (a b : Expr) : Bool := Id.run do
+  let amount : Option Nat := match_expr β with
+    | Nat => getNatValue? b
+    | Fin _ => (fun v => v.val.val) <$> getFinValue? b
+    | BitVec _ => (fun v => v.val.toNat) <$> getBitVecValue? b
+    | _ => none
+  let value : Option Nat := match_expr α with
+    | Nat => getNatValue? a
+    | Int => Int.natAbs <$> getIntValue? a
+    | Fin _ => (fun v => v.val.val) <$> getFinValue? a
+    | BitVec _ => (fun v => v.val.toNat) <$> getBitVecValue? a
+    | _ => none
+  let (some value, some amount) := (value, amount) | return true
+  return canEvalNatShiftLeft value amount
+
 def evalShift (left : Bool) (α β : Expr) (a b : Expr) : DSimpM Result :=
+  if left && !canEvalShiftLeft α β a b then return .rfl else
   if isSameExpr α β then
     match_expr α with
     | Nat => evalBinNat (shift left) a b
@@ -398,6 +419,7 @@ def evalBitVecCast (m a : Expr) : DSimpM Result := do
 def evalBitVecShiftLeftZeroExtend (a m : Expr) : DSimpM Result := do
   let some a := getBitVecValue? a | return .rfl
   let some m := getNatValue? m | return .rfl
+  unless canEvalNatShiftLeft a.val.toNat m do return .rfl
   let e ← share <| toExpr <|a.val.shiftLeftZeroExtend m
   return .step e (done := true)
 
@@ -553,7 +575,11 @@ public def evalGround (config : EvalStepConfig := {}) : DSimproc := fun e =>
     | BitVec _ => evalBitVecNatBool BitVec.getLsbD a i
     | _ => return .rfl
   | BitVec.append _ _ a b => evalBitVecAppend a b
-  | BitVec.shiftLeft _ a i => evalBitVecNatBitVec BitVec.shiftLeft a i
+  | BitVec.shiftLeft w a i =>
+    if canEvalShiftLeft (mkApp (mkConst ``BitVec) w) (mkConst ``Nat) a i then
+      evalBitVecNatBitVec BitVec.shiftLeft a i
+    else
+      return .rfl
   | BitVec.ushiftRight _ a i => evalBitVecNatBitVec BitVec.ushiftRight a i
   | BitVec.sshiftRight _ a i => evalBitVecNatBitVec BitVec.sshiftRight a i
   | BitVec.sshiftRight' _ _ a b => evalBinBitVec' BitVec.sshiftRight' a b
diff --git a/src/Lean/Meta/Sym/Simp/EvalGround.lean b/src/Lean/Meta/Sym/Simp/EvalGround.lean
index 91da4635cf4f..c5dbce475048 100644
--- a/src/Lean/Meta/Sym/Simp/EvalGround.lean
+++ b/src/Lean/Meta/Sym/Simp/EvalGround.lean
@@ -10,6 +10,7 @@ import Init.Sym.Lemmas
 import Lean.Meta.Sym.LitValues
 import Lean.Meta.StringLitProof
 import Lean.Meta.Offset
+import Lean.Util.SafeExponentiation
 namespace Lean.Meta.Sym.Simp
 
 /-!
@@ -283,7 +284,27 @@ def evalPow (maxExponent : Nat) (α β : Expr) (a b : Expr) : SimpM Result :=
 abbrev shift [ShiftLeft α] [ShiftRight α] (left : Bool) (a b : α) : α :=
   if left then a <<< b else a >>> b
 
+/--
+Returns `false` if `a <<< b` has literal arguments that the runtime cannot shift
+(see `canEvalNatShiftLeft`).
+-/
+def canEvalShiftLeft (α β : Expr) (a b : Expr) : Bool := Id.run do
+  let amount : Option Nat := match_expr β with
+    | Nat => getNatValue? b
+    | Fin _ => (fun v => v.val.val) <$> getFinValue? b
+    | BitVec _ => (fun v => v.val.toNat) <$> getBitVecValue? b
+    | _ => none
+  let value : Option Nat := match_expr α with
+    | Nat => getNatValue? a
+    | Int => Int.natAbs <$> getIntValue? a
+    | Fin _ => (fun v => v.val.val) <$> getFinValue? a
+    | BitVec _ => (fun v => v.val.toNat) <$> getBitVecValue? a
+    | _ => none
+  let (some value, some amount) := (value, amount) | return true
+  return canEvalNatShiftLeft value amount
+
 def evalShift (left : Bool) (α β : Expr) (a b : Expr) : SimpM Result :=
+  if left && !canEvalShiftLeft α β a b then return .rfl else
   if isSameExpr α β then
     match_expr α with
     | Nat => evalBinNat (shift left) a b
@@ -663,6 +684,7 @@ def evalBitVecReplicate (i a : Expr) : SimpM Result := do
 def evalBitVecShiftLeftZeroExtend (a m : Expr) : SimpM Result := do
   let some a := getBitVecValue? a | return .rfl
   let some m ← evalNat m |>.run | return .rfl
+  unless canEvalNatShiftLeft a.val.toNat m do return .rfl
   let e ← share <| toExpr <| a.val.shiftLeftZeroExtend m
   return .step e (mkRflBitVec e (a.n + m)) (done := true)
 
@@ -749,7 +771,11 @@ public def evalGround (config : EvalStepConfig := {}) : Simproc := fun e =>
     | BitVec _ => evalBitVecNatBool BitVec.getLsbD a i
     | _ => return .rfl
   | BitVec.append _ _ a b => evalBitVecAppend a b
-  | BitVec.shiftLeft w a i => evalBitVecNatBitVec (mkBitVecType w) BitVec.shiftLeft a i
+  | BitVec.shiftLeft w a i =>
+    if canEvalShiftLeft (mkBitVecType w) (mkConst ``Nat) a i then
+      evalBitVecNatBitVec (mkBitVecType w) BitVec.shiftLeft a i
+    else
+      return .rfl
   | BitVec.ushiftRight w a i => evalBitVecNatBitVec (mkBitVecType w) BitVec.ushiftRight a i
   | BitVec.sshiftRight w a i => evalBitVecNatBitVec (mkBitVecType w) BitVec.sshiftRight a i
   | BitVec.sshiftRight' n _ a b => evalBinBitVec' BitVec.sshiftRight' (mkBitVecType n) a b
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
index 65636bb15060..eea3f0084c7e 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
@@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 public import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Util.SafeExponentiation
 public section
 namespace Lean.Meta.Grind.Arith
 
@@ -39,7 +40,8 @@ The following propagator ensure that `3 &&& mask` is merged with the equivalence
 `mask = 15`.
 -/
 
-def propagateNatBinOp (declName : Name) (congrThmName : Name) (op : Nat → Nat → Nat) (e : Expr) : GoalM Unit := do
+def propagateNatBinOp (declName : Name) (congrThmName : Name) (op : Nat → Nat → Nat) (e : Expr)
+    (canEval : Nat → Nat → Bool := fun _ _ => true) : GoalM Unit := do
   let arity := 6
   unless e.isAppOfArity declName arity do return ()
   unless e.getArg! 0 |>.isConstOf ``Nat do return ()
@@ -50,6 +52,7 @@ def propagateNatBinOp (declName : Name) (congrThmName : Name) (op : Nat → Nat
   let b := e.getArg! (arity - 1) arity
   let bRoot ← getRoot b
   let some k₂ ← getNatValue? bRoot | return ()
+  unless canEval k₁ k₂ do return ()
   let k := op k₁ k₂
   let r ← shareCommon (mkNatLit k)
   internalize r 0
@@ -60,7 +63,7 @@ builtin_grind_propagator propagateNatAnd ↑HAnd.hAnd := propagateNatBinOp ``HAn
 builtin_grind_propagator propagateNatOr ↑HOr.hOr := propagateNatBinOp ``HOr.hOr ``Grind.Nat.or_congr (· ||| ·)
 builtin_grind_propagator propagateNatXOr ↑HXor.hXor := propagateNatBinOp ``HXor.hXor ``Grind.Nat.xor_congr (· ^^^ ·)
 builtin_grind_propagator propagateNatShiftLeft ↑HShiftLeft.hShiftLeft :=
-  propagateNatBinOp ``HShiftLeft.hShiftLeft ``Grind.Nat.shiftLeft_congr (· <<< ·)
+  propagateNatBinOp ``HShiftLeft.hShiftLeft ``Grind.Nat.shiftLeft_congr (· <<< ·) (canEval := canEvalNatShiftLeft)
 builtin_grind_propagator propagateNatShiftRight ↑HShiftRight.hShiftRight :=
   propagateNatBinOp ``HShiftRight.hShiftRight ``Grind.Nat.shiftRight_congr (· >>> ·)
 
diff --git a/src/Lean/Meta/Tactic/Grind/BitVec.lean b/src/Lean/Meta/Tactic/Grind/BitVec.lean
index 29a009eb183a..eab1220fa6af 100644
--- a/src/Lean/Meta/Tactic/Grind/BitVec.lean
+++ b/src/Lean/Meta/Tactic/Grind/BitVec.lean
@@ -11,6 +11,7 @@ import Lean.Meta.LitValues
 import Lean.ToExpr
 import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Util.SafeExponentiation
 public section
 namespace Lean.Meta.Grind
 
@@ -115,11 +116,13 @@ private def binOp (e : Expr) (eval : Expr → Expr → GoalM (Option Expr)) : Go
 
 /-- Table entry for `op : BitVec n → Nat → BitVec n` (shifts, rotations). -/
 @[inline] private def shiftBV (declName : Name) (arity : Nat)
-    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : GoalM Unit := do
+    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr)
+    (canEval : Nat → Nat → Bool := fun _ _ => true) : GoalM Unit := do
   unless e.isAppOfArity declName arity do return ()
   binOp e fun r₁ r₂ => do
     let some ⟨n, v⟩ ← getBitVecValue? r₁ | return none
     let some i ← getNatValue? r₂ | return none
+    unless canEval v.toNat i do return none
     some <$> mkBVLit n (op v i)
 
 /-- Table entry for `op : BitVec n → Nat → Bool` (`getLsbD`, `getMsbD`). -/
@@ -198,7 +201,7 @@ builtin_grind_propagator propagateBVAppend ↑HAppend.hAppend := fun e => do
     some <$> mkBVLit (n₁ + n₂) (v₁ ++ v₂)
 
 builtin_grind_propagator propagateBVShiftLeft ↑BitVec.shiftLeft :=
-  shiftBV ``BitVec.shiftLeft 3 BitVec.shiftLeft
+  shiftBV ``BitVec.shiftLeft 3 BitVec.shiftLeft (canEval := canEvalNatShiftLeft)
 builtin_grind_propagator propagateBVUShiftRight ↑BitVec.ushiftRight :=
   shiftBV ``BitVec.ushiftRight 3 BitVec.ushiftRight
 builtin_grind_propagator propagateBVSShiftRight ↑BitVec.sshiftRight :=
@@ -210,19 +213,20 @@ builtin_grind_propagator propagateBVRotateRight ↑BitVec.rotateRight :=
 
 /-- `x <<< i` and `x >>> i` where the shift amount is a `Nat` or a `BitVec`. -/
 @[inline] private def hShiftBV (declName : Name)
-    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : GoalM Unit := do
+    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr)
+    (canEval : Nat → Nat → Bool := fun _ _ => true) : GoalM Unit := do
   unless e.isAppOfArity declName 6 do return ()
   binOp e fun r₁ r₂ => do
     let some ⟨n, v⟩ ← getBitVecValue? r₁ | return none
-    if let some i ← getNatValue? r₂ then
-      some <$> mkBVLit n (op v i)
-    else if let some ⟨_, w⟩ ← getBitVecValue? r₂ then
-      some <$> mkBVLit n (op v w.toNat)
-    else
-      return none
+    let some i ← (do
+        if let some i ← getNatValue? r₂ then return some i
+        else if let some ⟨_, w⟩ ← getBitVecValue? r₂ then return some w.toNat
+        else return none : GoalM (Option Nat)) | return none
+    unless canEval v.toNat i do return none
+    some <$> mkBVLit n (op v i)
 
 builtin_grind_propagator propagateBVHShiftLeft ↑HShiftLeft.hShiftLeft :=
-  hShiftBV ``HShiftLeft.hShiftLeft (· <<< ·)
+  hShiftBV ``HShiftLeft.hShiftLeft (· <<< ·) (canEval := canEvalNatShiftLeft)
 builtin_grind_propagator propagateBVHShiftRight ↑HShiftRight.hShiftRight :=
   hShiftBV ``HShiftRight.hShiftRight (· >>> ·)
 
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
index 360cd9f6c490..cc88fd5a6834 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Lemmas
+import Lean.Util.SafeExponentiation
 
 public section
 
@@ -81,10 +82,12 @@ Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
 Helper function for reducing bitvector functions such as `shiftLeft` and `rotateRight`.
 -/
 @[inline] private def reduceShift (declName : Name) (arity : Nat)
-    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : SimpM DStep := do
+    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr)
+    (canEval : Nat → Nat → Bool := fun _ _ => true) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some v ← fromExpr? e.appFn!.appArg! | return .continue
   let some i ← Nat.fromExpr? e.appArg! | return .continue
+  unless canEval v.value.toNat i do return .continue
   return .done <| (← toExpr' (op v.value i))
 
 /--
@@ -203,7 +206,7 @@ builtin_dsimproc [simp, seval] reduceGetElem ((_ : BitVec _)[_]) := fun e => do
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
 /-- Simplification procedure for shift left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
-  reduceShift ``BitVec.shiftLeft 3 BitVec.shiftLeft
+  reduceShift ``BitVec.shiftLeft 3 BitVec.shiftLeft (canEval := canEvalNatShiftLeft)
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
 /-- Simplification procedure for unsigned shift right on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceUShiftRight (BitVec.ushiftRight _ _) :=
@@ -215,7 +218,7 @@ builtin_dsimproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
 /-- Simplification procedure for shift left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
-  reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+  reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·) (canEval := canEvalNatShiftLeft)
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
 /-- Simplification procedure for converting a shift with a bit-vector literal into a natural number literal. -/
 builtin_dsimproc [simp, seval] reduceHShiftLeft' ((_ <<< (_ : BitVec _) : BitVec _)) :=
@@ -380,6 +383,7 @@ builtin_dsimproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _
   let_expr shiftLeftZeroExtend _ v m ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some m ← Nat.fromExpr? m | return .continue
+  unless canEvalNatShiftLeft v.value.toNat m do return .continue
   return .done <| (← toExpr' (v.value.shiftLeftZeroExtend m))
 
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
index 7da39fce15b7..429de2426471 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Init.Omega
+import Lean.Util.SafeExponentiation
 
 public section
 
@@ -94,7 +95,15 @@ set_option linter.coreInternal.internalModule false in -- User-facing builtin si
 builtin_dsimproc [simp, seval] reduceXor ((_ ^^^ _ : Fin _)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
 
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
-builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Fin _))  := reduceBin ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Fin _)) := fun e => do
+  unless e.isAppOfArity ``HShiftLeft.hShiftLeft 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  unless canEvalNatShiftLeft v₁.value v₂.value do return .continue
+  if h : v₁.n = v₂.n then
+    return .done <| toExpr (v₁.value <<< (h ▸ v₂.value))
+  else
+    return .continue
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
 builtin_dsimproc [simp, seval] reduceShiftRight ((_ >>> _ : Fin _)) := reduceBin ``HShiftRight.hShiftRight 6 (· >>> ·)
 
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index 81c2ff1a8876..9bfc4a157693 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -99,8 +99,12 @@ set_option linter.coreInternal.internalModule false in -- User-facing builtin si
 builtin_dsimproc [simp, seval] reduceOr ((_ ||| _ : Nat)) := reduceBin ``HOr.hOr 6 (· ||| ·)
 
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
-builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Nat)) :=
-  reduceBin ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Nat)) := fun e => do
+  unless e.isAppOfArity ``HShiftLeft.hShiftLeft 6 do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  unless canEvalNatShiftLeft n m do return .continue
+  return .done <| toExpr (n <<< m)
 
 set_option linter.coreInternal.internalModule false in -- User-facing builtin simprocs are fine
 builtin_dsimproc [simp, seval] reduceShiftRight ((_ >>> _ : Nat)) :=
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index a395af246ba0..b30b4df19f84 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -1002,6 +1002,13 @@ def reducePow (a b : Expr) : MetaM (Option Expr) :=
   trace[Meta.isDefEq.whnf.reduceBinOp] "{a} ^ {b}"
   return mkRawNatLit <| a ^ b
 
+def reduceShiftLeft (a b : Expr) : MetaM (Option Expr) :=
+  withNatValue a fun a =>
+  withNatValue b fun b => OptionT.run do
+  guard (canEvalNatShiftLeft a b)
+  trace[Meta.isDefEq.whnf.reduceBinOp] "{a} <<< {b}"
+  return mkRawNatLit <| a <<< b
+
 def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Expr) := do
   withNatValue a fun a =>
   withNatValue b fun b =>
@@ -1028,7 +1035,7 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
     | ``Nat.land => reduceBinNatOp Nat.land a1 a2
     | ``Nat.lor  => reduceBinNatOp Nat.lor a1 a2
     | ``Nat.xor  => reduceBinNatOp Nat.xor a1 a2
-    | ``Nat.shiftLeft  => reduceBinNatOp Nat.shiftLeft a1 a2
+    | ``Nat.shiftLeft  => reduceShiftLeft a1 a2
     | ``Nat.shiftRight => reduceBinNatOp Nat.shiftRight a1 a2
     | _ => return none
   | _ =>
diff --git a/src/Lean/Util/SafeExponentiation.lean b/src/Lean/Util/SafeExponentiation.lean
index 476983a5900b..0e9077245113 100644
--- a/src/Lean/Util/SafeExponentiation.lean
+++ b/src/Lean/Util/SafeExponentiation.lean
@@ -35,4 +35,14 @@ def checkExponent (n : Nat) (warning := true) : CoreM Bool := do
   else
     return true
 
+/--
+Returns `true` if the runtime can evaluate the natural number shift `a <<< b`.
+
+`Nat.shiftLeft` aborts the whole process ("Nat.shiftl exponent is too big") when `a ≠ 0` and `b`
+does not fit in 32 bits. Procedures that evaluate shifts of literals during elaboration or
+compilation must leave the shift unevaluated in that case.
+-/
+def canEvalNatShiftLeft (a b : Nat) : Bool :=
+  a == 0 || b < UInt32.size
+
 end Lean
diff --git a/tests/elab/15193.lean b/tests/elab/15193.lean
new file mode 100644
index 000000000000..8656a95c9326
--- /dev/null
+++ b/tests/elab/15193.lean
@@ -0,0 +1,187 @@
+/-!
+Evaluating `Nat.shiftLeft` on literals whose shift amount does not fit in 32 bits used to abort the
+process ("Nat.shiftl exponent is too big") in `whnf`, `simp`, `cbv`, `grind` and the compiler.
+Such shifts are now left unevaluated.
+https://github.com/leanprover/lean4/issues/15193
+-/
+
+-- `whnf` (`Meta.reduceNat?`)
+/--
+error: Tactic `rfl` failed: The left-hand side
+  1 <<< 4294967296
+is not definitionally equal to the right-hand side
+  0
+
+⊢ 1 <<< 4294967296 = 0
+-/
+#guard_msgs in
+example : (1 <<< 4294967296 : Nat) = 0 := by rfl
+
+/--
+error: Tactic `decide` proved that the proposition
+  1 <<< 4294967296 = 0
+is false
+-/
+#guard_msgs in
+example : (1 <<< 4294967296 : Nat) = 0 := by decide
+
+/--
+error: Tactic `rfl` failed: The left-hand side
+  1 <<< 4294967296
+is not definitionally equal to the right-hand side
+  0
+
+⊢ 1 <<< 4294967296 = 0
+-/
+#guard_msgs in
+example : ((1 : Int) <<< (4294967296 : Nat)) = 0 := by rfl
+
+-- `simp` simprocs
+/--
+error: `simp` made no progress
+-/
+#guard_msgs in
+example : (1 <<< 4294967296 : Nat) = 0 := by simp only [Nat.reduceShiftLeft]
+
+/--
+error: `simp` made no progress
+-/
+#guard_msgs in
+example : ((1 : Fin (2^40)) <<< (4294967296 : Fin (2^40))) = 0 := by simp only [Fin.reduceShiftLeft]
+
+/--
+error: `simp` made no progress
+-/
+#guard_msgs in
+example : ((1#8) <<< (4294967296 : Nat)) = 0#8 := by simp only [BitVec.reduceHShiftLeft]
+
+/--
+error: `simp` made no progress
+-/
+#guard_msgs in
+example : BitVec.shiftLeftZeroExtend (1#8) 4294967296 = 0 := by
+  simp only [BitVec.reduceShiftLeftZeroExtend]
+
+-- `cbv` (`Sym` ground evaluation)
+/--
+error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example : (1 <<< 4294967296 : Nat) = 0 := by cbv
+
+/--
+error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example : ((1 : Int) <<< (4294967296 : Nat)) = 0 := by cbv
+
+/--
+error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example : ((1#8) <<< (4294967296 : Nat)) = 0#8 := by cbv
+
+/--
+error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example : ((1#64) <<< (4294967296#64)) = 0#64 := by cbv
+
+/--
+error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+example : ((1 : Fin (2^40)) <<< (4294967296 : Fin (2^40))) = 0 := by cbv
+
+-- `grind` propagators
+/--
+error: `grind` failed
+case grind
+x : Nat
+h : x = 4294967296
+h_1 : ¬1 <<< x = 0
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] x = 4294967296
+    [prop] ¬1 <<< x = 0
+    [prop] 1 ≤ 2 ^ x
+    [prop] 1 ≤ x → 2 ∣ 2 ^ x
+  [eqc] True propositions
+    [prop] 2 ∣ 2 ^ x
+    [prop] 1 ≤ x
+    [prop] 1 ≤ 2 ^ x
+    [prop] 1 ≤ x → 2 ∣ 2 ^ x
+  [eqc] False propositions
+    [prop] 1 <<< x = 0
+  [eqc] Equivalence classes
+    [eqc] {x, 4294967296}
+    [eqc] {2 ^ x, 1 <<< x}
+    [eqc] others
+      [eqc] {↑x, ↑4294967296}
+      [eqc] {↑0, 0}
+  [ematch] E-matching patterns
+    [thm] Int.shiftLeft_zero: [@HShiftLeft.hShiftLeft `[Int] `[Nat] `[Int] `[Int.instHShiftLeftNat] #0 `[0]]
+    [thm] Int.zero_shiftLeft: [@HShiftLeft.hShiftLeft `[Int] `[Nat] `[Int] `[Int.instHShiftLeftNat] `[0] #0]
+    [thm] Nat.zero_shiftLeft: [@HShiftLeft.hShiftLeft `[Nat] `[Nat] `[Nat] `[instHShiftLeftOfShiftLeft] `[0] #0]
+    [thm] Nat.shiftLeft_zero: [@HShiftLeft.hShiftLeft `[Nat] `[Nat] `[Nat] `[instHShiftLeftOfShiftLeft] #0 `[0]]
+    [thm] Nat.pow_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
+    [thm] Nat.div_pow_of_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
+    [thm] Nat.dvd_mul_right_of_dvd: [@Dvd.dvd `[Nat] `[Nat.instDvd] #3 #2,
+         @HMul.hMul `[Nat] `[Nat] `[Nat] `[instHMul] #2 #0]
+    [thm] Nat.dvd_mul_left_of_dvd: [@Dvd.dvd `[Nat] `[Nat.instDvd] #3 #2,
+         @HMul.hMul `[Nat] `[Nat] `[Nat] `[instHMul] #0 #2]
+  [cutsat] Assignment satisfying linear constraints
+    [assign] x := 4294967296
+    [assign] 「2 ^ x」 := 2
+    [assign] 「2 ^ x」 := 2
+    [assign] 1 <<< x := 2
+  [ring] Ring `Int`
+    [basis] Basis
+      [_] ↑x + -4294967296 = 0
+[grind] Issues
+  [issue] ring term with unexpected instance
+        2 ^ x
+  [issue] exponent 4294967296 exceeds threshold for exponentiation `(exp := 1048576)`
+  [issue] ring term with unexpected instance
+        2 ^ x
+  [issue] ring term with unexpected instance
+        2 ^ x
+  [issue] ring term with unexpected instance
+        2 ^ x
+  [issue] ring term with unexpected instance
+        2 ^ x
+[grind] Diagnostics
+  [ematch] E-matching Diagnostics
+    [thm] Theorem Instance Count
+      [thm] Nat.div_pow_of_pos ↦ 1
+      [thm] Nat.pow_pos ↦ 1
+-/
+#guard_msgs in
+example (x : Nat) (h : x = 4294967296) : (1 <<< x : Nat) = 0 := by grind
+
+/--
+
+-/
+#guard_msgs in
+example (x : Nat) (h : x = 4294967296) : ((1#8) <<< x) = 0#8 := by grind
+
+-- compiler constant folding
+def shiftTooFar : Nat := 1 <<< 4294967296
+
+-- Shifts that the runtime can evaluate are still evaluated.
+example : (1 <<< 100 : Nat) = 2 ^ 100 := by rfl
+example : (1 <<< 100 : Nat) = 1267650600228229401496703205376 := by simp
+example : (1 <<< 100 : Nat) = 1267650600228229401496703205376 := by cbv
+example : (0 <<< 4294967296 : Nat) = 0 := by simp
+example : (0 <<< 4294967296 : Nat) = 0 := by decide