feat: bv_decide rewrites for concatenation and extraction (#7441)
This PR adds the BV_CONCAT_CONST, BV_CONCAT_EXTRACT and ELIM_ZERO_EXTEND rule from Bitwuzla to bv_decide.
This commit is contained in:
Henrik Böving
GitHub
parent
589eff6187
commit
2952cf81e6
10 changed files with 170 additions and 169 deletions
|
|
@ -2506,6 +2506,16 @@ theorem setWidth_eq_append {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) :
|
|||
omega
|
||||
· simp [hiv, getLsbD_ge x i (by omega)]
|
||||
|
||||
theorem setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
|
||||
x.setWidth w = (x.extractLsb' 0 w).cast (by omega) := by
|
||||
rw [setWidth_eq_append_extractLsb']
|
||||
ext i hi
|
||||
simp only [getElem_cast, getElem_append]
|
||||
by_cases hiv : i < v
|
||||
· simp [hi]
|
||||
omega
|
||||
· simp [getLsbD_ge x i (by omega)]
|
||||
|
||||
theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
|
||||
x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by
|
||||
ext i hi
|
||||
|
|
|
|||
|
|
@ -36,8 +36,6 @@ instance : ToExpr BVUnOp where
|
|||
toExpr x :=
|
||||
match x with
|
||||
| .not => mkConst ``BVUnOp.not
|
||||
| .shiftLeftConst n => mkApp (mkConst ``BVUnOp.shiftLeftConst) (toExpr n)
|
||||
| .shiftRightConst n => mkApp (mkConst ``BVUnOp.shiftRightConst) (toExpr n)
|
||||
| .rotateLeft n => mkApp (mkConst ``BVUnOp.rotateLeft) (toExpr n)
|
||||
| .rotateRight n => mkApp (mkConst ``BVUnOp.rotateRight) (toExpr n)
|
||||
| .arithShiftRightConst n => mkApp (mkConst ``BVUnOp.arithShiftRightConst) (toExpr n)
|
||||
|
|
@ -50,8 +48,6 @@ where
|
|||
go {w : Nat} : BVExpr w → Expr
|
||||
| .var idx => mkApp2 (mkConst ``BVExpr.var) (toExpr w) (toExpr idx)
|
||||
| .const val => mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
|
||||
| .zeroExtend (w := oldWidth) val inner =>
|
||||
mkApp3 (mkConst ``BVExpr.zeroExtend) (toExpr oldWidth) (toExpr val) (go inner)
|
||||
| .signExtend (w := oldWidth) val inner =>
|
||||
mkApp3 (mkConst ``BVExpr.signExtend) (toExpr oldWidth) (toExpr val) (go inner)
|
||||
| .bin lhs op rhs => mkApp4 (mkConst ``BVExpr.bin) (toExpr w) (go lhs) (toExpr op) (go rhs)
|
||||
|
|
|
|||
|
|
@ -49,40 +49,24 @@ where
|
|||
unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
|
||||
| HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
|
||||
let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
|
||||
if distance?.isSome then
|
||||
shiftConstReflection
|
||||
β
|
||||
distanceExpr
|
||||
innerExpr
|
||||
.shiftLeftConst
|
||||
``BVUnOp.shiftLeftConst
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr
|
||||
else
|
||||
let_expr BitVec _ := β | return none
|
||||
shiftReflection
|
||||
distanceExpr
|
||||
innerExpr
|
||||
.shiftLeft
|
||||
``BVExpr.shiftLeft
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
|
||||
if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
|
||||
let_expr BitVec _ := β | return none
|
||||
shiftReflection
|
||||
distanceExpr
|
||||
innerExpr
|
||||
.shiftLeft
|
||||
``BVExpr.shiftLeft
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
|
||||
| HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
|
||||
let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
|
||||
if distance?.isSome then
|
||||
shiftConstReflection
|
||||
β
|
||||
distanceExpr
|
||||
innerExpr
|
||||
.shiftRightConst
|
||||
``BVUnOp.shiftRightConst
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr
|
||||
else
|
||||
let_expr BitVec _ := β | return none
|
||||
shiftReflection
|
||||
distanceExpr
|
||||
innerExpr
|
||||
.shiftRight
|
||||
``BVExpr.shiftRight
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
|
||||
if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
|
||||
let_expr BitVec _ := β | return none
|
||||
shiftReflection
|
||||
distanceExpr
|
||||
innerExpr
|
||||
.shiftRight
|
||||
``BVExpr.shiftRight
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
|
||||
| BitVec.sshiftRight _ innerExpr distanceExpr =>
|
||||
let some distance ← getNatValue? distanceExpr | return none
|
||||
shiftConstLikeReflection
|
||||
|
|
@ -98,27 +82,6 @@ where
|
|||
.arithShiftRight
|
||||
``BVExpr.arithShiftRight
|
||||
``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
|
||||
| BitVec.zeroExtend _ newWidthExpr innerExpr =>
|
||||
let some newWidth ← getNatValue? newWidthExpr | return none
|
||||
let some inner ← goOrAtom innerExpr | return none
|
||||
let bvExpr := .zeroExtend newWidth inner.bvExpr
|
||||
let expr :=
|
||||
mkApp3
|
||||
(mkConst ``BVExpr.zeroExtend)
|
||||
(toExpr inner.width)
|
||||
newWidthExpr
|
||||
inner.expr
|
||||
let proof := do
|
||||
let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
|
||||
-- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
|
||||
let some innerProof ← inner.evalsAtAtoms | return none
|
||||
return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
|
||||
newWidthExpr
|
||||
(toExpr inner.width)
|
||||
innerExpr
|
||||
innerEval
|
||||
innerProof
|
||||
return some ⟨newWidth, bvExpr, proof, expr⟩
|
||||
| BitVec.signExtend _ newWidthExpr innerExpr =>
|
||||
let some newWidth ← getNatValue? newWidthExpr | return none
|
||||
let some inner ← goOrAtom innerExpr | return none
|
||||
|
|
@ -131,7 +94,7 @@ where
|
|||
inner.expr
|
||||
let proof := do
|
||||
let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
|
||||
-- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
|
||||
-- This is safe as `signExtend_congr` holds definitionally if the arguments are defeq.
|
||||
let some innerProof ← inner.evalsAtAtoms | return none
|
||||
return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
|
||||
newWidthExpr
|
||||
|
|
@ -173,7 +136,7 @@ where
|
|||
inner.expr
|
||||
let proof := do
|
||||
let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
|
||||
-- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
|
||||
-- This is safe as `replicate_congr` holds definitionally if the arguments are defeq.
|
||||
let some innerProof ← inner.evalsAtAtoms | return none
|
||||
return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
|
||||
(toExpr n)
|
||||
|
|
@ -194,7 +157,7 @@ where
|
|||
inner.expr
|
||||
let proof := do
|
||||
let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
|
||||
-- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
|
||||
-- This is safe as `extract_congr` holds definitionally if the arguments are defeq.
|
||||
let some innerProof ← inner.evalsAtAtoms | return none
|
||||
return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
|
||||
startExpr
|
||||
|
|
@ -262,12 +225,6 @@ where
|
|||
let some distance ← getNatValue? distanceExpr | return none
|
||||
shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
|
||||
|
||||
shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
|
||||
(shiftOpName : Name) (congrThm : Name) :
|
||||
LemmaM (Option ReifiedBVExpr) := do
|
||||
let some distance ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr | return none
|
||||
shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm
|
||||
|
||||
shiftReflection (distanceExpr : Expr) (innerExpr : Expr)
|
||||
(shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
|
||||
(congrThm : Name) :
|
||||
|
|
|
|||
|
|
@ -263,5 +263,112 @@ builtin_simproc [bv_normalize] bv_elim_shiftLeft_const ((_ : BitVec _) <<< (_ :
|
|||
let proof := mkApp4 (mkConst ``BitVec.shiftLeft_eq_zero) wExpr lhsExpr rhsExpr h
|
||||
return .done { expr := expr, proof? := some proof }
|
||||
|
||||
builtin_simproc [bv_normalize] bv_concat_extract
|
||||
((HAppend.hAppend (α := BitVec (no_index _)) (β := BitVec (no_index _)) (γ := BitVec (no_index _))
|
||||
(BitVec.extractLsb' _ _ _)
|
||||
(BitVec.extractLsb' _ _ _)))
|
||||
:= fun e => do
|
||||
let_expr HAppend.hAppend _ _ _ _ lhsExpr rhsExpr := e | return .continue
|
||||
let_expr BitVec.extractLsb' wExpr lstartExpr llenExpr lhsVal := lhsExpr | return .continue
|
||||
let some lstart ← getNatValue? lstartExpr | return .continue
|
||||
let some llen ← getNatValue? llenExpr | return .continue
|
||||
let_expr BitVec.extractLsb' _ rstartExpr rlenExpr rhsVal := rhsExpr | return .continue
|
||||
let some rstart ← getNatValue? rstartExpr | return .continue
|
||||
let some rlen ← getNatValue? rlenExpr | return .continue
|
||||
if lhsVal != rhsVal then return .continue
|
||||
if lstart != rstart + rlen then return .continue
|
||||
let newLenExpr := toExpr (llen + rlen)
|
||||
let extract := mkApp4 (mkConst ``BitVec.extractLsb') wExpr rstartExpr newLenExpr lhsVal
|
||||
let expr := mkApp4 (mkConst ``BitVec.cast) newLenExpr newLenExpr (← mkEqRefl newLenExpr) extract
|
||||
let proof :=
|
||||
mkApp7
|
||||
(mkConst ``BitVec.extractLsb'_append_extractLsb'_eq_extractLsb')
|
||||
wExpr
|
||||
lstartExpr
|
||||
rstartExpr
|
||||
rlenExpr
|
||||
llenExpr
|
||||
lhsVal
|
||||
(← mkEqRefl lstartExpr)
|
||||
return .visit { expr := expr, proof? := some proof }
|
||||
|
||||
builtin_simproc [bv_normalize] bv_concat_not_extract
|
||||
((HAppend.hAppend (α := BitVec (no_index _)) (β := BitVec (no_index _)) (γ := BitVec (no_index _))
|
||||
(Complement.complement (α := BitVec (no_index _)) (BitVec.extractLsb' _ _ _))
|
||||
(Complement.complement (α := BitVec (no_index _)) (BitVec.extractLsb' _ _ _))))
|
||||
:= fun e => do
|
||||
let_expr HAppend.hAppend _ _ _ _ lhsExpr rhsExpr := e | return .continue
|
||||
let_expr Complement.complement _ _ lhsExpr := lhsExpr | return .continue
|
||||
let_expr Complement.complement _ _ rhsExpr := rhsExpr | return .continue
|
||||
let_expr BitVec.extractLsb' wExpr lstartExpr llenExpr lhsVal := lhsExpr | return .continue
|
||||
let some lstart ← getNatValue? lstartExpr | return .continue
|
||||
let some llen ← getNatValue? llenExpr | return .continue
|
||||
let_expr BitVec.extractLsb' _ rstartExpr rlenExpr rhsVal := rhsExpr | return .continue
|
||||
let some rstart ← getNatValue? rstartExpr | return .continue
|
||||
let some rlen ← getNatValue? rlenExpr | return .continue
|
||||
if lhsVal != rhsVal then return .continue
|
||||
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 expr := mkApp4 (mkConst ``BitVec.cast) newLenExpr newLenExpr (← mkEqRefl newLenExpr) not
|
||||
let proof :=
|
||||
mkApp7
|
||||
(mkConst ``BitVec.not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb')
|
||||
wExpr
|
||||
lstartExpr
|
||||
rstartExpr
|
||||
rlenExpr
|
||||
llenExpr
|
||||
lhsVal
|
||||
(← mkEqRefl lstartExpr)
|
||||
return .visit { expr := expr, proof? := some proof }
|
||||
|
||||
builtin_simproc [bv_normalize] bv_elim_setWidth (BitVec.setWidth _ _) := fun e => do
|
||||
let_expr BitVec.setWidth oldWidthExpr newWidthExpr targetExpr := e | return .continue
|
||||
let some oldWidth ← getNatValue? oldWidthExpr | return .continue
|
||||
let some newWidth ← getNatValue? newWidthExpr | return .continue
|
||||
if newWidth ≤ oldWidth then
|
||||
let extract :=
|
||||
mkApp4
|
||||
(mkConst ``BitVec.extractLsb')
|
||||
oldWidthExpr
|
||||
(toExpr 0)
|
||||
newWidthExpr
|
||||
targetExpr
|
||||
let expr :=
|
||||
mkApp4
|
||||
(mkConst ``BitVec.cast)
|
||||
newWidthExpr
|
||||
newWidthExpr
|
||||
(← mkEqRefl newWidthExpr)
|
||||
extract
|
||||
let proof :=
|
||||
mkApp4
|
||||
(mkConst ``BitVec.setWidth_eq_extractLsb')
|
||||
oldWidthExpr
|
||||
targetExpr
|
||||
newWidthExpr
|
||||
(← mkDecideProof (← mkLe newWidthExpr oldWidthExpr))
|
||||
return .visit { expr := expr, proof? := some proof }
|
||||
else
|
||||
let lhs := toExpr 0#(newWidth - oldWidth)
|
||||
let concat ← mkAppM ``HAppend.hAppend #[lhs ,targetExpr]
|
||||
let expr :=
|
||||
mkApp4
|
||||
(mkConst ``BitVec.cast)
|
||||
newWidthExpr
|
||||
newWidthExpr
|
||||
(← mkEqRefl newWidthExpr)
|
||||
concat
|
||||
let proof :=
|
||||
mkApp4
|
||||
(mkConst ``BitVec.setWidth_eq_append)
|
||||
oldWidthExpr
|
||||
targetExpr
|
||||
newWidthExpr
|
||||
(← mkDecideProof (← mkLe oldWidthExpr newWidthExpr))
|
||||
return .visit { expr := expr, proof? := some proof }
|
||||
|
||||
end Frontend.Normalize
|
||||
end Lean.Elab.Tactic.BVDecide
|
||||
|
|
|
|||
|
|
@ -119,22 +119,6 @@ inductive BVUnOp where
|
|||
-/
|
||||
| not
|
||||
/--
|
||||
Shifting left by a constant value.
|
||||
|
||||
This operation has a dedicated constant representation as shiftLeft can take `Nat` as a shift amount.
|
||||
We can obviously not bitblast a `Nat` but still want to support the case where the user shifts by a
|
||||
constant `Nat` value.
|
||||
-/
|
||||
| shiftLeftConst (n : Nat)
|
||||
/--
|
||||
Shifting right by a constant value.
|
||||
|
||||
This operation has a dedicated constant representation as shiftRight can take `Nat` as a shift amount.
|
||||
We can obviously not bitblast a `Nat` but still want to support the case where the user shifts by a
|
||||
constant `Nat` value.
|
||||
-/
|
||||
| shiftRightConst (n : Nat)
|
||||
/--
|
||||
Rotating left by a constant value.
|
||||
-/
|
||||
| rotateLeft (n : Nat)
|
||||
|
|
@ -155,8 +139,6 @@ namespace BVUnOp
|
|||
|
||||
def toString : BVUnOp → String
|
||||
| not => "~"
|
||||
| shiftLeftConst n => s!"<< {n}"
|
||||
| shiftRightConst n => s!">> {n}"
|
||||
| rotateLeft n => s!"rotL {n}"
|
||||
| rotateRight n => s!"rotR {n}"
|
||||
| arithShiftRightConst n => s!">>a {n}"
|
||||
|
|
@ -168,22 +150,12 @@ The semantics for `BVUnOp`.
|
|||
-/
|
||||
def eval : BVUnOp → (BitVec w → BitVec w)
|
||||
| not => (~~~ ·)
|
||||
| shiftLeftConst n => (· <<< n)
|
||||
| shiftRightConst n => (· >>> n)
|
||||
| rotateLeft n => (BitVec.rotateLeft · n)
|
||||
| rotateRight n => (BitVec.rotateRight · n)
|
||||
| arithShiftRightConst n => (BitVec.sshiftRight · n)
|
||||
|
||||
@[simp] theorem eval_not : eval .not = ((~~~ ·) : BitVec w → BitVec w) := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem eval_shiftLeftConst : eval (shiftLeftConst n) = ((· <<< n) : BitVec w → BitVec w) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem eval_shiftRightConst : eval (shiftRightConst n) = ((· >>> n) : BitVec w → BitVec w) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem eval_rotateLeft : eval (rotateLeft n) = ((BitVec.rotateLeft · n) : BitVec w → BitVec w) := by
|
||||
rfl
|
||||
|
|
@ -211,10 +183,6 @@ inductive BVExpr : Nat → Type where
|
|||
-/
|
||||
| const (val : BitVec w) : BVExpr w
|
||||
/--
|
||||
zero extend a `BitVec` by some constant amount.
|
||||
-/
|
||||
| zeroExtend (v : Nat) (expr : BVExpr w) : BVExpr v
|
||||
/--
|
||||
Extract a slice from a `BitVec`.
|
||||
-/
|
||||
| extract (start len : Nat) (expr : BVExpr w) : BVExpr len
|
||||
|
|
@ -256,7 +224,6 @@ namespace BVExpr
|
|||
def toString : BVExpr w → String
|
||||
| .var idx => s!"var{idx}"
|
||||
| .const val => ToString.toString val
|
||||
| .zeroExtend v expr => s!"(zext {v} {expr.toString})"
|
||||
| .extract start len expr => s!"{expr.toString}[{start}, {len}]"
|
||||
| .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
|
||||
| .un op operand => s!"({op.toString} {toString operand})"
|
||||
|
|
@ -303,7 +270,6 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
|
|||
else
|
||||
packedBv.bv.truncate w
|
||||
| .const val => val
|
||||
| .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
|
||||
| .extract start len expr => BitVec.extractLsb' start len (eval assign expr)
|
||||
| .bin lhs op rhs => op.eval (eval assign lhs) (eval assign rhs)
|
||||
| .un op operand => op.eval (eval assign operand)
|
||||
|
|
@ -326,10 +292,6 @@ theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.tru
|
|||
@[simp]
|
||||
theorem eval_const : eval assign (.const val) = val := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem eval_zeroExtend : eval assign (.zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem eval_extract : eval assign (.extract start len expr) = BitVec.extractLsb' start len (eval assign expr) := by
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -11,7 +11,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
|
|||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
|
||||
|
|
@ -45,14 +44,6 @@ where
|
|||
| .const val =>
|
||||
let res := bitblast.blastConst aig val
|
||||
⟨res, AIG.LawfulVecOperator.le_size (f := bitblast.blastConst) ..⟩
|
||||
| .zeroExtend (w := w) v inner =>
|
||||
let ⟨⟨aig, evec⟩, haig⟩ := go aig inner
|
||||
let res := bitblast.blastZeroExtend aig ⟨w, evec⟩
|
||||
have := by
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastZeroExtend)
|
||||
dsimp only at haig
|
||||
assumption
|
||||
⟨res, this⟩
|
||||
| .signExtend (w := w) v inner =>
|
||||
let ⟨⟨aig, evec⟩, haig⟩ := go aig inner
|
||||
let res := bitblast.blastSignExtend aig ⟨w, evec⟩
|
||||
|
|
@ -127,20 +118,6 @@ where
|
|||
dsimp only at heaig
|
||||
omega
|
||||
⟨res, this⟩
|
||||
| .shiftLeftConst distance =>
|
||||
let res := bitblast.blastShiftLeftConst eaig ⟨evec, distance⟩
|
||||
have := by
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastShiftLeftConst)
|
||||
dsimp only at heaig
|
||||
assumption
|
||||
⟨res, this⟩
|
||||
| .shiftRightConst distance =>
|
||||
let res := bitblast.blastShiftRightConst eaig ⟨evec, distance⟩
|
||||
have := by
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastShiftRightConst)
|
||||
dsimp only at heaig
|
||||
assumption
|
||||
⟨res, this⟩
|
||||
| .rotateLeft distance =>
|
||||
let res := bitblast.blastRotateLeft eaig ⟨evec, distance⟩
|
||||
have := by
|
||||
|
|
@ -251,19 +228,13 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
|
|||
apply Nat.le_trans <;> assumption
|
||||
| un op expr ih =>
|
||||
match op with
|
||||
| .not | .shiftLeftConst .. | .shiftRightConst .. | .rotateLeft .. | .rotateRight ..
|
||||
| .not | .rotateLeft .. | .rotateRight ..
|
||||
| .arithShiftRightConst .. =>
|
||||
dsimp only [go]
|
||||
rw [AIG.LawfulVecOperator.decl_eq]
|
||||
rw [ih]
|
||||
have := (go aig expr).property
|
||||
omega
|
||||
| zeroExtend w inner ih =>
|
||||
dsimp only [go]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := blastZeroExtend)]
|
||||
rw [ih]
|
||||
have := (go aig inner).property
|
||||
omega
|
||||
| signExtend w inner ih =>
|
||||
dsimp only [go]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := blastSignExtend)]
|
||||
|
|
|
|||
|
|
@ -11,7 +11,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Not
|
|||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
|
||||
|
|
@ -67,11 +66,6 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
simp [go, denote_blastConst]
|
||||
| var =>
|
||||
simp [go, hidx, denote_blastVar]
|
||||
| zeroExtend v inner ih =>
|
||||
simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
|
||||
eval_zeroExtend, BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and,
|
||||
Bool.and_iff_right_iff_imp, decide_eq_true_eq]
|
||||
apply BitVec.lt_of_getLsbD
|
||||
| append lhs rhs lih rih =>
|
||||
rename_i lw rw
|
||||
simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
|
||||
|
|
@ -229,16 +223,6 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
| un op expr ih =>
|
||||
cases op with
|
||||
| not => simp [go, ih, hidx]
|
||||
| shiftLeftConst i =>
|
||||
rename_i w
|
||||
simp [go, ih, hidx, show idx - i < w by omega]
|
||||
| shiftRightConst =>
|
||||
simp only [go, denote_blastShiftRightConst, ih, dite_eq_ite, Bool.if_false_right, eval_un,
|
||||
BVUnOp.eval_shiftRightConst, BitVec.getLsbD_ushiftRight, Bool.and_iff_right_iff_imp,
|
||||
decide_eq_true_eq]
|
||||
intro h
|
||||
apply BitVec.lt_of_getLsbD
|
||||
assumption
|
||||
| rotateLeft => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
|
||||
| rotateRight => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem]
|
||||
| arithShiftRightConst n =>
|
||||
|
|
|
|||
|
|
@ -37,9 +37,8 @@ theorem BitVec.gt_ult (x y : BitVec w) : x > y ↔ (y.ult x = true) := by
|
|||
theorem BitVec.ge_ule (x y : BitVec w) : x ≥ y ↔ ((!x.ult y) = true) := by
|
||||
simp [BitVec.le_ult]
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.truncate_eq_zeroExtend (x : BitVec w) : x.truncate n = x.zeroExtend n := by
|
||||
rfl
|
||||
attribute [bv_normalize] BitVec.zeroExtend_eq_setWidth
|
||||
attribute [bv_normalize] BitVec.truncate_eq_setWidth
|
||||
|
||||
attribute [bv_normalize] BitVec.extractLsb
|
||||
attribute [bv_normalize] BitVec.msb_eq_getLsbD_last
|
||||
|
|
@ -151,8 +150,6 @@ section Constant
|
|||
|
||||
attribute [bv_normalize] BitVec.add_zero
|
||||
attribute [bv_normalize] BitVec.zero_add
|
||||
attribute [bv_normalize] BitVec.setWidth_eq
|
||||
attribute [bv_normalize] BitVec.setWidth_zero
|
||||
attribute [bv_normalize] BitVec.getLsbD_zero
|
||||
attribute [bv_normalize] BitVec.getLsbD_zero_length
|
||||
attribute [bv_normalize] BitVec.getLsbD_concat_zero
|
||||
|
|
@ -419,5 +416,24 @@ theorem BitVec.and_const_left' :
|
|||
theorem BitVec.and_const_right' {a : BitVec w} :
|
||||
(a &&& BitVec.ofNat w b) &&& BitVec.ofNat w c = (BitVec.ofNat w b &&& BitVec.ofNat w c) &&& a := by
|
||||
ac_rfl
|
||||
|
||||
-- Explicit no_index so this theorem works in the presence of constant folding if w1/w2/w3 are fixed
|
||||
@[bv_normalize]
|
||||
theorem BitVec.append_const_left {c : BitVec w3} :
|
||||
HAppend.hAppend (β := BitVec (no_index _)) (γ := BitVec (no_index _))
|
||||
(BitVec.ofNat w1 a)
|
||||
(HAppend.hAppend (γ := BitVec (no_index _)) (BitVec.ofNat w2 b) c)
|
||||
= ((BitVec.ofNat w1 a ++ BitVec.ofNat w2 b) ++ c).cast (Nat.add_assoc ..) := by
|
||||
rw [BitVec.append_assoc]
|
||||
simp
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.append_const_right {a : BitVec w1} :
|
||||
HAppend.hAppend (α := BitVec (no_index _)) (γ := BitVec (no_index _))
|
||||
(HAppend.hAppend (γ := BitVec (no_index _)) a (BitVec.ofNat w2 b))
|
||||
(BitVec.ofNat w3 c)
|
||||
= (a ++ (BitVec.ofNat w2 b ++ BitVec.ofNat w3 c)).cast (Eq.symm <| Nat.add_assoc ..) := by
|
||||
rw [BitVec.append_assoc]
|
||||
|
||||
end Normalize
|
||||
end Std.Tactic.BVDecide
|
||||
|
|
|
|||
|
|
@ -36,19 +36,11 @@ theorem xor_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2
|
|||
theorem not_congr (w : Nat) (x x' : BitVec w) (h : x = x') : ~~~x' = ~~~x := by
|
||||
simp[*]
|
||||
|
||||
theorem shiftLeftNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
|
||||
x' <<< n = x <<< n := by
|
||||
simp[*]
|
||||
|
||||
theorem shiftLeft_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
|
||||
(rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
|
||||
lhs <<< rhs = lhs' <<< rhs' := by
|
||||
simp[*]
|
||||
|
||||
theorem shiftRightNat_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
|
||||
x' >>> n = x >>> n := by
|
||||
simp[*]
|
||||
|
||||
theorem shiftRight_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
|
||||
(rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
|
||||
lhs >>> rhs = lhs' >>> rhs' := by
|
||||
|
|
@ -67,10 +59,6 @@ theorem add_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2
|
|||
lhs' + rhs' = lhs + rhs := by
|
||||
simp[*]
|
||||
|
||||
theorem zeroExtend_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
|
||||
BitVec.zeroExtend n x' = BitVec.zeroExtend n x := by
|
||||
simp[*]
|
||||
|
||||
theorem signExtend_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
|
||||
BitVec.signExtend n x' = BitVec.signExtend n x := by
|
||||
simp[*]
|
||||
|
|
|
|||
|
|
@ -30,8 +30,6 @@ example (a b : Bool) : ((a = true) ↔ (b = true)) ↔ (a == b) := by bv_normali
|
|||
example {x : BitVec 16} : 0#16 + x = x := by bv_normalize
|
||||
example {x : BitVec 16} : x + 0#16 = x := by bv_normalize
|
||||
example {x : BitVec 16} : x.setWidth 16 = x := by bv_normalize
|
||||
example : (0#w).setWidth 32 = 0#32 := by bv_normalize
|
||||
example : (0#w).getLsbD i = false := by bv_normalize
|
||||
example {x : BitVec 0} : x.getLsbD i = false := by bv_normalize
|
||||
example {x : BitVec 16} {b : Bool} : (x.concat b).getLsbD 0 = b := by bv_normalize
|
||||
example {x : BitVec 16} : 1 * x = x := by bv_normalize
|
||||
|
|
@ -573,6 +571,18 @@ example {x : BitVec 8} : (x &&& 10) &&& 2 = 2 &&& x := by bv_normalize
|
|||
example {x : BitVec 8} : 2 &&& (x &&& 10) = 2 &&& x := by bv_normalize
|
||||
example {x : BitVec 8} : 2 &&& (10 &&& x) = 2 &&& x := by bv_normalize
|
||||
|
||||
-- BV_CONCAT_CONST
|
||||
example {x : BitVec 8} : 8#4 ++ (4#4 ++ x) = 132#8 ++ x := by bv_normalize
|
||||
example {x : BitVec 8} : (x ++ 4#4) ++ 8#4 = x ++ 72#8 := by bv_normalize
|
||||
|
||||
-- BV_CONCAT_EXTRACT
|
||||
example {x : BitVec 8} : x.extractLsb' 3 5 ++ x.extractLsb' 1 2 = x.extractLsb' 1 7 := by
|
||||
bv_normalize
|
||||
|
||||
example {x : BitVec 8} :
|
||||
(~~~x.extractLsb' 3 5) ++ (~~~x.extractLsb' 1 2) = ~~~x.extractLsb' 1 7 := by
|
||||
bv_normalize
|
||||
|
||||
section
|
||||
|
||||
example (x y : BitVec 256) : x * y = y * x := by
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue