runtimeverification / avm-semantics

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

bsqrt implementation #254

Closed nwatson22 closed 1 year ago

nwatson22 commented 1 year ago

This PR adds the bsqrt opcode. It is implemented in K by the sqrtUInt function. The bytes argument is converted to an int and then the square root is converted back into bytes. The sqrtTUInt64 function looks like it only works on integers <= MAX_UINT64, but this implementation should work on all nonnegative integers. It's possible we might be able to just hook both sqrt and bsqrt to this new implementation, but I'm not sure on that.