Ноль с плавающей запятой в реализациях C (инварианты IEEE 754?)

Упоминание C11 просто сбивает с толку ваш вопрос, потому что IEEE 754 не требуется ни одним стандартом C.

При этом, просто предполагая 32-битные числа с плавающей запятой IEEE 754 и не делая никаких предположений о x2 и y2 (кроме того, что они не бесконечны или NaN), вы не можете предположить, что все биты результата будут равны 0. Числа IEEE 754 имеют два нуля, один отрицательный и один положительный, и если выражение (y2 - y0) - (x2 - x0) отрицательное, результатом умножения его на ноль будет отрицательный нуль.

Мы можем проверить это на этом коротком примере:

#include <stdio.h>
#include <stdint.h>

int
main(int argc, char **argv)
{
    union {
        float f;
        uint32_t i;
    } foo;

    float a = 0;
    float b = -1;

    foo.f = a * b;
    printf("0x%x\n", foo.i);

    return 0;
}

Результат (заметьте, никаких оптимизаций, так как я не хочу, чтобы компилятор был умным):

$ cc -o foo foo.c && ./foo
0x80000000

О, я только что заметил, что вторая часть вашего вопроса, которую вы назвали «другими словами», на самом деле не является другими словами, потому что это другой вопрос.

Начать с:

(*(uint32_t*)(&a) == *(uint32_t*)(&b))

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