Two-word subtraction runtime

The two-word subtraction runtime combines the equal-exponent kernel with a complete finite candidate chain for every eligible layout. It reuses the pair-kernel storage layer; correctness proofs are isolated in Subtraction.Proof.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subNormalSameExponent? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Try exact native subtraction of same-sign normal operands with the same exponent.

An accepted nonzero result remains normal. Exact cancellation returns positive zero; a nonzero subnormal difference is left to the generic implementation.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.subFinite? {fmt : FloatFormat} (x y : Model fmt) : Option (Model fmt)

Evaluate finite two-word subtraction.

The fixed-limb equal-exponent kernel is attempted first. Every remaining finite case uses generic exact addition with a negated right operand; exceptional inputs remain visible to the dispatcher. Descriptor specialization follows the pattern described in Dispatch.Add.Runtime.