Определено ли поведение вычитания беззнакового целого?

Я наткнулся на код человека, который, кажется, считает, что существует проблема вычитания беззнакового числа из другого целого того же типа, когда результат будет отрицательным. Таким образом, подобный код будет некорректен, даже если он работает на большинстве архитектур.

unsigned int To, Tf;

To = getcounter();
while (1) {
    Tf = getcounter();
    if ((Tf-To) >= TIME_LIMIT) {
        break;
    } 
}

Это единственная смутно релевантная цитата из стандарта Си, которую я смог найти.

Вычисления с использованием неподписанных операндов никогда не могут переполняться, потому что результат, который не может быть представлен результирующим беззнаковым целым числом тип уменьшается по модулю число, которое на один больше самого большого значение, которое может быть представлено результирующим типом.

Я полагаю, что эту кавычку можно принять как означающую, что когда правый операнд больше, операция корректируется, чтобы быть осмысленной в контексте модуло-усеченных чисел.

т.е.

0x0000 - 0x0001 == 0x 1 0000 - 0x0001 == 0xFFFF

в отличие от использования зависимой от реализации знаковой семантики:

0x0000 - 0x0001 == (беззнаковой)(0 + -1) == (0xFFFFF, но также 0xFFFE или 0x8001)

Какая или какая интерпретация правильная? Она вообще определена?