feat(EDyadic.Arith): exact add/sub/mul on EDyadic

[bollu]

What

Adds exact (unbounded) arithmetic on EDyadic: EDyadic.add, EDyadic.sub, EDyadic.mul with Add/Sub/Mul instances. Dyadics are closed under +/−/×, so these are computed exactly with no rounding.

• add: common scale K := max ka kb, numerator na·2^(K-ka) + nb·2^(K-kb), rebuilt via Dyadic.ofIntWithPrec; exact cancellation collapses to a (provisional) zero.
• sub a b := add a (-b).
• mul: ofIntWithPrec (na*nb) (ka+kb).
• IEEE specials: NaN propagates; ∞ + (−∞) = NaN; ∞ * 0 = NaN; sign rules incl. signed zeros.

Tests in UnitTest/FP/EDyadic/Arith.lean check exact values and special cases.

Note on the sign of an additive zero

This layer is mode-free, so it does not decide the sign of an additive zero (x + (−x), or mixed-sign zero operands). Per IEEE-754 §6.3 that sign is mode-dependent (+0 except RTN → −0), and a zero value no longer records its operands — so add returns a provisional zero and the mode-aware EDyadic.addRound (in the edyadicfloat-ops PR, #791) assigns the correct sign. mul's zero sign is the mode-independent xor and is set here.

Stack

Part of full-precision-floats-edyadic (patch 1/6). Base: round-edyadic-fastfloat (#787).

🤖 Generated with Claude Code

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: 5c33170	Previous: eb0390c	Ratio
add-fold-worklist/create	1805000 ns (± 91057)	2198000 ns (± 109413)	0.82
add-fold-worklist/rewrite	3431000 ns (± 87765)	3733000 ns (± 84672)	0.92
add-fold-worklist-local/create	1821000 ns (± 60108)	2191000 ns (± 99246)	0.83
add-fold-worklist-local/rewrite	2783000 ns (± 47752)	3011000 ns (± 27372)	0.92
add-zero-worklist/create	1893000 ns (± 94118)	2140500 ns (± 109777)	0.88
add-zero-worklist/rewrite	2153500 ns (± 36908)	2383000 ns (± 53970)	0.90
add-zero-reuse-worklist/create	1526000 ns (± 29107)	1798000 ns (± 63295)	0.85
add-zero-reuse-worklist/rewrite	1779000 ns (± 33279)	1965000 ns (± 30368)	0.91
mul-two-worklist/create	1851000 ns (± 73840)	2191000 ns (± 103104)	0.84
mul-two-worklist/rewrite	4815000 ns (± 157071)	5176000 ns (± 80037)	0.93
add-fold-forwards/create	1816000 ns (± 104679)	2174500 ns (± 97824)	0.84
add-fold-forwards/rewrite	2678000 ns (± 101787)	2967500 ns (± 35897)	0.90
add-zero-forwards/create	1789000 ns (± 89446)	2115000 ns (± 33441)	0.85
add-zero-forwards/rewrite	1749000 ns (± 61942)	1903000 ns (± 16300)	0.92
add-zero-reuse-forwards/create	1532000 ns (± 63113)	1832000 ns (± 91568)	0.84
add-zero-reuse-forwards/rewrite	1508000 ns (± 63859)	1555000 ns (± 50375)	0.97
mul-two-forwards/create	1829000 ns (± 33144)	2126000 ns (± 70864)	0.86
mul-two-forwards/rewrite	3245000 ns (± 118008)	3520000 ns (± 48872)	0.92
add-zero-reuse-first/create	1521000 ns (± 60986)	1827500 ns (± 94828)	0.83
add-zero-reuse-first/rewrite	10000 ns (± 2149)	8000 ns (± 1592)	1.25
add-zero-lots-of-reuse-first/create	1524500 ns (± 52960)	1773000 ns (± 69739)	0.86
add-zero-lots-of-reuse-first/rewrite	807000 ns (± 60488)	759000 ns (± 9407)	1.06

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