Native binary64 subtraction runtime

The signed Sterbenz kernels live here; their refinement proofs are isolated in Subtraction.Proof.

The routines accept normal operands of the same sign whose magnitudes lie within a factor of two. Their exact difference fits in one native word, including when the result is subnormal. Other inputs are left to the arithmetic dispatcher.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.packExactDifference (sign : Bool) (difference exponent : UInt64) : Value

Pack an exact significand difference below 2^53 at an encoded exponent in 1..2046.

The represented magnitude is difference * 2^(exponent - 1075), with the exponent subtraction in Int. Zero becomes positive zero. Nonzero results below the minimum normal value are packed as subnormals; all other results are normalized without rounding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.subSterbenz? (x y : Value) : Option Value

Try exact subtraction of positive normal binary64 values in Sterbenz's factor-two region.

The same-exponent case aligns immediately. Adjacent exponents are accepted precisely when the significand of the larger operand is no greater than that of the smaller operand, which is the native field form of the factor-two condition.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.subSignedSterbenz? (x y : Value) : Option Value

Try exact Sterbenz subtraction for same-sign normal binary64 inputs.

Positive operands use subSterbenz? directly. Negative operands are negated and swapped so the same proved positive kernel computes x - y with the correct result sign.