feat: shiftRight bitblasting theorems #11
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
bollu
force-pushed
the
upstream-shiftRight-recurrence
branch
from
185f53b to
ffaa328
Compare
|
This did not lead to a clean PR? Maybe update origin/master and merge origin/master? |
bollu
force-pushed
the
upstream-shiftRight-recurrence
branch
from
ffaa328 to
80e05d8
Compare
|
@tobiasgrosser clean now. |
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
449
to
450
| theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) : | ||
| x >>> y = x >>> y.toNat := by rfl |
There was a problem hiding this comment.
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 |
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
471
to
472
| theorem getLsb_ushiftRight' (x : BitVec w) (y : BitVec w₂) (i : Nat) : | ||
| (x >>> y).getLsb i = x.getLsb (y.toNat + i) := by |
There was a problem hiding this comment.
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 |
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
490
to
479
| theorem shiftRight_eq_shiftRight_rec (x : BitVec ℘) (y : BitVec w₂) : | ||
| x >>> y = ushiftRight_rec x y (w₂ - 1) := by |
There was a problem hiding this comment.
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 |
Comment on lines
+498
to
+487
| def sshiftRightRec (x : BitVec w) (y : BitVec w₂) (n : Nat) : BitVec w := | ||
| let shiftAmt := (y &&& (twoPow w₂ n)) |
There was a problem hiding this comment.
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)) |
Comment on lines
+505
to
+494
| theorem sshiftRightRec_zero_eq (x : BitVec w) (y : BitVec w₂) : | ||
| sshiftRightRec x y 0 = x.sshiftRight' (y &&& 1#w₂) := by |
There was a problem hiding this comment.
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 |
Comment on lines
+510
to
+499
| 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 |
There was a problem hiding this comment.
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 |
Comment on lines
+514
to
+503
| theorem sshiftRight_or_eq_sshiftRight_sshiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂} | ||
| (h : y &&& z = 0#w₂) : |
There was a problem hiding this comment.
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₂) : |
Comment on lines
+517
to
+506
| simp [sshiftRight', ← add_eq_or_of_and_eq_zero _ _ h, | ||
| toNat_add_of_and_eq_zero h, sshiftRight'_add] |
There was a problem hiding this comment.
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/Bitblast.lean
Outdated
Comment on lines
465
to
454
| theorem ushiftRight_or_eq_ushiftRight_ushiftRight_of_and_eq_zero {x : BitVec w} {y z : BitVec w₂} | ||
| (h : y &&& z = 0#w₂) : |
There was a problem hiding this comment.
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₂) : |
src/Init/Data/BitVec/Bitblast.lean
Outdated
| (ushiftRight_rec x y n) >>> (y &&& twoPow w₂ (n + 1)) := by | ||
| simp [ushiftRight_rec] | ||
|
|
||
| theorem ushiftRight_eq' (x : BitVec w) (y : BitVec w₂) : |
There was a problem hiding this comment.
I am not a fan, but in the previous PR we marked this as simp, no?
|
The PR message states that there are still open TODOs. Is this up-to-date? |
bollu
force-pushed
the
upstream-shiftRight-recurrence
branch
2 times, most recently
from
a7c33b0 to
30a350a
Compare
bollu
force-pushed
the
upstream-shiftRight-recurrence
branch
from
30a350a to
d222874
Compare
Comment on lines
+463
to
+464
| ushiftRight_rec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by | ||
| induction n generalizing x y |
There was a problem hiding this comment.
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 |
Comment on lines
+509
to
+510
| sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by | ||
| induction n generalizing x y |
There was a problem hiding this comment.
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 |
|
These were merged in leanprover#4872 and leanprover#4889. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
These theorems allow us to bitblast arithmetic and logical shift rights. The TODOS are yet to be addressed.