From 337685a38a3de272cf70e2b4331df389746683cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 13 May 2025 20:32:12 +0200
Subject: [PATCH] feat: bv_decide support for BitVec.reverse (#8323)

This PR adds support for bv_decide to understand `BitVec.reverse` in
bitblasting.
---
 .../BVDecide/Frontend/BVDecide/Reflect.lean   |  1 +
 .../BVDecide/Frontend/BVDecide/Reify.lean     |  2 +
 .../Frontend/Normalize/Structures.lean        |  4 +-
 .../BVDecide/Bitblast/BVExpr/Basic.lean       |  8 ++++
 .../Bitblast/BVExpr/Circuit/Impl/Expr.lean    | 14 +++++--
 .../Circuit/Impl/Operations/Reverse.lean      | 34 ++++++++++++++++
 .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean  |  6 +++
 .../Circuit/Lemmas/Operations/Reverse.lean    | 39 +++++++++++++++++++
 src/Std/Tactic/BVDecide/Reflect.lean          |  4 ++
 tests/lean/run/bv_bitwise.lean                |  6 +++
 10 files changed, 113 insertions(+), 5 deletions(-)
 create mode 100644 src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Reverse.lean
 create mode 100644 src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Reverse.lean

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index 71e2ba8186..ac607cdd7f 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -39,6 +39,7 @@ instance : ToExpr BVUnOp where
     | .rotateLeft n => mkApp (mkConst ``BVUnOp.rotateLeft) (toExpr n)
     | .rotateRight n => mkApp (mkConst ``BVUnOp.rotateRight) (toExpr n)
     | .arithShiftRightConst n => mkApp (mkConst ``BVUnOp.arithShiftRightConst) (toExpr n)
+    | .reverse => mkConst ``BVUnOp.reverse
   toTypeExpr := mkConst ``BVUnOp
 
 instance : ToExpr (BVExpr w) where
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
index 4de8aa46ed..d0898d236b 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -182,6 +182,8 @@ where
       let some rhs ← goOrAtom rhsExpr | return none
       addCondLemmas discr atom lhs rhs discrExpr origExpr lhsExpr rhsExpr
       return some atom
+    | BitVec.reverse _ innerExpr =>
+      unaryReflection innerExpr .reverse ``Std.Tactic.BVDecide.Reflect.BitVec.reverse_congr origExpr
     | _ => return none
 
   /--
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
index ad4c9b71b5..a40e78b5e9 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
@@ -46,8 +46,7 @@ def addStructureSimpLemmas (simprocs : Simprocs) (lemmas : SimpTheoremsArray) :
     let lemmaName := mkInjectiveEqTheoremNameFor ctorName
     if (← getEnv).find? lemmaName |>.isSome then
       trace[Meta.Tactic.bv] m!"Using injEq lemma: {lemmaName}"
-      let statement ← mkConstWithLevelParams lemmaName
-      lemmas ← lemmas.addTheorem (.decl lemmaName) statement
+      lemmas ← lemmas.addTheorem (.decl lemmaName) (mkConst lemmaName)
     let fields := (getStructureInfo env const).fieldNames.size
     let numParams := constInfo.numParams
     for proj in [0:fields] do
@@ -71,6 +70,7 @@ partial def structuresPass : Pass where
       else
         let some const := (← instantiateMVars decl.type).getAppFn.constName? | return false
         return interesting.contains const
+
     match goals with
     | [goal] => postprocess goal
     | _ => throwError "structures preprocessor generated more than 1 goal"
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index 63c57eb974..4c6e5e715b 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -135,6 +135,10 @@ inductive BVUnOp where
   constant `Nat` value.
   -/
   | arithShiftRightConst (n : Nat)
+  /--
+  Reverse the bits in a bitvector.
+  -/
+  | reverse
   deriving Hashable, DecidableEq
 
 namespace BVUnOp
@@ -144,6 +148,7 @@ def toString : BVUnOp → String
   | rotateLeft n => s!"rotL {n}"
   | rotateRight n => s!"rotR {n}"
   | arithShiftRightConst n => s!">>a {n}"
+  | reverse => "rev"
 
 instance : ToString BVUnOp := ⟨toString⟩
 
@@ -155,6 +160,7 @@ def eval : BVUnOp → (BitVec w → BitVec w)
   | rotateLeft n => (BitVec.rotateLeft · n)
   | rotateRight n => (BitVec.rotateRight · n)
   | arithShiftRightConst n => (BitVec.sshiftRight · n)
+  | reverse =>  BitVec.reverse
 
 @[simp] theorem eval_not : eval .not = ((~~~ ·) : BitVec w → BitVec w) := by rfl
 
@@ -170,6 +176,8 @@ theorem eval_rotateRight : eval (rotateRight n) = ((BitVec.rotateRight · n) : B
 theorem eval_arithShiftRightConst : eval (arithShiftRightConst n) = (BitVec.sshiftRight · n : BitVec w → BitVec w) := by
   rfl
 
+@[simp] theorem eval_reverse : eval .reverse = (BitVec.reverse : BitVec w → BitVec w) := by rfl
+
 end BVUnOp
 
 /--
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
index 42b4252a6c..24eb087117 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -18,6 +18,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateRight
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
@@ -193,10 +194,10 @@ where
       | .not =>
         let res := bitblast.blastNot eaig evec
         have := by
-          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.map)
+          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastNot)
           dsimp only at heaig
           omega
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := AIG.RefVec.map) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastNot) ..)⟩
       | .rotateLeft distance =>
         let res := bitblast.blastRotateLeft eaig ⟨evec, distance⟩
         have := by
@@ -218,6 +219,13 @@ where
           dsimp only at heaig
           assumption
         ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩
+      | .reverse =>
+        let res := bitblast.blastReverse eaig evec
+        have := by
+          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReverse)
+          dsimp only at heaig
+          omega
+        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastReverse) ..)⟩
     | .append lhs rhs h =>
       let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache
       let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache
@@ -329,7 +337,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
         · apply Nat.le_trans <;> assumption
   · next op expr =>
     match op with
-    | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. =>
+    | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse =>
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq]
       have := (goCache aig expr cache).result.property
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Reverse.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Reverse.lean
new file mode 100644
index 0000000000..f890a921bb
--- /dev/null
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Reverse.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
+import Std.Sat.AIG.LawfulVecOperator
+
+/-!
+This module contains the implementation of a bitblaster for `BitVec.reverse`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+
+namespace BVExpr
+namespace bitblast
+
+variable [Hashable α] [DecidableEq α]
+
+def blastReverse (aig : AIG α) (s : AIG.RefVec aig w) : AIG.RefVecEntry α w :=
+  let ⟨refs, hrefs⟩ := s
+  ⟨aig, ⟨refs.reverse, by simp [hrefs]⟩⟩
+
+instance : AIG.LawfulVecOperator α AIG.RefVec blastReverse where
+  le_size := by simp [blastReverse]
+  decl_eq := by simp [blastReverse]
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 02599ac798..a5d05af99b 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -19,6 +19,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateRight
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Reverse
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 
 /-!
@@ -419,6 +420,11 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
       · rw [goCache_denote_eq]
         · simp [BitVec.msb_eq_getLsbD_last]
         · exact hinv
+    · rw [← hres]
+      simp only [denote_blastReverse, eval_un, BVUnOp.eval_reverse, hidx, BitVec.getLsbD_eq_getElem,
+        BitVec.getElem_reverse, BitVec.getMsbD_eq_getLsbD, decide_true, Bool.true_and]
+      rw [goCache_denote_eq]
+      exact hinv
   · next h =>
     subst h
     rw [← hres]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Reverse.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Reverse.lean
new file mode 100644
index 0000000000..e469b462e5
--- /dev/null
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Reverse.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
+
+/-!
+This module contains the verification of the bitblaster for `BitVec.reverse` from
+`Impl.Operations.Reverse`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+open Std.Sat.AIG
+
+namespace BVExpr
+namespace bitblast
+
+variable [Hashable α] [DecidableEq α]
+
+@[simp]
+theorem denote_blastReverse (aig : AIG α) (target : RefVec aig w)
+    (assign : α → Bool) :
+    ∀ (idx : Nat) (hidx : idx < w),
+        ⟦(blastReverse aig target).aig, (blastReverse aig target).vec.get idx hidx, assign⟧
+          =
+        ⟦aig, target.get (w - 1 - idx) (by omega), assign⟧ := by
+  intro idx hidx
+  simp [blastReverse, AIG.RefVec.get]
+
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index 2a186b1d84..d6a57937eb 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -115,6 +115,10 @@ theorem cond_false (discr : Bool) (lhs rhs : BitVec w) :
     (discr || ((bif discr then lhs else rhs) == rhs)) = true := by
   cases discr <;> simp
 
+theorem reverse_congr (w : Nat) (x x' : BitVec w) (h : x = x') :
+    BitVec.reverse x' = BitVec.reverse x := by
+  simp[*]
+
 end BitVec
 
 namespace Bool
diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean
index fc3d6b4c90..7d75e7572c 100644
--- a/tests/lean/run/bv_bitwise.lean
+++ b/tests/lean/run/bv_bitwise.lean
@@ -38,3 +38,9 @@ theorem bitwise_unit_9 (x y : BitVec 32) :
 
 theorem bitwise_unit_10 (x : BitVec 2) : (x.getMsbD 0) = x.msb := by
   bv_decide
+
+theorem bitwise_unit_11 (x : BitVec 32) : x.reverse.reverse = x := by
+  bv_decide
+
+theorem bitwise_unit_12 (x : BitVec 32) : x ≠ x.reverse → x ≠ 0 := by
+  bv_decide