Is unsigned integer subtraction defined behavior?

The result of a subtraction generating a negative number in an unsigned type is well-defined:

1. [...] A computation involving unsigned operands can never overflow, because a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type. (ISO/IEC 9899:1999 (E) §6.2.5/9)

As you can see, (unsigned)0 - (unsigned)1 equals -1 modulo UINT_MAX+1, or in other words, UINT_MAX.

Note that although it does say "A computation involving unsigned operands can never overflow", which might lead you to believe that it applies only for exceeding the upper limit, this is presented as a motivation for the actual binding part of the sentence: "a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type." This phrase is not restricted to overflow of the upper bound of the type, and applies equally to values too low to be represented.

Well, the first interpretation is correct. However, your reasoning about the "signed semantics" in this context is wrong.

Again, your first interpretation is correct. Unsigned arithmetic follow the rules of modulo arithmetic, meaning that 0x0000 - 0x0001 evaluates to 0xFFFF for 32-bit unsigned types.

However, the second interpretation (the one based on "signed semantics") is also required to produce the same result. I.e. even if you evaluate 0 - 1 in the domain of signed type and obtain -1 as the intermediate result, this -1 is still required to produce 0xFFFF when later it gets converted to unsigned type. Even if some platform uses an exotic representation for signed integers (1's complement, signed magnitude), this platform is still required to apply rules of modulo arithmetic when converting signed integer values to unsigned ones.

For example, this evaluation

signed int a = 0, b = 1;
unsigned int c = a - b;

is still guaranteed to produce UINT_MAX in c, even if the platform is using an exotic representation for signed integers.

When you work with unsigned types, modular arithmetic (also known as "wrap around" behavior) is taking place. To understand this modular arithmetic, just have a look at these clocks:

9 + 4 = 1 (13 mod 12), so to the other direction it is: 1 - 4 = 9 (-3 mod 12). The same principle is applied while working with unsigned types. If the result type is unsigned, then modular arithmetic takes place.

---

Now look at the following operations storing the result as an unsigned int:

unsigned int five = 5, seven = 7;
unsigned int a = five - seven;      // a = (-2 % 2^32) = 4294967294 

int one = 1, six = 6;
unsigned int b = one - six;         // b = (-5 % 2^32) = 4294967291

When you want to make sure that the result is signed, then stored it into signed variable or cast it to signed. When you want to get the difference between numbers and make sure that the modular arithmetic will not be applied, then you should consider using abs() function defined in stdlib.h:

int c = five - seven;       // c = -2
int d = abs(five - seven);  // d =  2

Be very careful, especially while writing conditions, because:

if (abs(five - seven) < seven)  // = if (2 < 7)
    // ...

if (five - seven < -1)          // = if (-2 < -1)
    // ...

if (one - six < 1)              // = if (-5 < 1)
    // ...

if ((int)(five - seven) < 1)    // = if (-2 < 1)
    // ...

but

if (five - seven < 1)   // = if ((unsigned int)-2 < 1) = if (4294967294 < 1)
    // ...

if (one - six < five)   // = if ((unsigned int)-5 < 5) = if (4294967291 < 5)
    // ...