feat: bv_decide support for structures of supported types (#6724)

This PR adds support for `bv_decide` to automatically split up
non-recursive structures that contain information about supported types.
It can be controlled using the new `structures` field in the `bv_decide`
config.

Author: hargoniX

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

@@ -11,6 +11,7 @@ import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Rewrite
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AndFlatten
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.EmbeddedConstraint
 import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AC
+import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Structures
 
 /-!
 This module contains the implementation of `bv_normalize`, the preprocessing tactic for `bv_decide`.
@@ -43,9 +44,17 @@ def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := d
     (go g).run cfg g
 where
   go (g : MVarId) : PreProcessM (Option MVarId) := do
-    let some g ← g.falseOrByContra | return none
+    let some g' ← g.falseOrByContra | return none
+    let mut g := g'
 
     trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}"
+    let cfg ← PreProcessM.getConfig
+
+    if cfg.structures then
+      let some g' ← structuresPass.run g | return none
+      g := g'
+
+    trace[Meta.Tactic.bv] m!"Running fixpoint pipeline on:\n{g}"
     let pipeline ← passPipeline
     Pass.fixpointPipeline pipeline g
 

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AndFlatten.lean

@@ -43,7 +43,7 @@ partial def andFlatteningPass : Pass where
 where
   processGoal (goal : MVarId) : StateRefT AndFlattenState MetaM Unit := do
     goal.withContext do
-      let hyps ← goal.getNondepPropHyps
+      let hyps ← getPropHyps
       hyps.forM processFVar
 
   processFVar (fvar : FVarId) : StateRefT AndFlattenState MetaM Unit := do

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean

@@ -32,16 +32,14 @@ def getConfig : PreProcessM BVDecideConfig := read
 @[inline]
 def checkRewritten (fvar : FVarId) : PreProcessM Bool := do
   let val := (← get).rewriteCache.contains fvar
-  trace[Meta.Tactic.bv] m!"{mkFVar fvar} was already rewritten? {val}"
   return val
 
 @[inline]
 def rewriteFinished (fvar : FVarId) : PreProcessM Unit := do
-  trace[Meta.Tactic.bv] m!"Adding {mkFVar fvar} to the rewritten set"
   modify (fun s => { s with rewriteCache := s.rewriteCache.insert fvar })
 
 def run (cfg : BVDecideConfig) (goal : MVarId) (x : PreProcessM α) : MetaM α := do
-  let hyps ← goal.getNondepPropHyps
+  let hyps ← goal.withContext do getPropHyps
   ReaderT.run x cfg |>.run' { rewriteCache := Std.HashSet.empty hyps.size }
 
 end PreProcessM

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean

@@ -27,7 +27,7 @@ def embeddedConstraintPass : Pass where
   name := `embeddedConstraintSubsitution
   run' goal := do
     goal.withContext do
-      let hyps ← goal.getNondepPropHyps
+      let hyps ← getPropHyps
       let mut relevantHyps : SimpTheoremsArray := #[]
       let mut seen : Std.HashSet Expr := {}
       let mut duplicates : Array FVarId := #[]
@@ -49,11 +49,12 @@ def embeddedConstraintPass : Pass where
         return goal
 
       let cfg ← PreProcessM.getConfig
+      let targets ← goal.withContext getPropHyps
       let simpCtx ← Simp.mkContext
         (config := { failIfUnchanged := false, maxSteps := cfg.maxSteps })
         (simpTheorems := relevantHyps)
         (congrTheorems := (← getSimpCongrTheorems))
-      let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := ← goal.getNondepPropHyps)
+      let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := targets)
       let some (_, newGoal) := result? | return none
       return newGoal
 

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Rewrite.lean

@@ -46,12 +46,12 @@ def rewriteRulesPass : Pass where
 
       let some (_, newGoal) := result? | return none
       newGoal.withContext do
-        (← newGoal.getNondepPropHyps).forM PreProcessM.rewriteFinished
+        (← getPropHyps).forM PreProcessM.rewriteFinished
       return newGoal
 where
   getHyps (goal : MVarId) : PreProcessM (Array FVarId) := do
     goal.withContext do
-      let mut hyps ← goal.getNondepPropHyps
+      let hyps ← getPropHyps
       let filter hyp := do
         return !(← PreProcessM.checkRewritten hyp)
       hyps.filterM filter

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean

@@ -0,0 +1,113 @@
+/-
+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 Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic
+import Lean.Meta.Tactic.Cases
+
+/-!
+This module contains the implementation of the pre processing pass for automatically splitting up
+structures containing information about supported types into individual parts recursively.
+
+The implementation runs cases recursively on all "interesting" types where a type is interesting if
+it is a non recursive structure and at least one of the following conditions hold:
+- it contains something of type `BitVec`/`UIntX`/`Bool`
+- it is parametrized by an interesting type
+- it contains another interesting type
+-/
+
+namespace Lean.Elab.Tactic.BVDecide
+namespace Frontend.Normalize
+
+open Lean.Meta
+
+/--
+Contains a cache for interesting and uninteresting types such that we don't duplicate work in the
+structures pass.
+-/
+structure InterestingStructures where
+  interesting : Std.HashMap Name Bool := {}
+
+private abbrev M := StateRefT InterestingStructures MetaM
+
+namespace M
+
+@[inline]
+def lookup (n : Name) : M (Option Bool) := do
+  let s ← get
+  return s.interesting.get? n
+
+@[inline]
+def markInteresting (n : Name) : M Unit := do
+  modify (fun s => {s with interesting := s.interesting.insert n true})
+
+@[inline]
+def markUninteresting (n : Name) : M Unit := do
+  modify (fun s => {s with interesting := s.interesting.insert n false})
+
+end M
+
+partial def structuresPass : Pass where
+  name := `structures
+  run' goal := do
+    let (_, { interesting, .. }) ← checkContext goal |>.run {}
+
+    let goals ← goal.casesRec fun decl => do
+      if decl.isLet || decl.isImplementationDetail then
+        return false
+      else
+        let some const := decl.type.getAppFn.constName? | return false
+        return interesting.getD const false
+    match goals with
+    | [goal] => return goal
+    | _ => throwError "structures preprocessor generated more than 1 goal"
+where
+  checkContext (goal : MVarId) : M Unit := do
+    goal.withContext do
+      for decl in ← getLCtx do
+        if !decl.isLet && !decl.isImplementationDetail then
+          discard <| typeInteresting decl.type
+
+  constInterestingCached (n : Name) : M Bool := do
+    if let some cached ← M.lookup n then
+      return cached
+
+    let interesting ← constInteresting n
+    if interesting then
+      M.markInteresting n
+      return true
+    else
+      M.markUninteresting n
+      return false
+
+  constInteresting (n : Name) : M Bool := do
+    let env ← getEnv
+    if !isStructure env n then
+      return false
+    let constInfo := (← getConstInfoInduct n)
+    if constInfo.isRec then
+      return false
+
+    let ctorTyp := (← getConstInfoCtor constInfo.ctors.head!).type
+    let analyzer state arg := do
+      return state || (← typeInteresting (← arg.fvarId!.getType))
+    forallTelescope ctorTyp fun args _ => args.foldlM (init := false) analyzer
+
+  typeInteresting (expr : Expr) : M Bool := do
+    match_expr expr with
+    | BitVec n => return (← getNatValue? n).isSome
+    | UInt8 => return true
+    | UInt16 => return true
+    | UInt32 => return true
+    | UInt64 => return true
+    | USize => return true
+    | Bool => return true
+    | _ =>
+      let some const := expr.getAppFn.constName? | return false
+      constInterestingCached const
+
+
+end Frontend.Normalize
+end Lean.Elab.Tactic.BVDecide

src/Std/Tactic/BVDecide/Syntax.lean

@@ -39,6 +39,11 @@ structure BVDecideConfig where
   -/
   embeddedConstraintSubst : Bool := true
   /--
+  Split up local declarations of structures that are collections of other supported types into their
+  individual parts automatically.
+  -/
+  structures : Bool := true
+  /--
   Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the
   Lean process.
   -/
@@ -67,8 +72,9 @@ syntax (name := bvCheck) "bv_check " optConfig str : tactic
 
 /--
 Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
-verifying it inside Lean. The solvable goals are currently limited to the Lean equivalent of
-[`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV):
+verifying it inside Lean. The solvable goals are currently limited to
+- the Lean equivalent of [`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV)
+- automatically splitting up `structure`s that contain information about `BitVec` or `Bool`
 ```lean
 example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
   intros

tests/lean/run/bv_structures.lean

@@ -0,0 +1,64 @@
+import Std.Tactic.BVDecide
+
+namespace Ex1
+
+structure Basic where
+  x : BitVec 32
+  y : BitVec 32
+
+example (b : Basic) : b.x + b.y = b.y + b.x := by
+  bv_decide
+
+end Ex1
+
+namespace Ex2
+
+structure Basic where
+  x : BitVec 32
+  y : BitVec 32
+  h : y + x = 0
+
+example (b : Basic) : b.x + b.y = 0 := by
+  bv_decide
+
+end Ex2
+
+namespace Ex3
+
+structure Recursive where
+  x : BitVec 32
+  foo : Recursive
+
+-- Don't get fooled by recursive structures
+example (_r : Recursive) (a b : BitVec 8) : a + b = b + a := by
+  bv_decide
+
+end Ex3
+
+namespace Ex4
+
+structure Foo where
+  x : BitVec 32
+  y : BitVec 32
+  h : x + y = 0
+
+structure Bar extends Foo where
+  z : BitVec 32
+
+structure FooBar extends Bar where
+  a : Unit
+
+example (f : FooBar) (h : f.z > 0) : f.x + f.y + f.z > 0 := by
+  bv_decide
+
+end Ex4
+
+namespace Ex5
+
+structure Param (x : BitVec 32) (y : BitVec 32) where
+  h : y + x = 0
+
+example (x y : BitVec 32) (p : Param x y) : x + y = 0 := by
+  bv_decide
+
+end Ex5