From 3e61514ce44aed1a7457016776d3ff7ef6a77654 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 17 Dec 2025 12:52:57 +0100 Subject: [PATCH] perf: partially evaluate bv_decide simprocs to avoid instance synthesis (#11712) This PR avoids invoking TC synthesis and other inference mechanisms in the simprocs of bv_decide. This can give significant speedups on problems that pressure these simprocs. --- .../BVDecide/Frontend/Normalize/Simproc.lean | 231 +++++++++++++----- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 3 + src/Std/Tactic/BVDecide/Normalize/Bool.lean | 3 + 3 files changed, 177 insertions(+), 60 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean index d2ba6c844a..f19d1d44ea 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean @@ -21,6 +21,96 @@ namespace Frontend.Normalize open Lean.Meta open Std.Tactic.BVDecide.Normalize +private def mkDecideProofWith (p : Expr) (inst : Expr) : Expr := + let decP := mkApp2 (mkConst ``Decidable.decide) p inst + let boolTy := mkConst ``Bool + let decEqTrue := mkApp3 (mkConst ``Eq [1]) boolTy decP (mkConst ``Bool.true) + let h := mkApp2 (mkConst ``Eq.refl [1]) boolTy (mkConst ``Bool.true) + let h := mkExpectedPropHint h decEqTrue + mkApp3 (mkConst ``of_decide_eq_true) p inst h + +namespace BitVec + +private def mkComplement (e : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp (mkConst ``BitVec.instComplement) wExpr + mkApp3 (mkConst ``Complement.complement [0]) ty inst e + +private def mkNeg (e : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp (mkConst ``BitVec.instNeg) wExpr + mkApp3 (mkConst ``Neg.neg [0]) ty inst e + +private def mkOr (lhs rhs : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp2 (mkConst ``instHOrOfOrOp [0]) ty (mkApp (mkConst ``BitVec.instOrOp) wExpr) + mkApp6 (mkConst ``HOr.hOr [0, 0, 0]) ty ty ty inst lhs rhs + +private def mkAdd (lhs rhs : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp2 (mkConst ``instHAdd [0]) ty (mkApp (mkConst ``BitVec.instAdd) wExpr) + mkApp6 (mkConst ``HAdd.hAdd [0, 0, 0]) ty ty ty inst lhs rhs + +private def mkMul (lhs rhs : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp2 (mkConst ``instHMul [0]) ty (mkApp (mkConst ``BitVec.instMul) wExpr) + mkApp6 (mkConst ``HMul.hMul [0, 0, 0]) ty ty ty inst lhs rhs + +private def mkAppend (lhs rhs : Expr) (wlExpr wrExpr wResExpr : Expr) : Expr := + let lty := mkApp (mkConst ``BitVec) wlExpr + let rty := mkApp (mkConst ``BitVec) wrExpr + let resty := mkApp (mkConst ``BitVec) wResExpr + let inst := mkApp2 (mkConst ``BitVec.instHAppendHAddNat) wlExpr wrExpr + mkApp6 (mkConst ``HAppend.hAppend [0, 0, 0]) lty rty resty inst lhs rhs + +private def mkNatShiftRight (lhs rhs : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp (mkConst ``BitVec.instHShiftRightNat) wExpr + mkApp6 (mkConst ``HShiftRight.hShiftRight [0, 0, 0]) ty (mkConst ``Nat) ty inst lhs rhs + +private def mkNatShiftLeft (lhs rhs : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let inst := mkApp (mkConst ``BitVec.instHShiftLeftNat) wExpr + mkApp6 (mkConst ``HShiftLeft.hShiftLeft [0, 0, 0]) ty (mkConst ``Nat) ty inst lhs rhs + +private def mkBEq (lhs rhs : Expr) (wExpr : Expr) : Expr := + let ty := mkApp (mkConst ``BitVec) wExpr + let instDec := mkApp (mkConst ``instDecidableEqBitVec) wExpr + let inst := mkApp2 (mkConst ``instBEqOfDecidableEq [0]) ty instDec + mkApp4 (mkConst ``BEq.beq [0]) ty inst lhs rhs + +end BitVec + +namespace Nat + +private def mkDecideProofEq (lhs rhs : Expr) : Expr := + let p := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) lhs rhs + let inst := mkApp2 (mkConst ``instDecidableEqNat) lhs rhs + mkDecideProofWith p inst + +private def mkDecideProofLt (lhs rhs : Expr) : Expr := + let p := mkApp4 (mkConst ``LT.lt [0]) (mkConst ``Nat) (mkConst ``instLTNat) lhs rhs + let inst := mkApp2 (mkConst ``Nat.decLt) lhs rhs + mkDecideProofWith p inst + +private def mkDecideProofLe (lhs rhs : Expr) : Expr := + let p := mkApp4 (mkConst ``LE.le [0]) (mkConst ``Nat) (mkConst ``instLENat) lhs rhs + let inst := mkApp2 (mkConst ``Nat.decLe) lhs rhs + mkDecideProofWith p inst + +private def mkPow (lhs rhs : Expr) : Expr := + let ty := mkConst ``Nat + let instPow := mkApp2 (mkConst ``instPowNat [0]) ty (mkConst ``instNatPowNat) + let inst := mkApp3 (mkConst ``instHPow [0, 0]) ty ty instPow + mkApp6 (mkConst ``HPow.hPow [0, 0, 0]) ty ty ty inst lhs rhs + +private def mkAdd (lhs rhs : Expr) : Expr := + let ty := mkConst ``Nat + let inst := mkApp2 (mkConst ``instHAdd [0]) ty (mkConst ``instAddNat) + mkApp6 (mkConst ``HAdd.hAdd [0, 0, 0]) ty ty ty inst lhs rhs + +end Nat + section SimpleUnifiers builtin_simproc [bv_normalize] bv_and ((_ : BitVec _) &&& (_ : BitVec _)) := fun e => do @@ -89,13 +179,13 @@ builtin_simproc [bv_normalize] bv_add ((_ : BitVec _) + (_ : BitVec _)) := fun e if llhs.isAppOf ``HMul.hMul then let_expr HMul.hMul _ _ _ _ lllhs llrhs := llhs | return none if lllhs == lrhs then - let newRhs ← mkAppM ``Complement.complement #[llrhs] - let expr ← mkMul lllhs newRhs + let newRhs := BitVec.mkComplement llrhs wExpr + let expr := BitVec.mkMul lllhs newRhs wExpr let proof := mkApp3 (mkConst ``BitVec.add_neg_mul'') wExpr lllhs llrhs return some <| .visit { expr := expr, proof? := some proof } else if llrhs == lrhs then - let newLhs ← mkAppM ``Complement.complement #[lllhs] - let expr ← mkMul newLhs llrhs + let newLhs := BitVec.mkComplement lllhs wExpr + let expr := BitVec.mkMul newLhs llrhs wExpr let proof := mkApp3 (mkConst ``BitVec.add_neg_mul''') wExpr llrhs lllhs return some <| .visit { expr := expr, proof? := some proof } else @@ -103,13 +193,13 @@ builtin_simproc [bv_normalize] bv_add ((_ : BitVec _) + (_ : BitVec _)) := fun e else if lrhs.isAppOf ``HMul.hMul then let_expr HMul.hMul _ _ _ _ lrlhs lrrhs := lrhs | return none if llhs == lrlhs then - let newRhs ← mkAppM ``Complement.complement #[lrrhs] - let expr ← mkMul lrlhs newRhs + let newRhs := BitVec.mkComplement lrrhs wExpr + let expr := BitVec.mkMul lrlhs newRhs wExpr let proof := mkApp3 (mkConst ``BitVec.add_neg_mul) wExpr lrlhs lrrhs return some <| .visit { expr := expr, proof? := some proof } else if llhs == lrrhs then - let newLhs ← mkAppM ``Complement.complement #[lrlhs] - let expr ← mkMul newLhs lrrhs + let newLhs := BitVec.mkComplement lrlhs wExpr + let expr := BitVec.mkMul newLhs lrrhs wExpr let proof := mkApp3 (mkConst ``BitVec.add_neg_mul') wExpr lrrhs lrlhs return some <| .visit { expr := expr, proof? := some proof } else @@ -120,14 +210,14 @@ builtin_simproc [bv_normalize] bv_add ((_ : BitVec _) + (_ : BitVec _)) := fun e let addShiftLeft : MetaM (Option Simp.Step) := do let_expr HShiftLeft.hShiftLeft _ _ _ _ rlhs rrhs := rhs | return none if lhs != rrhs then return none - let expr ← mkAppM ``HOr.hOr #[lhs, rhs] + let expr := BitVec.mkOr lhs rhs wExpr let proof := mkApp3 (mkConst ``BitVec.add_shiftLeft_eq_or_shiftLeft) wExpr lhs rlhs return some <| .visit { expr := expr, proof? := some proof } let shiftLeftAdd : MetaM (Option Simp.Step) := do let_expr HShiftLeft.hShiftLeft _ _ _ _ llhs lrhs := lhs | return none if rhs != lrhs then return none - let expr ← mkAppM ``HOr.hOr #[lhs, rhs] + let expr := BitVec.mkOr lhs rhs wExpr let proof := mkApp3 (mkConst ``BitVec.shiftLeft_add_eq_shiftLeft_or) wExpr rhs llhs return some <| .visit { expr := expr, proof? := some proof } @@ -205,14 +295,21 @@ builtin_simproc [bv_normalize] bool_and ((_ : Bool) && (_ : Bool)) := fun e => d else return .continue builtin_simproc [bv_normalize] bv_beq_self ((_ : BitVec _) == (_ : BitVec _)) := fun e => do - let_expr BEq.beq _ _ lhs rhs := e | return .continue + let_expr BEq.beq ty _ lhs rhs := e | return .continue + let_expr BitVec wExpr := ty | return .continue if lhs != rhs then return .continue - return .visit { expr := toExpr true, proof? := some (← mkAppM ``beq_self_eq_true #[lhs]) } + let proof := + mkApp2 + (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.beq_self_eq_true) + wExpr + lhs + return .visit { expr := toExpr true, proof? := some proof } builtin_simproc [bv_normalize] bool_beq ((_ : Bool) == (_ : Bool)) := fun e => do let_expr BEq.beq _ _ lhs rhs := e | return .continue if lhs == rhs then - return .visit { expr := toExpr true, proof? := some (← mkAppM ``beq_self_eq_true #[lhs]) } + let proof := mkApp (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.beq_self_eq_true) lhs + return .visit { expr := toExpr true, proof? := some proof } else let notSelf : MetaM (Option Simp.Step) := do let_expr Bool.not rhs := rhs | return none @@ -298,13 +395,13 @@ builtin_simproc [bv_normalize] maxUlt (BitVec.ult (BitVec.ofNat _ _) (_ : BitVec -- A specialised version of BitVec.neg_eq_not_add so it doesn't trigger on -constant builtin_simproc [bv_normalize] neg_eq_not_add (-(_ : BitVec _)) := fun e => do let_expr Neg.neg typ _ val := e | return .continue - let_expr BitVec widthExpr := typ | return .continue - let some w ← getNatValue? widthExpr | return .continue + let_expr BitVec wExpr := typ | return .continue + let some w ← getNatValue? wExpr | return .continue match ← getBitVecValue? val with | some _ => return .continue | none => let proof := mkApp2 (mkConst ``BitVec.neg_eq_not_add) (toExpr w) val - let expr ← mkAppM ``HAdd.hAdd #[← mkAppM ``Complement.complement #[val], (toExpr 1#w)] + let expr := BitVec.mkAdd (BitVec.mkComplement val wExpr) (toExpr 1#w) wExpr return .visit { expr := expr, proof? := some proof } /-- Return a number `k` such that `2^k = n`. -/ @@ -314,9 +411,6 @@ private def Nat.log2Exact (n : Nat) : Option Nat := do guard <| Nat.pow 2 k == n return k --- Build an expression for `x ^ y`. -def mkPow (x y : Expr) : MetaM Expr := mkAppM ``HPow.hPow #[x, y] - builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofNat _ _) : BitVec _)) := fun e => do let_expr HDiv.hDiv _α _β _γ _self x y := e | return .continue let some ⟨w, yVal⟩ ← getBitVecValue? y | return .continue @@ -325,13 +419,13 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN let some k := Nat.log2Exact n | return .continue -- check that k < w. if k ≥ w then return .continue - let rhs ← mkAppM ``HShiftRight.hShiftRight #[x, mkNatLit k] + let rhs := BitVec.mkNatShiftRight x (mkNatLit k) (toExpr w) -- 2^k = n - let hk ← mkDecideProof (← mkEq (← mkPow (mkNatLit 2) (mkNatLit k)) (mkNatLit n)) + let hk := Nat.mkDecideProofEq (Nat.mkPow (mkNatLit 2) (mkNatLit k)) (mkNatLit n) -- k < w - let hlt ← mkDecideProof (← mkLt (mkNatLit k) (mkNatLit w)) - let proof := mkAppN (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt) - #[mkNatLit w, x, mkNatLit n, mkNatLit k, hk, hlt] + let hlt := Nat.mkDecideProofLt (mkNatLit k) (mkNatLit w) + let proof := mkApp6 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt) + (toExpr w) x (toExpr n) (toExpr k) hk hlt return .done { expr := rhs proof? := some proof @@ -341,7 +435,7 @@ builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec. let_expr BEq.beq _ _ outerLhs rhs := e | return .continue let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue let_expr Complement.complement _ _ lhs := outerLhs | return .continue - let expr ← mkAppM ``BEq.beq #[lhs, toExpr (~~~rhsVal)] + let expr := BitVec.mkBEq lhs (toExpr (~~~rhsVal)) (toExpr w) let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm) (toExpr w) @@ -353,7 +447,7 @@ builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_ let_expr BEq.beq _ _ lhs outerRhs := e | return .continue let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue let_expr Complement.complement _ _ rhs := outerRhs | return .continue - let expr ← mkAppM ``BEq.beq #[rhs, toExpr (~~~lhsVal)] + let expr := BitVec.mkBEq rhs (toExpr (~~~lhsVal)) (toExpr w) let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm') (toExpr w) @@ -366,8 +460,8 @@ builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue if -1#w != rhsVal then return .continue let_expr HAnd.hAnd _ _ _ _ llhs lrhs := outerLhs | return .continue - let newLhs ← mkAppM ``BEq.beq #[llhs, rhs] - let newRhs ← mkAppM ``BEq.beq #[lrhs, rhs] + let newLhs := BitVec.mkBEq llhs rhs (toExpr w) + let newRhs := BitVec.mkBEq lrhs rhs (toExpr w) let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.and_eq_allOnes) @@ -381,8 +475,8 @@ builtin_simproc [bv_normalize] bv_allOnes_eq_and ((BitVec.ofNat _ _) == (_ : Bit let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue if -1#w != lhsVal then return .continue let_expr HAnd.hAnd _ _ _ _ rlhs rrhs := outerRhs | return .continue - let newLhs ← mkAppM ``BEq.beq #[rlhs, lhs] - let newRhs ← mkAppM ``BEq.beq #[rrhs, lhs] + let newLhs := BitVec.mkBEq rlhs lhs (toExpr w) + let newRhs := BitVec.mkBEq rrhs lhs (toExpr w) let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.allOnes_eq_and) @@ -399,8 +493,8 @@ builtin_simproc [bv_normalize] bv_extractLsb'_not (BitVec.extractLsb' _ _ (~~~(_ if !(startVal + lenVal) < initialWidthVal then return .continue let_expr Complement.complement _ _ inner := inner | return .continue let newInner := mkApp4 (mkConst ``BitVec.extractLsb') initialWidth start len inner - let expr ← mkAppM ``Complement.complement #[newInner] - let lt ← mkDecideProof (← mkAppM ``LT.lt #[(← mkAppM ``HAdd.hAdd #[start, len]), initialWidth]) + let expr := BitVec.mkComplement newInner len + let lt := Nat.mkDecideProofLt (Nat.mkAdd start len) initialWidth let proof := mkApp5 (mkConst ``BitVec.extractLsb'_not_of_lt) initialWidth inner start len lt return .visit { expr := expr, proof? := some proof } @@ -424,7 +518,7 @@ builtin_simproc [bv_normalize] bv_twoPow_mul ((BitVec.ofNat _ _) * (_ : BitVec _ let_expr HMul.hMul _ _ _ _ lhsExpr rhs := e | return .continue let some ⟨w, lhs⟩ ← getBitVecValue? lhsExpr | return .continue let some pow := isTwoPow lhs | return .continue - let expr ← mkAppM ``HShiftLeft.hShiftLeft #[rhs, toExpr pow] + let expr := BitVec.mkNatShiftLeft rhs (toExpr pow) (toExpr w) let proof := mkApp3 (mkConst ``BitVec.twoPow_mul_eq_shiftLeft) (toExpr w) rhs (toExpr pow) return .visit { expr := expr, proof? := some proof } @@ -432,7 +526,7 @@ builtin_simproc [bv_normalize] bv_mul_twoPow ((_ : BitVec _) * (BitVec.ofNat _ _ let_expr HMul.hMul _ _ _ _ lhs rhsExpr := e | return .continue let some ⟨w, rhs⟩ ← getBitVecValue? rhsExpr | return .continue let some pow := isTwoPow rhs | return .continue - let expr ← mkAppM ``HShiftLeft.hShiftLeft #[lhs, toExpr pow] + let expr := BitVec.mkNatShiftLeft lhs (toExpr pow) (toExpr w) let proof := mkApp3 (mkConst ``BitVec.mul_twoPow_eq_shiftLeft) (toExpr w) lhs (toExpr pow) return .visit { expr := expr, proof? := some proof } @@ -440,7 +534,7 @@ builtin_simproc [bv_normalize] bv_ones_mul ((BitVec.ofNat _ _) * (_ : BitVec _)) let_expr HMul.hMul _ _ _ _ lhsExpr rhs := e | return .continue let some ⟨w, lhs⟩ ← getBitVecValue? lhsExpr | return .continue if -1#w != lhs then return .continue - let expr ← mkAppM ``Neg.neg #[rhs] + let expr := BitVec.mkNeg rhs (toExpr w) let proof := mkApp2 (mkConst ``BitVec.ones_mul) (toExpr w) rhs return .visit { expr := expr, proof? := some proof } @@ -448,7 +542,7 @@ builtin_simproc [bv_normalize] bv_mul_ones ((_ : BitVec _) * (BitVec.ofNat _ _)) let_expr HMul.hMul _ _ _ _ lhs rhsExpr := e | return .continue let some ⟨w, rhs⟩ ← getBitVecValue? rhsExpr | return .continue if -1#w != rhs then return .continue - let expr ← mkAppM ``Neg.neg #[lhs] + let expr := BitVec.mkNeg lhs (toExpr w) let proof := mkApp2 (mkConst ``BitVec.mul_ones) (toExpr w) lhs return .visit { expr := expr, proof? := some proof } @@ -459,15 +553,17 @@ builtin_simproc [bv_normalize] bv_elim_ushiftRight_const ((_ : BitVec _) >>> (_ let some w ← getNatValue? wExpr | return .continue if rhs < w then let zero := toExpr 0#rhs - let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr rhsExpr (toExpr (w - rhs)) lhsExpr - let concat ← mkAppM ``HAppend.hAppend #[zero, extract] + let newLen := w - rhs + let newLenExpr := toExpr newLen + let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr rhsExpr newLenExpr lhsExpr + let concat := BitVec.mkAppend zero extract (toExpr rhs) newLenExpr (toExpr (newLen + rhs)) let expr := mkApp4 (mkConst ``BitVec.cast) wExpr wExpr (← mkEqRefl wExpr) concat - let h ← mkDecideProof (← mkLt rhsExpr wExpr) + let h := Nat.mkDecideProofLt rhsExpr wExpr let proof := mkApp4 (mkConst ``BitVec.ushiftRight_eq_extractLsb'_of_lt) wExpr lhsExpr rhsExpr h return .done { expr := expr, proof? := some proof } else let expr := toExpr 0#w - let h ← mkDecideProof (← mkLe wExpr rhsExpr) + let h := Nat.mkDecideProofLe wExpr rhsExpr let proof := mkApp4 (mkConst ``BitVec.ushiftRight_eq_zero) wExpr lhsExpr rhsExpr h return .done { expr := expr, proof? := some proof } @@ -478,15 +574,17 @@ builtin_simproc [bv_normalize] bv_elim_shiftLeft_const ((_ : BitVec _) <<< (_ : let some w ← getNatValue? wExpr | return .continue if rhs < w then let zero := toExpr 0#rhs - let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr (toExpr 0) (toExpr (w - rhs)) lhsExpr - let concat ← mkAppM ``HAppend.hAppend #[extract, zero] + let newLen := w - rhs + let newLenExpr := toExpr newLen + let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr (toExpr 0) newLenExpr lhsExpr + let concat := BitVec.mkAppend extract zero newLenExpr (toExpr rhs) (toExpr (newLen + rhs)) let expr := mkApp4 (mkConst ``BitVec.cast) wExpr wExpr (← mkEqRefl wExpr) concat - let h ← mkDecideProof (← mkLt rhsExpr wExpr) + let h := Nat.mkDecideProofLt rhsExpr wExpr let proof := mkApp4 (mkConst ``BitVec.shiftLeft_eq_concat_of_lt) wExpr lhsExpr rhsExpr h return .done { expr := expr, proof? := some proof } else let expr := toExpr 0#w - let h ← mkDecideProof (← mkLe wExpr rhsExpr) + let h := Nat.mkDecideProofLe wExpr rhsExpr let proof := mkApp4 (mkConst ``BitVec.shiftLeft_eq_zero) wExpr lhsExpr rhsExpr h return .done { expr := expr, proof? := some proof } @@ -537,7 +635,7 @@ builtin_simproc [bv_normalize] bv_concat_not_extract if lstart != rstart + rlen then return .continue let newLenExpr := toExpr (llen + rlen) let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr rstartExpr newLenExpr lhsVal - let not ← mkAppM ``Complement.complement #[extract] + let not := BitVec.mkComplement extract newLenExpr let expr := mkApp4 (mkConst ``BitVec.cast) newLenExpr newLenExpr (← mkEqRefl newLenExpr) not let proof := mkApp7 @@ -569,11 +667,17 @@ builtin_simproc [bv_normalize] bv_elim_setWidth (BitVec.setWidth _ _) := fun e = oldWidthExpr targetExpr newWidthExpr - (← mkDecideProof (← mkLe newWidthExpr oldWidthExpr)) + (Nat.mkDecideProofLe newWidthExpr oldWidthExpr) return .visit { expr := expr, proof? := some proof } else - let lhs := toExpr 0#(newWidth - oldWidth) - let concat ← mkAppM ``HAppend.hAppend #[lhs ,targetExpr] + let finalWidth := newWidth - oldWidth + let lhs := toExpr 0#finalWidth + let concat := BitVec.mkAppend + lhs + targetExpr + (toExpr finalWidth) + oldWidthExpr + (toExpr (finalWidth + oldWidth)) let expr := mkApp4 (mkConst ``BitVec.cast) @@ -587,7 +691,7 @@ builtin_simproc [bv_normalize] bv_elim_setWidth (BitVec.setWidth _ _) := fun e = oldWidthExpr targetExpr newWidthExpr - (← mkDecideProof (← mkLe oldWidthExpr newWidthExpr)) + (Nat.mkDecideProofLe oldWidthExpr newWidthExpr) return .visit { expr := expr, proof? := some proof } builtin_simproc [bv_normalize] bv_elim_signExtend (BitVec.signExtend _ _) := fun e => do @@ -608,18 +712,25 @@ builtin_simproc [bv_normalize] bv_elim_signExtend (BitVec.signExtend _ _) := fun oldWidthExpr targetExpr newWidthExpr - (← mkDecideProof (← mkLe newWidthExpr oldWidthExpr)) + (Nat.mkDecideProofLe newWidthExpr oldWidthExpr) return .visit { expr := expr, proof? := some proof } else let msb := mkApp2 (mkConst ``BitVec.msb) oldWidthExpr targetExpr + let finalWidth := newWidth - oldWidth + let finalWidthExpr := toExpr finalWidth let lhs := mkApp4 (mkConst ``cond [1]) - (mkApp (mkConst ``BitVec) (toExpr (newWidth - oldWidth))) + (mkApp (mkConst ``BitVec) finalWidthExpr) msb - (toExpr (-1#(newWidth - oldWidth))) - (toExpr (0#(newWidth - oldWidth))) - let concat ← mkAppM ``HAppend.hAppend #[lhs ,targetExpr] + (toExpr (-1#finalWidth)) + (toExpr (0#finalWidth)) + let concat := BitVec.mkAppend + lhs + targetExpr + finalWidthExpr + oldWidthExpr + (toExpr (finalWidth + oldWidth)) let expr := mkApp4 (mkConst ``BitVec.cast) @@ -633,14 +744,14 @@ builtin_simproc [bv_normalize] bv_elim_signExtend (BitVec.signExtend _ _) := fun oldWidthExpr targetExpr newWidthExpr - (← mkDecideProof (← mkLe oldWidthExpr newWidthExpr)) + (Nat.mkDecideProofLe oldWidthExpr newWidthExpr) return .visit { expr := expr, proof? := some proof } builtin_simproc [bv_normalize] bv_lt_allOnes_iff (BitVec.ult _ (BitVec.ofNat _ _)) := fun e => do let_expr BitVec.ult wExpr lhsExpr rhsExpr := e | return .continue let some ⟨w, rhs⟩ ← getBitVecValue? rhsExpr | return .continue if rhs != -1#w then return .continue - let expr := mkApp (mkConst ``Bool.not) (← mkAppM ``BEq.beq #[lhsExpr, toExpr (-1#w)]) + let expr := mkApp (mkConst ``Bool.not) (BitVec.mkBEq lhsExpr (toExpr (-1#w)) wExpr) let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ult_max') wExpr lhsExpr return .visit { expr := expr, proof? := some proof } @@ -665,7 +776,7 @@ builtin_simproc [bv_normalize] bv_extract_concat rhsExpr startExpr lenExpr - (← mkDecideProof (← mkLe (toExpr (start + len)) rhsWidthExpr)) + (Nat.mkDecideProofLe (toExpr (start + len)) rhsWidthExpr) return .visit { expr := expr, proof? := some proof } else if rhsWidth ≤ start then let expr := mkApp4 (mkConst ``BitVec.extractLsb') lhsWidthExpr (toExpr (start - rhsWidth)) lenExpr lhsExpr @@ -678,7 +789,7 @@ builtin_simproc [bv_normalize] bv_extract_concat rhsExpr startExpr lenExpr - (← mkDecideProof (← mkLe rhsWidthExpr startExpr)) + (Nat.mkDecideProofLe rhsWidthExpr startExpr) return .visit { expr := expr, proof? := some proof } else -- extract is not limited to side @@ -703,7 +814,7 @@ builtin_simproc [bv_normalize] extract_add lenExpr lhsExpr rhsExpr - (← mkDecideProof (← mkLe lenExpr widthExpr)) + (Nat.mkDecideProofLe lenExpr widthExpr) return .visit { expr := expr, proof? := some proof } builtin_simproc [bv_normalize] extract_mul @@ -725,7 +836,7 @@ builtin_simproc [bv_normalize] extract_mul lenExpr lhsExpr rhsExpr - (← mkDecideProof (← mkLe lenExpr widthExpr)) + (Nat.mkDecideProofLe lenExpr widthExpr) return .visit { expr := expr, proof? := some proof } end Frontend.Normalize diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index b5ef91c6e7..b89880a560 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -493,6 +493,9 @@ theorem BitVec.mul_beq_mul_short_circuit_right {x y₁ y₂ : BitVec w} : intros congr +theorem BitVec.beq_self_eq_true (a : BitVec w) : (a == a) = true := by + apply _root_.beq_self_eq_true + @[int_toBitVec] theorem UInt8.toBitVec_cond : UInt8.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by diff --git a/src/Std/Tactic/BVDecide/Normalize/Bool.lean b/src/Std/Tactic/BVDecide/Normalize/Bool.lean index 6c3a994c56..d9216e29a1 100644 --- a/src/Std/Tactic/BVDecide/Normalize/Bool.lean +++ b/src/Std/Tactic/BVDecide/Normalize/Bool.lean @@ -302,5 +302,8 @@ theorem Bool.and_right (lhs rhs : Bool) (h : (lhs && rhs) = true) : rhs = true : revert lhs rhs decide +theorem Bool.beq_self_eq_true (a : Bool) : (a == a) = true := by + apply _root_.beq_self_eq_true + end Normalize end Std.Tactic.BVDecide