Two-word pair-kernel storage runtime

The structural eligibility predicate and field helpers provide the storage interface shared by the fixed-limb arithmetic kernels. A value of an eligible format is split into a high and a low UInt64. The low word is entirely fraction; the high word holds the remaining fracWidth - 64 fraction bits, then the exponent field, then the sign. Every field position is derived from the descriptor, so one kernel serves every eligible layout, with 68 to 128 encoded bits and a fraction wider than one word. The correspondence with the width-generic carrier is proved in Core.Proof.

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

Structural capability required by the two-word kernels.

The conventional IEEE encoding selects the exact binary semantics shared with the generic kernels, and in particular the default bias. 64 < fracWidth places the sign, the exponent field, and the upper fraction bits in the high word and fills the low word with fraction bits. Only the fraction spans both words; the exponent and sign are contained in the high word. The fraction-width bound also keeps every four-limb product-rounding shift strictly above one word. bitWidth ≤ 128 bounds the storage to two words. Layouts whose fraction has at most 64 bits are outside this capability.

@[instance_reducible, inline]

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

Decide eligibility from the descriptor fields.

The explicit conditional and @[inline] annotation expose the decision to simplification at closed-format call sites.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracHighWidth (fmt : FloatFormat) : UInt64

Number of fraction bits stored in the high word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracHighMask (fmt : FloatFormat) : UInt64

Mask selecting the fraction bits stored in the high word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.expAllOnes (fmt : FloatFormat) : UInt64

The all-ones exponent field as a native word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.implicitBit (fmt : FloatFormat) : UInt64

The implicit leading significand bit 2^fracWidth, in high-word coordinates.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.signMask (fmt : FloatFormat) : UInt64

The sign bit 2^(expWidth + fracWidth), in high-word coordinates.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.toWords {fmt : FloatFormat} (x : Model fmt) : Numerics.FixedWord.UInt128

Split a stored value into its high and low native words.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.ofWords (fmt : FloatFormat) (words : Numerics.FixedWord.UInt128) : Model fmt

Join two native words into a stored value, keeping the low bitWidth bits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.signBit (fmt : FloatFormat) (high : UInt64) : Bool

Extract the sign from the high storage word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.expField (fmt : FloatFormat) (high : UInt64) : UInt64

Extract the biased exponent field from the high storage word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracHigh (fmt : FloatFormat) (high : UInt64) : UInt64

Extract the fraction bits held in the high storage word.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalMantissa (fmt : FloatFormat) (high low : UInt64) : Numerics.FixedWord.UInt128

Add the implicit bit to the two fraction limbs of a normal value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.implicitMantissa (fmt : FloatFormat) : Numerics.FixedWord.UInt128

The two-limb significand 2^fracWidth, the smallest normal significand.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.carryMantissa (fmt : FloatFormat) : Numerics.FixedWord.UInt128

The two-limb value 2^(fracWidth + 1) produced when nearest-even rounding carries out.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.isCarry (fmt : FloatFormat) (rounded : Numerics.FixedWord.UInt128) : Bool

Whether a rounded two-limb significand carried out to 2^(fracWidth + 1).

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalizeCarry (fmt : FloatFormat) (carry : Bool) (rounded : Numerics.FixedWord.UInt128) : Numerics.FixedWord.UInt128

Replace a carried-out significand by 2^fracWidth, leaving other significands unchanged.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.packNormal (fmt : FloatFormat) (sign : Bool) (exponent : UInt64) (mantissa : Numerics.FixedWord.UInt128) : Model fmt

Pack a finite normal result directly from its native exponent and significand words.

The exponent is masked to the exponent field, and the significand's implicit bit is discarded by the high fraction mask. The result is meaningful when the exponent fits the field and the significand is normal; Core.Proof.packNormal_eq_ofFields states that contract.