Deep kernel reduction detected after `simp`

[tobiasgrosser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

The following lean code leads to a deep kernel reduction detected error in Lean.

theorem minimal6 : ∀ (x : BitVec 32),
  ((some x).bind fun x =>
    (if False then none else some (x.sshiftRight 1)).bind fun x' =>
      some (x'.sshiftRight 1))
  = (some x) := by
  intro x
  simp only [Option.some_bind]
  sorry

Steps to Reproduce

1. Copy into lean
2. Observe the red line under the theorem name

Expected behavior: [Clear and concise description of what you expect to happen]

• simp should apply the lemma
• the proof should be marked as sorry with an orange line under the theorem name
• no kernel error

Versions

"4.12.0-nightly-2024-10-15"

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

This issue was reduced by @lfrenot.

[nomeata]

For smaller bitvec sizes it works, and around 12 it just gets very slow. With 8 diagnostics shows:

[kernel] unfolded declarations (max: 133127, num: 26): ▼
  [] Nat.casesOn ↦ 133127 
  [] Nat.mul.match_1 ↦ 66818 
  [] Nat.pred ↦ 66302 
  [] Nat.pow.match_1 ↦ 66302 
  [] Nat.rec ↦ 1803 
  [] BitVec.toNat ↦ 562 
  [] Fin.val ↦ 562 
  [] Int.casesOn ↦ 369 
  [] Int.toNat ↦ 308 
  [] Int.toNat.match_1 ↦ 308 
  [] Nat.brecOn ↦ 40 
  [] Decidable.casesOn ↦ 36 
  [] ite ↦ 34 
  [] HMul.hMul ↦ 34 
  [] Mul.mul ↦ 34 
  [] Nat.mul ↦ 34 
  [] BitVec.toInt ↦ 32 
  [] LT.lt ↦ 32 
  [] Nat.lt ↦ 32 
  [] HShiftRight.hShiftRight ↦ 30 
  [] Int.shiftRight ↦ 30 
  [] Int.shiftRight.match_1 ↦ 30 
  [] HMod.hMod ↦ 26 
  [] Int.emod ↦ 26 
  [] Mod.mod ↦ 26 
  [] Int.emod.match_1 ↦ 26 

I assumed to find some well-founded recursive function somewhere (maybe Nat.div?), but the data refutes that. Looks like Nat.mul is the culprit! But of course there shouldn’t be any computation here at all. Likely https://github.com/leanprover/lean4/pull/4595 will help.

[tobiasgrosser]

I just tried #4595 after merging in 2024-10-31 in https://github.com/opencompl/lean4/pull/32. #4595 indeed fixes the issue. Is there a reason it has not yet been merged? This issue seems to bit us across several of our experiments. 😞

[nomeata]

I think @leodemoura considered it an experiment so far and other issues that he hoped he could fix with it were not fixed, so he's holding back. But if you have evidence that it is useful, then that may change things.

[tobiasgrosser]

I just had a two hour debugging session with @hargoniX (after two days myself alone) and we found another instance that can be resolved with #4595. Unfortunately there is still one more issue in our codebase which I could not track down yet. Certainly, being able to build our codebase with #4595 enabled would be something I would try next on my quest to resolve these bugs.

[nomeata]

Did my secret clone work today? Or who did you debug with?

[tobiasgrosser]

@hargoniX, github outcompletion fooled me.

[tobiasgrosser]

Just to clarify, I can change the global flag for #4595 and did this, but this breaks mathlib so it is not immediately easy to try #4595 at scale.