fix: bv_decide internal error (#9031)

This PR fixes a minor usability issue in bv_decide.

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -47,9 +47,11 @@ where
       binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr origExpr
     | Complement.complement _ _ innerExpr =>
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr origExpr
-    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
+    | HShiftLeft.hShiftLeft α β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
-      if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
+      let_expr BitVec wExpr := α | return none
+      if (← getNatValue? wExpr).isSome && distance?.isSome then
+        throwError "internal error: constant shift should have been eliminated."
       let_expr BitVec _ := β | return none
       shiftReflection
         distanceExpr
@@ -58,9 +60,11 @@ where
         ``BVExpr.shiftLeft
         ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
         origExpr
-    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
+    | HShiftRight.hShiftRight α β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
-      if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
+      let_expr BitVec wExpr := α | return none
+      if (← getNatValue? wExpr).isSome && distance?.isSome then
+        throwError "internal error: constant shift should have been eliminated."
       let_expr BitVec _ := β | return none
       shiftReflection
         distanceExpr

tests/lean/run/bv_decide_shift_error.lean

@@ -0,0 +1,14 @@
+import Std.Tactic.BVDecide
+
+-- This previously was an internal error due to the constant shift not being eliminated because
+-- of the non constant width shift, now it's an error.
+
+/--
+error: The prover found a potentially spurious counterexample:
+- It abstracted the following unsupported expressions as opaque variables: [x <<< 1 == x]
+Consider the following assignment:
+x <<< 1 == x = false
+-/
+#guard_msgs in
+example (x : BitVec w) : x <<< (1 : Nat) = x := by
+  bv_decide