runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Bitwise not operator gives wrong output #228

Closed nwatson22 closed 1 year ago

nwatson22 commented 1 year ago

The ~ operator is currently using the K ~Int operator, which is the bitwise negation operator in two's complement. However, TEAL uses unsigned bitwise negation, where all the preceding zeros to make the number take up the full 64 bits are treated as present. I don't think this should affect the other bitwise arithmetic opcodes (since we're dealing with only unsigned integers, &Int, |Int, and ^Int should never result in the leftmost bit getting set), but I'm less sure of the two bit shifting operations.