From 2a0d78743dd100b9c9e5774c0321923c0d478486 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 8 Nov 2024 10:59:52 +0100 Subject: [PATCH] feat: migrate bv_decide to a configuration elaborator --- src/Lean/Elab/Tactic/BVDecide/External.lean | 4 +-- .../Elab/Tactic/BVDecide/Frontend/Attr.lean | 26 ++------------ .../Tactic/BVDecide/Frontend/BVCheck.lean | 25 ++++++------- .../Tactic/BVDecide/Frontend/BVDecide.lean | 27 +++++++------- .../Tactic/BVDecide/Frontend/BVTrace.lean | 11 +++--- .../Elab/Tactic/BVDecide/Frontend/LRAT.lean | 23 +++--------- .../Tactic/BVDecide/Frontend/Normalize.lean | 15 ++++---- src/Std/Tactic/BVDecide/Syntax.lean | 36 ++++++++++++++++--- tests/lean/run/bv_arith.lean | 2 -- tests/lean/run/bv_axiom_check.lean | 2 -- tests/lean/run/bv_bitwise.lean | 2 -- tests/lean/run/bv_decide_rewriter.lean | 6 ++-- tests/lean/run/bv_errors.lean | 9 ++--- tests/lean/run/bv_substructure.lean | 4 +-- 14 files changed, 86 insertions(+), 106 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/External.lean b/src/Lean/Elab/Tactic/BVDecide/External.lean index 2b58e2de4f4b..2ecfcb6679bd 100644 --- a/src/Lean/Elab/Tactic/BVDecide/External.lean +++ b/src/Lean/Elab/Tactic/BVDecide/External.lean @@ -170,8 +170,8 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro match out? with | .timeout => let mut err := "The SAT solver timed out while solving the problem.\n" - err := err ++ "Consider increasing the timeout with `set_option sat.timeout `.\n" - err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option." + err := err ++ "Consider increasing the timeout with the `timeout` config option.\n" + err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option." throwError err | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} => if exitCode == 255 then diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean index ce770dd5d59d..bfca67675de2 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean @@ -6,6 +6,7 @@ Authors: Kim Morrison, Henrik Böving prelude import Lean.Util.Trace import Lean.Elab.Tactic.Simp +import Std.Tactic.BVDecide.Syntax /-! Provides environment extensions around the `bv_decide` tactic frontends. @@ -32,30 +33,7 @@ register_builtin_option sat.solver : String := { to use the one that ships with Lean." } -register_builtin_option sat.timeout : Nat := { - defValue := 10 - descr := "the number of seconds that the sat solver is run before aborting" -} - -register_builtin_option sat.trimProofs : Bool := { - defValue := true - descr := "Whether to run the trimming algorithm on LRAT proofs" -} - -register_builtin_option sat.binaryProofs : Bool := { - defValue := true - descr := "Whether to use the binary LRAT proof format. Currently set to false and ignored on Windows due to a bug in CaDiCal." -} - -register_builtin_option debug.bv.graphviz : Bool := { - defValue := false - descr := "Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process." -} - -register_builtin_option bv.ac_nf : Bool := { - defValue := false - descr := "Canonicalize with respect to associativity and commutativitiy." -} +declare_config_elab elabBVDecideConfig Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig builtin_initialize bvNormalizeExt : Meta.SimpExtension ← Meta.registerSimpAttr `bv_normalize "simp theorems used by bv_normalize" diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean index f6846e08c1d3..0670c866b4bc 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean @@ -28,22 +28,22 @@ def getSrcDir : TermElabM System.FilePath := do | throwError "cannot compute parent directory of '{srcPath}'" return srcDir -def mkContext (lratPath : System.FilePath) : TermElabM TacticContext := do +def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM TacticContext := do let lratPath := (← getSrcDir) / lratPath - TacticContext.new lratPath + TacticContext.new lratPath cfg /-- Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`. -/ -def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do - let cert ← LratCert.ofFile cfg.lratPath cfg.trimProofs - cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true +def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do + let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs + cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true @[inherit_doc Lean.Parser.Tactic.bvCheck] -def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do +def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do let unsatProver : UnsatProver := fun _ reflectionResult _ => do withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do - let proof ← lratChecker cfg reflectionResult.bvExpr + let proof ← lratChecker ctx reflectionResult.bvExpr return .ok ⟨proof, ""⟩ let _ ← closeWithBVReflection g unsatProver return () @@ -52,14 +52,15 @@ def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do open Lean.Meta.Tactic in @[builtin_tactic Lean.Parser.Tactic.bvCheck] def evalBvCheck : Tactic := fun - | `(tactic| bv_check%$tk $path:str) => do - let cfg ← BVDecide.Frontend.BVCheck.mkContext path.getString + | `(tactic| bv_check%$tk $cfgStx:optConfig $path:str) => do + let cfg ← elabBVDecideConfig cfgStx + let ctx ← BVDecide.Frontend.BVCheck.mkContext path.getString cfg liftMetaFinishingTactic fun g => do - let g'? ← Normalize.bvNormalize g + let g'? ← Normalize.bvNormalize g cfg match g'? with - | some g' => bvCheck g' cfg + | some g' => bvCheck g' ctx | none => - let bvNormalizeStx ← `(tactic| bv_normalize) + let bvNormalizeStx ← `(tactic| bv_normalize $cfgStx) logWarning m!"This goal can be closed by only applying bv_normalize, no need to keep the LRAT proof around." TryThis.addSuggestion tk bvNormalizeStx (origSpan? := ← getRef) | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index d5098d04287a..6466e8ee9bdc 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -186,7 +186,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa err := err ++ m!"Consider the following assignment:\n" return err -def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult) +def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : MetaM (Except CounterExample UnsatProver.Result) := do let bvExpr := reflectionResult.bvExpr @@ -197,7 +197,7 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref let aigSize := entry.aig.decls.size trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes." - if cfg.graphviz then + if ctx.config.graphviz then IO.FS.writeFile ("." / "aig.gv") <| AIG.toGraphviz entry let (cnf, map) ← @@ -211,12 +211,12 @@ def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : Ref let res ← withTraceNode `sat (fun _ => return "Obtaining external proof certificate") do - runExternal cnf cfg.solver cfg.lratPath cfg.trimProofs cfg.timeout cfg.binaryProofs + runExternal cnf ctx.solver ctx.lratPath ctx.config.trimProofs ctx.config.timeout ctx.config.binaryProofs match res with | .ok cert => trace[Meta.Tactic.sat] "SAT solver found a proof." - let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true + let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true return .ok ⟨proof, cert⟩ | .error assignment => trace[Meta.Tactic.sat] "SAT solver found a counter example." @@ -267,10 +267,10 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) : return .ok cert | .error counterExample => return .error counterExample -def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do +def bvUnsat (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do - lratBitblaster g cfg reflectionResult atomsAssignment + lratBitblaster g ctx reflectionResult atomsAssignment closeWithBVReflection g unsatProver /-- @@ -287,18 +287,18 @@ structure Result where Try to close `g` using a bitblaster. Return either a `CounterExample` if one is found or a `Result` if `g` is proven. -/ -def bvDecide' (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample Result) := do - let g? ← Normalize.bvNormalize g +def bvDecide' (g : MVarId) (ctx : TacticContext) : MetaM (Except CounterExample Result) := do + let g? ← Normalize.bvNormalize g ctx.config let some g := g? | return .ok ⟨none⟩ - match ← bvUnsat g cfg with + match ← bvUnsat g ctx with | .ok lratCert => return .ok ⟨some lratCert⟩ | .error counterExample => return .error counterExample /-- Call `bvDecide'` and throw a pretty error if a counter example ends up being produced. -/ -def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do - match ← bvDecide' g cfg with +def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do + match ← bvDecide' g ctx with | .ok result => return result | .error counterExample => counterExample.goal.withContext do @@ -309,9 +309,10 @@ def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do @[builtin_tactic Lean.Parser.Tactic.bvDecide] def evalBvTrace : Tactic := fun - | `(tactic| bv_decide) => do + | `(tactic| bv_decide $cfg:optConfig) => do + let cfg ← elabBVDecideConfig cfg IO.FS.withTempFile fun _ lratFile => do - let cfg ← BVDecide.Frontend.TacticContext.new lratFile + let cfg ← BVDecide.Frontend.TacticContext.new lratFile cfg liftMetaFinishingTactic fun g => do discard <| bvDecide g cfg | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean index f1617c17b527..2d4aa1fac433 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean @@ -34,12 +34,13 @@ open Lean.Meta.Tactic in open Lean.Elab.Tactic.BVDecide.LRAT in @[builtin_tactic Lean.Parser.Tactic.bvTrace] def evalBvTrace : Tactic := fun - | `(tactic| bv_decide?%$tk) => do + | `(tactic| bv_decide?%$tk $cfgStx:optConfig) => do + let cfg := { (← elabBVDecideConfig cfgStx) with trimProofs := false } let lratFile : System.FilePath ← BVTrace.getLratFileName - let cfg := { (← BVCheck.mkContext lratFile) with trimProofs := false } + let ctx ← BVCheck.mkContext lratFile cfg let g ← getMainGoal let trace ← g.withContext do - bvDecide g cfg + bvDecide g ctx /- Ideally trace.lratCert would be the `ByteArray` version of the proof already and we just write it. This isn't yet possible so instead we do the following: @@ -57,12 +58,12 @@ def evalBvTrace : Tactic := fun let normalizeStx ← `(tactic| bv_normalize) TryThis.addSuggestion tk normalizeStx (origSpan? := ← getRef) | some .. => - if sat.trimProofs.get (← getOptions) then + if ctx.config.trimProofs then let lratPath := (← BVCheck.getSrcDir) / lratFile let proof ← loadLRATProof lratPath let trimmed ← IO.ofExcept <| trim proof dumpLRATProof lratPath trimmed cfg.binaryProofs - let bvCheckStx ← `(tactic| bv_check $(quote lratFile.toString)) + let bvCheckStx ← `(tactic| bv_check $cfgStx:optConfig $(quote lratFile.toString)) TryThis.addSuggestion tk bvCheckStx (origSpan? := ← getRef) | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean index cba5ce66dd16..4ee0206e3d67 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean @@ -30,37 +30,22 @@ structure TacticContext where reflectionDef : Name solver : System.FilePath lratPath : System.FilePath - graphviz : Bool - timeout : Nat - trimProofs : Bool - binaryProofs : Bool + config : BVDecideConfig -def TacticContext.new (lratPath : System.FilePath) : Lean.Elab.TermElabM TacticContext := do +def TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) : + Lean.Elab.TermElabM TacticContext := do let exprDef ← Lean.Elab.Term.mkAuxName `_expr_def let certDef ← Lean.Elab.Term.mkAuxName `_cert_def let reflectionDef ← Lean.Elab.Term.mkAuxName `_reflection_def - let opts ← getOptions let solver ← determineSolver trace[Meta.Tactic.sat] m!"Using SAT solver at '{solver}'" - let timeout := sat.timeout.get opts - let graphviz := debug.bv.graphviz.get opts - let trimProofs := sat.trimProofs.get opts - let binaryProofs := - -- Account for: https://github.com/arminbiere/cadical/issues/112 - if System.Platform.isWindows then - false - else - sat.binaryProofs.get opts return { exprDef, certDef, reflectionDef, solver, lratPath, - graphviz, - timeout, - trimProofs, - binaryProofs + config } where determineSolver : Lean.Elab.TermElabM System.FilePath := do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean index fc988a4eb1cd..02fd8b00f8bf 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean @@ -224,30 +224,29 @@ The normalization passes used by `bv_normalize` and thus `bv_decide`. -/ def defaultPipeline : List Pass := [rewriteRulesPass, embeddedConstraintPass] -def passPipeline : MetaM (List Pass) := do - let opts ← getOptions - +def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do let mut passPipeline := defaultPipeline - if bv.ac_nf.get opts then + if cfg.acNf then passPipeline := passPipeline ++ [acNormalizePass] return passPipeline end Pass -def bvNormalize (g : MVarId) : MetaM (Option MVarId) := do +def bvNormalize (g : MVarId) (cfg : BVDecideConfig) : MetaM (Option MVarId) := do withTraceNode `bv (fun _ => return "Normalizing goal") do -- Contradiction proof let some g ← g.falseOrByContra | return none trace[Meta.Tactic.bv] m!"Running preprocessing pipeline on:\n{g}" - Pass.fixpointPipeline (← Pass.passPipeline) g + Pass.fixpointPipeline (Pass.passPipeline cfg) g @[builtin_tactic Lean.Parser.Tactic.bvNormalize] def evalBVNormalize : Tactic := fun - | `(tactic| bv_normalize) => do + | `(tactic| bv_normalize $cfg:optConfig) => do + let cfg ← elabBVDecideConfig cfg let g ← getMainGoal - match ← bvNormalize g with + match ← bvNormalize g cfg with | some newGoal => replaceMainGoal [newGoal] | none => replaceMainGoal [] | _ => throwUnsupportedSyntax diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean index bbfaa1e0ca6b..0e14ad458657 100644 --- a/src/Std/Tactic/BVDecide/Syntax.lean +++ b/src/Std/Tactic/BVDecide/Syntax.lean @@ -9,6 +9,34 @@ import Init.Simproc set_option linter.missingDocs true -- keep it documented +namespace Lean.Elab.Tactic.BVDecide.Frontend + +/-- +The configuration options for `bv_decide`. +-/ +structure BVDecideConfig where + /-- The number of seconds that the SAT solver is run before aborting. -/ + timeout : Nat := 10 + /-- Whether to run the trimming algorithm on LRAT proofs. -/ + trimProofs : Bool := true + /-- + Whether to use the binary LRAT proof format. + Currently set to false and ignored on Windows due to a bug in CaDiCal. + -/ + binaryProofs : Bool := true + /-- + Canonicalize with respect to associativity and commutativitiy. + -/ + acNf : Bool := false + /-- + Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the + Lean process. + -/ + graphviz : Bool := false + +end Lean.Elab.Tactic.BVDecide.Frontend + + namespace Lean.Parser namespace Tactic @@ -21,7 +49,7 @@ current Lean file: bv_check "proof.lrat" ``` -/ -syntax (name := bvCheck) "bv_check " str : tactic +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 @@ -48,19 +76,19 @@ the `bv.ac_nf` option. Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator. -/ -syntax (name := bvDecide) "bv_decide" : tactic +syntax (name := bvDecide) "bv_decide" optConfig : tactic /-- Suggest a proof script for a `bv_decide` tactic call. Useful for caching LRAT proofs. -/ -syntax (name := bvTrace) "bv_decide?" : tactic +syntax (name := bvTrace) "bv_decide?" optConfig : tactic /-- Run the normalization procedure of `bv_decide` only. Sometimes this is enough to solve basic `BitVec` goals already. -/ -syntax (name := bvNormalize) "bv_normalize" : tactic +syntax (name := bvNormalize) "bv_normalize" optConfig : tactic end Tactic diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean index b40fe2360619..32805b47fa55 100644 --- a/tests/lean/run/bv_arith.lean +++ b/tests/lean/run/bv_arith.lean @@ -2,8 +2,6 @@ import Std.Tactic.BVDecide open BitVec -set_option bv.ac_nf false - theorem arith_unit_1 (x y : BitVec 64) : x + y = y + x := by bv_decide diff --git a/tests/lean/run/bv_axiom_check.lean b/tests/lean/run/bv_axiom_check.lean index 085c834e3ad1..2ef0d1732f2a 100644 --- a/tests/lean/run/bv_axiom_check.lean +++ b/tests/lean/run/bv_axiom_check.lean @@ -2,8 +2,6 @@ import Std.Tactic.BVDecide open BitVec -set_option bv.ac_nf false - theorem bv_axiomCheck (x y : BitVec 1) : x + y = y + x := by bv_decide diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean index 96923f7a12d7..fc3d6b4c9035 100644 --- a/tests/lean/run/bv_bitwise.lean +++ b/tests/lean/run/bv_bitwise.lean @@ -2,8 +2,6 @@ import Std.Tactic.BVDecide open BitVec -set_option bv.ac_nf false - theorem bitwise_unit_1 {x y : BitVec 64} : ~~~(x &&& y) = (~~~x ||| ~~~y) := by bv_decide diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 61d095045dab..6d4e3aa804d6 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -85,12 +85,10 @@ example {x : BitVec 16} : (BitVec.twoPow 16 2) = 4#16 := by bv_normalize section -set_option bv.ac_nf true - example (x y : BitVec 256) : x * y = y * x := by - bv_decide + bv_decide (config := { acNf := true }) example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by - bv_decide + bv_decide (config := { acNf := true }) end diff --git a/tests/lean/run/bv_errors.lean b/tests/lean/run/bv_errors.lean index 29023911f94b..9d668aba8ba2 100644 --- a/tests/lean/run/bv_errors.lean +++ b/tests/lean/run/bv_errors.lean @@ -2,17 +2,14 @@ import Std.Tactic.BVDecide open BitVec -set_option bv.ac_nf false - /-- error: The SAT solver timed out while solving the problem. -Consider increasing the timeout with `set_option sat.timeout `. -If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option. +Consider increasing the timeout with the `timeout` config option. +If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option. -/ #guard_msgs in -set_option sat.timeout 1 in theorem timeout (x y z : BitVec 1024) : x - (y + z) = x - y - z := by - bv_decide + bv_decide (config := { timeout := 1 }) /-- error: None of the hypotheses are in the supported BitVec fragment. diff --git a/tests/lean/run/bv_substructure.lean b/tests/lean/run/bv_substructure.lean index 3ecf37924227..472471886259 100644 --- a/tests/lean/run/bv_substructure.lean +++ b/tests/lean/run/bv_substructure.lean @@ -2,8 +2,6 @@ import Std.Tactic.BVDecide open BitVec -set_option bv.ac_nf false - theorem substructure_unit_1 (x y z : BitVec 8) : ((x = y) ∧ (y = z)) ↔ ¬(¬(x =y) ∨ (¬(y = z))) := by bv_decide @@ -33,7 +31,7 @@ theorem substructure_unit_6 (a b c: Bool) : (if a then b else c) = (if !a then c theorem substructure_unit_7 (a b c: Bool) : (bif a then b else c) = (bif !a then c else b) := by bv_decide - + theorem substructure_unit_8 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by bv_decide