fix: improve evalInt?

This PR improves the `evalInt?` function, which is used to evaluate
configuration parameters from the `ToInt` type class.
This PR also adds a new `evalNat?` function for handling the `IsCharP`
type class, and introduces a configuration option:
```
grind (exp := <num>)
```
This option controls the maximum exponent size considered during
expression evaluation. Previously, `evalInt?` used `whnf`,
which could run out of stack space when reducing terms such as `2^1024`.

closes #9427

src/Init/Grind/Tactics.lean

@@ -115,6 +115,11 @@ structure Config where
   When `true` (default: `true`), uses procedure for handling linear integer arithmetic for `Int` and `Nat`.
   -/
   cutsat := true
+  /--
+  Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
+  the characteristic of a ring.
+  -/
+  exp : Nat := 2^20
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean

@@ -8,6 +8,7 @@ import Init.Grind.ToIntLemmas
 import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.EvalNum
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -21,18 +22,6 @@ private def checkDecl (declName : Name) : MetaM Unit := do
   unless (← getEnv).contains declName do
     throwMissingDecl declName
 
--- TODO: improve this function
-private def evalInt? (e : Expr) : MetaM (Option Int) := do
-  let e ← whnfD e
-  match_expr e with
-  | Int.ofNat a =>
-    let some a ← getNatValue? (← whnfD a) | return none
-    return some (a : Int)
-  | Int.negSucc a =>
-    let some a ← getNatValue? (← whnfD a) | return none
-    return some (- (a : Int) - 1)
-  | _ => return none
-
 def getToIntId? (type : Expr) : GoalM (Option Nat) := do
   if let some id? := (← get').toIntIds.find? { expr := type } then
     return id?

src/Lean/Meta/Tactic/Grind/Arith/EvalNum.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind.Arith
+
+/-!
+This module provides functions for evaluating simple `Nat` and `Int` expressions that appear in type classes
+(e.g., `ToInt` and `IsCharP`) used to configure `grind`.
+Using `whnf` for this purpose is too expensive and can exhaust the stack.
+We considered `evalExpr` as an alternative, but it introduces considerable overhead in files with
+ many `grind` calls. We may still use `evalExpr` as a fallback in the future.
+-/
+
+private def checkExp (k : Nat) : OptionT GrindM Unit := do
+  if k > (← getConfig).exp then
+    reportIssue! "exponent {k} exceeds threshold for exponentiation `(exp := {(← getConfig).exp})`"
+    failure
+
+mutual
+private partial def evalNatCore (e : Expr) : OptionT GrindM Nat := do
+  match_expr e with
+  | Nat.zero => return 0
+  | Nat.succ a => return (← evalNatCore a) + 1
+  | Int.toNat a => return (← evalIntCore a).toNat
+  | Int.natAbs a => return (← evalIntCore a).natAbs
+  | HAdd.hAdd _ _ _ inst a b => guard (← isInstHAddNat inst); return (← evalNatCore a) + (← evalNatCore b)
+  | HMul.hMul _ _ _ inst a b => guard (← isInstHMulNat inst); return (← evalNatCore a) * (← evalNatCore b)
+  | HSub.hSub _ _ _ inst a b => guard (← isInstHSubNat inst); return (← evalNatCore a) - (← evalNatCore b)
+  | HDiv.hDiv _ _ _ inst a b => guard (← isInstHDivNat inst); return (← evalNatCore a) / (← evalNatCore b)
+  | HMod.hMod _ _ _ inst a b => guard (← isInstHModNat inst); return (← evalNatCore a) % (← evalNatCore b)
+  | OfNat.ofNat _ _ _ =>
+    let some n ← getNatValue? e | failure
+    return n
+  | HPow.hPow _ _ _ inst a k =>
+    guard (← isInstHPowNat inst)
+    let k ← evalNatCore k
+    checkExp k
+    let a ← evalNatCore a
+    return a ^ k
+  /-
+  Remark: possible improvements
+  - Expand constants
+  - `whnfCore`
+  - `evalExpr` as an expensive fallback.
+  -/
+  | _ => failure
+
+private partial def evalIntCore (e : Expr) : OptionT GrindM Int := do
+  match_expr e with
+  | Neg.neg _ i a => guard (← isInstNegInt i); return - (← evalIntCore a)
+  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddInt i); return (← evalIntCore a) + (← evalIntCore b)
+  | HSub.hSub _ _ _ i a b => guard (← isInstHSubInt i); return (← evalIntCore a) - (← evalIntCore b)
+  | HMul.hMul _ _ _ i a b => guard (← isInstHMulInt i); return (← evalIntCore a) * (← evalIntCore b)
+  | HDiv.hDiv _ _ _ i a b => guard (← isInstHDivInt i); return (← evalIntCore a) / (← evalIntCore b)
+  | HMod.hMod _ _ _ i a b => guard (← isInstHModInt i); return (← evalIntCore a) % (← evalIntCore b)
+  | HPow.hPow _ _ _ i a k =>
+    guard (← isInstHPowInt i)
+    let a ← evalIntCore a
+    let k ← evalNatCore k
+    checkExp k
+    return a ^ k
+  | OfNat.ofNat _ _ _ =>
+    let some n ← getIntValue? e | failure
+    return n
+  | NatCast.natCast _ i a =>
+    let_expr instNatCastInt ← i | failure
+    return (← evalNatCore a)
+  | Nat.cast _ i a =>
+    let_expr instNatCastInt ← i | failure
+    return (← evalNatCore a)
+  /- See comment at `evalNatCore` -/
+  | _ => failure
+
+end
+
+def evalNat? (e : Expr) : GrindM (Option Nat) :=
+  evalNatCore e |>.run
+
+def evalInt? (e : Expr) : GrindM (Option Int) :=
+  evalIntCore e |>.run
+
+end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/Arith/Insts.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Tactic.Grind.Arith.EvalNum
 import Lean.Meta.Tactic.Grind.SynthInstance
 
 namespace Lean.Meta.Grind.Arith
@@ -11,11 +12,10 @@ namespace Lean.Meta.Grind.Arith
 def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Option (Expr × Nat)) := do withNewMCtxDepth do
   let n ← mkFreshExprMVar (mkConst ``Nat)
   let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
-  let some charInst ← synthInstance? charType | pure none
+  let some charInst ← synthInstance? charType | return none
   let n ← instantiateMVars n
-  let some n ← evalNat n |>.run
-    | pure none
-  pure <| some (charInst, n)
+  let some n ← evalNat? n | return none
+  return some (charInst, n)
 
 def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
   let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -174,7 +174,7 @@ attribute [local grind] ofArray.foldl_folder_none_eq_none
 theorem ofArray.mem_of_mem_of_foldl_folder_eq_some
     (h : List.foldl DefaultClause.ofArray.folder (some acc) ls = some acc') (l) (h : l ∈ acc.toList) :
       l ∈ acc'.toList := by
-  induction ls generalizing acc with grind (gen := 7)
+  induction ls generalizing acc with grind
 
 attribute [local grind] ofArray.mem_of_mem_of_foldl_folder_eq_some
 
@@ -187,7 +187,7 @@ theorem ofArray.folder_foldl_mem_of_mem
   | cons x xs ih =>
     simp at hl h
     rw [DefaultClause.ofArray.folder.eq_def] at h -- TODO why doesn't `grind` handle this?
-    rcases hl <;> grind (gen := 7)
+    rcases hl <;> grind
 
 @[inline, local grind]
 def delete (c : DefaultClause n) (l : Literal (PosFin n)) : DefaultClause n where

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/grind_9427.lean

@@ -0,0 +1,38 @@
+example {n} (x y : BitVec n) : x * y = y * x := by
+  grind
+
+example {n} (x y z w : BitVec n) : w = z → x * y - z*w = 0 → z*z = y * x := by
+  grind
+
+example (x y : BitVec 64) : x * y = y * x := by
+  grind
+
+example (x y : BitVec 128) : x * y = y * x := by
+  grind
+
+example (x y : BitVec 128) : x * y = y * x + 2^64 * 2^64 * x := by
+  grind
+
+example (x y : BitVec 256) : x * y = y * x := by
+  grind
+
+example (x y : BitVec 1024) : x * y = y * x := by
+  grind
+
+example (x y : BitVec 1024) : x * y = y * x := by
+  grind -cutsat
+
+example (x y : BitVec 100000) : x * y = y * x := by
+  grind -cutsat
+
+example (x y z : BitVec 100000) : x * y - z*z = 0 → z*z = y * x := by
+  grind -cutsat
+
+/--
+trace: [grind.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
+[grind.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
+-/
+#guard_msgs in
+set_option trace.grind.issues true in
+example (x y : BitVec 1024) : x * y = y * x := by
+  grind (exp := 16)