fix: normalization of bitvector literals in grind (#14371)

This PR fixes two bugs in `grind` caused by non-normalized bitvector
literals. `BitVec.ofNatLT` literals and out-of-range `OfNat.ofNat`
literals (e.g., `(17 : BitVec 4)`) were not reduced to the `OfNat.ofNat`
normal form used by `grind`, so two representations of the same value
were treated as distinct values, and `grind` produced invalid proofs
rejected by the kernel:

```lean
example (x : BitVec 4) (_h1 : x = BitVec.ofNatLT 1 (by decide)) (_h2 : x = 1#4) : True := by
  grind -- kernel error before this PR
```

Author: leodemoura

src/Init/Data/BitVec/Lemmas.lean

@@ -336,7 +336,6 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
   simp [getMsbD, getLsbD]
 
-@[grind =]
 theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
   eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
 

src/Init/Grind/Norm.lean

@@ -234,5 +234,7 @@ init_grind_norm
   -- Semiring
   Semiring.one_mul Semiring.mul_one
   Semiring.zero_mul Semiring.mul_zero
+  -- Bitvectors
+  BitVec.ofNatLT_eq_ofNat
 
 end Lean.Grind

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -258,6 +258,19 @@ builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
     -/
     return .done (← mkNumeral (mkApp (mkConst ``BitVec) n) v)
 
+/--
+Simplification procedure for ensuring `OfNat.ofNat` bitvector literals are normalized.
+For example, `(17 : BitVec 4)` is reduced to `(1 : BitVec 4)` when `bitVecOfNat := false`,
+and to `1#4` when `bitVecOfNat := true`.
+-/
+builtin_dsimproc [simp, seval] isValue ((OfNat.ofNat _ : BitVec _)) := fun e => do
+  let_expr OfNat.ofNat _ m _ ← e | return .continue
+  let some m ← Nat.fromExpr? m | return .continue
+  let some ⟨_, v⟩ ← getBitVecValue? e | return .continue
+  if v.toNat == m && !(← Simp.getConfig).bitVecOfNat then
+    return .done e -- already normalized; `OfNat.ofNat` is the normal form when `bitVecOfNat := false`
+  return .done (← toExpr' v)
+
 /-- Simplification procedure for `=` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceEq  (( _ : BitVec _) = _)  := reduceBinPred ``Eq 3 (. = .)
 /-- Simplification procedure for `≠` on `BitVec`s. -/

tests/elab/grind_bitvec_ofnat_out_of_range.lean

@@ -0,0 +1,24 @@
+/-!
+Tests that `grind` reduces out-of-range `OfNat.ofNat` bitvector literals. The `grind` normal
+form for bitvector literals is `OfNat.ofNat` (see #14370). If a literal whose value exceeds
+`2^w` (e.g. `(17 : BitVec 4)`) is not reduced modulo `2^w`, then `(17 : BitVec 4)` and `1#4`
+are treated as two distinct interpreted values.
+-/
+
+/--
+This example used to expose the bug: merging the two representations of the same value made
+`grind` produce an invalid inconsistency proof rejected by the kernel.
+-/
+example (x : BitVec 4) (_h1 : x = (17 : BitVec 4)) (_h2 : x = 1#4) : True := by
+  grind
+
+example (x : BitVec 4) (h : x = (17 : BitVec 4)) : x = 1#4 := by
+  grind
+
+/-- Width-zero edge case: every literal must reduce to `0`. -/
+example (x : BitVec 0) (h : x = (1 : BitVec 0)) : x = 0#0 := by
+  grind
+
+/-- `grind` must still detect genuine disequalities involving out-of-range literals. -/
+example (x : BitVec 4) (h1 : x = (17 : BitVec 4)) (h2 : x = 2#4) : False := by
+  grind

tests/elab/grind_bitvec_ofnatlt_lit.lean

@@ -0,0 +1,29 @@
+/-!
+Tests that `grind` handles `BitVec.ofNatLT` literals correctly. The `grind` normal form for
+bitvector literals is `OfNat.ofNat` (see #14370), but `BitVec.ofNatLT` literals are not
+normalized to this form. Thus, `BitVec.ofNatLT 1 h : BitVec 4` and `1#4` are treated as two
+distinct interpreted values.
+-/
+
+/--
+This example exposes the bug: merging the two representations of the same value makes `grind`
+produce an invalid inconsistency proof rejected by the kernel.
+-/
+example (x : BitVec 4) (_h1 : x = BitVec.ofNatLT 1 (by decide)) (_h2 : x = 1#4) : True := by
+  grind
+
+/--
+The following two examples are not unsound, just incomplete: `grind` cannot connect the two
+representations. They should pass once `ofNatLT` literals are normalized.
+-/
+
+example (x : BitVec 4) (h : x = BitVec.ofNatLT 1 (by decide)) : x = 1#4 := by
+  grind
+
+open BitVec in
+example (x : BitVec 4) (h : x = 1#'(by decide)) : x = 1#4 := by
+  grind
+
+/-- `grind` must still detect genuine disequalities involving `ofNatLT` literals. -/
+example (x : BitVec 4) (h1 : x = BitVec.ofNatLT 1 (by decide)) (h2 : x = 2#4) : False := by
+  grind