From c8b21e3786221089b30751ba95e1d10872455ebb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 9 Jul 2024 15:51:57 +0200 Subject: [PATCH 1/5] feat: BitVec.shiftRight arbitrary width implementation --- LeanSAT/BitBlast/BVExpr/Basic.lean | 10 ++ .../BitBlast/BVExpr/BitBlast/Impl/Expr.lean | 26 ++++ .../BVExpr/BitBlast/Impl/ShiftRight.lean | 127 ++++++++++++++++++ .../BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean | 1 + LeanSAT/Tactics/BVDecide.lean | 35 +++-- 5 files changed, 190 insertions(+), 9 deletions(-) diff --git a/LeanSAT/BitBlast/BVExpr/Basic.lean b/LeanSAT/BitBlast/BVExpr/Basic.lean index b213da19..049a247c 100644 --- a/LeanSAT/BitBlast/BVExpr/Basic.lean +++ b/LeanSAT/BitBlast/BVExpr/Basic.lean @@ -216,6 +216,10 @@ sign extend a `BitVec` by some constant amount. shift left by another BitVec expression. For constant shifts there exists a `BVUnop`. -/ | shiftLeft (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m +/-- +shift right by another BitVec expression. For constant shifts there exists a `BVUnop`. +-/ +| shiftRight (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m namespace BVExpr @@ -229,6 +233,7 @@ def toString : BVExpr w → String | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})" | .signExtend v expr => s!"(sext {v} {expr.toString})" | .shiftLeft lhs rhs => s!"({lhs.toString} << {rhs.toString})" + | .shiftRight lhs rhs => s!"({lhs.toString} >> {rhs.toString})" instance : ToString (BVExpr w) := ⟨toString⟩ @@ -266,6 +271,7 @@ def eval (assign : Assignment) : BVExpr w → BitVec w | .append lhs rhs => (eval assign lhs) ++ (eval assign rhs) | .signExtend v expr => BitVec.signExtend v (eval assign expr) | .shiftLeft lhs rhs => (eval assign lhs) <<< (eval assign rhs) + | .shiftRight lhs rhs => (eval assign lhs) >>> (eval assign rhs) @[simp] theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.getD idx).bv.truncate _ := by @@ -302,6 +308,10 @@ theorem eval_signExtend : eval assign (.signExtend v expr) = BitVec.signExtend v theorem eval_shiftLeft : eval assign (.shiftLeft lhs rhs) = (eval assign lhs) <<< (eval assign rhs) := by rfl +@[simp] +theorem eval_shiftRight : eval assign (.shiftRight lhs rhs) = (eval assign lhs) >>> (eval assign rhs) := by + rfl + end BVExpr /-- diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean index 656c3e24..22a8c949 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean @@ -206,6 +206,20 @@ where dsimp at hlaig hraig omega ⟩ + | .shiftRight lhs rhs => + let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs + let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs + let lhs := lhs.cast <| by + dsimp at hlaig hraig + omega + let res := bitblast.blastShiftRight aig ⟨_, lhs, rhs⟩ + ⟨ + res, + by + apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := bitblast.blastShiftRight) + dsimp at hlaig hraig + omega + ⟩ theorem bitblast_le_size {aig : AIG BVBit} (expr : BVExpr w) @@ -293,6 +307,18 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) . apply Nat.le_trans . exact (bitblast.go aig lhs).property . exact (go (go aig lhs).1.aig rhs).property + | shiftRight lhs rhs lih rih => + dsimp [go] + rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftRight)] + rw [rih, lih] + . apply Nat.lt_of_lt_of_le + . exact h1 + . exact (bitblast.go aig lhs).property + . apply Nat.lt_of_lt_of_le + . exact h1 + . apply Nat.le_trans + . exact (bitblast.go aig lhs).property + . exact (go (go aig lhs).1.aig rhs).property theorem bitblast_decl_eq (aig : AIG BVBit) (expr : BVExpr w) diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/ShiftRight.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/ShiftRight.lean index 1c958cd2..3a73a83f 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/ShiftRight.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/ShiftRight.lean @@ -6,6 +6,7 @@ Authors: Henrik Böving import LeanSAT.BitBlast.BVExpr.Basic import LeanSAT.AIG.CachedGatesLemmas import LeanSAT.AIG.LawfulStreamOperator +import LeanSAT.AIG.If namespace BVExpr namespace bitblast @@ -114,5 +115,131 @@ instance : AIG.LawfulStreamOperator α AIG.ShiftTarget blastArithShiftRightConst unfold blastArithShiftRightConst simp +namespace blastShiftRight + +structure TwoPowShiftTarget (aig : AIG α) (w : Nat) where + n : Nat + lhs : AIG.RefStream aig w + rhs : AIG.RefStream aig n + pow : Nat + +def twoPowShift (aig : AIG α) (target : TwoPowShiftTarget aig w) : AIG.RefStreamEntry α w := + let ⟨n, lhs, rhs, pow⟩ := target + if h:pow < n then + let res := blastShiftRightConst aig ⟨lhs, (2 ^ pow) % 2^n⟩ + let aig := res.aig + let shifted := res.stream + + have := by + apply AIG.LawfulStreamOperator.le_size (f := blastShiftRightConst) + let rhs := rhs.cast this + let lhs := lhs.cast this + AIG.RefStream.ite aig ⟨rhs.getRef pow h, shifted, lhs⟩ + else + ⟨aig, lhs⟩ + +instance : AIG.LawfulStreamOperator α TwoPowShiftTarget twoPowShift where + le_size := by + intros + unfold twoPowShift + dsimp + split + . apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := AIG.RefStream.ite) + apply AIG.LawfulStreamOperator.le_size (f := blastShiftRightConst) + . simp + decl_eq := by + intros + unfold twoPowShift + dsimp + split + . rw [AIG.LawfulStreamOperator.decl_eq (f := AIG.RefStream.ite)] + rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftRightConst)] + apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := blastShiftRightConst) + assumption + . simp + +end blastShiftRight + +def blastShiftRight (aig : AIG α) (target : AIG.ArbitraryShiftTarget aig w) + : AIG.RefStreamEntry α w := + let ⟨n, input, distance⟩ := target + if n = 0 then + ⟨aig, input⟩ + else + let res := blastShiftRight.twoPowShift aig ⟨_, input, distance, 0⟩ + let aig := res.aig + let acc := res.stream + + have := by + apply AIG.LawfulStreamOperator.le_size (f := blastShiftRight.twoPowShift) + + let distance := distance.cast this + go aig distance 0 (by omega) acc +where + go {n : Nat} (aig : AIG α) (distance : AIG.RefStream aig n) (curr : Nat) (hcurr : curr ≤ n - 1) + (acc : AIG.RefStream aig w) + : AIG.RefStreamEntry α w := + if h:curr < n - 1 then + let res := blastShiftRight.twoPowShift aig ⟨_, acc, distance, curr + 1⟩ + let aig := res.aig + let acc := res.stream + have := by + apply AIG.LawfulStreamOperator.le_size (f := blastShiftRight.twoPowShift) + let distance := distance.cast this + + go aig distance (curr + 1) (by omega) acc + else + ⟨aig, acc⟩ + termination_by n - 1 - curr + +theorem blastShiftRight.go_le_size (aig : AIG α) (distance : AIG.RefStream aig n) (curr : Nat) + (hcurr : curr ≤ n - 1) (acc : AIG.RefStream aig w) + : aig.decls.size ≤ (go aig distance curr hcurr acc).aig.decls.size := by + unfold go + dsimp + split + . refine Nat.le_trans ?_ (by apply go_le_size) + apply AIG.LawfulStreamOperator.le_size (f := blastShiftRight.twoPowShift) + . simp +termination_by n - 1 - curr + +theorem blastShiftRight.go_decl_eq (aig : AIG α) (distance : AIG.RefStream aig n) (curr : Nat) + (hcurr : curr ≤ n - 1) (acc : AIG.RefStream aig w) + : ∀ (idx : Nat) (h1) (h2), + (go aig distance curr hcurr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1 := by + generalize hgo : go aig distance curr hcurr acc = res + unfold go at hgo + dsimp at hgo + split at hgo + . rw [← hgo] + intros + rw [blastShiftRight.go_decl_eq] + rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftRight.twoPowShift)] + apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := blastShiftRight.twoPowShift) + assumption + . simp [← hgo] +termination_by n - 1 - curr + + +instance : AIG.LawfulStreamOperator α AIG.ArbitraryShiftTarget blastShiftRight where + le_size := by + intros + unfold blastShiftRight + dsimp + split + . simp + . refine Nat.le_trans ?_ (by apply blastShiftRight.go_le_size) + apply AIG.LawfulStreamOperator.le_size (f := blastShiftRight.twoPowShift) + decl_eq := by + intros + unfold blastShiftRight + dsimp + split + . simp + . rw [blastShiftRight.go_decl_eq] + rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftRight.twoPowShift)] + apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := blastShiftRight.twoPowShift) + assumption + end bitblast end BVExpr diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean index 18a4e62a..48904046 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean @@ -124,6 +124,7 @@ theorem go_denote_eq_eval_getLsb (aig : AIG BVBit) (expr : BVExpr w) (assign : A . simp [Ref.hgate] . intros rw [← rih] + | shiftRight lhs rhs lih rih => sorry | bin lhs op rhs lih rih => cases op with | and => diff --git a/LeanSAT/Tactics/BVDecide.lean b/LeanSAT/Tactics/BVDecide.lean index a49da4f0..4ed15342 100644 --- a/LeanSAT/Tactics/BVDecide.lean +++ b/LeanSAT/Tactics/BVDecide.lean @@ -66,6 +66,8 @@ where mkApp4 (mkConst ``BVExpr.extract) (toExpr oldWidth) (toExpr hi) (toExpr lo) (go expr) | .shiftLeft (m := m) (n := n) lhs rhs => mkApp4 (mkConst ``BVExpr.shiftLeft) (toExpr m) (toExpr n) (go lhs) (go rhs) + | .shiftRight (m := m) (n := n) lhs rhs => + mkApp4 (mkConst ``BVExpr.shiftRight) (toExpr m) (toExpr n) (go lhs) (go rhs) instance : ToExpr BVPred where toExpr x := go x @@ -217,10 +219,15 @@ theorem shiftLeft_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : Bi : lhs <<< rhs = lhs' <<< rhs' := by simp[*] -theorem shiftRight_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') +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 + simp[*] + theorem arithShiftRight_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') : BitVec.sshiftRight x' n = BitVec.sshiftRight x n := by simp[*] @@ -285,7 +292,7 @@ partial def of (x : Expr) : M (Option ReifiedBVExpr) := do | Complement.complement _ _ innerExpr => unaryReflection innerExpr .not ``not_congr | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr => - let distance? ← getNatOrBvValue? β distanceExpr --| return ← ofAtom x + let distance? ← getNatOrBvValue? β distanceExpr if distance?.isSome then shiftConstReflection β @@ -303,13 +310,23 @@ partial def of (x : Expr) : M (Option ReifiedBVExpr) := do ``BVExpr.shiftLeft ``shiftLeft_congr | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr => - shiftConstReflection - β - distanceExpr - innerExpr - .shiftRightConst - ``BVUnOp.shiftRightConst - ``shiftRight_congr + let distance? ← getNatOrBvValue? β distanceExpr + if distance?.isSome then + shiftConstReflection + β + distanceExpr + innerExpr + .shiftRightConst + ``BVUnOp.shiftRightConst + ``shiftRightNat_congr + else + shiftReflection + β + distanceExpr + innerExpr + .shiftRight + ``BVExpr.shiftRight + ``shiftRight_congr | BitVec.sshiftRight _ innerExpr distanceExpr => let some distance ← getNatValue? distanceExpr | return ← ofAtom x shiftConstLikeReflection From d71085f218c382f4490641b079200f0ae689225c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 10 Jul 2024 17:52:56 +0200 Subject: [PATCH 2/5] feat: verify ushiftRight bitblasting --- .../BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean | 15 +- .../BVExpr/BitBlast/Lemmas/ShiftRight.lean | 152 +++++++++++++++++- 2 files changed, 164 insertions(+), 3 deletions(-) diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean index 48904046..e38c4f7e 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean @@ -124,7 +124,18 @@ theorem go_denote_eq_eval_getLsb (aig : AIG BVBit) (expr : BVExpr w) (assign : A . simp [Ref.hgate] . intros rw [← rih] - | shiftRight lhs rhs lih rih => sorry + | shiftRight lhs rhs lih rih => + simp [go] + apply blastShiftRight_eq_eval_getLsb + . intros + dsimp + rw [go_denote_mem_prefix] + rw [← lih (aig := aig)] + . simp + . assumption + . simp [Ref.hgate] + . intros + rw [← rih] | bin lhs op rhs lih rih => cases op with | and => @@ -177,7 +188,7 @@ theorem go_denote_eq_eval_getLsb (aig : AIG BVBit) (expr : BVExpr w) (assign : A | not => simp [go, ih, hidx] | shiftLeftConst => simp [go, ih, hidx] | shiftRightConst => - simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un, + simp only [go, blastShiftRightConst_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un, BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp, decide_eq_true_eq] intro h diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean index 79613247..b60c06b0 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean @@ -5,6 +5,7 @@ Authors: Henrik Böving -/ import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.Basic import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.ShiftRight +import LeanSAT.Tactics.Normalize.BitVec open AIG @@ -137,7 +138,7 @@ termination_by w - curr end blastShiftRightConst @[simp] -theorem blastShiftRight_eq_eval_getLsb (aig : AIG α) (target : ShiftTarget aig w) +theorem blastShiftRightConst_eq_eval_getLsb (aig : AIG α) (target : ShiftTarget aig w) (assign : α → Bool) : ∀ (idx : Nat) (hidx : idx < w), ⟦ @@ -250,5 +251,154 @@ theorem blastArithShiftRightConst_eq_eval_getLsb (aig : AIG α) (target : ShiftT rw [blastArithShiftRightConst.go_eq_eval_getLsb] omega +opaque ushiftRight_rec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ + +@[simp] +theorem ushiftRight_rec_zero (x : BitVec w₁) (y : BitVec w₂) : + ushiftRight_rec x y 0 = x >>> (y &&& BitVec.twoPow w₂ 0) := by + sorry + +@[simp] +theorem ushiftRight_rec_succ (x : BitVec w₁) (y : BitVec w₂) : + ushiftRight_rec x y (n + 1) = + (ushiftRight_rec x y n) >>> (y &&& BitVec.twoPow w₂ (n + 1)) := by + sorry + +theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) : + x >>> y = ushiftRight_rec x y (w₂ - 1) := by + sorry + +theorem getLsb_shiftRight' (x : BitVec w) (y : BitVec w₂) (i : Nat) : + (x >>> y).getLsb i = x.getLsb (y.toNat + i) := by + sorry + +namespace blastShiftRight + +theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w) + (rhs : BitVec target.n) (assign : α → Bool) + (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.getRef idx hidx, assign⟧ = lhs.getLsb idx) + (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.getRef idx hidx, assign⟧ = rhs.getLsb idx) + : ∀ (idx : Nat) (hidx : idx < w), + ⟦ + (twoPowShift aig target).aig, + (twoPowShift aig target).stream.getRef idx hidx, + assign + ⟧ + = + (lhs >>> (rhs &&& BitVec.twoPow target.n target.pow)).getLsb idx := by + intro idx hidx + generalize hg : twoPowShift aig target = res + rcases target with ⟨n, lstream, rstream, pow⟩ + simp only [BitVec.and_twoPow_eq] + unfold twoPowShift at hg + dsimp at hg + split at hg + . split + . next hif1 => + rw [← hg] + simp only [RefStream.denote_ite, RefStream.getRef_cast, Ref_cast', + blastShiftRightConst_eq_eval_getLsb] + rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := blastShiftRightConst)] + rw [hright] + simp only [hif1, ↓reduceIte] + split + . next hif2 => + rw [hleft] + simp [getLsb_shiftRight'] + . simp only [getLsb_shiftRight', BitVec.toNat_twoPow, Bool.false_eq] + apply BitVec.getLsb_ge + omega + . next hif1 => + simp only [Bool.not_eq_true] at hif1 + rw [← hg] + simp only [RefStream.denote_ite, RefStream.getRef_cast, Ref_cast', + blastShiftRightConst_eq_eval_getLsb] + rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := blastShiftRightConst)] + rw [hright] + simp only [hif1, Bool.false_eq_true, ↓reduceIte] + rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := blastShiftRightConst)] + rw [hleft] + simp only [BVDecide.Normalize.BitVec.shiftRight_zero] + . have : rhs.getLsb pow = false := by + apply BitVec.getLsb_ge + dsimp + omega + simp only [this, Bool.false_eq_true, ↓reduceIte] + rw [← hg] + rw [hleft] + simp only [BVDecide.Normalize.BitVec.shiftRight_zero] + +theorem go_eq_eval_getLsb (aig : AIG α) (distance : AIG.RefStream aig n) (curr : Nat) + (hcurr : curr ≤ n - 1) (acc : AIG.RefStream aig w) + (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool) + (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.getRef idx hidx, assign⟧ = (ushiftRight_rec lhs rhs curr).getLsb idx) + (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.getRef idx hidx, assign⟧ = rhs.getLsb idx) + : ∀ (idx : Nat) (hidx : idx < w), + ⟦ + (go aig distance curr hcurr acc).aig, + (go aig distance curr hcurr acc).stream.getRef idx hidx, + assign + ⟧ + = + (ushiftRight_rec lhs rhs (n - 1)).getLsb idx := by + intro idx hidx + generalize hgo : go aig distance curr hcurr acc = res + unfold go at hgo + dsimp at hgo + split at hgo + . rw [← hgo] + rw [go_eq_eval_getLsb] + . intro idx hidx + simp only [ushiftRight_rec_succ] + rw [twoPowShift_eq (lhs := ushiftRight_rec lhs rhs curr)] + . simp [hacc] + . simp [hright] + . intro idx hidx + rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := twoPowShift)] + . simp [hright] + . simp [Ref.hgate] + . have : curr = n - 1 := by omega + rw [← hgo] + simp [hacc, this] +termination_by n - 1 - curr + +end blastShiftRight + +theorem blastShiftRight_eq_eval_getLsb (aig : AIG α) (target : ArbitraryShiftTarget aig w0) + (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool) + (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.getRef idx hidx, assign⟧ = lhs.getLsb idx) + (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.getRef idx hidx, assign⟧ = rhs.getLsb idx) + : ∀ (idx : Nat) (hidx : idx < w0), + ⟦ + (blastShiftRight aig target).aig, + (blastShiftRight aig target).stream.getRef idx hidx, + assign + ⟧ + = + (lhs >>> rhs).getLsb idx := by + intro idx hidx + rw [shiftRight_eq_shiftRight_rec] + generalize hres : blastShiftRight aig target = res + rcases target with ⟨n, target, distance⟩ + unfold blastShiftRight at hres + dsimp at hres + split at hres + . next hzero => + dsimp + subst hzero + rw [← hres] + simp [hleft, BitVec.and_twoPow_eq] + . rw [← hres] + rw [blastShiftRight.go_eq_eval_getLsb] + . intro idx hidx + simp only [ushiftRight_rec_zero] + rw [blastShiftRight.twoPowShift_eq] + . simp [hleft] + . simp [hright] + . intros + rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := blastShiftRight.twoPowShift)] + . simp [hright] + . simp [Ref.hgate] + end bitblast end BVExpr From 20ff265ff7e165474fb0199b7f1ba055cdb82355 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 9 Jul 2024 15:54:09 +0200 Subject: [PATCH 3/5] test: adapt test for arbitrary shiftRight --- Test/Bv/Shift.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Test/Bv/Shift.lean b/Test/Bv/Shift.lean index a31316d3..4def0f1b 100644 --- a/Test/Bv/Shift.lean +++ b/Test/Bv/Shift.lean @@ -26,9 +26,8 @@ set_option trace.bv true in theorem shift_unit_5 {x y z : BitVec 16} : (x <<< y) <<< z = (x <<< z) <<< y := by bv_decide --- This demonstrates we correctly abstract shifts of arbitrary width as atoms instead of giving up. set_option trace.bv true in -theorem shift_unit_6 {x y : BitVec 64} : (x >>> y) + y = y + (x >>> y) := by +theorem shift_unit_6 {x y z : BitVec 16} : (x >>> y) >>> z = (x >>> z) >>> y := by bv_decide set_option trace.bv true in From 7db82a76518c51a60d121580ca81c1f1e17794a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 1 Aug 2024 15:45:51 +0200 Subject: [PATCH 4/5] feat: finish verifying --- .../BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean | 2 +- .../BVExpr/BitBlast/Lemmas/ShiftLeft.lean | 23 ---------- .../BVExpr/BitBlast/Lemmas/ShiftRight.lean | 42 +++++-------------- 3 files changed, 12 insertions(+), 55 deletions(-) diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean index e38c4f7e..35172d62 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean @@ -125,7 +125,7 @@ theorem go_denote_eq_eval_getLsb (aig : AIG BVBit) (expr : BVExpr w) (assign : A . intros rw [← rih] | shiftRight lhs rhs lih rih => - simp [go] + simp only [go, eval_shiftRight] apply blastShiftRight_eq_eval_getLsb . intros dsimp diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftLeft.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftLeft.lean index 309520bf..2b5f52e1 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftLeft.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftLeft.lean @@ -162,29 +162,6 @@ theorem blastShiftLeftConst_eq_eval_getLsb (aig : AIG α) (target : ShiftTarget apply blastShiftLeftConst.go_eq_eval_getLsb omega -/- -opaque shiftLeftRec (x : BitVec w0) (y : BitVec w1) (n : Nat) : BitVec w0 - -@[simp] -theorem shiftLeftRec_zero (x : BitVec w0) (y : BitVec w1) : - shiftLeftRec x y 0 = x <<< (y &&& BitVec.twoPow w1 0) := by - sorry - -@[simp] -theorem shiftLeftRec_succ (x : BitVec w0) (y : BitVec w1) : - shiftLeftRec x y (n + 1) = - (shiftLeftRec x y n) <<< (y &&& BitVec.twoPow w1 (n + 1)) := by - sorry - -theorem shiftLeft_eq_shiftLeft_rec (x : BitVec w0) (y : BitVec w1) : - x <<< y = shiftLeftRec x y (w1 - 1) := by - sorry - -theorem getLsb_shiftLeft' (x : BitVec w) (y : BitVec w₂) (i : Nat) : - (x <<< y).getLsb i = (decide (i < w) && !decide (i < y.toNat) && x.getLsb (i - y.toNat)) := by - sorry - -/ - namespace blastShiftLeft theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w) diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean index b60c06b0..71456afd 100644 --- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean +++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/ShiftRight.lean @@ -251,27 +251,6 @@ theorem blastArithShiftRightConst_eq_eval_getLsb (aig : AIG α) (target : ShiftT rw [blastArithShiftRightConst.go_eq_eval_getLsb] omega -opaque ushiftRight_rec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ - -@[simp] -theorem ushiftRight_rec_zero (x : BitVec w₁) (y : BitVec w₂) : - ushiftRight_rec x y 0 = x >>> (y &&& BitVec.twoPow w₂ 0) := by - sorry - -@[simp] -theorem ushiftRight_rec_succ (x : BitVec w₁) (y : BitVec w₂) : - ushiftRight_rec x y (n + 1) = - (ushiftRight_rec x y n) >>> (y &&& BitVec.twoPow w₂ (n + 1)) := by - sorry - -theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) : - x >>> y = ushiftRight_rec x y (w₂ - 1) := by - sorry - -theorem getLsb_shiftRight' (x : BitVec w) (y : BitVec w₂) (i : Nat) : - (x >>> y).getLsb i = x.getLsb (y.toNat + i) := by - sorry - namespace blastShiftRight theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w) @@ -289,7 +268,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : intro idx hidx generalize hg : twoPowShift aig target = res rcases target with ⟨n, lstream, rstream, pow⟩ - simp only [BitVec.and_twoPow_eq] + simp only [BitVec.and_twoPow] unfold twoPowShift at hg dsimp at hg split at hg @@ -304,8 +283,9 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : split . next hif2 => rw [hleft] - simp [getLsb_shiftRight'] - . simp only [getLsb_shiftRight', BitVec.toNat_twoPow, Bool.false_eq] + simp + . simp only [BitVec.ushiftRight_eq', BitVec.toNat_twoPow, BitVec.getLsb_ushiftRight, + Bool.false_eq] apply BitVec.getLsb_ge omega . next hif1 => @@ -331,7 +311,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : theorem go_eq_eval_getLsb (aig : AIG α) (distance : AIG.RefStream aig n) (curr : Nat) (hcurr : curr ≤ n - 1) (acc : AIG.RefStream aig w) (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool) - (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.getRef idx hidx, assign⟧ = (ushiftRight_rec lhs rhs curr).getLsb idx) + (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.getRef idx hidx, assign⟧ = (BitVec.ushiftRightRec lhs rhs curr).getLsb idx) (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.getRef idx hidx, assign⟧ = rhs.getLsb idx) : ∀ (idx : Nat) (hidx : idx < w), ⟦ @@ -340,7 +320,7 @@ theorem go_eq_eval_getLsb (aig : AIG α) (distance : AIG.RefStream aig n) (curr assign ⟧ = - (ushiftRight_rec lhs rhs (n - 1)).getLsb idx := by + (BitVec.ushiftRightRec lhs rhs (n - 1)).getLsb idx := by intro idx hidx generalize hgo : go aig distance curr hcurr acc = res unfold go at hgo @@ -349,8 +329,8 @@ theorem go_eq_eval_getLsb (aig : AIG α) (distance : AIG.RefStream aig n) (curr . rw [← hgo] rw [go_eq_eval_getLsb] . intro idx hidx - simp only [ushiftRight_rec_succ] - rw [twoPowShift_eq (lhs := ushiftRight_rec lhs rhs curr)] + simp only [BitVec.ushiftRightRec_succ] + rw [twoPowShift_eq (lhs := BitVec.ushiftRightRec lhs rhs curr)] . simp [hacc] . simp [hright] . intro idx hidx @@ -377,7 +357,7 @@ theorem blastShiftRight_eq_eval_getLsb (aig : AIG α) (target : ArbitraryShiftTa = (lhs >>> rhs).getLsb idx := by intro idx hidx - rw [shiftRight_eq_shiftRight_rec] + rw [BitVec.shiftRight_eq_ushiftRightRec] generalize hres : blastShiftRight aig target = res rcases target with ⟨n, target, distance⟩ unfold blastShiftRight at hres @@ -387,11 +367,11 @@ theorem blastShiftRight_eq_eval_getLsb (aig : AIG α) (target : ArbitraryShiftTa dsimp subst hzero rw [← hres] - simp [hleft, BitVec.and_twoPow_eq] + simp [hleft, BitVec.and_twoPow] . rw [← hres] rw [blastShiftRight.go_eq_eval_getLsb] . intro idx hidx - simp only [ushiftRight_rec_zero] + simp only [BitVec.ushiftRightRec_zero] rw [blastShiftRight.twoPowShift_eq] . simp [hleft] . simp [hright] From dbab5d07246ac24d3503243d34c021b42df00047 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 1 Aug 2024 15:56:35 +0200 Subject: [PATCH 5/5] test: move now succeeding Evals --- Eval/fail.txt | 7 ------- Test/Eval.lean | 7 +++++++ {Eval => Test/Eval}/bitvec_InstCombineShift__239.lean | 2 +- {Eval => Test/Eval}/bitvec_InstCombineShift__279.lean | 2 +- {Eval => Test/Eval}/bitvec_InstCombineShift__422_1.lean | 0 {Eval => Test/Eval}/bitvec_InstCombineShift__440.lean | 2 +- {Eval => Test/Eval}/bitvec_InstCombineShift__476.lean | 2 +- {Eval => Test/Eval}/bitvec_InstCombineShift__497.lean | 2 +- {Eval => Test/Eval}/bitvec_InstCombineShift__582.lean | 2 +- 9 files changed, 13 insertions(+), 13 deletions(-) rename {Eval => Test/Eval}/bitvec_InstCombineShift__239.lean (60%) rename {Eval => Test/Eval}/bitvec_InstCombineShift__279.lean (60%) rename {Eval => Test/Eval}/bitvec_InstCombineShift__422_1.lean (100%) rename {Eval => Test/Eval}/bitvec_InstCombineShift__440.lean (65%) rename {Eval => Test/Eval}/bitvec_InstCombineShift__476.lean (65%) rename {Eval => Test/Eval}/bitvec_InstCombineShift__497.lean (60%) rename {Eval => Test/Eval}/bitvec_InstCombineShift__582.lean (63%) diff --git a/Eval/fail.txt b/Eval/fail.txt index 3007a693..d2777e11 100644 --- a/Eval/fail.txt +++ b/Eval/fail.txt @@ -1,13 +1,6 @@ bitvec_AndOrXor_2443.lean -bitvec_InstCombineShift__239.lean -bitvec_InstCombineShift__279.lean -bitvec_InstCombineShift__422_1.lean bitvec_InstCombineShift__422_2.lean -bitvec_InstCombineShift__440.lean bitvec_InstCombineShift__458.lean -bitvec_InstCombineShift__476.lean -bitvec_InstCombineShift__497.lean -bitvec_InstCombineShift__582.lean g2008h02h16hSDivOverflow2_proof.lean g2008h02h23hMulSub_proof.lean gadd2_proof.lean diff --git a/Test/Eval.lean b/Test/Eval.lean index 65c351ad..c3b942b8 100644 --- a/Test/Eval.lean +++ b/Test/Eval.lean @@ -131,3 +131,10 @@ import Test.Eval.bitvec_InstCombineShift__497_alt import Test.Eval.bitvec_160 import Test.Eval.bitvec_290__292 import Test.Eval.bitvec_InstCombineShift__351 +import Test.Eval.bitvec_InstCombineShift__239 +import Test.Eval.bitvec_InstCombineShift__279 +import Test.Eval.bitvec_InstCombineShift__422_1 +import Test.Eval.bitvec_InstCombineShift__440 +import Test.Eval.bitvec_InstCombineShift__476 +import Test.Eval.bitvec_InstCombineShift__497 +import Test.Eval.bitvec_InstCombineShift__582 diff --git a/Eval/bitvec_InstCombineShift__239.lean b/Test/Eval/bitvec_InstCombineShift__239.lean similarity index 60% rename from Eval/bitvec_InstCombineShift__239.lean rename to Test/Eval/bitvec_InstCombineShift__239.lean index dc790e2b..7f21be51 100644 --- a/Eval/bitvec_InstCombineShift__239.lean +++ b/Test/Eval/bitvec_InstCombineShift__239.lean @@ -1,5 +1,5 @@ import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__239 : - ∀ (X C : BitVec 64), X <<< C >>> C = X &&& (-1 : BitVec _) >>> C + ∀ (X C : BitVec 32), X <<< C >>> C = X &&& (-1 : BitVec _) >>> C := by intros; bv_decide diff --git a/Eval/bitvec_InstCombineShift__279.lean b/Test/Eval/bitvec_InstCombineShift__279.lean similarity index 60% rename from Eval/bitvec_InstCombineShift__279.lean rename to Test/Eval/bitvec_InstCombineShift__279.lean index 6d97f3ea..c55cbc2d 100644 --- a/Eval/bitvec_InstCombineShift__279.lean +++ b/Test/Eval/bitvec_InstCombineShift__279.lean @@ -1,5 +1,5 @@ import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__279 : - ∀ (X C : BitVec 64), X >>> C <<< C = X &&& (-1 : BitVec _) <<< C + ∀ (X C : BitVec 32), X >>> C <<< C = X &&& (-1 : BitVec _) <<< C := by intros; bv_decide diff --git a/Eval/bitvec_InstCombineShift__422_1.lean b/Test/Eval/bitvec_InstCombineShift__422_1.lean similarity index 100% rename from Eval/bitvec_InstCombineShift__422_1.lean rename to Test/Eval/bitvec_InstCombineShift__422_1.lean diff --git a/Eval/bitvec_InstCombineShift__440.lean b/Test/Eval/bitvec_InstCombineShift__440.lean similarity index 65% rename from Eval/bitvec_InstCombineShift__440.lean rename to Test/Eval/bitvec_InstCombineShift__440.lean index 7ff89fc1..6dd4e50b 100644 --- a/Eval/bitvec_InstCombineShift__440.lean +++ b/Test/Eval/bitvec_InstCombineShift__440.lean @@ -1,5 +1,5 @@ import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__440 : - ∀ (Y X C C2 : BitVec 64), (Y ^^^ X >>> C &&& C2) <<< C = X &&& C2 <<< C ^^^ Y <<< C + ∀ (Y X C C2 : BitVec 32), (Y ^^^ X >>> C &&& C2) <<< C = X &&& C2 <<< C ^^^ Y <<< C := by intros; bv_decide diff --git a/Eval/bitvec_InstCombineShift__476.lean b/Test/Eval/bitvec_InstCombineShift__476.lean similarity index 65% rename from Eval/bitvec_InstCombineShift__476.lean rename to Test/Eval/bitvec_InstCombineShift__476.lean index 16b49ae8..84a0553f 100644 --- a/Eval/bitvec_InstCombineShift__476.lean +++ b/Test/Eval/bitvec_InstCombineShift__476.lean @@ -1,5 +1,5 @@ import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__476 : - ∀ (Y X C C2 : BitVec 64), (X >>> C &&& C2 ||| Y) <<< C = X &&& C2 <<< C ||| Y <<< C + ∀ (Y X C C2 : BitVec 32), (X >>> C &&& C2 ||| Y) <<< C = X &&& C2 <<< C ||| Y <<< C := by intros; bv_decide diff --git a/Eval/bitvec_InstCombineShift__497.lean b/Test/Eval/bitvec_InstCombineShift__497.lean similarity index 60% rename from Eval/bitvec_InstCombineShift__497.lean rename to Test/Eval/bitvec_InstCombineShift__497.lean index c7ad13bc..b1b71e4e 100644 --- a/Eval/bitvec_InstCombineShift__497.lean +++ b/Test/Eval/bitvec_InstCombineShift__497.lean @@ -1,5 +1,5 @@ import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__497 : - ∀ (X C C2 : BitVec 64), (X ^^^ C2) >>> C = X >>> C ^^^ C2 >>> C + ∀ (X C C2 : BitVec 32), (X ^^^ C2) >>> C = X >>> C ^^^ C2 >>> C := by intros; bv_decide diff --git a/Eval/bitvec_InstCombineShift__582.lean b/Test/Eval/bitvec_InstCombineShift__582.lean similarity index 63% rename from Eval/bitvec_InstCombineShift__582.lean rename to Test/Eval/bitvec_InstCombineShift__582.lean index 0771306f..811ce719 100644 --- a/Eval/bitvec_InstCombineShift__582.lean +++ b/Test/Eval/bitvec_InstCombineShift__582.lean @@ -3,5 +3,5 @@ import LeanSAT.Tactics.BVDecide open BitVec theorem bitvec_InstCombineShift__582 : - ∀ (X C : BitVec 64), X <<< C >>> C = X &&& (-1 : BitVec _) >>> C + ∀ (X C : BitVec 32), X <<< C >>> C = X &&& (-1 : BitVec _) >>> C := by intros; bv_decide