fix: do not evaluate Nat left shifts the runtime cannot perform

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]),

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

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

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 (· >>> ·)
 

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 (· >>> ·)
 

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

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 (· >>> ·)
 

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)) :=

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
   | _ =>

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