Correctness of native-word addition for generic binary32

The direct UInt64 addition kernel is proved equivalent to its exact-dyadic finite specification. Runtime clients can import Addition.Runtime without the alignment, packing, and rounding proof developments.

For exponent gaps at most 39, alignment and signed addition are exact in one word. For larger gaps, the smaller operand cannot change nearest-even rounding of the larger operand, including at a binade boundary. Both cases refine the same binary32 specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.addFiniteImpl_eq (x y : Value) : addFiniteImpl? x y = addFinite? x y

The direct UInt64 finite addition kernel equals the generic exact-dyadic implementation.

Non-finite operands return none, and zero operands use the exact-dyadic kernel. For nonzero finite operands, a gap of at most 39 permits an exact left shift of the larger-scale significand to the smaller scale. A larger gap rounds to the dominant operand for either choice of signs.