[amavect]

Cool!! I really like how the overflow condition reads. "When the source and destination have the same sign, but the result a different sign, then signed addition overflows."

x86 has SETC/SETNC and SETO/SETNO to pull the carry/overflow bits out of the status register.

  u+: ADD then SETNC
  u-: CMP then SETNC
  s+: ADD then SETNO
  s-: CMP then SETNO

C23 adds checked arithmetic, and gcc implements them as built-in, generating SETO/SETNO. I can't find a way to generate SETNO otherwise. https://godbolt.org/z/4EjecdW1d

  #include <stdint.h>
  #include <stdckdint.h>

  int add_u(unsigned x, unsigned y){
    return x <= ~y;
  }
  int sub_u(unsigned x, unsigned y) {
    return x <= y;
  }
  int add_u2(unsigned x, unsigned y){
    return !ckd_add(&x, x, y);
  }
  int sub_u2(unsigned x, unsigned y) {
    return !ckd_sub(&x, x, y);
  }
  int add_s(int x, int y){
    return !ckd_add(&x, x, y);
  }
  int sub_s(int x, int y) {
    return !ckd_sub(&x, x, y);
  }

Now, I the difficulty you talk about goes deeper than high level language semantics. Math and predicate logic can't easily talk about a carry flag or an overflow flag. Math equivocates unsigned comparisons with signed comparisons: unsigned < means carry flag, signed < means sign flag != overflow flag. Thus, by coincidence, unsigned < can talk about carry, but < cannot talk about only overflow (without the sign flag). Furthermore, a theorem-proving language wants to prove that overflow cannot happen before attempting to calculate it.

So, despite you clearly showing that carry and overflow have the same calculation cost, I don't know how to represent those predicates in a usual math language with equal symbol length or complexity.

[kazinator]

The important thing isn't the flag (piece of CPU state) but the function which calculates it from the two inputs and result. That is a pure Boolean function: do these three values indicate signed overflow or unsigned carry?

  int a = b + c; // safe version, like ADD on Motorola 68K.

  if (add_overflow_int(a, b, c)) ... macro/function determines overflow

The compiler could optimize that into accessing a flag, if the three inputs were just involved in an addition. In the general case, it has to emit the logic to test the bits of a, b, c.