Native one-word finite multiplication

The executable normal multiplication path here serves conventional IEEE formats whose storage, exponent, and significand intermediates fit in UInt64. Refinement proofs live in Mul.Proof.

The kernel declines exceptional, zero, and subnormal operands, products below the normal threshold before rounding, and overflow after rounding. The dispatcher handles those cases with the generic implementation. Each accepted result agrees with its correctly rounded finite-product result.

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.Eligible (fmt : FloatFormat) : Prop

Capacity contract for exact UInt64 normal multiplication.

Two normalized significands of at most 32 bits have an exact product of at most 64 bits. This is one fraction bit wider than the conservative contract shared with native division.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.instDecidableEligible (fmt : FloatFormat) : Decidable (Eligible fmt)

Product eligibility is decided from the descriptor fields; the conditional form is inlined and can be simplified for a closed format (see NativeSmallWord.StorageEligible).

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.declineWord : UInt64

Decline sentinel at bit 63, above every storage word admitted by Eligible.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.roundNormalProduct? (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) : Option (Model fmt)

Round an exact product of two normal finite significands in native words.

For eligible formats and normalized operands, none means the product is below the normal threshold before rounding or overflows after rounding. These cases use the generic rounder.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.roundNormalProductWord (fmt : FloatFormat) (sign : Bool) (xExponent yExponent xMantissa yMantissa : UInt64) : UInt64

Word-valued execution view of roundNormalProduct?.

The high decline bit is reserved as a sentinel. Every successful result is normal and cannot use that word for an eligible format.

@[inline]

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

Decode two normal finite values and try the reusable one-word product path.

Exceptional, zero, and subnormal operands return none before any significand arithmetic.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeSmallWordMul.mulNormalWord {fmt : FloatFormat} (x y : Model fmt) : UInt64

Word-valued execution view of mulNormal?.

Successful results stay in native fields until the final packed word. declineWord means the caller must use the general exact path.