Merge pull request #11765 from ethereum/fix_byte_formal

Fix implementation of BYTE

Author: chriseth

test/formal/byte_big.py

@@ -0,0 +1,18 @@
+from rule import Rule
+from opcodes import *
+
+"""
+byte(A, X) -> 0
+given A >= WordSize / 8
+"""
+
+rule = Rule()
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+
+rule.require(A >= n_bits / 8)
+rule.check(BYTE(A, X), 0)

test/formal/opcodes.py

@@ -59,4 +59,8 @@ def SAR(x, y):
 
 def BYTE(i, x):
 	bit = (i + 1) * 8
-	return If(UGT(bit, x.size()), BitVecVal(0, x.size()), (LShR(x, (x.size() - bit))) & 0xff)
+	return If(
+		UGT(i, x.size() / 8 - 1),
+		BitVecVal(0, x.size()),
+		(LShR(x, (x.size() - bit))) & 0xff
+	)