Wide-limb storage

The limb carrier of Core.Runtime represents the exact-width proof model through a bounded storage invariant. The storage invariant topLimbFits is shown equivalent to the value lying below 2 ^ bitWidth (topLimbFits_iff), which gives the codec laws toModel_ofModel and ofModel_toModel. The field accessors then agree with Model.signBit, Model.expField, and Model.fracField, so the compact finite decoder FiniteKernel.decode? of a stored value is read off the limbs (decode?_toModel). Finally toModel_pack states the exact model that pack produces; every arithmetic kernel of this backend ends in pack, so this is the contract each refinement proof uses. The main storage and packing results are Value.toNat_lt and toModel_pack.

Layout facts

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.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.WideLimb.Eligible.width_gt {fmt : FloatFormat} (h : Eligible fmt) : 128 < fmt.bitWidth

An eligible descriptor is wider than 128 bits.

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

An eligible exponent field fits one machine word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.three_le_bitWidth (fmt : FloatFormat) : 3 ≤ fmt.bitWidth

Every descriptor has at least three encoded bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.bitWidth_le_limbBits (fmt : FloatFormat) : fmt.bitWidth ≤ 32 * limbCount fmt

The limb count covers the encoded width.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.limbBits_lt_bitWidth (fmt : FloatFormat) : 32 * (limbCount fmt - 1) < fmt.bitWidth

The top limb holds at least one encoded bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.limbCount_pos (fmt : FloatFormat) : 0 < limbCount fmt

Every descriptor needs at least one limb; backend eligibility is not required.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.two_pow_bitWidth_le (fmt : FloatFormat) : 2 ^ fmt.bitWidth ≤ Numerics.LimbArray.radix ^ limbCount fmt

The encoded width fits the limbs as a power of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.fracWidth_div_lt (fmt : FloatFormat) : fmt.fracWidth / 32 + 1 ≤ limbCount fmt

The fraction offset lies strictly below the top limb boundary.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.signIndex_div_lt (fmt : FloatFormat) : (fmt.expWidth + fmt.fracWidth) / 32 + 1 ≤ limbCount fmt

The sign offset lies strictly below the top limb boundary.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.bitWidth_eq (fmt : FloatFormat) : fmt.bitWidth = fmt.expWidth + fmt.fracWidth + 1

The bit width is the sign bit plus the exponent and fraction widths.

The storage invariant

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.topLimbFits_iff {fmt : FloatFormat} (v : Numerics.LimbArray) (hsize : v.size = limbCount fmt) : topLimbFits fmt v = true ↔ v.toNat < 2 ^ fmt.bitWidth

The spare-bit test decides whether the value lies below 2 ^ bitWidth.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.Value.size_eq {fmt : FloatFormat} (v : Value fmt) : (↑v).size = limbCount fmt

A stored value has exactly limbCount fmt limbs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.Value.toNat_lt {fmt : FloatFormat} (v : Value fmt) : (↑v).toNat < 2 ^ fmt.bitWidth

A stored value lies below 2 ^ bitWidth.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.ofLimbs_val {fmt : FloatFormat} (w : Numerics.LimbArray) (hsize : w.size = limbCount fmt) (hlt : w.toNat < 2 ^ fmt.bitWidth) : ↑(ofLimbs fmt w) = w

A well-sized array below 2 ^ bitWidth is stored unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toNatBits_toModel {fmt : FloatFormat} (v : Value fmt) : (toModel v).toNatBits = (↑v).toNat

The model of a stored value has the stored bit pattern.

Codec laws

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_ofModel {fmt : FloatFormat} (x : Model fmt) : toModel (ofModel x) = x

Storing and reading back a model value is the identity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.ofModel_toModel {fmt : FloatFormat} (v : Value fmt) : ofModel (toModel v) = v

Reading a stored value and storing it again is the identity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_injective {fmt : FloatFormat} {v w : Value fmt} (h : toModel v = toModel w) : v = w

Two stored values with the same model are equal.

Field access

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.signBit_eq {fmt : FloatFormat} (v : Value fmt) : signBit v = (toModel v).signBit

The stored sign bit is the model sign.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expMask32_toNat {fmt : FloatFormat} (h : fmt.expWidth ≤ 32) : (expMask32 fmt).toNat = 2 ^ fmt.expWidth - 1

The exponent mask has expWidth low bits set, for exponent widths of at most 32.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expAllOnes_toNat {fmt : FloatFormat} (h : fmt.expWidth ≤ 32) : (expAllOnes fmt).toNat = fmt.expAllOnesNat

The all-ones exponent word is the descriptor's all-ones exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.normalExponent_of_expWord {fmt : FloatFormat} (h : Eligible fmt) (v : Value fmt) (hzero : expWord v ≠ 0) (hfinite : expWord v ≠ expAllOnes fmt) : expField v ≠ 0 ∧ expField v ≠ fmt.expAllOnesNat

A nonzero, finite exponent word gives a normal exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expField_eq {fmt : FloatFormat} (v : Value fmt) (h : fmt.expWidth ≤ 32) : expField v = (toModel v).expField

The stored exponent field is the model exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expField_lt {fmt : FloatFormat} (v : Value fmt) (h : fmt.expWidth ≤ 32) : expField v < 2 ^ fmt.expWidth

The exponent field is below 2 ^ expWidth.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.fraction_toNat {fmt : FloatFormat} (v : Value fmt) : (fraction v).toNat = (toModel v).fracField

The fraction limbs denote the model fraction field.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.size_fraction {fmt : FloatFormat} (v : Value fmt) : (fraction v).size = limbCount fmt

The fraction of a stored value has the format's limb count.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.fraction_toNat_lt {fmt : FloatFormat} (v : Value fmt) : (fraction v).toNat < 2 ^ fmt.fracWidth

The fraction limbs lie below 2 ^ fracWidth.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.normalMantissa_toNat {fmt : FloatFormat} (v : Value fmt) : (normalMantissa v).toNat = 2 ^ fmt.fracWidth + (toModel v).fracField

The normal significand is the fraction with the implicit bit.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.size_normalMantissa {fmt : FloatFormat} (v : Value fmt) : (normalMantissa v).size = limbCount fmt

The normal significand, fraction plus implicit bit, has the format's limb count.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.normalMantissa_bounds {fmt : FloatFormat} (v : Value fmt) : 2 ^ fmt.fracWidth ≤ (normalMantissa v).toNat ∧ (normalMantissa v).toNat < 2 ^ (fmt.fracWidth + 1)

The normal significand occupies exactly fracWidth + 1 bits.

Finite decoding

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.isFinite_toModel {fmt : FloatFormat} (v : Value fmt) (hieee : fmt.isIEEE = true) (h : fmt.expWidth ≤ 32) : (toModel v).isFinite = (expField v != fmt.expAllOnesNat)

For a conventional IEEE descriptor, finiteness is the exponent field being below all ones.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.decode?_toModel {fmt : FloatFormat} (v : Value fmt) (hieee : fmt.isIEEE = true) (h : fmt.expWidth ≤ 32) (hfinite : expField v ≠ fmt.expAllOnesNat) : FiniteKernel.decode? (toModel v) = some { sign := signBit v, exponent := expField v, mantissa := FiniteKernel.decodeMantissa fmt (expField v) (fraction v).toNat }

The compact finite decoder of a stored value with a finite exponent field reads its sign, exponent, and significand from the limbs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.decodeMantissa_eq_normalMantissa {fmt : FloatFormat} (v : Value fmt) (hnormal : expField v ≠ 0) : FiniteKernel.decodeMantissa fmt (expField v) (fraction v).toNat = (normalMantissa v).toNat

The decoded significand of a normal stored value is its limb significand.

Packing

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.expWord_and_mask_toNat {fmt : FloatFormat} (exponent : UInt32) (h : fmt.expWidth ≤ 32) : (exponent &&& expMask32 fmt).toNat = exponent.toNat % 2 ^ fmt.expWidth

The exponent word masked to the exponent field.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.pack_limbs_toNat {fmt : FloatFormat} (sign : Bool) (exponent : UInt32) (fraction : Numerics.LimbArray) (h : fmt.expWidth ≤ 32) : have base := (fraction.lowBits fmt.fracWidth).resize (limbCount fmt); have withExponent := base.addAt fmt.fracWidth (exponent &&& expMask32 fmt); have limbs := if sign = true then withExponent.addAt (fmt.expWidth + fmt.fracWidth) 1 else withExponent; (limbs.toNat = fraction.toNat % 2 ^ fmt.fracWidth + exponent.toNat % 2 ^ fmt.expWidth * 2 ^ fmt.fracWidth + if sign = true then 2 ^ (fmt.expWidth + fmt.fracWidth) else 0) ∧ limbs.size = limbCount fmt ∧ limbs.toNat < 2 ^ fmt.bitWidth

The limbs produced by pack, before the storage wrapper.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_pack {fmt : FloatFormat} (sign : Bool) (exponent : UInt32) (fraction : Numerics.LimbArray) (h : fmt.expWidth ≤ 32) : toModel (pack fmt sign exponent fraction) = ofFields fmt sign (exponent.toNat % 2 ^ fmt.expWidth) (fraction.toNat % 2 ^ fmt.fracWidth)

pack produces exactly the model field constructor on the masked fields.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.WideLimb.toModel_pack_of_lt {fmt : FloatFormat} (sign : Bool) (exponent : UInt32) (fraction : Numerics.LimbArray) (h : fmt.expWidth ≤ 32) (hexp : exponent.toNat < 2 ^ fmt.expWidth) (hfrac : fraction.toNat < 2 ^ fmt.fracWidth) : toModel (pack fmt sign exponent fraction) = ofFields fmt sign exponent.toNat fraction.toNat

pack on in-range fields produces exactly the model field constructor.