proof.py

from rule import Rule
from opcodes import *

rule = Rule()

for i in range(1, 25):
    X = BitVec('X', 8*i)
    Y = BitVec('Y', 8*i)
    max = 2**(8*i) - 1
    rule.check(
        SUB(AND(X, max), AND(Y, max)),
        AND(SUB(X, Y), max)
    )