No, that's not a refinement. What it means is that if the initial IR says "add x and y, and if it overflows return anything at all", then you can refine that to

No, that's not a refinement. What it means is that if the initial IR says "add x and y, and if it overflows return anything at all", then you can refine that to "add x and y, with wraparound at 2^64" because the latter has a subset of the behavior of the former.