feat: shiftRight bitblasting theorems #11

bollu · 2024-07-24T14:02:48Z

These theorems allow us to bitblast arithmetic and logical shift rights. The TODOS are yet to be addressed.

src/Init/Data/BitVec/Bitblast.lean

src/Init/Data/BitVec/Basic.lean

src/Init/Data/BitVec/Bitblast.lean

tobiasgrosser · 2024-07-30T19:20:52Z

This did not lead to a clean PR? Maybe update origin/master and merge origin/master?

bollu · 2024-07-30T19:29:04Z

@tobiasgrosser clean now.

tobiasgrosser · 2024-07-30T19:36:25Z

src/Init/Data/BitVec/Bitblast.lean

+theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) :
+  x >>> y = x >>> y.toNat := by rfl


Suggested change

theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) :

x >>> y = x >>> y.toNat := by rfl

theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :

x >>> y = x >>> y.toNat := by rfl

tobiasgrosser · 2024-07-30T19:37:03Z

src/Init/Data/BitVec/Bitblast.lean

+theorem getLsb_ushiftRight' (x : BitVec w) (y : BitVec w₂) (i : Nat) :
+    (x >>>  y).getLsb i = x.getLsb (y.toNat + i) := by


Suggested change

theorem getLsb_ushiftRight' (x : BitVec w) (y : BitVec w₂) (i : Nat) :

(x >>> y).getLsb i = x.getLsb (y.toNat + i) := by

theorem getLsb_ushiftRight' (x : BitVec w₁) (y : BitVec w₂) (i : Nat) :

(x >>> y).getLsb i = x.getLsb (y.toNat + i) := by

tobiasgrosser · 2024-07-30T19:37:52Z

src/Init/Data/BitVec/Bitblast.lean

+theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) :
+    x >>> y = ushiftRight_rec x y (w₂ - 1) := by


Suggested change

theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) :

x >>> y = ushiftRight_rec x y (w₂ - 1) := by

theorem shiftRight_eq_shiftRight_rec (x : BitVec w₁) (y : BitVec w₂) :

x >>> y = ushiftRight_rec x y (w₂ - 1) := by

tobiasgrosser · 2024-07-30T19:38:11Z

src/Init/Data/BitVec/Bitblast.lean

+def sshiftRightRec (x : BitVec w) (y : BitVec w₂) (n : Nat) : BitVec w :=
+  let shiftAmt := (y &&& (twoPow w₂ n))


Suggested change

def sshiftRightRec (x : BitVec w) (y : BitVec w₂) (n : Nat) : BitVec w :=

let shiftAmt := (y &&& (twoPow w₂ n))

def sshiftRightRec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ :=

let shiftAmt := (y &&& (twoPow w₂ n))

tobiasgrosser · 2024-07-30T19:38:24Z

src/Init/Data/BitVec/Bitblast.lean

+theorem sshiftRightRec_zero_eq (x : BitVec w) (y : BitVec w₂) :
+    sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by


Suggested change

theorem sshiftRightRec_zero_eq (x : BitVec w) (y : BitVec w₂) :

sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by

theorem sshiftRightRec_zero_eq (x : BitVec w₁) (y : BitVec w₂) :

sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by

tobiasgrosser · 2024-07-30T19:38:36Z

src/Init/Data/BitVec/Bitblast.lean

+theorem sshiftRightRec_succ_eq (x : BitVec w) (y : BitVec w₂) (n : Nat) :
+    sshiftRightRec x y (n + 1) = (sshiftRightRec x y n).sshiftRight' (y &&& twoPow w₂ (n + 1)) := by


Suggested change

theorem sshiftRightRec_succ_eq (x : BitVec w) (y : BitVec w₂) (n : Nat) :

sshiftRightRec x y (n + 1) = (sshiftRightRec x y n).sshiftRight' (y &&& twoPow w₂ (n + 1)) := by

theorem sshiftRightRec_succ_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :

sshiftRightRec x y (n + 1) = (sshiftRightRec x y n).sshiftRight' (y &&& twoPow w₂ (n + 1)) := by

tobiasgrosser · 2024-07-30T19:38:48Z

src/Init/Data/BitVec/Bitblast.lean

+theorem sshiftRight_or_eq_sshiftRight_sshiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}
+    (h : y &&& z = 0#w₂) :


Suggested change

theorem sshiftRight_or_eq_sshiftRight_sshiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}

(h : y &&& z = 0#w₂) :

theorem sshiftRight_or_eq_sshiftRight_sshiftRight_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}

(h : y &&& z = 0#w₂) :

tobiasgrosser · 2024-07-30T19:39:05Z

src/Init/Data/BitVec/Bitblast.lean

+  simp [sshiftRight', ← add_eq_or_of_and_eq_zero _ _ h,
+   toNat_add_of_and_eq_zero h, sshiftRight'_add]


Suggested change

simp [sshiftRight', ← add_eq_or_of_and_eq_zero _ _ h,

toNat_add_of_and_eq_zero h, sshiftRight'_add]

simp [sshiftRight', ← add_eq_or_of_and_eq_zero _ _ h,

toNat_add_of_and_eq_zero h, sshiftRight'_add]

src/Init/Data/BitVec/Lemmas.lean

tobiasgrosser · 2024-07-30T19:41:02Z

src/Init/Data/BitVec/Bitblast.lean

+theorem ushiftRight_or_eq_ushiftRight_ushiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}
+    (h : y &&& z = 0#w₂) :


Suggested change

theorem ushiftRight_or_eq_ushiftRight_ushiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}

(h : y &&& z = 0#w₂) :

theorem ushiftRight_or_eq_ushiftRight_ushiftRight_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}

(h : y &&& z = 0#w₂) :

tobiasgrosser · 2024-07-30T19:41:33Z

src/Init/Data/BitVec/Bitblast.lean

+      (ushiftRight_rec x y n) >>> (y &&& twoPow w₂ (n + 1)) := by
+  simp [ushiftRight_rec]
+
+theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) :


I am not a fan, but in the previous PR we marked this as simp, no?

tobiasgrosser · 2024-07-30T19:42:44Z

The PR message states that there are still open TODOs. Is this up-to-date?

tobiasgrosser · 2024-07-30T19:58:24Z

src/Init/Data/BitVec/Bitblast.lean

+  ushiftRight_rec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by
+  induction n generalizing x y


Suggested change

ushiftRight_rec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by

induction n generalizing x y

ushiftRight_rec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by

induction n generalizing x y

tobiasgrosser · 2024-07-30T19:58:43Z

src/Init/Data/BitVec/Bitblast.lean

+  sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by
+  induction n generalizing x y


Suggested change

sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by

induction n generalizing x y

sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by

induction n generalizing x y

tobiasgrosser · 2024-08-08T06:08:11Z

These were merged in leanprover#4872 and leanprover#4889.

bollu changed the base branch from master to upstream-shiftLeft-recurrence July 24, 2024 14:03

tobiasgrosser reviewed Jul 26, 2024

View reviewed changes

bollu force-pushed the upstream-shiftRight-recurrence branch from 185f53b to ffaa328 Compare July 30, 2024 19:17

bollu force-pushed the upstream-shiftRight-recurrence branch from ffaa328 to 80e05d8 Compare July 30, 2024 19:28

bollu changed the base branch from upstream-shiftLeft-recurrence to master July 30, 2024 19:28

tobiasgrosser reviewed Jul 30, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

tobiasgrosser reviewed Jul 30, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

tobiasgrosser reviewed Jul 30, 2024

View reviewed changes

bollu force-pushed the upstream-shiftRight-recurrence branch 2 times, most recently from a7c33b0 to 30a350a Compare July 30, 2024 19:56

feat: sshiftRight and ushiftRight bitblasting

d222874

bollu force-pushed the upstream-shiftRight-recurrence branch from 30a350a to d222874 Compare July 30, 2024 19:57

tobiasgrosser reviewed Jul 30, 2024

View reviewed changes

tobiasgrosser closed this Aug 8, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: shiftRight bitblasting theorems #11

feat: shiftRight bitblasting theorems #11

bollu commented Jul 24, 2024

tobiasgrosser commented Jul 30, 2024

bollu commented Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024 •

edited

Loading

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser commented Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser Jul 30, 2024

tobiasgrosser commented Aug 8, 2024

		theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) :
		x >>> y = x >>> y.toNat := by rfl

		theorem getLsb_ushiftRight' (x : BitVec w) (y : BitVec w₂) (i : Nat) :
		(x >>> y).getLsb i = x.getLsb (y.toNat + i) := by

		theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) :
		x >>> y = ushiftRight_rec x y (w₂ - 1) := by

		def sshiftRightRec (x : BitVec w) (y : BitVec w₂) (n : Nat) : BitVec w :=
		let shiftAmt := (y &&& (twoPow w₂ n))

		theorem sshiftRightRec_zero_eq (x : BitVec w) (y : BitVec w₂) :
		sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by

		theorem sshiftRightRec_succ_eq (x : BitVec w) (y : BitVec w₂) (n : Nat) :
		sshiftRightRec x y (n + 1) = (sshiftRightRec x y n).sshiftRight' (y &&& twoPow w₂ (n + 1)) := by

		theorem sshiftRight_or_eq_sshiftRight_sshiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}
		(h : y &&& z = 0#w₂) :

		simp [sshiftRight', ← add_eq_or_of_and_eq_zero _ _ h,
		toNat_add_of_and_eq_zero h, sshiftRight'_add]

		theorem ushiftRight_or_eq_ushiftRight_ushiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂}
		(h : y &&& z = 0#w₂) :

		ushiftRight_rec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by
		induction n generalizing x y

		sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by
		induction n generalizing x y

feat: shiftRight bitblasting theorems #11

feat: shiftRight bitblasting theorems #11

Conversation

bollu commented Jul 24, 2024

tobiasgrosser commented Jul 30, 2024

bollu commented Jul 30, 2024

Choose a reason for hiding this comment

tobiasgrosser Jul 30, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tobiasgrosser commented Jul 30, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tobiasgrosser commented Aug 8, 2024

tobiasgrosser Jul 30, 2024 •

edited

Loading