feat(EDyadic.DivRound): correctly-rounded EDyadic division

[bollu]

What

Adds EDyadic.divRound mode e s a b — fused, correctly-rounded division. Dyadics are not closed under division, so we long-divide with enough extra precision (≈ulp+3) and bake the remainder into a sticky bit:

1. Specials: x/0 → ±∞ (0/0 = NaN), ∞/∞ = NaN, ∞/finite = ∞, finite/∞ = 0, sign = sa xor sb.
2. Finite: left-shift |na| by p to reach ulp+3, capture q = (|na|<<p)/|nb|, r = …%|nb|.
3. Sticky: if r ≠ 0, OR 1 into q's low bit so the discarded tail is visible to the rounder.
4. Dyadic.round mode (ofIntWithPrec (±q) prec) e s.

This makes the result correctly rounded (not ~1 ulp). Tests in UnitTest/FP/EDyadic/DivRound.lean cover exact quotients, hand-verified inexact quotients at tiny formats, and specials.

Stack

Part of full-precision-floats-edyadic (patch 2/6). Base: #788.

🤖 Generated with Claude Code

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: ff0cad2	Previous: eb0390c	Ratio
add-fold-worklist/create	1782000 ns (± 15758)	2198000 ns (± 109413)	0.81
add-fold-worklist/rewrite	3342000 ns (± 19254)	3733000 ns (± 84672)	0.90
add-fold-worklist-local/create	1790000 ns (± 26520)	2191000 ns (± 99246)	0.82
add-fold-worklist-local/rewrite	2750000 ns (± 95929)	3011000 ns (± 27372)	0.91
add-zero-worklist/create	1833000 ns (± 68262)	2140500 ns (± 109777)	0.86
add-zero-worklist/rewrite	2167000 ns (± 55500)	2383000 ns (± 53970)	0.91
add-zero-reuse-worklist/create	1493000 ns (± 68964)	1798000 ns (± 63295)	0.83
add-zero-reuse-worklist/rewrite	1777000 ns (± 56316)	1965000 ns (± 30368)	0.90
mul-two-worklist/create	1833000 ns (± 60994)	2191000 ns (± 103104)	0.84
mul-two-worklist/rewrite	4778000 ns (± 96645)	5176000 ns (± 80037)	0.92
add-fold-forwards/create	1816000 ns (± 82600)	2174500 ns (± 97824)	0.84
add-fold-forwards/rewrite	2640000 ns (± 43741)	2967500 ns (± 35897)	0.89
add-zero-forwards/create	1775000 ns (± 8468)	2115000 ns (± 33441)	0.84
add-zero-forwards/rewrite	1793000 ns (± 53280)	1903000 ns (± 16300)	0.94
add-zero-reuse-forwards/create	1492000 ns (± 66654)	1832000 ns (± 91568)	0.81
add-zero-reuse-forwards/rewrite	1392000 ns (± 52419)	1555000 ns (± 50375)	0.90
mul-two-forwards/create	1807000 ns (± 81611)	2126000 ns (± 70864)	0.85
mul-two-forwards/rewrite	3349000 ns (± 164693)	3520000 ns (± 48872)	0.95
add-zero-reuse-first/create	1500500 ns (± 44884)	1827500 ns (± 94828)	0.82
add-zero-reuse-first/rewrite	10000 ns (± 3999)	8000 ns (± 1592)	1.25
add-zero-lots-of-reuse-first/create	1488000 ns (± 73345)	1773000 ns (± 69739)	0.84
add-zero-lots-of-reuse-first/rewrite	771000 ns (± 37762)	759000 ns (± 9407)	1.02

This comment was automatically generated by workflow using github-action-benchmark.