New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Symbolic bit rotates by more than word size have wrong semantics #160

Closed

brianhuffman opened this issue Jan 16, 2015 · 0 comments

Contributor

brianhuffman commented Jan 16, 2015

Rotation of a bitvector x : [n] works correctly for rotation amounts less than n, but not for n or above:

Cryptol> 0x01 <<< 8 == 0x01
True
Cryptol> :prove 0x01 <<< 8 == 0x01
(0x01 <<< 8 == 0x01) = False

Currently, rotations by n or more result in zero:

Cryptol> :sat (==) [ 0x8 <<< (i:[3]) | i <- [0..7] ]
(==) [0x8 <<< (i : [3]) | i <- [0 .. 7]] [0x8, 0x1, 0x2, 0x4, 0x0,
                                          0x0, 0x0, 0x0] = True

The correct behavior would be to reduce the rotation amount modulo n before doing the rotation.

The text was updated successfully, but these errors were encountered:

brianhuffman closed this as completed in

ae219c2

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment