(x << 2) >> 2 masks top bits (logical shift).
(self, kernel)
| 707 | assert prove(claim) |
| 708 | |
| 709 | def test_shift_left_right(self, kernel): |
| 710 | """(x << 2) >> 2 masks top bits (logical shift).""" |
| 711 | x = BitVec("x", 8) |
| 712 | # Logical shift: LShR(x << 2, 2) == x & 0x3F |
| 713 | claim = ForAll([x], LShR(x << 2, 2) == (x & BitVecVal(0x3F, 8))) |
| 714 | assert prove(claim) |
| 715 | |
| 716 | def test_rotate_left_right_inverse(self, kernel): |
| 717 | """RotateRight(RotateLeft(x, 3), 3) == x.""" |