feat: shiftRight for arbitrary widths

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

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
 
 /--

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)

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

LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean

@@ -124,6 +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 =>
+    simp only [go, eval_shiftRight]
+    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 =>
@@ -176,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

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)