mirror of
https://github.com/boykopovar/AnyPS5.git
synced 2026-11-03 12:57:27 +00:00
A v_mul_f32 in a FLOAT_MODE that flushes f32 denormals emits the nearest-even tininess check, the NaN result selection and then a result flush. The check already turns every product that rounds below 2^-126 into a zero of its sign, so the flush can't change what it keeps. DenormalFlushEliminator now proves that: a select arm guarded by the tiny-product check of the same denormal-free factors, an arm a select takes only when its own bits are NaN, and an and with a mask that has no significand bits are denormal-free. Co-Authored-By: Claude Opus 5.5 <[email protected]>