Kernel stack overflow with UInt64 arithmetic

[logical-misha]

Description

The kernel overflows when checking certain proof terms involving UInt64 arithmetic with large literals.

Minimal reproduction

-- Crashes (stack overflow)
theorem crashes (a b : UInt64) (h : a = b) :
  (fun x => if x < x + (-15 : UInt64) then x else 0) a =
  (fun x => if x < x + (-15 : UInt64) then x else 0) b :=
  Eq.ndrec rfl h

-- Works
theorem works (a b : UInt64) (h : a = b) :
  (if a < a + (-15 : UInt64) then a else 0) =
  (if b < b + (-15 : UInt64) then b else 0) :=
  ite_congr (congr (congrArg (· < ·) h) (congrArg (· + -15) h)) (fun _ => h) (fun _ => rfl)

Observation: operand order affects behavior

Swapping operand order avoids the stack overflow (though the proof then fails for a different reason):

-- Does NOT stack overflow (fails with type mismatch instead)
theorem no_overflow (a b : UInt64) (h : a = b) :
  (fun x => if x < (-15 : UInt64) + x then x else 0) a =
  (fun x => if x < (-15 : UInt64) + x then x else 0) b :=
  Eq.ndrec rfl h

The only difference is x + (-15) vs (-15) + x.

How I ran into this

I discovered this issue while using simp with an unfold lemma:

def myCond (x : UInt64) : Prop := x < x + (-15 : UInt64)
instance : Decidable (myCond x) := by unfold myCond; exact inferInstance
@[simp] theorem myCond_unfold : myCond x = (x < x + -15) := rfl

-- Works
theorem works (a b : UInt64) (h : a = b) :
  (if myCond a then a else 0) = (if myCond b then b else 0) := by simp only [h]

-- Crashes (stack overflow)
theorem crashes (a b : UInt64) (h : a = b) :
  (if myCond a then a else 0) = (if myCond b then b else 0) := by simp only [myCond_unfold, h]

Versions

• Lean 4.25.2

Related discussion

Zulip thread