Executable addition and subtraction backends

The generic path handles exact finite arithmetic and the descriptor's exceptional-value policy. The word dispatcher first tries a kernel justified by structural capabilities (native binary32 or binary64, a fixed pair of limbs, the one-word UInt64 kernel for small IEEE formats, or reusable small-word storage for the remaining one-word formats) and returns to that generic path when the specialization declines.

The @[specialize fmt] annotation exposes descriptor-dependent tests to specialization at closed-format call sites. The choice of kernel depends only on the descriptor; operand-dependent acceptance checks remain in the selected kernels. A runtime descriptor is checked on each call.

Refinement theorems live in Add.Proof, so runtime clients can import this module separately.

def FloatLib.Floats.Formats.BinaryInterchange.Model.AddBackend.generic {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Width-generic compiled addition.

Finite operands use the compact component decoder; exceptional operands retain the public NaN and infinity policy.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AddBackend.word {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Non-table implementation of addition.

Specialized kernels are selected by structural capabilities. Binary32 finite operands use the checked native-word backend. Binary64 first tries the one-word UInt64 kernel of NativeSmallWordAdd, whose capacity contract admits its 53-bit significands, and falls back to its fixed-format chain for wide alignment shifts and boundary results. Eligible two-word layouts use their fixed-limb and width-generic finite chain. Every other IEEE format with at most 30 exponent and 61 fraction bits adds entirely in UInt64 through NativeSmallWordAdd; the remaining one-word IEEE formats use the shared native-storage decoder before the compiled component kernel. Every decline and every exceptional case enters the single exact generic baseline here.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AddBackend.subWord {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Non-table implementation of subtraction.

Binary32 enters its checked native backend directly; binary64 first tries the one-word UInt64 kernel with the right sign toggled in the storage word and then its fixed-format chain. Eligible two-word layouts use their fixed-limb and width-generic finite subtraction chain. Every other one-word IEEE format with at most 30 exponent and 61 fraction bits subtracts through NativeSmallWordAdd; the remaining one-word formats use the shared native decoder on the negated operand. Exceptional cases enter exact generic addition with the negated right operand.