The specification of the \relaxedtrunc^u/s operators is missing cases for positive/negative infinity. Likewise, the explainer does not consider these cases in its Python pseudo code. I assume the intended semantics is analogous to that of out-of-range, is that correct?