feat: upstream LeanSAT's bitblaster (#5013)

Step 3/~7 in upstreaming LeanSAT.

A few thoughts:
- Why is this not in `Std.Sat`? LeanSAT's bitblaster operates on a
limited internal language. For example it has no idea that signed
comparision operators even exist. This is because it relies on a
normalization pass before being given the goal. For this reason I would
not classify the bitblaster as an API that we should publicly advertise
at this abstraction level
- Sometimes I slightly rebuild parts of the LawfulOperator
infrastructure for operators that work non-tail-recursively. This is
because they do not return an `Entrypoint` but instead an
`ExtendingEntrypoint` in order to even be defined in the first place
(casting Ref's and all that). Given the fact that this barely happens
and I never actually commit to rebuilding the full API I'm hoping that
this is indeed a fine decision?
- The single explicit `decreasing_by` that has a simp only which
*almost* looks like `simp_wf` is missing a singular lemma from `simp_wf`
because it doesn't terminate otherwise.
- I am not using functional induction because it basically always fails
at some generalization step, that is also the reason that there is lots
of explicit `generalize` and manually recursive proofs.

---------

Co-authored-by: Markus Himmel <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>

src/Lean/Elab/Tactic.lean

@@ -41,3 +41,4 @@ import Lean.Elab.Tactic.ShowTerm
 import Lean.Elab.Tactic.Rfl
 import Lean.Elab.Tactic.Rewrites
 import Lean.Elab.Tactic.DiscrTreeKey
+import Lean.Elab.Tactic.BVDecide

src/Lean/Elab/Tactic/BVDecide.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2024 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.Bitblast
+
+/-!
+This directory implements the `bv_decide` tactic as a verified bitblaster with subterm sharing.
+It makes use of proof by reflection and `ofReduceBool`, thus adding the Lean compiler to the trusted
+code base.
+-/

src/Lean/Elab/Tactic/BVDecide/Bitblast.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 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.Bitblast.BoolExpr
+import Lean.Elab.Tactic.BVDecide.Bitblast.BVExpr
+
+/-!
+This directory contains the implementation of the bitblaster itself. It is split up into two parts:
+1. Bitblasting of generic boolean substructures for SMT-like problems in `BoolExpr`.
+2. The specific bitblaster for `BitVec` problems with boolean substructure in `BVExpr`.
+-/

src/Lean/Elab/Tactic/BVDecide/Bitblast/BVExpr.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 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.Bitblast.BVExpr.Basic
+import Lean.Elab.Tactic.BVDecide.Bitblast.BVExpr.Circuit
+
+/-!
+This directory contains the definition and bitblaster of `BitVec` problems with boolean substructure.
+-/