feat(EDyadicFloat): EDyadicFloat type with ofPackedFloat/toPackedFloat

[bollu]

What

Adds the high-precision float model EDyadicFloat e s mode — a structure wrapping an EDyadic value held representable in (e, s) — mirroring FastFloat, plus:

• EDyadic.round mode e s : EDyadic → EDyadic (specials pass through; nonzeroFinite d _ → Dyadic.round mode d e s).
• EDyadicFloat.ofEDyadic / ofPackedFloat pf := ⟨pf.toEDyadic⟩ / toPackedFloat x := EDyadic.pack e s x.value.

This completes the FP story: PackedFloat (storage) → EDyadic (exact math) → EDyadicFloat (rounded math). Tests in UnitTest/FP/EDyadicFloat.lean check toPackedFloat ∘ ofPackedFloat = id on representable inputs, ofEDyadic rounding, and specials.

Stack

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

🤖 Generated with Claude Code

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: 44444b7	Previous: eb0390c	Ratio
add-fold-worklist/create	1818000 ns (± 80189)	2198000 ns (± 109413)	0.83
add-fold-worklist/rewrite	3358000 ns (± 43359)	3733000 ns (± 84672)	0.90
add-fold-worklist-local/create	1823000 ns (± 9711)	2191000 ns (± 99246)	0.83
add-fold-worklist-local/rewrite	2772000 ns (± 56509)	3011000 ns (± 27372)	0.92
add-zero-worklist/create	1867000 ns (± 53966)	2140500 ns (± 109777)	0.87
add-zero-worklist/rewrite	2163000 ns (± 34680)	2383000 ns (± 53970)	0.91
add-zero-reuse-worklist/create	1518000 ns (± 53864)	1798000 ns (± 63295)	0.84
add-zero-reuse-worklist/rewrite	1745000 ns (± 40127)	1965000 ns (± 30368)	0.89
mul-two-worklist/create	1826000 ns (± 80643)	2191000 ns (± 103104)	0.83
mul-two-worklist/rewrite	5102000 ns (± 186911)	5176000 ns (± 80037)	0.99
add-fold-forwards/create	1815000 ns (± 69936)	2174500 ns (± 97824)	0.83
add-fold-forwards/rewrite	2624000 ns (± 44415)	2967500 ns (± 35897)	0.88
add-zero-forwards/create	1809000 ns (± 78932)	2115000 ns (± 33441)	0.86
add-zero-forwards/rewrite	1746000 ns (± 71111)	1903000 ns (± 16300)	0.92
add-zero-reuse-forwards/create	1514000 ns (± 16456)	1832000 ns (± 91568)	0.83
add-zero-reuse-forwards/rewrite	1391000 ns (± 14450)	1555000 ns (± 50375)	0.89
mul-two-forwards/create	1830000 ns (± 77652)	2126000 ns (± 70864)	0.86
mul-two-forwards/rewrite	3231000 ns (± 73616)	3520000 ns (± 48872)	0.92
add-zero-reuse-first/create	1523000 ns (± 71079)	1827500 ns (± 94828)	0.83
add-zero-reuse-first/rewrite	10000 ns (± 1852)	8000 ns (± 1592)	1.25
add-zero-lots-of-reuse-first/create	1524000 ns (± 57648)	1773000 ns (± 69739)	0.86
add-zero-lots-of-reuse-first/rewrite	780000 ns (± 35830)	759000 ns (± 9407)	1.03

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