cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

An equivalence check for the Byte opcode

Browse Source 
Checks that the byte opcode (implemented using shift) is equivalent to a
canonical definition of byte using extract.
This commit is contained in:
hrkrshnn 2021-08-10 11:00:29 +02:00
parent 74c804d87d
commit a54addc2cb
1 changed files with 21 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
test/formal/byte_equivalence.py Normal file
View File

@ -0,0 +1,21 @@
from rule import Rule
from opcodes import *
"""
Checks that the byte opcode (implemented using shift) is equivalent to a
canonical definition of byte using extract.
"""
rule = Rule()
n_bits = 256
x = BitVec('X', n_bits)
for i in range(0, 32):
# For Byte, i = 0 corresponds to most significant bit
# But for extract i = 0 corresponds to the least significant bit
lsb = 31 - i
rule.check(
BYTE(BitVecVal(i, n_bits), x),
Concat(BitVecVal(0, n_bits - 8), Extract(8 * lsb + 7, 8 * lsb, x))
)