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.
This commit is contained in:
Henrik Böving
GitHub
parent
f63c2363ee
commit
3e61514ce4
3 changed files with 177 additions and 60 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue