Fix implementation of BYTE

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)