You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
round_float with TiesToAway rounds inputs just below half the smallest subnormal up #67
Hi! I was comparing gfloat's P3109 rounding with FloatLib, a Lean library for these formats, and found a small difference between round_float and round_ndarray.
For K = 8, P = 3, signed, extended, the smallest positive value is 2^-17. An input just below half of that should round to 0 under TiesToAway. round_ndarray returns 0, but round_float returns 2^-17:
Reproduced on main at caea0b1a, with Python 3.12.13 and NumPy 2.5.4.
Here delta is 0.5 - 2^-54, and delta + 0.5 rounds to 1.0 in binary64. The fix in src/gfloat/round.py appears to be the comparison round_ndarray.py already uses:
With this change round_float and round_ndarray agree on inputs below, at and above the midpoint, for both signs. I'm happy to send a PR with a regression test :)
Activity
awf commentedon Oct 18, 2026
Thanks! Taking a look.
awf commentedon Oct 18, 2026
Copilot auto-fix did as predicted, so I've merged it.