add OP_CMPB formal proof