> multiplying two 32-bit values, recast as 64-bit signed integers, will not overflow

Factually wrong. Consider: (int64_t)0xFFFFFFFF * (int64_t)0xFFFFFFFF. It definitely overflows.