IEEE 754语义下，若x*y非2的幂，x*y == ((x*y)/y)*y是否恒成立？

这是此前问题的后续提问，加粗部分为新增限制条件。

问题描述 #

给定两个非零、有限的双精度（binary64）浮点数x和y，在默认¹IEEE 754语义下，若浮点数运算x * y的结果不是2的某次幂（即x * y的尾数用二进制表示时至少有两位被置1），判断以下等式是否始终成立：

x * y == ((x * y) / y) * y

已做验证 #

• 使用MPFR对半精度（binary16）浮点数的所有可能组合进行暴力检查，确认该断言在该范围内成立。
• 通过编程在binary64范围内（含非正规数区间）搜索了数十亿种可能，未找到反例，但无法证明断言的正确性。

已知结论 #

更简单的断言x == (x / y) * y和x == (x * y) / y均不成立，可轻松找到反例。

¹包含默认舍入模式：“四舍五入，偶进舍”

内容的提问来源于stack exchange，提问作者Hans Brende