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, and 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 fixes the binary semantics shared with the generic kernels, including the default bias. 64 < fracWidth fills the low word with fraction bits and puts the sign, the exponent field, and the upper fraction bits in the high word, so only the fraction spans both words. The same bound keeps every four-limb product-rounding shift strictly above one word. bitWidth ≤ 128 bounds the storage to two words.

@[instance_reducible, inline]

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

Decide eligibility from the descriptor fields.

Written as an inline if, the decision simplifies 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.packNormalWords (fmt : FloatFormat) (sign : Bool) (exponent : UInt64) (mantissa : Numerics.FixedWord.UInt128) : Numerics.FixedWord.UInt128

The two storage words of a finite normal result with the given sign, exponent, and significand.

Packing masks the exponent to the exponent field, and the high fraction mask discards the significand's implicit bit. Two-word carriers store these words as they are.

@[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 from its native exponent and significand words.

The result is meaningful when the exponent fits the field and the significand is normal, the contract that packNormal_eq_ofFields in Core.Proof states.