Two-word pair-kernel storage

The field helpers in Core.Runtime agree with the width-generic carrier under NativePair.Eligible. The eligibility bounds ensure that field extraction and packing do not lose bits to native-word overflow.

packNormal_eq_ofFields relates native packing to the canonical field constructor for an in-range exponent field and a normalized significand. decode_of_normalExponent gives the finite components when the exponent is nonzero and not all ones. These contracts apply to binary128 and every other eligible descriptor.

Layout bounds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.isIEEE {fmt : FloatFormat} (h : Eligible fmt) : fmt.isIEEE = true

An eligible descriptor uses the conventional IEEE encoding and bias.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.frac_gt {fmt : FloatFormat} (h : Eligible fmt) : 64 < fmt.fracWidth

An eligible fraction is wider than one word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.width_le {fmt : FloatFormat} (h : Eligible fmt) : fmt.bitWidth ≤ 128

An eligible descriptor fits in two words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.sum_le {fmt : FloatFormat} (h : Eligible fmt) : fmt.expWidth + fmt.fracWidth ≤ 127

The exponent and fraction of an eligible descriptor share at most 127 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.frac_le {fmt : FloatFormat} (h : Eligible fmt) : fmt.fracWidth ≤ 125

An eligible fraction has at most 125 bits, since the exponent field has at least two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.exp_le {fmt : FloatFormat} (h : Eligible fmt) : fmt.expWidth ≤ 62

An eligible exponent field has at most 62 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.encoding {fmt : FloatFormat} (h : Eligible fmt) : fmt.encoding = FloatFormat.Encoding.ieee

An eligible descriptor uses the IEEE exceptional-value encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.exponentBias_eq {fmt : FloatFormat} (h : Eligible fmt) : fmt.exponentBias = fmt.bias

An eligible descriptor uses the conventional bias.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.Eligible.bias_lt {fmt : FloatFormat} (h : Eligible fmt) : fmt.bias < 2 ^ 61

The bias of an eligible descriptor is below 2^61.

Layout constants

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracHighWidth_toNat {fmt : FloatFormat} (h : Eligible fmt) : (fracHighWidth fmt).toNat = fmt.fracWidth - 64

The high word holds fracWidth - 64 fraction bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracHighMask_toNat {fmt : FloatFormat} (h : Eligible fmt) : (fracHighMask fmt).toNat = 2 ^ (fmt.fracWidth - 64) - 1

The high fraction mask is 2^(fracWidth - 64) - 1.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.expAllOnes_toNat {fmt : FloatFormat} (h : Eligible fmt) : (expAllOnes fmt).toNat = fmt.expAllOnesNat

The native all-ones exponent field is the descriptor's all-ones exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.implicitBit_toNat {fmt : FloatFormat} (h : Eligible fmt) : (implicitBit fmt).toNat = 2 ^ (fmt.fracWidth - 64)

The implicit bit sits at high-word position fracWidth - 64.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.carryBit_toNat {fmt : FloatFormat} (h : Eligible fmt) : (implicitBit fmt <<< 1).toNat = 2 ^ (fmt.fracWidth - 63)

The carry bit sits at high-word position fracWidth - 63.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.signMask_toNat {fmt : FloatFormat} (h : Eligible fmt) : (signMask fmt).toNat = 2 ^ (fmt.expWidth + fmt.fracWidth - 64)

The sign bit sits at high-word position expWidth + fracWidth - 64.

Splitting and joining words

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.low_word_toNat {fmt : FloatFormat} (x : Model fmt) : (toWords x).lo.toNat = x.toNatBits % 2 ^ 64

The low storage word is the low 64 bits of the encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.high_word_toNat {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : (toWords x).hi.toNat = x.toNatBits / 2 ^ 64

The high storage word is the encoding shifted down by 64 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.toWords_toNat {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : (toWords x).toNat = x.toNatBits

The two native storage words reconstruct the exact encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.ofWords_toNat {fmt : FloatFormat} (words : Numerics.FixedWord.UInt128) (hfit : words.toNat < 2 ^ fmt.bitWidth) : (ofWords fmt words).toNatBits = words.toNat

Joining two native words reconstructs their value whenever it fits the storage width.

Field extraction

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.signBit_eq {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : signBit fmt (toWords x).hi = x.signBit

Native sign extraction agrees with the public carrier.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.expField_toNat {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : (expField fmt (toWords x).hi).toNat = x.expField

Native exponent extraction agrees with the public carrier.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fraction_toNat {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) : (fracHigh fmt (toWords x).hi).toNat * 2 ^ 64 + (toWords x).lo.toNat = x.fracField

The two fraction limbs reconstruct the public fraction field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.fracHigh_lt {fmt : FloatFormat} (h : Eligible fmt) (high : UInt64) : (fracHigh fmt high).toNat < 2 ^ (fmt.fracWidth - 64)

The high fraction limb occupies at most fracWidth - 64 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.expField_lt {fmt : FloatFormat} (h : Eligible fmt) (high : UInt64) : (expField fmt high).toNat < 2 ^ fmt.expWidth

The native exponent field fits the exponent width.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalExponent_bounds {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) (hnonzero : expField fmt (toWords x).hi ≠ 0) (hnotAllOnes : expField fmt (toWords x).hi ≠ expAllOnes fmt) : 0 < (expField fmt (toWords x).hi).toNat ∧ (expField fmt (toWords x).hi).toNat < fmt.expAllOnesNat

A nonzero, nonexceptional native exponent lies in the normal range.

Normal significands

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalMantissa_toNat {fmt : FloatFormat} (h : Eligible fmt) (high low : UInt64) (hhigh : high.toNat < 2 ^ (fmt.fracWidth - 64)) : (normalMantissa fmt high low).toNat = 2 ^ fmt.fracWidth + high.toNat * 2 ^ 64 + low.toNat

The normal significand is 2^fracWidth plus the two fraction limbs in place.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalMantissa_bounds {fmt : FloatFormat} (h : Eligible fmt) (high low : UInt64) (hhigh : high.toNat < 2 ^ (fmt.fracWidth - 64)) : 2 ^ fmt.fracWidth ≤ (normalMantissa fmt high low).toNat ∧ (normalMantissa fmt high low).toNat < 2 ^ (fmt.fracWidth + 1)

A normal significand occupies exactly fracWidth + 1 bits, including its implicit bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.implicitMantissa_toNat {fmt : FloatFormat} (h : Eligible fmt) : (implicitMantissa fmt).toNat = 2 ^ fmt.fracWidth

The significand 2^fracWidth as two limbs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.carryMantissa_toNat {fmt : FloatFormat} (h : Eligible fmt) : (carryMantissa fmt).toNat = 2 ^ (fmt.fracWidth + 1)

The carried-out significand 2^(fracWidth + 1) as two limbs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.isCarry_iff {fmt : FloatFormat} (h : Eligible fmt) (value : Numerics.FixedWord.UInt128) : isCarry fmt value = true ↔ value.toNat = pow2 (fmt.fracWidth + 1)

The two-limb carry test is exactly the carry produced by fracWidth + 1-bit rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalizeCarry_toNat {fmt : FloatFormat} (h : Eligible fmt) (carry : Bool) (rounded : Numerics.FixedWord.UInt128) : (normalizeCarry fmt carry rounded).toNat = if carry = true then pow2 fmt.fracWidth else rounded.toNat

Carry normalization of a rounded significand is either that significand or 2^fracWidth.

Packing

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.packNormal_eq_ofFields {fmt : FloatFormat} (h : Eligible fmt) (sign : Bool) (exponent : UInt64) (mantissa : Numerics.FixedWord.UInt128) (hexponent : exponent.toNat < 2 ^ fmt.expWidth) (hmantissaLower : 2 ^ fmt.fracWidth ≤ mantissa.toNat) (hmantissaUpper : mantissa.toNat < 2 ^ (fmt.fracWidth + 1)) : packNormal fmt sign exponent mantissa = ofFields fmt sign exponent.toNat (mantissa.toNat - pow2 fmt.fracWidth)

Native packing agrees with the field constructor for a normalized significand and an in-range exponent field.

Finite decoding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.decode_of_normalExponent {fmt : FloatFormat} (h : Eligible fmt) (x : Model fmt) (hexponentZero : expField fmt (toWords x).hi ≠ 0) (hexponentFinite : expField fmt (toWords x).hi ≠ expAllOnes fmt) : FiniteKernel.decode? x = some { sign := signBit fmt (toWords x).hi, exponent := (expField fmt (toWords x).hi).toNat, mantissa := (normalMantissa fmt (fracHigh fmt (toWords x).hi) (toWords x).lo).toNat }

Decode a normal finite value directly from its two native storage words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.normalComponents_toDyadic {fmt : FloatFormat} (h : Eligible fmt) (sign : Bool) (exponent mantissa : ℕ) (hexponent : exponent ≠ 0) (hmantissa : mantissa ≠ 0) : FiniteKernel.Components.toDyadic fmt { sign := sign, exponent := exponent, mantissa := mantissa } = { negative := sign, significand := mantissa, exponent := Int.ofNat exponent - Int.ofNat (fmt.bias + fmt.fracWidth) }

Interpret normal finite-kernel components as their exact dyadic value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativePair.roundScaleExponent {fmt : FloatFormat} (h : Eligible fmt) (exponent : ℕ) : Int.ofNat (exponent + (fmt.bias + fmt.fracWidth - 2)) - Int.ofNat (2 * fmt.ieeeSubnormalAlignExp) = Int.ofNat exponent - Int.ofNat (fmt.bias + fmt.fracWidth)

Normalize the scale used by the product-round kernels.