feat(EDyadicFloat): add/sub/mul/div with correctly-rounded results

[bollu]

What

Adds arithmetic to EDyadicFloat: mul computes exactly on EDyadic then rounds once; div uses the fused EDyadic.divRound. add/sub use the new mode-aware EDyadic.addRound, which forms the exact sum and then applies both the magnitude rounding and the IEEE-754 §6.3 sign-of-zero rule. Provides Add/Sub/Mul/Div instances. Each operation yields the correctly-rounded result for (e, s) under mode.

addRound / addZeroSign

The sign of an additive zero is mode-dependent (+0 except RTN → −0), and a zero value can't record the operands that produced it — so it can't be recovered by the value-level rounder. addRound mirrors divRound: exact core (EDyadic.add) + mode-aware finalization. addZeroSign keeps a like-signed zero pair's sign and otherwise defers to the mode. (mul needs none of this — its zero sign is the mode-independent xor.)

Tests extend UnitTest/FP/EDyadicFloat.lean with round-trip arithmetic #guards and a section pinning the additive-zero sign across .RNE vs .RTN (cancellation, mixed-sign zeros, like-signed zeros).

Stack

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

🤖 Generated with Claude Code

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: c641963	Previous: eb0390c	Ratio
add-fold-worklist/create	2207000 ns (± 92696)	2198000 ns (± 109413)	1.00
add-fold-worklist/rewrite	3804000 ns (± 79515)	3733000 ns (± 84672)	1.02
add-fold-worklist-local/create	2168000 ns (± 69590)	2191000 ns (± 99246)	0.99
add-fold-worklist-local/rewrite	3083000 ns (± 36942)	3011000 ns (± 27372)	1.02
add-zero-worklist/create	2176000 ns (± 64834)	2140500 ns (± 109777)	1.02
add-zero-worklist/rewrite	2358000 ns (± 28693)	2383000 ns (± 53970)	0.99
add-zero-reuse-worklist/create	1840000 ns (± 88696)	1798000 ns (± 63295)	1.02
add-zero-reuse-worklist/rewrite	1991000 ns (± 46922)	1965000 ns (± 30368)	1.01
mul-two-worklist/create	2202000 ns (± 33178)	2191000 ns (± 103104)	1.01
mul-two-worklist/rewrite	5345000 ns (± 94859)	5176000 ns (± 80037)	1.03
add-fold-forwards/create	2228000 ns (± 107777)	2174500 ns (± 97824)	1.02
add-fold-forwards/rewrite	2974000 ns (± 59174)	2967500 ns (± 35897)	1.00
add-zero-forwards/create	2183000 ns (± 88267)	2115000 ns (± 33441)	1.03
add-zero-forwards/rewrite	1907000 ns (± 22309)	1903000 ns (± 16300)	1.00
add-zero-reuse-forwards/create	1734000 ns (± 49541)	1832000 ns (± 91568)	0.95
add-zero-reuse-forwards/rewrite	1525000 ns (± 36760)	1555000 ns (± 50375)	0.98
mul-two-forwards/create	2173500 ns (± 118997)	2126000 ns (± 70864)	1.02
mul-two-forwards/rewrite	3642000 ns (± 122584)	3520000 ns (± 48872)	1.03
add-zero-reuse-first/create	1820000 ns (± 88414)	1827500 ns (± 94828)	1.00
add-zero-reuse-first/rewrite	8000 ns (± 4612)	8000 ns (± 1592)	1
add-zero-lots-of-reuse-first/create	1856000 ns (± 56409)	1773000 ns (± 69739)	1.05
add-zero-lots-of-reuse-first/rewrite	781000 ns (± 34326)	759000 ns (± 9407)	1.03

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