fix shift_rot formal proof