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 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 result is Value.toNat_lt.

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 has at most 32 bits.

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, eligible or not.

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

Masking an exponent word keeps its value modulo 2 ^ expWidth.

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 that pack builds, before the storage wrapper, denote the masked fields.

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 is 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

On in-range fields, pack is the model field constructor.