Deep recursion with defeq

Stream: lean4

[František Silváši 🦉]

I have a defeq check failing on me with (kernel) deep recursion detected.
Can someone please explain what's happening?

Start with 34367:

theorem minimal₀ {b : Fin (2 ^ 64)} (h : (34367 - b) * 4 % 34367 < (256 :Fin (2 ^ 64)) ) :
  { toFin := 34367 - b } * 4#64 % 34367#64 < 256#64 := h

While 34368 _does_ work:

theorem minimal₁ {b : Fin (2 ^ 64)} (h : (34368 - b) * 4 % 34368 < (256 :Fin (2 ^ 64)) ) :
  { toFin := 34368 - b } * 4#64 % 34368 < 256#64 := h

If we drop the type annotation from b and we keep 34368, it breaks:

theorem minimal₃ (h : (34368 - b) * 4 % 34368 < (256 :Fin (2 ^ 64)) ) :
  { toFin := 34368 - b } * 4#64 % 34368#64 < 256#64 := h

If we keep the type annotation and we increase to 34369, we break:

theorem minimal₂ {b : Fin (2 ^ 64)} (h : (34369 - b) * 4 % 34369 < (256 :Fin (2 ^ 64)) ) :
  { toFin := 34369 - b } * 4#64 % 34369 < 256#64 := h

set_option trace.Meta.isDefEq true gives:
image.png
But I cannot interpret this to my satisfaction.

Is there anything to learn from this beyond 'I happen to be hitting some arbitrary kernel limitations'?

lean4:v4.22.0-rc2

[Robin Arnez]

Kernel errors are hard to debug (there are no traces available) but it seems like it just unfolded everything here (in particular probably % for Fin first, and then maybe * for Fin etc. oh no). If the kernel doesn't know what to do first, it can do some weird stuff, so perhaps just do it for the kernel:

theorem minimal₂ {b : Fin (2 ^ 64)} (h : (34369 - b) * 4 % 34369 < (256 :Fin (2 ^ 64)) ) :
    { toFin := 34369 - b } * 4#64 % 34369 < 256#64 := by
  rw [BitVec.lt_def, BitVec.toNat, BitVec.toNat, ← Fin.lt_def, BitVec.toFin_umod,
    BitVec.toFin_mul]
  exact h

[František Silváši 🦉]

Yeah I can propositionally fix the proofs; the main issue I am running into is that automation times out. simp_all unhappy, grind unhappy, aesop unhappy, etc. - when these kinds of goals arise in bigger contexts.