From 56d3de53581aece4f600f7e68ea433274ce9f950 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 27 Jun 2025 11:10:21 +0200 Subject: [PATCH] fix: bv_decide internal error (#9031) This PR fixes a minor usability issue in bv_decide. --- .../Tactic/BVDecide/Frontend/BVDecide/Reify.lean | 12 ++++++++---- tests/lean/run/bv_decide_shift_error.lean | 14 ++++++++++++++ 2 files changed, 22 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/bv_decide_shift_error.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean index 581b79cff4..ce60b7560e 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean +++ b/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 diff --git a/tests/lean/run/bv_decide_shift_error.lean b/tests/lean/run/bv_decide_shift_error.lean new file mode 100644 index 0000000000..aa20fb0f92 --- /dev/null +++ b/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