Hmm... can we introduce a hypothetical signed integer type HI that is wider than every actual integer type, and then just specify the effects by simple comparison after casting to HI?

If that was a possibility, might as well raise the operation to the mathematical domain.

If that was a possibility, might as well raise the operation to the mathematical domain.

I think raising it to the mathematical domain would be better than introducing such a hypothetical integer type, but I'm not sure how to word. One must consider ambiguity with the C++ less-than operator for example.

Returns: true if x is mathematically lower than y

Might work perhaps. However, I also don't see a strong reason to not just use a C++ equality. All equivalences which delegate to cmp_less or cmp_equal are very short as a result.

There's no need to say "mathematically". Saying "x is less than y" already implies that. There is no allowance for turning that into the C++ expression x > y, and if we did mean that, we'd have to say "true if x < y is true" (due to our specification rules), or simply Returns: x < y. If it says Returns: true if x is less than y then it means "mathematically". We could also use a math font < sign instead of code font <.

However, I think there is value in specying it in code, as it makes the required semantics very explicit and easily checkable. Doing it with an imaginary type means reasoning about a type that doesn't actually exist.

FWIW in GCC I implemented it exactly as proposed here. But I don't really have an opinion on whether to accept the change or not. Implementations are free to optimize it but the spec should be precise and unambiguous first, and clear to read as a close second. The current spec meets those requirements. In particular, I think the definition of cmp_less_equal is "obviously correct" at a glance, whereas the optimized version using cmp_less on the reversed arguments takes a second or two more to reason about. That's fine for a real implementation where the code has to actually execute. But we don't need to optimize for speed in the standard. I don't agree that using cmp_greater requires you to follow a longer chain of reasoning, because you don't need to inspect the implementation of cmp_greater to see that !cmp_greater(x, y) is obviously correct.

However, I think there is value in specying it in code, as it makes the required semantics very explicit and easily checkable. Doing it with an imaginary type means reasoning about a type that doesn't actually exist.

I agree.

But we don't need to optimize for speed in the standard. I don't agree that using cmp_greater requires you to follow a longer chain of reasoning, because you don't need to inspect the implementation of cmp_greater to see that !cmp_greater(x, y) is obviously correct.

You're probably right about that. I still think that the changes to the implementation of cmp_equal and cmp_less should be kept because it's more concise and arguably easier to understand than the old equivalence. I'll revert the change to cmp_less_equal

The current change (getting rid of the slightly funny blah ? false : something) looks ok to me, although I don't think there's a pressing need for a change.

@tkoeppe?